GraphMomentBounds.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Expected costs before graph clipping

The cost uses the actual vector state and the two fourth powers. The finite-sample estimate retains the diagonal correction, so increasing the number of samples removes the diagonal cost. The final scalar lemma chooses a stage and a sample size from convergence of the mixed moments.

def OAI.KadisonKastler.graphMomentCost line 29
Source documentation
The nonnegative cost appearing before graph-vector clipping.
```
def graphMomentCost (Ω : H) (k : ℝ) (x : H →L[ℂ] H) : ℝ :=
…
```
theorem OAI.KadisonKastler.operatorVectorState_star_mul_self line 34
Source documentation
The exact complex value of the positive vector-state square.
```
theorem operatorVectorState_star_mul_self (Ω : H) (x : H →L[ℂ] H) :
    operatorVectorState Ω (star x * x) = (‖x Ω‖ ^ 2 : ℝ) := by
…
```
Mentions: OAI.KadisonKastler.operatorVectorState
theorem OAI.KadisonKastler.normalizedFiniteSignSum_apply line 45
Source documentation
Applying an operator sign sum to a vector is the Hilbert sign sum.
```
theorem normalizedFiniteSignSum_apply (a : I → H →L[ℂ] H) (ε : I → Bool) (Ω : H) :
    (normalizedFiniteSignSum a ε) Ω =
      normalizedHilbertSignSum (fun i => a i Ω) ε := by
…
```
Mentions: OAI.KadisonKastler.normalizedFiniteSignSum, OAI.KadisonKastler.normalizedHilbertSignSum

theorem OAI.KadisonKastler.expect_normalizedSignSum_vector_second line 52

Source documentation

The exact second moment holds for the vector state, without traciality.

theorem expect_normalizedSignSum_vector_second (Ω : H) (a : I → H →L[ℂ] H) :
    (𝔼 ε : I → Bool,
      realVectorState Ω (star (normalizedFiniteSignSum a ε) * normalizedFiniteSignSum a ε)) =
      (Fintype.card I : ℝ)⁻¹ * ∑ i, realVectorState Ω (star (a i) * a i) := by
…

Mentions: OAI.KadisonKastler.realVectorState, OAI.KadisonKastler.normalizedFiniteSignSum

theorem OAI.KadisonKastler.star_normalizedSignSum line 60

theorem OAI.KadisonKastler.expect_sampledNormalizedSignSum_vector_second line 66

Source documentation

The second moment after independent sampling is the single-sample second moment.

theorem expect_sampledNormalizedSignSum_vector_second
    [Nonempty I] (Ω : H) (a : G → H →L[ℂ] H) :
    (𝔼 ω : I → G, 𝔼 ε : I → Bool,
      realVectorState Ω (star (normalizedFiniteSignSum (fun i => a (ω i)) ε) *
        normalizedFiniteSignSum (fun i => a (ω i)) ε)) =
      𝔼 g, realVectorState Ω (star (a g) * a g) := by
…

Mentions: OAI.KadisonKastler.realVectorState, OAI.KadisonKastler.normalizedFiniteSignSum

theorem OAI.KadisonKastler.expect_sampledNormalizedSignSum_vector_left_second line 81

Source documentation

The left square has the corresponding exact second moment.

theorem expect_sampledNormalizedSignSum_vector_left_second
    [Nonempty I] (Ω : H) (a : G → H →L[ℂ] H) :
    (𝔼 ω : I → G, 𝔼 ε : I → Bool,
      realVectorState Ω (normalizedFiniteSignSum (fun i => a (ω i)) ε *
        star (normalizedFiniteSignSum (fun i => a (ω i)) ε))) =
      𝔼 g, realVectorState Ω (a g * star (a g)) := by
…

Mentions: OAI.KadisonKastler.realVectorState, OAI.KadisonKastler.normalizedFiniteSignSum

def OAI.KadisonKastler.orbitSecondMoment line 91
Source documentation
The four scalar statistics needed for the expected graph cost.
```
def orbitSecondMoment (Ω : H) (k : ℝ) (a : G → H →L[ℂ] H) : ℝ :=
…
```
def OAI.KadisonKastler.orbitDiagonalMoment line 95
def OAI.KadisonKastler.orbitFirstPairMoment line 98
def OAI.KadisonKastler.orbitThirdPairMoment line 101

theorem OAI.KadisonKastler.expect_sampled_graphMomentCost_le line 106

Source documentation

The actual cost of independently sampled normalized sign sums is bounded by its single-sample, diagonal, and off-diagonal moments.

theorem expect_sampled_graphMomentCost_le [Nonempty I]
    (Ω : H) {k : ℝ} (hk : 0 ≤ k) (a : G → H →L[ℂ] H) :
    (𝔼 ω : I → G, 𝔼 ε : I → Bool,
      graphMomentCost Ω k (normalizedFiniteSignSum (fun i => a (ω i)) ε)) ≤
      orbitSecondMoment Ω k a +
      (orbitDiagonalMoment Ω a + k * orbitDiagonalMoment Ω (fun g => star (a g))) /
        Fintype.card I +
      (1 - (Fintype.card I : ℝ)⁻¹) *
        (orbitFirstPairMoment Ω a + 2 * orbitThirdPairMoment Ω a +
          k * (orbitFirstPairMoment Ω (fun g => star (a g)) +
            2 * orbitThirdPairMoment Ω (fun g => star (a g)))) := by
…

Mentions: OAI.KadisonKastler.graphMomentCost, OAI.KadisonKastler.normalizedFiniteSignSum, OAI.KadisonKastler.orbitSecondMoment, OAI.KadisonKastler.orbitDiagonalMoment, OAI.KadisonKastler.orbitFirstPairMoment, OAI.KadisonKastler.orbitThirdPairMoment

theorem OAI.KadisonKastler.graph_pairing_scalar_le_six line 141

Source documentation

The scalar off-diagonal cost stays bounded uniformly in the graph rescaling when α + k β = 1 and k ≥ 1.

theorem graph_pairing_scalar_le_six {α β k : ℝ}
    (hα : 0 ≤ α) (hβ : 0 ≤ β) (hk : 1 ≤ k) (hn : α + k * β ≤ 1) :
    α ^ 2 + k * β ^ 2 + 2 * (k + 1) * α * β ≤ 6 := by
…

theorem OAI.KadisonKastler.exists_stage_sample_cost_le_ten line 162

Source documentation

A convergent off-diagonal statistic and a fixed diagonal bound give an actual finite stage and sample size with expected cost at most ten.

theorem exists_stage_sample_cost_le_ten
    (C : ℕ → ℕ → ℝ) (T : ℕ → ℝ) {D L : ℝ}
    (hL0 : 0 ≤ L) (hL : L ≤ 6) (hT : Tendsto T atTop (𝓝 L))
    (hC : ∀ j m, 1 ≤ m →
      C j m ≤ 1 + D / m + (1 - (m : ℝ)⁻¹) * T j) :
    ∃ j m, 1 ≤ m ∧ C j m ≤ 10 := by
…