HaarTail.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

The geometric-polynomial tail in scalar recovery

The normalization here uses angular Haar measure dt / (2 * pi).

def OAI.KadisonKastler.haarGeometricSum line 22
Source documentation
The sum of the first N positive powers on the circle.
```
def haarGeometricSum (N : ℕ) (t : ℝ) : ℂ :=
…
```
def OAI.KadisonKastler.haarPolynomial line 26
Source documentation
The normalized polynomial used in the Haar tail estimate.
```
def haarPolynomial (N : ℕ) (t : ℝ) : ℂ :=
…
```
theorem OAI.KadisonKastler.haarGeometricSum_eq_sum_exp line 29

theorem OAI.KadisonKastler.haar_chord_lower_bound line 41

Source documentation

The chord of the circle is bounded below linearly on the principal arc.

theorem haar_chord_lower_bound {t : ℝ} (ht : |t| ≤ Real.pi) :
    2 * |t| / Real.pi ≤ ‖Complex.exp (Complex.I * (t : ℂ)) - 1‖ := by
…

theorem OAI.KadisonKastler.haarGeometricSum_mul_chord_le line 56
Source documentation
The geometric identity gives a numerator of norm at most two.
```
theorem haarGeometricSum_mul_chord_le (N : ℕ) (t : ℝ) :
    ‖haarGeometricSum N t‖ * ‖Complex.exp (Complex.I * (t : ℂ)) - 1‖ ≤ 2 := by
…
```
Mentions: OAI.KadisonKastler.haarGeometricSum
theorem OAI.KadisonKastler.norm_haarGeometricSum_le line 71
Source documentation
The precise pointwise estimate from the manuscript.
```
theorem norm_haarGeometricSum_le {N : ℕ} {t : ℝ}
    (ht0 : 0 < |t|) (htpi : |t| ≤ Real.pi) :
    ‖haarGeometricSum N t‖ ≤ Real.pi / |t| := by
…
```
Mentions: OAI.KadisonKastler.haarGeometricSum
theorem OAI.KadisonKastler.haarPolynomial_norm_sq_le line 83
theorem OAI.KadisonKastler.continuous_haarGeometricSum line 100
theorem OAI.KadisonKastler.continuous_haarPolynomial line 104
theorem OAI.KadisonKastler.norm_haarGeometricSum_le_card line 109
theorem OAI.KadisonKastler.norm_haarPolynomial_le_sqrt line 117
theorem OAI.KadisonKastler.haarGeometricSum_neg line 130
theorem OAI.KadisonKastler.norm_haarPolynomial_neg line 141
def OAI.KadisonKastler.haarTailEnergy line 146
Source documentation
The normalized angular integral outside the symmetric arc of radius a.
```
def haarTailEnergy (N : ℕ) (a : ℝ) : ℝ :=
…
```
theorem OAI.KadisonKastler.haarTailEnergy_eq line 150
theorem OAI.KadisonKastler.haarTailEnergy_nonneg line 160
theorem OAI.KadisonKastler.haarTailEnergy_of_pi_le line 166

theorem OAI.KadisonKastler.integral_haarPolynomial_norm_sq_le line 171

Source documentation

Integration of the square geometric bound away from its singular point.

theorem integral_haarPolynomial_norm_sq_le {N : ℕ} (hN : 0 < N)
    {a : ℝ} (ha : 0 < a) (hapi : a ≤ Real.pi) :
    (∫ t in a..Real.pi, ‖haarPolynomial N t‖ ^ 2) ≤
      Real.pi ^ 2 / (N : ℝ) * (a⁻¹ - Real.pi⁻¹) := by
…

Mentions: OAI.KadisonKastler.haarPolynomial

theorem OAI.KadisonKastler.haarTailEnergy_le line 197
theorem OAI.KadisonKastler.haarTailEnergy_div_le line 216
Source documentation
The Haar tail bound at arc radius R/N, with the manuscript's constant.
```
theorem haarTailEnergy_div_le {N : ℕ} (hN : 0 < N) {R : ℝ} (hR : 0 < R) :
    haarTailEnergy N (R / (N : ℝ)) ≤ Real.pi / R := by
…
```
Mentions: OAI.KadisonKastler.haarTailEnergy