OAI/Analysis/PlaneSpectrum/RadialEnergy.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PlaneFiveColor.Spectral.equal_moduli_quadratic line 9
2. lemma OAI.PlaneFiveColor.Spectral.projectedMass_pair_mean line 51
3. lemma OAI.PlaneFiveColor.Spectral.kCoeff_scale_two line 58
4. lemma OAI.PlaneFiveColor.Spectral.kCoeff_scale_one line 61
5. lemma OAI.PlaneFiveColor.Spectral.char_two_term line 64
6. lemma OAI.PlaneFiveColor.Spectral.char_three_term line 69
7. lemma OAI.PlaneFiveColor.Spectral.quadratic_mass_inequality line 82
8. def OAI.PlaneFiveColor.Spectral.sqrtF line 123
9. lemma OAI.PlaneFiveColor.Spectral.sqrtF_sq line 130
10. lemma OAI.PlaneFiveColor.Spectral.norm_ofF line 133
11. def OAI.PlaneFiveColor.Spectral.massReal line 143
12. lemma OAI.PlaneFiveColor.Spectral.projectedMass_neg line 146
13. lemma OAI.PlaneFiveColor.Spectral.massReal_abs line 151
14. lemma OAI.PlaneFiveColor.Spectral.massReal_difference line 157
15. lemma OAI.PlaneFiveColor.Spectral.reF_sum line 177
16. lemma OAI.PlaneFiveColor.Spectral.reF_zsmul line 180
17. lemma OAI.PlaneFiveColor.Spectral.reF_nsmul line 185
18. lemma OAI.PlaneFiveColor.Spectral.selected_mass_bound line 192

    Source documentation

    The signed capped-residue conclusion for any integral transverse selection.

    lemma selected_mass_bound (m : F → ℝ) (hm0 : m 0 = 1)
        (hd : ∀ a b : F, 0 ≤ a → 0 ≤ b → m a*m b ≤ m |a-b|)
        (c : ℝ) (hc0 : 0 ≤ c) (hc1 : c ≤ 1)
        (r : F) (hr : 0 < r) {n : ℕ} (k : Fin n → E) (a b : Fin n → ℤ)
        (D M : ℕ) (hD : 0 < D) (hM : 0 < M)
        (ha : (∑ j, a j • k j) = D • (1:E))
        (hb : (∑ j, b j • k j) = D • imagUnit)
        (hab : (∑ j, ((a j).natAbs+(b j).natAbs)) ≤ M)
        (v : E) (hv : ‖(v:ℂ)‖ = 1) (hsmall : |reF v| < (M:F)⁻¹)
        (hgood : ∀ j, c ≤ m |2*r*reF (k j*v)|) :
        c^(4*M) ≤ m |2*r*D*reF v| := by
    …

    Mentions: OAI.PlaneFiveColor.Spectral.F, OAI.PlaneFiveColor.Spectral.E, OAI.PlaneFiveColor.Spectral.D, OAI.PlaneFiveColor.Spectral.j, OAI.PlaneFiveColor.Spectral.imagUnit, OAI.PlaneFiveColor.Spectral.reF

19. lemma OAI.PlaneFiveColor.Spectral.circle_realPart line 259
20. lemma OAI.PlaneFiveColor.Spectral.cover_mass_positive line 280

    Source documentation

    Arithmetic propagation: one syndetic positive mass level forces uniformly positive mass at every sufficiently small positive algebraic radius.

    lemma cover_mass_positive (m : F → ℝ) (hm0 : m 0 = 1)
        (hd : ∀ a b : F, 0 ≤ a → 0 ≤ b → m a*m b ≤ m |a-b|)
        (c : ℝ) (hc0 : 0 < c) (hc1 : c ≤ 1)
        (r : F) (hr : 0 < r) (Q : Finset E) (hQ : ∀ q ∈ Q, ‖(q:ℂ)‖ = 1)
        (hcover : ∀ v : E, ‖(v:ℂ)‖ = 1 → ∃ q ∈ Q, c ≤ m |2*r*reF (q*v)|) :
        ∃ δ : F, 0 < δ ∧ ∃ ε : ℝ, 0 < ε ∧ ε ≤ 1 ∧
          ∀ s : F, 0 < s → s < δ → ε ≤ m s := by
    …

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

21. lemma OAI.PlaneFiveColor.Spectral.kCoeff_scale_neg_one line 346
22. lemma OAI.PlaneFiveColor.Spectral.char_symmetric line 351
23. def OAI.PlaneFiveColor.Spectral.radiusFamily line 373
24. lemma OAI.PlaneFiveColor.Spectral.radiusFamily_apply line 384
25. lemma OAI.PlaneFiveColor.Spectral.radiusFamily_mean line 387
26. lemma OAI.PlaneFiveColor.Spectral.radius_syndetic line 399
27. lemma OAI.PlaneFiveColor.Spectral.radial_positive_near_zero line 421
28. lemma OAI.PlaneFiveColor.Spectral.massReal_vanish line 452