OAI/Analysis/DiskMaximal/GreenBounds.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PlanePotential.integral_affine line 42
2. lemma OAI.PlanePotential.integrable_affine_iff line 53
3. lemma OAI.PlanePotential.integral_affine_reverse line 64
4. lemma OAI.PlanePotential.segment_ftc line 69
5. def OAI.PlanePotential.segmentForm line 82
6. def OAI.PlanePotential.pullbackForm line 84
7. lemma OAI.PlanePotential.pullback_identity line 87
8. lemma OAI.PlanePotential.segmentForm_continuous line 97
9. lemma OAI.PlanePotential.segmentForm_integrable_column line 103
10. lemma OAI.PlanePotential.pullbackForm_measurable line 109
11. lemma OAI.PlanePotential.pullbackForm_integrable_column line 116
12. lemma OAI.PlanePotential.pullback_column_integral line 123
13. lemma OAI.PlanePotential.pullback_column_norm line 130
14. lemma OAI.PlanePotential.segmentForm_bound line 138
15. lemma OAI.PlanePotential.segment_weight_integrable line 149
16. theorem OAI.PlanePotential.pullbackForm_integrable line 156

    Source documentation

    Absolute integrability justifies the double integral even at t approaching zero.

    theorem pullbackForm_integrable {ψ g : ℂ → ℝ} (hψ : Continuous ψ)
        (hψc : HasCompactSupport ψ) (hg : ContDiff ℝ 1 g) {D : ℝ}
        (hD : ∀ y, ‖fderiv ℝ g y‖ ≤ D) (x : ℂ) :
        Integrable (fun p : ℝ × ℂ => pullbackForm ψ g x p.1 p.2)
          ((volume.restrict (Ioc (0:ℝ) 1)).prod volume) := by
    …

    Mentions: OAI.PlanePotential.pullbackForm

17. lemma OAI.PlanePotential.segmentForm_integrable line 174
18. lemma OAI.PlanePotential.green_pullback line 191
19. theorem OAI.PlanePotential.green_representation line 196

    Source documentation

    The true segment-kernel representation, with Fubini justified absolutely.

    theorem green_representation {ψ g : ℂ → ℝ} (hψ : Continuous ψ)
        (hψc : HasCompactSupport ψ) (hg : ContDiff ℝ 1 g) {D : ℝ}
        (hD : ∀ y, ‖fderiv ℝ g y‖ ≤ D) (hψ1 : ∫ z, ψ z = 1) (x : ℂ) :
        (∫ y, fderiv ℝ g y (green ψ x y)) = g x-∫ z, ψ z*g z := by
    …

    Mentions: OAI.PlanePotential.green

20. lemma OAI.PlanePotential.lintegral_norm_rpow_near line 230
21. lemma OAI.PlanePotential.lintegral_norm_rpow_far line 236
22. lemma OAI.PlanePotential.lintegral_translated_near line 242
23. lemma OAI.PlanePotential.lintegral_translated_far line 255
24. lemma OAI.PlanePotential.norm_power_bound line 264
25. lemma OAI.PlanePotential.kernel_near_three_halves line 277
26. lemma OAI.PlanePotential.kernel_far_three_halves line 297
27. lemma OAI.PlanePotential.green_diagonal line 322
28. lemma OAI.PlanePotential.green_size_all line 325
29. lemma OAI.PlanePotential.green_near_column line 335
30. lemma OAI.PlanePotential.green_far_column line 350
31. def OAI.PlanePotential.cancelledGreen line 381

    Source documentation

    The center is subtracted only off the near region, so this measurable kernel retains integrability at the center and realizes zero-mass cancellation.

    def cancelledGreen (ψ : ℂ → ℝ) (z : ℂ) (a : ℝ) (x y : ℂ) : ℂ :=
    …

32. lemma OAI.PlanePotential.cancelledGreen_measurable line 384
33. lemma OAI.PlanePotential.green_piece_column line 392
34. theorem OAI.PlanePotential.kernel_column_lp line 434
35. lemma OAI.PlanePotential.potential_domination line 469

    Source documentation

    No pointwise integrability assertion for the singular kernel is needed in this domination: the Bochner integral is bounded by the nonnegative integral.

    lemma potential_domination {L : ℂ → ℂ} (hL : Measurable L) {b : ℂ → ℂ}
        (hb : Integrable b) :
        ENNReal.ofReal |∫ y, ⟪L y,b y⟫| ≤
          ∫⁻ y, ENNReal.ofReal ‖L y‖ ∂volume.withDensity (fun y => ENNReal.ofReal ‖b y‖) := by
    …

36. theorem OAI.PlanePotential.cancelled_potential_lp line 487
37. lemma OAI.PlanePotential.zero_mass_kernel_shift line 523
38. lemma OAI.PlanePotential.cancelled_potential_eq line 538
39. lemma OAI.PlanePotential.column_scaling line 548

    Source documentation

    Uniform scaling of the exact p-th power column constant: in dimension two and at p=3/2 its radius dependence is precisely a^(1/2).

    lemma column_scaling {K D a : ℝ} (hD : 0 ≤ D) (ha : 0 < a) :
        K^(3/2:ℝ)*(4*Real.pi*(4*a)^(1/2:ℝ)) +
          (D*a)^(3/2:ℝ)*(2*Real.pi/(2*a)) =
          (8*Real.pi*K^(3/2:ℝ)+Real.pi*D^(3/2:ℝ))*a^(1/2:ℝ) := by
    …

40. theorem OAI.PlanePotential.green_zero_piece_lp line 562