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

One-dimensional second-derivative controls

def AleksandrovDifferentiability.HasOneDimSecondDerivativeSourceMassBound (μ : MeasureTheory.Measure ℝ) (osc : ℝ) : Prop

The second-derivative measure has finite source mass bounded by twice the oscillation.

Equations

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

def AleksandrovDifferentiability.HasOneDimSecondDerivativeEndpointControl (v : ℝ → ℝ) (μ : MeasureTheory.Measure ℝ) (ρ K : ℝ) : Prop

Source endpoint estimate supplied by the one-dimensional convex second-derivative measure.

The variables are centered at an arbitrary x ∈ (-1,1) because coordinate slices in the cube proof are centered at the coordinate x i, not necessarily at 0. The later proof should obtain this from the distributional derivative of the monotone one-sided derivative.

Equations

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

def AleksandrovDifferentiability.HasOneDimSecondDerivativeSymmetricRemainderBound (v : ℝ → ℝ) (μ : MeasureTheory.Measure ℝ) (ρ : ℝ) : Prop

Symmetric interval-mass control of the one-dimensional affine remainder.

For the Stieltjes measure of a convex right derivative, this is the analytic integration step still to be proved: the affine remainder at x ± h is bounded by h times the measure of the symmetric interval (x-h,x+h).

Equations

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

def AleksandrovDifferentiability.HasOneDimSecondDerivativeOpenIntervalDerivativeGapBound (v : ℝ → ℝ) (μ : MeasureTheory.Measure ℝ) (ρ : ℝ) : Prop

Open-interval derivative-gap control by a one-dimensional second-derivative measure.

For the clamped Stieltjes measure of the convex right derivative, this should follow from the Ioo interval formula and the endpoint identities leftLim (rightDeriv v) (x+h) = leftDeriv v (x+h) and rightLim (rightDeriv v) (x-h) = rightDeriv v (x-h).

Equations

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

theorem AleksandrovDifferentiability.HasOneDimSecondDerivativeOpenIntervalDerivativeGapBound.symmetricRemainderBound_of_convex {v : ℝ → ℝ} {μ : MeasureTheory.Measure ℝ} {ρ : ℝ} (hgap : HasOneDimSecondDerivativeOpenIntervalDerivativeGapBound v μ ρ) (hv : ConvexOn ℝ (Set.Ioo (-3) 3) v) (hρ_le_one : ρ ≤ 1) : HasOneDimSecondDerivativeSymmetricRemainderBound v μ ρ

Convexity turns open-interval derivative-gap control into symmetric affine-remainder control.

theorem AleksandrovDifferentiability.HasOneDimSecondDerivativeOpenIntervalDerivativeGapBound.of_sourceRightDerivStieltjes_endpointBounds {v : ℝ → ℝ} {hmono : MonotoneOn (rightDeriv v) (Set.Icc (-2) 2)} {ρ : ℝ} (hendpoints : ∀ ⦃x h : ℝ⦄, x ∈ sourceMaximalWindow → 0 < h → h < ρ → leftDeriv v (x + h) ≤ Function.leftLim (↑(sourceRightDerivStieltjesSecondDerivativeFunction v hmono)) (x + h) ∧ ↑(sourceRightDerivStieltjesSecondDerivativeFunction v hmono) (x - h) ≤ rightDeriv v (x - h)) : HasOneDimSecondDerivativeOpenIntervalDerivativeGapBound v (sourceRightDerivStieltjesSecondDerivativeMeasure v hmono) ρ

Endpoint comparisons for the source-local Stieltjes representative imply the open-interval derivative-gap bound.

The remaining convex-analysis endpoint work is now isolated in the hypothesis hendpoints: inside the source window, the left derivative at the right endpoint must be bounded by the left limit of the Stieltjes representative, while the representative at the left endpoint must be bounded by the right derivative there.

theorem AleksandrovDifferentiability.HasOneDimSecondDerivativeSymmetricRemainderBound.endpointControl {v : ℝ → ℝ} {μ : MeasureTheory.Measure ℝ} {ρ : ℝ} (hrem : HasOneDimSecondDerivativeSymmetricRemainderBound v μ ρ) (hρ_le_one : ρ ≤ 1) : HasOneDimSecondDerivativeEndpointControl v μ ρ 2

