OAI/Analysis/SignedDisk/DiskScales3.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SignedDisk.DiskScales.directionTailConstant line 21
2. lemma OAI.SignedDisk.DiskScales.directionTailConstant_pos line 23
3. theorem OAI.SignedDisk.LocalCancellation.direction_tail line 36

   Source documentation

   A genuine superlevel bound with exponent 34/25 > 1 for all neighborhood maxima, independent of the number of positive or cancelling pieces.

   theorem direction_tail {Cs κ : ℝ} (hCs : 0 ≤ Cs) (hκ : 0 < κ) :
       ∃ L : ℝ, 1 ≤ L ∧ ∀ {ι : Type*} [Fintype ι] {e : ℂ} (a : ConeDensity e κ)
         (b : ι → ErrorPiece Cs), ‖e‖ = 1 →
         0 < errorPrice b (1/100) → ∀ t : ℝ, L*errorPrice b (1/100) ≤ t →
         ∀ g : ℂ → ℝ, ContDiff ℝ 1 g →
         ∃ E : Set ℂ, MeasurableSet E ∧
           volume E ≤ ENNReal.ofReal (directionTailConstant Cs κ*(errorPrice b (1/100)/t)^(34/25 : ℝ)) ∧
           ∀ x ∉ E,
             (∀ᵐ y, y ∈ Metric.ball x 3 → a.density y+∑ j, (b j).density y = gradient g y) →
             ∀ r, NeighborhoodRadius g x r →
               max 0 (-inner ℝ e (∫ y in Metric.ball x r, gradient g y)) ≤ t := by
   …

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

4. lemma OAI.SignedDisk.LocalCancellation.cone_ball_nonneg line 96
5. theorem OAI.SignedDisk.LocalCancellation.direction_majorant line 105

   Source documentation

   Full Borel integrable directional price. This is the hard local cancellation estimate, not an assumed maximal-operator endpoint.

   theorem direction_majorant {Cs κ : ℝ} (hCs : 0 ≤ Cs) (hκ : 0 < κ) :
       ∃ C : ℝ, 0 < C ∧ ∀ {ι : Type*} [Fintype ι] {e : ℂ} (a : ConeDensity e κ)
         (b : ι → ErrorPiece Cs), ‖e‖ = 1 →
         ∀ g : ℂ → ℝ, ContDiff ℝ 1 g → ∀ Q : Set ℂ, volume Q ≤ ENNReal.ofReal 1 →
         ∃ F : ℂ → ℝ≥0∞, Measurable F ∧
           (∫⁻ x in Q, F x) ≤ ENNReal.ofReal (C*errorPrice b (1/100)) ∧
           ∀ x, (∀ᵐ y, y ∈ Metric.ball x 3 → a.density y+∑ j, (b j).density y = gradient g y) →
             ∀ r, NeighborhoodRadius g x r →
               ENNReal.ofReal (max 0 (-inner ℝ e (∫ y in Metric.ball x r, gradient g y))) ≤ F x := by
   …

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

6. lemma OAI.SignedDisk.DiskMaximalTools.volume_dilate_five line 174
7. theorem OAI.SignedDisk.DiskMaximalTools.weak_bound_bounded_family line 181

   Source documentation

   The actual Vitali weak-(1,1) estimate, with no assumed maximal inequality.

   theorem weak_bound_bounded_family {ι : Type*} (t : Set ι) (x : ι → ℂ) (r : ι → ℝ)
       (ν : Measure ℂ) {R a : ℝ} (ha : 0 < a)
       (hr : ∀ i ∈ t, 0 < r i) (hR : ∀ i ∈ t, r i ≤ R)
       (hav : ∀ i ∈ t, ENNReal.ofReal a * volume (ball (x i) (r i)) ≤ ν (ball (x i) (r i))) :
       volume (⋃ i ∈ t, ball (x i) (r i)) ≤ (25 / ENNReal.ofReal a) * ν univ := by
   …

8. lemma OAI.SignedDisk.DiskMaximalTools.volume_disk_real line 215
9. theorem OAI.SignedDisk.DiskMaximalTools.weak_bound line 223

   Source documentation

   All high-average balls of a finite measure have a common finite radius bound; the bounded-family Vitali argument therefore controls every radius.

   theorem weak_bound {ν : Measure ℂ} [IsFiniteMeasure ν] {a : ℝ} (ha : 0 < a) :
       volume {x : ℂ | ∃ r : ℝ, 0 < r ∧
         ENNReal.ofReal a * volume (ball x r) ≤ ν (ball x r)} ≤
         (25 / ENNReal.ofReal a) * ν univ := by
   …

10. def OAI.SignedDisk.DiskMaximalTools.rationalMaximal line 247

    Source documentation

    A countable measurable envelope, sufficiently rich for every actual disk.

    def rationalMaximal (ν : Measure ℂ) (x : ℂ) : ℝ≥0∞ :=
    …

11. lemma OAI.SignedDisk.DiskMaximalTools.measurable_ball_mass line 250
12. lemma OAI.SignedDisk.DiskMaximalTools.measurable_rationalMaximal line 256
13. lemma OAI.SignedDisk.DiskMaximalTools.weak_rationalMaximal line 268
14. lemma OAI.SignedDisk.DiskMaximalTools.disk_average_le_rationalMaximal line 283
15. lemma OAI.SignedDisk.DiskMaximalTools.weak_split line 314

    Source documentation

    Truncating an input below half the testing height sharpens weak type by charging only its large values. This is the interpolation mechanism.

    lemma weak_split {ν η : Measure ℂ} [IsFiniteMeasure η] {a : ℝ} (ha : 0 < a)
        (hsplit : ∀ x r, 0 < r → ν (ball x r) ≤ η (ball x r)+
          ENNReal.ofReal (a/2)*volume (ball x r)) :
        volume {x | ENNReal.ofReal a < rationalMaximal ν x} ≤
          (25 / ENNReal.ofReal (a/2)) * η univ := by
    …

    Mentions: OAI.SignedDisk.DiskMaximalTools.rationalMaximal

16. lemma OAI.SignedDisk.DiskMaximalTools.weak_truncated line 340
17. lemma OAI.SignedDisk.DiskMaximalTools.lintegral_rpow_Ioo line 376
18. lemma OAI.SignedDisk.DiskMaximalTools.truncation_layer_single line 389
19. theorem OAI.SignedDisk.DiskMaximalTools.truncation_layer_integral line 420

    Source documentation

    Exact Tonelli computation behind strong maximal interpolation, for every p > 1. The singularity at testing height zero is actually integrated.

    theorem truncation_layer_integral {α : Type*} [MeasurableSpace α] {μ : Measure α}
        [SFinite μ] {f : α → ℝ} (hf : Measurable f) (hf0 : ∀ x, 0 ≤ f x) {p : ℝ} (hp : 1 < p) :
        (∫⁻ t in Ioi 0,
          (∫⁻ x, if t < 2*f x then ENNReal.ofReal (f x) else 0 ∂μ)*ENNReal.ofReal (t^(p-2))) =
          ENNReal.ofReal (2^(p-1)/(p-1))*(∫⁻ x, ENNReal.ofReal ((f x)^p) ∂μ) := by
    …