OAI/Analysis/DiskMaximal/Cancellation.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LocalCancellation.integrable_lip_mul line 20
2. lemma OAI.LocalCancellation.lip_cancellation line 39

   Source documentation

   Cancellation against the actual integrable complex error density.

   lemma lip_cancellation {b F : ℂ → ℂ} (hb : Integrable b) (hzero : ∫ y, b y = 0)
       {L : ℝ≥0} (hF : LipschitzWith L F) (z : ℂ) {s : ℝ}
       (hsupp : ∀ᵐ y, b y ≠ 0 → ‖y-z‖ ≤ s) :
       ‖∫ y, F y * b y‖ ≤ (L : ℝ) * s * ∫ y, ‖b y‖ := by
   …

3. lemma OAI.LocalCancellation.bounded_pairing line 60
4. lemma OAI.LocalCancellation.min_one_le_rpow line 68
5. structure OAI.LocalCancellation.ErrorPiece line 79
6. def OAI.LocalCancellation.ErrorPiece.mass line 89
7. lemma OAI.LocalCancellation.ErrorPiece.mass_nonneg line 91
8. lemma OAI.LocalCancellation.piece_discount line 95

   Source documentation

   The single-piece interpolation discount, with no smoothness assumed on the density.

   lemma piece_discount {Cs α δ C : ℝ} (b : ErrorPiece Cs)
       (hα0 : 0 ≤ α) (hα1 : α ≤ 1) (hδ : 0 < δ) (hδ1 : δ ≤ 1)
       (hC : 1 ≤ C) {L : ℝ≥0} {F : ℂ → ℂ} (hF : LipschitzWith L F)
       (hFb : ∀ y, ‖F y‖ ≤ 1) (hLC : (L : ℝ) * Cs ≤ C / δ) :
       ‖∫ y, F y * b.density y‖ ≤ C * (b.size / δ) ^ α * b.mass := by
   …

   Mentions: OAI.LocalCancellation.ErrorPiece

9. lemma OAI.LocalCancellation.position_lipschitz line 131

   Source documentation

   Multiplication by the position keeps a bounded-support Lipschitz test Lipschitz.

   lemma position_lipschitz {F : ℂ → ℂ} {L M R : ℝ≥0} (hF : LipschitzWith L F)
       (hM : ∀ y, ‖F y‖ ≤ M) (x : ℂ)
       (hR : ∀ y, F y ≠ 0 → ‖y-x‖ ≤ R) :
       LipschitzWith (R*L+M) (fun y => star (y-x) * F y) := by
   …

10. def OAI.LocalCancellation.correction line 161
11. lemma OAI.LocalCancellation.correction_eq line 163
12. lemma OAI.LocalCancellation.norm_correction line 173
13. lemma OAI.LocalCancellation.correction_cap_bound line 177
14. lemma OAI.LocalCancellation.correction_bounded line 187
15. lemma OAI.LocalCancellation.corrected_lipschitz line 198

    Source documentation

    Global Lipschitz control of the corrected increment test.

    lemma corrected_lipschitz {F : ℂ → ℂ} {L M R H : ℝ≥0} (hF : LipschitzWith L F)
        (hM : ∀ y, ‖F y‖ ≤ M) (x z : ℂ)
        (hR : ∀ y, F y ≠ 0 → ‖y-x‖ ≤ R) (hH : ‖(star (z-x))⁻¹‖ ≤ H) :
        LipschitzWith (L+H*(R*L+M)) (fun y => correction x z y * F y) := by
    …

    Mentions: OAI.LocalCancellation.correction

16. def OAI.LocalCancellation.errorPrice line 224
17. lemma OAI.LocalCancellation.errorPrice_nonneg line 227
18. lemma OAI.LocalCancellation.square_rpow line 231
19. lemma OAI.LocalCancellation.coarse_mass_mul_le line 235
20. lemma OAI.LocalCancellation.fine_size_sum_le line 252
21. lemma OAI.LocalCancellation.total_pairing_discount line 280
22. lemma OAI.LocalCancellation.fine_pairing_bound line 297

    Source documentation

    All fine errors together retain the stronger, summable power of the width.

    lemma fine_pairing_bound {Cs α δ : ℝ} (b : ι → ErrorPiece Cs) (hCs : 0 ≤ Cs)
        (hα : α ≤ 1) (hδ : 0 ≤ δ) (hδ1 : δ ≤ 1)
        {L : ℝ≥0} {F : ℂ → ℂ} (hF : LipschitzWith L F) :
        ‖∑ d ∈ Finset.univ.filter (fun d => (b d).size < δ^2), ∫ y, F y*(b d).density y‖ ≤
          (L : ℝ)*Cs*δ^(2*(1-α))*errorPrice b α := by
    …

    Mentions: OAI.LocalCancellation.ErrorPiece, OAI.LocalCancellation.errorPrice

