MatrixGraphMomentBounds.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Finite matrix samples with bounded graph cost

The matrix-stage centralizer identities preserve the two second moments and the diagonal fourth moments. Relative irreducibility supplies the mixed-moment limits. Thus the bound of ten is attained by an actual finite stage and a finite independent sample family.

theorem OAI.KadisonKastler.expect_comp_equiv line 23
theorem OAI.KadisonKastler.expect_pair_comp_equiv line 27
theorem OAI.KadisonKastler.firstMoment_comp_equiv line 35
theorem OAI.KadisonKastler.thirdMoment_comp_equiv line 41
theorem OAI.KadisonKastler.star_matrixOrbitSample line 48
Source documentation
Taking adjoints exchanges the two independent matrix samples.
```
theorem star_matrixOrbitSample {d : ℕ}
    (E : Generator.MatrixUnitSystem (Fin d) (H →L[ℂ] H))
    (x : H →L[ℂ] H) (g : MatrixOrbitIndex d) :
    star (matrixOrbitSample E x g) = matrixOrbitSample E (star x) g.swap := by
…
```
Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.MatrixOrbitIndex, OAI.KadisonKastler.matrixOrbitSample
theorem OAI.KadisonKastler.state_conj line 55
Distinct definitions of this name: OAI/Analysis/KadisonKastler/MatrixOrbitSampleLaw.lean:48 (different declaration text). Qualify references as OAI.KadisonKastler.state_conj@path.

theorem OAI.KadisonKastler.matrixOrbit_right_second line 73

Source documentation

Every actual matrix sample has the original right second moment.

theorem matrixOrbit_right_second (M : VonNeumannAlgebra H) (Ω : H) {d : ℕ}
    (E : Generator.MatrixUnitSystem (Fin d) (H →L[ℂ] H))
    (hEM : E.algebra ≤ M.toStarSubalgebra)
    (hc : ∀ a ∈ E.algebra, ∀ z ∈ M,
      inner ℂ Ω ((a * z) Ω) = inner ℂ Ω ((z * a) Ω))
    (x : H →L[ℂ] H) (hx : x ∈ M) (g : MatrixOrbitIndex d) :
    realVectorState Ω (star (matrixOrbitSample E x g) * matrixOrbitSample E x g) =
      ‖x Ω‖ ^ 2 := by
…

Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.MatrixOrbitIndex, OAI.KadisonKastler.realVectorState, OAI.KadisonKastler.matrixOrbitSample

theorem OAI.KadisonKastler.matrixOrbit_left_second line 86

Source documentation

The left second moment is preserved as well.

theorem matrixOrbit_left_second (M : VonNeumannAlgebra H) (Ω : H) {d : ℕ}
    (E : Generator.MatrixUnitSystem (Fin d) (H →L[ℂ] H))
    (hEM : E.algebra ≤ M.toStarSubalgebra)
    (hc : ∀ a ∈ E.algebra, ∀ z ∈ M,
      inner ℂ Ω ((a * z) Ω) = inner ℂ Ω ((z * a) Ω))
    (x : H →L[ℂ] H) (hx : x ∈ M) (g : MatrixOrbitIndex d) :
    realVectorState Ω (matrixOrbitSample E x g * star (matrixOrbitSample E x g)) =
      ‖star x Ω‖ ^ 2 := by
…

Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.MatrixOrbitIndex, OAI.KadisonKastler.realVectorState, OAI.KadisonKastler.matrixOrbitSample

theorem OAI.KadisonKastler.left_positive_state line 98
theorem OAI.KadisonKastler.matrixOrbit_firstMoment_tendsto line 118
Source documentation
The first actual sample pairing converges to the square of its right second moment.
```
theorem matrixOrbit_firstMoment_tendsto :
    Tendsto (fun j => orbitFirstPairMoment Ω (matrixOrbitSample (E j) x)) atTop
      (𝓝 ((‖x Ω‖ ^ 2) ^ 2)) := by
…
```
Mentions: OAI.KadisonKastler.orbitFirstPairMoment, OAI.KadisonKastler.matrixOrbitSample
theorem OAI.KadisonKastler.matrixOrbit_thirdMoment_tendsto line 133
Source documentation
The positive mixed pairing converges to the product of the right and left second moments.
```
theorem matrixOrbit_thirdMoment_tendsto :
    Tendsto (fun j => orbitThirdPairMoment Ω (matrixOrbitSample (E j) x)) atTop
      (𝓝 (‖x Ω‖ ^ 2 * ‖star x Ω‖ ^ 2)) := by
…
```
Mentions: OAI.KadisonKastler.orbitThirdPairMoment, OAI.KadisonKastler.matrixOrbitSample

theorem OAI.KadisonKastler.matrixOrbit_graphPairing_tendsto line 148

Source documentation

The full off-diagonal cost has its required actual scalar limit.

theorem matrixOrbit_graphPairing_tendsto (k : ℝ) :
    Tendsto (fun j =>
      orbitFirstPairMoment Ω (matrixOrbitSample (E j) x) +
      2 * orbitThirdPairMoment Ω (matrixOrbitSample (E j) x) +
      k * (orbitFirstPairMoment Ω (fun g => star (matrixOrbitSample (E j) x g)) +
        2 * orbitThirdPairMoment Ω (fun g => star (matrixOrbitSample (E j) x g)))) atTop
      (𝓝 ((‖x Ω‖ ^ 2) ^ 2 + k * (‖star x Ω‖ ^ 2) ^ 2 +
        2 * (k + 1) * ‖x Ω‖ ^ 2 * ‖star x Ω‖ ^ 2)) := by
…

Mentions: OAI.KadisonKastler.orbitFirstPairMoment, OAI.KadisonKastler.matrixOrbitSample, OAI.KadisonKastler.orbitThirdPairMoment

theorem OAI.KadisonKastler.exists_matrixOrbit_graphCost_le_ten line 182
Source documentation
There is a genuine finite matrix stage and a positive sample size whose independently sampled signed graph cost is at most ten.
```
theorem exists_matrixOrbit_graphCost_le_ten {k : ℝ} (hk : 1 ≤ k)
    (hxnorm : ‖x Ω‖ ^ 2 + k * ‖star x Ω‖ ^ 2 = 1) :
    ∃ j m, 1 ≤ m ∧
      (𝔼 ω : Fin m → MatrixOrbitIndex (d j), 𝔼 ε : Fin m → Bool,
        graphMomentCost Ω k
          (normalizedFiniteSignSum (fun i => matrixOrbitSample (E j) x (ω i)) ε)) ≤ 10 := by
…
```
Mentions: OAI.KadisonKastler.MatrixOrbitIndex, OAI.KadisonKastler.graphMomentCost, OAI.KadisonKastler.normalizedFiniteSignSum, OAI.KadisonKastler.matrixOrbitSample