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

Localized one-dimensional maximal functions

This file records the source-proof localized maximal-function notation used in the one-dimensional measure estimate. The analytic weak-type proof is intentionally kept as a named statement boundary; later work should prove it using Mathlib's one-dimensional Vitali covering machinery.

noncomputable def AleksandrovDifferentiability.openIntervalMeasureAverage (μ : MeasureTheory.Measure ℝ) (a b : ℝ) : ℝ

Average mass of a measure over the open interval (a,b), using the Euclidean length b-a. The source only uses this when a < b.

Equations

• AleksandrovDifferentiability.openIntervalMeasureAverage μ a b = μ.real (Set.Ioo a b) / (b - a)

theorem AleksandrovDifferentiability.tendsto_measureReal_iUnion_atTop {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : ℕ → Set α} (hm : Monotone s) (hfin : μ (⋃ (n : ℕ), s n) < ⊤) : Filter.Tendsto (fun (n : ℕ) => μ.real (s n)) Filter.atTop (nhds (μ.real (⋃ (n : ℕ), s n)))

Real-valued continuity from below for an increasing sequence of sets with finite union mass.

theorem AleksandrovDifferentiability.tendsto_measureReal_Ioo_of_iUnion_eq {μ : MeasureTheory.Measure ℝ} {a b : ℝ} {q r : ℕ → ℝ} (hmono : Monotone fun (n : ℕ) => Set.Ioo (q n) (r n)) (hUnion : ⋃ (n : ℕ), Set.Ioo (q n) (r n) = Set.Ioo a b) (hfin : μ (Set.Ioo a b) < ⊤) : Filter.Tendsto (fun (n : ℕ) => μ.real (Set.Ioo (q n) (r n))) Filter.atTop (nhds (μ.real (Set.Ioo a b)))

If a monotone sequence of open intervals exhausts (a,b) and the limiting interval has finite mass, then the real masses converge to the limiting real mass.

theorem AleksandrovDifferentiability.monotone_Ioo_of_antitone_left_monotone_right {q r : ℕ → ℝ} (hq : Antitone q) (hr : Monotone r) : Monotone fun (n : ℕ) => Set.Ioo (q n) (r n)

Open intervals are monotone under decreasing left endpoints and increasing right endpoints.

theorem AleksandrovDifferentiability.iUnion_Ioo_eq_Ioo_of_forall_mem_tendsto {a b : ℝ} {q r : ℕ → ℝ} (hqmem : ∀ (n : ℕ), a < q n) (hrmem : ∀ (n : ℕ), r n < b) (hq : Filter.Tendsto q Filter.atTop (nhds a)) (hr : Filter.Tendsto r Filter.atTop (nhds b)) : ⋃ (n : ℕ), Set.Ioo (q n) (r n) = Set.Ioo a b

Inner open intervals whose endpoints tend to the endpoints of (a,b) exhaust (a,b).

theorem AleksandrovDifferentiability.tendsto_measureReal_Ioo_of_antitone_left_monotone_right_tendsto {μ : MeasureTheory.Measure ℝ} {a b : ℝ} {q r : ℕ → ℝ} (hqmem : ∀ (n : ℕ), a < q n) (hrmem : ∀ (n : ℕ), r n < b) (hqanti : Antitone q) (hrmono : Monotone r) (hqtend : Filter.Tendsto q Filter.atTop (nhds a)) (hrtend : Filter.Tendsto r Filter.atTop (nhds b)) (hfin : μ (Set.Ioo a b) < ⊤) : Filter.Tendsto (fun (n : ℕ) => μ.real (Set.Ioo (q n) (r n))) Filter.atTop (nhds (μ.real (Set.Ioo a b)))

Mass convergence for nested inner intervals whose endpoints tend to the limiting endpoints.

theorem AleksandrovDifferentiability.exists_rat_strictAnti_tendsto_within {a s : ℝ} (has : a < s) : ∃ (q : ℕ → ℚ), StrictAnti q ∧ (∀ (n : ℕ), a < ↑(q n) ∧ ↑(q n) < s) ∧ Filter.Tendsto (fun (n : ℕ) => ↑(q n)) Filter.atTop (nhds a)

