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

Secant approximations for clamped coordinate-slice right derivatives

This file proves measurability of fixed coordinate-slice secant slopes and the source-local secant approximation identity for the clamped right derivative.

theorem AleksandrovDifferentiability.coordinateSliceConvexSourceSecantSlopeValue_measurable {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} (i : Fin n) (s h : ℝ) (hpos : 0 < h) (hlt : h < 1) : CoordinateSliceConvexSourceSecantSlopeValueAtMeasurable u hu i s h

theorem AleksandrovDifferentiability.sourceForwardSecantStep_pos (m : ℕ) : 0 < sourceForwardSecantStep m

The standard forward secant step is positive.

theorem AleksandrovDifferentiability.sourceForwardSecantStep_lt_one (m : ℕ) : sourceForwardSecantStep m < 1

The standard forward secant step is smaller than one.

theorem AleksandrovDifferentiability.tendsto_sourceForwardSecantStep : Filter.Tendsto sourceForwardSecantStep Filter.atTop (nhds 0)

The standard forward secant steps tend to zero.

theorem AleksandrovDifferentiability.antitone_sourceForwardSecantStep : Antitone sourceForwardSecantStep

The standard forward secant steps are decreasing.

theorem AleksandrovDifferentiability.ConvexOn.rightDeriv_eq_iInf_slope_sourceForwardSecantStep {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} (hf : ConvexOn ℝ S f) (hx : x ∈ interior S) (hstep : ∀ (m : ℕ), x + sourceForwardSecantStep m ∈ S) : rightDeriv f x = ⨅ (m : ℕ), slope f x (x + sourceForwardSecantStep m)

For a one-dimensional convex function, the project-local right derivative at an interior point is the infimum of the standard forward secant slopes, provided the forward points stay in the convexity set.

theorem AleksandrovDifferentiability.coordinateSliceConvexSourceSecantSlopeValue_standard_measurable {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} (i : Fin n) (s : ℝ) (m : ℕ) : CoordinateSliceConvexSourceSecantSlopeValueAtMeasurable u hu i s (sourceForwardSecantStep m)

The standard forward secant slopes are measurable.

theorem AleksandrovDifferentiability.CoordinateSliceConvexSourceRightDerivExtensionValueMeasurable.of_secantApprox {n : ℕ} {u : SourceCubeSpace n → ℝ} {hu : ConvexOn ℝ (sourceOpenCube n 3) u} (happrox : CoordinateSliceConvexSourceRightDerivExtensionValueSecantApprox u hu) : CoordinateSliceConvexSourceRightDerivExtensionValueMeasurable u hu

The secant approximation identity reduces clamped right-derivative extension measurability to the already proved measurability of fixed forward secant slopes.

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

Concrete convex coordinate slices satisfy the standard secant approximation identity for the clamped right-derivative extension.

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

Fixed clamped right-derivative extension evaluations of concrete convex coordinate slices are measurable.