OAI/Analysis/PlaneSpectrum/Characters.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PlaneFiveColor.ContinuousCharacters.abs_arg_exp_le line 12
2. theorem OAI.PlaneFiveColor.ContinuousCharacters.abs_arg_pow_le line 24
3. def OAI.PlaneFiveColor.ContinuousCharacters.frequency line 32

   Source documentation

   Canonical frequencies of the dyadic restrictions.

   def frequency (X : ℕ → Circle) (n : ℕ) : ℝ :=
   …

4. theorem OAI.PlaneFiveColor.ContinuousCharacters.frequency_abs_mono line 35
5. theorem OAI.PlaneFiveColor.ContinuousCharacters.exp_frequency_div line 48
6. theorem OAI.PlaneFiveColor.ContinuousCharacters.frequency_exp_previous line 52
7. theorem OAI.PlaneFiveColor.ContinuousCharacters.frequency_stabilizes line 60
8. theorem OAI.PlaneFiveColor.ContinuousCharacters.chord_bound line 88

   Source documentation

   The quantitative lower chord bound on the principal argument.

   theorem chord_bound (z : Circle) :
       2 / Real.pi * |Complex.arg (z : ℂ)| ≤ ‖(z : ℂ) - 1‖ := by
   …

9. theorem OAI.PlaneFiveColor.ContinuousCharacters.geom_sum_chord_bound line 112

   Source documentation

   Cesàro averages of a circle point are small away from one.

   theorem geom_sum_chord_bound (z : Circle) (m : ℕ) :
       ‖∑ k ∈ Finset.range m, (z : ℂ)^k‖ * ‖(z : ℂ)-1‖ ≤ 2 := by
   …

10. theorem OAI.PlaneFiveColor.ContinuousCharacters.average_deviation line 120

    Source documentation

    A large canonical frequency has a large averaged real deviation.

    theorem average_deviation (z : Circle) (m : ℕ)
        (h : 4 ≤ (m : ℝ) * ‖(z : ℂ)-1‖) :
        (m : ℝ) / 2 ≤ ∑ k ∈ Finset.range m, (1 - ((z : ℂ)^k).re) := by
    …

11. def OAI.PlaneFiveColor.ContinuousCharacters.deviation line 140
12. lemma OAI.PlaneFiveColor.ContinuousCharacters.deviation_bound line 142
13. lemma OAI.PlaneFiveColor.ContinuousCharacters.deviation_measurable line 148
14. lemma OAI.PlaneFiveColor.ContinuousCharacters.deviation_integrable line 152
15. theorem OAI.PlaneFiveColor.ContinuousCharacters.frequency_tail_bound line 161

    Source documentation

    Uniform small deviations imply a quantitative frequency-tail bound.

    theorem frequency_tail_bound {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω)
        [IsFiniteMeasure μ] (X : Ω → Circle) (hX : Measurable (fun x => (X x : ℂ)))
        (n m : ℕ) (hm : 0 < m) (R ε : ℝ)
        (hR : 4 ≤ (m : ℝ) * (2 / Real.pi) * (R / (2 : ℝ)^n))
        (hε : ∀ k ∈ Finset.range m, ∫ x, deviation (X x) k ∂μ ≤ ε) :
        μ.real {x | R ≤ |(2 : ℝ)^n * Complex.arg (X x : ℂ)|} ≤ 2 * ε := by
    …

    Mentions: OAI.PlaneFiveColor.ContinuousCharacters.deviation

16. theorem OAI.PlaneFiveColor.ContinuousCharacters.dyadic_tail_bound line 200

    Source documentation

    Choosing a Cesàro window within a fixed neighborhood of zero gives frequency tightness with a bound independent of the dyadic level.

    theorem dyadic_tail_bound {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω)
        [IsFiniteMeasure μ] (X : ℕ → Ω → Circle) (hX : ∀ n, Measurable (fun x => (X n x : ℂ)))
        (δ ε : ℝ) (hδ : 0 < δ)
        (he : ∀ (n k : ℕ), (k : ℝ)/(2 : ℝ)^n < δ →
          ∫ x, deviation (X n x) k ∂μ ≤ ε) (n : ℕ) :
        μ.real {x | 2 * Real.pi / δ ≤ |frequency (fun j => X j x) n|} ≤ 2*ε := by
    …

    Mentions: OAI.PlaneFiveColor.ContinuousCharacters.deviation, OAI.PlaneFiveColor.ContinuousCharacters.frequency

