import RNLAPhaseB.B3Base
import RNLAPhaseB.Complexity

open MeasureTheory
open scoped Matrix
open scoped Matrix.Norms.L2Operator
open scoped BigOperators
open scoped ENNReal
open scoped ComplexOrder

namespace RNLAPhaseB.HMT2011.SpecNormSum

/-- HMT Proposition (prop:spec-norm-sum): for each partitioned psd matrix
`M = [[A, B], [B^*, C]]`, the spectral norm satisfies `‖M‖ ≤ ‖A‖ + ‖C‖`.

`‖·‖` is the spectral (ℓ₂ operator) norm, via the scoped instance
`Matrix.Norms.L2Operator`. The partitioned matrix is `Matrix.fromBlocks A B Bᴴ C`,
where `Bᴴ` is the conjugate transpose (the source's `B^*`). "psd" is
`Matrix.PosSemidef`, which includes Hermitian-ness. It uses the standard `ComplexOrder`
partial order on the `RCLike` scalars, so `0 ≤ x^* M x` means the quadratic form is real
and nonnegative. The scalar field is any `RCLike` field, which covers both the real and
the complex case. The block sizes are arbitrary finite index types. -/
theorem spec_norm_sum_of_psd_partitioned
    {𝕜 : Type*} [RCLike 𝕜]
    {m n : Type*} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n]
    (A : Matrix m m 𝕜) (B : Matrix m n 𝕜) (C : Matrix n n 𝕜)
    (hM : (Matrix.fromBlocks A B Bᴴ C).PosSemidef) :
    ‖Matrix.fromBlocks A B Bᴴ C‖ ≤ ‖A‖ + ‖C‖ := by
  sorry

end RNLAPhaseB.HMT2011.SpecNormSum