Ported for Lean Pool: imports relocated and code adapted to Lean/Mathlib v4.34.0.

Localized maximal estimates

theorem AleksandrovDifferentiability.SourceLocalizedMaximalBadPredicateMeasurable.of_measurable_parts {α : Type u_1} [MeasurableSpace α] {μparam : α → MeasureTheory.Measure ℝ} {t : ℝ} (hunbdd : MeasurableSet {p : α × ℝ | ¬BddAbove (localizedIntervalAverageSet (μparam p.1) sourceMaximalDomain p.2)}) (hsuper : MeasurableSet {p : α × ℝ | t < localizedMaximalFunction (μparam p.1) sourceMaximalDomain p.2}) : SourceLocalizedMaximalBadPredicateMeasurable μparam t

theorem AleksandrovDifferentiability.SourceLocalizedMaximalBadPredicateMeasurableOnWindow.of_averageExceeds {α : Type u_1} [MeasurableSpace α] {μparam : α → MeasureTheory.Measure ℝ} {t : ℝ} (havg : SourceLocalizedMaximalAverageExceedsMeasurable μparam t) : SourceLocalizedMaximalBadPredicateMeasurableOnWindow μparam t

The source-window maximal bad predicate is measurable as soon as the equivalent interval-average-exceeds set is measurable.

theorem AleksandrovDifferentiability.bddAbove_of_not_localizedMaximalBadPredicate {μ : MeasureTheory.Measure ℝ} {domain : Set ℝ} {s t : ℝ} (hnot : ¬localizedMaximalBadPredicate μ domain s t) : BddAbove (localizedIntervalAverageSet μ domain s)

theorem AleksandrovDifferentiability.not_lt_localizedMaximalFunction_of_not_localizedMaximalBadPredicate {μ : MeasureTheory.Measure ℝ} {domain : Set ℝ} {s t : ℝ} (hnot : ¬localizedMaximalBadPredicate μ domain s t) : ¬t < localizedMaximalFunction μ domain s

theorem AleksandrovDifferentiability.bddAbove_of_not_sourceLocalizedMaximalBadPredicate {μ : MeasureTheory.Measure ℝ} {s t : ℝ} (hnot : ¬sourceLocalizedMaximalBadPredicate μ s t) : BddAbove (localizedIntervalAverageSet μ sourceMaximalDomain s)

theorem AleksandrovDifferentiability.not_lt_localizedMaximalFunction_of_not_sourceLocalizedMaximalBadPredicate {μ : MeasureTheory.Measure ℝ} {s t : ℝ} (hnot : ¬sourceLocalizedMaximalBadPredicate μ s t) : ¬t < localizedMaximalFunction μ sourceMaximalDomain s

theorem AleksandrovDifferentiability.openIntervalMeasureAverage_le_localizedMaximalFunction {μ : MeasureTheory.Measure ℝ} {domain : Set ℝ} {s a b : ℝ} (hbdd : BddAbove (localizedIntervalAverageSet μ domain s)) (hab : a < b) (hsub : Set.Ioo a b ⊆ domain) (hs : s ∈ Set.Ioo a b) : openIntervalMeasureAverage μ a b ≤ localizedMaximalFunction μ domain s

Every admissible interval average is bounded by the localized maximal function, provided the defining set of averages is bounded above. The boundedness hypothesis is intentionally explicit: for measures with atoms these averages need not be bounded a priori.

theorem AleksandrovDifferentiability.openIntervalMeasureAverage_le_of_not_localizedMaximalBadPredicate {μ : MeasureTheory.Measure ℝ} {domain : Set ℝ} {s t a b : ℝ} (hnot : ¬localizedMaximalBadPredicate μ domain s t) (hab : a < b) (hsub : Set.Ioo a b ⊆ domain) (hs : s ∈ Set.Ioo a b) : openIntervalMeasureAverage μ a b ≤ t

A point outside the localized maximal bad predicate controls every admissible interval average through that point.

theorem AleksandrovDifferentiability.openIntervalMeasureAverage_le_of_not_sourceLocalizedMaximalBadPredicate {μ : MeasureTheory.Measure ℝ} {s t a b : ℝ} (hnot : ¬sourceLocalizedMaximalBadPredicate μ s t) (hab : a < b) (hsub : Set.Ioo a b ⊆ sourceMaximalDomain) (hs : s ∈ Set.Ioo a b) : openIntervalMeasureAverage μ a b ≤ t

