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

Localized maximal slice predicates on source cubes

This file connects the one-dimensional localized maximal-function notation to the source-cube coordinate-slice bad predicate used in the upper-contact estimate.

theorem AleksandrovDifferentiability.prod_measure_le_mul_of_fiber_bound {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {s : Set (α × β)} {A : Set α} {C B : ENNReal} (hs : MeasurableSet s) (hA : MeasurableSet A) (hsupport : s ⊆ A ×ˢ Set.univ) (hAmeasure : μ A ≤ C) (hfiber : ∀ a ∈ A, ν (Prod.mk a ⁻¹' s) ≤ B) : (μ.prod ν) s ≤ C * B

Quantitative product-measure Fubini estimate with a transverse support set.

If a measurable set s ⊆ A × univ has every vertical fiber over A bounded by B, and the transverse set A has measure at most C, then the product measure of s is at most C * B. This is the measure-theoretic core of the source proof's passage from one-dimensional coordinate line estimates to coordinate bad-set estimates.

@[reducible, inline]

abbrev AleksandrovDifferentiability.CoordinateSliceMeasureFamily (n : ℕ) : Type

A family of one-dimensional measures assigned to every coordinate direction and coordinate line base. In the source proof these will be the distributional second derivative measures of the convex restrictions s ↦ u(y + s e_i).

Equations

• AleksandrovDifferentiability.CoordinateSliceMeasureFamily n = (Fin n → AleksandrovDifferentiability.SourceCubeSpace n → MeasureTheory.Measure ℝ)

def AleksandrovDifferentiability.coordinateSliceMaximalBadPredicate {n : ℕ} (μslice : CoordinateSliceMeasureFamily n) : CoordinateSliceBadPredicate n

Concrete source-route slice bad predicate from localized maximal functions of a coordinate slice measure family.

Equations

• AleksandrovDifferentiability.coordinateSliceMaximalBadPredicate μslice i y s t = AleksandrovDifferentiability.sourceLocalizedMaximalBadPredicate (μslice i y) s t

def AleksandrovDifferentiability.coordinateSliceLineBadSet {n : ℕ} (μslice : CoordinateSliceMeasureFamily n) (i : Fin n) (y : SourceCubeSpace n) (t : ℝ) : Set ℝ

One-dimensional bad set on the coordinate line with base y, direction i, and threshold t. This is the fiber set appearing in the Fubini step for E_i(t).

Equations

• AleksandrovDifferentiability.coordinateSliceLineBadSet μslice i y t = AleksandrovDifferentiability.sourceLocalizedMaximalBadSet (μslice i y) t

def AleksandrovDifferentiability.CoordinateSliceMaximalBadPredicateMeasurable {n : ℕ} (μslice : CoordinateSliceMeasureFamily n) (t : ℝ) : Prop

Product-coordinate measurability obligation for the concrete localized maximal slice predicate.

Equations

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

def AleksandrovDifferentiability.CoordinateSliceSourceLocalizedMaximalMeasurable {n : ℕ} (μslice : CoordinateSliceMeasureFamily n) (t : ℝ) : Prop

One-dimensional parameterized measurability obligation for every coordinate slice family.

For each coordinate direction i, the parameter is the coordinate-line base y, and the one-dimensional source-local maximal bad predicate is measurable in (y,s).

Equations

• AleksandrovDifferentiability.CoordinateSliceSourceLocalizedMaximalMeasurable μslice t = ∀ (i : Fin n), AleksandrovDifferentiability.SourceLocalizedMaximalBadPredicateMeasurable (μslice i) t

def AleksandrovDifferentiability.CoordinateSliceSourceLocalizedMaximalMeasurableOnWindow {n : ℕ} (μslice : CoordinateSliceMeasureFamily n) (t : ℝ) : Prop

Source-window-restricted one-dimensional measurability obligation for every coordinate slice family. This is sufficient for the cube bad sets, since their coordinate parameter lies in sourceMaximalWindow.

Equations

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

def AleksandrovDifferentiability.CoordinateSliceSourceLocalizedMaximalAverageExceedsMeasurable {n : ℕ} (μslice : CoordinateSliceMeasureFamily n) (t : ℝ) : Prop

Interval-average-exceeds measurability obligation for every coordinate slice family.

Equations

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

def AleksandrovDifferentiability.CoordinateSliceSourceLocalizedMaximalAverageExceedsCountableIntervalFamilyMeasurable {n : ℕ} (μslice : CoordinateSliceMeasureFamily n) (a b : ℕ → ℝ) (t : ℝ) : Prop

Coordinate version of countable fixed-interval measurability for source-local maximal average-exceeds sets.

Equations

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

def AleksandrovDifferentiability.CoordinateSliceSourceLocalizedMaximalAverageExceedsCountableIntervalCover {n : ℕ} (μslice : CoordinateSliceMeasureFamily n) (a b : ℕ → ℝ) (t : ℝ) : Prop

Coordinate version of the assertion that the source average-exceeds set is represented by a countable fixed-interval family.

Equations

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

def AleksandrovDifferentiability.CoordinateSliceSourceLocalizedMaximalAverageExceedsCountableIntervalReverseCover {n : ℕ} (μslice : CoordinateSliceMeasureFamily n) (a b : ℕ → ℝ) (t : ℝ) : Prop

Coordinate version of the reverse-cover assertion for a countable fixed-interval family.

Equations

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

def AleksandrovDifferentiability.CoordinateSliceSourceLocalizedMaximalAverageExceedsRationalRefinement {n : ℕ} (μslice : CoordinateSliceMeasureFamily n) (t : ℝ) : Prop

Coordinate version of rational refinement for source-local average-exceeds witnesses.

Equations

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

def AleksandrovDifferentiability.CoordinateSliceSourceLocalizedMaximalAverageExceedsInnerRationalRefinement {n : ℕ} (μslice : CoordinateSliceMeasureFamily n) (t : ℝ) : Prop

Coordinate version of inner-rational refinement for source-local average-exceeds witnesses.

Equations

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

def AleksandrovDifferentiability.CoordinateSliceSourceLocalizedMaximalAverageExceedsInnerRationalTendsto {n : ℕ} (μslice : CoordinateSliceMeasureFamily n) (t : ℝ) : Prop

Coordinate version of sequential inner-rational average approximation.

Equations

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

def AleksandrovDifferentiability.CoordinateSliceSourceLocalizedMaximalAverageExceedsInnerRationalMassTendsto {n : ℕ} (μslice : CoordinateSliceMeasureFamily n) (t : ℝ) : Prop

Coordinate version of sequential inner-rational mass approximation.

Equations

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

def AleksandrovDifferentiability.CoordinateSliceSourceLocalizedMaximalFixedIntervalAverageMeasurable {n : ℕ} (μslice : CoordinateSliceMeasureFamily n) (a b : ℕ → ℝ) : Prop

Measurability of all fixed-interval coordinate averages.

Equations

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

def AleksandrovDifferentiability.CoordinateSliceMaximalBadSetMeasurable {n : ℕ} (μslice : CoordinateSliceMeasureFamily n) (t : ℝ) : Prop

Measurability obligation for the source-route coordinate maximal bad sets.

This names the analytic measurability input needed by the Fubini step. It deliberately only records measurability of the ambient coordinate bad sets E_i(t); the product chart and transverse Fubini bookkeeping are proved separately below.

Equations

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

theorem AleksandrovDifferentiability.CoordinateSliceMaximalBadPredicateMeasurable.badSetMeasurable {n : ℕ} {μslice : CoordinateSliceMeasureFamily n} {t : ℝ} (hbad : CoordinateSliceMaximalBadPredicateMeasurable μslice t) : CoordinateSliceMaximalBadSetMeasurable μslice t

Joint product-coordinate measurability of the maximal bad predicate gives measurability of the ambient coordinate maximal bad sets.

theorem AleksandrovDifferentiability.CoordinateSliceSourceLocalizedMaximalMeasurable.badPredicateMeasurable {n : ℕ} {μslice : CoordinateSliceMeasureFamily n} {t : ℝ} (hbad : CoordinateSliceSourceLocalizedMaximalMeasurable μslice t) : CoordinateSliceMaximalBadPredicateMeasurable μslice t

Parameterized one-dimensional maximal measurability supplies the product-coordinate measurability of the coordinate maximal bad predicate.

theorem AleksandrovDifferentiability.CoordinateSliceSourceLocalizedMaximalMeasurable.badSetMeasurable {n : ℕ} {μslice : CoordinateSliceMeasureFamily n} {t : ℝ} (hbad : CoordinateSliceSourceLocalizedMaximalMeasurable μslice t) : CoordinateSliceMaximalBadSetMeasurable μslice t

Parameterized one-dimensional maximal measurability supplies measurability of the ambient coordinate maximal bad sets.

theorem AleksandrovDifferentiability.CoordinateSliceSourceLocalizedMaximalMeasurableOnWindow.badSetMeasurable {n : ℕ} {μslice : CoordinateSliceMeasureFamily n} {t : ℝ} (hbad : CoordinateSliceSourceLocalizedMaximalMeasurableOnWindow μslice t) : CoordinateSliceMaximalBadSetMeasurable μslice t

Source-window-restricted one-dimensional maximal measurability supplies measurability of the ambient coordinate maximal bad sets.

theorem AleksandrovDifferentiability.CoordinateSliceSourceLocalizedMaximalAverageExceedsMeasurable.badSetMeasurable {n : ℕ} {μslice : CoordinateSliceMeasureFamily n} {t : ℝ} (havg : CoordinateSliceSourceLocalizedMaximalAverageExceedsMeasurable μslice t) : CoordinateSliceMaximalBadSetMeasurable μslice t

Interval-average-exceeds measurability supplies measurability of the ambient coordinate maximal bad sets.

theorem AleksandrovDifferentiability.CoordinateSliceSourceLocalizedMaximalAverageExceedsMeasurable.of_countableIntervalFamily {n : ℕ} {μslice : CoordinateSliceMeasureFamily n} {a b : ℕ → ℝ} {t : ℝ} (hfixed : CoordinateSliceSourceLocalizedMaximalAverageExceedsCountableIntervalFamilyMeasurable μslice a b t) (hcover : CoordinateSliceSourceLocalizedMaximalAverageExceedsCountableIntervalCover μslice a b t) : CoordinateSliceSourceLocalizedMaximalAverageExceedsMeasurable μslice t

A countable fixed-interval representation of the source average-exceeds sets gives the coordinate average-exceeds measurability input.

theorem AleksandrovDifferentiability.CoordinateSliceSourceLocalizedMaximalAverageExceedsCountableIntervalCover.of_reverseCover {n : ℕ} {μslice : CoordinateSliceMeasureFamily n} {a b : ℕ → ℝ} {t : ℝ} (hadm : SourceAdmissibleIntervalEnumeration a b) (hreverse : CoordinateSliceSourceLocalizedMaximalAverageExceedsCountableIntervalReverseCover μslice a b t) : CoordinateSliceSourceLocalizedMaximalAverageExceedsCountableIntervalCover μslice a b t

An admissible interval enumeration plus the coordinate reverse-cover direction gives the coordinate countable-interval representation.

theorem AleksandrovDifferentiability.CoordinateSliceSourceLocalizedMaximalAverageExceedsRationalRefinement.tendsto_of_massTendsto {n : ℕ} {μslice : CoordinateSliceMeasureFamily n} {t : ℝ} (hmassApprox : CoordinateSliceSourceLocalizedMaximalAverageExceedsInnerRationalMassTendsto μslice t) : CoordinateSliceSourceLocalizedMaximalAverageExceedsInnerRationalTendsto μslice t

Coordinate sequential inner-rational mass approximation gives coordinate sequential inner-rational average approximation.

theorem AleksandrovDifferentiability.CoordinateSliceSourceLocalizedMaximalAverageExceedsRationalRefinement.inner_of_tendsto {n : ℕ} {μslice : CoordinateSliceMeasureFamily n} {t : ℝ} (happrox : CoordinateSliceSourceLocalizedMaximalAverageExceedsInnerRationalTendsto μslice t) : CoordinateSliceSourceLocalizedMaximalAverageExceedsInnerRationalRefinement μslice t

Coordinate sequential inner-rational approximation gives coordinate inner-rational refinement.

theorem AleksandrovDifferentiability.CoordinateSliceSourceLocalizedMaximalAverageExceedsRationalRefinement.of_inner {n : ℕ} {μslice : CoordinateSliceMeasureFamily n} {t : ℝ} (hrefine : CoordinateSliceSourceLocalizedMaximalAverageExceedsInnerRationalRefinement μslice t) : CoordinateSliceSourceLocalizedMaximalAverageExceedsRationalRefinement μslice t

Coordinate inner-rational refinement gives coordinate rational refinement.

theorem AleksandrovDifferentiability.CoordinateSliceSourceLocalizedMaximalAverageExceedsCountableIntervalReverseCover.rationalRefinement_of_inner {n : ℕ} {μslice : CoordinateSliceMeasureFamily n} {t : ℝ} (hrefine : CoordinateSliceSourceLocalizedMaximalAverageExceedsInnerRationalRefinement μslice t) : CoordinateSliceSourceLocalizedMaximalAverageExceedsRationalRefinement μslice t

Coordinate inner-rational refinement gives coordinate rational refinement.

theorem AleksandrovDifferentiability.CoordinateSliceSourceLocalizedMaximalAverageExceedsCountableIntervalReverseCover.of_rationalRefinement {n : ℕ} {μslice : CoordinateSliceMeasureFamily n} {a b : ℕ → ℝ} {t : ℝ} (henum : SourceRationalIntervalEnumeration a b) (hrefine : CoordinateSliceSourceLocalizedMaximalAverageExceedsRationalRefinement μslice t) : CoordinateSliceSourceLocalizedMaximalAverageExceedsCountableIntervalReverseCover μslice a b t

A rational interval enumeration and coordinate rational refinement give the coordinate reverse-cover direction.

theorem AleksandrovDifferentiability.CoordinateSliceAverageExceedsCountableIntervalFamily.of_measurableAverage {n : ℕ} {μslice : CoordinateSliceMeasureFamily n} {a b : ℕ → ℝ} {t : ℝ} (havg : CoordinateSliceSourceLocalizedMaximalFixedIntervalAverageMeasurable μslice a b) : CoordinateSliceSourceLocalizedMaximalAverageExceedsCountableIntervalFamilyMeasurable μslice a b t

Measurable fixed-interval coordinate averages give the coordinate countable-interval measurability input.

theorem AleksandrovDifferentiability.CoordinateSliceAverageExceedsCountableIntervalFamily.badSetMeasurable {n : ℕ} {μslice : CoordinateSliceMeasureFamily n} {a b : ℕ → ℝ} {t : ℝ} (hfixed : CoordinateSliceSourceLocalizedMaximalAverageExceedsCountableIntervalFamilyMeasurable μslice a b t) (hcover : CoordinateSliceSourceLocalizedMaximalAverageExceedsCountableIntervalCover μslice a b t) : CoordinateSliceMaximalBadSetMeasurable μslice t

A countable fixed-interval representation of the source average-exceeds sets is enough for coordinate maximal bad-set measurability.

def AleksandrovDifferentiability.CoordinateSliceSourceMassBound {n : ℕ} (μslice : CoordinateSliceMeasureFamily n) (osc : ℝ) : Prop

Uniform source mass bound for every coordinate slice over bases in Q_1. In the source proof this comes from the one-dimensional convex second-derivative mass estimate applied to s ↦ u(y + s e_i), and the bound by osc_{Q_3} u.

Equations

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

@[simp]

theorem AleksandrovDifferentiability.mem_coordinateSliceLineBadSet {n : ℕ} {μslice : CoordinateSliceMeasureFamily n} {i : Fin n} {y : SourceCubeSpace n} {t s : ℝ} : s ∈ coordinateSliceLineBadSet μslice i y t ↔ s ∈ sourceMaximalWindow ∧ sourceLocalizedMaximalBadPredicate (μslice i y) s t

theorem AleksandrovDifferentiability.mem_coordinateSliceLineBadSet_iff_exists_average_gt {n : ℕ} {μslice : CoordinateSliceMeasureFamily n} {i : Fin n} {y : SourceCubeSpace n} {t s : ℝ} : s ∈ coordinateSliceLineBadSet μslice i y t ↔ s ∈ sourceMaximalWindow ∧ ∃ (a : ℝ) (b : ℝ), a < b ∧ Set.Ioo a b ⊆ sourceMaximalDomain ∧ s ∈ Set.Ioo a b ∧ t < openIntervalMeasureAverage (μslice i y) a b

Membership in a coordinate-line maximal bad set is equivalent to the existence of one source-admissible interval through the line parameter whose slice-measure average exceeds the threshold.

def AleksandrovDifferentiability.coordinateSliceBadSetProductModel {n : ℕ} (μslice : CoordinateSliceMeasureFamily n) (i : Fin n) (t : ℝ) : Set (SourceTransverseSpace i × ℝ)

Product-chart preimage of the concrete coordinate bad set for direction i.

Equations

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

@[simp]

theorem AleksandrovDifferentiability.mem_coordinateSliceBadSetProductModel {n : ℕ} {μslice : CoordinateSliceMeasureFamily n} {i : Fin n} {t : ℝ} {p : SourceTransverseSpace i × ℝ} : p ∈ coordinateSliceBadSetProductModel μslice i t ↔ sourceCoordinateChartPoint i p.1 p.2 ∈ coordinateSliceBadSet (coordinateSliceMaximalBadPredicate μslice) i t

theorem AleksandrovDifferentiability.MeasurableSet.coordinateSliceBadSetProductModel {n : ℕ} {μslice : CoordinateSliceMeasureFamily n} {i : Fin n} {t : ℝ} (hbad : MeasurableSet (coordinateSliceBadSet (coordinateSliceMaximalBadPredicate μslice) i t)) : MeasurableSet (AleksandrovDifferentiability.coordinateSliceBadSetProductModel μslice i t)

Measurability of the product-model bad set follows from measurability of the ambient coordinate bad set and continuity of the coordinate chart.

theorem AleksandrovDifferentiability.coordinateSliceBadSet_measure_le_of_productModel {n : ℕ} {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {μslice : CoordinateSliceMeasureFamily n} {i : Fin n} {Ctrans t : ℝ} {B : ENNReal} {A : Set α} {S : Set (α × ℝ)} {base : α → SourceCubeSpace n} (hbad_le : MeasureTheory.volume (coordinateSliceBadSet (coordinateSliceMaximalBadPredicate μslice) i t) ≤ (μ.prod MeasureTheory.volume) S) (hS : MeasurableSet S) (hA : MeasurableSet A) (hsupport : S ⊆ A ×ˢ Set.univ) (hAmeasure : μ A ≤ ENNReal.ofReal Ctrans) (hbase : ∀ a ∈ A, base a ∈ sourceOpenCube n 1) (hsection : ∀ a ∈ A, Prod.mk a ⁻¹' S ⊆ coordinateSliceLineBadSet μslice i (base a) t) (hline : ∀ (j : Fin n) ⦃y : SourceCubeSpace n⦄, y ∈ sourceOpenCube n 1 → MeasureTheory.volume (coordinateSliceLineBadSet μslice j y t) ≤ B) : MeasureTheory.volume (coordinateSliceBadSet (coordinateSliceMaximalBadPredicate μslice) i t) ≤ ENNReal.ofReal Ctrans * B

Product-model version of the coordinate-slice Fubini bound for one fixed coordinate.

The data A, S, and base represent a transverse product chart for the coordinate bad set: S is the product-model preimage of the coordinate bad set, A is the allowed transverse set, and base a is the source-cube base point of the coordinate line over a. Once this geometric data is available, the quantitative estimate follows from prod_measure_le_mul_of_fiber_bound and the one-dimensional line bounds.

theorem AleksandrovDifferentiability.mem_coordinateSliceBadSet_maximal_iff {n : ℕ} {μslice : CoordinateSliceMeasureFamily n} {i : Fin n} {t : ℝ} {x : SourceCubeSpace n} : x ∈ coordinateSliceBadSet (coordinateSliceMaximalBadPredicate μslice) i t ↔ x ∈ sourceOpenCube n 1 ∧ x.ofLp i ∈ coordinateSliceLineBadSet μslice i (coordinateLineBase i x) t

Membership in the concrete coordinate bad set is membership in Q_1 together with membership of the coordinate parameter in the corresponding one-dimensional localized maximal bad set.

theorem AleksandrovDifferentiability.mem_coordinateSliceBadSet_maximal_iff_exists_average_gt {n : ℕ} {μslice : CoordinateSliceMeasureFamily n} {i : Fin n} {t : ℝ} {x : SourceCubeSpace n} : x ∈ coordinateSliceBadSet (coordinateSliceMaximalBadPredicate μslice) i t ↔ x ∈ sourceOpenCube n 1 ∧ ∃ (a : ℝ) (b : ℝ), a < b ∧ Set.Ioo a b ⊆ sourceMaximalDomain ∧ x.ofLp i ∈ Set.Ioo a b ∧ t < openIntervalMeasureAverage (μslice i (coordinateLineBase i x)) a b

Ambient coordinate maximal bad-set membership in interval-average form. This is the source-proof description of E_i(t): a point of Q_1 is bad in coordinate direction i iff some source-admissible interval through its coordinate parameter has average larger than t.

theorem AleksandrovDifferentiability.coordinateSliceBadSetProductModel_subset_transverse {n : ℕ} {μslice : CoordinateSliceMeasureFamily n} {i : Fin n} {t : ℝ} : coordinateSliceBadSetProductModel μslice i t ⊆ sourceTransverseOpenCube i 1 ×ˢ Set.univ

The product-model coordinate bad set is supported over the transverse unit cube.

theorem AleksandrovDifferentiability.coordinateSliceBadSetProductModel_section_subset_lineBadSet {n : ℕ} {μslice : CoordinateSliceMeasureFamily n} {i : Fin n} {t : ℝ} {a : SourceTransverseSpace i} : Prod.mk a ⁻¹' coordinateSliceBadSetProductModel μslice i t ⊆ coordinateSliceLineBadSet μslice i (sourceTransverseEmbed i a) t

Each product-model vertical fiber is contained in the corresponding one-dimensional line bad set.

theorem AleksandrovDifferentiability.sourceTransverseOpenCube_volume_lt_top {n : ℕ} (i : Fin n) : MeasureTheory.volume (sourceTransverseOpenCube i 1) < ⊤

The transverse unit cube has finite Lebesgue measure.

theorem AleksandrovDifferentiability.sourceTransverseOpenCube_volume_le_ofReal_toReal {n : ℕ} (i : Fin n) : MeasureTheory.volume (sourceTransverseOpenCube i 1) ≤ ENNReal.ofReal (MeasureTheory.volume (sourceTransverseOpenCube i 1)).toReal

The finite transverse volume gives an admissible transverse Fubini constant for the canonical transverse unit cube.

theorem AleksandrovDifferentiability.exists_forall_sourceTransverseOpenCube_volume_le_ofReal {n : ℕ} : ∃ (Ctrans : ℝ), ∀ (i : Fin n), MeasureTheory.volume (sourceTransverseOpenCube i 1) ≤ ENNReal.ofReal Ctrans

There exists a real transverse constant bounding the Lebesgue measure of every coordinate transverse unit cube. This is the constant-existence form needed before choosing a cleaner closed-form scalar in the final source estimate.

theorem AleksandrovDifferentiability.exists_nonneg_forall_sourceTransverseOpenCube_volume_le_ofReal {n : ℕ} : ∃ (Ctrans : ℝ), 0 ≤ Ctrans ∧ ∀ (i : Fin n), MeasureTheory.volume (sourceTransverseOpenCube i 1) ≤ ENNReal.ofReal Ctrans

There exists a nonnegative real transverse constant bounding the Lebesgue measure of every coordinate transverse unit cube.

theorem AleksandrovDifferentiability.sourceCoordinateChartMap_measurePreserving {n : ℕ} (i : Fin n) : MeasureTheory.MeasurePreserving (sourceCoordinateChartMap i) (MeasureTheory.volume.prod MeasureTheory.volume) MeasureTheory.volume

The canonical coordinate chart from transverse coordinates and the distinguished coordinate is Lebesgue-measure preserving.

theorem AleksandrovDifferentiability.coordinateSliceBadSet_measure_le_of_coordinateProductModel {n : ℕ} {μslice : CoordinateSliceMeasureFamily n} {i : Fin n} {Ctrans t : ℝ} {B : ENNReal} (hbad_le : MeasureTheory.volume (coordinateSliceBadSet (coordinateSliceMaximalBadPredicate μslice) i t) ≤ (MeasureTheory.volume.prod MeasureTheory.volume) (coordinateSliceBadSetProductModel μslice i t)) (hS : MeasurableSet (coordinateSliceBadSetProductModel μslice i t)) (hAmeasure : MeasureTheory.volume (sourceTransverseOpenCube i 1) ≤ ENNReal.ofReal Ctrans) (hline : ∀ (j : Fin n) ⦃y : SourceCubeSpace n⦄, y ∈ sourceOpenCube n 1 → MeasureTheory.volume (coordinateSliceLineBadSet μslice j y t) ≤ B) : MeasureTheory.volume (coordinateSliceBadSet (coordinateSliceMaximalBadPredicate μslice) i t) ≤ ENNReal.ofReal Ctrans * B

Fixed-coordinate product-model Fubini estimate specialized to the canonical coordinate chart. The remaining hypotheses are exactly the measurable/product-measure facts about that chart.

theorem AleksandrovDifferentiability.coordinateSliceBadSet_measure_eq_productModel_of_chartMeasurePreserving {n : ℕ} {μslice : CoordinateSliceMeasureFamily n} {i : Fin n} {t : ℝ} (hchart : MeasureTheory.MeasurePreserving (sourceCoordinateChartMap i) (MeasureTheory.volume.prod MeasureTheory.volume) MeasureTheory.volume) (hbad : MeasureTheory.NullMeasurableSet (coordinateSliceBadSet (coordinateSliceMaximalBadPredicate μslice) i t) MeasureTheory.volume) : (MeasureTheory.volume.prod MeasureTheory.volume) (coordinateSliceBadSetProductModel μslice i t) = MeasureTheory.volume (coordinateSliceBadSet (coordinateSliceMaximalBadPredicate μslice) i t)

If the canonical coordinate chart is measure-preserving, then the ambient coordinate bad set has the same measure as its product-model preimage.

theorem AleksandrovDifferentiability.coordinateSliceBadSet_measure_le_of_coordinateChartMeasurePreserving {n : ℕ} {μslice : CoordinateSliceMeasureFamily n} {i : Fin n} {Ctrans t : ℝ} {B : ENNReal} (hchart : MeasureTheory.MeasurePreserving (sourceCoordinateChartMap i) (MeasureTheory.volume.prod MeasureTheory.volume) MeasureTheory.volume) (hbad : MeasurableSet (coordinateSliceBadSet (coordinateSliceMaximalBadPredicate μslice) i t)) (hAmeasure : MeasureTheory.volume (sourceTransverseOpenCube i 1) ≤ ENNReal.ofReal Ctrans) (hline : ∀ (j : Fin n) ⦃y : SourceCubeSpace n⦄, y ∈ sourceOpenCube n 1 → MeasureTheory.volume (coordinateSliceLineBadSet μslice j y t) ≤ B) : MeasureTheory.volume (coordinateSliceBadSet (coordinateSliceMaximalBadPredicate μslice) i t) ≤ ENNReal.ofReal Ctrans * B

Fixed-coordinate product-model Fubini estimate using a measure-preserving coordinate chart. The remaining assumptions are measurability of the ambient coordinate bad set, the chart measure-preserving fact, and the transverse-volume bound.