Documentation

LeanPool.ViscositySolutionTheory.AleksandrovDifferentiability.Statements.Cube.Stieltjes.Measurability.CountableIntervals

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

Countable interval reductions for Stieltjes coordinate-slice maximal sets #

This file connects endpoint-average measurability to fixed-interval average maps and the countable interval formulation of the source-local maximal bad sets.

source
theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableInterval.endpointAverageMeasurable_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

Endpoint-value and endpoint-left-limit measurability gives endpoint-average measurability.

source
theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableInterval.fixedIntervalAverageMeasurable_of_endpointAverage {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {a b : ℕ → ℝ} (hab : ∀ (k : ℕ), a k < b k) (hend : CoordinateSliceConvexSourceRightDerivStieltjesEndpointAverageMeasurable u hu a b) :
CoordinateSliceConvexSourceRightDerivStieltjesFixedIntervalAverageMeasurable u hu a b

Endpoint-expression measurability gives fixed-interval average-map measurability for genuine intervals.

source
theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableInterval.measurable_of_averageMaps {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {a b : ℕ → ℝ} {t : ℝ} (havg : CoordinateSliceConvexSourceRightDerivStieltjesFixedIntervalAverageMeasurable u hu a b) :
CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableIntervalMeasurable u hu a b t

Measurable fixed-interval average maps give the concrete convex Stieltjes countable-interval measurability input.

source
theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableInterval.cover_of_reverseCover {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {a b : ℕ → ℝ} {t : ℝ} (hadm : SourceAdmissibleIntervalEnumeration a b) (hreverse : CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableIntervalReverseCover u hu a b t) :
CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableIntervalCover u hu a b t

An admissible interval enumeration and the concrete reverse-cover direction give the countable fixed-interval representation for convex Stieltjes slices.

source
theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableInterval.reverseCover_of_rationalRefinement {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {a b : ℕ → ℝ} {t : ℝ} (henum : SourceRationalIntervalEnumeration a b) (hrefine : CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsRationalRefinement u hu t) :
CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableIntervalReverseCover u hu a b t

A rational interval enumeration and rational refinement give the concrete reverse-cover direction for convex Stieltjes slices.

source
theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableInterval.rationalRefinement_of_inner {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {t : ℝ} (hrefine : CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsInnerRationalRefinement u hu t) :
CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsRationalRefinement u hu t

Inner-rational refinement gives the concrete rational-refinement target for convex Stieltjes slices.

source
theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableInterval.innerRationalRefinement_of_tendsto {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {t : ℝ} (happrox : CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsInnerRationalTendsto u hu t) :
CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsInnerRationalRefinement u hu t

Sequential inner-rational approximation gives the concrete inner-rational refinement target for convex Stieltjes slices.

source
theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableInterval.innerRationalRefinement_of_massTendsto {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {t : ℝ} (hmassApprox : CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsInnerRationalMassTendsto u hu t) :
CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsInnerRationalRefinement u hu t

Sequential inner-rational mass approximation gives the concrete inner-rational refinement target for convex Stieltjes slices.

source
theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableInterval.rationalRefinement_of_tendsto {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {t : ℝ} (happrox : CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsInnerRationalTendsto u hu t) :
CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsRationalRefinement u hu t

Sequential inner-rational approximation gives the concrete rational-refinement target for convex Stieltjes slices.

source
theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableInterval.rationalRefinement_of_massTendsto {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {t : ℝ} (hmassApprox : CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsInnerRationalMassTendsto u hu t) :
CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsRationalRefinement u hu t

Sequential inner-rational mass approximation gives the concrete rational-refinement target for convex Stieltjes slices.

source
theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableInterval.reverseCover_of_innerRationalRefinement {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {a b : ℕ → ℝ} {t : ℝ} (henum : SourceRationalIntervalEnumeration a b) (hrefine : CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsInnerRationalRefinement u hu t) :
CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableIntervalReverseCover u hu a b t

A rational interval enumeration and inner-rational refinement give the concrete reverse-cover direction for convex Stieltjes slices.

source
theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableInterval.reverseCover_of_tendsto {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {a b : ℕ → ℝ} {t : ℝ} (henum : SourceRationalIntervalEnumeration a b) (happrox : CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsInnerRationalTendsto u hu t) :
CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableIntervalReverseCover u hu a b t

A rational interval enumeration and sequential inner-rational approximation give the concrete reverse-cover direction for convex Stieltjes slices.

source
theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableInterval.reverseCover_of_massTendsto {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {a b : ℕ → ℝ} {t : ℝ} (henum : SourceRationalIntervalEnumeration a b) (hmassApprox : CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsInnerRationalMassTendsto u hu t) :
CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableIntervalReverseCover u hu a b t

A rational interval enumeration and sequential inner-rational mass approximation give the concrete reverse-cover direction for convex Stieltjes slices.

source
theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableInterval.cover_of_rationalRefinement {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {a b : ℕ → ℝ} {t : ℝ} (henum : SourceRationalIntervalEnumeration a b) (hrefine : CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsRationalRefinement u hu t) :
CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableIntervalCover u hu a b t

A rational interval enumeration and rational refinement give the concrete countable fixed-interval representation for convex Stieltjes slices.

source
theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableInterval.cover_of_innerRationalRefinement {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {a b : ℕ → ℝ} {t : ℝ} (henum : SourceRationalIntervalEnumeration a b) (hrefine : CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsInnerRationalRefinement u hu t) :
CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableIntervalCover u hu a b t

A rational interval enumeration and inner-rational refinement give the concrete countable fixed-interval representation for convex Stieltjes slices.

source
theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableInterval.cover_of_tendsto {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {a b : ℕ → ℝ} {t : ℝ} (henum : SourceRationalIntervalEnumeration a b) (happrox : CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsInnerRationalTendsto u hu t) :
CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableIntervalCover u hu a b t

A rational interval enumeration and sequential inner-rational approximation give the concrete countable fixed-interval representation for convex Stieltjes slices.

source
theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableInterval.cover_of_massTendsto {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {a b : ℕ → ℝ} {t : ℝ} (henum : SourceRationalIntervalEnumeration a b) (hmassApprox : CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsInnerRationalMassTendsto u hu t) :
CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableIntervalCover u hu a b t

A rational interval enumeration and sequential inner-rational mass approximation give the concrete countable fixed-interval representation for convex Stieltjes slices.

source
theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableInterval.averageExceedsMeasurable {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {a b : ℕ → ℝ} {t : ℝ} (hfixed : CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableIntervalMeasurable u hu a b t) (hcover : CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableIntervalCover u hu a b t) :
CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsMeasurable u hu t

A countable fixed-interval representation gives the concrete convex Stieltjes average-exceeds measurability input.

source
theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableInterval.averageExceedsMeasurable_of_reverseCover {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {a b : ℕ → ℝ} {t : ℝ} (hfixed : CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableIntervalMeasurable u hu a b t) (hadm : SourceAdmissibleIntervalEnumeration a b) (hreverse : CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableIntervalReverseCover u hu a b t) :
CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsMeasurable u hu t

Fixed-interval measurability plus the reverse-cover direction gives the concrete convex Stieltjes average-exceeds measurability input.

source
theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableInterval.averageExceedsMeasurable_of_rationalRefinement {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {a b : ℕ → ℝ} {t : ℝ} (hfixed : CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableIntervalMeasurable u hu a b t) (henum : SourceRationalIntervalEnumeration a b) (hrefine : CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsRationalRefinement u hu t) :
CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsMeasurable u hu t

Fixed-interval measurability plus rational refinement gives the concrete convex Stieltjes average-exceeds measurability input.

source
theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableInterval.averageExceedsMeasurable_of_innerRationalRefinement {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {a b : ℕ → ℝ} {t : ℝ} (hfixed : CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableIntervalMeasurable u hu a b t) (henum : SourceRationalIntervalEnumeration a b) (hrefine : CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsInnerRationalRefinement u hu t) :
CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsMeasurable u hu t

Fixed-interval measurability plus inner-rational refinement gives the concrete convex Stieltjes average-exceeds measurability input.

source
theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableInterval.averageExceedsMeasurable_of_tendsto {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {a b : ℕ → ℝ} {t : ℝ} (hfixed : CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableIntervalMeasurable u hu a b t) (henum : SourceRationalIntervalEnumeration a b) (happrox : CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsInnerRationalTendsto u hu t) :
CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsMeasurable u hu t

Fixed-interval measurability plus sequential inner-rational approximation gives the concrete convex Stieltjes average-exceeds measurability input.

source
theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableInterval.averageExceedsMeasurable_of_massTendsto {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {a b : ℕ → ℝ} {t : ℝ} (hfixed : CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableIntervalMeasurable u hu a b t) (henum : SourceRationalIntervalEnumeration a b) (hmassApprox : CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsInnerRationalMassTendsto u hu t) :
CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsMeasurable u hu t

Fixed-interval measurability plus sequential inner-rational mass approximation gives the concrete convex Stieltjes average-exceeds measurability input.

source
theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableInterval.badSetMeasurable {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {a b : ℕ → ℝ} {t : ℝ} (hfixed : CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableIntervalMeasurable u hu a b t) (hcover : CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableIntervalCover u hu a b t) :
CoordinateSliceConvexSourceRightDerivStieltjesMaximalBadSetMeasurable u hu t

A countable fixed-interval representation is enough for the concrete ambient coordinate maximal bad-set measurability.

source
theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableInterval.badSetMeasurable_of_reverseCover {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {a b : ℕ → ℝ} {t : ℝ} (hfixed : CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableIntervalMeasurable u hu a b t) (hadm : SourceAdmissibleIntervalEnumeration a b) (hreverse : CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableIntervalReverseCover u hu a b t) :
CoordinateSliceConvexSourceRightDerivStieltjesMaximalBadSetMeasurable u hu t

Fixed-interval measurability plus the reverse-cover direction is enough for the concrete ambient coordinate maximal bad-set measurability.

source
theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableInterval.badSetMeasurable_of_rationalRefinement {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {a b : ℕ → ℝ} {t : ℝ} (hfixed : CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableIntervalMeasurable u hu a b t) (henum : SourceRationalIntervalEnumeration a b) (hrefine : CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsRationalRefinement u hu t) :
CoordinateSliceConvexSourceRightDerivStieltjesMaximalBadSetMeasurable u hu t

Fixed-interval measurability plus rational refinement is enough for the concrete ambient coordinate maximal bad-set measurability.

source
theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableInterval.badSetMeasurable_of_innerRationalRefinement {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {a b : ℕ → ℝ} {t : ℝ} (hfixed : CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableIntervalMeasurable u hu a b t) (henum : SourceRationalIntervalEnumeration a b) (hrefine : CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsInnerRationalRefinement u hu t) :
CoordinateSliceConvexSourceRightDerivStieltjesMaximalBadSetMeasurable u hu t

Fixed-interval measurability plus inner-rational refinement is enough for the concrete ambient coordinate maximal bad-set measurability.

source
theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableInterval.badSetMeasurable_of_tendsto {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {a b : ℕ → ℝ} {t : ℝ} (hfixed : CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableIntervalMeasurable u hu a b t) (henum : SourceRationalIntervalEnumeration a b) (happrox : CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsInnerRationalTendsto u hu t) :
CoordinateSliceConvexSourceRightDerivStieltjesMaximalBadSetMeasurable u hu t

Fixed-interval measurability plus sequential inner-rational approximation is enough for the concrete ambient coordinate maximal bad-set measurability.

source
theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableInterval.badSetMeasurable_of_massTendsto {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} {a b : ℕ → ℝ} {t : ℝ} (hfixed : CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsCountableIntervalMeasurable u hu a b t) (henum : SourceRationalIntervalEnumeration a b) (hmassApprox : CoordinateSliceConvexSourceRightDerivStieltjesAverageExceedsInnerRationalMassTendsto u hu t) :
CoordinateSliceConvexSourceRightDerivStieltjesMaximalBadSetMeasurable u hu t

Fixed-interval measurability plus sequential inner-rational mass approximation is enough for the concrete ambient coordinate maximal bad-set measurability.