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

One-dimensional convex second-derivative measure interfaces

This file records the source-proof interface for the distributional second derivative measure of a bounded convex function on (-3,3). The actual construction of this measure is still future work; the statements here isolate exactly the mass and endpoint-control facts needed by the localized maximal argument.

Stieltjes-measure candidate

noncomputable def AleksandrovDifferentiability.monotoneStieltjesSecondDerivativeFunction (g : ℝ → ℝ) (hg : Monotone g) : StieltjesFunction ℝ

The Stieltjes function associated to a monotone real function.

For the source proof, g will be a one-sided derivative of a one-dimensional convex function. Mathlib's construction replaces g by its right-continuous representative rightLim g, which is the usual convention for the Stieltjes measure assigning mass G(b) - G(a) to (a,b].

Equations

• AleksandrovDifferentiability.monotoneStieltjesSecondDerivativeFunction g hg = hg.stieltjesFunction

noncomputable def AleksandrovDifferentiability.monotoneStieltjesSecondDerivativeMeasure (g : ℝ → ℝ) (hg : Monotone g) : MeasureTheory.Measure ℝ

The Stieltjes measure associated to a monotone real function.

This is the concrete candidate for the distributional derivative measure of a monotone one-sided derivative.

Equations

• AleksandrovDifferentiability.monotoneStieltjesSecondDerivativeMeasure g hg = (AleksandrovDifferentiability.monotoneStieltjesSecondDerivativeFunction g hg).measure

noncomputable def AleksandrovDifferentiability.rightDerivStieltjesSecondDerivativeFunction (v : ℝ → ℝ) (hmono : Monotone (rightDeriv v)) : StieltjesFunction ℝ

The Stieltjes function associated to the project-local right derivative, assuming that right derivative has already been extended or localized as a globally monotone function.

Equations

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

noncomputable def AleksandrovDifferentiability.rightDerivStieltjesSecondDerivativeMeasure (v : ℝ → ℝ) (hmono : Monotone (rightDeriv v)) : MeasureTheory.Measure ℝ

The Stieltjes second-derivative measure associated to the project-local right derivative, under a global monotonicity hypothesis.

The convex source proof will eventually supply this by applying the construction to a monotone extension of the right derivative from (-3,3).

Equations

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

@[simp]

theorem AleksandrovDifferentiability.monotoneStieltjesSecondDerivativeFunction_apply {g : ℝ → ℝ} (hg : Monotone g) (x : ℝ) : ↑(monotoneStieltjesSecondDerivativeFunction g hg) x = Function.rightLim g x

@[simp]

theorem AleksandrovDifferentiability.monotoneStieltjesSecondDerivativeMeasure_Ioc {g : ℝ → ℝ} (hg : Monotone g) (a b : ℝ) : (monotoneStieltjesSecondDerivativeMeasure g hg) (Set.Ioc a b) = ENNReal.ofReal (↑(monotoneStieltjesSecondDerivativeFunction g hg) b - ↑(monotoneStieltjesSecondDerivativeFunction g hg) a)

@[simp]

theorem AleksandrovDifferentiability.rightDerivStieltjesSecondDerivativeMeasure_Ioc {v : ℝ → ℝ} (hmono : Monotone (rightDeriv v)) (a b : ℝ) : (rightDerivStieltjesSecondDerivativeMeasure v hmono) (Set.Ioc a b) = ENNReal.ofReal (↑(rightDerivStieltjesSecondDerivativeFunction v hmono) b - ↑(rightDerivStieltjesSecondDerivativeFunction v hmono) a)

@[simp]

theorem AleksandrovDifferentiability.monotoneStieltjesSecondDerivativeMeasure_sourceMaximalDomain {g : ℝ → ℝ} (hg : Monotone g) : (monotoneStieltjesSecondDerivativeMeasure g hg) sourceMaximalDomain = ENNReal.ofReal (Function.leftLim (↑(monotoneStieltjesSecondDerivativeFunction g hg)) 2 - ↑(monotoneStieltjesSecondDerivativeFunction g hg) (-2))

@[simp]

theorem AleksandrovDifferentiability.rightDerivStieltjesSecondDerivativeMeasure_sourceMaximalDomain {v : ℝ → ℝ} (hmono : Monotone (rightDeriv v)) : (rightDerivStieltjesSecondDerivativeMeasure v hmono) sourceMaximalDomain = ENNReal.ofReal (Function.leftLim (↑(rightDerivStieltjesSecondDerivativeFunction v hmono)) 2 - ↑(rightDerivStieltjesSecondDerivativeFunction v hmono) (-2))