Symmetric interval-mass control plus maximal non-badness gives the source endpoint-control estimate, with the explicit constant 2.

def AleksandrovDifferentiability.HasRightDerivStieltjesSourceMassBound (v : ℝ → ℝ) (hmono : Monotone (rightDeriv v)) (osc : ℝ) : Prop

Source mass estimate specialized to the Stieltjes measure of a globally monotone right derivative. This is a target interface: the source proof later supplies the estimate from boundedness/oscillation of the underlying convex function on (-3,3).

Equations

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

def AleksandrovDifferentiability.HasRightDerivStieltjesEndpointControl (v : ℝ → ℝ) (hmono : Monotone (rightDeriv v)) (ρ K : ℝ) : Prop

Source endpoint estimate specialized to the Stieltjes measure of a globally monotone right derivative.

Equations

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

def AleksandrovDifferentiability.HasSourceRightDerivStieltjesSourceMassBound (v : ℝ → ℝ) (hmono : MonotoneOn (rightDeriv v) (Set.Icc (-2) 2)) (osc : ℝ) : Prop

Source mass estimate specialized to the clamped source-local right-derivative Stieltjes measure.

Equations

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

theorem AleksandrovDifferentiability.HasSourceRightDerivStieltjesSourceMassBound.of_sourceJump_le {v : ℝ → ℝ} {hmono : MonotoneOn (rightDeriv v) (Set.Icc (-2) 2)} {osc : ℝ} (hjump : sourceRightDerivStieltjesSourceJump v hmono ≤ 2 * osc) : HasSourceRightDerivStieltjesSourceMassBound v hmono osc

A bound on the Stieltjes source jump gives the source mass estimate required by the localized maximal argument.

theorem AleksandrovDifferentiability.HasSourceRightDerivStieltjesSourceMassBound.of_function_bounds {v : ℝ → ℝ} {hmono : MonotoneOn (rightDeriv v) (Set.Icc (-2) 2)} {lower upper osc : ℝ} (hlower : lower ≤ ↑(sourceRightDerivStieltjesSecondDerivativeFunction v hmono) (-2)) (hupper : Function.leftLim (↑(sourceRightDerivStieltjesSecondDerivativeFunction v hmono)) 2 ≤ upper) (hwidth : upper - lower ≤ 2 * osc) : HasSourceRightDerivStieltjesSourceMassBound v hmono osc

theorem AleksandrovDifferentiability.HasSourceRightDerivStieltjesSourceMassBound.of_abs_function_bound {v : ℝ → ℝ} {hmono : MonotoneOn (rightDeriv v) (Set.Icc (-2) 2)} {osc : ℝ} (hlower : -osc ≤ ↑(sourceRightDerivStieltjesSecondDerivativeFunction v hmono) (-2)) (hupper : Function.leftLim (↑(sourceRightDerivStieltjesSecondDerivativeFunction v hmono)) 2 ≤ osc) : HasSourceRightDerivStieltjesSourceMassBound v hmono osc

theorem AleksandrovDifferentiability.HasSourceRightDerivStieltjesSourceMassBound.of_rightDeriv_bounds {v : ℝ → ℝ} {hmono : MonotoneOn (rightDeriv v) (Set.Icc (-2) 2)} {osc : ℝ} (hlower : -osc ≤ rightDeriv v (-2)) (hupper : rightDeriv v 2 ≤ osc) : HasSourceRightDerivStieltjesSourceMassBound v hmono osc

theorem AleksandrovDifferentiability.HasSourceRightDerivStieltjesSourceMassBound.of_convex_secant_bounds {v : ℝ → ℝ} {hmono : MonotoneOn (rightDeriv v) (Set.Icc (-2) 2)} {osc : ℝ} (hv : ConvexOn ℝ (Set.Ioo (-3) 3) v) (hleft : ∀ (ε : ℝ), 0 < ε → ∃ y ∈ Set.Ioo (-3) (-2), -osc - ε ≤ slope v y (-2)) (hright : ∀ (ε : ℝ), 0 < ε → ∃ y ∈ Set.Ioo 2 3, slope v 2 y ≤ osc + ε) : HasSourceRightDerivStieltjesSourceMassBound v hmono osc