Source-local version of openIntervalMeasureAverage_le_of_not_localizedMaximalBadPredicate.

theorem AleksandrovDifferentiability.measureReal_Ioo_le_mul_of_not_sourceLocalizedMaximalBadPredicate {μ : MeasureTheory.Measure ℝ} {s t a b : ℝ} (hnot : ¬sourceLocalizedMaximalBadPredicate μ s t) (hab : a < b) (hsub : Set.Ioo a b ⊆ sourceMaximalDomain) (hs : s ∈ Set.Ioo a b) : μ.real (Set.Ioo a b) ≤ t * (b - a)

A source non-bad point controls the real measure of every admissible interval through it. This is the interval-mass estimate used in the one-dimensional endpoint-control proof.

theorem AleksandrovDifferentiability.sourceMaximalWindow_Ioo_symm_subset_sourceMaximalDomain {x h : ℝ} (hx : x ∈ sourceMaximalWindow) (hh : h < 1) : Set.Ioo (x - h) (x + h) ⊆ sourceMaximalDomain

A short symmetric interval around a source-window point stays inside the source maximal domain.

theorem AleksandrovDifferentiability.measureReal_Ioo_symm_le_two_mul_of_not_sourceLocalizedMaximalBadPredicate {μ : MeasureTheory.Measure ℝ} {x t h : ℝ} (hnot : ¬sourceLocalizedMaximalBadPredicate μ x t) (hx : x ∈ sourceMaximalWindow) (hh_pos : 0 < h) (hh : h < 1) : μ.real (Set.Ioo (x - h) (x + h)) ≤ t * (2 * h)

Symmetric interval-mass bound at a source non-bad point.

def AleksandrovDifferentiability.LocalizedMaximalEstimateStatement (C : ℝ) : Prop

Source weak-type localized maximal estimate, packaged as a theorem boundary.

The source proves this with the one-dimensional Vitali covering lemma. The hypothesis μ sourceMaximalDomain < ⊤ records that the localized measure has finite mass on (-2,2).

Equations

• One or more equations did not get rendered due to their size.

def AleksandrovDifferentiability.ExistsLocalizedMaximalEstimateStatement : Prop

Existential form of the source weak-type localized maximal estimate. This is the theorem boundary corresponding to the one-dimensional Vitali covering argument in the source proof.

Equations

• AleksandrovDifferentiability.ExistsLocalizedMaximalEstimateStatement = ∃ (C : ℝ), AleksandrovDifferentiability.LocalizedMaximalEstimateStatement C

theorem AleksandrovDifferentiability.localizedMaximalEstimateStatement_four : LocalizedMaximalEstimateStatement 4

The source localized maximal weak-type estimate, proved by the one-dimensional Vitali covering argument above. The explicit constant 4 comes from taking enlargement factor τ = 4 > 3.

theorem AleksandrovDifferentiability.existsLocalizedMaximalEstimateStatement : ExistsLocalizedMaximalEstimateStatement

Existential source localized maximal weak-type estimate.

theorem AleksandrovDifferentiability.LocalizedMaximalEstimateStatement.sourceBadSet_measure_le_of_mass_bound {C M osc : ℝ} (hmax : LocalizedMaximalEstimateStatement C) {μ : MeasureTheory.Measure ℝ} {t : ℝ} (ht : 0 < t) (hfinite : μ sourceMaximalDomain < ⊤) (hmass : μ.real sourceMaximalDomain ≤ M * osc) : MeasureTheory.volume (sourceLocalizedMaximalBadSet μ t) ≤ ENNReal.ofReal (C * M * osc / t)

Consequence of the localized maximal estimate after replacing the source interval mass by an external mass bound. This is the algebraic step used after the one-dimensional convex second-derivative mass estimate.

theorem AleksandrovDifferentiability.LocalizedMaximalEstimateStatement.sourceBadSet_measure_le_of_two_mul_osc {C osc : ℝ} (hmax : LocalizedMaximalEstimateStatement C) {μ : MeasureTheory.Measure ℝ} {t : ℝ} (ht : 0 < t) (hfinite : μ sourceMaximalDomain < ⊤) (hmass : μ.real sourceMaximalDomain ≤ 2 * osc) : MeasureTheory.volume (sourceLocalizedMaximalBadSet μ t) ≤ ENNReal.ofReal (2 * C * osc / t)

Source-form consequence with the one-dimensional convex mass bound μ((-2,2)) <= 2 * osc.