OAI/Analysis/SignedDisk/PlanePotential1.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SignedDisk.PlanePotential.kernel_lp_three_halves line 29

   Source documentation

   Hölder followed by Tonelli gives the integral-kernel Minkowski estimate at p=3/2. Both measures and the actual joint kernel remain explicit.

   theorem kernel_lp_three_halves {α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
       (μ : Measure α) (ν : Measure β) [SFinite μ] [SFinite ν]
       {K : α × β → ℝ≥0∞} (hK : Measurable K) {C : ℝ≥0∞}
       (hC : ∀ y, (∫⁻ x, (K (x,y))^(3/2:ℝ) ∂μ) ≤ C^(3/2:ℝ)) :
       (∫⁻ x, (∫⁻ y, K (x,y) ∂ν)^(3/2:ℝ) ∂μ) ≤ (C*ν univ)^(3/2:ℝ) := by
   …

2. structure OAI.SignedDisk.FiniteLabels.Law line 72
3. instance OAI.SignedDisk.FiniteLabels.(instance at line 77) line 77
4. def OAI.SignedDisk.FiniteLabels.delta line 79
5. lemma OAI.SignedDisk.FiniteLabels.law_le_one line 84
6. def OAI.SignedDisk.FiniteLabels.move line 88
7. lemma OAI.SignedDisk.FiniteLabels.move_apply line 96
8. def OAI.SignedDisk.FiniteLabels.l1dist line 99
9. lemma OAI.SignedDisk.FiniteLabels.l1dist_nonneg line 100
10. lemma OAI.SignedDisk.FiniteLabels.l1dist_triangle line 101
11. theorem OAI.SignedDisk.FiniteLabels.move_contract line 107

    Source documentation

    Stochastic matrices contract the l1 norm of every signed row difference.

    theorem move_contract (μ ν : Law ι) (P : ι → Law κ) :
        l1dist (move μ P) (move ν P) ≤ l1dist μ ν := by
    …

    Mentions: OAI.SignedDisk.FiniteLabels.Law, OAI.SignedDisk.FiniteLabels.l1dist, OAI.SignedDisk.FiniteLabels.move

12. lemma OAI.SignedDisk.FiniteLabels.move_rows line 126
13. lemma OAI.SignedDisk.FiniteLabels.move_compare line 143
14. lemma OAI.SignedDisk.FiniteLabels.expectation_difference line 147
15. def OAI.SignedDisk.FiniteLabels.switchRow line 159
16. lemma OAI.SignedDisk.FiniteLabels.switchRow_formula line 175
17. lemma OAI.SignedDisk.FiniteLabels.delta_distance line 183
18. theorem OAI.SignedDisk.FiniteLabels.switchRow_distance line 192

    Source documentation

    The row difference is paid by the actual switched mass, not by a bare Lipschitz constant. This is essential to the spatial comparison argument.

    theorem switchRow_distance [DecidableEq ι] (old : ι) (sample sample' : Law κ)
        (target : κ → ι) (p : κ → ℝ) (hp0 : ∀ z, 0 ≤ p z) (hp1 : ∀ z, p z ≤ 1) :
        l1dist (switchRow old sample target p hp0 hp1) (switchRow old sample' target p hp0 hp1)
          ≤ 2*∑ z, |sample z-sample' z| *p z := by
    …

    Mentions: OAI.SignedDisk.FiniteLabels.Law, OAI.SignedDisk.FiniteLabels.l1dist, OAI.SignedDisk.FiniteLabels.switchRow

19. def OAI.SignedDisk.PlanePotential.greenScalar line 226
20. def OAI.SignedDisk.PlanePotential.green line 228
21. lemma OAI.SignedDisk.PlanePotential.segment_support line 230
22. lemma OAI.SignedDisk.PlanePotential.integrable_power_cutoff line 244
23. lemma OAI.SignedDisk.PlanePotential.integral_power_cutoff line 249
24. lemma OAI.SignedDisk.PlanePotential.singular_integral_bound line 255

    Source documentation

    A singular segment integral is genuinely integrable because of its geometric lower cutoff. The bound retains the exact power, rather than a supremum times 1.

    lemma singular_integral_bound {F : ℝ → ℝ} (hFm : Measurable F)
        {q δ B : ℝ} (hq : q < -1) (hδ : 0 < δ) (hB : 0 ≤ B)
        (hzero : ∀ t ∈ Ioc (0:ℝ) 1, t < δ → F t = 0)
        (hbound : ∀ t ∈ Ioc (0:ℝ) 1, |F t| ≤ B*t^q) :
        IntegrableOn F (Ioc (0:ℝ) 1) ∧
          |∫ t in Ioc (0:ℝ) 1, F t| ≤ B*(-(δ/2)^(q+1)/(q+1)) := by
    …

25. lemma OAI.SignedDisk.PlanePotential.greenScalar_measurable line 289
26. lemma OAI.SignedDisk.PlanePotential.green_measurable line 297
27. theorem OAI.SignedDisk.PlanePotential.green_norm_bound line 302

    Source documentation

    Quantitative kernel size on every observation ball, with an explicit constant.

    theorem green_norm_bound {ψ : ℂ → ℝ} (hψm : Measurable ψ) {R X B : ℝ}
        (hψs : ∀ z, ψ z ≠ 0 → ‖z‖ ≤ R) (hψB : ∀ z, |ψ z| ≤ B)
        (hM : 0 < R+X) (hB : 0 ≤ B) {x y : ℂ} (hx : ‖x‖ ≤ X) (hxy : y ≠ x) :
        ‖green ψ x y‖ ≤ 2*B*(R+X)^2/‖y-x‖ := by
    …

    Mentions: OAI.SignedDisk.PlanePotential.green

28. lemma OAI.SignedDisk.PlanePotential.segment_integrand_measurable line 341
29. lemma OAI.SignedDisk.PlanePotential.scalar_data line 348
30. theorem OAI.SignedDisk.PlanePotential.green_difference_bound line 376

    Source documentation

    A difference bound proves the needed cancellation estimate without hiding any differentiation under the singular integral.

    theorem green_difference_bound {ψ : ℂ → ℝ} (hψm : Measurable ψ) {R X B L : ℝ}
        (hψs : ∀ z, ψ z ≠ 0 → ‖z‖ ≤ R) (hψB : ∀ z, |ψ z| ≤ B)
        (hψL : ∀ u v, |ψ u-ψ v| ≤ L*‖u-v‖)
        (hM : 0 < R+X) (hB : 0 ≤ B) (hL : 0 ≤ L)
        {x y z : ℂ} (hx : ‖x‖ ≤ X) (hzx : z ≠ x) (hyz : ‖y-z‖ ≤ ‖z-x‖/2) :
        ‖green ψ x y-green ψ x z‖ ≤
          (8*B*(R+X)^2+(64/3:ℝ)*L*(R+X)^3)*‖y-z‖/‖z-x‖^2 := by
    …

    Mentions: OAI.SignedDisk.PlanePotential.green