theorem AleksandrovDifferentiability.HasSourceRightDerivStieltjesSourceMassBound.of_convex_pairwise_sub_le {v : ℝ → ℝ} {hmono : MonotoneOn (rightDeriv v) (Set.Icc (-2) 2)} {osc : ℝ} (hv : ConvexOn ℝ (Set.Ioo (-3) 3) v) (hosc : 0 ≤ osc) (hbound : ∀ ⦃x y : ℝ⦄, x ∈ Set.Ioo (-3) 3 → y ∈ Set.Ioo (-3) 3 → v y - v x ≤ osc) : HasSourceRightDerivStieltjesSourceMassBound v hmono osc

def AleksandrovDifferentiability.HasSourceRightDerivStieltjesEndpointControl (v : ℝ → ℝ) (hmono : MonotoneOn (rightDeriv v) (Set.Icc (-2) 2)) (ρ K : ℝ) : Prop

Source endpoint estimate specialized to the clamped source-local right-derivative Stieltjes measure.

Equations

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

def AleksandrovDifferentiability.HasSourceRightDerivStieltjesEndpointIdentities (v : ℝ → ℝ) (hmono : MonotoneOn (rightDeriv v) (Set.Icc (-2) 2)) (ρ : ℝ) : Prop

Exact endpoint identities for the clamped source-local right-derivative Stieltjes representative.

For a one-dimensional convex function, these should follow from right-continuity of the right derivative and from identifying the left derivative with the left limit of the right derivative.

Equations

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

def AleksandrovDifferentiability.HasSourceRightDerivStieltjesEndpointBounds (v : ℝ → ℝ) (hmono : MonotoneOn (rightDeriv v) (Set.Icc (-2) 2)) (ρ : ℝ) : Prop

Endpoint comparison hypothesis for the clamped source-local right-derivative Stieltjes representative.

This is the remaining local convex-analysis input needed to identify the open-interval Stieltjes mass with the derivative gap used by the affine-remainder estimate.

Equations

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

theorem AleksandrovDifferentiability.HasSourceRightDerivStieltjesEndpointIdentities.endpointBounds {v : ℝ → ℝ} {hmono : MonotoneOn (rightDeriv v) (Set.Icc (-2) 2)} {ρ : ℝ} (hident : HasSourceRightDerivStieltjesEndpointIdentities v hmono ρ) : HasSourceRightDerivStieltjesEndpointBounds v hmono ρ

Exact endpoint identities imply the endpoint comparison bounds used by the Stieltjes open-interval argument.

theorem AleksandrovDifferentiability.HasSourceRightDerivStieltjesEndpointIdentities.of_leftLim_eq_leftDeriv_of_extensionRightLim {v : ℝ → ℝ} {hmono : MonotoneOn (rightDeriv v) (Set.Icc (-2) 2)} {ρ : ℝ} (hleft : ∀ ⦃x h : ℝ⦄, x ∈ sourceMaximalWindow → 0 < h → h < ρ → Function.leftLim (↑(sourceRightDerivStieltjesSecondDerivativeFunction v hmono)) (x + h) = leftDeriv v (x + h)) (hright : ∀ ⦃x h : ℝ⦄, x ∈ sourceMaximalWindow → 0 < h → h < ρ → Function.rightLim (sourceRightDerivExtension v) (x - h) = rightDeriv v (x - h)) : HasSourceRightDerivStieltjesEndpointIdentities v hmono ρ

A version of the endpoint-identity interface with the right endpoint written as right-continuity of the clamped right-derivative extension.

theorem AleksandrovDifferentiability.HasSourceRightDerivStieltjesEndpointIdentities.of_extensionEndpointLimits {v : ℝ → ℝ} {hmono : MonotoneOn (rightDeriv v) (Set.Icc (-2) 2)} {ρ : ℝ} (hleft : ∀ ⦃x h : ℝ⦄, x ∈ sourceMaximalWindow → 0 < h → h < ρ → Function.leftLim (sourceRightDerivExtension v) (x + h) = leftDeriv v (x + h)) (hright : ∀ ⦃x h : ℝ⦄, x ∈ sourceMaximalWindow → 0 < h → h < ρ → Function.rightLim (sourceRightDerivExtension v) (x - h) = rightDeriv v (x - h)) : HasSourceRightDerivStieltjesEndpointIdentities v hmono ρ