Rational points decreasing to the left endpoint from inside a prescribed interval.

theorem AleksandrovDifferentiability.exists_rat_strictMono_tendsto_within {s b : ℝ} (hsb : s < b) : ∃ (r : ℕ → ℚ), StrictMono r ∧ (∀ (n : ℕ), s < ↑(r n) ∧ ↑(r n) < b) ∧ Filter.Tendsto (fun (n : ℕ) => ↑(r n)) Filter.atTop (nhds b)

Rational points increasing to the right endpoint from inside a prescribed interval.

theorem AleksandrovDifferentiability.exists_rat_inner_tendsto_measureReal_Ioo {μ : MeasureTheory.Measure ℝ} {a s b : ℝ} (has : a < s) (hsb : s < b) (hfin : μ (Set.Ioo a b) < ⊤) : ∃ (q : ℕ → ℚ) (r : ℕ → ℚ), (∀ (n : ℕ), a < ↑(q n) ∧ ↑(q n) < s ∧ s < ↑(r n) ∧ ↑(r n) < b) ∧ Filter.Tendsto (fun (n : ℕ) => ↑(q n)) Filter.atTop (nhds a) ∧ Filter.Tendsto (fun (n : ℕ) => ↑(r n)) Filter.atTop (nhds b) ∧ Filter.Tendsto (fun (n : ℕ) => μ.real (Set.Ioo ↑(q n) ↑(r n))) Filter.atTop (nhds (μ.real (Set.Ioo a b)))

Generic rational inner-interval mass approximation by continuity from below.

theorem AleksandrovDifferentiability.tendsto_openIntervalMeasureAverage_of_tendsto_measureReal {μ : MeasureTheory.Measure ℝ} {a b : ℝ} {q r : ℕ → ℝ} (hmass : Filter.Tendsto (fun (n : ℕ) => μ.real (Set.Ioo (q n) (r n))) Filter.atTop (nhds (μ.real (Set.Ioo a b)))) (hq : Filter.Tendsto q Filter.atTop (nhds a)) (hr : Filter.Tendsto r Filter.atTop (nhds b)) (hab : a < b) : Filter.Tendsto (fun (n : ℕ) => openIntervalMeasureAverage μ (q n) (r n)) Filter.atTop (nhds (openIntervalMeasureAverage μ a b))

Interval averages converge if the numerator masses converge and the endpoint lengths converge to a nonzero length.

theorem AleksandrovDifferentiability.tendsto_openIntervalMeasureAverage_of_tendsto_measureReal_rat {μ : MeasureTheory.Measure ℝ} {a b : ℝ} {q r : ℕ → ℚ} (hmass : Filter.Tendsto (fun (n : ℕ) => μ.real (Set.Ioo ↑(q n) ↑(r n))) Filter.atTop (nhds (μ.real (Set.Ioo a b)))) (hq : Filter.Tendsto (fun (n : ℕ) => ↑(q n)) Filter.atTop (nhds a)) (hr : Filter.Tendsto (fun (n : ℕ) => ↑(r n)) Filter.atTop (nhds b)) (hab : a < b) : Filter.Tendsto (fun (n : ℕ) => openIntervalMeasureAverage μ ↑(q n) ↑(r n)) Filter.atTop (nhds (openIntervalMeasureAverage μ a b))

Rational endpoint version of tendsto_openIntervalMeasureAverage_of_tendsto_measureReal.

def AleksandrovDifferentiability.localizedIntervalAverageSet (μ : MeasureTheory.Measure ℝ) (domain : Set ℝ) (s : ℝ) : Set ℝ

The set of interval averages used in the localized maximal function. Naming this set keeps later endpoint-control lemmas from repeatedly unfolding the sSup expression.

Equations

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

noncomputable def AleksandrovDifferentiability.localizedMaximalFunction (μ : MeasureTheory.Measure ℝ) (domain : Set ℝ) (s : ℝ) : ℝ

Localized one-dimensional Hardy-Littlewood maximal function over open intervals contained in domain.

This matches the source expression sup { μ(I) / |I| : I ⊂ domain open interval, s ∈ I }, written with endpoints a < b.

Equations

