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

Concrete Stieltjes endpoint and mass controls

def AleksandrovDifferentiability.CoordinateSliceSourceRightDerivStieltjesEndpointControl {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)) (ρ K : ℝ) : Prop

Each coordinate slice satisfies the source Stieltjes endpoint remainder estimates.

Equations

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

def AleksandrovDifferentiability.CoordinateSliceSourceRightDerivStieltjesEndpointIdentities {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)) (ρ : ℝ) : Prop

Exact endpoint identities for the clamped source-local right-derivative Stieltjes slices.

Equations

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

def AleksandrovDifferentiability.CoordinateSliceSourceRightDerivStieltjesEndpointBounds {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)) (ρ : ℝ) : Prop

Endpoint comparison bounds for the clamped source-local right-derivative Stieltjes slices.

Equations

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

theorem AleksandrovDifferentiability.CoordinateSliceSourceRightDerivStieltjesEndpointIdentities.endpointBounds {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)} {ρ : ℝ} (hident : CoordinateSliceSourceRightDerivStieltjesEndpointIdentities u hmono ρ) : CoordinateSliceSourceRightDerivStieltjesEndpointBounds u hmono ρ

Exact endpoint identities imply endpoint comparison bounds slicewise.

theorem AleksandrovDifferentiability.CoordinateSliceSourceRightDerivStieltjesEndpointBounds.endpointControl {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)} {ρ : ℝ} (hbounds : CoordinateSliceSourceRightDerivStieltjesEndpointBounds u hmono ρ) (hconv : ∀ ⦃x : SourceCubeSpace n⦄, x ∈ sourceOpenCube n 1 → DifferentiableAt ℝ u x → ∀ (i : Fin n), ConvexOn ℝ (Set.Ioo (-3) 3) (lineRestriction u (coordinateLineBase i x) (sourceCoordinateVector i))) (hρ_le_one : ρ ≤ 1) : CoordinateSliceSourceRightDerivStieltjesEndpointControl u hmono ρ 2

Slice-level endpoint comparisons imply slice-level endpoint control with constant 2, provided the coordinate slices are convex on the source interval.

def AleksandrovDifferentiability.CoordinateSliceSourceRightDerivStieltjesSymmetricRemainderBound {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)) (ρ : ℝ) : Prop

Slice-level symmetric-remainder estimate for the clamped source-local right-derivative Stieltjes measures. This is the remaining one-dimensional analytic input before endpoint control.

Equations

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

theorem AleksandrovDifferentiability.CoordinateSliceSourceRightDerivStieltjesSymmetricRemainderBound.endpointControl {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)} {ρ : ℝ} (hrem : CoordinateSliceSourceRightDerivStieltjesSymmetricRemainderBound u hmono ρ) (hρ_le_one : ρ ≤ 1) : CoordinateSliceSourceRightDerivStieltjesEndpointControl u hmono ρ 2

Slice-level symmetric-remainder estimates imply slice-level endpoint control with constant 2.

def AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesEndpointControl {n : ℕ} (u : SourceCubeSpace n → ℝ) (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (ρ K : ℝ) : Prop

Endpoint control for the concrete convex source-local Stieltjes slice family.

Equations

• AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesEndpointControl u hu ρ K = AleksandrovDifferentiability.CoordinateSliceSourceRightDerivStieltjesEndpointControl u ⋯ ρ K

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

Exact endpoint identities for the concrete convex source-local Stieltjes slice family.

Equations

• AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesEndpointIdentities u hu ρ = AleksandrovDifferentiability.CoordinateSliceSourceRightDerivStieltjesEndpointIdentities u ⋯ ρ

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

Endpoint comparison bounds for the concrete convex source-local Stieltjes slice family.

Equations

• AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesEndpointBounds u hu ρ = AleksandrovDifferentiability.CoordinateSliceSourceRightDerivStieltjesEndpointBounds u ⋯ ρ

theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesEndpointIdentities.of_convex {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {ρ : ℝ} (hρ_le_one : ρ ≤ 1) : CoordinateSliceConvexSourceRightDerivStieltjesEndpointIdentities u hu ρ

Ambient convexity supplies the concrete slicewise endpoint identities.

theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesEndpointIdentities.endpointBounds {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {ρ : ℝ} (hident : CoordinateSliceConvexSourceRightDerivStieltjesEndpointIdentities u hu ρ) : CoordinateSliceConvexSourceRightDerivStieltjesEndpointBounds u hu ρ

Concrete convex endpoint identities imply concrete endpoint comparison bounds.

theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesEndpointBounds.endpointControl {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {ρ : ℝ} (hbounds : CoordinateSliceConvexSourceRightDerivStieltjesEndpointBounds u hu ρ) (hρ_le_one : ρ ≤ 1) : CoordinateSliceConvexSourceRightDerivStieltjesEndpointControl u hu ρ 2

Concrete convex endpoint comparisons imply concrete endpoint control with constant 2.

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

Symmetric-remainder estimates for the concrete convex source-local Stieltjes slice family.

Equations

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

theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesSymmetricRemainderBound.endpointControl {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {ρ : ℝ} (hrem : CoordinateSliceConvexSourceRightDerivStieltjesSymmetricRemainderBound u hu ρ) (hρ_le_one : ρ ≤ 1) : CoordinateSliceConvexSourceRightDerivStieltjesEndpointControl u hu ρ 2

Concrete convex source-local symmetric-remainder estimates imply concrete endpoint control with constant 2.

theorem AleksandrovDifferentiability.CoordinateSliceSourceRightDerivStieltjesEndpointControl.coordinateSliceOneDimEndpointControl {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)} {ρ K : ℝ} (hendpoint : CoordinateSliceSourceRightDerivStieltjesEndpointControl u hmono ρ K) : CoordinateSliceOneDimEndpointControl u (coordinateSliceSourceRightDerivStieltjesMeasureFamily u hmono) ρ K

The clamped source-local Stieltjes endpoint input implies the abstract one-dimensional endpoint-control input expected by Cube.Maximal.

theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesEndpointControl.of_convex {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {ρ : ℝ} (hρ_le_one : ρ ≤ 1) : CoordinateSliceConvexSourceRightDerivStieltjesEndpointControl u hu ρ 2

Ambient convexity supplies concrete slicewise endpoint control with constant 2.

theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesEndpointControl.coordinateSliceOneDimEndpointControl {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {ρ K : ℝ} (hendpoint : CoordinateSliceConvexSourceRightDerivStieltjesEndpointControl u hu ρ K) : CoordinateSliceOneDimEndpointControl u (coordinateSliceConvexSourceRightDerivStieltjesMeasureFamily u hu) ρ K

The concrete convex source-local Stieltjes endpoint input implies the abstract one-dimensional endpoint-control input expected by Cube.Maximal.

theorem AleksandrovDifferentiability.CoordinateSliceMaximalFubiniEstimate.coordinate_bound_of_sourceRightDerivStieltjesMassBound {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)} {Cmax Ccoord osc t : ℝ} (hfubini : CoordinateSliceMaximalFubiniEstimate (coordinateSliceSourceRightDerivStieltjesMeasureFamily u hmono) (2 * Cmax) Ccoord osc t) (hmass : ∀ (i : Fin n) ⦃y : SourceCubeSpace n⦄ (hy : y ∈ sourceOpenCube n 1), HasSourceRightDerivStieltjesSourceMassBound (lineRestriction u (coordinateLineBase i y) (sourceCoordinateVector i)) ⋯ osc) (hmax : LocalizedMaximalEstimateStatement Cmax) (ht : 0 < t) (i : Fin n) : MeasureTheory.volume (coordinateSliceBadSet (coordinateSliceMaximalBadPredicate (coordinateSliceSourceRightDerivStieltjesMeasureFamily u hmono)) i t) ≤ ENNReal.ofReal (Ccoord * osc / t)

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

theorem AleksandrovDifferentiability.CoordinateSliceMaximalFubiniEstimate.coordinate_bound_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)} {Cmax Ccoord osc t : ℝ} (hfubini : CoordinateSliceMaximalFubiniEstimate (coordinateSliceSourceRightDerivStieltjesMeasureFamily u hmono) (2 * Cmax) Ccoord osc t) (hjump : ∀ (i : Fin n) ⦃y : SourceCubeSpace n⦄ (hy : y ∈ sourceOpenCube n 1), sourceRightDerivStieltjesSourceJump (lineRestriction u (coordinateLineBase i y) (sourceCoordinateVector i)) ⋯ ≤ 2 * osc) (hmax : LocalizedMaximalEstimateStatement Cmax) (ht : 0 < t) (i : Fin n) : MeasureTheory.volume (coordinateSliceBadSet (coordinateSliceMaximalBadPredicate (coordinateSliceSourceRightDerivStieltjesMeasureFamily u hmono)) i t) ≤ ENNReal.ofReal (Ccoord * osc / t)

Fubini plus clamped source-local Stieltjes source jump bounds give the per-coordinate bad-set estimate for localized maximal slices.

theorem AleksandrovDifferentiability.CoordinateSliceMaximalFubiniEstimate.coordinate_bound_of_sourceRightDerivStieltjesAbsBounds {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)} {Cmax Ccoord osc t : ℝ} (hfubini : CoordinateSliceMaximalFubiniEstimate (coordinateSliceSourceRightDerivStieltjesMeasureFamily u hmono) (2 * Cmax) Ccoord osc t) (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) (hmax : LocalizedMaximalEstimateStatement Cmax) (ht : 0 < t) (i : Fin n) : MeasureTheory.volume (coordinateSliceBadSet (coordinateSliceMaximalBadPredicate (coordinateSliceSourceRightDerivStieltjesMeasureFamily u hmono)) i t) ≤ ENNReal.ofReal (Ccoord * osc / t)

Fubini plus symmetric endpoint bounds for clamped source-local Stieltjes functions give the per-coordinate bad-set estimate for localized maximal slices.

theorem AleksandrovDifferentiability.CoordinateSliceMaximalFubiniEstimate.coordinate_bound_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)} {Cmax Ccoord osc t : ℝ} (hfubini : CoordinateSliceMaximalFubiniEstimate (coordinateSliceSourceRightDerivStieltjesMeasureFamily u hmono) (2 * Cmax) Ccoord osc t) (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) (hmax : LocalizedMaximalEstimateStatement Cmax) (ht : 0 < t) (i : Fin n) : MeasureTheory.volume (coordinateSliceBadSet (coordinateSliceMaximalBadPredicate (coordinateSliceSourceRightDerivStieltjesMeasureFamily u hmono)) i t) ≤ ENNReal.ofReal (Ccoord * osc / t)