A version of the endpoint-identity interface stated entirely in terms of the clamped right-derivative extension before passing to its Stieltjes representative.

theorem AleksandrovDifferentiability.HasSourceRightDerivStieltjesEndpointIdentities.of_rightDerivEndpointLimits {v : ℝ → ℝ} {hmono : MonotoneOn (rightDeriv v) (Set.Icc (-2) 2)} {ρ : ℝ} (hρ_le_one : ρ ≤ 1) (hleft : ∀ ⦃x h : ℝ⦄, x ∈ sourceMaximalWindow → 0 < h → h < ρ → Filter.Tendsto (rightDeriv v) (nhdsWithin (x + h) (Set.Iio (x + h))) (nhds (leftDeriv v (x + h)))) (hright : ∀ ⦃x h : ℝ⦄, x ∈ sourceMaximalWindow → 0 < h → h < ρ → Filter.Tendsto (rightDeriv v) (nhdsWithin (x - h) (Set.Ioi (x - h))) (nhds (rightDeriv v (x - h)))) : HasSourceRightDerivStieltjesEndpointIdentities v hmono ρ

Endpoint identities for the clamped Stieltjes representative follow from the ordinary one-sided endpoint limits of the right derivative, once the endpoints are known to stay in the source interval.

theorem AleksandrovDifferentiability.HasSourceRightDerivStieltjesEndpointIdentities.of_leftEndpointLimits_of_convex {v : ℝ → ℝ} {hmono : MonotoneOn (rightDeriv v) (Set.Icc (-2) 2)} {ρ : ℝ} (hρ_le_one : ρ ≤ 1) (hv : ConvexOn ℝ (Set.Ioo (-3) 3) v) (hleft : ∀ ⦃x h : ℝ⦄, x ∈ sourceMaximalWindow → 0 < h → h < ρ → Filter.Tendsto (rightDeriv v) (nhdsWithin (x + h) (Set.Iio (x + h))) (nhds (leftDeriv v (x + h)))) : HasSourceRightDerivStieltjesEndpointIdentities v hmono ρ

Source endpoint identities reduced to the remaining left-limit endpoint theorem for ordinary right derivatives. The right-continuity endpoint is supplied by convexity.

theorem AleksandrovDifferentiability.HasSourceRightDerivStieltjesEndpointIdentities.of_convex {v : ℝ → ℝ} {hmono : MonotoneOn (rightDeriv v) (Set.Icc (-2) 2)} {ρ : ℝ} (hρ_le_one : ρ ≤ 1) (hv : ConvexOn ℝ (Set.Ioo (-3) 3) v) : HasSourceRightDerivStieltjesEndpointIdentities v hmono ρ

Convexity supplies both endpoint identities for the clamped source-local right-derivative Stieltjes representative.

theorem AleksandrovDifferentiability.HasSourceRightDerivStieltjesEndpointControl.of_symmetricRemainderBound {v : ℝ → ℝ} {hmono : MonotoneOn (rightDeriv v) (Set.Icc (-2) 2)} {ρ : ℝ} (hrem : HasOneDimSecondDerivativeSymmetricRemainderBound v (sourceRightDerivStieltjesSecondDerivativeMeasure v hmono) ρ) (hρ_le_one : ρ ≤ 1) : HasSourceRightDerivStieltjesEndpointControl v hmono ρ 2

The remaining analytic symmetric-remainder estimate for the clamped Stieltjes measure implies the source endpoint-control estimate with constant 2.

theorem AleksandrovDifferentiability.HasSourceRightDerivStieltjesEndpointControl.of_openIntervalDerivativeGapBound {v : ℝ → ℝ} {hmono : MonotoneOn (rightDeriv v) (Set.Icc (-2) 2)} {ρ : ℝ} (hgap : HasOneDimSecondDerivativeOpenIntervalDerivativeGapBound v (sourceRightDerivStieltjesSecondDerivativeMeasure v hmono) ρ) (hv : ConvexOn ℝ (Set.Ioo (-3) 3) v) (hρ_le_one : ρ ≤ 1) : HasSourceRightDerivStieltjesEndpointControl v hmono ρ 2

