HaarArc.lean`

40 declarations, 0 contain sorry, 0 declared as axioms

Continuous approximation of a Haar arc

The arc is the closed metric ball about zero in the circle of length 2 * pi. Continuous thickened indicators decrease towards its indicator, stay between zero and one, and converge in scalar Haar L². No operator spectral projection is assumed in this construction.

def OAI.KadisonKastler.haarArc line 26
Source documentation
The centered closed arc of angular radius a.
```
def haarArc (a : ℝ) : Set HaarCircle := Metric.closedBall 0 a
```
Mentions: OAI.KadisonKastler.HaarCircle
theorem OAI.KadisonKastler.isClosed_haarArc line 28
theorem OAI.KadisonKastler.measurableSet_haarArc line 30
def OAI.KadisonKastler.haarArcIndicator line 34
Source documentation
The real indicator of the centered arc.
```
def haarArcIndicator (a : ℝ) : HaarCircle → ℝ :=
…
```
Mentions: OAI.KadisonKastler.HaarCircle
def OAI.KadisonKastler.haarArcRadius line 38
Source documentation
A positive sequence of radii tending to zero.
```
def haarArcRadius (n : ℕ) : ℝ := 1 / ((n : ℝ) + 1)
```
theorem OAI.KadisonKastler.haarArcRadius_pos line 40
theorem OAI.KadisonKastler.tendsto_haarArcRadius line 44
def OAI.KadisonKastler.haarArcCutoffReal line 48
Source documentation
Continuous real cutoffs, equal to one on the arc.
```
def haarArcCutoffReal (a : ℝ) (n : ℕ) : C(HaarCircle, ℝ) where
…
```
Mentions: OAI.KadisonKastler.HaarCircle
def OAI.KadisonKastler.haarArcCutoff line 54
Source documentation
The same cutoffs in the complex continuous functional calculus.
```
def haarArcCutoff (a : ℝ) (n : ℕ) : C(HaarCircle, ℂ) where
…
```
Mentions: OAI.KadisonKastler.HaarCircle
theorem OAI.KadisonKastler.haarArcCutoffReal_nonneg line 58
theorem OAI.KadisonKastler.haarArcCutoffReal_le_one line 61
theorem OAI.KadisonKastler.haarArcCutoffReal_eq_one line 65
theorem OAI.KadisonKastler.haarArcCutoffReal_mono line 71
theorem OAI.KadisonKastler.norm_haarArcCutoff_apply_le_one line 80
theorem OAI.KadisonKastler.norm_haarArcCutoff_le_one line 86
theorem OAI.KadisonKastler.star_haarArcCutoff line 91
theorem OAI.KadisonKastler.haarArcIndicator_nonneg line 96
theorem OAI.KadisonKastler.haarArcIndicator_le_one line 99
theorem OAI.KadisonKastler.measurable_haarArcIndicator line 102
theorem OAI.KadisonKastler.tendsto_haarArcCutoffReal line 106
Source documentation
Convergence holds even at the two endpoints, since the arc is closed.
```
theorem tendsto_haarArcCutoffReal (a : ℝ) (t : HaarCircle) :
    Tendsto (fun n => haarArcCutoffReal a n t) atTop (𝓝 (haarArcIndicator a t)) := by
