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

One-dimensional convex analysis

This file gives project-local names for the one-dimensional slope and one-sided derivative facts used at the start of the convex Aleksandrov proof route.

noncomputable def AleksandrovDifferentiability.rightDeriv (f : ℝ → ℝ) (x : ℝ) : ℝ

The right derivative of a real function at x, represented by Mathlib's derivative within the open ray to the right of x.

Equations

• AleksandrovDifferentiability.rightDeriv f x = derivWithin f (Set.Ioi x) x

noncomputable def AleksandrovDifferentiability.leftDeriv (f : ℝ → ℝ) (x : ℝ) : ℝ

The left derivative of a real function at x, represented by Mathlib's derivative within the open ray to the left of x.

Equations

• AleksandrovDifferentiability.leftDeriv f x = derivWithin f (Set.Iio x) x

def AleksandrovDifferentiability.rightDerivDifferentiabilitySet (S : Set ℝ) (f : ℝ → ℝ) : Set ℝ

The set where the project-local right derivative is differentiable within the interior of the one-dimensional domain.

Equations

• AleksandrovDifferentiability.rightDerivDifferentiabilitySet S f = {x : ℝ | DifferentiableWithinAt ℝ (AleksandrovDifferentiability.rightDeriv f) (interior S) x}

def AleksandrovDifferentiability.leftDerivDifferentiabilitySet (S : Set ℝ) (f : ℝ → ℝ) : Set ℝ

The set where the project-local left derivative is differentiable within the interior of the one-dimensional domain.

Equations

• AleksandrovDifferentiability.leftDerivDifferentiabilitySet S f = {x : ℝ | DifferentiableWithinAt ℝ (AleksandrovDifferentiability.leftDeriv f) (interior S) x}

def AleksandrovDifferentiability.oneSidedDerivDifferentiabilitySet (S : Set ℝ) (f : ℝ → ℝ) : Set ℝ

The set where both project-local one-sided derivative functions are differentiable within the interior of the one-dimensional domain.

Equations

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

def AleksandrovDifferentiability.HasRightDerivAverageRemainderAt (f : ℝ → ℝ) (x : ℝ) : Prop

The local estimate saying that the affine remainder is asymptotically the average of the endpoint right-derivative increment times the displacement.

For convex functions this is the one-dimensional averaging ingredient that remains between the currently formalized derivative-good information and the final scalar quadratic Taylor estimate.

Equations

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

def AleksandrovDifferentiability.rightDerivAverageRemainderSet (f : ℝ → ℝ) : Set ℝ

Points where the averaged right-derivative remainder estimate holds.

Equations

• AleksandrovDifferentiability.rightDerivAverageRemainderSet f = {x : ℝ | AleksandrovDifferentiability.HasRightDerivAverageRemainderAt f x}

@[simp]

theorem AleksandrovDifferentiability.mem_rightDerivDifferentiabilitySet {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} : x ∈ rightDerivDifferentiabilitySet S f ↔ DifferentiableWithinAt ℝ (rightDeriv f) (interior S) x

@[simp]

theorem AleksandrovDifferentiability.mem_leftDerivDifferentiabilitySet {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} : x ∈ leftDerivDifferentiabilitySet S f ↔ DifferentiableWithinAt ℝ (leftDeriv f) (interior S) x

@[simp]

theorem AleksandrovDifferentiability.mem_oneSidedDerivDifferentiabilitySet {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} : x ∈ oneSidedDerivDifferentiabilitySet S f ↔ DifferentiableWithinAt ℝ (rightDeriv f) (interior S) x ∧ DifferentiableWithinAt ℝ (leftDeriv f) (interior S) x

@[simp]

theorem AleksandrovDifferentiability.mem_rightDerivAverageRemainderSet {f : ℝ → ℝ} {x : ℝ} : x ∈ rightDerivAverageRemainderSet f ↔ HasRightDerivAverageRemainderAt f x

theorem AleksandrovDifferentiability.ConvexOn.hasDerivWithinAt_rightDeriv {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} (hf : ConvexOn ℝ S f) (hx : x ∈ interior S) : HasDerivWithinAt f (rightDeriv f x) (Set.Ioi x) x

A convex function has the project-local right derivative at interior points.