The open-interval derivative-gap bound for the clamped Stieltjes measure, together with convexity, gives source endpoint control with constant 2.

theorem AleksandrovDifferentiability.HasSourceRightDerivStieltjesEndpointControl.of_endpointBounds {v : ℝ → ℝ} {hmono : MonotoneOn (rightDeriv v) (Set.Icc (-2) 2)} {ρ : ℝ} (hendpoints : HasSourceRightDerivStieltjesEndpointBounds v hmono ρ) (hv : ConvexOn ℝ (Set.Ioo (-3) 3) v) (hρ_le_one : ρ ≤ 1) : HasSourceRightDerivStieltjesEndpointControl v hmono ρ 2

Endpoint comparisons for the clamped Stieltjes representative, together with convexity, give source endpoint control with constant 2.

theorem AleksandrovDifferentiability.HasSourceRightDerivStieltjesEndpointControl.of_convex {v : ℝ → ℝ} {hmono : MonotoneOn (rightDeriv v) (Set.Icc (-2) 2)} {ρ : ℝ} (hv : ConvexOn ℝ (Set.Ioo (-3) 3) v) (hρ_le_one : ρ ≤ 1) : HasSourceRightDerivStieltjesEndpointControl v hmono ρ 2

Convexity supplies the source endpoint-control estimate for the clamped source-local right-derivative Stieltjes measure, with constant 2.

theorem AleksandrovDifferentiability.sourceRightDerivStieltjes_measureReal_Ioo_symm_le_two_mul_of_not_bad {v : ℝ → ℝ} {hmono : MonotoneOn (rightDeriv v) (Set.Icc (-2) 2)} {x t h : ℝ} (hnot : ¬sourceLocalizedMaximalBadPredicate (sourceRightDerivStieltjesSecondDerivativeMeasure v hmono) x t) (hx : x ∈ sourceMaximalWindow) (hh_pos : 0 < h) (hh : h < 1) : (sourceRightDerivStieltjesSecondDerivativeMeasure v hmono).real (Set.Ioo (x - h) (x + h)) ≤ t * (2 * h)

At a source non-bad point, the clamped Stieltjes measure of a symmetric short interval is controlled by the maximal threshold. This is the measure input for the future one-dimensional endpoint-control estimate.

theorem AleksandrovDifferentiability.HasRightDerivStieltjesSourceMassBound.sourceBadSet_measure_le {C osc : ℝ} {v : ℝ → ℝ} {hmono : Monotone (rightDeriv v)} {t : ℝ} (hmass : HasRightDerivStieltjesSourceMassBound v hmono osc) (hmax : LocalizedMaximalEstimateStatement C) (ht : 0 < t) : MeasureTheory.volume (sourceLocalizedMaximalBadSet (rightDerivStieltjesSecondDerivativeMeasure v hmono) t) ≤ ENNReal.ofReal (2 * C * osc / t)

theorem AleksandrovDifferentiability.HasSourceRightDerivStieltjesSourceMassBound.sourceBadSet_measure_le {C osc : ℝ} {v : ℝ → ℝ} {hmono : MonotoneOn (rightDeriv v) (Set.Icc (-2) 2)} {t : ℝ} (hmass : HasSourceRightDerivStieltjesSourceMassBound v hmono osc) (hmax : LocalizedMaximalEstimateStatement C) (ht : 0 < t) : MeasureTheory.volume (sourceLocalizedMaximalBadSet (sourceRightDerivStieltjesSecondDerivativeMeasure v hmono) t) ≤ ENNReal.ofReal (2 * C * osc / t)

theorem AleksandrovDifferentiability.HasOneDimSecondDerivativeSourceMassBound.sourceBadSet_measure_le {C osc : ℝ} {μ : MeasureTheory.Measure ℝ} {t : ℝ} (hmass : HasOneDimSecondDerivativeSourceMassBound μ osc) (hmax : LocalizedMaximalEstimateStatement C) (ht : 0 < t) : MeasureTheory.volume (sourceLocalizedMaximalBadSet μ t) ≤ ENNReal.ofReal (2 * C * osc / t)

The source bad set estimate obtained by combining the localized maximal weak-type theorem with the one-dimensional convex mass bound.