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

Line subgradient lift interfaces #

def AleksandrovDifferentiability.LineSubgradientLiftsToAmbient {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (s : Set E) (u : E → ℝ) (x z : E) (t q : ℝ) :

Prop

A scalar subgradient of a line restriction is represented by an ambient subgradient.

Equations

AleksandrovDifferentiability.LineSubgradientLiftsToAmbient s u x z t q = ∃ (p : E), AleksandrovDifferentiability.SubgradientOn s u (x + t • z) p ∧ q = inner ℝ p z

Instances For

source

def AleksandrovDifferentiability.LineSubgradientLiftsToAmbientFunctional {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (s : Set E) (u : E → ℝ) (x z : E) (t q : ℝ) :

Prop

Functional form of LineSubgradientLiftsToAmbient.

This is the form naturally produced by a geometric Hahn-Banach/separation argument: a continuous linear functional supports the epigraph of u at x + t • z and has value q on the line direction z. In complete real inner-product spaces, Fréchet-Riesz converts this functional form into the vector-valued subgradient form used elsewhere in the project.

Equations

AleksandrovDifferentiability.LineSubgradientLiftsToAmbientFunctional s u x z t q = ∃ (ℓ : StrongDual ℝ E), (∀ y ∈ s, u (x + t • z) + ℓ (y - (x + t • z)) ≤ u y) ∧ q = ℓ z

Instances For

source

theorem AleksandrovDifferentiability.SubgradientOn.lineSubgradientLiftsToAmbient_at {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x z p : E} {t : ℝ} (hp : SubgradientOn s u (x + t • z) p) :

LineSubgradientLiftsToAmbient s u x z t (inner ℝ p z)

An ambient subgradient at a point on the line gives a vector-valued lift of its directional pairing.

source

theorem AleksandrovDifferentiability.SubgradientOn.lineSubgradientLiftsToAmbientFunctional_at {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x z p : E} {t : ℝ} (hp : SubgradientOn s u (x + t • z) p) :

LineSubgradientLiftsToAmbientFunctional s u x z t (inner ℝ p z)

An ambient subgradient at a point on the line gives a functional lift of its directional pairing.

source

theorem AleksandrovDifferentiability.lineSubgradientLiftsToAmbientFunctional_of_exists_subgradient_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x z : E} {t q : ℝ} (h : ∃ (p : E), SubgradientOn s u (x + t • z) p ∧ q = inner ℝ p z) :

LineSubgradientLiftsToAmbientFunctional s u x z t q

If a scalar slope is attained by an ambient subgradient in direction z, then it has a functional lift.

source

theorem AleksandrovDifferentiability.lineSubgradientLiftsToAmbient_of_exists_subgradient_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x z : E} {t q : ℝ} (h : ∃ (p : E), SubgradientOn s u (x + t • z) p ∧ q = inner ℝ p z) :

LineSubgradientLiftsToAmbient s u x z t q

If a scalar slope is attained by an ambient subgradient in direction z, then it has a vector-valued lift.

source

theorem AleksandrovDifferentiability.lineRightDeriv_liftsToAmbientFunctional_of_exists_subgradient_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x z : E} {t : ℝ} (h : ∃ (p : E), SubgradientOn s u (x + t • z) p ∧ rightDeriv (lineRestriction u x z) t = inner ℝ p z) :

LineSubgradientLiftsToAmbientFunctional s u x z t (rightDeriv (lineRestriction u x z) t)

Right-derivative endpoint attainment by an ambient subgradient gives the corresponding functional lift.

source

theorem AleksandrovDifferentiability.lineRightDeriv_liftsToAmbient_of_exists_subgradient_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x z : E} {t : ℝ} (h : ∃ (p : E), SubgradientOn s u (x + t • z) p ∧ rightDeriv (lineRestriction u x z) t = inner ℝ p z) :

LineSubgradientLiftsToAmbient s u x z t (rightDeriv (lineRestriction u x z) t)

Right-derivative endpoint attainment by an ambient subgradient gives the corresponding vector-valued lift.

source

theorem AleksandrovDifferentiability.lineLeftDeriv_liftsToAmbientFunctional_of_exists_subgradient_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x z : E} {t : ℝ} (h : ∃ (p : E), SubgradientOn s u (x + t • z) p ∧ leftDeriv (lineRestriction u x z) t = inner ℝ p z) :

