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

Quadratic trapping

This file records elementary trapping lemmas obtained by subtracting an affine function from a convex function with a lower supporting hyperplane and an upper quadratic contact.

def AleksandrovDifferentiability.affineRemainder {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (u : E → ℝ) (x p y : E) : ℝ

The error after subtracting the affine function with slope p at x.

Equations

• AleksandrovDifferentiability.affineRemainder u x p y = u y - (u x + inner ℝ p (y - x))

@[simp]

theorem AleksandrovDifferentiability.affineRemainder_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (u : E → ℝ) (x p : E) : affineRemainder u x p x = 0

theorem AleksandrovDifferentiability.ConvexOn.affineRemainder_increment {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p : E} (hu : ConvexOn ℝ s u) : ConvexOn ℝ ((fun (z : E) => x + z) ⁻¹' s) fun (z : E) => affineRemainder u x p (x + z)

The affine remainder, viewed as a function of increments z with x + z ∈ s, is convex whenever u is convex on s. This is the source proof's normalized function \tilde u(z) = u(x+z)-u(x)-p·z.

theorem AleksandrovDifferentiability.affineRemainder_comp_linearIsometryEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (e : E ≃ₗᵢ[ℝ] F) (u : E → ℝ) (x p y : E) : affineRemainder (u ∘ ⇑e.symm) (e x) (e p) (e y) = affineRemainder u x p y

Affine remainders commute with rebasing a function through a linear isometry equivalence.

theorem AleksandrovDifferentiability.SubgradientOn.affineRemainder_nonneg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p y : E} (hp : SubgradientOn s u x p) (hy : y ∈ s) : 0 ≤ affineRemainder u x p y

A subgradient makes the affine remainder nonnegative on the domain.

theorem AleksandrovDifferentiability.SubgradientOn.inner_sub_le_affineRemainder_sub {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x0 x1 p0 p1 y : E} (hp1 : SubgradientOn s u x1 p1) (hy : y ∈ s) : inner ℝ (p1 - p0) (y - x1) ≤ affineRemainder u x0 p0 y - affineRemainder u x0 p0 x1

Comparing a subgradient at x1 with an arbitrary affine slope at x0 is controlled by the change in the affine remainder based at x0.

This is the algebraic core of the source proof's good-set gradient-control step.

theorem AleksandrovDifferentiability.SubgradientOn.inner_sub_le_affineRemainder_of_nonneg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x0 x1 p0 p1 y : E} (hp1 : SubgradientOn s u x1 p1) (hy : y ∈ s) (h0 : 0 ≤ affineRemainder u x0 p0 x1) : inner ℝ (p1 - p0) (y - x1) ≤ affineRemainder u x0 p0 y

If the affine remainder based at x0 is nonnegative at x1, then the preceding comparison is bounded above by the affine remainder at y.

theorem AleksandrovDifferentiability.HasUpperContactWithSlopeOn.affineRemainder_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p y : E} {a : ℝ} (h : HasUpperContactWithSlopeOn s u x p a) (hy : y ∈ s) : affineRemainder u x p y ≤ a / 2 * ‖y - x‖ ^ 2

An upper contact with the same slope bounds the affine remainder by the quadratic opening.

theorem AleksandrovDifferentiability.affineRemainder_nonneg_and_le_of_subgradient_of_upperContact {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p y : E} {a : ℝ} (hp : SubgradientOn s u x p) (h : HasUpperContactWithSlopeOn s u x p a) (hy : y ∈ s) : 0 ≤ affineRemainder u x p y ∧ affineRemainder u x p y ≤ a / 2 * ‖y - x‖ ^ 2

If the same slope gives a lower support and an upper quadratic contact, then the affine remainder is trapped between 0 and the quadratic opening.

theorem AleksandrovDifferentiability.abs_affineRemainder_le_of_nonneg_and_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x p y : E} {C : ℝ} (h0 : 0 ≤ affineRemainder u x p y) (hC : affineRemainder u x p y ≤ C) : |affineRemainder u x p y| ≤ C

A two-sided affine-remainder trap gives an absolute-value upper bound.

