OAI/Analysis/SignedDisk/LocalCancellation2.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SignedDisk.LocalCancellation.integrable_bounded_pairing line 21
2. lemma OAI.SignedDisk.LocalCancellation.position_bound line 30
3. lemma OAI.SignedDisk.LocalCancellation.corrected_increment_bound line 43

   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.SignedDisk.LocalCancellation.ErrorPiece, OAI.SignedDisk.LocalCancellation.coarseMass, OAI.SignedDisk.LocalCancellation.errorPrice

4. lemma OAI.SignedDisk.DiskKernels.kernel_nonneg line 102
5. lemma OAI.SignedDisk.DiskKernels.kernel_le_one line 105
6. lemma OAI.SignedDisk.DiskKernels.complex_kernel_lipschitz line 108
7. lemma OAI.SignedDisk.DiskKernels.complex_kernel_bound line 112
8. lemma OAI.SignedDisk.DiskKernels.difference_bound line 116
9. lemma OAI.SignedDisk.DiskKernels.difference_support line 122
10. lemma OAI.SignedDisk.DiskKernels.tendsto_kernel line 144

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

11. lemma OAI.SignedDisk.DiskKernels.tendsto_kernel_pairing line 170

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

12. theorem OAI.SignedDisk.LocalCancellation.size_step line 202
13. lemma OAI.SignedDisk.DiskGeometry.thinShell_eq_diff line 258
14. lemma OAI.SignedDisk.DiskGeometry.volume_thinShell line 266

    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.SignedDisk.DiskGeometry.thinShell

15. lemma OAI.SignedDisk.DiskGeometry.measurableSet_shellPairs line 282
16. def OAI.SignedDisk.DiskGeometry.shellMass line 286
17. lemma OAI.SignedDisk.DiskGeometry.measurable_shellMass line 288
18. lemma OAI.SignedDisk.DiskGeometry.shell_symm line 292
19. lemma OAI.SignedDisk.DiskGeometry.lintegral_shellMass line 296

    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.SignedDisk.DiskGeometry.shellMass

20. lemma OAI.SignedDisk.DiskGeometry.shellMass_exception line 318
21. lemma OAI.SignedDisk.DiskGeometry.thinShell_subset_endpoint line 330

    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.SignedDisk.DiskGeometry.thinShell

22. def OAI.SignedDisk.DiskScales.width line 344
23. lemma OAI.SignedDisk.DiskScales.width_pos line 346
24. lemma OAI.SignedDisk.DiskScales.width_le line 350
25. lemma OAI.SignedDisk.DiskScales.width_succ line 354
26. lemma OAI.SignedDisk.DiskScales.width_antitone line 358
27. lemma OAI.SignedDisk.DiskScales.tendsto_width line 365
28. lemma OAI.SignedDisk.DiskScales.width_rpow line 371
29. lemma OAI.SignedDisk.DiskScales.ratio_norm_lt line 378
30. lemma OAI.SignedDisk.DiskScales.summable_width_rpow line 382
31. lemma OAI.SignedDisk.DiskScales.tsum_width_rpow line 387
32. lemma OAI.SignedDisk.DiskScales.scaled_increment line 393
33. lemma OAI.SignedDisk.DiskScales.exists_admissible_width line 431

    Source documentation

    A single small width works for both shell geometry and every smaller width.

    lemma exists_admissible_width : ∃ δ₀ : ℝ, 0 < δ₀ ∧ δ₀ ≤ 1/4 ∧
        ∀ δ : ℝ, 0 < δ → δ ≤ δ₀ → δ ≤ (δ^(1/5 : ℝ))^2/1600 := by
    …