Projection bound through matrix powers

import RNLAPhaseB.B3Base
import RNLAPhaseB.Complexity

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

namespace RNLAPhaseB.HMT2011.PropProjPower

/-- `P` is an orthogonal projector: idempotent and self-adjoint. -/
def IsOrthogonalProjector {𝕜 : Type*} [RCLike 𝕜] {m : ℕ}
    (P : Matrix (Fin m) (Fin m) 𝕜) : Prop :=
  P * P = P ∧ Pᴴ = P

/-- The real power `A ^ q` of a square matrix, defined by the continuous functional
calculus `cfc (fun x => x ^ q) A`. For a Hermitian `A = U diag(λ) U^*` this is
`U diag(λ^q) U^*`. It is used below only for the psd matrix `A = M Mᴴ`, whose
eigenvalues are nonnegative, so `λ ^ q` is the ordinary real power. -/
noncomputable def psdRpow {𝕜 : Type*} [RCLike 𝕜] {m : ℕ}
    (A : Matrix (Fin m) (Fin m) 𝕜) (q : ℝ) : Matrix (Fin m) (Fin m) 𝕜 :=
  cfc (fun x : ℝ => x ^ q) A

/-- Sanity check: for natural-number exponents, `psdRpow (M Mᴴ) k` is the ordinary
monoid power `(M Mᴴ) ^ k`. -/
theorem psdRpow_natCast {𝕜 : Type*} [RCLike 𝕜] {m n : ℕ}
    (M : Matrix (Fin m) (Fin n) 𝕜) (k : ℕ) :
    psdRpow (M * Mᴴ) (k : ℝ) = (M * Mᴴ) ^ k := by
  unfold psdRpow
  have h : IsSelfAdjoint (M * Mᴴ) := by
    simpa [IsSelfAdjoint, Matrix.star_eq_conjTranspose] using
      (Matrix.isHermitian_mul_conjTranspose_self M)
  simp only [Real.rpow_natCast]
  rw [cfc_pow_id (M * Mᴴ) k h]

/-- HMT 2011, Proposition (prop:proj-power). Let `P` be an orthogonal projector and
let `M` be a matrix. For each positive number `q`,
`‖P M‖ ≤ ‖P (M M^*)^q M‖^{1/(2q+1)}`, where `‖·‖` is the spectral (ℓ₂ operator) norm.
The source says "each positive number q" and does not restrict `q` to integers, so
`q` ranges over real numbers `q > 0`. `(M M^*)^q` is the real power of the psd matrix
`M Mᴴ`, given by the functional calculus (`psdRpow`). For natural `q` it coincides
with the monoid power (`psdRpow_natCast`). -/
theorem proj_power {𝕜 : Type*} [RCLike 𝕜] {m n : ℕ}
    (P : Matrix (Fin m) (Fin m) 𝕜) (hP : IsOrthogonalProjector P)
    (M : Matrix (Fin m) (Fin n) 𝕜) (q : ℝ) (hq : 0 < q) :
    ‖P * M‖ ≤ ‖P * psdRpow (M * Mᴴ) q * M‖ ^ ((1 : ℝ) / (2 * q + 1)) := by
  sorry

end RNLAPhaseB.HMT2011.PropProjPower