theorem AleksandrovDifferentiability.ConvexOn.hasDerivWithinAt_leftDeriv {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} (hf : ConvexOn ℝ S f) (hx : x ∈ interior S) : HasDerivWithinAt f (leftDeriv f x) (Set.Iio x) x

A convex function has the project-local left derivative at interior points.

theorem AleksandrovDifferentiability.ConvexOn.monotoneOn_projectRightDeriv {S : Set ℝ} {f : ℝ → ℝ} (hf : ConvexOn ℝ S f) : MonotoneOn (rightDeriv f) (interior S)

Right derivatives of a one-dimensional convex function are monotone on the interior.

theorem AleksandrovDifferentiability.ConvexOn.monotoneOn_projectLeftDeriv {S : Set ℝ} {f : ℝ → ℝ} (hf : ConvexOn ℝ S f) : MonotoneOn (leftDeriv f) (interior S)

Left derivatives of a one-dimensional convex function are monotone on the interior.

theorem AleksandrovDifferentiability.ConvexOn.ae_differentiableWithinAt_projectRightDeriv_of_mem {S : Set ℝ} {f : ℝ → ℝ} (hf : ConvexOn ℝ S f) : ∀ᵐ (x : ℝ), x ∈ interior S → DifferentiableWithinAt ℝ (rightDeriv f) (interior S) x

The project-local right derivative of a one-dimensional convex function is differentiable almost everywhere on the interior, in implication form.

theorem AleksandrovDifferentiability.ConvexOn.ae_differentiableWithinAt_projectLeftDeriv_of_mem {S : Set ℝ} {f : ℝ → ℝ} (hf : ConvexOn ℝ S f) : ∀ᵐ (x : ℝ), x ∈ interior S → DifferentiableWithinAt ℝ (leftDeriv f) (interior S) x

The project-local left derivative of a one-dimensional convex function is differentiable almost everywhere on the interior, in implication form.

theorem AleksandrovDifferentiability.ConvexOn.ae_differentiableWithinAt_projectRightDeriv {S : Set ℝ} {f : ℝ → ℝ} (hf : ConvexOn ℝ S f) (hS : MeasurableSet (interior S)) : ∀ᵐ (x : ℝ) ∂MeasureTheory.volume.restrict (interior S), DifferentiableWithinAt ℝ (rightDeriv f) (interior S) x

Restricted-measure version of ConvexOn.ae_differentiableWithinAt_projectRightDeriv_of_mem.

theorem AleksandrovDifferentiability.ConvexOn.ae_differentiableWithinAt_projectLeftDeriv {S : Set ℝ} {f : ℝ → ℝ} (hf : ConvexOn ℝ S f) (hS : MeasurableSet (interior S)) : ∀ᵐ (x : ℝ) ∂MeasureTheory.volume.restrict (interior S), DifferentiableWithinAt ℝ (leftDeriv f) (interior S) x

Restricted-measure version of ConvexOn.ae_differentiableWithinAt_projectLeftDeriv_of_mem.

theorem AleksandrovDifferentiability.ConvexOn.ae_mem_oneSidedDerivDifferentiabilitySet_of_mem {S : Set ℝ} {f : ℝ → ℝ} (hf : ConvexOn ℝ S f) : ∀ᵐ (x : ℝ), x ∈ interior S → x ∈ oneSidedDerivDifferentiabilitySet S f

Both project-local one-sided derivative functions are differentiable within the interior almost everywhere, in implication form.

theorem AleksandrovDifferentiability.ConvexOn.ae_mem_oneSidedDerivDifferentiabilitySet {S : Set ℝ} {f : ℝ → ℝ} (hf : ConvexOn ℝ S f) (hS : MeasurableSet (interior S)) : ∀ᵐ (x : ℝ) ∂MeasureTheory.volume.restrict (interior S), x ∈ oneSidedDerivDifferentiabilitySet S f

Restricted-measure version of ConvexOn.ae_mem_oneSidedDerivDifferentiabilitySet_of_mem.

theorem AleksandrovDifferentiability.ConvexOn.measure_interior_diff_rightDerivDifferentiabilitySet_eq_zero {S : Set ℝ} {f : ℝ → ℝ} (hf : ConvexOn ℝ S f) : MeasureTheory.volume (interior S \ rightDerivDifferentiabilitySet S f) = 0

