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

Concrete Stieltjes upper-contact estimate assembly

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateDecompositionStatement.of_convexSourceRightDerivStieltjesControls_with_chosenConstant {n : ℕ} {Cmax Ccoord Cmeasure ρ K₀ : ℝ} (hCmeasure_nonneg : 0 ≤ Cmeasure) (hρ : 0 < ρ) (hρ_le_one : ρ ≤ 1) (hK₀ : 0 ≤ K₀) (hmax : LocalizedMaximalEstimateStatement Cmax) (hdiff : ∀ ⦃u : SourceCubeSpace n → ℝ⦄, BoundedOn (sourceOpenCube n 3) u → ConvexOn ℝ (sourceOpenCube n 3) u → MeasureTheory.volume (sourceOpenCube n 1 \ firstOrderDifferentiabilitySet u) = 0) (hendpoint : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u), BoundedOn (sourceOpenCube n 3) u → CoordinateSliceConvexSourceRightDerivStieltjesEndpointControl u hu ρ K₀) (hfubini : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → CoordinateSliceMaximalFubiniEstimate (coordinateSliceConvexSourceRightDerivStieltjesMeasureFamily u hu) (2 * Cmax) Ccoord (sourceCubeOscillation n u) t) (hbound : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → ↑n * ENNReal.ofReal (Ccoord * sourceCubeOscillation n u / t) ≤ ENNReal.ofReal (Cmeasure * sourceCubeOscillation n u / t)) : ConvexUpperContactEstimateDecompositionStatement n

Source-route assembly theorem for the concrete convex source-local Stieltjes slice family.

This packages the current state of the upper-contact estimate route: once first differentiability a.e., the one-dimensional endpoint-control estimate, the Fubini estimate, and the scalar measure constant comparison are supplied for the concrete Stieltjes slices, the abstract upper-contact decomposition follows with the chosen dimensional constant from Cube.Maximal.

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateDecompositionStatement.of_convexSourceRightDerivStieltjesControls_with_chosenMeasureConstant {n : ℕ} {Cmax Ccoord Cmeasure ρ K₀ : ℝ} (hCmeasure_nonneg : 0 ≤ Cmeasure) (hρ : 0 < ρ) (hρ_le_one : ρ ≤ 1) (hK₀ : 0 ≤ K₀) (hmeasure : ↑n * Ccoord ≤ Cmeasure) (hmax : LocalizedMaximalEstimateStatement Cmax) (hdiff : ∀ ⦃u : SourceCubeSpace n → ℝ⦄, BoundedOn (sourceOpenCube n 3) u → ConvexOn ℝ (sourceOpenCube n 3) u → MeasureTheory.volume (sourceOpenCube n 1 \ firstOrderDifferentiabilitySet u) = 0) (hendpoint : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u), BoundedOn (sourceOpenCube n 3) u → CoordinateSliceConvexSourceRightDerivStieltjesEndpointControl u hu ρ K₀) (hfubini : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → CoordinateSliceMaximalFubiniEstimate (coordinateSliceConvexSourceRightDerivStieltjesMeasureFamily u hu) (2 * Cmax) Ccoord (sourceCubeOscillation n u) t) : ConvexUpperContactEstimateDecompositionStatement n

Source-route assembly theorem for the concrete convex source-local Stieltjes slice family, with the finite-union measure constant supplied as the source-style real coefficient inequality (n : ℝ) * Ccoord ≤ Cmeasure.

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateDecompositionStatement.of_convexSourceRightDerivStieltjesSymmetricRemainderControls_with_chosenMeasureConstant {n : ℕ} {Cmax Ccoord Cmeasure ρ : ℝ} (hCmeasure_nonneg : 0 ≤ Cmeasure) (hρ : 0 < ρ) (hρ_le_one : ρ ≤ 1) (hmeasure : ↑n * Ccoord ≤ Cmeasure) (hmax : LocalizedMaximalEstimateStatement Cmax) (hdiff : ∀ ⦃u : SourceCubeSpace n → ℝ⦄, BoundedOn (sourceOpenCube n 3) u → ConvexOn ℝ (sourceOpenCube n 3) u → MeasureTheory.volume (sourceOpenCube n 1 \ firstOrderDifferentiabilitySet u) = 0) (hrem : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u), BoundedOn (sourceOpenCube n 3) u → CoordinateSliceConvexSourceRightDerivStieltjesSymmetricRemainderBound u hu ρ) (hfubini : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → CoordinateSliceMaximalFubiniEstimate (coordinateSliceConvexSourceRightDerivStieltjesMeasureFamily u hu) (2 * Cmax) Ccoord (sourceCubeOscillation n u) t) : ConvexUpperContactEstimateDecompositionStatement n

