IndependentOrbitMoments.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Fourth moments for independently sampled operator coefficients

The diagonal correction in the sign expansion is retained before the independent samples are averaged. Consequently its coefficient is 1/m, while the two off-diagonal pairings have coefficient 1-1/m.

theorem OAI.KadisonKastler.expect_sampledSignSum_vector_fourth_le line 24

Source documentation

Exact diagonal counting and the crossed-pairing inequality give the unnormalized sampled fourth-moment estimate.

theorem expect_sampledSignSum_vector_fourth_le
    (Ω : H) (a : G → H →L[ℂ] H) :
    (𝔼 ω : I → G, 𝔼 ε : I → Bool,
      realVectorState Ω ((star (finiteSignSum (fun i => a (ω i)) ε) *
        finiteSignSum (fun i => a (ω i)) ε) ^ 2)) ≤
      (Fintype.card I : ℝ) * (𝔼 g, realVectorState Ω ((star (a g) * a g) ^ 2)) +
      (Fintype.card I : ℝ) * ((Fintype.card I : ℝ) - 1) *
        ((𝔼 g, 𝔼 h, realVectorState Ω ((star (a g) * a g) * (star (a h) * a h))) +
          2 * (𝔼 g, 𝔼 h, realVectorState Ω
            ((star (a g) * a h) * (star (a h) * a g)))) := by
…

Mentions: OAI.KadisonKastler.realVectorState, OAI.KadisonKastler.finiteSignSum

theorem OAI.KadisonKastler.vector_fourth_smul line 79

theorem OAI.KadisonKastler.expect_sampledNormalizedSignSum_vector_fourth_le line 90

Source documentation

Normalizing by the sample size yields the exact 1/m diagonal cost and the two independent off-diagonal moments.

theorem expect_sampledNormalizedSignSum_vector_fourth_le
    (Ω : H) (a : G → H →L[ℂ] H) :
    (𝔼 ω : I → G, 𝔼 ε : I → Bool,
      realVectorState Ω ((star (normalizedFiniteSignSum (fun i => a (ω i)) ε) *
        normalizedFiniteSignSum (fun i => a (ω i)) ε) ^ 2)) ≤
      (𝔼 g, realVectorState Ω ((star (a g) * a g) ^ 2)) / Fintype.card I +
      (1 - (Fintype.card I : ℝ)⁻¹) *
        ((𝔼 g, 𝔼 h, realVectorState Ω ((star (a g) * a g) * (star (a h) * a h))) +
          2 * (𝔼 g, 𝔼 h, realVectorState Ω
            ((star (a g) * a h) * (star (a h) * a g)))) := by
…

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