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

Localized maximal witness intervals

def AleksandrovDifferentiability.SourceMaximalWitnessInterval (μ : MeasureTheory.Measure ℝ) (t : ℝ) : Type

An open interval in the source domain whose measure average exceeds the threshold.

Equations

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

def AleksandrovDifferentiability.SourceMaximalWitnessInterval.left {μ : MeasureTheory.Measure ℝ} {t : ℝ} (I : SourceMaximalWitnessInterval μ t) : ℝ

Left endpoint of a source maximal witness interval.

Equations

• I.left = (↑I).1

def AleksandrovDifferentiability.SourceMaximalWitnessInterval.right {μ : MeasureTheory.Measure ℝ} {t : ℝ} (I : SourceMaximalWitnessInterval μ t) : ℝ

Right endpoint of a source maximal witness interval.

Equations

• I.right = (↑I).2

def AleksandrovDifferentiability.SourceMaximalWitnessInterval.interval {μ : MeasureTheory.Measure ℝ} {t : ℝ} (I : SourceMaximalWitnessInterval μ t) : Set ℝ

Underlying open interval of a source maximal witness.

Equations

• I.interval = Set.Ioo I.left I.right

noncomputable def AleksandrovDifferentiability.SourceMaximalWitnessInterval.center {μ : MeasureTheory.Measure ℝ} {t : ℝ} (I : SourceMaximalWitnessInterval μ t) : ℝ

Center of the witness interval, for the ball formulation of the covering lemma.

Equations

• I.center = (I.left + I.right) / 2

noncomputable def AleksandrovDifferentiability.SourceMaximalWitnessInterval.radius {μ : MeasureTheory.Measure ℝ} {t : ℝ} (I : SourceMaximalWitnessInterval μ t) : ℝ

Radius of the witness interval, for the ball formulation of the covering lemma.

Equations

• I.radius = (I.right - I.left) / 2

theorem AleksandrovDifferentiability.SourceMaximalWitnessInterval.left_lt_right {μ : MeasureTheory.Measure ℝ} {t : ℝ} (I : SourceMaximalWitnessInterval μ t) : I.left < I.right

theorem AleksandrovDifferentiability.SourceMaximalWitnessInterval.interval_subset_sourceMaximalDomain {μ : MeasureTheory.Measure ℝ} {t : ℝ} (I : SourceMaximalWitnessInterval μ t) : I.interval ⊆ sourceMaximalDomain

theorem AleksandrovDifferentiability.SourceMaximalWitnessInterval.average_gt {μ : MeasureTheory.Measure ℝ} {t : ℝ} (I : SourceMaximalWitnessInterval μ t) : t < openIntervalMeasureAverage μ I.left I.right

theorem AleksandrovDifferentiability.SourceMaximalWitnessInterval.radius_pos {μ : MeasureTheory.Measure ℝ} {t : ℝ} (I : SourceMaximalWitnessInterval μ t) : 0 < I.radius

theorem AleksandrovDifferentiability.SourceMaximalWitnessInterval.interval_eq_ball {μ : MeasureTheory.Measure ℝ} {t : ℝ} (I : SourceMaximalWitnessInterval μ t) : I.interval = Metric.ball I.center I.radius

theorem AleksandrovDifferentiability.SourceMaximalWitnessInterval.left_ge_neg_two_of_Ioo_subset_sourceMaximalDomain {a b : ℝ} (hab : a < b) (hsub : Set.Ioo a b ⊆ sourceMaximalDomain) : -2 ≤ a

The left endpoint of any source-admissible open interval is at least -2.

theorem AleksandrovDifferentiability.SourceMaximalWitnessInterval.right_le_two_of_Ioo_subset_sourceMaximalDomain {a b : ℝ} (hab : a < b) (hsub : Set.Ioo a b ⊆ sourceMaximalDomain) : b ≤ 2

The right endpoint of any source-admissible open interval is at most 2.

theorem AleksandrovDifferentiability.SourceMaximalWitnessInterval.left_ge_neg_two {μ : MeasureTheory.Measure ℝ} {t : ℝ} (I : SourceMaximalWitnessInterval μ t) : -2 ≤ I.left