Source-route assembly from symmetric-remainder estimates for the concrete convex source-local Stieltjes slice family. The one-dimensional endpoint constant is fixed to 2, because the maximal non-bad estimate controls the symmetric interval mass by t * (2*h).

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateDecompositionStatement.of_convexSourceRightDerivStieltjesEndpointBounds_with_chosenMeasureConstant {n : ℕ} {Cmax Ccoord Cmeasure ρ : ℝ} (hCmeasure_nonneg : 0 ≤ Cmeasure) (hρ : 0 < ρ) (hρ_le_one : ρ ≤ 1) (hmeasure : ↑n * Ccoord ≤ Cmeasure) (hmax : LocalizedMaximalEstimateStatement Cmax) (hdiff : ∀ ⦃u : SourceCubeSpace n → ℝ⦄, BoundedOn (sourceOpenCube n 3) u → ConvexOn ℝ (sourceOpenCube n 3) u → MeasureTheory.volume (sourceOpenCube n 1 \ firstOrderDifferentiabilitySet u) = 0) (hbounds : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u), BoundedOn (sourceOpenCube n 3) u → CoordinateSliceConvexSourceRightDerivStieltjesEndpointBounds u hu ρ) (hfubini : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → CoordinateSliceMaximalFubiniEstimate (coordinateSliceConvexSourceRightDerivStieltjesMeasureFamily u hu) (2 * Cmax) Ccoord (sourceCubeOscillation n u) t) : ConvexUpperContactEstimateDecompositionStatement n

Source-route assembly from endpoint comparison bounds for the concrete convex source-local Stieltjes slice family.

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateDecompositionStatement.of_convexSourceRightDerivStieltjesEndpointIdentities_with_chosenMeasureConstant {n : ℕ} {Cmax Ccoord Cmeasure ρ : ℝ} (hCmeasure_nonneg : 0 ≤ Cmeasure) (hρ : 0 < ρ) (hρ_le_one : ρ ≤ 1) (hmeasure : ↑n * Ccoord ≤ Cmeasure) (hmax : LocalizedMaximalEstimateStatement Cmax) (hdiff : ∀ ⦃u : SourceCubeSpace n → ℝ⦄, BoundedOn (sourceOpenCube n 3) u → ConvexOn ℝ (sourceOpenCube n 3) u → MeasureTheory.volume (sourceOpenCube n 1 \ firstOrderDifferentiabilitySet u) = 0) (hident : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u), BoundedOn (sourceOpenCube n 3) u → CoordinateSliceConvexSourceRightDerivStieltjesEndpointIdentities u hu ρ) (hfubini : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → CoordinateSliceMaximalFubiniEstimate (coordinateSliceConvexSourceRightDerivStieltjesMeasureFamily u hu) (2 * Cmax) Ccoord (sourceCubeOscillation n u) t) : ConvexUpperContactEstimateDecompositionStatement n

Source-route assembly from exact endpoint identities for the concrete convex source-local Stieltjes slice family.

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateDecompositionStatement.of_convexSourceRightDerivStieltjes_with_chosenMeasureConstant {n : ℕ} {Cmax Ccoord Cmeasure ρ : ℝ} (hCmeasure_nonneg : 0 ≤ Cmeasure) (hρ : 0 < ρ) (hρ_le_one : ρ ≤ 1) (hmeasure : ↑n * Ccoord ≤ Cmeasure) (hmax : LocalizedMaximalEstimateStatement Cmax) (hdiff : ∀ ⦃u : SourceCubeSpace n → ℝ⦄, BoundedOn (sourceOpenCube n 3) u → ConvexOn ℝ (sourceOpenCube n 3) u → MeasureTheory.volume (sourceOpenCube n 1 \ firstOrderDifferentiabilitySet u) = 0) (hfubini : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → CoordinateSliceMaximalFubiniEstimate (coordinateSliceConvexSourceRightDerivStieltjesMeasureFamily u hu) (2 * Cmax) Ccoord (sourceCubeOscillation n u) t) : ConvexUpperContactEstimateDecompositionStatement n