…
```
Mentions: OAI.KadisonKastler.HaarCircle, OAI.KadisonKastler.haarArcCutoffReal, OAI.KadisonKastler.haarArcIndicator
theorem OAI.KadisonKastler.tendsto_haarArcCutoff line 118
theorem OAI.KadisonKastler.haarArcCutoff_error_sq_le_four line 122
theorem OAI.KadisonKastler.integrable_haarArcCutoff_error_sq line 131

theorem OAI.KadisonKastler.tendsto_integral_haarArcCutoff_error_sq line 143

Source documentation

Scalar Haar L² convergence of the actual continuous cutoffs.

theorem tendsto_integral_haarArcCutoff_error_sq (a : ℝ) :
    Tendsto (fun n => ∫ t, ‖haarArcCutoff a n t - (haarArcIndicator a t : ℂ)‖ ^ 2
      ∂(AddCircle.haarAddCircle (T := 2 * Real.pi))) atTop (𝓝 0) := by
…

Mentions: OAI.KadisonKastler.haarArcCutoff, OAI.KadisonKastler.haarArcIndicator

theorem OAI.KadisonKastler.integral_haarArcCutoff_sub_sq_le line 176
Source documentation
A direct scalar square-distance estimate, usable without constructing an L² space.
```
theorem integral_haarArcCutoff_sub_sq_le (a : ℝ) (m n : ℕ) :
    (∫ t, ‖haarArcCutoff a m t - haarArcCutoff a n t‖ ^ 2
      ∂(AddCircle.haarAddCircle (T := 2 * Real.pi))) ≤
…
```
Mentions: OAI.KadisonKastler.haarArcCutoff
theorem OAI.KadisonKastler.haarArcCutoff_square_integral_cauchy line 221
theorem OAI.KadisonKastler.haarArcCutoff_idempotency_error_sq_le line 234

theorem OAI.KadisonKastler.tendsto_integral_haarArcCutoff_idempotency_error_sq line 253

Source documentation

The approximate projections become idempotent in scalar Haar L².

theorem tendsto_integral_haarArcCutoff_idempotency_error_sq (a : ℝ) :
    Tendsto (fun n => ∫ t,
      ‖haarArcCutoff a n t * haarArcCutoff a n t - haarArcCutoff a n t‖ ^ 2
        ∂(AddCircle.haarAddCircle (T := 2 * Real.pi))) atTop (𝓝 0) := by
…

Mentions: OAI.KadisonKastler.haarArcCutoff

theorem OAI.KadisonKastler.integral_haarArcIndicator line 273
Source documentation
The mass of a centered arc under probability Haar measure.
```
theorem integral_haarArcIndicator {a : ℝ} (ha : 0 ≤ a) (hapi : a ≤ Real.pi) :
    (∫ t, haarArcIndicator a t ∂(AddCircle.haarAddCircle (T := 2 * Real.pi))) =
…
```
Mentions: OAI.KadisonKastler.haarArcIndicator
theorem OAI.KadisonKastler.haarArc_measureReal line 286

theorem OAI.KadisonKastler.tendsto_integral_haarArcCutoffReal line 292

Source documentation

The cutoff integrals converge to the arc's normalized angular length.

theorem tendsto_integral_haarArcCutoffReal {a : ℝ} (ha : 0 ≤ a) (hapi : a ≤ Real.pi) :
    Tendsto (fun n => ∫ t, haarArcCutoffReal a n t
      ∂(AddCircle.haarAddCircle (T := 2 * Real.pi))) atTop (𝓝 (a / Real.pi)) := by
…

Mentions: OAI.KadisonKastler.haarArcCutoffReal

theorem OAI.KadisonKastler.mem_haarArc_coe_iff line 307
Source documentation
On the principal angular interval, the metric arc is the ordinary interval.
```
theorem mem_haarArc_coe_iff {a t : ℝ} (ht : |t| ≤ Real.pi) :
    (t : HaarCircle) ∈ haarArc a ↔ |t| ≤ a := by
…
```
Mentions: OAI.KadisonKastler.HaarCircle, OAI.KadisonKastler.haarArc
theorem OAI.KadisonKastler.integral_haarArc_compl line 315
Source documentation
Scalar integration over the arc complement is exactly the two angular tails.
```
theorem integral_haarArc_compl {a : ℝ} (ha : 0 ≤ a) (hapi : a ≤ Real.pi)
    (g : C(HaarCircle, ℝ)) :
    (∫ t, (haarArc a)ᶜ.indicator g t
      ∂(AddCircle.haarAddCircle (T := 2 * Real.pi))) =