theorem AleksandrovDifferentiability.SourceMaximalWitnessInterval.right_le_two {μ : MeasureTheory.Measure ℝ} {t : ℝ} (I : SourceMaximalWitnessInterval μ t) : I.right ≤ 2

theorem AleksandrovDifferentiability.SourceMaximalWitnessInterval.radius_le_two {μ : MeasureTheory.Measure ℝ} {t : ℝ} (I : SourceMaximalWitnessInterval μ t) : I.radius ≤ 2

Witness intervals have radius at most 2, since they are contained in (-2,2).

theorem AleksandrovDifferentiability.SourceMaximalWitnessInterval.length_eq_two_mul_radius {μ : MeasureTheory.Measure ℝ} {t : ℝ} (I : SourceMaximalWitnessInterval μ t) : I.right - I.left = 2 * I.radius

The Euclidean length of a witness interval is twice its radius.

theorem AleksandrovDifferentiability.SourceMaximalWitnessInterval.t_mul_length_lt_measureReal_interval {μ : MeasureTheory.Measure ℝ} {t : ℝ} (I : SourceMaximalWitnessInterval μ t) : t * (I.right - I.left) < μ.real I.interval

The witness average inequality, rewritten as a mass lower bound.

theorem AleksandrovDifferentiability.SourceMaximalWitnessInterval.t_mul_two_mul_radius_lt_measureReal_interval {μ : MeasureTheory.Measure ℝ} {t : ℝ} (I : SourceMaximalWitnessInterval μ t) : t * (2 * I.radius) < μ.real I.interval

The witness average inequality, in radius form.

theorem AleksandrovDifferentiability.SourceMaximalWitnessInterval.volume_enlargedBall_le_of_average {μ : MeasureTheory.Measure ℝ} {t : ℝ} (I : SourceMaximalWitnessInterval μ t) {τ : ℝ} (ht : 0 < t) (hτ : 0 ≤ τ) : MeasureTheory.volume (Metric.ball I.center (τ * I.radius)) ≤ ENNReal.ofReal (τ / t * μ.real I.interval)

Pointwise bound for the Lebesgue measure of an enlarged witness ball.

This is the quantitative step in the source Vitali argument: the average bound t < μ(I) / |I| implies |B(c, τ r)| <= (τ / t) μ(I).

theorem AleksandrovDifferentiability.SourceMaximalWitnessInterval.volume_enlargedBall_le_mul_measure_interval {μ : MeasureTheory.Measure ℝ} {t : ℝ} (I : SourceMaximalWitnessInterval μ t) {τ : ℝ} (ht : 0 < t) (hτ : 0 ≤ τ) (hfinite : μ I.interval ≠ ⊤) : MeasureTheory.volume (Metric.ball I.center (τ * I.radius)) ≤ ENNReal.ofReal (τ / t) * μ I.interval

Pointwise enlarged-ball bound in the measure-valued form used for summing.

theorem AleksandrovDifferentiability.SourceMaximalWitnessInterval.countable_of_pairwiseDisjoint_witnessBall {μ : MeasureTheory.Measure ℝ} {t : ℝ} {u : Set (SourceMaximalWitnessInterval μ t)} (hdisj : u.PairwiseDisjoint fun (I : SourceMaximalWitnessInterval μ t) => Metric.ball I.center I.radius) : u.Countable

A disjoint subfamily of nonempty witness balls is countable.

theorem AleksandrovDifferentiability.sourceLocalizedMaximalBadSet_subset_iUnion_witnessInterval {μ : MeasureTheory.Measure ℝ} {t : ℝ} : sourceLocalizedMaximalBadSet μ t ⊆ ⋃ (I : SourceMaximalWitnessInterval μ t), I.interval

The source localized maximal bad set is covered by all its witness intervals.

