FiniteSignFourthMoment.lean`

29 declarations, 0 contain sorry, 0 declared as axioms

Fourth moments of finite independent signs

The finite probability space is the set of all Boolean sign assignments. The four-sign identity and tracial Cauchy–Schwarz give the estimate used in the bounded-vector test in manuscript §5.

def OAI.KadisonKastler.finiteSign line 24
Source documentation
The coordinate signs on the uniform finite Boolean probability space.
```
def finiteSign (ε : ι → Bool) (i : ι) : ℝ := if ε i then -1 else 1
…
```
theorem OAI.KadisonKastler.finiteSign_sq line 28
def OAI.KadisonKastler.flipSign line 31
theorem OAI.KadisonKastler.finiteSign_flip_same line 46
theorem OAI.KadisonKastler.finiteSign_flip_ne line 51
theorem OAI.KadisonKastler.finiteSign_pair line 56
Source documentation
Coordinate sign orthogonality.
```
theorem finiteSign_pair (i j : ι) :
    (𝔼 ε : ι → Bool, finiteSign ε i * finiteSign ε j) = if i = j then 1 else 0 := by
…
```
Mentions: OAI.KadisonKastler.finiteSign

theorem OAI.KadisonKastler.finiteSign_four_single line 72

Source documentation

A sign appearing exactly once kills a four-sign expectation.

private theorem finiteSign_four_single (i j k l : ι)
    (hij : j ≠ i) (hik : k ≠ i) (hil : l ≠ i) :
    (𝔼 ε : ι → Bool, finiteSign ε i * finiteSign ε j *
      finiteSign ε k * finiteSign ε l) = 0 := by
…

Mentions: OAI.KadisonKastler.finiteSign

theorem OAI.KadisonKastler.finiteSign_four line 87

Source documentation

The three pairings, with the common diagonal counted only once.

theorem finiteSign_four (i j k l : ι) :
    (𝔼 ε : ι → Bool, finiteSign ε i * finiteSign ε j *
      finiteSign ε k * finiteSign ε l) =
      (if i = j ∧ k = l then 1 else 0) +
      (if i = k ∧ j = l then 1 else 0) +
      (if i = l ∧ j = k then 1 else 0) -
      (if i = j ∧ j = k ∧ k = l then 2 else 0) := by
…

Mentions: OAI.KadisonKastler.finiteSign

theorem OAI.KadisonKastler.expect_finiteSign_four_sum line 131

Source documentation

The fourth-sign identity integrated against any four-index coefficient.

theorem expect_finiteSign_four_sum (F : ι → ι → ι → ι → ℝ) :
    (𝔼 ε : ι → Bool, ∑ i, ∑ j, ∑ k, ∑ l,
      (finiteSign ε i * finiteSign ε j * finiteSign ε k * finiteSign ε l) * F i j k l) =
      (∑ i, ∑ k, F i i k k) + (∑ i, ∑ j, F i j i j) +
        (∑ i, ∑ j, F i j j i) - 2 * ∑ i, F i i i i := by
…

Mentions: OAI.KadisonKastler.finiteSign

def OAI.KadisonKastler.realTrace line 143
Source documentation
The real part of the trace, viewed as a real-linear functional.
```
def realTrace (τ : FaithfulTracialState B) : B →ₗ[ℝ] ℝ :=
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState
theorem OAI.KadisonKastler.realTrace_apply line 147
def OAI.KadisonKastler.finiteSignSum line 151
Source documentation
The unnormalized random sum; normalization is introduced after expansion.
```
def finiteSignSum (a : ι → B) (ε : ι → Bool) : B := ∑ i, finiteSign ε i • a i
…
```
Mentions: OAI.KadisonKastler.finiteSign
theorem OAI.KadisonKastler.fourth_integrand_expand line 154
theorem OAI.KadisonKastler.realTrace_sum_square line 182

theorem OAI.KadisonKastler.expect_finiteSignSum_fourth line 188

Source documentation

Exact fourth-moment pairing formula before scalar normalization.

theorem expect_finiteSignSum_fourth (τ : FaithfulTracialState B) (a : ι → B) :
    (𝔼 ε : ι → Bool, realTrace τ ((star (finiteSignSum a ε) * finiteSignSum a ε) ^ 2)) =
      realTrace τ ((∑ i, star (a i) * a i) ^ 2) +
        (∑ i, ∑ j, realTrace τ ((star (a i) * a j) ^ 2)) +
        realTrace τ ((∑ i, a i * star (a i)) ^ 2) -
        2 * ∑ i, realTrace τ ((star (a i) * a i) ^ 2) := by
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.realTrace, OAI.KadisonKastler.finiteSignSum

