OAI/Analysis/PlaneSpectrum/FourierTests.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PlaneFiveColor.InvariantMean.integralReal_congr line 20
2. lemma OAI.PlaneFiveColor.InvariantMean.integralReal_mul line 32
3. lemma OAI.PlaneFiveColor.InvariantMean.integralReal_sum line 46
4. lemma OAI.PlaneFiveColor.InvariantMean.weighted_bound line 66
5. theorem OAI.PlaneFiveColor.InvariantMean.exists_small_nonnegative_tests line 76

   Source documentation

   Positivity of the literal invariant integral supplies a common small parameter for finitely many nonnegative tests. This makes no ordinary measurability assumption on any test.

   theorem exists_small_nonnegative_tests {ι : Type*} (s : Finset ι)
       (φ : AF → ℝ) (f : ι → AF → ℝ) {N : ℕ} {B ε : ℝ}
       (hs : ∀ t : AF, (N : ℝ) < |(t : ℝ)| → φ t = 0)
       (hb : ∀ t, ‖φ t‖ ≤ B) (hp : ∀ t, 0 ≤ φ t)
       (hI : 0 < integralReal φ hs hb) (hε : 0 < ε)
       (hf : ∀ i t, 0 ≤ f i t ∧ f i t ≤ 1)
       (hz : ∀ i, integralReal (fun t => φ t * f i t)
         (fun t ht => by rw [hs t ht, zero_mul])
         (weighted_bound φ (f i) hb (hf i)) = 0) :
       ∃ t : AF, 0 < φ t ∧ ∀ i ∈ s, f i t < ε := by
   …

   Mentions: OAI.PlaneFiveColor.InvariantMean.AF, OAI.PlaneFiveColor.InvariantMean.integralReal, OAI.PlaneFiveColor.InvariantMean.weighted_bound

6. lemma OAI.PlaneFiveColor.Spectral.lineFourier_zero line 130
7. lemma OAI.PlaneFiveColor.Spectral.lineFourier_re_le_one line 134
8. lemma OAI.PlaneFiveColor.Spectral.wild_line_average_re_zero line 140

   Source documentation

   Real part of the checked vanishing line average, with the same invariant integral and the same compact window.

   lemma wild_line_average_re_zero (ν : Measure D) [IsProbabilityMeasure ν]
       (hν : IsWild ν) {a : E} (ha : a ≠ 0)
       (φ : ℝ → ℝ) (hc : UniformContinuous φ) {N : ℕ} {B : ℝ}
       (hs : ∀ t : ℝ, (N : ℝ) < |t| → φ t = 0)
       (hb : ∀ t, |φ t| ≤ B) :
       integralReal (fun t : F => φ t * (lineFourier ν a t).re)
         (fun t ht => by rw [hs t ht, zero_mul])
         (fun t => by
           rw [norm_mul, Real.norm_eq_abs, Real.norm_eq_abs]
           exact (mul_le_of_le_one_right (abs_nonneg _)
             ((Complex.abs_re_le_norm _).trans (lineFourier_norm_le ν a t))).trans (hb t)) = 0 := by
   …

   Mentions: OAI.PlaneFiveColor.Spectral.D, OAI.PlaneFiveColor.Spectral.IsWild, OAI.PlaneFiveColor.Spectral.E, OAI.PlaneFiveColor.Spectral.F, OAI.PlaneFiveColor.Spectral.lineFourier, OAI.PlaneFiveColor.Spectral.lineFourier_norm_le

9. lemma OAI.PlaneFiveColor.Spectral.exists_positive_window line 171

   Source documentation

   A compact tent window strictly inside the requested parameter radius.

   lemma exists_positive_window {r : ℝ} (hr : 0 < r) :
       ∃ (φ : C(ℝ, ℝ)) (N : ℕ) (B : ℝ),
         (∀ t : ℝ, (N : ℝ) < |t| → φ t = 0) ∧
         (∀ t, ‖φ t‖ ≤ B) ∧ (∀ t, 0 ≤ φ t) ∧
         UniformContinuous φ ∧ (0 < ∫ t : ℝ, φ t) ∧
         (∀ t, 0 < φ t → |t| < r) := by
   …

   Mentions: OAI.PlaneFiveColor.Spectral.C

10. theorem OAI.PlaneFiveColor.Spectral.exists_small_wild_parameter line 200
11. def OAI.EuclideanFiveColor.DifferenceFourier.differenceLaw line 235
12. instance OAI.EuclideanFiveColor.DifferenceFourier.differenceLaw_probability line 238
13. lemma OAI.EuclideanFiveColor.DifferenceFourier.coe_character_div line 246
14. lemma OAI.EuclideanFiveColor.DifferenceFourier.independent_coefficient line 251
15. lemma OAI.EuclideanFiveColor.DifferenceFourier.difference_coefficient line 261
16. lemma OAI.EuclideanFiveColor.DifferenceFourier.difference_coefficient_nonneg line 279