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

Stieltjes coordinate-slice measures on source cubes

This file specializes the abstract coordinate-slice measure family from Cube.Maximal to the Stieltjes measures of the project-local right derivatives of coordinate-line restrictions.

noncomputable def AleksandrovDifferentiability.coordinateSliceRightDerivStieltjesMeasureFamily {n : ℕ} (u : SourceCubeSpace n → ℝ) (hmono : ∀ (i : Fin n) (y : SourceCubeSpace n), Monotone (rightDeriv (lineRestriction u y (sourceCoordinateVector i)))) : CoordinateSliceMeasureFamily n

The concrete coordinate-slice measure family obtained from Stieltjes measures of right derivatives of coordinate-line restrictions.

The monotonicity hypothesis is global on the line parameter. For the source proof this should eventually be supplied by applying the Stieltjes construction to a monotone extension of the right derivative from the source interval (-3,3).

Equations

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

theorem AleksandrovDifferentiability.CoordinateSliceSourceMassBound.of_rightDerivStieltjes {n : ℕ} {u : SourceCubeSpace n → ℝ} {hmono : ∀ (i : Fin n) (y : SourceCubeSpace n), Monotone (rightDeriv (lineRestriction u y (sourceCoordinateVector i)))} {osc : ℝ} (hmass : ∀ (i : Fin n) ⦃y : SourceCubeSpace n⦄, y ∈ sourceOpenCube n 1 → HasRightDerivStieltjesSourceMassBound (lineRestriction u y (sourceCoordinateVector i)) ⋯ osc) : CoordinateSliceSourceMassBound (coordinateSliceRightDerivStieltjesMeasureFamily u hmono) osc

Source mass bounds for the concrete right-derivative Stieltjes slices supply the abstract coordinate-slice source mass bound used by the localized maximal argument.

def AleksandrovDifferentiability.CoordinateSliceRightDerivStieltjesEndpointControl {n : ℕ} (u : SourceCubeSpace n → ℝ) (hmono : ∀ (i : Fin n) (y : SourceCubeSpace n), Monotone (rightDeriv (lineRestriction u y (sourceCoordinateVector i)))) (ρ K : ℝ) : Prop

Endpoint control for the concrete right-derivative Stieltjes slices.

Equations

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

theorem AleksandrovDifferentiability.CoordinateSliceRightDerivStieltjesEndpointControl.coordinateSliceOneDimEndpointControl {n : ℕ} {u : SourceCubeSpace n → ℝ} {hmono : ∀ (i : Fin n) (y : SourceCubeSpace n), Monotone (rightDeriv (lineRestriction u y (sourceCoordinateVector i)))} {ρ K : ℝ} (hendpoint : CoordinateSliceRightDerivStieltjesEndpointControl u hmono ρ K) : CoordinateSliceOneDimEndpointControl u (coordinateSliceRightDerivStieltjesMeasureFamily u hmono) ρ K

The concrete right-derivative Stieltjes endpoint input implies the abstract one-dimensional endpoint-control input expected by Cube.Maximal.

theorem AleksandrovDifferentiability.CoordinateSliceMaximalFubiniEstimate.coordinate_bound_of_rightDerivStieltjesMassBound {n : ℕ} {u : SourceCubeSpace n → ℝ} {hmono : ∀ (i : Fin n) (y : SourceCubeSpace n), Monotone (rightDeriv (lineRestriction u y (sourceCoordinateVector i)))} {Cmax Ccoord osc t : ℝ} (hfubini : CoordinateSliceMaximalFubiniEstimate (coordinateSliceRightDerivStieltjesMeasureFamily u hmono) (2 * Cmax) Ccoord osc t) (hmass : ∀ (i : Fin n) ⦃y : SourceCubeSpace n⦄, y ∈ sourceOpenCube n 1 → HasRightDerivStieltjesSourceMassBound (lineRestriction u y (sourceCoordinateVector i)) ⋯ osc) (hmax : LocalizedMaximalEstimateStatement Cmax) (ht : 0 < t) (i : Fin n) : MeasureTheory.volume (coordinateSliceBadSet (coordinateSliceMaximalBadPredicate (coordinateSliceRightDerivStieltjesMeasureFamily u hmono)) i t) ≤ ENNReal.ofReal (Ccoord * osc / t)