…
```
Mentions: OAI.KadisonKastler.HaarCircle, OAI.KadisonKastler.haarArc
theorem OAI.KadisonKastler.tendsto_integral_haarArcCutoff_compl_mul line 390
Source documentation
Continuous weighted traces of the complementary cutoffs converge to the corresponding integral off the closed arc.
```
theorem tendsto_integral_haarArcCutoff_compl_mul (a : ℝ) (g : C(HaarCircle, ℝ)) :
    Tendsto (fun n => ∫ t, g t * (1 - haarArcCutoffReal a n t)
      ∂(AddCircle.haarAddCircle (T := 2 * Real.pi))) atTop
…
```
Mentions: OAI.KadisonKastler.HaarCircle, OAI.KadisonKastler.haarArcCutoffReal
def OAI.KadisonKastler.haarCirclePolynomial line 415
Source documentation
The actual normalized Fourier polynomial on the quotient circle.
```
def haarCirclePolynomial (N : ℕ) : C(HaarCircle, ℂ) :=
…
```
Mentions: OAI.KadisonKastler.HaarCircle
theorem OAI.KadisonKastler.haarCirclePolynomial_coe line 418
theorem OAI.KadisonKastler.integral_haarCirclePolynomial_tail line 434
Source documentation
The scalar energy outside the actual circle arc is the tail already estimated by the geometric-sum calculation.
```
theorem integral_haarCirclePolynomial_tail {a : ℝ} (ha : 0 ≤ a) (hapi : a ≤ Real.pi)
    (N : ℕ) :
    (∫ t, (haarArc a)ᶜ.indicator (fun t => ‖haarCirclePolynomial N t‖ ^ 2) t
      ∂(AddCircle.haarAddCircle (T := 2 * Real.pi))) = haarTailEnergy N a := by
…
```
Mentions: OAI.KadisonKastler.haarArc, OAI.KadisonKastler.haarCirclePolynomial, OAI.KadisonKastler.haarTailEnergy
theorem OAI.KadisonKastler.tendsto_integral_haarCirclePolynomial_cutoff_compl line 443

theorem OAI.KadisonKastler.haarArcCutoff_traceTwoNorm_cauchy line 457

Source documentation

The scalar Cauchy estimate transfers directly through the Haar functional calculus, in the form required by bounded tracial completeness.

theorem haarArcCutoff_traceTwoNorm_cauchy (τ : FaithfulTracialState B) (v : unitary B)
    (hhaar : ∀ k : ℤ, k ≠ 0 → τ.toLinearMap (haarPower v k) = 0)
    (Φ : C(HaarCircle, ℂ) →⋆ₐ[ℂ] B)
    (hΦ : ∀ n : ℤ, Φ (fourier n) = haarPower v n) (a : ℝ) :
    ∀ ε > 0, ∃ N : ℕ, ∀ m ≥ N, ∀ n ≥ N,
      traceTwoNorm τ (Φ (haarArcCutoff a m) - Φ (haarArcCutoff a n)) < ε := by
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.haarPower, OAI.KadisonKastler.HaarCircle, OAI.KadisonKastler.traceTwoNorm, OAI.KadisonKastler.haarArcCutoff

theorem OAI.KadisonKastler.tendsto_traceTwoNorm_haarArcCutoff_idempotency line 470

Source documentation

The same actual functional-calculus cutoffs are asymptotically idempotent.

theorem tendsto_traceTwoNorm_haarArcCutoff_idempotency (τ : FaithfulTracialState B)
    (v : unitary B) (hhaar : ∀ k : ℤ, k ≠ 0 → τ.toLinearMap (haarPower v k) = 0)
    (Φ : C(HaarCircle, ℂ) →⋆ₐ[ℂ] B)
    (hΦ : ∀ n : ℤ, Φ (fourier n) = haarPower v n) (a : ℝ) :
    Tendsto (fun n => traceTwoNorm τ
      (Φ (haarArcCutoff a n) * Φ (haarArcCutoff a n) - Φ (haarArcCutoff a n)))
      atTop (𝓝 0) := by
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.haarPower, OAI.KadisonKastler.HaarCircle, OAI.KadisonKastler.traceTwoNorm, OAI.KadisonKastler.haarArcCutoff