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

Coordinate-slice maximal Fubini estimates

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

A uniform measure bound on line sections controls each coordinate bad set by Fubini.

Equations

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

theorem AleksandrovDifferentiability.CoordinateSliceMaximalTransverseFubiniEstimate.of_coordinateProductModel {n : ℕ} {μslice : CoordinateSliceMeasureFamily n} {Ctrans t : ℝ} (hbad_le : ∀ (i : Fin n), MeasureTheory.volume (coordinateSliceBadSet (coordinateSliceMaximalBadPredicate μslice) i t) ≤ (MeasureTheory.volume.prod MeasureTheory.volume) (coordinateSliceBadSetProductModel μslice i t)) (hS : ∀ (i : Fin n), MeasurableSet (coordinateSliceBadSetProductModel μslice i t)) (hAmeasure : ∀ (i : Fin n), MeasureTheory.volume (sourceTransverseOpenCube i 1) ≤ ENNReal.ofReal Ctrans) : CoordinateSliceMaximalTransverseFubiniEstimate μslice Ctrans t

The transverse Fubini estimate follows from the canonical coordinate product model once the chart measurability, chart measure comparison, and transverse-volume bound are supplied.

theorem AleksandrovDifferentiability.CoordinateSliceMaximalTransverseFubiniEstimate.of_coordinateChartMeasurePreserving {n : ℕ} {μslice : CoordinateSliceMeasureFamily n} {Ctrans t : ℝ} (hchart : ∀ (i : Fin n), MeasureTheory.MeasurePreserving (sourceCoordinateChartMap i) (MeasureTheory.volume.prod MeasureTheory.volume) MeasureTheory.volume) (hbad : ∀ (i : Fin n), MeasurableSet (coordinateSliceBadSet (coordinateSliceMaximalBadPredicate μslice) i t)) (hAmeasure : ∀ (i : Fin n), MeasureTheory.volume (sourceTransverseOpenCube i 1) ≤ ENNReal.ofReal Ctrans) : CoordinateSliceMaximalTransverseFubiniEstimate μslice Ctrans t

The transverse Fubini estimate follows from measure-preserving canonical coordinate charts, measurability of the coordinate bad sets, and the transverse-volume bound.

theorem AleksandrovDifferentiability.CoordinateSliceMaximalTransverseFubiniEstimate.of_coordinateBadSetMeasurable {n : ℕ} {μslice : CoordinateSliceMeasureFamily n} {Ctrans t : ℝ} (hbad : ∀ (i : Fin n), MeasurableSet (coordinateSliceBadSet (coordinateSliceMaximalBadPredicate μslice) i t)) (hAmeasure : ∀ (i : Fin n), MeasureTheory.volume (sourceTransverseOpenCube i 1) ≤ ENNReal.ofReal Ctrans) : CoordinateSliceMaximalTransverseFubiniEstimate μslice Ctrans t

The transverse Fubini estimate follows from coordinate bad-set measurability and transverse volume bounds; the canonical coordinate charts are measure-preserving.

theorem AleksandrovDifferentiability.CoordinateSliceMaximalTransverseFubiniEstimate.of_badSetMeasurable {n : ℕ} {μslice : CoordinateSliceMeasureFamily n} {Ctrans t : ℝ} (hbad : CoordinateSliceMaximalBadSetMeasurable μslice t) (hAmeasure : ∀ (i : Fin n), MeasureTheory.volume (sourceTransverseOpenCube i 1) ≤ ENNReal.ofReal Ctrans) : CoordinateSliceMaximalTransverseFubiniEstimate μslice Ctrans t

Named-obligation version of CoordinateSliceMaximalTransverseFubiniEstimate.of_coordinateBadSetMeasurable.