theorem OAI.KadisonKastler.realTrace_square_le_star_square line 217
Source documentation
Tracial Cauchy–Schwarz bounds the crossed pairing by a covariance term.
```
theorem realTrace_square_le_star_square (τ : FaithfulTracialState B) (x : B) :
    realTrace τ (x ^ 2) ≤ realTrace τ (star x * x) := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.realTrace

theorem OAI.KadisonKastler.expect_finiteSignSum_fourth_le line 226

Source documentation

The unnormalized fourth moment is controlled by the two covariance squares.

theorem expect_finiteSignSum_fourth_le (τ : FaithfulTracialState B) (a : ι → B) :
    (𝔼 ε : ι → Bool, realTrace τ ((star (finiteSignSum a ε) * finiteSignSum a ε) ^ 2)) ≤
      realTrace τ ((∑ i, star (a i) * a i) ^ 2) +
        2 * realTrace τ ((∑ i, a i * star (a i)) ^ 2) := by
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.realTrace, OAI.KadisonKastler.finiteSignSum

def OAI.KadisonKastler.normalizedFiniteSignSum line 254
Source documentation
The usual variance-one normalization of the finite sign sum.
```
def normalizedFiniteSignSum (a : ι → B) (ε : ι → Bool) : B :=
…
```
def OAI.KadisonKastler.finiteSignRightCovariance line 258
Source documentation
Right covariance of the coefficients.
```
def finiteSignRightCovariance (a : ι → B) : B :=
…
```
def OAI.KadisonKastler.finiteSignLeftCovariance line 262
Source documentation
Left covariance of the coefficients.
```
def finiteSignLeftCovariance (a : ι → B) : B :=
…
```
theorem OAI.KadisonKastler.realTrace_square_smul line 265
theorem OAI.KadisonKastler.realTrace_fourth_smul line 269
theorem OAI.KadisonKastler.expect_normalizedFiniteSignSum_fourth_le line 277
Source documentation
The normalized fourth moment is bounded by the two covariance squares.
```
theorem expect_normalizedFiniteSignSum_fourth_le
    (τ : FaithfulTracialState B) (a : ι → B) :
    (𝔼 ε : ι → Bool,
      realTrace τ ((star (normalizedFiniteSignSum a ε) * normalizedFiniteSignSum a ε) ^ 2)) ≤
      traceTwoNorm τ (finiteSignRightCovariance a) ^ 2 +
        2 * traceTwoNorm τ (finiteSignLeftCovariance a) ^ 2 := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.realTrace, OAI.KadisonKastler.normalizedFiniteSignSum, OAI.KadisonKastler.traceTwoNorm, OAI.KadisonKastler.finiteSignRightCovariance, OAI.KadisonKastler.finiteSignLeftCovariance

theorem OAI.KadisonKastler.expect_normalizedFiniteSignSum_fourth_le_twelve line 307

Source documentation

Covariance two-norms bounded by two give the manuscript constant twelve.

theorem expect_normalizedFiniteSignSum_fourth_le_twelve
    (τ : FaithfulTracialState B) (a : ι → B)
    (hQ : traceTwoNorm τ (finiteSignRightCovariance a) ≤ 2)
    (hL : traceTwoNorm τ (finiteSignLeftCovariance a) ≤ 2) :
    (𝔼 ε : ι → Bool,
      (τ.toLinearMap ((star (normalizedFiniteSignSum a ε) *
        normalizedFiniteSignSum a ε) ^ 2)).re) ≤ 12 := by
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceTwoNorm, OAI.KadisonKastler.finiteSignRightCovariance, OAI.KadisonKastler.finiteSignLeftCovariance, OAI.KadisonKastler.normalizedFiniteSignSum

theorem OAI.KadisonKastler.finiteSign_complex_pair line 322
Source documentation
Real signs also form an orthogonal family of complex phases.
```
theorem finiteSign_complex_pair (i j : ι) :
    (𝔼 ε : ι → Bool, star (finiteSign ε i : ℂ) * (finiteSign ε j : ℂ)) =
      if i = j then 1 else 0 := by
…
```
Mentions: OAI.KadisonKastler.finiteSign
theorem OAI.KadisonKastler.expect_finiteSign_pair_sum line 330
theorem OAI.KadisonKastler.expect_normalizedFiniteSignSum_twoNorm_sq line 337
Source documentation
The second moment is the average of the coefficient two-norm squares.
```
theorem expect_normalizedFiniteSignSum_twoNorm_sq
    (τ : FaithfulTracialState B) (a : ι → B) :
    (𝔼 ε : ι → Bool, traceTwoNorm τ (normalizedFiniteSignSum a ε) ^ 2) =
      (Fintype.card ι : ℝ)⁻¹ * ∑ i, traceTwoNorm τ (a i) ^ 2 := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceTwoNorm, OAI.KadisonKastler.normalizedFiniteSignSum
theorem OAI.KadisonKastler.map_normalizedFiniteSignSum line 364
Distinct definitions of this name: OAI/Analysis/KadisonKastler/GraphSignalSelection.lean:27 (different declaration text). Qualify references as OAI.KadisonKastler.map_normalizedFiniteSignSum@path.

theorem OAI.KadisonKastler.expect_normalizedFiniteSignSum_pairing line 372

Source documentation

Mixed sign orthogonality, with any complex-linear realization and bounded operator.

theorem expect_normalizedFiniteSignSum_pairing
    (J : B →ₗ[ℂ] H) (V : H →L[ℂ] H) (a b : ι → B) :
    (𝔼 ε : ι → Bool, inner ℂ (V (J (normalizedFiniteSignSum a ε)))
      (J (normalizedFiniteSignSum b ε))) =
      (Fintype.card ι : ℂ)⁻¹ * ∑ i, inner ℂ (V (J (a i))) (J (b i)) := by
…

Mentions: OAI.KadisonKastler.normalizedFiniteSignSum