Source-local right-derivative extension

def AleksandrovDifferentiability.sourceDerivativeClamp (s : ℝ) : ℝ

Clamp a real parameter to the closed source interval [-2,2].

This is used to turn the right derivative, known to be monotone only on the source line interval, into a globally monotone function to which Mathlib's Stieltjes construction applies.

Equations

• AleksandrovDifferentiability.sourceDerivativeClamp s = max (-2) (min 2 s)

theorem AleksandrovDifferentiability.sourceDerivativeClamp_mem_Icc (s : ℝ) : sourceDerivativeClamp s ∈ Set.Icc (-2) 2

theorem AleksandrovDifferentiability.monotone_sourceDerivativeClamp : Monotone sourceDerivativeClamp

theorem AleksandrovDifferentiability.sourceDerivativeClamp_eq_of_mem_sourceMaximalDomain {s : ℝ} (hs : s ∈ sourceMaximalDomain) : sourceDerivativeClamp s = s

noncomputable def AleksandrovDifferentiability.sourceRightDerivExtension (v : ℝ → ℝ) (s : ℝ) : ℝ

The source-local right derivative extended to all of ℝ by clamping the line parameter to [-2,2].

Equations

• AleksandrovDifferentiability.sourceRightDerivExtension v s = AleksandrovDifferentiability.rightDeriv v (AleksandrovDifferentiability.sourceDerivativeClamp s)

theorem AleksandrovDifferentiability.sourceRightDerivExtension_eq_of_mem_sourceMaximalDomain {v : ℝ → ℝ} {s : ℝ} (hs : s ∈ sourceMaximalDomain) : sourceRightDerivExtension v s = rightDeriv v s

theorem AleksandrovDifferentiability.sourceDerivativeClamp_eventuallyEq_id_nhdsLT {s : ℝ} (hs : s ∈ sourceMaximalDomain) : sourceDerivativeClamp =ᶠ[nhdsWithin s (Set.Iio s)] id

To the left of a point strictly inside the source interval, the clamp is eventually the identity.

theorem AleksandrovDifferentiability.sourceDerivativeClamp_eventuallyEq_id_nhdsGT {s : ℝ} (hs : s ∈ sourceMaximalDomain) : sourceDerivativeClamp =ᶠ[nhdsWithin s (Set.Ioi s)] id

To the right of a point strictly inside the source interval, the clamp is eventually the identity.

theorem AleksandrovDifferentiability.sourceRightDerivExtension_eventuallyEq_rightDeriv_nhdsLT {v : ℝ → ℝ} {s : ℝ} (hs : s ∈ sourceMaximalDomain) : sourceRightDerivExtension v =ᶠ[nhdsWithin s (Set.Iio s)] rightDeriv v

To the left of a point strictly inside the source interval, the clamped right-derivative extension is eventually the ordinary right derivative.

theorem AleksandrovDifferentiability.sourceRightDerivExtension_eventuallyEq_rightDeriv_nhdsGT {v : ℝ → ℝ} {s : ℝ} (hs : s ∈ sourceMaximalDomain) : sourceRightDerivExtension v =ᶠ[nhdsWithin s (Set.Ioi s)] rightDeriv v

To the right of a point strictly inside the source interval, the clamped right-derivative extension is eventually the ordinary right derivative.

theorem AleksandrovDifferentiability.sourceRightDerivExtension_leftLim_eq_of_tendsto_rightDeriv_nhdsLT {v : ℝ → ℝ} {s L : ℝ} (hs : s ∈ sourceMaximalDomain) (hlim : Filter.Tendsto (rightDeriv v) (nhdsWithin s (Set.Iio s)) (nhds L)) : Function.leftLim (sourceRightDerivExtension v) s = L

A left limit of the ordinary right derivative transfers to the clamped source extension at points strictly inside the source interval.

theorem AleksandrovDifferentiability.sourceRightDerivExtension_rightLim_eq_of_tendsto_rightDeriv_nhdsGT {v : ℝ → ℝ} {s L : ℝ} (hs : s ∈ sourceMaximalDomain) (hlim : Filter.Tendsto (rightDeriv v) (nhdsWithin s (Set.Ioi s)) (nhds L)) : Function.rightLim (sourceRightDerivExtension v) s = L

A right limit of the ordinary right derivative transfers to the clamped source extension at points strictly inside the source interval.