theorem AleksandrovDifferentiability.sourceLocalizedMaximalBadSet_subset_iUnion_witnessBall {μ : MeasureTheory.Measure ℝ} {t : ℝ} : sourceLocalizedMaximalBadSet μ t ⊆ ⋃ (I : SourceMaximalWitnessInterval μ t), Metric.ball I.center I.radius

Ball-form version of the witness cover, ready for the one-dimensional Vitali covering theorem.

theorem AleksandrovDifferentiability.exists_disjoint_witnessBall_covering_enlargement {μ : MeasureTheory.Measure ℝ} {t τ : ℝ} (hτ : 3 < τ) : ∃ (u : Set (SourceMaximalWitnessInterval μ t)), (u.PairwiseDisjoint fun (I : SourceMaximalWitnessInterval μ t) => Metric.ball I.center I.radius) ∧ sourceLocalizedMaximalBadSet μ t ⊆ ⋃ I ∈ u, Metric.ball I.center (τ * I.radius)

Vitali's ball-covering lemma applied to source maximal witness intervals: there is a disjoint family of witness balls whose τ-enlargements cover the source maximal bad set.

theorem AleksandrovDifferentiability.volume_biUnion_enlarged_witnessBall_le_tsum {μ : MeasureTheory.Measure ℝ} {t τ : ℝ} {u : Set (SourceMaximalWitnessInterval μ t)} (hcount : u.Countable) : MeasureTheory.volume (⋃ I ∈ u, Metric.ball I.center (τ * I.radius)) ≤ ∑' (I : ↑u), MeasureTheory.volume (Metric.ball (↑I).center (τ * (↑I).radius))

Countable subadditivity for the τ-enlargements of a selected witness family.

theorem AleksandrovDifferentiability.volume_biUnion_enlarged_witnessBall_le_tsum_average {μ : MeasureTheory.Measure ℝ} {t τ : ℝ} {u : Set (SourceMaximalWitnessInterval μ t)} (hcount : u.Countable) (ht : 0 < t) (hτ : 0 ≤ τ) : MeasureTheory.volume (⋃ I ∈ u, Metric.ball I.center (τ * I.radius)) ≤ ∑' (I : ↑u), ENNReal.ofReal (τ / t * μ.real (↑I).interval)

The source pointwise ball estimate summed over a countable selected witness family.

theorem AleksandrovDifferentiability.volume_biUnion_enlarged_witnessBall_le_mul_tsum_measure {μ : MeasureTheory.Measure ℝ} {t τ : ℝ} {u : Set (SourceMaximalWitnessInterval μ t)} (hcount : u.Countable) (ht : 0 < t) (hτ : 0 ≤ τ) (hfinite : μ sourceMaximalDomain < ⊤) : MeasureTheory.volume (⋃ I ∈ u, Metric.ball I.center (τ * I.radius)) ≤ ENNReal.ofReal (τ / t) * ∑' (I : ↑u), μ (↑I).interval

The source pointwise ball estimate summed in measure-valued form over a countable selected witness family.

theorem AleksandrovDifferentiability.pairwiseDisjoint_witnessInterval_of_pairwiseDisjoint_witnessBall {μ : MeasureTheory.Measure ℝ} {t : ℝ} {u : Set (SourceMaximalWitnessInterval μ t)} (hdisj : u.PairwiseDisjoint fun (I : SourceMaximalWitnessInterval μ t) => Metric.ball I.center I.radius) : u.PairwiseDisjoint fun (I : SourceMaximalWitnessInterval μ t) => I.interval

Disjoint witness balls give disjoint witness intervals.

theorem AleksandrovDifferentiability.tsum_measure_witnessInterval_le_sourceMaximalDomain {μ : MeasureTheory.Measure ℝ} {t : ℝ} {u : Set (SourceMaximalWitnessInterval μ t)} (hcount : u.Countable) (hdisj : u.PairwiseDisjoint fun (I : SourceMaximalWitnessInterval μ t) => Metric.ball I.center I.radius) : ∑' (I : ↑u), μ (↑I).interval ≤ μ sourceMaximalDomain

The total measure of a selected disjoint witness family is bounded by the measure of the source domain.