GraphScaleRows.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Uniform row flattening at arbitrary large rescalings

Rounding the squared rescaling up changes the moment normalization by at most a factor two. The same fixed row cutoff remains sufficient.

theorem OAI.KadisonKastler.rowLimit_numeric_bound_480 line 21

theorem OAI.KadisonKastler.exists_matrixGraphRow_cost_le_480 line 41

Source documentation

For every flattened element, an actual finite matrix-orbit row has uniformly bounded cost. The row length is exactly the square rescaling.

theorem exists_matrixGraphRow_cost_le_480
    (M : VonNeumannAlgebra H) (Ω : H) (hΩ : ‖Ω‖ = 1)
    (d : ℕ → ℕ) (E : ∀ n, Generator.MatrixUnitSystem (Fin (d n)) (H →L[ℂ] H))
    (hmono : Monotone (fun n => (E n).algebra))
    (hEM : ∀ n, (E n).algebra ≤ M.toStarSubalgebra)
    (hirr : ∀ T ∈ M, (∀ n a, a ∈ (E n).algebra → a * T = T * a) →
      ∃ c : ℂ, T = c • (1 : H →L[ℂ] H))
    (hc : ∀ n a, a ∈ (E n).algebra → ∀ x ∈ M,
      inner ℂ Ω ((a * x) Ω) = inner ℂ Ω ((x * a) Ω))
    {k : ℕ} (hk : 0 < k) (z : H →L[ℂ] H) (hz : z ∈ M)
    (hznorm : ‖z‖ ≤ 128) (hzsize : ‖z Ω‖ ^ 2 + k * ‖star z Ω‖ ^ 2 ≤ 480) :
    ∃ j, ∃ ω : Fin k → SignedPermutation (Fin (d j)),
…

Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.SignedPermutation

theorem OAI.KadisonKastler.norm_rescaledGraphVector_mono_square line 78

Source documentation

Increasing the square of the graph scale increases its norm.

theorem norm_rescaledGraphVector_mono_square
    (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H) {c b : ℝ} (hcb : c ^ 2 ≤ b ^ 2)
    (x : H →L[ℂ] H) :
    ‖rescaledGraphVector J Ω c x‖ ≤ ‖rescaledGraphVector J Ω b x‖ := by
…

Mentions: OAI.KadisonKastler.rescaledGraphVector

theorem OAI.KadisonKastler.clippedGraphRow_error_le_scale line 88
Source documentation
At a scale whose square is at most the row length, the same cutoff has the same normalized graph error bound.
```
theorem clippedGraphRow_error_le_scale {k : ℕ} (hk : 0 < k)
    (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H) {c : ℝ} (hc : c ^ 2 ≤ (k : ℝ))
    (Y : Fin k → H →L[ℂ] H) (hcost : graphRowCost Ω Y ≤ 16777216) :
    finiteRMS (fun i => rescaledGraphVector J Ω c
      (Y i - clippedGraphRow 131072 Y i)) ≤ 1 / 32 := by
…
```
Mentions: OAI.KadisonKastler.graphRowCost, OAI.KadisonKastler.finiteRMS, OAI.KadisonKastler.rescaledGraphVector, OAI.KadisonKastler.clippedGraphRow

theorem OAI.KadisonKastler.clippedGraphRow_signal_le_scale line 99

Source documentation

The retained signal estimate at every graph scale up to sqrt(k).

theorem clippedGraphRow_signal_le_scale {k : ℕ} (hk : 0 < k)
    (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H) {c : ℝ} (hc : c ^ 2 ≤ (k : ℝ))
    (T : TomitaGraphHilbert H →L[ℂ] TomitaGraphHilbert H)
    (Y : Fin k → H →L[ℂ] H) (hcost : graphRowCost Ω Y ≤ 16777216)
    (hsignal : ‖T‖ / 8 ≤ finiteRMS (fun i => T (rescaledGraphVector J Ω c (Y i)))) :
    ‖T‖ / 16 ≤ finiteRMS (fun i =>
      T (rescaledGraphVector J Ω c (clippedGraphRow 131072 Y i))) := by
…

Mentions: OAI.KadisonKastler.TomitaGraphHilbert, OAI.KadisonKastler.graphRowCost, OAI.KadisonKastler.finiteRMS, OAI.KadisonKastler.rescaledGraphVector, OAI.KadisonKastler.clippedGraphRow

theorem OAI.KadisonKastler.graphRowRMS_le_scale line 126
Source documentation
The normalized graph metric is controlled by the whole row norm at any graph scale whose square is at most its length.
```
theorem graphRowRMS_le_scale {k : ℕ} (hk : 0 < k)
    (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H) {c : ℝ} (hc : c ^ 2 ≤ (k : ℝ))
    (Y : Fin k → H →L[ℂ] H) :
    finiteRMS (fun i => rescaledGraphVector J Ω c (Y i)) ≤
      Real.sqrt 2 * ‖operatorRow Y‖ * ‖Ω‖ := by
…
```
Mentions: OAI.KadisonKastler.finiteRMS, OAI.KadisonKastler.rescaledGraphVector, OAI.KadisonKastler.operatorRow