ArcFourier.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

The centered arc, its exact second moment, and its nonzero Fourier coefficients, computed using normalized angular Lebesgue integration.

def OAI.KadisonSimilarity.centeredArc line 15
Source documentation
A representative of the centered arc indicator; endpoints have measure zero.
```
def centeredArc (θ x : ℝ) : ℝ :=
…
```
theorem OAI.KadisonSimilarity.intervalIntegrable_indicator_of line 18
theorem OAI.KadisonSimilarity.integral_indicator_subinterval line 25
theorem OAI.KadisonSimilarity.centeredArc_integrable line 34
theorem OAI.KadisonSimilarity.centeredArc_abs_le_one line 39
theorem OAI.KadisonSimilarity.centeredArc_integral_zero line 49

theorem OAI.KadisonSimilarity.centeredArc_second_moment line 62

Source documentation

The normalized second moment is the Bernoulli variance of the arc.

theorem centeredArc_second_moment {θ : ℝ} (hθ : 0 ≤ θ) (hπ : θ ≤ Real.pi) :
    (2 * Real.pi)⁻¹ * (∫ x in -Real.pi..Real.pi, centeredArc θ x ^ 2) =
      (θ / Real.pi) * (1 - θ / Real.pi) := by
…

Mentions: OAI.KadisonSimilarity.centeredArc

theorem OAI.KadisonSimilarity.centeredArc_second_moment_le line 84

theorem OAI.KadisonSimilarity.integral_arc_exponential line 93

Source documentation

Nonzero frequency integration over a symmetric arc.

theorem integral_arc_exponential (θ r : ℝ) (hr : r ≠ 0) :
    (∫ x in -θ..θ, Complex.exp ((r * x : ℝ) * Complex.I)) =
      (2 * Real.sin (r * θ) / r : ℝ) := by
…

def OAI.KadisonSimilarity.arcFourierIntegral line 103
Source documentation
The normalized angular Fourier transform of the actual centered arc.
```
def arcFourierIntegral (θ : ℝ) (l : ℤ) : ℂ :=
…
```
theorem OAI.KadisonSimilarity.arcFourierIntegral_zero line 108
theorem OAI.KadisonSimilarity.arcFourierIntegral_ne_zero line 115
theorem OAI.KadisonSimilarity.arcFourierIntegral_eq_arcCoefficient line 146
Source documentation
The positive entries used in the finite Hankel block are these Fourier coefficients.
```
theorem arcFourierIntegral_eq_arcCoefficient {N : ℕ} (hN : 0 < N)
    {l : ℕ} (hl : 0 < l) :
    arcFourierIntegral (arcWidth N) l = (arcCoefficient N l : ℂ) := by
…
```
Mentions: OAI.KadisonSimilarity.arcFourierIntegral, OAI.KadisonSimilarity.arcWidth, OAI.KadisonSimilarity.arcCoefficient
def OAI.KadisonSimilarity.realArcFourierCoefficient line 160
Source documentation
The real Fourier coefficient, including the centered zero frequency.
```
def realArcFourierCoefficient (θ : ℝ) (l : ℤ) : ℝ :=
…
```
theorem OAI.KadisonSimilarity.arcFourierIntegral_eq_real line 163
theorem OAI.KadisonSimilarity.realArcFourierCoefficient_pos_index line 170