GraphRowMoments.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Moments of a finite replicated graph row

The row consists of independently chosen left matrix translates of the same clipped element. Its two fourth-moment sums reduce to the actual matrix averages already shown to converge to the vector state.

def OAI.KadisonKastler.graphRowSquare line 24
Source documentation
The positive left square of an operator row.
```
def graphRowSquare {I : Type*} [Fintype I] (Y : I → H →L[ℂ] H) : H →L[ℂ] H :=
…
```
def OAI.KadisonKastler.graphRowCost line 28
Source documentation
The fourth-moment cost controlling both rescaled row coordinates.
```
def graphRowCost (Ω : H) {I : Type*} [Fintype I] (Y : I → H →L[ℂ] H) : ℝ :=
…
```
def OAI.KadisonKastler.matrixGraphRow line 33
Source documentation
The concrete row of independently sampled left matrix translates.
```
def matrixGraphRow {I : Type*} {d : ℕ}
    (E : Generator.MatrixUnitSystem (Fin d) (H →L[ℂ] H)) (z : H →L[ℂ] H)
    (ω : I → SignedPermutation (Fin d)) (i : I) : H →L[ℂ] H :=
…
```
Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.SignedPermutation
theorem OAI.KadisonKastler.re_finiteAverage line 38
theorem OAI.KadisonKastler.realState_conj line 46
theorem OAI.KadisonKastler.leftTranslate_left_square line 59
theorem OAI.KadisonKastler.leftTranslate_pair line 64
theorem OAI.KadisonKastler.leftTranslate_pair_diagonal line 72

theorem OAI.KadisonKastler.graphRowCost_eq_pair_sums line 80

Source documentation

Expanding the actual row cost yields two independent pair sums.

theorem graphRowCost_eq_pair_sums (Ω : H) {I : Type*} [Fintype I]
    (Y : I → H →L[ℂ] H) :
    graphRowCost Ω Y =
      (∑ i, ∑ j, realVectorState Ω ((Y i * star (Y i)) * (Y j * star (Y j)))) +
      (Fintype.card I : ℝ)⁻¹ *
        ∑ i, ∑ j, realVectorState Ω (star (Y i) * (Y j * star (Y j)) * Y i) := by
…

Mentions: OAI.KadisonKastler.graphRowCost, OAI.KadisonKastler.realVectorState

theorem OAI.KadisonKastler.expect_matrixGraphRow_cost line 93

Source documentation

The finite independent sampling law gives the exact expected cost of the replicated row, before any limiting estimate.

theorem expect_matrixGraphRow_cost (M : VonNeumannAlgebra H) (Ω : H)
    {I : Type*} [Fintype I] [DecidableEq I] [Nonempty I] {d : ℕ}
    (E : Generator.MatrixUnitSystem (Fin d) (H →L[ℂ] H))
    (hEM : E.algebra ≤ M.toStarSubalgebra)
    (hc : ∀ a ∈ E.algebra, ∀ x ∈ M,
      inner ℂ Ω ((a * x) Ω) = inner ℂ Ω ((x * a) Ω))
    (z : H →L[ℂ] H) (hz : z ∈ M) :
    (𝔼 ω : I → SignedPermutation (Fin d), graphRowCost Ω (matrixGraphRow E z ω)) =
      (Fintype.card I : ℝ) * realVectorState Ω ((z * star z) ^ 2) +
      (Fintype.card I : ℝ) * ((Fintype.card I : ℝ) - 1) *
        realVectorState Ω ((z * star z) * matrixUnitAverage E (z * star z)) +
      realVectorState Ω ((star z * z) ^ 2) +
…

Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.SignedPermutation, OAI.KadisonKastler.graphRowCost, OAI.KadisonKastler.matrixGraphRow, OAI.KadisonKastler.realVectorState, OAI.KadisonKastler.matrixUnitAverage

theorem OAI.KadisonKastler.realVectorState_fourth_le_norm_sq line 159
Source documentation
A bounded operator controls the fourth vector-state moment by its second moment, without a trace assumption.
```
theorem realVectorState_fourth_le_norm_sq (Ω : H) (z : H →L[ℂ] H) :
    realVectorState Ω ((star z * z) ^ 2) ≤ ‖z‖ ^ 2 * ‖z Ω‖ ^ 2 := by
…
```
Mentions: OAI.KadisonKastler.realVectorState
theorem OAI.KadisonKastler.realVectorState_reverse_fourth_le_norm_sq line 170
Source documentation
The corresponding bound holds for the left square.
```
theorem realVectorState_reverse_fourth_le_norm_sq (Ω : H) (z : H →L[ℂ] H) :
    realVectorState Ω ((z * star z) ^ 2) ≤ ‖z‖ ^ 2 * ‖star z Ω‖ ^ 2 := by
…
```
Mentions: OAI.KadisonKastler.realVectorState

theorem OAI.KadisonKastler.matrixGraphRow_cost_tendsto line 175

Source documentation

The exact limiting cost of the independent replicated row.

theorem matrixGraphRow_cost_tendsto (M : VonNeumannAlgebra H) (Ω : H) (hΩ : ‖Ω‖ = 1)
    {I : Type*} [Fintype I] [DecidableEq I] [Nonempty I]
    (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) Ω))
    (z : H →L[ℂ] H) (hz : z ∈ M) :
    Tendsto (fun n => 𝔼 ω : I → SignedPermutation (Fin (d n)),
      graphRowCost Ω (matrixGraphRow (E n) z ω)) atTop
…

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