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

Source-route wrappers from Stieltjes measurability reductions

This file packages the countable-interval and endpoint measurability reductions into the source-local upper-contact estimate statement interfaces.

@[reducible, inline]

abbrev AleksandrovDifferentiability.ConvexStieltjesCountableIntervalReverseCover {n : ℕ} (u : SourceCubeSpace n → ℝ) (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (a b : ℕ → ℝ) (t : ℝ) : Prop

Short wrapper-file name for the concrete convex Stieltjes countable-interval reverse-cover obligation.

Equations

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

@[reducible, inline]

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

Short wrapper-file name for the concrete convex Stieltjes rational-refinement obligation.

Equations

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

@[reducible, inline]

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

Short wrapper-file name for the concrete convex Stieltjes inner-rational-refinement obligation.

Equations

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

@[reducible, inline]

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

Short wrapper-file name for the concrete convex Stieltjes sequential inner-rational approximation obligation.

Equations

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

@[reducible, inline]

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

Short wrapper-file name for the concrete convex Stieltjes sequential inner-rational mass approximation obligation.

Equations

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

Packaged source-route wrappers from endpoint measurability

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateDecompositionStatement.of_convexStieltjes_of_countableIntervals_with_chosenMeasureConstant {n : ℕ} {Cmax Ctrans Ccoord Cmeasure ρ : ℝ} {a b : ℕ → ℝ} (hCmeasure_nonneg : 0 ≤ Cmeasure) (hρ : 0 < ρ) (hρ_le_one : ρ ≤ 1) (hmeasure : ↑n * Ccoord ≤ Cmeasure) (hCtrans_nonneg : 0 ≤ Ctrans) (hAmeasure : ∀ (i : Fin n), MeasureTheory.volume (sourceTransverseOpenCube i 1) ≤ ENNReal.ofReal Ctrans) (hfubiniConst : Ctrans * (2 * Cmax) ≤ Ccoord) (hmax : LocalizedMaximalEstimateStatement Cmax) (hfixed : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableIntervalMeasurable u hu a b t) (hcover : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableIntervalCover u hu a b t) : ConvexUpperContactEstimateDecompositionStatement n

Concrete convex source-local Stieltjes decomposition route from a countable fixed-interval representation of the interval-average-exceeds set.

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateDecompositionStatement.of_convexStieltjes_of_countableIntervalReverseCover_with_chosenMeasureConstant {n : ℕ} {Cmax Ctrans Ccoord Cmeasure ρ : ℝ} {a b : ℕ → ℝ} (hadm : SourceAdmissibleIntervalEnumeration a b) (hCmeasure_nonneg : 0 ≤ Cmeasure) (hρ : 0 < ρ) (hρ_le_one : ρ ≤ 1) (hmeasure : ↑n * Ccoord ≤ Cmeasure) (hCtrans_nonneg : 0 ≤ Ctrans) (hAmeasure : ∀ (i : Fin n), MeasureTheory.volume (sourceTransverseOpenCube i 1) ≤ ENNReal.ofReal Ctrans) (hfubiniConst : Ctrans * (2 * Cmax) ≤ Ccoord) (hmax : LocalizedMaximalEstimateStatement Cmax) (hfixed : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableIntervalMeasurable u hu a b t) (hreverse : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → ConvexStieltjesCountableIntervalReverseCover u hu a b t) : ConvexUpperContactEstimateDecompositionStatement n

Concrete convex source-local Stieltjes decomposition route from a countable fixed-interval family whose reverse-cover direction has been proved.

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateDecompositionStatement.of_convexStieltjes_of_rationalRefinement_with_chosenMeasureConstant {n : ℕ} {Cmax Ctrans Ccoord Cmeasure ρ : ℝ} {a b : ℕ → ℝ} (henum : SourceRationalIntervalEnumeration a b) (hCmeasure_nonneg : 0 ≤ Cmeasure) (hρ : 0 < ρ) (hρ_le_one : ρ ≤ 1) (hmeasure : ↑n * Ccoord ≤ Cmeasure) (hCtrans_nonneg : 0 ≤ Ctrans) (hAmeasure : ∀ (i : Fin n), MeasureTheory.volume (sourceTransverseOpenCube i 1) ≤ ENNReal.ofReal Ctrans) (hfubiniConst : Ctrans * (2 * Cmax) ≤ Ccoord) (hmax : LocalizedMaximalEstimateStatement Cmax) (hfixed : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableIntervalMeasurable u hu a b t) (hrefine : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → ConvexStieltjesAverageExceedsRationalRefinement u hu t) : ConvexUpperContactEstimateDecompositionStatement n

Concrete convex source-local Stieltjes decomposition route from rational refinement of source-local average witnesses.

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateDecompositionStatement.of_convexStieltjes_of_innerRationalRefinement_with_chosenMeasureConstant {n : ℕ} {Cmax Ctrans Ccoord Cmeasure ρ : ℝ} {a b : ℕ → ℝ} (henum : SourceRationalIntervalEnumeration a b) (hCmeasure_nonneg : 0 ≤ Cmeasure) (hρ : 0 < ρ) (hρ_le_one : ρ ≤ 1) (hmeasure : ↑n * Ccoord ≤ Cmeasure) (hCtrans_nonneg : 0 ≤ Ctrans) (hAmeasure : ∀ (i : Fin n), MeasureTheory.volume (sourceTransverseOpenCube i 1) ≤ ENNReal.ofReal Ctrans) (hfubiniConst : Ctrans * (2 * Cmax) ≤ Ccoord) (hmax : LocalizedMaximalEstimateStatement Cmax) (hfixed : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableIntervalMeasurable u hu a b t) (hrefine : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → ConvexStieltjesAverageExceedsInnerRationalRefinement u hu t) : ConvexUpperContactEstimateDecompositionStatement n

Concrete convex source-local Stieltjes decomposition route from inner-rational refinement of source-local average witnesses.

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateDecompositionStatement.of_convexStieltjes_of_innerRationalTendsto_with_chosenMeasureConstant {n : ℕ} {Cmax Ctrans Ccoord Cmeasure ρ : ℝ} {a b : ℕ → ℝ} (henum : SourceRationalIntervalEnumeration a b) (hCmeasure_nonneg : 0 ≤ Cmeasure) (hρ : 0 < ρ) (hρ_le_one : ρ ≤ 1) (hmeasure : ↑n * Ccoord ≤ Cmeasure) (hCtrans_nonneg : 0 ≤ Ctrans) (hAmeasure : ∀ (i : Fin n), MeasureTheory.volume (sourceTransverseOpenCube i 1) ≤ ENNReal.ofReal Ctrans) (hfubiniConst : Ctrans * (2 * Cmax) ≤ Ccoord) (hmax : LocalizedMaximalEstimateStatement Cmax) (hfixed : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableIntervalMeasurable u hu a b t) (happrox : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → ConvexStieltjesAverageExceedsInnerRationalTendsto u hu t) : ConvexUpperContactEstimateDecompositionStatement n

Concrete convex source-local Stieltjes decomposition route from sequential inner-rational average approximation.

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateDecompositionStatement.of_convexStieltjes_of_innerRationalMassTendsto_with_chosenMeasureConstant {n : ℕ} {Cmax Ctrans Ccoord Cmeasure ρ : ℝ} {a b : ℕ → ℝ} (henum : SourceRationalIntervalEnumeration a b) (hCmeasure_nonneg : 0 ≤ Cmeasure) (hρ : 0 < ρ) (hρ_le_one : ρ ≤ 1) (hmeasure : ↑n * Ccoord ≤ Cmeasure) (hCtrans_nonneg : 0 ≤ Ctrans) (hAmeasure : ∀ (i : Fin n), MeasureTheory.volume (sourceTransverseOpenCube i 1) ≤ ENNReal.ofReal Ctrans) (hfubiniConst : Ctrans * (2 * Cmax) ≤ Ccoord) (hmax : LocalizedMaximalEstimateStatement Cmax) (hfixed : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableIntervalMeasurable u hu a b t) (hmassApprox : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → ConvexStieltjesAverageExceedsInnerRationalMassTendsto u hu t) : ConvexUpperContactEstimateDecompositionStatement n

Concrete convex source-local Stieltjes decomposition route from sequential inner-rational mass approximation.

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateDecompositionStatement.of_convexStieltjes_of_averageIntervalMaps_with_chosenMeasureConstant {n : ℕ} {Cmax Ctrans Ccoord Cmeasure ρ : ℝ} {a b : ℕ → ℝ} (hCmeasure_nonneg : 0 ≤ Cmeasure) (hρ : 0 < ρ) (hρ_le_one : ρ ≤ 1) (hmeasure : ↑n * Ccoord ≤ Cmeasure) (hCtrans_nonneg : 0 ≤ Ctrans) (hAmeasure : ∀ (i : Fin n), MeasureTheory.volume (sourceTransverseOpenCube i 1) ≤ ENNReal.ofReal Ctrans) (hfubiniConst : Ctrans * (2 * Cmax) ≤ Ccoord) (hmax : LocalizedMaximalEstimateStatement Cmax) (havg : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → CoordinateSliceConvexSourceRightDerivStieltjesFixedIntervalAverageMeasurable u hu a b) (hcover : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableIntervalCover u hu a b t) : ConvexUpperContactEstimateDecompositionStatement n

Concrete convex source-local Stieltjes decomposition route from measurable fixed-interval average maps and a countable fixed-interval representation of the interval-average-exceeds set.

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateDecompositionStatement.of_convexStieltjes_of_endpointAverageMaps_with_chosenMeasureConstant {n : ℕ} {Cmax Ctrans Ccoord Cmeasure ρ : ℝ} {a b : ℕ → ℝ} (hab : ∀ (k : ℕ), a k < b k) (hCmeasure_nonneg : 0 ≤ Cmeasure) (hρ : 0 < ρ) (hρ_le_one : ρ ≤ 1) (hmeasure : ↑n * Ccoord ≤ Cmeasure) (hCtrans_nonneg : 0 ≤ Ctrans) (hAmeasure : ∀ (i : Fin n), MeasureTheory.volume (sourceTransverseOpenCube i 1) ≤ ENNReal.ofReal Ctrans) (hfubiniConst : Ctrans * (2 * Cmax) ≤ Ccoord) (hmax : LocalizedMaximalEstimateStatement Cmax) (hend : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → CoordinateSliceConvexSourceRightDerivStieltjesEndpointAverageMeasurable u hu a b) (hcover : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableIntervalCover u hu a b t) : ConvexUpperContactEstimateDecompositionStatement n

Concrete convex source-local Stieltjes decomposition route from measurable endpoint expressions and a countable fixed-interval representation of the interval-average-exceeds set.

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateDecompositionStatement.of_convexStieltjes_of_endpointValueLeftLimit_with_chosenMeasureConstant {n : ℕ} {Cmax Ctrans Ccoord Cmeasure ρ : ℝ} {a b : ℕ → ℝ} (hab : ∀ (k : ℕ), a k < b k) (hCmeasure_nonneg : 0 ≤ Cmeasure) (hρ : 0 < ρ) (hρ_le_one : ρ ≤ 1) (hmeasure : ↑n * Ccoord ≤ Cmeasure) (hCtrans_nonneg : 0 ≤ Ctrans) (hAmeasure : ∀ (i : Fin n), MeasureTheory.volume (sourceTransverseOpenCube i 1) ≤ ENNReal.ofReal Ctrans) (hfubiniConst : Ctrans * (2 * Cmax) ≤ Ccoord) (hmax : LocalizedMaximalEstimateStatement Cmax) (hleft : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → CoordinateSliceConvexSourceRightDerivStieltjesEndpointLeftLimitMeasurable u hu b) (hvalue : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → CoordinateSliceConvexSourceRightDerivStieltjesEndpointValueMeasurable u hu a) (hcover : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableIntervalCover u hu a b t) : ConvexUpperContactEstimateDecompositionStatement n

Concrete convex source-local Stieltjes decomposition route from measurable endpoint values, measurable endpoint left limits, and a countable fixed-interval representation of the interval-average-exceeds set.

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateStatement.of_convexSourceRightDerivStieltjes_of_countableIntervals_with_chosenMeasureConstant {n : ℕ} {Cmax Ctrans Ccoord Cmeasure ρ : ℝ} {a b : ℕ → ℝ} (hCmeasure_nonneg : 0 ≤ Cmeasure) (hρ : 0 < ρ) (hρ_le_one : ρ ≤ 1) (hmeasure : ↑n * Ccoord ≤ Cmeasure) (hCtrans_nonneg : 0 ≤ Ctrans) (hAmeasure : ∀ (i : Fin n), MeasureTheory.volume (sourceTransverseOpenCube i 1) ≤ ENNReal.ofReal Ctrans) (hfubiniConst : Ctrans * (2 * Cmax) ≤ Ccoord) (hmax : LocalizedMaximalEstimateStatement Cmax) (hfixed : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableIntervalMeasurable u hu a b t) (hcover : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableIntervalCover u hu a b t) : ConvexUpperContactEstimateStatement n

Packaged upper-contact estimate from a countable fixed-interval representation of the concrete convex source-local Stieltjes interval-average-exceeds sets.

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateStatement.of_convexSourceRightDerivStieltjes_of_averageMaps_with_chosenMeasureConstant {n : ℕ} {Cmax Ctrans Ccoord Cmeasure ρ : ℝ} {a b : ℕ → ℝ} (hCmeasure_nonneg : 0 ≤ Cmeasure) (hρ : 0 < ρ) (hρ_le_one : ρ ≤ 1) (hmeasure : ↑n * Ccoord ≤ Cmeasure) (hCtrans_nonneg : 0 ≤ Ctrans) (hAmeasure : ∀ (i : Fin n), MeasureTheory.volume (sourceTransverseOpenCube i 1) ≤ ENNReal.ofReal Ctrans) (hfubiniConst : Ctrans * (2 * Cmax) ≤ Ccoord) (hmax : LocalizedMaximalEstimateStatement Cmax) (havg : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → CoordinateSliceConvexSourceRightDerivStieltjesFixedIntervalAverageMeasurable u hu a b) (hcover : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableIntervalCover u hu a b t) : ConvexUpperContactEstimateStatement n

Packaged upper-contact estimate from measurable fixed-interval average maps and a countable fixed-interval representation of the concrete convex Stieltjes interval-average-exceeds sets.

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateStatement.of_convexSourceRightDerivStieltjes_of_endpointAverageMaps_with_chosenMeasureConstant {n : ℕ} {Cmax Ctrans Ccoord Cmeasure ρ : ℝ} {a b : ℕ → ℝ} (hab : ∀ (k : ℕ), a k < b k) (hCmeasure_nonneg : 0 ≤ Cmeasure) (hρ : 0 < ρ) (hρ_le_one : ρ ≤ 1) (hmeasure : ↑n * Ccoord ≤ Cmeasure) (hCtrans_nonneg : 0 ≤ Ctrans) (hAmeasure : ∀ (i : Fin n), MeasureTheory.volume (sourceTransverseOpenCube i 1) ≤ ENNReal.ofReal Ctrans) (hfubiniConst : Ctrans * (2 * Cmax) ≤ Ccoord) (hmax : LocalizedMaximalEstimateStatement Cmax) (hend : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → CoordinateSliceConvexSourceRightDerivStieltjesEndpointAverageMeasurable u hu a b) (hcover : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableIntervalCover u hu a b t) : ConvexUpperContactEstimateStatement n

Packaged upper-contact estimate from measurable endpoint expressions and a countable fixed-interval representation of the concrete convex Stieltjes interval-average-exceeds sets.

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateStatement.of_convexSourceRightDerivStieltjes_of_endpointValueLeftLimit_with_chosenMeasureConstant {n : ℕ} {Cmax Ctrans Ccoord Cmeasure ρ : ℝ} {a b : ℕ → ℝ} (hab : ∀ (k : ℕ), a k < b k) (hCmeasure_nonneg : 0 ≤ Cmeasure) (hρ : 0 < ρ) (hρ_le_one : ρ ≤ 1) (hmeasure : ↑n * Ccoord ≤ Cmeasure) (hCtrans_nonneg : 0 ≤ Ctrans) (hAmeasure : ∀ (i : Fin n), MeasureTheory.volume (sourceTransverseOpenCube i 1) ≤ ENNReal.ofReal Ctrans) (hfubiniConst : Ctrans * (2 * Cmax) ≤ Ccoord) (hmax : LocalizedMaximalEstimateStatement Cmax) (hleft : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → CoordinateSliceConvexSourceRightDerivStieltjesEndpointLeftLimitMeasurable u hu b) (hvalue : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → CoordinateSliceConvexSourceRightDerivStieltjesEndpointValueMeasurable u hu a) (hcover : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableIntervalCover u hu a b t) : ConvexUpperContactEstimateStatement n

Packaged upper-contact estimate from measurable endpoint values, measurable endpoint left limits, and a countable fixed-interval representation of the concrete convex Stieltjes interval-average-exceeds sets.

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateStatement.of_convexSourceRightDerivStieltjes_of_countableIntervalCover_with_chosenMeasureConstant {n : ℕ} {Cmax Ctrans Ccoord Cmeasure ρ : ℝ} {a b : ℕ → ℝ} (hab : ∀ (k : ℕ), a k < b k) (hCmeasure_nonneg : 0 ≤ Cmeasure) (hρ : 0 < ρ) (hρ_le_one : ρ ≤ 1) (hmeasure : ↑n * Ccoord ≤ Cmeasure) (hCtrans_nonneg : 0 ≤ Ctrans) (hAmeasure : ∀ (i : Fin n), MeasureTheory.volume (sourceTransverseOpenCube i 1) ≤ ENNReal.ofReal Ctrans) (hfubiniConst : Ctrans * (2 * Cmax) ≤ Ccoord) (hmax : LocalizedMaximalEstimateStatement Cmax) (hcover : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableIntervalCover u hu a b t) : ConvexUpperContactEstimateStatement n

Packaged upper-contact estimate from the concrete convex Stieltjes endpoint measurability proved in this file and a countable fixed-interval representation of the interval-average exceeds sets.

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateStatement.of_convexSourceRightDerivStieltjes_of_countableIntervalReverseCover_with_chosenMeasureConstant {n : ℕ} {Cmax Ctrans Ccoord Cmeasure ρ : ℝ} {a b : ℕ → ℝ} (hadm : SourceAdmissibleIntervalEnumeration a b) (hCmeasure_nonneg : 0 ≤ Cmeasure) (hρ : 0 < ρ) (hρ_le_one : ρ ≤ 1) (hmeasure : ↑n * Ccoord ≤ Cmeasure) (hCtrans_nonneg : 0 ≤ Ctrans) (hAmeasure : ∀ (i : Fin n), MeasureTheory.volume (sourceTransverseOpenCube i 1) ≤ ENNReal.ofReal Ctrans) (hfubiniConst : Ctrans * (2 * Cmax) ≤ Ccoord) (hmax : LocalizedMaximalEstimateStatement Cmax) (hreverse : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → ConvexStieltjesCountableIntervalReverseCover u hu a b t) : ConvexUpperContactEstimateStatement n

Packaged upper-contact estimate from the concrete convex Stieltjes endpoint measurability proved in this file and the reverse-cover direction for a countable fixed-interval family.

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateStatement.of_convexSourceRightDerivStieltjes_of_rationalRefinement_with_chosenMeasureConstant {n : ℕ} {Cmax Ctrans Ccoord Cmeasure ρ : ℝ} {a b : ℕ → ℝ} (henum : SourceRationalIntervalEnumeration a b) (hCmeasure_nonneg : 0 ≤ Cmeasure) (hρ : 0 < ρ) (hρ_le_one : ρ ≤ 1) (hmeasure : ↑n * Ccoord ≤ Cmeasure) (hCtrans_nonneg : 0 ≤ Ctrans) (hAmeasure : ∀ (i : Fin n), MeasureTheory.volume (sourceTransverseOpenCube i 1) ≤ ENNReal.ofReal Ctrans) (hfubiniConst : Ctrans * (2 * Cmax) ≤ Ccoord) (hmax : LocalizedMaximalEstimateStatement Cmax) (hrefine : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → ConvexStieltjesAverageExceedsRationalRefinement u hu t) : ConvexUpperContactEstimateStatement n

Packaged upper-contact estimate from the concrete convex Stieltjes endpoint measurability proved in this file and rational refinement of source-local average witnesses.

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateStatement.of_convexSourceRightDerivStieltjes_of_innerRationalRefinement_with_chosenMeasureConstant {n : ℕ} {Cmax Ctrans Ccoord Cmeasure ρ : ℝ} {a b : ℕ → ℝ} (henum : SourceRationalIntervalEnumeration a b) (hCmeasure_nonneg : 0 ≤ Cmeasure) (hρ : 0 < ρ) (hρ_le_one : ρ ≤ 1) (hmeasure : ↑n * Ccoord ≤ Cmeasure) (hCtrans_nonneg : 0 ≤ Ctrans) (hAmeasure : ∀ (i : Fin n), MeasureTheory.volume (sourceTransverseOpenCube i 1) ≤ ENNReal.ofReal Ctrans) (hfubiniConst : Ctrans * (2 * Cmax) ≤ Ccoord) (hmax : LocalizedMaximalEstimateStatement Cmax) (hrefine : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → ConvexStieltjesAverageExceedsInnerRationalRefinement u hu t) : ConvexUpperContactEstimateStatement n

Packaged upper-contact estimate from the concrete convex Stieltjes endpoint measurability proved in this file and inner-rational refinement of source-local average witnesses.

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateStatement.of_convexSourceRightDerivStieltjes_of_innerRationalTendsto_with_chosenMeasureConstant {n : ℕ} {Cmax Ctrans Ccoord Cmeasure ρ : ℝ} {a b : ℕ → ℝ} (henum : SourceRationalIntervalEnumeration a b) (hCmeasure_nonneg : 0 ≤ Cmeasure) (hρ : 0 < ρ) (hρ_le_one : ρ ≤ 1) (hmeasure : ↑n * Ccoord ≤ Cmeasure) (hCtrans_nonneg : 0 ≤ Ctrans) (hAmeasure : ∀ (i : Fin n), MeasureTheory.volume (sourceTransverseOpenCube i 1) ≤ ENNReal.ofReal Ctrans) (hfubiniConst : Ctrans * (2 * Cmax) ≤ Ccoord) (hmax : LocalizedMaximalEstimateStatement Cmax) (happrox : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → ConvexStieltjesAverageExceedsInnerRationalTendsto u hu t) : ConvexUpperContactEstimateStatement n

Packaged upper-contact estimate from the concrete convex Stieltjes endpoint measurability proved in this file and sequential inner-rational average approximation.

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateStatement.of_convexSourceRightDerivStieltjes_of_innerRationalMassTendsto_with_chosenMeasureConstant {n : ℕ} {Cmax Ctrans Ccoord Cmeasure ρ : ℝ} {a b : ℕ → ℝ} (henum : SourceRationalIntervalEnumeration a b) (hCmeasure_nonneg : 0 ≤ Cmeasure) (hρ : 0 < ρ) (hρ_le_one : ρ ≤ 1) (hmeasure : ↑n * Ccoord ≤ Cmeasure) (hCtrans_nonneg : 0 ≤ Ctrans) (hAmeasure : ∀ (i : Fin n), MeasureTheory.volume (sourceTransverseOpenCube i 1) ≤ ENNReal.ofReal Ctrans) (hfubiniConst : Ctrans * (2 * Cmax) ≤ Ccoord) (hmax : LocalizedMaximalEstimateStatement Cmax) (hmassApprox : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → ConvexStieltjesAverageExceedsInnerRationalMassTendsto u hu t) : ConvexUpperContactEstimateStatement n

Packaged upper-contact estimate from the concrete convex Stieltjes endpoint measurability proved in this file and sequential inner-rational mass approximation.

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateStatement.of_convexSourceRightDerivStieltjes_of_rationalEnumeration_with_chosenMeasureConstant {n : ℕ} {Cmax Ctrans Ccoord Cmeasure ρ : ℝ} {a b : ℕ → ℝ} (henum : SourceRationalIntervalEnumeration a b) (hCmeasure_nonneg : 0 ≤ Cmeasure) (hρ : 0 < ρ) (hρ_le_one : ρ ≤ 1) (hmeasure : ↑n * Ccoord ≤ Cmeasure) (hCtrans_nonneg : 0 ≤ Ctrans) (hAmeasure : ∀ (i : Fin n), MeasureTheory.volume (sourceTransverseOpenCube i 1) ≤ ENNReal.ofReal Ctrans) (hfubiniConst : Ctrans * (2 * Cmax) ≤ Ccoord) (hmax : LocalizedMaximalEstimateStatement Cmax) : ConvexUpperContactEstimateStatement n

Packaged upper-contact estimate from the concrete convex Stieltjes endpoint measurability, the automatic inner-rational mass approximation, and a rational interval enumeration.

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateStatement.of_convexSourceRightDerivStieltjes_of_existsRationalEnumeration_with_chosenMeasureConstant {n : ℕ} {Cmax Ctrans Ccoord Cmeasure ρ : ℝ} (hCmeasure_nonneg : 0 ≤ Cmeasure) (hρ : 0 < ρ) (hρ_le_one : ρ ≤ 1) (hmeasure : ↑n * Ccoord ≤ Cmeasure) (hCtrans_nonneg : 0 ≤ Ctrans) (hAmeasure : ∀ (i : Fin n), MeasureTheory.volume (sourceTransverseOpenCube i 1) ≤ ENNReal.ofReal Ctrans) (hfubiniConst : Ctrans * (2 * Cmax) ≤ Ccoord) (hmax : LocalizedMaximalEstimateStatement Cmax) : ConvexUpperContactEstimateStatement n

Packaged upper-contact estimate from the concrete convex Stieltjes endpoint measurability and automatic enumeration of all rational source-admissible intervals.

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateStatement.of_convexSourceRightDerivStieltjes_of_localizedMaximal {n : ℕ} {Cmax : ℝ} (hmax : LocalizedMaximalEstimateStatement Cmax) : ConvexUpperContactEstimateStatement n

Packaged upper-contact estimate from the concrete convex Stieltjes route after choosing the transverse and finite-union scalar constants internally. The only remaining analytic input at this boundary is the source-local one-dimensional maximal estimate.

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateStatement.of_convexSourceRightDerivStieltjes_of_existsLocalizedMaximal {n : ℕ} (hmax : ExistsLocalizedMaximalEstimateStatement) : ConvexUpperContactEstimateStatement n

Packaged upper-contact estimate from the existential source-local one-dimensional maximal estimate. This is the source-facing boundary after the concrete Stieltjes, measurability, enumeration, transverse-volume, and scalar-constant bookkeeping has been discharged.

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateStatement.of_convexSourceRightDerivStieltjes {n : ℕ} : ConvexUpperContactEstimateStatement n

Packaged upper-contact estimate from the concrete convex Stieltjes route and the proved source-local one-dimensional maximal estimate.

theorem AleksandrovDifferentiability.ConvexFiniteUpperContactOpeningAEOnCubeStatement.of_convexSourceRightDerivStieltjes {n : ℕ} : ConvexFiniteUpperContactOpeningAEOnCubeStatement n

Finite upper-contact opening a.e. on the source cube from the concrete convex Stieltjes upper-contact estimate.

theorem AleksandrovDifferentiability.volume_sourceOpenCube_diff_iUnion_cubeGoodSet_eq_zero_of_convexSourceRightDerivStieltjes {n : ℕ} (hn : 1 ≤ n) {u : SourceCubeSpace n → ℝ} (hbounded : BoundedOn (sourceOpenCube n 3) u) (hconvex : ConvexOn ℝ (sourceOpenCube n 3) u) : MeasureTheory.volume (sourceOpenCube n 1 \ ⋃ (m : ℕ), cubeGoodSet n u ↑m) = 0

The countable source cube good sets Omega_m cover Q_1 up to a null set by the concrete convex Stieltjes route.