23. def OAI.LocalCancellation.densityMeasure line 329

    Source documentation

    Norm total-variation measure of an actual complex density.

    def densityMeasure (b : ℂ → ℂ) : Measure ℂ := volume.withDensity (fun y => ENNReal.ofReal ‖b y‖)

24. lemma OAI.LocalCancellation.densityMeasure_apply line 331
25. lemma OAI.LocalCancellation.densityMeasure_univ line 337
26. lemma OAI.LocalCancellation.densityMeasure_finite line 341
27. lemma OAI.LocalCancellation.pairing_majorant line 347

    Source documentation

    A cap decomposition bound, with all integrals over genuine densities.

    lemma pairing_majorant {b F : ℂ → ℂ} (hb : Integrable b) {A : Set ℂ}
        (hA : MeasurableSet A) (c d : ℝ)
        (hF : ∀ y, ‖F y‖ ≤ c + d*A.indicator (fun _ => (1 : ℝ)) y) :
        ‖∫ y, F y*b y‖ ≤ c*(∫ y, ‖b y‖)+d*(∫ y in A, ‖b y‖) := by
    …

28. lemma OAI.LocalCancellation.moment_correction line 369

    Source documentation

    Cancellation of an exact complex moment allows an off-center correction.

    lemma moment_correction {b F : ℂ → ℂ} (x z : ℂ)
        (hF : Integrable (fun y => F y*b y))
        (hM : Integrable (fun y => star (y-x)*F y*b y))
        (hzero : ∫ y, star (y-x)*F y*b y = 0) :
        (∫ y, F y*b y) = ∫ y, (1-star (y-x)/star (z-x))*F y*b y := by
    …

29. lemma OAI.LocalCancellation.corrected_pairing_cap line 385
30. lemma OAI.LocalCancellation.supported_pairing line 409
31. def OAI.LocalCancellation.coarseMeasure line 423
32. def OAI.LocalCancellation.coarseMass line 426
33. lemma OAI.LocalCancellation.coarseMass_nonneg line 429
34. lemma OAI.LocalCancellation.coarseMeasure_apply line 432
35. instance OAI.LocalCancellation.coarseMeasure_finite line 439
36. lemma OAI.LocalCancellation.coarseMass_univ line 445
37. lemma OAI.LocalCancellation.coarseMass_bound line 449
38. lemma OAI.LocalCancellation.increment_bound line 455

    Source documentation

    The uncorrected increment costs only shell mass plus the fine-error discount.

    lemma increment_bound {Cs α δ : ℝ} (b : ι → ErrorPiece Cs) (hCs : 0 ≤ Cs)
        (hα : α ≤ 1) (hδ : 0 ≤ δ) (hδ1 : δ ≤ 1)
        {L : ℝ≥0} {F : ℂ → ℂ} (hF : LipschitzWith L F) {D : Set ℂ} (hD : MeasurableSet D)
        (hFb : ∀ y, ‖F y‖ ≤ 1) (hFD : ∀ y, F y ≠ 0 → y ∈ D) :
        ‖∑ d, ∫ y, F y*(b d).density y‖ ≤
          coarseMass b δ D+(L : ℝ)*Cs*δ^(2*(1-α))*errorPrice b α := by
    …

    Mentions: OAI.LocalCancellation.ErrorPiece, OAI.LocalCancellation.coarseMass, OAI.LocalCancellation.errorPrice

39. lemma OAI.LocalCancellation.integrable_bounded_pairing line 478
40. lemma OAI.LocalCancellation.position_bound line 487
41. lemma OAI.LocalCancellation.corrected_increment_bound line 500

    Source documentation

    The decisive corrected active increment, prior to substitution of the dyadic powers. The zero moment is the exact one furnished by two balanced kernels, not a bound.

    lemma corrected_increment_bound {Cs α δ ρ : ℝ} (b : ι → ErrorPiece Cs) (hCs : 0 ≤ Cs)
        (hα : α ≤ 1) (hδ : 0 ≤ δ) (hδ1 : δ ≤ 1) (hρ : 0 ≤ ρ)
        {L : ℝ≥0} {F : ℂ → ℂ} (hF : LipschitzWith L F) {D : Set ℂ} (hD : MeasurableSet D)
        (hFb : ∀ y, ‖F y‖ ≤ 1) (hFD : ∀ y, F y ≠ 0 → y ∈ D) (x z : ℂ)
        (hz : (1 : ℝ)/2 ≤ ‖z-x‖) (hD3 : ∀ y ∈ D, ‖y-x‖ ≤ 3)
        (hzero : ∑ d, ∫ y, star (y-x)*F y*(b d).density y = 0) :
        ‖∑ d, ∫ y, F y*(b d).density y‖ ≤
          2*ρ*coarseMass b δ univ+7*coarseMass b δ (D \ Metric.ball z ρ)+
          ((L : ℝ)+2*(3*(L : ℝ)+1))*Cs*δ^(2*(1-α))*errorPrice b α := by
    …

    Mentions: OAI.LocalCancellation.ErrorPiece, OAI.LocalCancellation.coarseMass, OAI.LocalCancellation.errorPrice