theorem AleksandrovDifferentiability.norm_affineRemainder_le_of_nonneg_and_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x p y : E} {C : ℝ} (h0 : 0 ≤ affineRemainder u x p y) (hC : affineRemainder u x p y ≤ C) : ‖affineRemainder u x p y‖ ≤ C

A two-sided affine-remainder trap gives a norm upper bound.

theorem AleksandrovDifferentiability.affineRemainder_div_norm_sq_le_of_nonneg_and_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x p y : E} {C : ℝ} (h0 : 0 ≤ affineRemainder u x p y) (hC : affineRemainder u x p y ≤ C * ‖y - x‖ ^ 2) (hyx : y ≠ x) : ‖affineRemainder u x p y‖ / ‖y - x‖ ^ 2 ≤ C

A quadratic trap gives a normalized affine-remainder bound away from the base point.

theorem AleksandrovDifferentiability.affineRemainder_nonneg_and_le_of_subgradient_of_upperContactOpening {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p y : E} {A η : ℝ} (hp : SubgradientOn s u x p) (h : HasUpperContactWithSlopeOpeningAtMostOn s u x p A) (hη : 0 < η) (hy : y ∈ s) : 0 ≤ affineRemainder u x p y ∧ affineRemainder u x p y ≤ (A + η) / 2 * ‖y - x‖ ^ 2

Approximate quadratic trapping from a fixed-slope upper-contact opening bound.

theorem AleksandrovDifferentiability.norm_affineRemainder_le_of_subgradient_of_upperContactOpening {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p y : E} {A η : ℝ} (hp : SubgradientOn s u x p) (h : HasUpperContactWithSlopeOpeningAtMostOn s u x p A) (hη : 0 < η) (hy : y ∈ s) : ‖affineRemainder u x p y‖ ≤ (A + η) / 2 * ‖y - x‖ ^ 2

Norm bound from a fixed-slope upper-contact opening trap.

theorem AleksandrovDifferentiability.affineRemainder_norm_div_norm_sq_le_of_subgradient_of_upperContactOpening {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p y : E} {A η : ℝ} (hp : SubgradientOn s u x p) (h : HasUpperContactWithSlopeOpeningAtMostOn s u x p A) (hη : 0 < η) (hy : y ∈ s) (hyx : y ≠ x) : ‖affineRemainder u x p y‖ / ‖y - x‖ ^ 2 ≤ (A + η) / 2

Normalized affine-remainder bound from a fixed-slope upper-contact opening trap.

theorem AleksandrovDifferentiability.exists_affineRemainder_trap_of_upperContactOpening_of_convex_of_mem_interior {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x y : E} {A η : ℝ} (h : HasUpperContactOpeningAtMostOn s u x A) (hu : ConvexOn ℝ s u) (hx : x ∈ interior s) (hη : 0 < η) (hy : y ∈ s) : ∃ (p : E), SubgradientOn s u x p ∧ HasUpperContactWithSlopeOn s u x p (A + η) ∧ 0 ≤ affineRemainder u x p y ∧ affineRemainder u x p y ≤ (A + η) / 2 * ‖y - x‖ ^ 2

For convex functions, a non-fixed upper-contact opening bound gives an existential affine remainder trap with a slope that is both a subgradient and an upper-contact slope.

theorem AleksandrovDifferentiability.exists_uniform_affineRemainder_trap_of_upperContactOpening_of_convex_of_mem_interior {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x : E} {A : ℝ} (h : HasUpperContactOpeningAtMostOn s u x A) (hu : ConvexOn ℝ s u) (hx : x ∈ interior s) : ∃ (p : E), SubgradientOn s u x p ∧ HasUpperContactWithSlopeOpeningAtMostOn s u x p A ∧ ∀ (η : ℝ), 0 < η → ∀ y ∈ s, 0 ≤ affineRemainder u x p y ∧ affineRemainder u x p y ≤ (A + η) / 2 * ‖y - x‖ ^ 2

For convex functions, a non-fixed upper-contact opening bound gives a single slope that traps the affine remainder for every larger opening.