theorem AleksandrovDifferentiability.exists_coordinateSliceMaximalTransverseFubiniEstimate_of_coordinateBadSetMeasurable {n : ℕ} {μslice : CoordinateSliceMeasureFamily n} {t : ℝ} (hbad : ∀ (i : Fin n), MeasurableSet (coordinateSliceBadSet (coordinateSliceMaximalBadPredicate μslice) i t)) : ∃ (Ctrans : ℝ), CoordinateSliceMaximalTransverseFubiniEstimate μslice Ctrans t

If the coordinate bad sets are measurable, then some real transverse constant gives the transverse Fubini estimate. This is the constant-existence form of the source Fubini step.

theorem AleksandrovDifferentiability.CoordinateSliceMaximalBadSetMeasurable.exists_transverseFubiniEstimate {n : ℕ} {μslice : CoordinateSliceMeasureFamily n} {t : ℝ} (hbad : CoordinateSliceMaximalBadSetMeasurable μslice t) : ∃ (Ctrans : ℝ), CoordinateSliceMaximalTransverseFubiniEstimate μslice Ctrans t

Named-obligation version of the existential transverse Fubini step.

theorem AleksandrovDifferentiability.CoordinateSliceSourceMassBound.lineBadSet_measure_le {n : ℕ} {μslice : CoordinateSliceMeasureFamily n} {osc C t : ℝ} (hmass : CoordinateSliceSourceMassBound μslice osc) (hmax : LocalizedMaximalEstimateStatement C) (ht : 0 < t) (i : Fin n) {y : SourceCubeSpace n} (hy : y ∈ sourceOpenCube n 1) : MeasureTheory.volume (coordinateSliceLineBadSet μslice i y t) ≤ ENNReal.ofReal (2 * C * osc / t)

The one-dimensional localized maximal estimate plus the source mass bound controls each coordinate-line bad fiber.

def AleksandrovDifferentiability.CoordinateSliceMaximalEndpointControl {n : ℕ} (u : SourceCubeSpace n → ℝ) (μslice : CoordinateSliceMeasureFamily n) (ρ K t : ℝ) : Prop

Endpoint control for the concrete localized-maximal slice predicate. This is the exact one-dimensional convex estimate still to be proved from the distributional second derivative measure of the slice.

Equations

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

def AleksandrovDifferentiability.CoordinateSliceOneDimEndpointControl {n : ℕ} (u : SourceCubeSpace n → ℝ) (μslice : CoordinateSliceMeasureFamily n) (ρ K : ℝ) : Prop

Coordinate-slice version of the one-dimensional endpoint-control input. The constant K is a multiplier for the maximal threshold t, matching the source estimate \tilde u(±h e_i) <= C t h^2.

Equations

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

theorem AleksandrovDifferentiability.coordinateLineDomain_sourceOpenCube_three_of_mem_sourceOpenCube_one {n : ℕ} {i : Fin n} {x : SourceCubeSpace n} (hx : x ∈ sourceOpenCube n 1) : lineDomain (sourceOpenCube n 3) (coordinateLineBase i x) (sourceCoordinateVector i) = Set.Ioo (-3) 3

For a coordinate line through a point of Q_1, the parameters that stay in Q_3 are exactly the source interval (-3,3).

