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

Averaged one-dimensional remainders

This file begins the interval-integral route to the remaining one-dimensional averaging lemma. The first named fact records the exact integral of the linear model that will appear after linearizing the right derivative.

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

Local interval-integral representation of the affine remainder using the project-local right derivative increment. For convex functions this should follow from FTC for one-sided derivatives.

Equations

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

def AleksandrovDifferentiability.HasRightDerivIntegralLinearizationAt (f : ℝ → ℝ) (x q : ℝ) : Prop

The integral of the right-derivative increment is locally modeled by the integral of the linearized derivative increment. This is the estimate supplied by differentiability of rightDeriv f once interval-integral bounds are available.

Equations

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

theorem AleksandrovDifferentiability.eventually_uIcc_subset_of_mem_nhds {x : ℝ} {U : Set ℝ} (hU : U ∈ nhds x) : ∀ᶠ (z : ℝ) in nhds 0, Set.uIcc x (x + z) ⊆ U

If U is a neighborhood of x, then every sufficiently short interval from x to x + z is contained in U.

theorem AleksandrovDifferentiability.intervalIntegral_linear_deriv_model (x z q : ℝ) : ∫ (t : ℝ) in x..x + z, q * (t - x) = 1 / 2 * q * z ^ 2

Integral of the affine derivative model along the interval from x to x + z.

theorem AleksandrovDifferentiability.norm_unit_interval_remainder_le_of_integral_model_bound {f g : ℝ → ℝ} {a q R : ℝ} (hrepr : f 1 - f 0 = ∫ (t : ℝ) in 0..1, g t) (hint : IntervalIntegrable g MeasureTheory.volume 0 1) (hbound : ∀ t ∈ Set.uIoc 0 1, ‖g t - (a + t * q)‖ ≤ R) : ‖f 1 - f 0 - a - 1 / 2 * q‖ ≤ R

If an integrand on [0,1] is uniformly close to the affine model a + t q, then its integral is close to a + q / 2.

This is the calculus bookkeeping in the source proof's final line-segment integration: once the right derivative of the line restriction is controlled by the linear model, the endpoint increment has the corresponding quadratic model.

theorem AleksandrovDifferentiability.eventually_norm_half_rightDeriv_increment_sub_linear_model_le {S : Set ℝ} {f : ℝ → ℝ} {x q : ℝ} (hx : x ∈ interior S) (hderiv : HasDerivWithinAt (rightDeriv f) q (interior S) x) (ε : ℝ) : 0 < ε → ∀ᶠ (z : ℝ) in nhds 0, ‖1 / 2 * (rightDeriv f (x + z) - rightDeriv f x) * z - 1 / 2 * q * z ^ 2‖ ≤ ε * ‖z‖ ^ 2

Differentiability of the project-local right derivative controls the endpoint average of its increment by the linear model.

theorem AleksandrovDifferentiability.ConvexOn.eventually_intervalIntegrable_rightDeriv {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} (hf : ConvexOn ℝ S f) (hx : x ∈ interior S) : ∀ᶠ (z : ℝ) in nhds 0, IntervalIntegrable (rightDeriv f) MeasureTheory.volume x (x + z)

Near an interior point of a one-dimensional convex domain, the project-local right derivative is interval-integrable on the small interval from x to x + z.

theorem AleksandrovDifferentiability.ConvexOn.intervalIntegrable_rightDeriv_of_uIcc_subset_interior {S : Set ℝ} {f : ℝ → ℝ} {a b : ℝ} (hf : ConvexOn ℝ S f) (hinterval : Set.uIcc a b ⊆ interior S) : IntervalIntegrable (rightDeriv f) MeasureTheory.volume a b

If the whole interval between a and b lies in the interior of a one-dimensional convex domain, then the right derivative is interval-integrable on that interval.

theorem AleksandrovDifferentiability.ConvexOn.eventually_integral_rightDeriv_eq_sub {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} (hf : ConvexOn ℝ S f) (hx : x ∈ interior S) : ∀ᶠ (z : ℝ) in nhds 0, ∫ (t : ℝ) in x..x + z, rightDeriv f t = f (x + z) - f x