theorem AleksandrovDifferentiability.exists_uniform_affineRemainder_norm_div_norm_sq_le_of_upperContactOpening_of_convex {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x : E} {A : ℝ} (h : HasUpperContactOpeningAtMostOn s u x A) (hu : ConvexOn ℝ s u) (hx : x ∈ interior s) : ∃ (p : E), SubgradientOn s u x p ∧ HasUpperContactWithSlopeOpeningAtMostOn s u x p A ∧ ∀ (η : ℝ), 0 < η → ∀ y ∈ s, y ≠ x → ‖affineRemainder u x p y‖ / ‖y - x‖ ^ 2 ≤ (A + η) / 2

Uniform normalized affine-remainder bound from ordinary bounded upper-contact opening in the convex interior setting.

theorem AleksandrovDifferentiability.oneDimensional_affineRemainder_trap_of_upperContactOpening {S : Set ℝ} {f : ℝ → ℝ} {p t A η : ℝ} (hp : SubgradientOn S f 0 p) (h : HasUpperContactWithSlopeOpeningAtMostOn S f 0 p A) (hη : 0 < η) (ht : t ∈ S) : 0 ≤ affineRemainder f 0 p t ∧ affineRemainder f 0 p t ≤ (A + η) / 2 * ‖t‖ ^ 2

One-dimensional approximate quadratic trapping at the base point 0.

theorem AleksandrovDifferentiability.affineRemainder_lineRestriction {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (u : E → ℝ) (x p v : E) (t : ℝ) : affineRemainder (lineRestriction u x v) 0 (inner ℝ p v) t = affineRemainder u x p (x + t • v)

The affine remainder commutes with restricting to a line through the base point.

theorem AleksandrovDifferentiability.affineRemainder_lineRestriction_at {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (u : E → ℝ) (x p v : E) (t r : ℝ) : affineRemainder (lineRestriction u x v) t (inner ℝ p v) r = affineRemainder u (x + t • v) p (x + r • v)

The affine remainder commutes with restricting to a line at an arbitrary line parameter.

theorem AleksandrovDifferentiability.SubgradientOn.lineRestriction_affineRemainder_nonneg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p v : E} (hp : SubgradientOn s u x p) {t : ℝ} (ht : t ∈ lineDomain s x v) : 0 ≤ affineRemainder (lineRestriction u x v) 0 (inner ℝ p v) t

A subgradient gives nonnegativity of the affine remainder of each line restriction.

theorem AleksandrovDifferentiability.SubgradientOn.lineRestriction_affineRemainder_nonneg_at {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p v : E} {t r : ℝ} (hp : SubgradientOn s u (x + t • v) p) (hr : r ∈ lineDomain s x v) : 0 ≤ affineRemainder (lineRestriction u x v) t (inner ℝ p v) r

Shifted version of SubgradientOn.lineRestriction_affineRemainder_nonneg.

theorem AleksandrovDifferentiability.HasUpperContactWithSlopeOn.lineRestriction_affineRemainder_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p v : E} {a : ℝ} (h : HasUpperContactWithSlopeOn s u x p a) {t : ℝ} (ht : t ∈ lineDomain s x v) : affineRemainder (AleksandrovDifferentiability.lineRestriction u x v) 0 (inner ℝ p v) t ≤ a * ‖v‖ ^ 2 / 2 * ‖t - 0‖ ^ 2

An upper contact gives a quadratic upper bound for the affine remainder of each line restriction.

theorem AleksandrovDifferentiability.HasUpperContactWithSlopeOn.lineRestriction_affineRemainder_le_at {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p v : E} {t r a : ℝ} (h : HasUpperContactWithSlopeOn s u (x + t • v) p a) (hr : r ∈ lineDomain s x v) : affineRemainder (AleksandrovDifferentiability.lineRestriction u x v) t (inner ℝ p v) r ≤ a * ‖v‖ ^ 2 / 2 * ‖r - t‖ ^ 2

Shifted version of HasUpperContactWithSlopeOn.lineRestriction_affineRemainder_le.