The exceptional set inside the interior where the project-local right derivative is not differentiable has zero Lebesgue measure.

theorem AleksandrovDifferentiability.ConvexOn.measure_interior_diff_leftDerivDifferentiabilitySet_eq_zero {S : Set ℝ} {f : ℝ → ℝ} (hf : ConvexOn ℝ S f) : MeasureTheory.volume (interior S \ leftDerivDifferentiabilitySet S f) = 0

The exceptional set inside the interior where the project-local left derivative is not differentiable has zero Lebesgue measure.

theorem AleksandrovDifferentiability.ConvexOn.measure_interior_diff_oneSidedDerivDifferentiabilitySet_eq_zero {S : Set ℝ} {f : ℝ → ℝ} (hf : ConvexOn ℝ S f) : MeasureTheory.volume (interior S \ oneSidedDerivDifferentiabilitySet S f) = 0

The exceptional set inside the interior where one of the one-sided derivative functions is not differentiable has zero Lebesgue measure.

theorem AleksandrovDifferentiability.ConvexOn.measure_interior_diff_oneSided_eq_zero {S : Set ℝ} {f : ℝ → ℝ} (hf : ConvexOn ℝ S f) : MeasureTheory.volume (interior S \ oneSidedDerivDifferentiabilitySet S f) = 0

Short-name alias for the null exceptional set where one of the one-sided derivative functions is not differentiable.

theorem AleksandrovDifferentiability.ConvexOn.leftDeriv_le_rightDeriv {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} (hf : ConvexOn ℝ S f) (hx : x ∈ interior S) : leftDeriv f x ≤ rightDeriv f x

The left derivative is bounded by the right derivative at an interior point of a convex function.

theorem AleksandrovDifferentiability.ConvexOn.rightDeriv_le_slope {S : Set ℝ} {f : ℝ → ℝ} {x y : ℝ} (hf : ConvexOn ℝ S f) (hx : x ∈ interior S) (hy : y ∈ S) (hxy : x < y) : rightDeriv f x ≤ slope f x y

At an interior point, the right derivative is bounded above by every forward secant slope.

theorem AleksandrovDifferentiability.ConvexOn.slope_le_leftDeriv {S : Set ℝ} {f : ℝ → ℝ} {x y : ℝ} (hf : ConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ interior S) (hxy : x < y) : slope f x y ≤ leftDeriv f y

At an interior point, every backward secant slope is bounded above by the left derivative.

theorem AleksandrovDifferentiability.ConvexOn.tendsto_rightDeriv_nhdsGT {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} (hf : ConvexOn ℝ S f) (hx : x ∈ interior S) : Filter.Tendsto (rightDeriv f) (nhdsWithin x (Set.Ioi x)) (nhds (rightDeriv f x))

The project-local right derivative of a one-dimensional convex function is right-continuous at interior points.

theorem AleksandrovDifferentiability.ConvexOn.tendsto_rightDeriv_nhdsLT_leftDeriv {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} (hf : ConvexOn ℝ S f) (hx : x ∈ interior S) : Filter.Tendsto (rightDeriv f) (nhdsWithin x (Set.Iio x)) (nhds (leftDeriv f x))

The left limit of the project-local right derivative of a one-dimensional convex function is the project-local left derivative at interior points.

theorem AleksandrovDifferentiability.ConvexOn.norm_sub_linear_rightDeriv_le_norm_mul_rightDeriv_sub {S : Set ℝ} {f : ℝ → ℝ} {x y : ℝ} (hf : ConvexOn ℝ S f) (hx : x ∈ interior S) (hy : y ∈ interior S) : ‖f y - f x - rightDeriv f x * (y - x)‖ ≤ ‖y - x‖ * ‖rightDeriv f y - rightDeriv f x‖

Convex secant control by the variation of the project-local right derivative.

This is a pointwise estimate for the affine remainder with slope rightDeriv f x. It is weaker than the final scalar quadratic Taylor estimate, but it is the basic convex inequality used to turn differentiability of rightDeriv f into local quadratic control of the original function.