42. lemma OAI.DiskKernels.kernel_nonneg line 559
43. lemma OAI.DiskKernels.kernel_le_one line 562
44. lemma OAI.DiskKernels.complex_kernel_lipschitz line 565
45. lemma OAI.DiskKernels.complex_kernel_bound line 569
46. lemma OAI.DiskKernels.difference_bound line 573
47. lemma OAI.DiskKernels.difference_support line 579
48. lemma OAI.DiskKernels.tendsto_kernel line 605

    Source documentation

    At every point away from the boundary circle, all such mixtures tend to the actual sharp disk. No convergence of the chosen radius densities is assumed.

    lemma tendsto_kernel {r : ℝ} {δ : ℕ → ℝ} {M : ℕ → ℝ≥0}
        (k : ∀ n, RadiusDensity (r-δ n) (r+δ n) (M n))
        (hδ : Tendsto δ atTop (𝓝 0)) (x y : ℂ) (hy : ‖y-x‖ ≠ r) :
        Tendsto (fun n => kernel (k n) x y) atTop
          (𝓝 ((Metric.ball x r).indicator (fun _ => (1 : ℝ)) y)) := by
    …

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

49. lemma OAI.DiskKernels.tendsto_kernel_pairing line 631

    Source documentation

    Dominated convergence of an arbitrary sequence of mixtures against each actual absolutely continuous finite vector measure.

    lemma tendsto_kernel_pairing {r : ℝ} {δ : ℕ → ℝ} {M : ℕ → ℝ≥0}
        (k : ∀ n, RadiusDensity (r-δ n) (r+δ n) (M n))
        (hδ : Tendsto δ atTop (𝓝 0)) (x : ℂ) {b : ℂ → ℂ} (hb : Integrable b) :
        Tendsto (fun n => ∫ y, (kernel (k n) x y : ℂ)*b y) atTop
          (𝓝 (∫ y in Metric.ball x r, b y)) := by
    …

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

50. theorem OAI.LocalCancellation.size_step line 663
51. lemma OAI.DiskGeometry.thinShell_eq_diff line 719
52. lemma OAI.DiskGeometry.volume_thinShell line 727

    Source documentation

    Exact area of an annulus, including the inner and outer circles.

    lemma volume_thinShell (x : ℂ) {r δ : ℝ} (hδ : 0 ≤ δ) (hr : δ ≤ r) :
        volume (thinShell x r δ) = ENNReal.ofReal (4*Real.pi*r*δ) := by
    …

    Mentions: OAI.DiskGeometry.thinShell

53. lemma OAI.DiskGeometry.measurableSet_shellPairs line 743
54. def OAI.DiskGeometry.shellMass line 747
55. lemma OAI.DiskGeometry.measurable_shellMass line 749
56. lemma OAI.DiskGeometry.shell_symm line 753
57. lemma OAI.DiskGeometry.lintegral_shellMass line 757

    Source documentation

    The integrated shell mass is its exact area times the total input mass.

    lemma lintegral_shellMass (ν : Measure ℂ) [IsFiniteMeasure ν] {r δ : ℝ}
        (hδ : 0 ≤ δ) (hr : δ ≤ r) :
        (∫⁻ x, shellMass ν r δ x) = ENNReal.ofReal (4*Real.pi*r*δ)*ν univ := by
    …

    Mentions: OAI.DiskGeometry.shellMass

58. lemma OAI.DiskGeometry.shellMass_exception line 779
59. lemma OAI.DiskGeometry.thinShell_subset_endpoint line 791

    Source documentation

    A shell whose radius is sufficiently close to an endpoint is contained in the endpoint annulus; this covers forced endpoint radii as well.

    lemma thinShell_subset_endpoint {x : ℂ} {r a δ : ℝ} (hra : |r-a| ≤ δ) :
        thinShell x r δ ⊆ thinShell x a (2*δ) := by
    …

    Mentions: OAI.DiskGeometry.thinShell