theorem AleksandrovDifferentiability.ConvexOn.coordinateLineRestriction_sourceCube_three {n : ℕ} {u : SourceCubeSpace n → ℝ} (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (i : Fin n) {y : SourceCubeSpace n} (hy : y ∈ sourceOpenCube n 1) : ConvexOn ℝ (Set.Ioo (-3) 3) (AleksandrovDifferentiability.lineRestriction u (coordinateLineBase i y) (sourceCoordinateVector i))

Convexity on the source cube restricts to convexity of every coordinate slice over a base in Q_1, with the source interval (-3,3) as line domain.

theorem AleksandrovDifferentiability.ConvexOn.coordinateLineRightDeriv_monotoneOn_sourceIcc {n : ℕ} {u : SourceCubeSpace n → ℝ} (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (i : Fin n) {y : SourceCubeSpace n} (hy : y ∈ sourceOpenCube n 1) : MonotoneOn (rightDeriv (AleksandrovDifferentiability.lineRestriction u (coordinateLineBase i y) (sourceCoordinateVector i))) (Set.Icc (-2) 2)

Convexity on the source cube supplies the monotonicity hypothesis needed for the source-local clamped Stieltjes measure of each coordinate slice.

theorem AleksandrovDifferentiability.CoordinateSliceOneDimEndpointControl.coordinateSliceMaximalEndpointControl {n : ℕ} {u : SourceCubeSpace n → ℝ} {μslice : CoordinateSliceMeasureFamily n} {ρ K t : ℝ} (hendpoint : CoordinateSliceOneDimEndpointControl u μslice ρ K) (hu : ConvexOn ℝ (sourceOpenCube n 3) u) : CoordinateSliceMaximalEndpointControl u μslice ρ (K * t) t

The one-dimensional endpoint-control estimate for every coordinate slice supplies the concrete endpoint-control input used by the source upper-contact inclusion.

def AleksandrovDifferentiability.CoordinateSliceMaximalTotalBadSetEstimate {n : ℕ} (u : SourceCubeSpace n → ℝ) (μslice : CoordinateSliceMeasureFamily n) (C t : ℝ) : Prop

Total bad-set measure estimate for the concrete localized-maximal slice predicate. This is the exact Fubini plus weak-type estimate still to be proved from the one-dimensional localized maximal theorem and the source mass bound for slice second-derivative measures.

Equations

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

theorem AleksandrovDifferentiability.CoordinateSliceMaximalTotalBadSetEstimate.mono_constant {n : ℕ} {u : SourceCubeSpace n → ℝ} {μslice : CoordinateSliceMeasureFamily n} {C C' t : ℝ} (h : CoordinateSliceMaximalTotalBadSetEstimate u μslice C t) (hCC' : C ≤ C') (ht : 0 < t) (hosc : 0 ≤ sourceCubeOscillation n u) : CoordinateSliceMaximalTotalBadSetEstimate u μslice C' t

The concrete localized-maximal total-bad-set estimate is monotone in the dimensional constant.

theorem AleksandrovDifferentiability.CoordinateSliceMaximalTotalBadSetEstimate.mono_constant_of_boundedOn {n : ℕ} {u : SourceCubeSpace n → ℝ} {μslice : CoordinateSliceMeasureFamily n} {C C' t : ℝ} (h : CoordinateSliceMaximalTotalBadSetEstimate u μslice C t) (hCC' : C ≤ C') (ht : 0 < t) (hbounded : BoundedOn (sourceOpenCube n 3) u) : CoordinateSliceMaximalTotalBadSetEstimate u μslice C' t

Boundedness supplies the oscillation nonnegativity needed for monotonicity of the concrete localized-maximal total-bad-set estimate.

theorem AleksandrovDifferentiability.CoordinateSliceMaximalTotalBadSetEstimate.of_coordinate_bound {n : ℕ} {u : SourceCubeSpace n → ℝ} {μslice : CoordinateSliceMeasureFamily n} {C t : ℝ} {B : ENNReal} (hdiff : MeasureTheory.volume (sourceOpenCube n 1 \ firstOrderDifferentiabilitySet u) = 0) (hcoord : ∀ (i : Fin n), MeasureTheory.volume (coordinateSliceBadSet (coordinateSliceMaximalBadPredicate μslice) i t) ≤ B) (hbound : ↑n * B ≤ ENNReal.ofReal (C * sourceCubeOscillation n u / t)) : CoordinateSliceMaximalTotalBadSetEstimate u μslice C t

Constant-bound finite-union assembly for the concrete localized-maximal total bad set. The remaining Fubini work should provide the coordinate bounds; this theorem packages the null non-differentiability set and finite union over coordinate directions.

def AleksandrovDifferentiability.CoordinateSliceMaximalFubiniEstimate {n : ℕ} (μslice : CoordinateSliceMeasureFamily n) (Cline Ccoord osc t : ℝ) : Prop

The remaining per-coordinate Fubini obligation for localized maximal bad sets. It says that uniform one-dimensional bad-fiber bounds imply coordinate bad-set bounds. The constants are kept separate because the Fubini step may introduce a dimensional factor.

Equations

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

theorem AleksandrovDifferentiability.CoordinateSliceMaximalTransverseFubiniEstimate.fubiniEstimate {n : ℕ} {μslice : CoordinateSliceMeasureFamily n} {Ctrans Cline Ccoord osc t : ℝ} (htrans : CoordinateSliceMaximalTransverseFubiniEstimate μslice Ctrans t) (hCtrans_nonneg : 0 ≤ Ctrans) (hC : Ctrans * Cline ≤ Ccoord) (hscale : 0 ≤ osc / t) : CoordinateSliceMaximalFubiniEstimate μslice Cline Ccoord osc t

The transverse Fubini estimate plus a real-valued constant comparison supplies the older packaged per-coordinate Fubini estimate.

theorem AleksandrovDifferentiability.CoordinateSliceMaximalFubiniEstimate.of_badSetMeasurable {n : ℕ} {μslice : CoordinateSliceMeasureFamily n} {Ctrans Cline Ccoord osc t : ℝ} (hbad : CoordinateSliceMaximalBadSetMeasurable μslice t) (hAmeasure : ∀ (i : Fin n), MeasureTheory.volume (sourceTransverseOpenCube i 1) ≤ ENNReal.ofReal Ctrans) (hCtrans_nonneg : 0 ≤ Ctrans) (hC : Ctrans * Cline ≤ Ccoord) (hscale : 0 ≤ osc / t) : CoordinateSliceMaximalFubiniEstimate μslice Cline Ccoord osc t

Coordinate bad-set measurability, the transverse-volume bound, and a scalar constant comparison supply the older packaged Fubini estimate used by the maximal-slice assembly.

theorem AleksandrovDifferentiability.CoordinateSliceMaximalFubiniEstimate.coordinate_bound_of_sourceMassBound {n : ℕ} {μslice : CoordinateSliceMeasureFamily n} {Cmax Ccoord osc t : ℝ} (hfubini : CoordinateSliceMaximalFubiniEstimate μslice (2 * Cmax) Ccoord osc t) (hmass : CoordinateSliceSourceMassBound μslice osc) (hmax : LocalizedMaximalEstimateStatement Cmax) (ht : 0 < t) (i : Fin n) : MeasureTheory.volume (coordinateSliceBadSet (coordinateSliceMaximalBadPredicate μslice) i t) ≤ ENNReal.ofReal (Ccoord * osc / t)

Source mass bounds plus the localized maximal estimate supply the line-fiber hypotheses needed by CoordinateSliceMaximalFubiniEstimate.

theorem AleksandrovDifferentiability.CoordinateSliceMaximalTotalBadSetEstimate.of_fubiniEstimate {n : ℕ} {u : SourceCubeSpace n → ℝ} {μslice : CoordinateSliceMeasureFamily n} {Cmax Ccoord Cmeasure t : ℝ} (hdiff : MeasureTheory.volume (sourceOpenCube n 1 \ firstOrderDifferentiabilitySet u) = 0) (hmass : CoordinateSliceSourceMassBound μslice (sourceCubeOscillation n u)) (hmax : LocalizedMaximalEstimateStatement Cmax) (ht : 0 < t) (hfubini : CoordinateSliceMaximalFubiniEstimate μslice (2 * Cmax) Ccoord (sourceCubeOscillation n u) t) (hbound : ↑n * ENNReal.ofReal (Ccoord * sourceCubeOscillation n u / t) ≤ ENNReal.ofReal (Cmeasure * sourceCubeOscillation n u / t)) : CoordinateSliceMaximalTotalBadSetEstimate u μslice Cmeasure t

Assembly from the per-coordinate Fubini estimate to the concrete localized-maximal total bad-set estimate.