Fubini plus concrete Stieltjes source mass bounds give the per-coordinate bad-set estimate for localized maximal slices.

Source-local clamped Stieltjes slices

noncomputable def AleksandrovDifferentiability.coordinateSliceSourceRightDerivStieltjesMeasureFamily {n : ℕ} (u : SourceCubeSpace n → ℝ) (hmono : ∀ (i : Fin n) ⦃y : SourceCubeSpace n⦄, y ∈ sourceOpenCube n 1 → MonotoneOn (rightDeriv (lineRestriction u (coordinateLineBase i y) (sourceCoordinateVector i))) (Set.Icc (-2) 2)) : CoordinateSliceMeasureFamily n

Coordinate-slice measure family obtained from the source-local clamped Stieltjes measure.

Unlike coordinateSliceRightDerivStieltjesMeasureFamily, this construction only asks for monotonicity of the right derivative on the source interval [-2,2], and only for line bases in Q_1. Outside those bases the family is filled with the zero measure, which is harmless for the source bad sets.

Equations

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

noncomputable def AleksandrovDifferentiability.coordinateSliceConvexSourceRightDerivStieltjesMeasureFamily {n : ℕ} (u : SourceCubeSpace n → ℝ) (hu : ConvexOn ℝ (sourceOpenCube n 3) u) : CoordinateSliceMeasureFamily n

Source-local clamped Stieltjes slice family with the monotonicity proof supplied by ambient convexity on Q_3. This is the concrete coordinate-slice measure family intended for the convex source proof.

Equations

• AleksandrovDifferentiability.coordinateSliceConvexSourceRightDerivStieltjesMeasureFamily u hu = AleksandrovDifferentiability.coordinateSliceSourceRightDerivStieltjesMeasureFamily u ⋯