theorem AleksandrovDifferentiability.monotone_sourceRightDerivExtension {v : ℝ → ℝ} (hmono : MonotoneOn (rightDeriv v) (Set.Icc (-2) 2)) : Monotone (sourceRightDerivExtension v)

A right derivative monotone on the source interval [-2,2] gives a globally monotone clamped extension.

noncomputable def AleksandrovDifferentiability.sourceRightDerivStieltjesSecondDerivativeFunction (v : ℝ → ℝ) (hmono : MonotoneOn (rightDeriv v) (Set.Icc (-2) 2)) : StieltjesFunction ℝ

Stieltjes function of the source-local right-derivative extension.

Equations

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

noncomputable def AleksandrovDifferentiability.sourceRightDerivStieltjesSecondDerivativeMeasure (v : ℝ → ℝ) (hmono : MonotoneOn (rightDeriv v) (Set.Icc (-2) 2)) : MeasureTheory.Measure ℝ

Stieltjes measure of the source-local right-derivative extension.

This is the source-local concrete candidate for the distributional second derivative measure used by the localized maximal argument.

Equations

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

theorem AleksandrovDifferentiability.sourceRightDerivStieltjesSecondDerivativeMeasure_Ioo_lt_top {v : ℝ → ℝ} (hmono : MonotoneOn (rightDeriv v) (Set.Icc (-2) 2)) (a b : ℝ) : (sourceRightDerivStieltjesSecondDerivativeMeasure v hmono) (Set.Ioo a b) < ⊤

The source-local Stieltjes measure has finite mass on every bounded open interval.

@[simp]

theorem AleksandrovDifferentiability.sourceRightDerivStieltjesSecondDerivativeFunction_apply {v : ℝ → ℝ} (hmono : MonotoneOn (rightDeriv v) (Set.Icc (-2) 2)) (s : ℝ) : ↑(sourceRightDerivStieltjesSecondDerivativeFunction v hmono) s = Function.rightLim (sourceRightDerivExtension v) s

theorem AleksandrovDifferentiability.sourceRightDerivStieltjesSecondDerivativeFunction_leftLim_eq_extension_leftLim {v : ℝ → ℝ} (hmono : MonotoneOn (rightDeriv v) (Set.Icc (-2) 2)) (s : ℝ) : Function.leftLim (↑(sourceRightDerivStieltjesSecondDerivativeFunction v hmono)) s = Function.leftLim (sourceRightDerivExtension v) s

The left limit of the right-continuous Stieltjes representative agrees with the left limit of the clamped right-derivative extension that generated it.

@[simp]

theorem AleksandrovDifferentiability.sourceRightDerivStieltjesSecondDerivativeMeasure_Ioc {v : ℝ → ℝ} (hmono : MonotoneOn (rightDeriv v) (Set.Icc (-2) 2)) (a b : ℝ) : (sourceRightDerivStieltjesSecondDerivativeMeasure v hmono) (Set.Ioc a b) = ENNReal.ofReal (↑(sourceRightDerivStieltjesSecondDerivativeFunction v hmono) b - ↑(sourceRightDerivStieltjesSecondDerivativeFunction v hmono) a)

@[simp]

theorem AleksandrovDifferentiability.sourceRightDerivStieltjesSecondDerivativeMeasure_sourceMaximalDomain {v : ℝ → ℝ} (hmono : MonotoneOn (rightDeriv v) (Set.Icc (-2) 2)) : (sourceRightDerivStieltjesSecondDerivativeMeasure v hmono) sourceMaximalDomain = ENNReal.ofReal (Function.leftLim (↑(sourceRightDerivStieltjesSecondDerivativeFunction v hmono)) 2 - ↑(sourceRightDerivStieltjesSecondDerivativeFunction v hmono) (-2))

noncomputable def AleksandrovDifferentiability.sourceRightDerivStieltjesSourceJump (v : ℝ → ℝ) (hmono : MonotoneOn (rightDeriv v) (Set.Icc (-2) 2)) : ℝ

The real jump of the clamped right-derivative Stieltjes function across the source maximal domain (-2,2). By the Stieltjes interval formula this is the real mass of (-2,2).

Equations

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

theorem AleksandrovDifferentiability.sourceRightDerivStieltjesSourceJump_nonneg {v : ℝ → ℝ} (hmono : MonotoneOn (rightDeriv v) (Set.Icc (-2) 2)) : 0 ≤ sourceRightDerivStieltjesSourceJump v hmono