Fubini plus endpoint bounds for the ordinary right derivatives of clamped source-local slices give the per-coordinate bad-set estimate for localized maximal slices.

theorem AleksandrovDifferentiability.CoordinateSliceMaximalFubiniEstimate.coordinate_bound_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)} {Cmax Ccoord osc t : ℝ} (hfubini : CoordinateSliceMaximalFubiniEstimate (coordinateSliceSourceRightDerivStieltjesMeasureFamily u hmono) (2 * Cmax) Ccoord osc t) (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 + ε) (hmax : LocalizedMaximalEstimateStatement Cmax) (ht : 0 < t) (i : Fin n) : MeasureTheory.volume (coordinateSliceBadSet (coordinateSliceMaximalBadPredicate (coordinateSliceSourceRightDerivStieltjesMeasureFamily u hmono)) i t) ≤ ENNReal.ofReal (Ccoord * osc / t)

Fubini plus convexity and endpoint secant bounds for clamped source-local slices give the per-coordinate bad-set estimate for localized maximal slices.

theorem AleksandrovDifferentiability.CoordinateSliceMaximalTotalBadSetEstimate.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)} {Cmax Ccoord Cmeasure t : ℝ} (hdiff : MeasureTheory.volume (sourceOpenCube n 1 \ firstOrderDifferentiabilitySet u) = 0) (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), -sourceCubeOscillation n u - ε ≤ 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 ≤ sourceCubeOscillation n u + ε) (hmax : LocalizedMaximalEstimateStatement Cmax) (ht : 0 < t) (hfubini : CoordinateSliceMaximalFubiniEstimate (coordinateSliceSourceRightDerivStieltjesMeasureFamily u hmono) (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 (coordinateSliceSourceRightDerivStieltjesMeasureFamily u hmono) Cmeasure t

Total bad-set estimate for clamped source-local Stieltjes slices, using convexity and endpoint secant bounds for the coordinate restrictions to supply the source mass estimate.

theorem AleksandrovDifferentiability.CoordinateSliceMaximalTotalBadSetEstimate.of_convexSourceRightDerivStieltjesSecantBounds {n : ℕ} {u : SourceCubeSpace n → ℝ} {Cmax Ccoord Cmeasure t : ℝ} (hdiff : MeasureTheory.volume (sourceOpenCube n 1 \ firstOrderDifferentiabilitySet u) = 0) (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (hleft : ∀ (i : Fin n) ⦃y : SourceCubeSpace n⦄, y ∈ sourceOpenCube n 1 → ∀ (ε : ℝ), 0 < ε → ∃ s ∈ Set.Ioo (-3) (-2), -sourceCubeOscillation n u - ε ≤ 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 ≤ sourceCubeOscillation n u + ε) (hmax : LocalizedMaximalEstimateStatement Cmax) (ht : 0 < t) (hfubini : CoordinateSliceMaximalFubiniEstimate (coordinateSliceConvexSourceRightDerivStieltjesMeasureFamily u hu) (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 (coordinateSliceConvexSourceRightDerivStieltjesMeasureFamily u hu) Cmeasure t

Total bad-set estimate for the concrete convex source-local Stieltjes slice family. Ambient convexity supplies slice convexity and right-derivative monotonicity; the remaining assumptions are the source endpoint secant estimates and the Fubini/weak-type bookkeeping.

theorem AleksandrovDifferentiability.CoordinateSliceMaximalTotalBadSetEstimate.of_convexSourceRightDerivStieltjes_boundedOn {n : ℕ} {u : SourceCubeSpace n → ℝ} {Cmax Ccoord Cmeasure t : ℝ} (hdiff : MeasureTheory.volume (sourceOpenCube n 1 \ firstOrderDifferentiabilitySet u) = 0) (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (hbounded : BoundedOn (sourceOpenCube n 3) u) (hmax : LocalizedMaximalEstimateStatement Cmax) (ht : 0 < t) (hfubini : CoordinateSliceMaximalFubiniEstimate (coordinateSliceConvexSourceRightDerivStieltjesMeasureFamily u hu) (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 (coordinateSliceConvexSourceRightDerivStieltjesMeasureFamily u hu) Cmeasure t

Total bad-set estimate for the concrete convex source-local Stieltjes slice family from ambient convexity, boundedness, the localized maximal theorem, and the Fubini bookkeeping.

theorem AleksandrovDifferentiability.CoordinateSliceMaximalTotalBadSetEstimate.of_convexStieltjes_boundedOn_measureConstant {n : ℕ} {u : SourceCubeSpace n → ℝ} {Cmax Ccoord Cmeasure t : ℝ} (hdiff : MeasureTheory.volume (sourceOpenCube n 1 \ firstOrderDifferentiabilitySet u) = 0) (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (hbounded : BoundedOn (sourceOpenCube n 3) u) (hmax : LocalizedMaximalEstimateStatement Cmax) (ht : 0 < t) (hfubini : CoordinateSliceMaximalFubiniEstimate (coordinateSliceConvexSourceRightDerivStieltjesMeasureFamily u hu) (2 * Cmax) Ccoord (sourceCubeOscillation n u) t) (hmeasure : ↑n * Ccoord ≤ Cmeasure) : CoordinateSliceMaximalTotalBadSetEstimate u (coordinateSliceConvexSourceRightDerivStieltjesMeasureFamily u hu) Cmeasure t

Total bad-set estimate for the concrete convex source-local Stieltjes slice family from ambient convexity, boundedness, the localized maximal theorem, and the Fubini bookkeeping, with the finite-union constant supplied as a real coefficient inequality.