theorem AleksandrovDifferentiability.lineRestriction_affineRemainder_nonneg_and_le_of_subgradient_of_upperContact {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p v : E} {a : ℝ} (hp : SubgradientOn s u x p) (h : HasUpperContactWithSlopeOn s u x p a) {t : ℝ} (ht : t ∈ lineDomain s x v) : 0 ≤ affineRemainder (lineRestriction u x v) 0 (inner ℝ p v) t ∧ affineRemainder (lineRestriction u x v) 0 (inner ℝ p v) t ≤ a * ‖v‖ ^ 2 / 2 * ‖t - 0‖ ^ 2

Along every line, a shared subgradient and upper-contact slope trap the affine remainder between 0 and the line-scaled quadratic opening.

theorem AleksandrovDifferentiability.lineRestriction_affineRemainder_nonneg_and_le_of_subgradient_of_upperContact_at {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p v : E} {t r a : ℝ} (hp : SubgradientOn s u (x + t • v) p) (h : HasUpperContactWithSlopeOn s u (x + t • v) p a) (hr : r ∈ lineDomain s x v) : 0 ≤ affineRemainder (lineRestriction u x v) t (inner ℝ p v) r ∧ affineRemainder (lineRestriction u x v) t (inner ℝ p v) r ≤ a * ‖v‖ ^ 2 / 2 * ‖r - t‖ ^ 2

Shifted line trap from a shared subgradient and upper-contact slope.

theorem AleksandrovDifferentiability.lineRestriction_affineRemainder_nonneg_and_le_of_subgradient_of_upperContactOpening {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p v : E} {A η : ℝ} (hp : SubgradientOn s u x p) (h : HasUpperContactWithSlopeOpeningAtMostOn s u x p A) (hη : 0 < η) {t : ℝ} (ht : t ∈ lineDomain s x v) : 0 ≤ affineRemainder (lineRestriction u x v) 0 (inner ℝ p v) t ∧ affineRemainder (lineRestriction u x v) 0 (inner ℝ p v) t ≤ (A + η) * ‖v‖ ^ 2 / 2 * ‖t - 0‖ ^ 2

Approximate quadratic trapping along a line from a fixed-slope upper-contact opening bound.

theorem AleksandrovDifferentiability.lineRestriction_affineRemainder_nonneg_and_le_of_subgradient_of_upperContactOpening_at {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p v : E} {t r A η : ℝ} (hp : SubgradientOn s u (x + t • v) p) (h : HasUpperContactWithSlopeOpeningAtMostOn s u (x + t • v) p A) (hη : 0 < η) (hr : r ∈ lineDomain s x v) : 0 ≤ affineRemainder (lineRestriction u x v) t (inner ℝ p v) r ∧ affineRemainder (lineRestriction u x v) t (inner ℝ p v) r ≤ (A + η) * ‖v‖ ^ 2 / 2 * ‖r - t‖ ^ 2

Shifted approximate quadratic trapping along a line from a fixed-slope upper-contact opening bound.

theorem AleksandrovDifferentiability.lineRestriction_affineRemainder_trap_of_upperContactOpening_norm_eq_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p v : E} {A η : ℝ} (hp : SubgradientOn s u x p) (h : HasUpperContactWithSlopeOpeningAtMostOn s u x p A) (hv : ‖v‖ = 1) (hη : 0 < η) {t : ℝ} (ht : t ∈ lineDomain s x v) : 0 ≤ affineRemainder (lineRestriction u x v) 0 (inner ℝ p v) t ∧ affineRemainder (lineRestriction u x v) 0 (inner ℝ p v) t ≤ (A + η) / 2 * ‖t‖ ^ 2

Unit-direction version of approximate line trapping, with the standard one-dimensional quadratic bound.

theorem AleksandrovDifferentiability.lineRestriction_affineRemainder_trap_at_of_upperContactOpening_norm_eq_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p v : E} {t r A η : ℝ} (hp : SubgradientOn s u (x + t • v) p) (h : HasUpperContactWithSlopeOpeningAtMostOn s u (x + t • v) p A) (hv : ‖v‖ = 1) (hη : 0 < η) (hr : r ∈ lineDomain s x v) : 0 ≤ affineRemainder (lineRestriction u x v) t (inner ℝ p v) r ∧ affineRemainder (lineRestriction u x v) t (inner ℝ p v) r ≤ (A + η) / 2 * ‖r - t‖ ^ 2