theorem AleksandrovDifferentiability.ConvexOn.rightDeriv_le_leftDeriv_of_continuousWithinAt_rightDeriv {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} (hf : ConvexOn ℝ S f) (hx : x ∈ interior S) (hcont : ContinuousWithinAt (rightDeriv f) (interior S) x) : rightDeriv f x ≤ leftDeriv f x

If the right derivative of a one-dimensional convex function is continuous within the interior at x, then the usual convex gap between the left and right derivatives closes from the opposite direction.

theorem AleksandrovDifferentiability.ConvexOn.leftDeriv_eq_rightDeriv_of_continuousWithinAt_rightDeriv {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} (hf : ConvexOn ℝ S f) (hx : x ∈ interior S) (hcont : ContinuousWithinAt (rightDeriv f) (interior S) x) : leftDeriv f x = rightDeriv f x

Continuity within the interior of the right derivative identifies the two one-sided derivatives of a one-dimensional convex function.

theorem AleksandrovDifferentiability.ConvexOn.hasDerivAt_rightDeriv_of_continuousWithinAt_rightDeriv {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} (hf : ConvexOn ℝ S f) (hx : x ∈ interior S) (hcont : ContinuousWithinAt (rightDeriv f) (interior S) x) : HasDerivAt f (rightDeriv f x) x

At an interior point of a one-dimensional convex function, continuity within the interior of the right derivative upgrades the two one-sided derivative statements to an ordinary derivative.

theorem AleksandrovDifferentiability.ConvexOn.hasDerivAt_rightDeriv_of_mem_oneSidedDerivDifferentiabilitySet {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} (hf : ConvexOn ℝ S f) (hx : x ∈ interior S) (hgood : x ∈ oneSidedDerivDifferentiabilitySet S f) : HasDerivAt f (rightDeriv f x) x

Points where the project-local one-sided derivatives are differentiable within the interior are ordinary differentiability points of the original convex function.

theorem AleksandrovDifferentiability.ConvexOn.differentiableAt_of_mem_oneSidedDerivDifferentiabilitySet {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} (hf : ConvexOn ℝ S f) (hx : x ∈ interior S) (hgood : x ∈ oneSidedDerivDifferentiabilitySet S f) : DifferentiableAt ℝ f x

Set-level differentiability consequence of belonging to the one-sided derivative-good set.

theorem AleksandrovDifferentiability.ConvexOn.interior_inter_oneSidedDerivDifferentiabilitySet_subset_differentiabilitySet {S : Set ℝ} {f : ℝ → ℝ} (hf : ConvexOn ℝ S f) : interior S ∩ oneSidedDerivDifferentiabilitySet S f ⊆ {x : ℝ | DifferentiableAt ℝ f x}

Set-level version of the differentiability consequence for the one-sided derivative-good set.

theorem AleksandrovDifferentiability.ConvexOn.exists_eventually_norm_sub_linear_rightDeriv_le_const_mul_norm_sq {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} (hf : ConvexOn ℝ S f) (hx : x ∈ interior S) (hgood : x ∈ oneSidedDerivDifferentiabilitySet S f) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ᶠ (z : ℝ) in nhds 0, ‖f (x + z) - f x - rightDeriv f x * z‖ ≤ C * ‖z‖ ^ 2

At a derivative-good interior point of a one-dimensional convex function, subtracting the tangent line with slope rightDeriv f x leaves a locally quadratically bounded remainder.

This is a Big-O type consequence of differentiability of the one-sided derivative. The final scalar Aleksandrov estimate still needs the sharper averaged statement with the coefficient (1 / 2) * q.

theorem AleksandrovDifferentiability.SubgradientOn.le_rightDeriv_of_convex {S : Set ℝ} {f : ℝ → ℝ} {x p : ℝ} (hp : SubgradientOn S f x p) (hf : ConvexOn ℝ S f) (hx : x ∈ interior S) : p ≤ rightDeriv f x

A one-dimensional subgradient at an interior point is bounded above by the right derivative.

theorem AleksandrovDifferentiability.SubgradientOn.leftDeriv_le_of_convex {S : Set ℝ} {f : ℝ → ℝ} {x p : ℝ} (hp : SubgradientOn S f x p) (hf : ConvexOn ℝ S f) (hx : x ∈ interior S) : leftDeriv f x ≤ p

The left derivative is bounded above by any one-dimensional subgradient at an interior point.