LineSubgradientLiftsToAmbientFunctional s u x z t (leftDeriv (lineRestriction u x z) t)

Left-derivative endpoint attainment by an ambient subgradient gives the corresponding functional lift.

source

theorem AleksandrovDifferentiability.lineLeftDeriv_liftsToAmbient_of_exists_subgradient_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x z : E} {t : ℝ} (h : ∃ (p : E), SubgradientOn s u (x + t • z) p ∧ leftDeriv (lineRestriction u x z) t = inner ℝ p z) :

LineSubgradientLiftsToAmbient s u x z t (leftDeriv (lineRestriction u x z) t)

Left-derivative endpoint attainment by an ambient subgradient gives the corresponding vector-valued lift.

source

theorem AleksandrovDifferentiability.exists_nonneg_add_eq_one_and_eq_combo_of_mem_Icc {l q r : ℝ} (hlq : l ≤ q) (hqr : q ≤ r) :

∃ (a : ℝ) (b : ℝ), 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ q = a * l + b * r

A point in a real interval is a convex combination of the endpoints.

source

theorem AleksandrovDifferentiability.SubgradientOn.lineRestriction_supporting_slope_inequality {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x z : E} {t q r : ℝ} (hq : SubgradientOn (lineDomain s x z) (lineRestriction u x z) t q) (hr : r ∈ lineDomain s x z) :

u (x + t • z) + q * (r - t) ≤ u (x + r • z)

A one-dimensional subgradient of a line restriction is exactly an affine minorant along that line. This is the line datum that the Hahn-Banach/separation step must extend to the ambient domain.

source

theorem AleksandrovDifferentiability.LineSubgradientLiftsToAmbientFunctional.line_inequality {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x z : E} {t q r : ℝ} (h : LineSubgradientLiftsToAmbientFunctional s u x z t q) (hr : r ∈ lineDomain s x z) :

u (x + t • z) + q * (r - t) ≤ u (x + r • z)

If an ambient supporting functional has the prescribed value on the line direction, it extends the line affine minorant determined by a line subgradient. This records the compatibility between the line-subgradient datum and the functional lift target.

source

theorem AleksandrovDifferentiability.LineSubgradientLiftsToAmbient.to_lineSubgradientLiftsToAmbientFunctional {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x z : E} {t q : ℝ} (h : LineSubgradientLiftsToAmbient s u x z t q) :

LineSubgradientLiftsToAmbientFunctional s u x z t q

A vector-valued ambient subgradient lift gives the functional lift by the Riesz embedding p ↦ (y ↦ p · y). The reverse implication uses Fréchet-Riesz and therefore requires completeness; see LineSubgradientLiftsToAmbientFunctional.to_lineSubgradientLiftsToAmbient.

source

theorem AleksandrovDifferentiability.LineSubgradientLiftsToAmbient.smul_add_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x z : E} {t q₀ q₁ a b : ℝ} (h₀ : LineSubgradientLiftsToAmbient s u x z t q₀) (h₁ : LineSubgradientLiftsToAmbient s u x z t q₁) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) :

LineSubgradientLiftsToAmbient s u x z t (a * q₀ + b * q₁)

Convex combinations of vector-valued line-subgradient lifts are again vector-valued lifts. This records the interval-convexity of directional values of ambient subgradients.

source

theorem AleksandrovDifferentiability.LineSubgradientLiftsToAmbientFunctional.smul_add_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x z : E} {t q₀ q₁ a b : ℝ} (h₀ : LineSubgradientLiftsToAmbientFunctional s u x z t q₀) (h₁ : LineSubgradientLiftsToAmbientFunctional s u x z t q₁) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) :

LineSubgradientLiftsToAmbientFunctional s u x z t (a * q₀ + b * q₁)

Convex combinations of functional line-subgradient lifts are again functional lifts.

source

theorem AleksandrovDifferentiability.ConvexOn.lineSubgradient_liftsToAmbientFunctional_of_leftRightDeriv_lift {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x z : E} {t q : ℝ} (hu : ConvexOn ℝ s u) (ht : x + t • z ∈ interior s) (hq : SubgradientOn (lineDomain s x z) (AleksandrovDifferentiability.lineRestriction u x z) t q) (hleft : LineSubgradientLiftsToAmbientFunctional s u x z t (leftDeriv (AleksandrovDifferentiability.lineRestriction u x z) t)) (hright : LineSubgradientLiftsToAmbientFunctional s u x z t (rightDeriv (AleksandrovDifferentiability.lineRestriction u x z) t)) :