Shifted unit-direction version of approximate line trapping.

theorem AleksandrovDifferentiability.exists_uniform_lineRestriction_affineRemainder_trap_norm_eq_one_of_upperContactOpening {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x v : E} {A : ℝ} (h : HasUpperContactOpeningAtMostOn s u x A) (hu : ConvexOn ℝ s u) (hx : x ∈ interior s) (hv : ‖v‖ = 1) : ∃ (p : E), SubgradientOn s u x p ∧ HasUpperContactWithSlopeOpeningAtMostOn s u x p A ∧ ∀ (η : ℝ), 0 < η → ∀ t ∈ lineDomain s x v, 0 ≤ affineRemainder (lineRestriction u x v) 0 (inner ℝ p v) t ∧ affineRemainder (lineRestriction u x v) 0 (inner ℝ p v) t ≤ (A + η) / 2 * ‖t‖ ^ 2

For convex functions, ordinary bounded upper-contact opening gives a single slope whose line restrictions have the standard one-dimensional quadratic trap in every unit direction.

theorem AleksandrovDifferentiability.exists_uniform_lineRestriction_affineRemainder_trap_at_norm_eq_one_of_upperContactOpening {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x v : E} {t A : ℝ} (h : HasUpperContactOpeningAtMostOn s u (x + t • v) A) (hu : ConvexOn ℝ s u) (hx : x + t • v ∈ interior s) (hv : ‖v‖ = 1) : ∃ (p : E), SubgradientOn s u (x + t • v) p ∧ HasUpperContactWithSlopeOpeningAtMostOn s u (x + t • v) p A ∧ ∀ (η : ℝ), 0 < η → ∀ r ∈ lineDomain s x v, 0 ≤ affineRemainder (lineRestriction u x v) t (inner ℝ p v) r ∧ affineRemainder (lineRestriction u x v) t (inner ℝ p v) r ≤ (A + η) / 2 * ‖r - t‖ ^ 2

Shifted version of exists_uniform_lineRestriction_affineRemainder_trap_norm_eq_one_of_upperContactOpening.

theorem AleksandrovDifferentiability.exists_uniform_lineRestriction_affineRemainder_norm_div_norm_sq_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x v : E} {A : ℝ} (h : HasUpperContactOpeningAtMostOn s u x A) (hu : ConvexOn ℝ s u) (hx : x ∈ interior s) (hv : ‖v‖ = 1) : ∃ (p : E), SubgradientOn s u x p ∧ HasUpperContactWithSlopeOpeningAtMostOn s u x p A ∧ ∀ (η : ℝ), 0 < η → ∀ t ∈ lineDomain s x v, t ≠ 0 → ‖affineRemainder (lineRestriction u x v) 0 (inner ℝ p v) t‖ / ‖t‖ ^ 2 ≤ (A + η) / 2

Uniform normalized line-restriction affine-remainder bound in a unit direction.

theorem AleksandrovDifferentiability.exists_uniform_lineRestriction_affineRemainder_norm_div_norm_sq_le_at {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x v : E} {t A : ℝ} (h : HasUpperContactOpeningAtMostOn s u (x + t • v) A) (hu : ConvexOn ℝ s u) (hx : x + t • v ∈ interior s) (hv : ‖v‖ = 1) : ∃ (p : E), SubgradientOn s u (x + t • v) p ∧ HasUpperContactWithSlopeOpeningAtMostOn s u (x + t • v) p A ∧ ∀ (η : ℝ), 0 < η → ∀ r ∈ lineDomain s x v, r ≠ t → ‖affineRemainder (lineRestriction u x v) t (inner ℝ p v) r‖ / ‖r - t‖ ^ 2 ≤ (A + η) / 2

Shifted uniform normalized line-restriction affine-remainder bound in a unit direction.