OAI/Analysis/DiskMaximal/Moments.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DiskMoments.rotation line 20
2. lemma OAI.DiskMoments.rotation_apply line 22
3. lemma OAI.DiskMoments.rotation_zero line 26
4. lemma OAI.DiskMoments.rotation_norm line 28
5. lemma OAI.DiskMoments.integral_rotation line 31
6. lemma OAI.DiskMoments.hasDerivAt_rotation line 42
7. theorem OAI.DiskMoments.rotational_moment_zero line 52

   Source documentation

   The circulation moment of a smooth gradient on a disk vanishes.

   theorem rotational_moment_zero {g : ℂ → ℝ} (hg : ContDiff ℝ 1 g)
       (x : ℂ) (r : ℝ) :
       (∫ z in Metric.ball 0 r, (fderiv ℝ g (x + z)) (Complex.I * z)) = 0 := by
   …

8. lemma OAI.DiskMoments.integral_translate_ball line 94
9. lemma OAI.DiskMoments.continuous_gradient line 104
10. lemma OAI.DiskMoments.real_moment_integrand line 108
11. lemma OAI.DiskMoments.imaginary_moment_integrand line 113
12. theorem OAI.DiskMoments.imaginary_moment_zero line 120

    Source documentation

    The imaginary part of the actual complex disk moment is zero.

    theorem imaginary_moment_zero {g : ℂ → ℝ} (hg : ContDiff ℝ 1 g)
        (x : ℂ) (r : ℝ) :
        (∫ y in Metric.ball x r, star (y - x) * gradient g y).im = 0 := by
    …

13. theorem OAI.DiskMoments.hasDerivAt_integral_unitDisk line 138

    Source documentation

    Differentiate a disk average on its fixed unit-disk model.

    theorem hasDerivAt_integral_unitDisk {g : ℂ → ℝ} (hg : ContDiff ℝ 1 g)
        (x : ℂ) (t : ℝ) :
        HasDerivAt (fun s : ℝ => ∫ z in Metric.ball (0 : ℂ) 1, g (x + s • z))
          (∫ z in Metric.ball (0 : ℂ) 1, (fderiv ℝ g (x + t • z)) z) t := by
    …

14. lemma OAI.DiskMoments.integral_scale_ball line 179
15. def OAI.DiskMoments.signedAverage line 187

    Source documentation

    Signed normalized average on a centered Euclidean disk in the complex plane.

    def signedAverage (g : ℂ → ℝ) (x : ℂ) (t : ℝ) : ℝ :=
    …

16. lemma OAI.DiskMoments.signedAverage_fixedDomain line 190
17. lemma OAI.DiskMoments.integral_fderiv_scale line 196
18. lemma OAI.DiskMoments.integral_fderiv_moment_real line 211
19. theorem OAI.DiskMoments.hasDerivAt_signedAverage line 225

    Source documentation

    The radial disk derivative is the real part of its complex moment.

    theorem hasDerivAt_signedAverage {g : ℂ → ℝ} (hg : ContDiff ℝ 1 g)
        (x : ℂ) {t : ℝ} (ht : 0 < t) :
        HasDerivAt (signedAverage g x)
          ((∫ y in Metric.ball x t, star (y-x) * gradient g y).re / (Real.pi * t^3)) t := by
    …

    Mentions: OAI.DiskMoments.signedAverage

20. lemma OAI.DiskMoments.ball_ae_closedBall line 238
21. lemma OAI.DiskMoments.continuous_integral_fderiv_unit line 245
22. structure OAI.DiskKernels.RadiusDensity line 263

    Source documentation

    An ordinary nonnegative probability density supported on a radius interval.

    structure RadiusDensity (a b : ℝ) (M : ℝ≥0) where
    …

23. instance OAI.DiskKernels.(instance at line 271) line 271
24. def OAI.DiskKernels.tail line 274
25. lemma OAI.DiskKernels.tail_nonneg line 277
26. lemma OAI.DiskKernels.tail_le_one line 280
27. lemma OAI.DiskKernels.tail_one line 285
28. lemma OAI.DiskKernels.tail_zero line 294
29. lemma OAI.DiskKernels.tail_lipschitz line 304
30. def OAI.DiskKernels.kernel line 316
31. lemma OAI.DiskKernels.kernel_lipschitz line 319
32. lemma OAI.DiskKernels.kernel_one line 326
33. lemma OAI.DiskKernels.kernel_zero line 329
34. lemma OAI.DiskKernels.kernel_eq_integral line 334

    Source documentation

    The radial tail is exactly the positive average of disk indicators.

    lemma kernel_eq_integral {a b : ℝ} {M : ℝ≥0} (k : RadiusDensity a b M) (x y : ℂ) :
        kernel k x y = ∫ t, k t * (Metric.ball x t).indicator (fun _ => (1 : ℝ)) y := by
    …

    Mentions: OAI.DiskKernels.RadiusDensity, OAI.DiskKernels.kernel

