HilbertSignMoments.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Hilbert-space second and fourth moments of independent signs

The fourth-moment constant is three. Real Hilbert spaces suffice for the proof and complex Hilbert spaces are covered by restriction of scalars.

def OAI.KadisonKastler.hilbertSignSum line 21
Source documentation
The Hilbert-space sum of independent signs.
```
def hilbertSignSum (a : ι → V) (ε : ι → Bool) : V :=
…
```
def OAI.KadisonKastler.normalizedHilbertSignSum line 25
Source documentation
The variance-one normalized Hilbert-space sign sum.
```
def normalizedHilbertSignSum (a : ι → V) (ε : ι → Bool) : V :=
…
```
theorem OAI.KadisonKastler.sign_norm_sq line 29
theorem OAI.KadisonKastler.expect_hilbertSignSum_sq line 40
Source documentation
Sign orthogonality gives the exact second moment.
```
theorem expect_hilbertSignSum_sq (a : ι → V) :
    (𝔼 ε : ι → Bool, ‖hilbertSignSum a ε‖ ^ 2) = ∑ i, ‖a i‖ ^ 2 := by
…
```
Mentions: OAI.KadisonKastler.hilbertSignSum
theorem OAI.KadisonKastler.sign_norm_fourth line 47
theorem OAI.KadisonKastler.expect_hilbertSignSum_fourth_le line 59
Source documentation
Hilbert-space fourth moments require no operator trace.
```
theorem expect_hilbertSignSum_fourth_le (a : ι → V) :
    (𝔼 ε : ι → Bool, ‖hilbertSignSum a ε‖ ^ 4) ≤
      3 * (∑ i, ‖a i‖ ^ 2) ^ 2 := by
…
```
Mentions: OAI.KadisonKastler.hilbertSignSum

theorem OAI.KadisonKastler.expect_normalizedHilbertSignSum_sq line 92

Source documentation

Exact normalized second moment.

theorem expect_normalizedHilbertSignSum_sq (a : ι → V) :
    (𝔼 ε : ι → Bool, ‖normalizedHilbertSignSum a ε‖ ^ 2) =
      (Fintype.card ι : ℝ)⁻¹ * ∑ i, ‖a i‖ ^ 2 := by
…

Mentions: OAI.KadisonKastler.normalizedHilbertSignSum

theorem OAI.KadisonKastler.expect_normalizedHilbertSignSum_fourth_le line 102
Source documentation
Normalized fourth moment is at most three times the second moment squared, for every finite family of Hilbert vectors.
```
theorem expect_normalizedHilbertSignSum_fourth_le (a : ι → V) :
    (𝔼 ε : ι → Bool, ‖normalizedHilbertSignSum a ε‖ ^ 4) ≤
      3 * ((Fintype.card ι : ℝ)⁻¹ * ∑ i, ‖a i‖ ^ 2) ^ 2 := by
…
```
Mentions: OAI.KadisonKastler.normalizedHilbertSignSum