OAI/Analysis/PlaneSpectrum/Multipliers.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PlaneFiveColor.LpMultiplier.mul_memLp line 19
2. def OAI.PlaneFiveColor.LpMultiplier.mul line 25
3. lemma OAI.PlaneFiveColor.LpMultiplier.mul_ae line 29
4. lemma OAI.PlaneFiveColor.LpMultiplier.mul_norm line 33
5. def OAI.PlaneFiveColor.LpMultiplier.mulIsometry line 43
6. lemma OAI.PlaneFiveColor.LpMultiplier.mul_inverse line 58
7. def OAI.PlaneFiveColor.LpMultiplier.mulEquiv line 70
8. def OAI.PlaneFiveColor.LpMultiplier.weight line 76

   Source documentation

   Spectral weighting by a Hilbert vector, exactly |v|² μ.

   def weight (v : Lp ℂ 2 μ) : Measure X :=
   …

9. lemma OAI.PlaneFiveColor.LpMultiplier.weight_measurable line 79
10. instance OAI.PlaneFiveColor.LpMultiplier.weight_finite line 83
11. lemma OAI.PlaneFiveColor.LpMultiplier.weight_ac line 89
12. lemma OAI.PlaneFiveColor.LpMultiplier.weight_inner line 92
13. lemma OAI.PlaneFiveColor.LpMultiplier.weight_eq_zero_iff line 107
14. lemma OAI.PlaneFiveColor.LpMultiplier.norm_mul_sub_sq line 120
15. lemma OAI.PlaneFiveColor.LpMultiplier.lp_norm_sq_integral line 127
16. lemma OAI.PlaneFiveColor.LpMultiplier.weight_deviation line 132
17. def OAI.PlaneFiveColor.Spectral.lineU line 152
18. lemma OAI.PlaneFiveColor.Spectral.lineU_apply line 156
19. lemma OAI.PlaneFiveColor.Spectral.lineU_ae line 161
20. lemma OAI.PlaneFiveColor.Spectral.lineU_add line 166
21. lemma OAI.PlaneFiveColor.Spectral.lineU_zero line 179
22. lemma OAI.PlaneFiveColor.Spectral.weighted_coeff line 184
23. theorem OAI.PlaneFiveColor.Spectral.strong_vector_zero line 195

    Source documentation

    A wild law has no nonzero strongly continuous vector for any nonzero algebraic line. The arbitrary L² vector is handled by its actual |v|² weight.

    theorem strong_vector_zero (ν : Measure D) [IsProbabilityMeasure ν]
        (hν : IsWild ν) {a : E} (ha : a ≠ 0) (v : Lp ℂ 2 ν)
        (hc : Tendsto (fun t => lineU ν a t v) (𝓝 0) (𝓝 v)) : v = 0 := by
    …

    Mentions: OAI.PlaneFiveColor.Spectral.D, OAI.PlaneFiveColor.Spectral.IsWild, OAI.PlaneFiveColor.Spectral.E, OAI.PlaneFiveColor.Spectral.lineU

24. theorem OAI.PlaneFiveColor.Spectral.wild_smoothed_zero line 213

    Source documentation

    Every ordinary compact window has zero weak vector average along a nonzero algebraic line of a wild law.

    theorem wild_smoothed_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) (v : Lp ℂ 2 ν) :
        InvariantMean.smoothedVector (lineU ν a) (fun t => φ t)
          (fun t ht => hs t ht) (fun t => hb t) v = 0 := by
    …

    Mentions: OAI.PlaneFiveColor.Spectral.D, OAI.PlaneFiveColor.Spectral.IsWild, OAI.PlaneFiveColor.Spectral.E, OAI.PlaneFiveColor.InvariantMean.smoothedVector, OAI.PlaneFiveColor.Spectral.lineU

25. lemma OAI.PlaneFiveColor.InvariantMean.weakMean_complex line 227
26. lemma OAI.PlaneFiveColor.InvariantMean.weakIntegral_complex line 242
27. def OAI.PlaneFiveColor.Spectral.lineFourier line 252
28. lemma OAI.PlaneFiveColor.Spectral.lineFourier_norm_le line 255
29. lemma OAI.PlaneFiveColor.Spectral.lineFourier_inner line 261
30. theorem OAI.PlaneFiveColor.Spectral.wild_line_average_zero line 272

    Source documentation

    The invariant scalar Fourier average on a nonzero algebraic line vanishes for every real ordinary compact window; no measurability of t ↦ fν(at).

    theorem wild_line_average_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) :
        InvariantMean.integralComplex
          (fun t : F => (φ t : ℂ) * lineFourier ν a t)
          (fun t ht => by rw [hs t ht, Complex.ofReal_zero, zero_mul])
          (fun t => by
            rw [norm_mul, Complex.norm_real, Real.norm_eq_abs]
            exact (mul_le_of_le_one_right (abs_nonneg _) (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.InvariantMean.integralComplex, OAI.PlaneFiveColor.Spectral.F, OAI.PlaneFiveColor.Spectral.lineFourier, OAI.PlaneFiveColor.Spectral.lineFourier_norm_le