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

Endpoint measurability reductions for Stieltjes coordinate-slice measures

This file reduces Stieltjes endpoint values and endpoint left limits to countable rational and secant approximations, then packages the concrete convex endpoint measurability facts.

theorem AleksandrovDifferentiability.coordinateSliceConvexSourceRightDerivStieltjesEndpointValue_eq_iInf_ratApprox {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} (i : Fin n) (c : ℝ) (y : SourceCubeSpace n) : coordinateSliceConvexSourceRightDerivStieltjesEndpointValue u hu i c y = ⨅ (q : { q' : ℚ // c < ↑q' }), coordinateSliceConvexSourceRightDerivStieltjesEndpointValueRatApprox u hu i c q y

theorem AleksandrovDifferentiability.stieltjesEndpointValueAtMeasurable_of_ratApprox {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {i : Fin n} {c : ℝ} (happrox : CoordinateSliceConvexSourceRightDerivStieltjesEndpointValueRatApproxMeasurable u hu i c) : CoordinateSliceConvexSourceRightDerivStieltjesEndpointValueAtMeasurable u hu i c

Measurability of all rational right-approximations gives measurability of the fixed right-continuous Stieltjes endpoint value.

theorem AleksandrovDifferentiability.coordinateSliceConvexSourceRightDerivStieltjesEndpointValueRatApprox_eq_iInf_extension {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} (i : Fin n) (c : ℝ) (q : { q' : ℚ // c < ↑q' }) (y : SourceCubeSpace n) : coordinateSliceConvexSourceRightDerivStieltjesEndpointValueRatApprox u hu i c q y = ⨅ (r : { r' : ℚ // ↑↑q < ↑r' }), coordinateSliceConvexSourceRightDerivStieltjesEvaluationExtensionRatApprox u hu i (↑↑q) r y

A rational right-approximation of the Stieltjes endpoint value is the infimum of the underlying clamped right-derivative extension at rational points to its right.

theorem AleksandrovDifferentiability.stieltjesEndpointValueRatApproxMeasurable_of_extensionRatApprox {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {i : Fin n} {c : ℝ} {q : { q' : ℚ // c < ↑q' }} (happrox : CoordinateSliceConvexSourceRightDerivStieltjesEvaluationExtensionRatApproxMeasurable u hu i ↑↑q) : Measurable fun (y : SourceCubeSpace n) => coordinateSliceConvexSourceRightDerivStieltjesEndpointValueRatApprox u hu i c q y

Measurability of the underlying extension approximations gives measurability of one rational right-approximation of the Stieltjes endpoint value.

theorem AleksandrovDifferentiability.stieltjesEvaluationExtensionRatApproxMeasurable_of_extensionValueAt {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {i : Fin n} {s : ℝ} (hvalue : ∀ (r : { r' : ℚ // s < ↑r' }), CoordinateSliceConvexSourceRightDerivExtensionValueAtMeasurable u hu i ↑↑r) : CoordinateSliceConvexSourceRightDerivStieltjesEvaluationExtensionRatApproxMeasurable u hu i s

Fixed clamped-extension measurability gives measurability of all rational extension approximations above one base point.

theorem AleksandrovDifferentiability.stieltjesEvaluationExtensionRatApproxMeasurable_of_extensionValue {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {i : Fin n} {s : ℝ} (hvalue : CoordinateSliceConvexSourceRightDerivExtensionValueMeasurable u hu) : CoordinateSliceConvexSourceRightDerivStieltjesEvaluationExtensionRatApproxMeasurable u hu i s

Global fixed clamped-extension measurability gives measurability of all rational extension approximations above one base point.

theorem AleksandrovDifferentiability.stieltjesEndpointValueRatApproxMeasurable_of_extensionValue {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {i : Fin n} {c : ℝ} {q : { q' : ℚ // c < ↑q' }} (hvalue : CoordinateSliceConvexSourceRightDerivExtensionValueMeasurable u hu) : Measurable fun (y : SourceCubeSpace n) => coordinateSliceConvexSourceRightDerivStieltjesEndpointValueRatApprox u hu i c q y

Global fixed clamped-extension measurability gives measurability of every rational right-approximation of a Stieltjes endpoint value.

theorem AleksandrovDifferentiability.coordinateSliceConvexSourceRightDerivStieltjesEndpointLeftLimit_eq_iSup_ratApprox {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} (i : Fin n) (c : ℝ) (y : SourceCubeSpace n) : coordinateSliceConvexSourceRightDerivStieltjesEndpointLeftLimit u hu i c y = ⨆ (q : { q' : ℚ // ↑q' < c }), coordinateSliceConvexSourceRightDerivStieltjesEndpointLeftLimitRatApprox u hu i c q y

The Stieltjes endpoint left limit is the supremum of its rational left-approximations.

theorem AleksandrovDifferentiability.stieltjesEndpointLeftLimitAtMeasurable_of_ratApprox {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {i : Fin n} {c : ℝ} (happrox : CoordinateSliceConvexSourceRightDerivStieltjesEndpointLeftLimitRatApproxMeasurable u hu i c) : CoordinateSliceConvexSourceRightDerivStieltjesEndpointLeftLimitAtMeasurable u hu i c

Measurability of all rational left-approximations gives measurability of the fixed Stieltjes endpoint left limit.

theorem AleksandrovDifferentiability.coordinateSliceConvexSourceRightDerivStieltjesEndpointLeftLimitRatApprox_eq_iInf_extension {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} (i : Fin n) (c : ℝ) (q : { q' : ℚ // ↑q' < c }) (y : SourceCubeSpace n) : coordinateSliceConvexSourceRightDerivStieltjesEndpointLeftLimitRatApprox u hu i c q y = ⨅ (r : { r' : ℚ // ↑↑q < ↑r' }), coordinateSliceConvexSourceRightDerivStieltjesEvaluationExtensionRatApprox u hu i (↑↑q) r y

A rational left-approximation of the Stieltjes endpoint left limit is the infimum of the underlying clamped right-derivative extension at rational points to its right.

theorem AleksandrovDifferentiability.stieltjesEndpointLeftLimitRatApproxMeasurable_of_extensionRatApprox {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {i : Fin n} {c : ℝ} {q : { q' : ℚ // ↑q' < c }} (happrox : CoordinateSliceConvexSourceRightDerivStieltjesEvaluationExtensionRatApproxMeasurable u hu i ↑↑q) : Measurable fun (y : SourceCubeSpace n) => coordinateSliceConvexSourceRightDerivStieltjesEndpointLeftLimitRatApprox u hu i c q y

Measurability of the underlying extension approximations gives measurability of one rational left-approximation of the Stieltjes endpoint left limit.

theorem AleksandrovDifferentiability.stieltjesEndpointLeftLimitRatApproxMeasurable_of_extensionValue {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {i : Fin n} {c : ℝ} {q : { q' : ℚ // ↑q' < c }} (hvalue : CoordinateSliceConvexSourceRightDerivExtensionValueMeasurable u hu) : Measurable fun (y : SourceCubeSpace n) => coordinateSliceConvexSourceRightDerivStieltjesEndpointLeftLimitRatApprox u hu i c q y

Global fixed clamped-extension measurability gives measurability of every rational left-approximation of a Stieltjes endpoint left limit.

theorem AleksandrovDifferentiability.stieltjesEndpointValueAtMeasurable_of_extensionValue {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {i : Fin n} {c : ℝ} (hvalue : CoordinateSliceConvexSourceRightDerivExtensionValueMeasurable u hu) : CoordinateSliceConvexSourceRightDerivStieltjesEndpointValueAtMeasurable u hu i c

Global fixed clamped-extension measurability gives measurability of one right-continuous Stieltjes endpoint value.

theorem AleksandrovDifferentiability.stieltjesEndpointLeftLimitAtMeasurable_of_extensionValue {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {i : Fin n} {c : ℝ} (hvalue : CoordinateSliceConvexSourceRightDerivExtensionValueMeasurable u hu) : CoordinateSliceConvexSourceRightDerivStieltjesEndpointLeftLimitAtMeasurable u hu i c

Global fixed clamped-extension measurability gives measurability of one Stieltjes endpoint left limit.

theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesEndpointValueMeasurable.of_extensionValue {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {a : ℕ → ℝ} (hvalue : CoordinateSliceConvexSourceRightDerivExtensionValueMeasurable u hu) : CoordinateSliceConvexSourceRightDerivStieltjesEndpointValueMeasurable u hu a

Global fixed clamped-extension measurability gives the packaged endpoint-value measurability for any endpoint enumeration.

theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesEndpointLeftLimitMeasurable.of_extensionValue {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {b : ℕ → ℝ} (hvalue : CoordinateSliceConvexSourceRightDerivExtensionValueMeasurable u hu) : CoordinateSliceConvexSourceRightDerivStieltjesEndpointLeftLimitMeasurable u hu b

Global fixed clamped-extension measurability gives the packaged endpoint-left-limit measurability for any endpoint enumeration.

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

Convex source-local Stieltjes endpoint values are measurable for any endpoint enumeration.

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

Convex source-local Stieltjes endpoint left limits are measurable for any endpoint enumeration.

theorem AleksandrovDifferentiability.coordinateSliceConvexSourceRightDerivStieltjes_endpointAverageExpression_eq {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} (i : Fin n) (a b : ℝ) (y : SourceCubeSpace n) : coordinateSliceConvexSourceRightDerivStieltjesEndpointAverageExpression u hu i a b y = (coordinateSliceConvexSourceRightDerivStieltjesEndpointLeftLimit u hu i b y - coordinateSliceConvexSourceRightDerivStieltjesEndpointValue u hu i a y) / (b - a)

The endpoint-average expression is the quotient of the endpoint left limit minus the endpoint value.

theorem AleksandrovDifferentiability.stieltjesEndpointAverageAtMeasurable_of_endpointValue_leftLimit {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {i : Fin n} {a b : ℝ} (hleft : CoordinateSliceConvexSourceRightDerivStieltjesEndpointLeftLimitAtMeasurable u hu i b) (hvalue : CoordinateSliceConvexSourceRightDerivStieltjesEndpointValueAtMeasurable u hu i a) : CoordinateSliceConvexSourceRightDerivStieltjesEndpointAverageAtMeasurable u hu i a b

Measurability of one endpoint value and one endpoint left limit gives measurability of the corresponding endpoint-average expression.

theorem AleksandrovDifferentiability.CoordinateSliceStieltjesEndpointAverageMeasurable.of_endpointValue_leftLimit {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {a b : ℕ → ℝ} (hleft : CoordinateSliceConvexSourceRightDerivStieltjesEndpointLeftLimitMeasurable u hu b) (hvalue : CoordinateSliceConvexSourceRightDerivStieltjesEndpointValueMeasurable u hu a) : CoordinateSliceConvexSourceRightDerivStieltjesEndpointAverageMeasurable u hu a b

Measurability of endpoint values and endpoint left limits gives measurability of the endpoint-average expressions.

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

Convex source-local Stieltjes endpoint-average expressions are measurable for any endpoint enumeration.

theorem AleksandrovDifferentiability.coordinateSliceConvexSourceRightDerivStieltjes_average_eq_endpointAverageExpression {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} (i : Fin n) {a b : ℝ} (hab : a < b) (y : SourceCubeSpace n) : openIntervalMeasureAverage (coordinateSliceConvexSourceRightDerivStieltjesMeasureFamily u hu i y) a b = coordinateSliceConvexSourceRightDerivStieltjesEndpointAverageExpression u hu i a b y

For a genuine interval a < b, the fixed-interval average of the concrete convex Stieltjes slice measure is the corresponding endpoint expression.