Source-route assembly for the concrete convex source-local Stieltjes slice family.

This is the current source-faithful cube wrapper: convexity supplies the one-dimensional Stieltjes endpoint-control input, so the remaining analytic assumptions are first differentiability a.e., the localized maximal estimate, the Fubini estimate for the coordinate maximal bad fibers, and the scalar finite-union constant comparison.

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateDecompositionStatement.of_convexStieltjes_with_chosenMeasureConstant {n : ℕ} {Cmax Ccoord Cmeasure ρ : ℝ} (hCmeasure_nonneg : 0 ≤ Cmeasure) (hρ : 0 < ρ) (hρ_le_one : ρ ≤ 1) (hmeasure : ↑n * Ccoord ≤ Cmeasure) (hmax : LocalizedMaximalEstimateStatement Cmax) (hdiff : ∀ ⦃u : SourceCubeSpace n → ℝ⦄, BoundedOn (sourceOpenCube n 3) u → ConvexOn ℝ (sourceOpenCube n 3) u → MeasureTheory.volume (sourceOpenCube n 1 \ firstOrderDifferentiabilitySet u) = 0) (hfubini : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → CoordinateSliceMaximalFubiniEstimate (coordinateSliceConvexSourceRightDerivStieltjesMeasureFamily u hu) (2 * Cmax) Ccoord (sourceCubeOscillation n u) t) : ConvexUpperContactEstimateDecompositionStatement n

Shorter alias for the concrete convex source-local Stieltjes decomposition route.

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateDecompositionStatement.of_convexStieltjes_of_fubini_with_chosenMeasureConstant {n : ℕ} {Cmax Ccoord Cmeasure ρ : ℝ} (hCmeasure_nonneg : 0 ≤ Cmeasure) (hρ : 0 < ρ) (hρ_le_one : ρ ≤ 1) (hmeasure : ↑n * Ccoord ≤ Cmeasure) (hmax : LocalizedMaximalEstimateStatement Cmax) (hfubini : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → CoordinateSliceMaximalFubiniEstimate (coordinateSliceConvexSourceRightDerivStieltjesMeasureFamily u hu) (2 * Cmax) Ccoord (sourceCubeOscillation n u) t) : ConvexUpperContactEstimateDecompositionStatement n

Concrete convex source-local Stieltjes decomposition route after discharging the first-differentiability-a.e. input by Rademacher and local Lipschitz regularity of convex functions. The remaining analytic input is the coordinate Fubini estimate for the localized maximal bad fibers.

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateDecompositionStatement.of_convexStieltjes_of_transverseFubini_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) (hfubiniConst : Ctrans * (2 * Cmax) ≤ Ccoord) (hmax : LocalizedMaximalEstimateStatement Cmax) (htrans : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → CoordinateSliceMaximalTransverseFubiniEstimate (coordinateSliceConvexSourceRightDerivStieltjesMeasureFamily u hu) Ctrans t) : ConvexUpperContactEstimateDecompositionStatement n

Concrete convex source-local Stieltjes decomposition route from the sharper transverse Fubini boundary. This leaves the remaining Fubini work in the source-proof form: a product measure estimate with transverse constant Ctrans, plus the scalar comparison Ctrans * (2 * Cmax) <= Ccoord.

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateDecompositionStatement.of_convexStieltjes_of_badSetMeasurable_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) (hbad : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → CoordinateSliceConvexSourceRightDerivStieltjesMaximalBadSetMeasurable u hu t) : ConvexUpperContactEstimateDecompositionStatement n