• AleksandrovDifferentiability.localizedMaximalFunction μ domain s = sSup (AleksandrovDifferentiability.localizedIntervalAverageSet μ domain s)

def AleksandrovDifferentiability.localizedMaximalBadPredicate (μ : MeasureTheory.Measure ℝ) (domain : Set ℝ) (s t : ℝ) : Prop

Pointwise localized maximal bad predicate.

The first disjunct records the extended-valued case: if the interval averages through s are unbounded, the maximal function is effectively infinite and s is bad for every finite threshold.

Equations

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

def AleksandrovDifferentiability.localizedMaximalBadSet (μ : MeasureTheory.Measure ℝ) (domain window : Set ℝ) (t : ℝ) : Set ℝ

Bad set for a localized one-dimensional maximal function, restricted to a window.

Equations

• AleksandrovDifferentiability.localizedMaximalBadSet μ domain window t = {s : ℝ | s ∈ window ∧ AleksandrovDifferentiability.localizedMaximalBadPredicate μ domain s t}

def AleksandrovDifferentiability.sourceMaximalDomain : Set ℝ

Source domain (-2,2) for the localized maximal estimate.

Equations

• AleksandrovDifferentiability.sourceMaximalDomain = Set.Ioo (-2) 2

def AleksandrovDifferentiability.sourceMaximalWindow : Set ℝ

Source conclusion window (-1,1) for the localized maximal estimate.

Equations

• AleksandrovDifferentiability.sourceMaximalWindow = Set.Ioo (-1) 1

def AleksandrovDifferentiability.sourceLocalizedMaximalBadSet (μ : MeasureTheory.Measure ℝ) (t : ℝ) : Set ℝ

Source localized maximal bad set {s ∈ (-1,1) : M μ(s) > t}.

Equations

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

def AleksandrovDifferentiability.sourceLocalizedMaximalBadPredicate (μ : MeasureTheory.Measure ℝ) (s t : ℝ) : Prop

Pointwise source localized maximal bad predicate, without the (-1,1) window restriction. The cube bad sets already impose x ∈ Q_1, so they use this predicate form.

Equations

• AleksandrovDifferentiability.sourceLocalizedMaximalBadPredicate μ s t = AleksandrovDifferentiability.localizedMaximalBadPredicate μ AleksandrovDifferentiability.sourceMaximalDomain s t

def AleksandrovDifferentiability.SourceLocalizedMaximalBadPredicateMeasurable {α : Type u_1} [MeasurableSpace α] (μparam : α → MeasureTheory.Measure ℝ) (t : ℝ) : Prop

Product-coordinate measurability of a parameterized source-local maximal bad predicate.

Here μparam a is the one-dimensional measure attached to parameter a, and the product coordinate is (a,s). This is the natural measurability target for sliced Fubini arguments.

Equations

• AleksandrovDifferentiability.SourceLocalizedMaximalBadPredicateMeasurable μparam t = MeasurableSet {p : α × ℝ | AleksandrovDifferentiability.sourceLocalizedMaximalBadPredicate (μparam p.1) p.2 t}

def AleksandrovDifferentiability.SourceLocalizedMaximalBadPredicateMeasurableOnWindow {α : Type u_1} [MeasurableSpace α] (μparam : α → MeasureTheory.Measure ℝ) (t : ℝ) : Prop

Source-window-restricted product-coordinate measurability of a parameterized source-local maximal bad predicate. This is the exact form needed by the source cube proof, where the coordinate parameter is already known to lie in (-1,1).

Equations

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

def AleksandrovDifferentiability.sourceLocalizedMaximalAverageExceedsSet {α : Type u_1} (μparam : α → MeasureTheory.Measure ℝ) (t : ℝ) : Set (α × ℝ)

Source-window interval-average existence set for a parameterized one-dimensional measure family.

Equations

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

def AleksandrovDifferentiability.sourceLocalizedMaximalAverageExceedsFixedIntervalSet {α : Type u_1} (μparam : α → MeasureTheory.Measure ℝ) (a b t : ℝ) : Set (α × ℝ)

Fixed-interval piece of the source-window interval-average existence set.

Equations

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