Local right-derivative FTC identity for a one-dimensional convex function at an interior point.

theorem AleksandrovDifferentiability.ConvexOn.integral_rightDeriv_eq_sub_of_uIcc_subset_interior {S : Set ℝ} {f : ℝ → ℝ} {a b : ℝ} (hf : ConvexOn ℝ S f) (hinterval : Set.uIcc a b ⊆ interior S) : ∫ (t : ℝ) in a..b, rightDeriv f t = f b - f a

Right-derivative FTC identity on any interval contained in the interior of a one-dimensional convex domain.

theorem AleksandrovDifferentiability.ConvexOn.hasRightDerivIntegralRemainderAt {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} (hf : ConvexOn ℝ S f) (hx : x ∈ interior S) : HasRightDerivIntegralRemainderAt f x

Local affine-remainder integral representation for a one-dimensional convex function at an interior point.

theorem AleksandrovDifferentiability.hasRightDerivIntegralLinearizationAt_of_hasDerivWithinAt_of_eventually_intervalIntegrable {S : Set ℝ} {f : ℝ → ℝ} {x q : ℝ} (hx : x ∈ interior S) (hderiv : HasDerivWithinAt (rightDeriv f) q (interior S) x) (hint : ∀ᶠ (z : ℝ) in nhds 0, IntervalIntegrable (rightDeriv f) MeasureTheory.volume x (x + z)) : HasRightDerivIntegralLinearizationAt f x q

Differentiability of rightDeriv f, together with local interval integrability of rightDeriv f, gives the integral linearization estimate. The extra integrability hypothesis is the part later supplied by convexity, via monotonicity of one-sided derivatives.

theorem AleksandrovDifferentiability.ConvexOn.hasRightDerivIntegralLinearizationAt_of_hasDerivWithinAt {S : Set ℝ} {f : ℝ → ℝ} {x q : ℝ} (hf : ConvexOn ℝ S f) (hx : x ∈ interior S) (hderiv : HasDerivWithinAt (rightDeriv f) q (interior S) x) : HasRightDerivIntegralLinearizationAt f x q

For a one-dimensional convex function, differentiability of the project-local right derivative within the interior gives the integral linearization estimate.

theorem AleksandrovDifferentiability.hasRightDerivAverageRemainderAt_of_integral_linearization {S : Set ℝ} {f : ℝ → ℝ} {x q : ℝ} (hx : x ∈ interior S) (hrepr : HasRightDerivIntegralRemainderAt f x) (hlin : HasRightDerivIntegralLinearizationAt f x q) (hderiv : HasDerivWithinAt (rightDeriv f) q (interior S) x) : HasRightDerivAverageRemainderAt f x

If the affine remainder has the interval-integral representation and that integral is quadratically close to the linearized right-derivative model, then differentiability of the right derivative gives the averaged endpoint-remainder estimate.

theorem AleksandrovDifferentiability.ConvexOn.hasRightDerivAverageRemainderAt_of_integralRemainder_of_hasDerivWithinAt {S : Set ℝ} {f : ℝ → ℝ} {x q : ℝ} (hf : ConvexOn ℝ S f) (hx : x ∈ interior S) (hrepr : HasRightDerivIntegralRemainderAt f x) (hderiv : HasDerivWithinAt (rightDeriv f) q (interior S) x) : HasRightDerivAverageRemainderAt f x

For a convex one-dimensional function, the local affine-remainder integral representation is the only remaining ingredient needed to obtain the averaged right-derivative remainder estimate at points where the right derivative is differentiable within the interior.

theorem AleksandrovDifferentiability.ConvexOn.hasRightDerivAverageRemainderAt_of_good_of_integralRemainder {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} (hf : ConvexOn ℝ S f) (hx : x ∈ interior S) (hgood : x ∈ oneSidedDerivDifferentiabilitySet S f) (hrepr : HasRightDerivIntegralRemainderAt f x) : HasRightDerivAverageRemainderAt f x

Derivative-good points of a convex one-dimensional function satisfy the averaged right-derivative remainder estimate once the local affine-remainder integral representation is known there.