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

Basic measurability interfaces for Stieltjes coordinate-slice measures

This file contains the basic endpoint and countable-interval interfaces used by the concrete source-local Stieltjes route.

Countable interval and endpoint measurability interfaces

theorem AleksandrovDifferentiability.stieltjesFunction_leftLim_eq_iSup_rat_lt (F : StieltjesFunction ℝ) (c : ℝ) : Function.leftLim (↑F) c = ⨆ (q : { q' : ℚ // ↑q' < c }), ↑F ↑↑q

The left limit of a Stieltjes function is the supremum of its values at rational points strictly to the left.

theorem AleksandrovDifferentiability.monotone_rightLim_eq_iInf_rat_gt {g : ℝ → ℝ} (hg : Monotone g) (c : ℝ) : Function.rightLim g c = ⨅ (q : { q' : ℚ // c < ↑q' }), g ↑↑q

The right limit of a monotone real function is the infimum of its values at rational points strictly to the right.

theorem AleksandrovDifferentiability.sourceDerivativeClamp_mem_Ioo_three (s : ℝ) : sourceDerivativeClamp s ∈ Set.Ioo (-3) 3

The clamped source derivative parameter lies strictly inside the source line domain (-3, 3).

theorem AleksandrovDifferentiability.sourceDerivativeClamp_add_mem_Ioo_three {s h : ℝ} (hpos : 0 < h) (hlt : h < 1) : sourceDerivativeClamp s + h ∈ Set.Ioo (-3) 3

If 0 < h < 1, then the forward point from the clamped source derivative parameter also lies strictly inside the source line domain (-3, 3).

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

Countable fixed-interval measurability for the concrete convex Stieltjes source-local average-exceeds sets.

Equations

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

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

Countable fixed-interval cover for the concrete convex Stieltjes source-local average-exceeds sets.

Equations

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

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

Reverse-cover direction for a countable fixed-interval model of the concrete convex Stieltjes source-local average-exceeds sets.

Equations

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

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

Rational refinement target for concrete convex Stieltjes source-local average-exceeds witnesses.

Equations

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

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

Inner-rational refinement target for concrete convex Stieltjes source-local average-exceeds witnesses.

Equations

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

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

Sequential inner-rational average approximation target for concrete convex Stieltjes source-local average-exceeds witnesses.

Equations

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

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

Sequential inner-rational mass approximation target for concrete convex Stieltjes source-local average-exceeds witnesses.

Equations

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

theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsInnerRationalMassTendsto.of_convex {n : ℕ} (u : SourceCubeSpace n → ℝ) (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (t : ℝ) : CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsInnerRationalMassTendsto u hu t

Concrete convex source-local Stieltjes slices satisfy the sequential inner-rational mass approximation target.

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

Measurability of all fixed-interval average maps for the concrete convex Stieltjes source-local slice family.

Equations

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

noncomputable def AleksandrovDifferentiability.coordinateSliceConvexSourceRightDerivStieltjesEndpointValue {n : ℕ} (u : SourceCubeSpace n → ℝ) (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (i : Fin n) (c : ℝ) (y : SourceCubeSpace n) : ℝ

Right-continuous Stieltjes endpoint value for a concrete convex source-local slice, extended by zero away from Q_1.

Equations

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

noncomputable def AleksandrovDifferentiability.coordinateSliceConvexSourceRightDerivStieltjesEndpointLeftLimit {n : ℕ} (u : SourceCubeSpace n → ℝ) (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (i : Fin n) (c : ℝ) (y : SourceCubeSpace n) : ℝ

Left-limit Stieltjes endpoint value for a concrete convex source-local slice, extended by zero away from Q_1.

Equations

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

noncomputable def AleksandrovDifferentiability.coordinateSliceConvexSourceRightDerivStieltjesEndpointAverageExpression {n : ℕ} (u : SourceCubeSpace n → ℝ) (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (i : Fin n) (a b : ℝ) (y : SourceCubeSpace n) : ℝ

Endpoint expression for a fixed interval average of the concrete convex source-local Stieltjes slice family. It is zero away from Q_1, matching the zero extension in coordinateSliceSourceRightDerivStieltjesMeasureFamily.

Equations

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

noncomputable def AleksandrovDifferentiability.coordinateSliceConvexSourceRightDerivExtensionValue {n : ℕ} (u : SourceCubeSpace n → ℝ) (_hu : ConvexOn ℝ (sourceOpenCube n 3) u) (i : Fin n) (s : ℝ) (y : SourceCubeSpace n) : ℝ

Evaluation of the source-local clamped right-derivative extension for a concrete convex coordinate slice, extended by zero away from Q_1.

Equations

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

noncomputable def AleksandrovDifferentiability.coordinateSliceConvexSourceSecantSlopeValue {n : ℕ} (u : SourceCubeSpace n → ℝ) (_hu : ConvexOn ℝ (sourceOpenCube n 3) u) (i : Fin n) (s h : ℝ) (y : SourceCubeSpace n) : ℝ

A forward secant slope of a concrete convex coordinate slice, based at the clamped source parameter and extended by zero away from Q_1.

Equations

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

noncomputable def AleksandrovDifferentiability.coordinateSliceConvexSourceRightDerivStieltjesEvaluationExtensionRatApprox {n : ℕ} (u : SourceCubeSpace n → ℝ) (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (i : Fin n) (s : ℝ) (r : { r' : ℚ // s < ↑r' }) (y : SourceCubeSpace n) : ℝ

Rational right-approximation of a Stieltjes representative evaluation by the underlying clamped right-derivative extension.

Equations

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

noncomputable def AleksandrovDifferentiability.coordinateSliceConvexSourceRightDerivStieltjesEndpointValueRatApprox {n : ℕ} (u : SourceCubeSpace n → ℝ) (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (i : Fin n) (c : ℝ) (q : { q' : ℚ // c < ↑q' }) (y : SourceCubeSpace n) : ℝ

Rational right-approximation of the right-continuous Stieltjes endpoint value. For a fixed endpoint c, the subtype index ranges over rational q > c.

Equations

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

noncomputable def AleksandrovDifferentiability.coordinateSliceConvexSourceRightDerivStieltjesEndpointLeftLimitRatApprox {n : ℕ} (u : SourceCubeSpace n → ℝ) (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (i : Fin n) (c : ℝ) (q : { q' : ℚ // ↑q' < c }) (y : SourceCubeSpace n) : ℝ

Rational left-approximation of the Stieltjes endpoint left limit. For a fixed endpoint c, the subtype index ranges over rational q < c.

Equations

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

def AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesEndpointValueAtMeasurable {n : ℕ} (u : SourceCubeSpace n → ℝ) (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (i : Fin n) (c : ℝ) : Prop

Measurability of one right-continuous Stieltjes endpoint value for a fixed coordinate and endpoint.

Equations

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

def AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesEndpointLeftLimitAtMeasurable {n : ℕ} (u : SourceCubeSpace n → ℝ) (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (i : Fin n) (c : ℝ) : Prop

Measurability of one left-limit Stieltjes endpoint value for a fixed coordinate and endpoint.

Equations

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

def AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesEndpointAverageAtMeasurable {n : ℕ} (u : SourceCubeSpace n → ℝ) (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (i : Fin n) (a b : ℝ) : Prop

Measurability of one endpoint-average expression for a fixed coordinate and interval.

Equations

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

def AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesEndpointValueRatApproxMeasurable {n : ℕ} (u : SourceCubeSpace n → ℝ) (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (i : Fin n) (c : ℝ) : Prop

Measurability of every rational right-approximation for a fixed coordinate and endpoint.

Equations

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

def AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesEndpointLeftLimitRatApproxMeasurable {n : ℕ} (u : SourceCubeSpace n → ℝ) (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (i : Fin n) (c : ℝ) : Prop

Measurability of every rational left-approximation for a fixed coordinate and endpoint.

Equations

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

def AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivExtensionValueAtMeasurable {n : ℕ} (u : SourceCubeSpace n → ℝ) (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (i : Fin n) (s : ℝ) : Prop

Measurability of one fixed clamped right-derivative extension evaluation for a concrete convex coordinate slice.

Equations

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

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

Measurability of all fixed clamped right-derivative extension evaluations for concrete convex coordinate slices.

Equations

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

def AleksandrovDifferentiability.CoordinateSliceConvexSourceSecantSlopeValueAtMeasurable {n : ℕ} (u : SourceCubeSpace n → ℝ) (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (i : Fin n) (s h : ℝ) : Prop

Measurability of one fixed forward secant slope of a concrete convex coordinate slice.

Equations

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

noncomputable def AleksandrovDifferentiability.sourceForwardSecantStep (m : ℕ) : ℝ

Standard positive forward secant step used to approximate right derivatives.

Equations

• AleksandrovDifferentiability.sourceForwardSecantStep m = (↑(m + 2))⁻¹

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

The clamped right-derivative extension is represented as the infimum of the standard forward secant slopes. This is isolated as the remaining convex-analysis identity needed to turn secant-slope measurability into clamped-extension measurability.

Equations

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

def AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesEvaluationExtensionRatApproxMeasurable {n : ℕ} (u : SourceCubeSpace n → ℝ) (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (i : Fin n) (s : ℝ) : Prop

Measurability of every rational right-approximation of a Stieltjes evaluation by the underlying clamped right-derivative extension.

Equations

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

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

Measurability of all right-continuous Stieltjes endpoint values for a fixed endpoint enumeration.

Equations

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

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

Measurability of all left-limit Stieltjes endpoint values for a fixed endpoint enumeration.

Equations

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

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

Measurability of the endpoint expressions representing all fixed-interval averages for the concrete convex Stieltjes source-local slice family.

Equations

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

theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesEndpointValueMeasurable.of_at {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {a : ℕ → ℝ} (h : ∀ (i : Fin n) (k : ℕ), CoordinateSliceConvexSourceRightDerivStieltjesEndpointValueAtMeasurable u hu i (a k)) : CoordinateSliceConvexSourceRightDerivStieltjesEndpointValueMeasurable u hu a

Fixed-endpoint measurability for each enumerated endpoint gives the packaged endpoint-value measurability obligation.

theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesEndpointLeftLimitMeasurable.of_at {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {b : ℕ → ℝ} (h : ∀ (i : Fin n) (k : ℕ), CoordinateSliceConvexSourceRightDerivStieltjesEndpointLeftLimitAtMeasurable u hu i (b k)) : CoordinateSliceConvexSourceRightDerivStieltjesEndpointLeftLimitMeasurable u hu b

Fixed-endpoint measurability for each enumerated endpoint gives the packaged endpoint-left limit measurability obligation.

theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesEndpointAverageMeasurable.of_at {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {a b : ℕ → ℝ} (h : ∀ (i : Fin n) (k : ℕ), CoordinateSliceConvexSourceRightDerivStieltjesEndpointAverageAtMeasurable u hu i (a k) (b k)) : CoordinateSliceConvexSourceRightDerivStieltjesEndpointAverageMeasurable u hu a b

Fixed-interval endpoint-average measurability for each enumerated interval gives the packaged endpoint-average measurability obligation.