LineSubgradientLiftsToAmbientFunctional s u x z t q

If the left and right derivatives of a convex line restriction have functional ambient lifts, then every one-dimensional subgradient slope has a functional ambient lift.

source

theorem AleksandrovDifferentiability.ConvexOn.lineSubgradient_liftsToAmbient_of_leftRightDeriv_lift {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x z : E} {t q : ℝ} (hu : ConvexOn ℝ s u) (ht : x + t • z ∈ interior s) (hq : SubgradientOn (lineDomain s x z) (AleksandrovDifferentiability.lineRestriction u x z) t q) (hleft : LineSubgradientLiftsToAmbient s u x z t (leftDeriv (AleksandrovDifferentiability.lineRestriction u x z) t)) (hright : LineSubgradientLiftsToAmbient s u x z t (rightDeriv (AleksandrovDifferentiability.lineRestriction u x z) t)) :

LineSubgradientLiftsToAmbient s u x z t q

Vector-valued version of ConvexOn.lineSubgradient_liftsToAmbientFunctional_of_leftRightDeriv_lift.

source

theorem AleksandrovDifferentiability.ConvexOn.eventually_lineSubgradient_liftsToAmbientFunctional_of_leftRightDeriv_lift {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x : E} (hu : ConvexOn ℝ s u) (hsegmentInterior : ∀ᶠ (z : E) in nhds 0, ∀ t ∈ Set.uIoc 0 1, x + t • z ∈ interior s) (hleft : ∀ᶠ (z : E) in nhds 0, ∀ t ∈ Set.uIoc 0 1, LineSubgradientLiftsToAmbientFunctional s u x z t (leftDeriv (AleksandrovDifferentiability.lineRestriction u x z) t)) (hright : ∀ᶠ (z : E) in nhds 0, ∀ t ∈ Set.uIoc 0 1, LineSubgradientLiftsToAmbientFunctional s u x z t (rightDeriv (AleksandrovDifferentiability.lineRestriction u x z) t)) :

∀ᶠ (z : E) in nhds 0, ∀ t ∈ Set.uIoc 0 1, ∀ (q : ℝ), SubgradientOn (lineDomain s x z) (AleksandrovDifferentiability.lineRestriction u x z) t q → LineSubgradientLiftsToAmbientFunctional s u x z t q

Eventual functional lift of all line subgradients from eventual lifts of the left and right derivatives.

source

theorem AleksandrovDifferentiability.ConvexOn.eventually_lineSubgradient_liftsToAmbient_of_leftRightDeriv_lift {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x : E} (hu : ConvexOn ℝ s u) (hsegmentInterior : ∀ᶠ (z : E) in nhds 0, ∀ t ∈ Set.uIoc 0 1, x + t • z ∈ interior s) (hleft : ∀ᶠ (z : E) in nhds 0, ∀ t ∈ Set.uIoc 0 1, LineSubgradientLiftsToAmbient s u x z t (leftDeriv (AleksandrovDifferentiability.lineRestriction u x z) t)) (hright : ∀ᶠ (z : E) in nhds 0, ∀ t ∈ Set.uIoc 0 1, LineSubgradientLiftsToAmbient s u x z t (rightDeriv (AleksandrovDifferentiability.lineRestriction u x z) t)) :

∀ᶠ (z : E) in nhds 0, ∀ t ∈ Set.uIoc 0 1, ∀ (q : ℝ), SubgradientOn (lineDomain s x z) (AleksandrovDifferentiability.lineRestriction u x z) t q → LineSubgradientLiftsToAmbient s u x z t q

Eventual vector-valued lift of all line subgradients from eventual lifts of the left and right derivatives.

source