theorem AleksandrovDifferentiability.ConvexOn.subgradientOn_of_leftDeriv_le_of_le_rightDeriv {S : Set ℝ} {f : ℝ → ℝ} {x p : ℝ} (hf : ConvexOn ℝ S f) (hx : x ∈ interior S) (hl : leftDeriv f x ≤ p) (hr : p ≤ rightDeriv f x) : SubgradientOn S f x p

Conversely, a slope lying between the left and right derivatives of a one-dimensional convex function at an interior point is a subgradient.

theorem AleksandrovDifferentiability.ConvexOn.subgradientOn_iff_leftDeriv_le_and_le_rightDeriv {S : Set ℝ} {f : ℝ → ℝ} {x p : ℝ} (hf : ConvexOn ℝ S f) (hx : x ∈ interior S) : SubgradientOn S f x p ↔ leftDeriv f x ≤ p ∧ p ≤ rightDeriv f x

At an interior point of a one-dimensional convex function, being a subgradient is equivalent to lying between the left and right derivatives.

theorem AleksandrovDifferentiability.ConvexOn.subgradientOn_of_hasDerivAt {S : Set ℝ} {f : ℝ → ℝ} {x p : ℝ} (hf : ConvexOn ℝ S f) (hx : x ∈ interior S) (hd : HasDerivAt f p x) : SubgradientOn S f x p

At a differentiability point of a one-dimensional convex function, the ordinary derivative is the subgradient slope.

theorem AleksandrovDifferentiability.HasUpperContactWithSlopeOn.slope_le_of_lt {S : Set ℝ} {f : ℝ → ℝ} {x y p a : ℝ} (h : HasUpperContactWithSlopeOn S f x p a) (hy : y ∈ S) (hxy : x < y) : slope f x y ≤ p + a / 2 * (y - x)

A one-dimensional upper quadratic contact gives an upper bound on forward secant slopes.

theorem AleksandrovDifferentiability.HasUpperContactWithSlopeOn.le_slope_of_lt {S : Set ℝ} {f : ℝ → ℝ} {x y p a : ℝ} (h : HasUpperContactWithSlopeOn S f x p a) (hy : y ∈ S) (hyx : y < x) : p + a / 2 * (y - x) ≤ slope f x y

A one-dimensional upper quadratic contact gives a lower bound on backward secant slopes.

theorem AleksandrovDifferentiability.HasUpperContactWithSlopeOn.rightDeriv_le_of_convex {S : Set ℝ} {f : ℝ → ℝ} {x p a : ℝ} (h : HasUpperContactWithSlopeOn S f x p a) (hf : ConvexOn ℝ S f) (hx : x ∈ interior S) : rightDeriv f x ≤ p

At an interior point of a convex one-dimensional function, an upper quadratic contact bounds the right derivative above by the contact slope.

theorem AleksandrovDifferentiability.HasUpperContactWithSlopeOn.le_leftDeriv_of_convex {S : Set ℝ} {f : ℝ → ℝ} {x p a : ℝ} (h : HasUpperContactWithSlopeOn S f x p a) (hf : ConvexOn ℝ S f) (hx : x ∈ interior S) : p ≤ leftDeriv f x

At an interior point of a convex one-dimensional function, an upper quadratic contact bounds the contact slope above by the left derivative.

theorem AleksandrovDifferentiability.HasUpperContactWithSlopeOn.leftDeriv_eq_and_rightDeriv_eq_of_convex {S : Set ℝ} {f : ℝ → ℝ} {x p a : ℝ} (h : HasUpperContactWithSlopeOn S f x p a) (hf : ConvexOn ℝ S f) (hx : x ∈ interior S) : leftDeriv f x = p ∧ rightDeriv f x = p

A convex one-dimensional function with an upper quadratic contact at an interior point has matching one-sided derivatives there, equal to the contact slope.

theorem AleksandrovDifferentiability.HasUpperContactWithSlopeOn.subgradientOn_of_convex {S : Set ℝ} {f : ℝ → ℝ} {x p a : ℝ} (h : HasUpperContactWithSlopeOn S f x p a) (hf : ConvexOn ℝ S f) (hx : x ∈ interior S) : SubgradientOn S f x p

For a convex one-dimensional function, the slope of an upper quadratic contact at an interior point is a subgradient.