theorem AleksandrovDifferentiability.sourceRightDerivStieltjesSourceJump_le_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) : sourceRightDerivStieltjesSourceJump v hmono ≤ 2 * osc

theorem AleksandrovDifferentiability.sourceRightDerivStieltjesSourceJump_le_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) : sourceRightDerivStieltjesSourceJump v hmono ≤ 2 * osc

theorem AleksandrovDifferentiability.sourceRightDerivStieltjesFunction_neg_two_ge_of_rightDeriv_lower {v : ℝ → ℝ} {hmono : MonotoneOn (rightDeriv v) (Set.Icc (-2) 2)} {lower : ℝ} (hlower : lower ≤ rightDeriv v (-2)) : lower ≤ ↑(sourceRightDerivStieltjesSecondDerivativeFunction v hmono) (-2)

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

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

theorem AleksandrovDifferentiability.sourceRightDerivStieltjesSecondDerivativeMeasure_real_sourceMaximalDomain {v : ℝ → ℝ} (hmono : MonotoneOn (rightDeriv v) (Set.Icc (-2) 2)) : (sourceRightDerivStieltjesSecondDerivativeMeasure v hmono).real sourceMaximalDomain = sourceRightDerivStieltjesSourceJump v hmono

theorem AleksandrovDifferentiability.sourceRightDerivStieltjesSecondDerivativeMeasure_real_Ioo {v : ℝ → ℝ} (hmono : MonotoneOn (rightDeriv v) (Set.Icc (-2) 2)) {a b : ℝ} (hab : a < b) : (sourceRightDerivStieltjesSecondDerivativeMeasure v hmono).real (Set.Ioo a b) = Function.leftLim (↑(sourceRightDerivStieltjesSecondDerivativeFunction v hmono)) b - ↑(sourceRightDerivStieltjesSecondDerivativeFunction v hmono) a

Real-valued Ioo formula for the source-local clamped right-derivative Stieltjes measure.

theorem AleksandrovDifferentiability.sourceRightDerivStieltjesSecondDerivativeMeasure_sourceMaximalDomain_lt_top {v : ℝ → ℝ} (hmono : MonotoneOn (rightDeriv v) (Set.Icc (-2) 2)) : (sourceRightDerivStieltjesSecondDerivativeMeasure v hmono) sourceMaximalDomain < ⊤

theorem AleksandrovDifferentiability.ConvexOn.monotoneOn_projectRightDeriv_sourceIcc {v : ℝ → ℝ} (hv : ConvexOn ℝ (Set.Ioo (-3) 3) v) : MonotoneOn (rightDeriv v) (Set.Icc (-2) 2)

Convexity on (-3,3) supplies the monotonicity of the project-local right derivative on the clamped source interval [-2,2].

theorem AleksandrovDifferentiability.exists_right_secant_two_le_add_of_pairwise_sub_le {v : ℝ → ℝ} {osc ε : ℝ} (hosc : 0 ≤ osc) (hε : 0 < ε) (hbound : ∀ ⦃x y : ℝ⦄, x ∈ Set.Ioo (-3) 3 → y ∈ Set.Ioo (-3) 3 → v y - v x ≤ osc) : ∃ y ∈ Set.Ioo 2 3, slope v 2 y ≤ osc + ε

If all value differences on (-3,3) are bounded above by osc, then a forward secant from 2 to a point near 3 has slope at most osc + ε.

This is the elementary endpoint step used in the source proof to turn bounded oscillation into right-derivative control.

theorem AleksandrovDifferentiability.exists_neg_add_le_left_secant_neg_two_of_pairwise_sub_le {v : ℝ → ℝ} {osc ε : ℝ} (hosc : 0 ≤ osc) (hε : 0 < ε) (hbound : ∀ ⦃x y : ℝ⦄, x ∈ Set.Ioo (-3) 3 → y ∈ Set.Ioo (-3) 3 → v y - v x ≤ osc) : ∃ y ∈ Set.Ioo (-3) (-2), -osc - ε ≤ slope v y (-2)

If all value differences on (-3,3) are bounded above by osc, then a backward secant from a point near -3 to -2 has slope at least -osc - ε.

theorem AleksandrovDifferentiability.ConvexOn.rightDeriv_two_le_of_forall_exists_secant_le_add {v : ℝ → ℝ} {osc : ℝ} (hv : ConvexOn ℝ (Set.Ioo (-3) 3) v) (hsec : ∀ (ε : ℝ), 0 < ε → ∃ y ∈ Set.Ioo 2 3, slope v 2 y ≤ osc + ε) : rightDeriv v 2 ≤ osc