def AleksandrovDifferentiability.sourceLocalizedMaximalAverageExceedsCountableIntervalSet {α : Type u_1} (μparam : α → MeasureTheory.Measure ℝ) (a b : ℕ → ℝ) (t : ℝ) : Set (α × ℝ)

Countable fixed-interval model for the source-window interval-average existence set. Later Stieltjes work should instantiate this with a rational interval family and prove that it agrees with sourceLocalizedMaximalAverageExceedsSet.

Equations

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

def AleksandrovDifferentiability.SourceAdmissibleIntervalEnumeration (a b : ℕ → ℝ) : Prop

An enumerated interval family is admissible for the source-local maximal construction if each interval is nondegenerate and contained in the source maximal domain.

Equations

• AleksandrovDifferentiability.SourceAdmissibleIntervalEnumeration a b = ∀ (k : ℕ), a k < b k ∧ Set.Ioo (a k) (b k) ⊆ AleksandrovDifferentiability.sourceMaximalDomain

def AleksandrovDifferentiability.SourceRationalIntervalEnumeration (a b : ℕ → ℝ) : Prop

An enumerated interval family contains every rational source-admissible interval. This is the countability part of the source-local maximal measurability reduction; the analytic approximation step is kept separate below.

Equations

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

def AleksandrovDifferentiability.SourceRationalAdmissibleInterval : Type

The type of rational source-admissible intervals. This is the countable subtype whose surjective enumeration supplies SourceRationalIntervalEnumeration.

Equations