theorem AleksandrovDifferentiability.coordinateSliceConvexSourceRightDerivStieltjesMeasureFamily_Ioo_lt_top {n : ℕ} (u : SourceCubeSpace n → ℝ) (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (i : Fin n) (y : SourceCubeSpace n) (a b : ℝ) : (coordinateSliceConvexSourceRightDerivStieltjesMeasureFamily u hu i y) (Set.Ioo a b) < ⊤

Concrete convex source-local Stieltjes slices have finite mass on every bounded open interval.

def AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesMaximalBadPredicateMeasurable {n : ℕ} (u : SourceCubeSpace n → ℝ) (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ) : Prop

Product-coordinate measurability obligation for the concrete convex source-local Stieltjes maximal bad predicate.

Equations

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

def AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesSourceLocalizedMaximalMeasurable {n : ℕ} (u : SourceCubeSpace n → ℝ) (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ) : Prop

One-dimensional parameterized source-local maximal measurability for the concrete convex Stieltjes slice family.

Equations

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

def AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesSourceLocalizedMaximalMeasurableOnWindow {n : ℕ} (u : SourceCubeSpace n → ℝ) (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ) : Prop

Source-window-restricted one-dimensional maximal measurability for the concrete convex Stieltjes slice family.

Equations

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

def AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsMeasurable {n : ℕ} (u : SourceCubeSpace n → ℝ) (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ) : Prop

Interval-average-exceeds measurability for the concrete convex Stieltjes slice family.

Equations

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

def AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesMaximalBadSetMeasurable {n : ℕ} (u : SourceCubeSpace n → ℝ) (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ) : Prop

Measurability obligation for the concrete convex source-local Stieltjes maximal bad sets.

This is the source-route analytic measurability input for the Fubini step, specialized to the coordinate Stieltjes measure family supplied by convexity.

Equations

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

theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesMaximalBadPredicateMeasurable.badSetMeasurable {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {t : ℝ} (hbad : CoordinateSliceConvexSourceRightDerivStieltjesMaximalBadPredicateMeasurable u hu t) : CoordinateSliceConvexSourceRightDerivStieltjesMaximalBadSetMeasurable u hu t

Product-coordinate measurability of the concrete convex source-local Stieltjes maximal predicate gives measurability of the ambient coordinate maximal bad sets.

theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesSourceLocalizedMaximalMeasurable.badPredicateMeasurable {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {t : ℝ} (hbad : CoordinateSliceConvexSourceRightDerivStieltjesSourceLocalizedMaximalMeasurable u hu t) : CoordinateSliceConvexSourceRightDerivStieltjesMaximalBadPredicateMeasurable u hu t

Parameterized one-dimensional source-local maximal measurability implies the concrete product-coordinate maximal bad-predicate measurability.

theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesSourceLocalizedMaximalMeasurable.badSetMeasurable {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {t : ℝ} (hbad : CoordinateSliceConvexSourceRightDerivStieltjesSourceLocalizedMaximalMeasurable u hu t) : CoordinateSliceConvexSourceRightDerivStieltjesMaximalBadSetMeasurable u hu t

Parameterized one-dimensional source-local maximal measurability implies the concrete ambient coordinate maximal bad-set measurability.

theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesSourceLocalizedMaximalMeasurableOnWindow.badSetMeasurable {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {t : ℝ} (hbad : CoordinateSliceConvexSourceRightDerivStieltjesSourceLocalizedMaximalMeasurableOnWindow u hu t) : CoordinateSliceConvexSourceRightDerivStieltjesMaximalBadSetMeasurable u hu t

Source-window-restricted one-dimensional maximal measurability implies the concrete ambient coordinate maximal bad-set measurability.

theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsMeasurable.badSetMeasurable {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {t : ℝ} (havg : CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsMeasurable u hu t) : CoordinateSliceConvexSourceRightDerivStieltjesMaximalBadSetMeasurable u hu t

Interval-average-exceeds measurability implies the concrete ambient coordinate maximal bad-set measurability.

theorem AleksandrovDifferentiability.CoordinateSliceSourceMassBound.of_sourceRightDerivStieltjes {n : ℕ} {u : SourceCubeSpace n → ℝ} {hmono : ∀ (i : Fin n) ⦃y : SourceCubeSpace n⦄, y ∈ sourceOpenCube n 1 → MonotoneOn (rightDeriv (lineRestriction u (coordinateLineBase i y) (sourceCoordinateVector i))) (Set.Icc (-2) 2)} {osc : ℝ} (hmass : ∀ (i : Fin n) ⦃y : SourceCubeSpace n⦄ (hy : y ∈ sourceOpenCube n 1), HasSourceRightDerivStieltjesSourceMassBound (lineRestriction u (coordinateLineBase i y) (sourceCoordinateVector i)) ⋯ osc) : CoordinateSliceSourceMassBound (coordinateSliceSourceRightDerivStieltjesMeasureFamily u hmono) osc

Source mass bounds for the clamped source-local Stieltjes slices supply the abstract coordinate-slice source mass bound used by the localized maximal argument.

theorem AleksandrovDifferentiability.CoordinateSliceSourceMassBound.of_sourceRightDerivStieltjesJumpBound {n : ℕ} {u : SourceCubeSpace n → ℝ} {hmono : ∀ (i : Fin n) ⦃y : SourceCubeSpace n⦄, y ∈ sourceOpenCube n 1 → MonotoneOn (rightDeriv (lineRestriction u (coordinateLineBase i y) (sourceCoordinateVector i))) (Set.Icc (-2) 2)} {osc : ℝ} (hjump : ∀ (i : Fin n) ⦃y : SourceCubeSpace n⦄ (hy : y ∈ sourceOpenCube n 1), sourceRightDerivStieltjesSourceJump (lineRestriction u (coordinateLineBase i y) (sourceCoordinateVector i)) ⋯ ≤ 2 * osc) : CoordinateSliceSourceMassBound (coordinateSliceSourceRightDerivStieltjesMeasureFamily u hmono) osc

Source jump bounds for the clamped source-local Stieltjes slices supply the abstract coordinate-slice source mass bound.

theorem AleksandrovDifferentiability.CoordinateSliceSourceMassBound.of_sourceRightDerivStieltjesAbsFunctionBounds {n : ℕ} {u : SourceCubeSpace n → ℝ} {hmono : ∀ (i : Fin n) ⦃y : SourceCubeSpace n⦄, y ∈ sourceOpenCube n 1 → MonotoneOn (rightDeriv (lineRestriction u (coordinateLineBase i y) (sourceCoordinateVector i))) (Set.Icc (-2) 2)} {osc : ℝ} (hlower : ∀ (i : Fin n) ⦃y : SourceCubeSpace n⦄ (hy : y ∈ sourceOpenCube n 1), -osc ≤ ↑(sourceRightDerivStieltjesSecondDerivativeFunction (lineRestriction u (coordinateLineBase i y) (sourceCoordinateVector i)) ⋯) (-2)) (hupper : ∀ (i : Fin n) ⦃y : SourceCubeSpace n⦄ (hy : y ∈ sourceOpenCube n 1), Function.leftLim (↑(sourceRightDerivStieltjesSecondDerivativeFunction (lineRestriction u (coordinateLineBase i y) (sourceCoordinateVector i)) ⋯)) 2 ≤ osc) : CoordinateSliceSourceMassBound (coordinateSliceSourceRightDerivStieltjesMeasureFamily u hmono) osc

Symmetric endpoint bounds for the clamped Stieltjes functions of every coordinate slice imply the abstract coordinate-slice source mass bound.

theorem AleksandrovDifferentiability.CoordinateSliceSourceMassBound.of_sourceRightDerivBounds {n : ℕ} {u : SourceCubeSpace n → ℝ} {hmono : ∀ (i : Fin n) ⦃y : SourceCubeSpace n⦄, y ∈ sourceOpenCube n 1 → MonotoneOn (rightDeriv (lineRestriction u (coordinateLineBase i y) (sourceCoordinateVector i))) (Set.Icc (-2) 2)} {osc : ℝ} (hlower : ∀ (i : Fin n) ⦃y : SourceCubeSpace n⦄, y ∈ sourceOpenCube n 1 → -osc ≤ rightDeriv (lineRestriction u (coordinateLineBase i y) (sourceCoordinateVector i)) (-2)) (hupper : ∀ (i : Fin n) ⦃y : SourceCubeSpace n⦄, y ∈ sourceOpenCube n 1 → rightDeriv (lineRestriction u (coordinateLineBase i y) (sourceCoordinateVector i)) 2 ≤ osc) : CoordinateSliceSourceMassBound (coordinateSliceSourceRightDerivStieltjesMeasureFamily u hmono) osc

Endpoint bounds for the ordinary right derivatives of every coordinate slice imply the abstract coordinate-slice source mass bound.

theorem AleksandrovDifferentiability.CoordinateSliceSourceMassBound.of_sourceRightDerivConvexSecantBounds {n : ℕ} {u : SourceCubeSpace n → ℝ} {hmono : ∀ (i : Fin n) ⦃y : SourceCubeSpace n⦄, y ∈ sourceOpenCube n 1 → MonotoneOn (rightDeriv (lineRestriction u (coordinateLineBase i y) (sourceCoordinateVector i))) (Set.Icc (-2) 2)} {osc : ℝ} (hconv : ∀ (i : Fin n) ⦃y : SourceCubeSpace n⦄, y ∈ sourceOpenCube n 1 → ConvexOn ℝ (Set.Ioo (-3) 3) (lineRestriction u (coordinateLineBase i y) (sourceCoordinateVector i))) (hleft : ∀ (i : Fin n) ⦃y : SourceCubeSpace n⦄, y ∈ sourceOpenCube n 1 → ∀ (ε : ℝ), 0 < ε → ∃ s ∈ Set.Ioo (-3) (-2), -osc - ε ≤ slope (lineRestriction u (coordinateLineBase i y) (sourceCoordinateVector i)) s (-2)) (hright : ∀ (i : Fin n) ⦃y : SourceCubeSpace n⦄, y ∈ sourceOpenCube n 1 → ∀ (ε : ℝ), 0 < ε → ∃ s ∈ Set.Ioo 2 3, slope (lineRestriction u (coordinateLineBase i y) (sourceCoordinateVector i)) 2 s ≤ osc + ε) : CoordinateSliceSourceMassBound (coordinateSliceSourceRightDerivStieltjesMeasureFamily u hmono) osc

Convexity of each coordinate restriction plus endpoint secant bounds supply the abstract coordinate-slice source mass bound. This is the slice-level form of the source proof's one-dimensional oscillation-to-mass estimate, before the oscillation hypotheses are proved from the cube bound.

theorem AleksandrovDifferentiability.CoordinateSliceSourceMassBound.of_convexSourceRightDerivStieltjesSecantBounds {n : ℕ} {u : SourceCubeSpace n → ℝ} {osc : ℝ} (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (hleft : ∀ (i : Fin n) ⦃y : SourceCubeSpace n⦄, y ∈ sourceOpenCube n 1 → ∀ (ε : ℝ), 0 < ε → ∃ s ∈ Set.Ioo (-3) (-2), -osc - ε ≤ slope (lineRestriction u (coordinateLineBase i y) (sourceCoordinateVector i)) s (-2)) (hright : ∀ (i : Fin n) ⦃y : SourceCubeSpace n⦄, y ∈ sourceOpenCube n 1 → ∀ (ε : ℝ), 0 < ε → ∃ s ∈ Set.Ioo 2 3, slope (lineRestriction u (coordinateLineBase i y) (sourceCoordinateVector i)) 2 s ≤ osc + ε) : CoordinateSliceSourceMassBound (coordinateSliceConvexSourceRightDerivStieltjesMeasureFamily u hu) osc

Ambient convexity plus endpoint secant bounds supply the source mass bound for the concrete convex source-local Stieltjes slice family.

theorem AleksandrovDifferentiability.coordinateLine_pairwiseSub_le_sourceCubeOscillation_of_boundedOn {n : ℕ} {u : SourceCubeSpace n → ℝ} (hbounded : BoundedOn (sourceOpenCube n 3) u) (i : Fin n) {y : SourceCubeSpace n} (hy : y ∈ sourceOpenCube n 1) ⦃s r : ℝ⦄ (hs : s ∈ Set.Ioo (-3) 3) (hr : r ∈ Set.Ioo (-3) 3) : lineRestriction u (coordinateLineBase i y) (sourceCoordinateVector i) r - lineRestriction u (coordinateLineBase i y) (sourceCoordinateVector i) s ≤ sourceCubeOscillation n u

Along every coordinate slice over a base in Q_1, the source-cube oscillation bounds all one-dimensional value differences on the source interval (-3,3).

theorem AleksandrovDifferentiability.CoordinateSliceSourceMassBound.of_convexSourceRightDerivStieltjes_boundedOn {n : ℕ} {u : SourceCubeSpace n → ℝ} (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (hbounded : BoundedOn (sourceOpenCube n 3) u) : CoordinateSliceSourceMassBound (coordinateSliceConvexSourceRightDerivStieltjesMeasureFamily u hu) (sourceCubeOscillation n u)

Ambient convexity and boundedness on Q_3 supply the source mass bound for the concrete convex source-local Stieltjes slice family.