MaximalEstimates.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.DiskMaximalTools.volume_dilate_five line 24

theorem OAI.DiskMaximalTools.weak_bound_bounded_family line 31

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
…

lemma OAI.DiskMaximalTools.volume_disk_real line 65

theorem OAI.DiskMaximalTools.weak_bound line 73

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
…

def OAI.DiskMaximalTools.rationalMaximal line 97
Source documentation
A countable measurable envelope, sufficiently rich for every actual disk.
```
def rationalMaximal (ν : Measure ℂ) (x : ℂ) : ℝ≥0∞ :=
…
```
lemma OAI.DiskMaximalTools.measurable_ball_mass line 100
lemma OAI.DiskMaximalTools.measurable_rationalMaximal line 106
lemma OAI.DiskMaximalTools.weak_rationalMaximal line 118
lemma OAI.DiskMaximalTools.disk_average_le_rationalMaximal line 133

lemma OAI.DiskMaximalTools.weak_split line 164

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.DiskMaximalTools.rationalMaximal

lemma OAI.DiskMaximalTools.weak_truncated line 190
lemma OAI.DiskMaximalTools.lintegral_rpow_Ioo line 226
lemma OAI.DiskMaximalTools.truncation_layer_single line 239

theorem OAI.DiskMaximalTools.truncation_layer_integral line 270

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
…

lemma OAI.DiskMaximalTools.maximal_layer_coefficient line 300

theorem OAI.DiskMaximalTools.strong_rationalMaximal line 320

Source documentation

A full strong p estimate from Vitali, truncation and Tonelli. No maximal inequality is supplied as an assumption. The real representative is controlled even before a separate almost-everywhere finiteness argument.

theorem strong_rationalMaximal {f : ℂ → ℝ} (hf : Measurable f)
    (hf0 : ∀ x, 0 ≤ f x) [IsFiniteMeasure (volume.withDensity (fun x => ENNReal.ofReal (f x)))]
    {p : ℝ} (hp : 1 < p) :
    (∫⁻ x, ENNReal.ofReal ((rationalMaximal (volume.withDensity (fun x => ENNReal.ofReal (f x))) x).toReal^p)) ≤
      ENNReal.ofReal (50*p*2^(p-1)/(p-1)) * (∫⁻ x, ENNReal.ofReal ((f x)^p)) := by
…

Mentions: OAI.DiskMaximalTools.rationalMaximal

lemma OAI.DiskMaximalTools.disk_average_le_rationalMaximal_exact line 378
theorem OAI.DiskMaximalTools.all_radii_eq_rational line 423
Source documentation
Countability loses neither radii nor high values: the rational expression is exactly the centered disk maximal function of the measure.
```
theorem all_radii_eq_rational (ν : Measure ℂ) (x : ℂ) :
    (⨆ (r : ℝ) (_ : 0 < r), ν (ball x r)/volume (ball x r)) = rationalMaximal ν x := by
…
```
Mentions: OAI.DiskMaximalTools.rationalMaximal
lemma OAI.DiskMaximalTools.rationalMaximal_le_of_density_le line 439