theorem AleksandrovDifferentiability.ConvexOn.eventually_lineSubgradient_liftsToAmbientFunctional_of_leftRightDeriv_attainment {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x : E} (hu : ConvexOn ℝ s u) (hsegmentInterior : ∀ᶠ (z : E) in nhds 0, ∀ t ∈ Set.uIoc 0 1, x + t • z ∈ interior s) (hleft : ∀ᶠ (z : E) in nhds 0, ∀ t ∈ Set.uIoc 0 1, ∃ (p : E), SubgradientOn s u (x + t • z) p ∧ leftDeriv (AleksandrovDifferentiability.lineRestriction u x z) t = inner ℝ p z) (hright : ∀ᶠ (z : E) in nhds 0, ∀ t ∈ Set.uIoc 0 1, ∃ (p : E), SubgradientOn s u (x + t • z) p ∧ rightDeriv (AleksandrovDifferentiability.lineRestriction u x z) t = inner ℝ p z) :

Eventual functional lift of all line subgradients from endpoint attainment of the left and right derivatives by ambient subgradients. This is the form expected from the endpoint support-function/Hahn-Banach step.

source

theorem AleksandrovDifferentiability.ConvexOn.eventually_lineSubgradient_liftsToAmbient_of_leftRightDeriv_attainment {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x : E} (hu : ConvexOn ℝ s u) (hsegmentInterior : ∀ᶠ (z : E) in nhds 0, ∀ t ∈ Set.uIoc 0 1, x + t • z ∈ interior s) (hleft : ∀ᶠ (z : E) in nhds 0, ∀ t ∈ Set.uIoc 0 1, ∃ (p : E), SubgradientOn s u (x + t • z) p ∧ leftDeriv (AleksandrovDifferentiability.lineRestriction u x z) t = inner ℝ p z) (hright : ∀ᶠ (z : E) in nhds 0, ∀ t ∈ Set.uIoc 0 1, ∃ (p : E), SubgradientOn s u (x + t • z) p ∧ rightDeriv (AleksandrovDifferentiability.lineRestriction u x z) t = inner ℝ p z) :

Eventual vector-valued lift of all line subgradients from endpoint attainment of the left and right derivatives by ambient subgradients.

source

