VectorStateFourthMoment.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Nontracial fourth moments of independent signs

The three-pairing sign identity holds for the actual vector functional. The crossed pairing is bounded after summing the two orders of its indices. This avoids applying a tracial fourth-moment theorem to the nontracial vector state in the modular graph argument.

def OAI.KadisonKastler.realVectorState line 25
Source documentation
Real part of the ambient vector state, as a real-linear functional.
```
def realVectorState (Ω : H) : (H →L[ℂ] H) →ₗ[ℝ] ℝ :=
…
```
theorem OAI.KadisonKastler.realVectorState_apply line 29
theorem OAI.KadisonKastler.realVectorState_star_mul_self line 34
Source documentation
Positivity of the vector functional is a Hilbert norm identity.
```
theorem realVectorState_star_mul_self (Ω : H) (x : H →L[ℂ] H) :
    realVectorState Ω (star x * x) = ‖x Ω‖ ^ 2 := by
…
```
Mentions: OAI.KadisonKastler.realVectorState
theorem OAI.KadisonKastler.sign_fourth_integrand line 42

theorem OAI.KadisonKastler.expect_finiteSignSum_vector_fourth line 71

Source documentation

Exact three-pairing expansion in an arbitrary vector state. The third pairing stays in its original order; no trace cycling is used.

theorem expect_finiteSignSum_vector_fourth (Ω : H) (a : ι → H →L[ℂ] H) :
    (𝔼 ε : ι → Bool,
      realVectorState Ω ((star (finiteSignSum a ε) * finiteSignSum a ε) ^ 2)) =
      (∑ i, ∑ j, realVectorState Ω ((star (a i) * a i) * (star (a j) * a j))) +
      (∑ i, ∑ j, realVectorState Ω ((star (a i) * a j) ^ 2)) +
      (∑ i, ∑ j, realVectorState Ω ((star (a i) * a j) * (star (a j) * a i))) -
      2 * ∑ i, realVectorState Ω ((star (a i) * a i) ^ 2) := by
…

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

theorem OAI.KadisonKastler.sum_vectorState_crossed_le line 85
Source documentation
Summing both index orders bounds the crossed pairing by the positive pairing, even though the state is not tracial.
```
theorem sum_vectorState_crossed_le (Ω : H) (a : ι → H →L[ℂ] H) :
    (∑ i, ∑ j, realVectorState Ω ((star (a i) * a j) ^ 2)) ≤
      ∑ i, ∑ j, realVectorState Ω ((star (a i) * a j) * (star (a j) * a i)) := by
…
```
Mentions: OAI.KadisonKastler.realVectorState

theorem OAI.KadisonKastler.expect_finiteSignSum_vector_fourth_le line 111

Source documentation

The nontracial sign fourth moment is controlled by its two positive pairings. This is the estimate needed before averaging the matrix orbits.

theorem expect_finiteSignSum_vector_fourth_le (Ω : H) (a : ι → H →L[ℂ] H) :
    (𝔼 ε : ι → Bool,
      realVectorState Ω ((star (finiteSignSum a ε) * finiteSignSum a ε) ^ 2)) ≤
      (∑ i, ∑ j, realVectorState Ω ((star (a i) * a i) * (star (a j) * a j))) +
      2 * (∑ i, ∑ j,
        realVectorState Ω ((star (a i) * a j) * (star (a j) * a i))) := by
…

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