GraphRowMetric.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The normalized graph metric of a rectangular operator row

The second graph coordinate loses its rescaling factor after summing the adjoint column. This is the exact matrix-level estimate used with complete near-inclusion, without an ordinary-gap amplification claim.

theorem OAI.KadisonKastler.finiteRMS_apply_le line 24

Source documentation

A continuous operator acts contractively on finite RMS up to its norm.

theorem finiteRMS_apply_le {I K : Type*} [Fintype I]
    [NormedAddCommGroup K] [InnerProductSpace ℂ K]
    (T : H →L[ℂ] K) (v : I → H) :
    finiteRMS (fun i => T (v i)) ≤ ‖T‖ * finiteRMS v := by
…

Mentions: OAI.KadisonKastler.finiteRMS

theorem OAI.KadisonKastler.finiteRMS_eq_of_norm_eq line 36
Source documentation
Constant pointwise norm gives the same norm in finite RMS.
```
theorem finiteRMS_eq_of_norm_eq {I : Type*} [Fintype I] [Nonempty I]
    (v : I → H) {C : ℝ} (hC : 0 ≤ C) (hv : ∀ i, ‖v i‖ = C) : finiteRMS v = C := by
…
```
Mentions: OAI.KadisonKastler.finiteRMS
theorem OAI.KadisonKastler.graphRowRMS_sq_le line 43
Source documentation
At rescaling sqrt(k), the normalized squared graph norm is controlled by twice the squared rectangular row norm.
```
theorem graphRowRMS_sq_le {k : ℕ} (hk : 0 < k)
    (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H) (Y : Fin k → H →L[ℂ] H) :
    (finiteRMS (fun i => rescaledGraphVector J Ω (Real.sqrt (k : ℝ)) (Y i))) ^ 2 ≤
      2 * ‖operatorRow Y‖ ^ 2 * ‖Ω‖ ^ 2 := by
…
```
Mentions: OAI.KadisonKastler.finiteRMS, OAI.KadisonKastler.rescaledGraphVector, OAI.KadisonKastler.operatorRow

theorem OAI.KadisonKastler.graphRowRMS_le line 72

Source documentation

The rectangular row estimate in norm form.

theorem graphRowRMS_le {k : ℕ} (hk : 0 < k)
    (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H) (Y : Fin k → H →L[ℂ] H) :
    finiteRMS (fun i => rescaledGraphVector J Ω (Real.sqrt (k : ℝ)) (Y i)) ≤
      Real.sqrt 2 * ‖operatorRow Y‖ * ‖Ω‖ := by
…

Mentions: OAI.KadisonKastler.finiteRMS, OAI.KadisonKastler.rescaledGraphVector, OAI.KadisonKastler.operatorRow