Forward secants approaching the right source endpoint control the right derivative at 2.

This is the source-proof shape needed because the ambient interval is open at 3.

theorem AleksandrovDifferentiability.ConvexOn.neg_osc_le_rightDeriv_neg_two_of_forall_exists_secant_add_le {v : ℝ → ℝ} {osc : ℝ} (hv : ConvexOn ℝ (Set.Ioo (-3) 3) v) (hsec : ∀ (ε : ℝ), 0 < ε → ∃ y ∈ Set.Ioo (-3) (-2), -osc - ε ≤ slope v y (-2)) : -osc ≤ rightDeriv v (-2)

Backward secants approaching the left source endpoint control the right derivative at -2 from below.

theorem AleksandrovDifferentiability.SubgradientOn.affineRemainder_add_le_mul_rightDeriv_sub {S : Set ℝ} {v : ℝ → ℝ} {x p h : ℝ} (_hp : SubgradientOn S v x p) (hv : ConvexOn ℝ S v) (hx : x ∈ interior S) (hxh : x + h ∈ interior S) (hh : 0 ≤ h) : affineRemainder v x p (x + h) ≤ h * (rightDeriv v (x + h) - p)

Forward affine remainders of a one-dimensional convex function are controlled by the gap between the right derivative at the endpoint and the chosen subgradient.

theorem AleksandrovDifferentiability.SubgradientOn.affineRemainder_add_le_mul_leftDeriv_sub {S : Set ℝ} {v : ℝ → ℝ} {x p h : ℝ} (_hp : SubgradientOn S v x p) (hv : ConvexOn ℝ S v) (hx : x ∈ interior S) (hxh : x + h ∈ interior S) (hh : 0 ≤ h) : affineRemainder v x p (x + h) ≤ h * (leftDeriv v (x + h) - p)

Forward affine remainders of a one-dimensional convex function are controlled by the gap between the left derivative at the endpoint and the chosen subgradient.

This variant is better suited to open-interval Stieltjes masses, which see the left limit at the right endpoint.

theorem AleksandrovDifferentiability.SubgradientOn.affineRemainder_sub_le_mul_sub_rightDeriv {S : Set ℝ} {v : ℝ → ℝ} {x p h : ℝ} (_hp : SubgradientOn S v x p) (hv : ConvexOn ℝ S v) (hx : x ∈ interior S) (hxmh : x - h ∈ interior S) (hh : 0 ≤ h) : affineRemainder v x p (x - h) ≤ h * (p - rightDeriv v (x - h))

Backward affine remainders of a one-dimensional convex function are controlled by the gap between the chosen subgradient and the right derivative at the left endpoint.

theorem AleksandrovDifferentiability.SubgradientOn.affineRemainder_pm_le_mul_rightDeriv_sub {S : Set ℝ} {v : ℝ → ℝ} {x p h : ℝ} (hp : SubgradientOn S v x p) (hv : ConvexOn ℝ S v) (hx : x ∈ interior S) (hxmh : x - h ∈ interior S) (hxph : x + h ∈ interior S) (hh : 0 ≤ h) : affineRemainder v x p (x + h) ≤ h * (rightDeriv v (x + h) - rightDeriv v (x - h)) ∧ affineRemainder v x p (x - h) ≤ h * (rightDeriv v (x + h) - rightDeriv v (x - h))

Two-sided affine remainders of a one-dimensional convex function are controlled by the right-derivative variation across the symmetric interval.

theorem AleksandrovDifferentiability.SubgradientOn.affineRemainder_pm_le_mul_leftDeriv_sub_rightDeriv {S : Set ℝ} {v : ℝ → ℝ} {x p h : ℝ} (hp : SubgradientOn S v x p) (hv : ConvexOn ℝ S v) (hx : x ∈ interior S) (hxmh : x - h ∈ interior S) (hxph : x + h ∈ interior S) (hh : 0 ≤ h) : affineRemainder v x p (x + h) ≤ h * (leftDeriv v (x + h) - rightDeriv v (x - h)) ∧ affineRemainder v x p (x - h) ≤ h * (leftDeriv v (x + h) - rightDeriv v (x - h))

Two-sided affine remainders of a one-dimensional convex function are controlled by the open-interval derivative variation from the right derivative at the left endpoint to the left derivative at the right endpoint.