theorem AleksandrovDifferentiability.LineSubgradientLiftsToAmbientFunctional.to_lineSubgradientLiftsToAmbient {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {s : Set E} {u : E → ℝ} {x z : E} {t q : ℝ} (hmem : x + t • z ∈ s) (h : LineSubgradientLiftsToAmbientFunctional s u x z t q) :

LineSubgradientLiftsToAmbient s u x z t q

A functional lift gives the vector-valued ambient subgradient lift by Fréchet-Riesz.

source

theorem AleksandrovDifferentiability.eventually_lineSubgradientLiftsToAmbient_of_functional {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {s : Set E} {u : E → ℝ} {x : E} (hsegment : ∀ᶠ (z : E) in nhds 0, ∀ t ∈ Set.uIoc 0 1, x + t • z ∈ s) (hlift : ∀ᶠ (z : E) in nhds 0, ∀ t ∈ Set.uIoc 0 1, ∀ (q : ℝ), SubgradientOn (lineDomain s x z) (lineRestriction u x z) t q → LineSubgradientLiftsToAmbientFunctional s u x z t q) :

∀ᶠ (z : E) in nhds 0, ∀ t ∈ Set.uIoc 0 1, ∀ (q : ℝ), SubgradientOn (lineDomain s x z) (lineRestriction u x z) t q → LineSubgradientLiftsToAmbient s u x z t q

Eventual version of the Fréchet-Riesz conversion from functional line-subgradient lifts to vector-valued ambient subgradient lifts.

source

theorem AleksandrovDifferentiability.eventually_lineSubgradientLiftsToAmbientFunctional_of_vector {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x : E} (hlift : ∀ᶠ (z : E) in nhds 0, ∀ t ∈ Set.uIoc 0 1, ∀ (q : ℝ), SubgradientOn (lineDomain s x z) (lineRestriction u x z) t q → LineSubgradientLiftsToAmbient s u x z t q) :

∀ᶠ (z : E) in nhds 0, ∀ t ∈ Set.uIoc 0 1, ∀ (q : ℝ), SubgradientOn (lineDomain s x z) (lineRestriction u x z) t q → LineSubgradientLiftsToAmbientFunctional s u x z t q

Eventual conversion from vector-valued line-subgradient lifts to functional lifts.

source

theorem AleksandrovDifferentiability.ConvexOn.lineLeftDeriv_liftsToAmbientFunctional_of_lineSubgradientLift {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x z : E} {t : ℝ} (hu : ConvexOn ℝ s u) (ht : x + t • z ∈ interior s) (hlift : ∀ (q : ℝ), SubgradientOn (lineDomain s x z) (AleksandrovDifferentiability.lineRestriction u x z) t q → LineSubgradientLiftsToAmbientFunctional s u x z t q) :

LineSubgradientLiftsToAmbientFunctional s u x z t (leftDeriv (AleksandrovDifferentiability.lineRestriction u x z) t)

Pointwise functional lift of the left derivative, once all line subgradients are known to lift. Convexity supplies the fact that the left derivative is itself a one-dimensional subgradient.

source

theorem AleksandrovDifferentiability.ConvexOn.lineLeftDeriv_liftsToAmbient_of_lineSubgradientLift {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x z : E} {t : ℝ} (hu : ConvexOn ℝ s u) (ht : x + t • z ∈ interior s) (hlift : ∀ (q : ℝ), SubgradientOn (lineDomain s x z) (AleksandrovDifferentiability.lineRestriction u x z) t q → LineSubgradientLiftsToAmbient s u x z t q) :

LineSubgradientLiftsToAmbient s u x z t (leftDeriv (AleksandrovDifferentiability.lineRestriction u x z) t)

Pointwise vector-valued lift of the left derivative, once all line subgradients are known to lift.

source

theorem AleksandrovDifferentiability.ConvexOn.lineRightDeriv_liftsToAmbientFunctional_of_lineSubgradientLift {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x z : E} {t : ℝ} (hu : ConvexOn ℝ s u) (ht : x + t • z ∈ interior s) (hlift : ∀ (q : ℝ), SubgradientOn (lineDomain s x z) (AleksandrovDifferentiability.lineRestriction u x z) t q → LineSubgradientLiftsToAmbientFunctional s u x z t q) :

LineSubgradientLiftsToAmbientFunctional s u x z t (rightDeriv (AleksandrovDifferentiability.lineRestriction u x z) t)

Pointwise functional lift of the right derivative, once all line subgradients are known to lift. Convexity supplies the fact that the right derivative is itself a one-dimensional subgradient.

source

theorem AleksandrovDifferentiability.ConvexOn.lineRightDeriv_liftsToAmbient_of_lineSubgradientLift {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x z : E} {t : ℝ} (hu : ConvexOn ℝ s u) (ht : x + t • z ∈ interior s) (hlift : ∀ (q : ℝ), SubgradientOn (lineDomain s x z) (AleksandrovDifferentiability.lineRestriction u x z) t q → LineSubgradientLiftsToAmbient s u x z t q) :

LineSubgradientLiftsToAmbient s u x z t (rightDeriv (AleksandrovDifferentiability.lineRestriction u x z) t)

Pointwise vector-valued lift of the right derivative, once all line subgradients are known to lift.

source

theorem AleksandrovDifferentiability.ConvexOn.eventually_lineLeftDeriv_liftsToAmbientFunctional_of_lineSubgradientLift {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x : E} (hu : ConvexOn ℝ s u) (hsegmentInterior : ∀ᶠ (z : E) in nhds 0, ∀ t ∈ Set.uIoc 0 1, x + t • z ∈ interior s) (hlift : ∀ᶠ (z : E) in nhds 0, ∀ t ∈ Set.uIoc 0 1, ∀ (q : ℝ), SubgradientOn (lineDomain s x z) (AleksandrovDifferentiability.lineRestriction u x z) t q → LineSubgradientLiftsToAmbientFunctional s u x z t q) :

∀ᶠ (z : E) in nhds 0, ∀ t ∈ Set.uIoc 0 1, LineSubgradientLiftsToAmbientFunctional s u x z t (leftDeriv (AleksandrovDifferentiability.lineRestriction u x z) t)

Eventual functional lift of the left derivative along short segments.

source

theorem AleksandrovDifferentiability.ConvexOn.eventually_lineLeftDeriv_liftsToAmbient_of_lineSubgradientLift {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x : E} (hu : ConvexOn ℝ s u) (hsegmentInterior : ∀ᶠ (z : E) in nhds 0, ∀ t ∈ Set.uIoc 0 1, x + t • z ∈ interior s) (hlift : ∀ᶠ (z : E) in nhds 0, ∀ t ∈ Set.uIoc 0 1, ∀ (q : ℝ), SubgradientOn (lineDomain s x z) (AleksandrovDifferentiability.lineRestriction u x z) t q → LineSubgradientLiftsToAmbient s u x z t q) :

∀ᶠ (z : E) in nhds 0, ∀ t ∈ Set.uIoc 0 1, LineSubgradientLiftsToAmbient s u x z t (leftDeriv (AleksandrovDifferentiability.lineRestriction u x z) t)

Eventual vector-valued lift of the left derivative along short segments.

source

theorem AleksandrovDifferentiability.ConvexOn.eventually_lineRightDeriv_liftsToAmbientFunctional_of_lineSubgradientLift {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x : E} (hu : ConvexOn ℝ s u) (hsegmentInterior : ∀ᶠ (z : E) in nhds 0, ∀ t ∈ Set.uIoc 0 1, x + t • z ∈ interior s) (hlift : ∀ᶠ (z : E) in nhds 0, ∀ t ∈ Set.uIoc 0 1, ∀ (q : ℝ), SubgradientOn (lineDomain s x z) (AleksandrovDifferentiability.lineRestriction u x z) t q → LineSubgradientLiftsToAmbientFunctional s u x z t q) :

∀ᶠ (z : E) in nhds 0, ∀ t ∈ Set.uIoc 0 1, LineSubgradientLiftsToAmbientFunctional s u x z t (rightDeriv (AleksandrovDifferentiability.lineRestriction u x z) t)

Eventual functional lift of the right derivative along short segments. This is the separation-facing analogue of ConvexOn.eventually_lineRightDeriv_realized_by_subgradient_of_lineSubgradientLift.

source

theorem AleksandrovDifferentiability.ConvexOn.eventually_lineRightDeriv_liftsToAmbient_of_lineSubgradientLift {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x : E} (hu : ConvexOn ℝ s u) (hsegmentInterior : ∀ᶠ (z : E) in nhds 0, ∀ t ∈ Set.uIoc 0 1, x + t • z ∈ interior s) (hlift : ∀ᶠ (z : E) in nhds 0, ∀ t ∈ Set.uIoc 0 1, ∀ (q : ℝ), SubgradientOn (lineDomain s x z) (AleksandrovDifferentiability.lineRestriction u x z) t q → LineSubgradientLiftsToAmbient s u x z t q) :

∀ᶠ (z : E) in nhds 0, ∀ t ∈ Set.uIoc 0 1, LineSubgradientLiftsToAmbient s u x z t (rightDeriv (AleksandrovDifferentiability.lineRestriction u x z) t)

Eventual vector-valued lift of the right derivative along short segments.

source

theorem AleksandrovDifferentiability.ConvexOn.eventually_lineRightDeriv_realized_by_subgradient_of_lineSubgradientLift {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x : E} (hu : ConvexOn ℝ s u) (hsegmentInterior : ∀ᶠ (z : E) in nhds 0, ∀ t ∈ Set.uIoc 0 1, x + t • z ∈ interior s) (hlift : ∀ᶠ (z : E) in nhds 0, ∀ t ∈ Set.uIoc 0 1, ∀ (q : ℝ), SubgradientOn (lineDomain s x z) (AleksandrovDifferentiability.lineRestriction u x z) t q → LineSubgradientLiftsToAmbient s u x z t q) :

∀ᶠ (z : E) in nhds 0, ∀ t ∈ Set.uIoc 0 1, ∃ (p : E), SubgradientOn s u (x + t • z) p ∧ rightDeriv (AleksandrovDifferentiability.lineRestriction u x z) t = inner ℝ p z

If every one-dimensional subgradient along short segments lifts to an ambient subgradient, then the right derivative of the line restriction is realized by an ambient subgradient.

This packages the already-formalized one-dimensional fact ConvexOn.lineRestriction_rightDeriv_subgradientOn_at: at interior line parameters the right derivative is itself a line subgradient.

Documentation

LeanPool.ViscositySolutionTheory.AleksandrovDifferentiability.Analysis.LineRestriction.Lifts

Line subgradient lift interfaces #