17. theorem OAI.PlaneFiveColor.ContinuousCharacters.dyadic_frequencies_ae_bounded line 224

    Source documentation

    A measure with coefficients continuous at zero is almost surely supported on dyadic paths whose principal frequencies are bounded.

    theorem dyadic_frequencies_ae_bounded {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω)
        [IsFiniteMeasure μ] (X : ℕ → Ω → Circle) (hX : ∀ n, Measurable (fun x => (X n x : ℂ)))
        (hcoh : ∀ x n, X n x = X (n+1) x ^ 2)
        (hcont : ∀ ε : ℝ, 0 < ε → ∃ δ : ℝ, 0 < δ ∧
          ∀ (n k : ℕ), (k : ℝ)/(2 : ℝ)^n < δ → ∫ x, deviation (X n x) k ∂μ ≤ ε) :
        ∀ᵐ x ∂μ, ∃ R : ℝ, ∀ n, |frequency (fun j => X j x) n| ≤ R := by
    …

    Mentions: OAI.PlaneFiveColor.ContinuousCharacters.deviation, OAI.PlaneFiveColor.ContinuousCharacters.frequency

18. theorem OAI.PlaneFiveColor.ContinuousCharacters.dyadic_frequencies_ae_stable line 259

    Source documentation

    The canonical frequencies of almost every such path eventually stabilize.

    theorem dyadic_frequencies_ae_stable {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω)
        [IsFiniteMeasure μ] (X : ℕ → Ω → Circle) (hX : ∀ n, Measurable (fun x => (X n x : ℂ)))
        (hcoh : ∀ x n, X n x = X (n+1) x ^ 2)
        (hcont : ∀ ε : ℝ, 0 < ε → ∃ δ : ℝ, 0 < δ ∧
          ∀ (n k : ℕ), (k : ℝ)/(2 : ℝ)^n < δ → ∫ x, deviation (X n x) k ∂μ ≤ ε) :
        ∀ᵐ x ∂μ, ∃ N, ∀ n, N ≤ n →
          frequency (fun j => X j x) n = frequency (fun j => X j x) N := by
    …

    Mentions: OAI.PlaneFiveColor.ContinuousCharacters.deviation, OAI.PlaneFiveColor.ContinuousCharacters.frequency

19. theorem OAI.PlaneFiveColor.ContinuousCharacters.ordinary_of_stable line 271

    Source documentation

    A stable coherent path is an ordinary frequency on every dyadic scale.

    theorem ordinary_of_stable (X : ℕ → Circle) (hX : ∀ n, X n = X (n+1)^2)
        (N : ℕ) (hN : ∀ n, N ≤ n → frequency X n = frequency X N) :
        ∀ n, X n = Circle.exp (frequency X N / (2 : ℝ)^n) := by
    …

    Mentions: OAI.PlaneFiveColor.ContinuousCharacters.frequency

20. abbrev OAI.PlaneFiveColor.ContinuousCharacters.F line 286
21. def OAI.PlaneFiveColor.ContinuousCharacters.dyadicApprox line 288
22. lemma OAI.PlaneFiveColor.ContinuousCharacters.dyadicApprox_error line 291
23. lemma OAI.PlaneFiveColor.ContinuousCharacters.dyadicApprox_tendsto line 309
24. lemma OAI.PlaneFiveColor.ContinuousCharacters.circle_sq_dist line 317

    Source documentation

    Exact squared distance identity for unit characters.

    lemma circle_sq_dist (z w : Circle) :
        ‖(z : ℂ)-(w : ℂ)‖^2 = 2 * deviation (z/w) 1 := by
    …

    Mentions: OAI.PlaneFiveColor.ContinuousCharacters.deviation

25. def OAI.PlaneFiveColor.ContinuousCharacters.coeff line 329
26. lemma OAI.PlaneFiveColor.ContinuousCharacters.coeff_zero line 332
27. lemma OAI.PlaneFiveColor.ContinuousCharacters.coeff_small line 336
28. lemma OAI.PlaneFiveColor.ContinuousCharacters.char_nat_dyadic line 349
29. lemma OAI.PlaneFiveColor.ContinuousCharacters.char_int_dyadic line 357
30. lemma OAI.PlaneFiveColor.ContinuousCharacters.char_dyadic_coherent line 365
31. theorem OAI.PlaneFiveColor.ContinuousCharacters.character_ae_dyadic line 375

    Source documentation

    Continuous averaged coefficients give ordinary frequencies on dyadics a.e.

    theorem character_ae_dyadic (μ : Measure Ω) [IsFiniteMeasure μ]
        (χ : Ω → Multiplicative F →* Circle)
        (hχ : ∀ t : F, Measurable (fun x => (χ x (Multiplicative.ofAdd t) : ℂ)))
        (hc : ContinuousAt (coeff μ χ) 0) :
        ∀ᵐ x ∂μ, ∃ l : ℝ, ∀ n : ℕ,
          χ x (Multiplicative.ofAdd (((2 : F)^n)⁻¹)) = Circle.exp (l/(2 : ℝ)^n) := by
    …

    Mentions: OAI.PlaneFiveColor.ContinuousCharacters.F, OAI.PlaneFiveColor.ContinuousCharacters.coeff