• AleksandrovDifferentiability.SourceRationalAdmissibleInterval = { p : ℚ × ℚ // ↑p.1 < ↑p.2 ∧ Set.Ioo ↑p.1 ↑p.2 ⊆ AleksandrovDifferentiability.sourceMaximalDomain }

theorem AleksandrovDifferentiability.nonempty_sourceRationalAdmissibleInterval : Nonempty SourceRationalAdmissibleInterval

The source rational-admissible interval type is nonempty, for instance by (-1,1).

theorem AleksandrovDifferentiability.exists_sourceRationalIntervalEnumeration : ∃ (a : ℕ → ℝ) (b : ℕ → ℝ), SourceRationalIntervalEnumeration a b

There exists a sequence of real endpoints enumerating every rational source-admissible interval and only source-admissible intervals.

theorem AleksandrovDifferentiability.SourceRationalIntervalEnumeration.admissible {a b : ℕ → ℝ} (henum : SourceRationalIntervalEnumeration a b) : SourceAdmissibleIntervalEnumeration a b

The admissibility part of a rational source interval enumeration.

theorem AleksandrovDifferentiability.SourceRationalIntervalEnumeration.exists_index {a b : ℕ → ℝ} (henum : SourceRationalIntervalEnumeration a b) {q r : ℚ} (hqr : ↑q < ↑r) (hsub : Set.Ioo ↑q ↑r ⊆ sourceMaximalDomain) : ∃ (k : ℕ), a k = ↑q ∧ b k = ↑r

A rational source interval enumeration contains any rational admissible interval.

theorem AleksandrovDifferentiability.rat_Ioo_subset_sourceMaximalDomain_of_subset {a b : ℝ} {q r : ℚ} (hsub : Set.Ioo a b ⊆ sourceMaximalDomain) (haq : a < ↑q) (hrb : ↑r < b) : Set.Ioo ↑q ↑r ⊆ sourceMaximalDomain

A rational subinterval of a source-admissible real interval is source-admissible.

theorem AleksandrovDifferentiability.exists_rat_sourceInterval_subset_of_mem {a b s : ℝ} (hsub : Set.Ioo a b ⊆ sourceMaximalDomain) (hs : s ∈ Set.Ioo a b) : ∃ (q : ℚ) (r : ℚ), a < ↑q ∧ ↑q < s ∧ s < ↑r ∧ ↑r < b ∧ ↑q < ↑r ∧ Set.Ioo ↑q ↑r ⊆ sourceMaximalDomain

Pure geometry: every source-admissible real interval through s contains a rational source-admissible subinterval through s.

def AleksandrovDifferentiability.SourceLocalizedMaximalAverageExceedsCountableIntervalReverseCover {α : Type u_1} (μparam : α → MeasureTheory.Measure ℝ) (a b : ℕ → ℝ) (t : ℝ) : Prop

Reverse cover obligation for a countable interval model of the source average-exceeds set.

This is the analytic density/approximation direction: every real admissible interval with average strictly above the threshold must be replaceable by one of the enumerated intervals.

Equations

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

def AleksandrovDifferentiability.SourceLocalizedMaximalAverageExceedsRationalRefinement {α : Type u_1} (μparam : α → MeasureTheory.Measure ℝ) (t : ℝ) : Prop

Rational refinement of the source average-exceeds set: every point witnessed by some real admissible interval has a rational source-admissible interval witness with the same strict average inequality.

Equations

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

def AleksandrovDifferentiability.SourceRealIntervalAverageExceedsRationalRefinement {α : Type u_1} (μparam : α → MeasureTheory.Measure ℝ) (t : ℝ) : Prop

Real-interval form of the rational refinement obligation. This is the form closest to the source proof: start from one admissible real interval with average above the threshold and shrink/perturb to a rational admissible interval preserving the strict inequality.

Equations

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

def AleksandrovDifferentiability.SourceRealIntervalAverageExceedsInnerRationalRefinement {α : Type u_1} (μparam : α → MeasureTheory.Measure ℝ) (t : ℝ) : Prop

Inner-rational refinement form of the average-exceeds obligation. This is the exact source-continuity step: the rational witness is a subinterval of the original real witness and still contains the base point.

Equations

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

def AleksandrovDifferentiability.SourceRealIntervalAverageExceedsInnerRationalTendsto {α : Type u_1} (μparam : α → MeasureTheory.Measure ℝ) (t : ℝ) : Prop

Sequential inner-rational average approximation. This is the continuity-from-below form which should be proved for the Stieltjes slice measures: choose rational inner intervals through p.2 whose averages converge to the original interval average.

Equations

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

def AleksandrovDifferentiability.SourceRealIntervalAverageExceedsInnerRationalMassTendsto {α : Type u_1} (μparam : α → MeasureTheory.Measure ℝ) (t : ℝ) : Prop

Sequential inner-rational mass approximation. This is the measure-continuity part of the source-local rational refinement: rational inner intervals through p.2 have masses converging to the original interval mass.

Equations

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

theorem AleksandrovDifferentiability.SourceRealIntervalAverageExceedsInnerRationalMassTendsto.of_finiteOnAdmissibleIntervals {α : Type u_1} {μparam : α → MeasureTheory.Measure ℝ} {t : ℝ} (hfinite : ∀ (x : α) {a b : ℝ}, a < b → Set.Ioo a b ⊆ sourceMaximalDomain → (μparam x) (Set.Ioo a b) < ⊤) : SourceRealIntervalAverageExceedsInnerRationalMassTendsto μparam t

Finite mass on every source-admissible real interval gives the sequential inner-rational mass approximation target.

theorem AleksandrovDifferentiability.SourceRealIntervalAverageExceedsInnerRationalTendsto.of_massTendsto {α : Type u_1} {μparam : α → MeasureTheory.Measure ℝ} {t : ℝ} (hmassApprox : SourceRealIntervalAverageExceedsInnerRationalMassTendsto μparam t) : SourceRealIntervalAverageExceedsInnerRationalTendsto μparam t

Mass convergence along rational inner intervals gives average convergence along those intervals.

theorem AleksandrovDifferentiability.SourceRealIntervalAverageExceedsInnerRationalRefinement.of_tendsto {α : Type u_1} {μparam : α → MeasureTheory.Measure ℝ} {t : ℝ} (happrox : SourceRealIntervalAverageExceedsInnerRationalTendsto μparam t) : SourceRealIntervalAverageExceedsInnerRationalRefinement μparam t

Sequential inner-rational approximation gives the existential inner-rational refinement because the original average inequality is strict.

theorem AleksandrovDifferentiability.SourceRealIntervalAverageExceedsRationalRefinement.of_inner {α : Type u_1} {μparam : α → MeasureTheory.Measure ℝ} {t : ℝ} (hrefine : SourceRealIntervalAverageExceedsInnerRationalRefinement μparam t) : SourceRealIntervalAverageExceedsRationalRefinement μparam t

The inner-rational refinement form gives the real-interval rational refinement form.

theorem AleksandrovDifferentiability.SourceLocalizedMaximalAverageExceedsRationalRefinement.of_realInterval {α : Type u_1} {μparam : α → MeasureTheory.Measure ℝ} {t : ℝ} (hrefine : SourceRealIntervalAverageExceedsRationalRefinement μparam t) : SourceLocalizedMaximalAverageExceedsRationalRefinement μparam t

The real-interval refinement form gives the set-level rational refinement form.

theorem AleksandrovDifferentiability.SourceLocalizedMaximalAverageExceedsCountableIntervalReverseCover.of_rationalRefinement {α : Type u_1} {μparam : α → MeasureTheory.Measure ℝ} {a b : ℕ → ℝ} {t : ℝ} (henum : SourceRationalIntervalEnumeration a b) (hrefine : SourceLocalizedMaximalAverageExceedsRationalRefinement μparam t) : SourceLocalizedMaximalAverageExceedsCountableIntervalReverseCover μparam a b t

A rational interval enumeration converts rational average refinement into the reverse-cover direction needed for countable fixed-interval measurability.

theorem AleksandrovDifferentiability.sourceLocalizedMaximalAverageExceedsCountableIntervalSet_subset {α : Type u_1} {μparam : α → MeasureTheory.Measure ℝ} {a b : ℕ → ℝ} {t : ℝ} (hadm : SourceAdmissibleIntervalEnumeration a b) : sourceLocalizedMaximalAverageExceedsCountableIntervalSet μparam a b t ⊆ sourceLocalizedMaximalAverageExceedsSet μparam t

The countable interval model is contained in the real-existential average-exceeds set as soon as every enumerated interval is source-admissible.

theorem AleksandrovDifferentiability.sourceLocalizedMaximalAverageExceedsCountableIntervalCover_of_reverseCover {α : Type u_1} {μparam : α → MeasureTheory.Measure ℝ} {a b : ℕ → ℝ} {t : ℝ} (hadm : SourceAdmissibleIntervalEnumeration a b) (hreverse : SourceLocalizedMaximalAverageExceedsCountableIntervalReverseCover μparam a b t) : sourceLocalizedMaximalAverageExceedsSet μparam t = sourceLocalizedMaximalAverageExceedsCountableIntervalSet μparam a b t

An admissible countable interval family represents the source average-exceeds set once the analytic reverse-cover direction has been proved.

def AleksandrovDifferentiability.SourceLocalizedMaximalAverageExceedsMeasurable {α : Type u_1} [MeasurableSpace α] (μparam : α → MeasureTheory.Measure ℝ) (t : ℝ) : Prop

Source-window interval-average existence measurability for a parameterized one-dimensional measure family.

Equations

• AleksandrovDifferentiability.SourceLocalizedMaximalAverageExceedsMeasurable μparam t = MeasurableSet (AleksandrovDifferentiability.sourceLocalizedMaximalAverageExceedsSet μparam t)

def AleksandrovDifferentiability.SourceLocalizedMaximalAverageExceedsCountableIntervalFamilyMeasurable {α : Type u_1} [MeasurableSpace α] (μparam : α → MeasureTheory.Measure ℝ) (a b : ℕ → ℝ) (t : ℝ) : Prop

Measurability of every fixed-interval piece in a countable interval model.

Equations

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

theorem AleksandrovDifferentiability.measurableSet_sourceLocalizedMaximalAverageExceedsFixedIntervalSet {α : Type u_1} [MeasurableSpace α] {μparam : α → MeasureTheory.Measure ℝ} {a b t : ℝ} (havg : Measurable fun (y : α) => openIntervalMeasureAverage (μparam y) a b) : MeasurableSet (sourceLocalizedMaximalAverageExceedsFixedIntervalSet μparam a b t)

A fixed-interval source-window average-exceeds piece is measurable if the corresponding fixed-interval average is measurable in the parameter.

theorem AleksandrovDifferentiability.SourceLocalizedMaximalAverageExceedsCountableIntervalFamilyMeasurable.of_measurableAverage {α : Type u_1} [MeasurableSpace α] {μparam : α → MeasureTheory.Measure ℝ} {a b : ℕ → ℝ} {t : ℝ} (havg : ∀ (k : ℕ), Measurable fun (y : α) => openIntervalMeasureAverage (μparam y) (a k) (b k)) : SourceLocalizedMaximalAverageExceedsCountableIntervalFamilyMeasurable μparam a b t

A countable family of fixed intervals is measurable if each fixed-interval average is measurable in the parameter.

theorem AleksandrovDifferentiability.SourceLocalizedMaximalAverageExceedsMeasurable.of_countableIntervalFamily {α : Type u_1} [MeasurableSpace α] {μparam : α → MeasureTheory.Measure ℝ} {a b : ℕ → ℝ} {t : ℝ} (hfixed : SourceLocalizedMaximalAverageExceedsCountableIntervalFamilyMeasurable μparam a b t) (hcover : sourceLocalizedMaximalAverageExceedsSet μparam t = sourceLocalizedMaximalAverageExceedsCountableIntervalSet μparam a b t) : SourceLocalizedMaximalAverageExceedsMeasurable μparam t

If the source-window interval-average existence set is represented by a countable fixed interval family, then measurability of the fixed-interval pieces gives measurability of the full source-window interval-average existence set.

@[simp]

theorem AleksandrovDifferentiability.mem_localizedMaximalBadSet {μ : MeasureTheory.Measure ℝ} {domain window : Set ℝ} {t s : ℝ} : s ∈ localizedMaximalBadSet μ domain window t ↔ s ∈ window ∧ localizedMaximalBadPredicate μ domain s t

@[simp]

theorem AleksandrovDifferentiability.mem_sourceLocalizedMaximalBadSet {μ : MeasureTheory.Measure ℝ} {t s : ℝ} : s ∈ sourceLocalizedMaximalBadSet μ t ↔ s ∈ sourceMaximalWindow ∧ sourceLocalizedMaximalBadPredicate μ s t

theorem AleksandrovDifferentiability.localizedMaximalFunction_eq_sSup_intervalAverageSet (μ : MeasureTheory.Measure ℝ) (domain : Set ℝ) (s : ℝ) : localizedMaximalFunction μ domain s = sSup (localizedIntervalAverageSet μ domain s)

theorem AleksandrovDifferentiability.localizedMaximalBadPredicate_iff_exists_average_gt {μ : MeasureTheory.Measure ℝ} {domain : Set ℝ} {s t : ℝ} (hne : (localizedIntervalAverageSet μ domain s).Nonempty) : localizedMaximalBadPredicate μ domain s t ↔ ∃ (a : ℝ) (b : ℝ), a < b ∧ Set.Ioo a b ⊆ domain ∧ s ∈ Set.Ioo a b ∧ t < openIntervalMeasureAverage μ a b

The localized maximal bad predicate is equivalent to the existence of one admissible interval through the point whose average is larger than the threshold. The explicit unbounded-average case in the definition is exactly what makes this equivalence valid without a boundedness hypothesis.

theorem AleksandrovDifferentiability.localizedIntervalAverageSet_source_nonempty_of_mem_window (μ : MeasureTheory.Measure ℝ) {s : ℝ} (hs : s ∈ sourceMaximalWindow) : (localizedIntervalAverageSet μ sourceMaximalDomain s).Nonempty

A source-window point has at least one admissible interval in the source maximal domain.

theorem AleksandrovDifferentiability.sourceLocalizedMaximalBadPredicate_iff_exists_average_gt_of_mem_window {μ : MeasureTheory.Measure ℝ} {s t : ℝ} (hs : s ∈ sourceMaximalWindow) : sourceLocalizedMaximalBadPredicate μ s t ↔ ∃ (a : ℝ) (b : ℝ), a < b ∧ Set.Ioo a b ⊆ sourceMaximalDomain ∧ s ∈ Set.Ioo a b ∧ t < openIntervalMeasureAverage μ a b

Source-window version of localizedMaximalBadPredicate_iff_exists_average_gt.