OAI/Analysis/SignedDisk/DiskKernels1.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.SignedDisk.DiskKernels.RadiusDensity line 23

   Source documentation

   An ordinary nonnegative probability density supported on a radius interval.

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

2. instance OAI.SignedDisk.DiskKernels.(instance at line 31) line 31
3. def OAI.SignedDisk.DiskKernels.tail line 34
4. lemma OAI.SignedDisk.DiskKernels.tail_nonneg line 37
5. lemma OAI.SignedDisk.DiskKernels.tail_le_one line 40
6. lemma OAI.SignedDisk.DiskKernels.tail_one line 45
7. lemma OAI.SignedDisk.DiskKernels.tail_zero line 54
8. lemma OAI.SignedDisk.DiskKernels.tail_lipschitz line 64
9. def OAI.SignedDisk.DiskKernels.kernel line 76
10. lemma OAI.SignedDisk.DiskKernels.kernel_lipschitz line 79
11. lemma OAI.SignedDisk.DiskKernels.kernel_one line 86
12. lemma OAI.SignedDisk.DiskKernels.kernel_zero line 89
13. lemma OAI.SignedDisk.DiskKernels.kernel_eq_integral line 94

    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.SignedDisk.DiskKernels.RadiusDensity, OAI.SignedDisk.DiskKernels.kernel

14. def OAI.SignedDisk.DiskKernels.mix line 104

    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.SignedDisk.DiskKernels.RadiusDensity

15. lemma OAI.SignedDisk.DiskKernels.convex_zero line 120

    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
    …

16. def OAI.SignedDisk.DiskKernels.inverseCube line 133
17. def OAI.SignedDisk.DiskKernels.cubeMass line 135
18. lemma OAI.SignedDisk.DiskKernels.inverseCube_bounds line 137
19. lemma OAI.SignedDisk.DiskKernels.continuousOn_inverseCube line 152
20. lemma OAI.SignedDisk.DiskKernels.cubeMass_lower line 158
21. lemma OAI.SignedDisk.DiskKernels.cubeMass_pos line 173
22. def OAI.SignedDisk.DiskKernels.cubeDensity line 176
23. lemma OAI.SignedDisk.DiskKernels.cubeDensity_integrable line 179
24. lemma OAI.SignedDisk.DiskKernels.cubeDensity_integral line 183
25. lemma OAI.SignedDisk.DiskKernels.cubeDensity_nonneg line 189
26. lemma OAI.SignedDisk.DiskKernels.cubeDensity_bound line 196
27. def OAI.SignedDisk.DiskKernels.inverseCubeDensity line 214

    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.SignedDisk.DiskKernels.RadiusDensity

28. def OAI.SignedDisk.DiskKernels.enlarge line 223
29. theorem OAI.SignedDisk.DiskKernels.kernel_pairing line 233

    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.SignedDisk.DiskKernels.RadiusDensity, OAI.SignedDisk.DiskKernels.kernel

30. def OAI.SignedDisk.DiskMoments.moment line 265
31. def OAI.SignedDisk.DiskMoments.radialDerivative line 268
32. lemma OAI.SignedDisk.DiskMoments.continuous_radialDerivative line 271
33. lemma OAI.SignedDisk.DiskMoments.moment_coefficient line 274
34. lemma OAI.SignedDisk.DiskMoments.hasDerivAt_signedAverage_fixed line 280
35. lemma OAI.SignedDisk.DiskMoments.moment_eq line 286
36. lemma OAI.SignedDisk.DiskMoments.integral_radialDerivative line 296
37. lemma OAI.SignedDisk.DiskMoments.cubeDensity_moment_integrable line 305
38. lemma OAI.SignedDisk.DiskMoments.cubeDensity_moment_integral line 323
39. lemma OAI.SignedDisk.DiskMoments.gradient_hasCompactSupport line 346
40. lemma OAI.SignedDisk.DiskMoments.moment_density_integrable line 349
41. theorem OAI.SignedDisk.DiskKernels.kernel_pairing_local line 359

    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.SignedDisk.DiskKernels.RadiusDensity, OAI.SignedDisk.DiskKernels.kernel

42. theorem OAI.SignedDisk.DiskMoments.balanced_kernel line 387

    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.SignedDisk.DiskMoments.signedAverage