OAI/Analysis/Triangular/Energy/Density.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.TriangularUniversal.LPFunction line 11

   Source documentation

   Regularity actually used by the density LP proof. Gaussian-bounded Fourier pairs are put into this class below; no separation of a competitor is assumed.

   structure LPFunction where
   …

2. instance OAI.TriangularUniversal.(instance at line 20) line 20
3. lemma OAI.TriangularUniversal.regular_kernel_integrable line 22
4. lemma OAI.TriangularUniversal.regular_firstMoment_integrable line 29
5. lemma OAI.TriangularUniversal.firstMoment_nonneg line 32
6. lemma OAI.TriangularUniversal.kernelForm_cutoff line 35
7. lemma OAI.TriangularUniversal.kernelForm_cutoff_self_upper line 42
8. def OAI.TriangularUniversal.pointsMeasure line 70
9. instance OAI.TriangularUniversal.pointsMeasure_finite line 72
10. lemma OAI.TriangularUniversal.integral_pointsMeasure line 76
11. lemma OAI.TriangularUniversal.kernelForm_points_points line 83
12. lemma OAI.TriangularUniversal.kernelForm_points_cutoff_lower line 89
13. lemma OAI.TriangularUniversal.fourier_zero_eq_integral line 103
14. lemma OAI.TriangularUniversal.finite_disk_lp line 110

    Source documentation

    The exact finite-disk estimate underlying the density-only bound. The correction uses a cutoff of thickness T and its first moment, never a uniform spacing or local-count bound on S.

    lemma finite_disk_lp (f : LPFunction)
        (hreal : ∀ w, (𝓕 (f : Plane → ℂ) w).im = 0)
        (hpos : ∀ w, 0 ≤ (𝓕 (f : Plane → ℂ) w).re)
        (S : Finset Plane) {R T : ℝ} (hR : 0 ≤ R) (hT : 0 < T)
        (hS : ∀ x ∈ S, ‖x‖ ≤ R) :
        2*(S.card : ℝ)*((∫ z, f z).re - firstMoment f/T) -
          ((∫ z, f z).re + firstMoment f/T)*Real.pi*(R+T)^2 ≤
          ∑ x ∈ S, ∑ y ∈ S, (f (x-y)).re := by
    …

    Mentions: OAI.TriangularUniversal.LPFunction, OAI.TriangularUniversal.Plane, OAI.TriangularUniversal.firstMoment

15. lemma OAI.TriangularUniversal.ofReal_finset_sum_le line 128
16. lemma OAI.TriangularUniversal.offdiag_sum_eq line 137
17. lemma OAI.TriangularUniversal.normalized_offdiag_minorization line 151
18. lemma OAI.TriangularUniversal.finite_disk_energy_lp line 173
19. lemma OAI.TriangularUniversal.density_count_eventually_pos line 210
20. lemma OAI.TriangularUniversal.density_volume_ratio line 219
21. lemma OAI.TriangularUniversal.density_lp_epsilon line 229
22. lemma OAI.TriangularUniversal.density_lp line 255

    Source documentation

    Source §2, density-only linear programming bound, for the exact ordered-pair centered-disk ENNReal liminf. This requires no uniform separation, special local-count bound, finite energy, or decay of the potential.

    lemma density_lp (f : LPFunction)
        (hreal : ∀ w, (𝓕 (f : Plane → ℂ) w).im = 0)
        (hpos : ∀ w, 0 ≤ (𝓕 (f : Plane → ℂ) w).re)
        (g : ℝ → ℝ) (hminor : ∀ x : Plane, x ≠ 0 → (f x).re ≤ g (‖x‖^2))
        {C : Set Plane} (hD : DensityOne C) :
        ENNReal.ofReal ((∫ z, f z).re - (f 0).re) ≤ energy g C := by
    …

    Mentions: OAI.TriangularUniversal.LPFunction, OAI.TriangularUniversal.Plane, OAI.TriangularUniversal.DensityOne, OAI.TriangularUniversal.energy