32. lemma OAI.PlaneFiveColor.ContinuousCharacters.char_sub line 403
33. lemma OAI.PlaneFiveColor.ContinuousCharacters.char_sq_distance line 408
34. lemma OAI.PlaneFiveColor.ContinuousCharacters.char_sq_integrable line 413
35. lemma OAI.PlaneFiveColor.ContinuousCharacters.char_sq_integral line 421
36. lemma OAI.PlaneFiveColor.ContinuousCharacters.character_tendstoInMeasure line 428

    Source documentation

    At coefficient-continuity points, dyadic character evaluations converge in measure.

    lemma character_tendstoInMeasure (μ : Measure Ω) [IsFiniteMeasure μ]
        (χ : Ω → Multiplicative F →* Circle)
        (hχ : ∀ t : F, Measurable (fun x => (χ x (Multiplicative.ofAdd t) : ℂ)))
        (hc : ContinuousAt (coeff μ χ) 0) (r : ℕ → F) (t : F)
        (hr : Filter.Tendsto r Filter.atTop (nhds t)) :
        TendstoInMeasure μ (fun n x => (χ x (Multiplicative.ofAdd (r n)) : ℂ))
          Filter.atTop (fun x => (χ x (Multiplicative.ofAdd t) : ℂ)) := by
    …

    Mentions: OAI.PlaneFiveColor.ContinuousCharacters.F, OAI.PlaneFiveColor.ContinuousCharacters.coeff

37. instance OAI.PlaneFiveColor.ContinuousCharacters.F_countable line 461
38. lemma OAI.PlaneFiveColor.ContinuousCharacters.char_dyadicApprox_eq line 469
39. theorem OAI.PlaneFiveColor.ContinuousCharacters.character_ae_ordinary line 482

    Source documentation

    Direct ordinary-character support theorem on the algebraic real line. No Bochner representing-measure theorem is an input: frequency tightness and an a.e. subsequence argument prove the actual simultaneous character formula.

    theorem character_ae_ordinary (μ : Measure Ω) [IsFiniteMeasure μ]
        (χ : Ω → Multiplicative F →* Circle)
        (hχ : ∀ t : F, Measurable (fun x => (χ x (Multiplicative.ofAdd t) : ℂ)))
        (hc : ContinuousAt (coeff μ χ) 0) :
        ∀ᵐ x ∂μ, ∃ l : ℝ, ∀ t : F,
          χ x (Multiplicative.ofAdd t) = Circle.exp (l*(t : ℝ)) := by
    …

    Mentions: OAI.PlaneFiveColor.ContinuousCharacters.F, OAI.PlaneFiveColor.ContinuousCharacters.coeff

40. def OAI.PlaneFiveColor.Spectral.lineCharacter line 522

    Source documentation

    The actual character on the algebraic parameter line, forgetting only its discrete-domain continuity proof.

    def lineCharacter (a : E) (d : D) : Multiplicative F →* Circle :=
    …

    Mentions: OAI.PlaneFiveColor.Spectral.E, OAI.PlaneFiveColor.Spectral.D, OAI.PlaneFiveColor.Spectral.F

41. theorem OAI.PlaneFiveColor.Spectral.lineCharacter_measurable line 525
42. theorem OAI.PlaneFiveColor.Spectral.wild_continuous_coefficient_zero line 534

    Source documentation

    The exact replacement of Bochner's support step for an arbitrary finite weight absolutely continuous with respect to a wild law.

    theorem wild_continuous_coefficient_zero (ν μ : Measure D) [IsProbabilityMeasure ν]
        [IsFiniteMeasure μ] (hν : IsWild ν) (hμ : μ ≪ ν) {a : E} (ha : a ≠ 0)
        (hc : ContinuousAt (ContinuousCharacters.coeff μ (lineCharacter a)) 0) : μ = 0 := by
    …

    Mentions: OAI.PlaneFiveColor.Spectral.D, OAI.PlaneFiveColor.Spectral.IsWild, OAI.PlaneFiveColor.Spectral.E, OAI.PlaneFiveColor.ContinuousCharacters.coeff, OAI.PlaneFiveColor.Spectral.lineCharacter