Concrete convex source-local Stieltjes decomposition route from measurability of the coordinate maximal bad sets. The canonical coordinate charts are already measure-preserving; this wrapper leaves only the genuine analytic measurability obligation plus scalar constants.

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateDecompositionStatement.of_convexStieltjes_of_averageExceedsMeasurable_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) (havg : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsMeasurable u hu t) : ConvexUpperContactEstimateDecompositionStatement n

Concrete convex source-local Stieltjes decomposition route from measurability of the interval-average-exceeds set. This is the current sharp source-facing measurability input for the Fubini step.

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateStatement.of_convexSourceRightDerivStieltjes_with_chosenMeasureConstant {n : ℕ} {Cmax Ccoord Cmeasure ρ : ℝ} (hCmeasure_nonneg : 0 ≤ Cmeasure) (hρ : 0 < ρ) (hρ_le_one : ρ ≤ 1) (hmeasure : ↑n * Ccoord ≤ Cmeasure) (hmax : LocalizedMaximalEstimateStatement Cmax) (hdiff : ∀ ⦃u : SourceCubeSpace n → ℝ⦄, BoundedOn (sourceOpenCube n 3) u → ConvexOn ℝ (sourceOpenCube n 3) u → MeasureTheory.volume (sourceOpenCube n 1 \ firstOrderDifferentiabilitySet u) = 0) (hfubini : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → CoordinateSliceMaximalFubiniEstimate (coordinateSliceConvexSourceRightDerivStieltjesMeasureFamily u hu) (2 * Cmax) Ccoord (sourceCubeOscillation n u) t) : ConvexUpperContactEstimateStatement n

Packaged upper-contact estimate from the concrete convex source-local Stieltjes route.

Convexity supplies the coordinate Stieltjes endpoint-control input. The remaining hypotheses are the first-differentiability-a.e. input, the localized maximal estimate, the coordinate Fubini estimate for the localized maximal bad fibers, and the scalar finite-union constant comparison.

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateStatement.of_convexSourceRightDerivStieltjes_of_fubini_with_chosenMeasureConstant {n : ℕ} {Cmax Ccoord Cmeasure ρ : ℝ} (hCmeasure_nonneg : 0 ≤ Cmeasure) (hρ : 0 < ρ) (hρ_le_one : ρ ≤ 1) (hmeasure : ↑n * Ccoord ≤ Cmeasure) (hmax : LocalizedMaximalEstimateStatement Cmax) (hfubini : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → CoordinateSliceMaximalFubiniEstimate (coordinateSliceConvexSourceRightDerivStieltjesMeasureFamily u hu) (2 * Cmax) Ccoord (sourceCubeOscillation n u) t) : ConvexUpperContactEstimateStatement n

Packaged upper-contact estimate from the concrete convex source-local Stieltjes route after discharging first differentiability a.e. The remaining analytic input is the coordinate Fubini estimate for the localized maximal bad fibers.

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateStatement.of_convexSourceRightDerivStieltjes_of_transverseFubini_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) (hfubiniConst : Ctrans * (2 * Cmax) ≤ Ccoord) (hmax : LocalizedMaximalEstimateStatement Cmax) (htrans : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → CoordinateSliceMaximalTransverseFubiniEstimate (coordinateSliceConvexSourceRightDerivStieltjesMeasureFamily u hu) Ctrans t) : ConvexUpperContactEstimateStatement n

Packaged upper-contact estimate from the sharper transverse Fubini boundary.

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateStatement.of_convexSourceRightDerivStieltjes_of_badSetMeasurable_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) (hbad : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → CoordinateSliceConvexSourceRightDerivStieltjesMaximalBadSetMeasurable u hu t) : ConvexUpperContactEstimateStatement n

Packaged upper-contact estimate from measurability of the concrete convex source-local Stieltjes maximal bad sets.

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateStatement.of_convexSourceRightDerivStieltjes_of_averageExceedsMeasurable_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) (havg : ∀ ⦃u : SourceCubeSpace n → ℝ⦄ (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsMeasurable u hu t) : ConvexUpperContactEstimateStatement n

Packaged upper-contact estimate from measurability of the concrete convex source-local Stieltjes interval-average-exceeds sets.