35. def OAI.DiskKernels.mix line 344

    Source documentation

    Convex combinations preserve all density and support bounds.

    def mix {a b : ℝ} {M : ℝ≥0} (k l : RadiusDensity a b M)
        (w : ℝ) (hw0 : 0 ≤ w) (hw1 : w ≤ 1) : RadiusDensity a b M where
    …

    Mentions: OAI.DiskKernels.RadiusDensity

36. lemma OAI.DiskKernels.convex_zero line 360

    Source documentation

    Two oppositely signed moments admit an explicit convex zero.

    lemma convex_zero {A B : ℝ} (hA : 0 ≤ A) (hB : B ≤ 0) :
        ∃ w : ℝ, 0 ≤ w ∧ w ≤ 1 ∧ w*A+(1-w)*B = 0 := by
    …

37. def OAI.DiskKernels.inverseCube line 373
38. def OAI.DiskKernels.cubeMass line 375
39. lemma OAI.DiskKernels.inverseCube_bounds line 377
40. lemma OAI.DiskKernels.continuousOn_inverseCube line 392
41. lemma OAI.DiskKernels.cubeMass_lower line 398
42. lemma OAI.DiskKernels.cubeMass_pos line 413
43. def OAI.DiskKernels.cubeDensity line 416
44. lemma OAI.DiskKernels.cubeDensity_integrable line 419
45. lemma OAI.DiskKernels.cubeDensity_integral line 423
46. lemma OAI.DiskKernels.cubeDensity_nonneg line 429
47. lemma OAI.DiskKernels.cubeDensity_bound line 436
48. def OAI.DiskKernels.inverseCubeDensity line 454

    Source documentation

    The concrete normalized inverse-cube density, with an absolute width bound.

    def inverseCubeDensity (a b : ℝ) (ha : (1 : ℝ)/2 ≤ a) (hb : b ≤ 3) (hab : a < b) :
        RadiusDensity a b ⟨216/(b-a), by positivity⟩ where
    …

    Mentions: OAI.DiskKernels.RadiusDensity

49. def OAI.DiskKernels.enlarge line 463
50. theorem OAI.DiskKernels.kernel_pairing line 473

    Source documentation

    Fubini identifies a radial kernel pairing with the average of disk pairings.

    theorem kernel_pairing {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
        {a b : ℝ} {M : ℝ≥0} (k : RadiusDensity a b M) (x : ℂ)
        {f : ℂ → E} (hf : Integrable f) :
        (∫ y, kernel k x y • f y) = ∫ t, k t • ∫ y in Metric.ball x t, f y := by
    …

    Mentions: OAI.DiskKernels.RadiusDensity, OAI.DiskKernels.kernel

51. def OAI.DiskMoments.moment line 505
52. def OAI.DiskMoments.radialDerivative line 508
53. lemma OAI.DiskMoments.continuous_radialDerivative line 511
54. lemma OAI.DiskMoments.moment_coefficient line 514
55. lemma OAI.DiskMoments.hasDerivAt_signedAverage_fixed line 520
56. lemma OAI.DiskMoments.moment_eq line 526
57. lemma OAI.DiskMoments.integral_radialDerivative line 536
58. lemma OAI.DiskMoments.cubeDensity_moment_integrable line 545
59. lemma OAI.DiskMoments.cubeDensity_moment_integral line 563
60. lemma OAI.DiskMoments.gradient_hasCompactSupport line 586
61. lemma OAI.DiskMoments.moment_density_integrable line 589
62. theorem OAI.DiskKernels.kernel_pairing_local line 599

    Source documentation

    Only integrability over the largest supporting disk is required.

    theorem kernel_pairing_local {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
        [CompleteSpace E] {a b : ℝ} {M : ℝ≥0} (k : RadiusDensity a b M) (x : ℂ)
        {f : ℂ → E} (hf : IntegrableOn f (Metric.ball x b)) :
        (∫ y, kernel k x y • f y) = ∫ t, k t • ∫ y in Metric.ball x t, f y := by
    …

    Mentions: OAI.DiskKernels.RadiusDensity, OAI.DiskKernels.kernel

63. theorem OAI.DiskMoments.balanced_kernel line 627

    Source documentation

    A faithful balanced disk-mixture kernel, with an explicit absolute bound.

    theorem balanced_kernel {g : ℂ → ℝ} (hg : ContDiff ℝ 1 g) (x : ℂ)
        {r δ : ℝ} (hr : r ∈ Icc (1 : ℝ) 2) (hδ : 0 < δ) (hδ' : δ ≤ 1/4)
        (hm : signedAverage g x (r-δ) ≤ signedAverage g x r)
        (hp : signedAverage g x (r+δ) ≤ signedAverage g x r) :
        ∃ k : RadiusDensity (r-δ) (r+δ) ⟨216/δ, by positivity⟩,
          (∫ y, kernel k x y • (star (y-x) * gradient g y)) = 0 := by
    …

    Mentions: OAI.DiskMoments.signedAverage