Line restrictions commute with a linear isometry equivalence. This is the affine-line bookkeeping needed to move fixed-direction slice predicates through an orthonormal coordinate change.

source

theorem AleksandrovDifferentiability.lineDomain_preimage_linearIsometryEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (e : E ≃ₗᵢ[ℝ ] F) (s : Set F) (x v : E) :

lineDomain (⇑e ⁻¹' s) x v = lineDomain s (e x) (e v)

Line domains commute with taking the preimage under a linear isometry equivalence.

source

theorem AleksandrovDifferentiability.isOpen_image_linearIsometryEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (e : E ≃ₗᵢ[ℝ ] F) {s : Set E} (hs : IsOpen s) :

IsOpen (⇑e '' s)

The image of an open set under a linear isometry equivalence is open. This packages the domain side of an orthonormal coordinate change.

source

theorem AleksandrovDifferentiability.convex_image_linearIsometryEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (e : E ≃ₗᵢ[ℝ ] F) {s : Set E} (hs : Convex ℝ s) :

Convex ℝ (⇑e '' s)

The image of a convex set under a linear isometry equivalence is convex.

source

theorem AleksandrovDifferentiability.ConvexOn.image_linearIsometryEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (e : E ≃ₗᵢ[ℝ ] F) {s : Set E} {u : E → ℝ} (hu : ConvexOn ℝ s u) :

ConvexOn ℝ (⇑e '' s) (u ∘ ⇑e.symm)

Convexity of a function on a set is preserved by rebasing through a linear isometry equivalence.

source

theorem AleksandrovDifferentiability.lineRestriction_rebase_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (u : E → ℝ) (x v : E) (t r : ℝ) :

lineRestriction u (x + t • v) v r = lineRestriction u x v (t + r)

Rebase a line restriction at parameter t: evaluating at the new parameter r agrees with the original line restriction at t + r.

source

theorem AleksandrovDifferentiability.mem_lineDomain_rebase_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {x v : E} {t r : ℝ} :

r ∈ lineDomain s (x + t • v) v ↔ t + r ∈ lineDomain s x v

Rebase the line domain at parameter t.

source

theorem AleksandrovDifferentiability.lineDomain_rebase {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (s : Set E) (x v : E) (t : ℝ) :

lineDomain s (x + t • v) v = {r : ℝ | t + r ∈ lineDomain s x v}

Set-level rebase formula for line domains.

source

theorem AleksandrovDifferentiability.lineRestriction_smul_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (u : E → ℝ) (x v : E) (c t : ℝ) :

lineRestriction u x (c • v) t = lineRestriction u x v (c * t)

Replacing a line direction by a scalar multiple corresponds to scaling the line parameter.

source

theorem AleksandrovDifferentiability.mem_lineDomain_smul_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {x v : E} {c t : ℝ} :

t ∈ lineDomain s x (c • v) ↔ c * t ∈ lineDomain s x v

Domain version of lineRestriction_smul_apply.

source

theorem AleksandrovDifferentiability.lineDomain_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (s : Set E) (x v : E) (c : ℝ) :

lineDomain s x (c • v) = {t : ℝ | c * t ∈ lineDomain s x v}

Set-level scalar-rescaling formula for line domains.

source

@[simp]

theorem AleksandrovDifferentiability.lineRestriction_neg_direction {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (u : E → ℝ) (x v : E) (t : ℝ) :

lineRestriction u x (-v) t = lineRestriction u x v (-t)

source

@[simp]

theorem AleksandrovDifferentiability.lineDomain_neg_direction {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (s : Set E) (x v : E) :

lineDomain s x (-v) = {t : ℝ | -t ∈ lineDomain s x v}

source

theorem AleksandrovDifferentiability.isOpen_lineDomain {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {x v : E} (hs : IsOpen s) :

IsOpen (lineDomain s x v)

The line domain of an open ambient set is open.

source

@[simp]

theorem AleksandrovDifferentiability.lineRestriction_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (u : E → ℝ) (x v : E) :

lineRestriction u x v 0 = u x

source

theorem AleksandrovDifferentiability.zero_mem_lineDomain {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {x v : E} (hx : x ∈ s) :

0 ∈ lineDomain s x v

source

theorem AleksandrovDifferentiability.zero_mem_interior_lineDomain {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {x v : E} (hx : x ∈ interior s) :

0 ∈ interior (lineDomain s x v)

If the base point is interior to the ambient domain, then 0 is interior to the line-restricted domain in every direction.

source

theorem AleksandrovDifferentiability.mem_interior_lineDomain_of_line_mem_interior {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {x v : E} {t : ℝ} (ht : x + t • v ∈ interior s) :

t ∈ interior (lineDomain s x v)

If a point on the line lies in the interior of the ambient domain, then the corresponding line parameter lies in the interior of the line domain.

source

theorem AleksandrovDifferentiability.SubgradientOn.line_supporting_inequality {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) :

u x + inner ℝ p (t • v) ≤ lineRestriction u x v t

An ambient subgradient gives the supporting inequality along every line through the base point.

source

theorem AleksandrovDifferentiability.SubgradientOn.lineRestriction_supporting_inequality {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) :

lineRestriction u x v 0 + inner ℝ p (t • v) ≤ lineRestriction u x v t

The line-restricted supporting inequality, written with the value at parameter 0.

source

theorem AleksandrovDifferentiability.SubgradientOn.lineRestriction_subgradientOn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p v : E} (hp : SubgradientOn s u x p) :

SubgradientOn (lineDomain s x v) (lineRestriction u x v) 0 (inner ℝ p v)

An ambient subgradient restricts to a one-dimensional subgradient along every line through the base point.

source

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

SubgradientOn (lineDomain s x v) (lineRestriction u x v) t (inner ℝ p v)

An ambient subgradient at the point with line parameter t restricts to a one-dimensional subgradient at t.

source

theorem AleksandrovDifferentiability.HasUpperContactWithSlopeOn.lineRestriction {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) :

HasUpperContactWithSlopeOn (lineDomain s x v) (AleksandrovDifferentiability.lineRestriction u x v) 0 (inner ℝ p v) (a * ‖v‖ ^ 2)

An ambient upper quadratic contact with a specified slope restricts to an upper quadratic contact on every affine line, with slope paired against the line direction and opening scaled by the squared length of the direction vector.

source

theorem AleksandrovDifferentiability.HasUpperContactWithSlopeOn.lineRestriction_at {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p v : E} {t a : ℝ} (h : HasUpperContactWithSlopeOn s u (x + t • v) p a) :

HasUpperContactWithSlopeOn (lineDomain s x v) (AleksandrovDifferentiability.lineRestriction u x v) t (inner ℝ p v) (a * ‖v‖ ^ 2)

Shifted version of HasUpperContactWithSlopeOn.lineRestriction: an ambient contact at the point with line parameter t restricts to a one-dimensional contact at t.

source

theorem AleksandrovDifferentiability.HasUpperContactOn.lineRestriction {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x v : E} {a : ℝ} (h : HasUpperContactOn s u x a) :

HasUpperContactOn (lineDomain s x v) (AleksandrovDifferentiability.lineRestriction u x v) 0 (a * ‖v‖ ^ 2)

An ambient upper quadratic contact restricts to an upper quadratic contact on every affine line, with the opening scaled by the squared length of the direction vector.

source

theorem AleksandrovDifferentiability.HasUpperContactOn.lineRestriction_at {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x v : E} {t a : ℝ} (h : HasUpperContactOn s u (x + t • v) a) :

HasUpperContactOn (lineDomain s x v) (AleksandrovDifferentiability.lineRestriction u x v) t (a * ‖v‖ ^ 2)

Shifted version of HasUpperContactOn.lineRestriction: an ambient contact at the point with line parameter t restricts to a one-dimensional contact at t.

source

theorem AleksandrovDifferentiability.HasUpperContactOpeningAtMostOn.lineRestriction_of_norm_pos {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x v : E} {A : ℝ} (h : HasUpperContactOpeningAtMostOn s u x A) (hv : 0 < ‖v‖) :

HasUpperContactOpeningAtMostOn (lineDomain s x v) (lineRestriction u x v) 0 (A * ‖v‖ ^ 2)

A bound on the upper-contact opening restricts to every nonconstant affine line, with the opening scaled by the squared length of the direction vector.

source

theorem AleksandrovDifferentiability.HasUpperContactOpeningAtMostOn.lineRestriction_of_norm_eq_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x v : E} {A : ℝ} (h : HasUpperContactOpeningAtMostOn s u x A) (hv : ‖v‖ = 1) :

HasUpperContactOpeningAtMostOn (lineDomain s x v) (lineRestriction u x v) 0 A

Unit-direction version of HasUpperContactOpeningAtMostOn.lineRestriction_of_norm_pos.

source

theorem AleksandrovDifferentiability.HasUpperContactOpeningAtMostOn.lineRestriction_at_of_norm_pos {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) (hv : 0 < ‖v‖) :

HasUpperContactOpeningAtMostOn (lineDomain s x v) (lineRestriction u x v) t (A * ‖v‖ ^ 2)

Shifted version of HasUpperContactOpeningAtMostOn.lineRestriction_of_norm_pos.

source

theorem AleksandrovDifferentiability.HasUpperContactOpeningAtMostOn.lineRestriction_at_of_norm_eq_one {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) (hv : ‖v‖ = 1) :

HasUpperContactOpeningAtMostOn (lineDomain s x v) (lineRestriction u x v) t A

Unit-direction version of HasUpperContactOpeningAtMostOn.lineRestriction_at_of_norm_pos.

source

theorem AleksandrovDifferentiability.HasUpperContactWithSlopeOpeningAtMostOn.lineRestriction_of_norm_pos {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p v : E} {A : ℝ} (h : HasUpperContactWithSlopeOpeningAtMostOn s u x p A) (hv : 0 < ‖v‖) :

HasUpperContactWithSlopeOpeningAtMostOn (lineDomain s x v) (lineRestriction u x v) 0 (inner ℝ p v) (A * ‖v‖ ^ 2)

Fixed-slope bounded upper-contact openings restrict to every nonconstant affine line, with the slope paired against the line direction and the opening scaled by the squared direction length.

source

theorem AleksandrovDifferentiability.HasUpperContactWithSlopeOpeningAtMostOn.lineRestriction_of_norm_eq_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p v : E} {A : ℝ} (h : HasUpperContactWithSlopeOpeningAtMostOn s u x p A) (hv : ‖v‖ = 1) :

HasUpperContactWithSlopeOpeningAtMostOn (lineDomain s x v) (lineRestriction u x v) 0 (inner ℝ p v) A

Unit-direction version of HasUpperContactWithSlopeOpeningAtMostOn.lineRestriction_of_norm_pos.

source

theorem AleksandrovDifferentiability.HasUpperContactWithSlopeOpeningAtMostOn.lineRestriction_at_of_norm_pos {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p v : E} {t A : ℝ} (h : HasUpperContactWithSlopeOpeningAtMostOn s u (x + t • v) p A) (hv : 0 < ‖v‖) :

HasUpperContactWithSlopeOpeningAtMostOn (lineDomain s x v) (lineRestriction u x v) t (inner ℝ p v) (A * ‖v‖ ^ 2)

Shifted version of HasUpperContactWithSlopeOpeningAtMostOn.lineRestriction_of_norm_pos.

source

theorem AleksandrovDifferentiability.HasUpperContactWithSlopeOpeningAtMostOn.lineRestriction_at_of_norm_eq_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p v : E} {t A : ℝ} (h : HasUpperContactWithSlopeOpeningAtMostOn s u (x + t • v) p A) (hv : ‖v‖ = 1) :

HasUpperContactWithSlopeOpeningAtMostOn (lineDomain s x v) (lineRestriction u x v) t (inner ℝ p v) A

Unit-direction version of HasUpperContactWithSlopeOpeningAtMostOn.lineRestriction_at_of_norm_pos.

source

theorem AleksandrovDifferentiability.preimage_lineMap_upperContactWithSlopeSet_subset {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p v : E} {a : ℝ} :

{t : ℝ | x + t • v ∈ upperContactWithSlopeSet s u p a} ⊆ upperContactWithSlopeSet (lineDomain s x v) (lineRestriction u x v) (inner ℝ p v) (a * ‖v‖ ^ 2)

The preimage of an ambient slope-specific contact set along a line is contained in the corresponding contact set for the one-dimensional restriction.

source

theorem AleksandrovDifferentiability.preimage_lineMap_upperContactSet_subset {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x v : E} {a : ℝ} :

{t : ℝ | x + t • v ∈ upperContactSet s u a} ⊆ upperContactSet (lineDomain s x v) (lineRestriction u x v) (a * ‖v‖ ^ 2)

The preimage of an ambient contact set along a line is contained in the contact set for the one-dimensional restriction.

source

theorem AleksandrovDifferentiability.preimage_lineMap_upperContactOpeningAtMostSet_subset_of_norm_pos {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x v : E} {A : ℝ} (hv : 0 < ‖v‖) :

{t : ℝ | x + t • v ∈ upperContactOpeningAtMostSet s u A} ⊆ upperContactOpeningAtMostSet (lineDomain s x v) (lineRestriction u x v) (A * ‖v‖ ^ 2)

Bounded upper-contact openings pass to line-restricted contact loci on nonconstant lines.

source

theorem AleksandrovDifferentiability.preimage_lineMap_upperContactOpeningAtMostSet_subset_of_norm_eq_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x v : E} {A : ℝ} (hv : ‖v‖ = 1) :

{t : ℝ | x + t • v ∈ upperContactOpeningAtMostSet s u A} ⊆ upperContactOpeningAtMostSet (lineDomain s x v) (lineRestriction u x v) A

Unit-direction version of preimage_lineMap_upperContactOpeningAtMostSet_subset_of_norm_pos.

source

theorem AleksandrovDifferentiability.preimage_lineMap_upperContactWithSlopeOpeningAtMostSet_subset_of_norm_pos {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p v : E} {A : ℝ} (hv : 0 < ‖v‖) :

{t : ℝ | x + t • v ∈ upperContactWithSlopeOpeningAtMostSet s u p A} ⊆ upperContactWithSlopeOpeningAtMostSet (lineDomain s x v) (lineRestriction u x v) (inner ℝ p v) (A * ‖v‖ ^ 2)

Fixed-slope bounded upper-contact openings pass to line-restricted contact loci on nonconstant lines.

source

theorem AleksandrovDifferentiability.preimage_lineMap_upperContactWithSlopeOpeningAtMostSet_subset_of_norm_eq_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p v : E} {A : ℝ} (hv : ‖v‖ = 1) :

{t : ℝ | x + t • v ∈ upperContactWithSlopeOpeningAtMostSet s u p A} ⊆ upperContactWithSlopeOpeningAtMostSet (lineDomain s x v) (lineRestriction u x v) (inner ℝ p v) A

Unit-direction version of preimage_lineMap_upperContactWithSlopeOpeningAtMostSet_subset_of_norm_pos.

source

theorem AleksandrovDifferentiability.ConvexOn.lineRestriction {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x v : E} (hu : ConvexOn ℝ s u) :

ConvexOn ℝ (lineDomain s x v) (AleksandrovDifferentiability.lineRestriction u x v)

Convexity restricts to every affine line.

source

theorem AleksandrovDifferentiability.ConvexOn.tendsto_lineRightDeriv_posLine {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s D : Set E} {u : E → ℝ} {x v : E} (hu : ConvexOn ℝ s u) (hx : x ∈ interior s) :

Filter.Tendsto (fun (t : ℝ) => rightDeriv (AleksandrovDifferentiability.lineRestriction u x v) t) (nhdsWithin 0 {t : ℝ | 0 < t ∧ x + t • v ∈ D}) (nhds (rightDeriv (AleksandrovDifferentiability.lineRestriction u x v) 0))

Convex right-continuity of the line-restricted right derivative, restricted further to a positive line filter through an arbitrary set D.

This is the filter form used in the cluster-gradient reduction: adding the differentiability-set restriction to the positive ray only makes the filter smaller.

source

theorem AleksandrovDifferentiability.lineRightDeriv_eq_inner_of_gradient_mapClusterPt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_3} {l : Filter ι} {u : E → ℝ} {x v q : E} {G : ι → E} {τ : ι → ℝ} (hq : MapClusterPt q l G) (hlim : Filter.Tendsto (fun (a : ι) => rightDeriv (lineRestriction u x v) (τ a)) l (nhds (rightDeriv (lineRestriction u x v) 0))) (hrealize : ∀ᶠ (a : ι) in l, rightDeriv (lineRestriction u x v) (τ a) = inner ℝ (G a) v) :

rightDeriv (lineRestriction u x v) 0 = inner ℝ q v

If vector gradients cluster along a parameter filter, and their directional components eventually realize the right derivative of a line restriction whose right derivatives converge back to the endpoint, then the cluster value has exactly the endpoint right-derivative directional component.

source

theorem AleksandrovDifferentiability.ConvexOn.lineRightDeriv_eq_inner_of_posLine_gradient_mapClusterPt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s D : Set E} {u : E → ℝ} {x v q : E} {G : ℝ → E} (hu : ConvexOn ℝ s u) (hx : x ∈ interior s) (hq : MapClusterPt q (nhdsWithin 0 {t : ℝ | 0 < t ∧ x + t • v ∈ D}) G) (hrealize : ∀ᶠ (t : ℝ) in nhdsWithin 0 {t : ℝ | 0 < t ∧ x + t • v ∈ D}, rightDeriv (AleksandrovDifferentiability.lineRestriction u x v) t = inner ℝ (G t) v) :

rightDeriv (AleksandrovDifferentiability.lineRestriction u x v) 0 = inner ℝ q v

Positive-line convex specialization of lineRightDeriv_eq_inner_of_gradient_mapClusterPt.

source

theorem AleksandrovDifferentiability.ConvexOn.lineRightDeriv_le_inner_of_posLine_gradient_mapClusterPt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s D : Set E} {u : E → ℝ} {x v q : E} {G : ℝ → E} (hu : ConvexOn ℝ s u) (hx : x ∈ interior s) (hq : MapClusterPt q (nhdsWithin 0 {t : ℝ | 0 < t ∧ x + t • v ∈ D}) G) (hrealize : ∀ᶠ (t : ℝ) in nhdsWithin 0 {t : ℝ | 0 < t ∧ x + t • v ∈ D}, rightDeriv (AleksandrovDifferentiability.lineRestriction u x v) t = inner ℝ (G t) v) :

rightDeriv (AleksandrovDifferentiability.lineRestriction u x v) 0 ≤ inner ℝ q v

Inequality form of ConvexOn.lineRightDeriv_eq_inner_of_posLine_gradient_mapClusterPt, matching the current cube-level cluster-density boundary.

source

theorem AleksandrovDifferentiability.rightDeriv_eq_of_hasDerivAt {f : ℝ → ℝ} {x p : ℝ} (h : HasDerivAt f p x) :

rightDeriv f x = p

An ordinary derivative realizes the project-local right derivative.

source

theorem AleksandrovDifferentiability.HasFDerivAt.lineRestriction_at {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x v : E} {t : ℝ} {ℓ : E →L[ℝ ] ℝ} (h : HasFDerivAt u ℓ (x + t • v)) :

HasDerivAt (lineRestriction u x v) (ℓ v) t

Differentiability of u at a point of an affine line differentiates the corresponding line restriction at that parameter.

source

theorem AleksandrovDifferentiability.lineRestriction_rightDeriv_eq_fderiv_apply_of_differentiableAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x v : E} {t : ℝ} (h : DifferentiableAt ℝ u (x + t • v)) :

rightDeriv (lineRestriction u x v) t = (fderiv ℝ u (x + t • v)) v

At a Fréchet differentiability point on an affine line, the line-restricted right derivative is the Fréchet derivative applied to the line direction.

source

theorem AleksandrovDifferentiability.ConvexOn.subgradientOn_of_hasFDerivAt_of_forall_eq_inner {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p : E} {ℓ : E →L[ℝ ] ℝ} (hu : ConvexOn ℝ s u) (hx : x ∈ interior s) (hd : HasFDerivAt u ℓ x) (hℓ : ∀ (v : E), ℓ v = inner ℝ p v) :

SubgradientOn s u x p

A differentiable convex function has its derivative as a subgradient, expressed with an explicit inner-product representative of the Fréchet derivative. The proof follows the source-document convex route: restrict to the line segment from x to y and apply the one-dimensional supporting-line statement.

source

theorem AleksandrovDifferentiability.ConvexOn.ae_lineRightDeriv_differentiableWithinAt_of_mem {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x v : E} (hu : ConvexOn ℝ s u) :

∀ᵐ (t : ℝ), t ∈ interior (lineDomain s x v) → DifferentiableWithinAt ℝ (rightDeriv (AleksandrovDifferentiability.lineRestriction u x v)) (interior (lineDomain s x v)) t

The right derivative of a convex affine-line restriction is differentiable almost everywhere on the interior of the line domain, in implication form.

source

theorem AleksandrovDifferentiability.ConvexOn.ae_lineLeftDeriv_differentiableWithinAt_of_mem {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x v : E} (hu : ConvexOn ℝ s u) :

∀ᵐ (t : ℝ), t ∈ interior (lineDomain s x v) → DifferentiableWithinAt ℝ (leftDeriv (AleksandrovDifferentiability.lineRestriction u x v)) (interior (lineDomain s x v)) t

The left derivative of a convex affine-line restriction is differentiable almost everywhere on the interior of the line domain, in implication form.

source

theorem AleksandrovDifferentiability.ConvexOn.ae_lineRightDeriv_differentiableWithinAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x v : E} (hu : ConvexOn ℝ s u) (hline : MeasurableSet (interior (lineDomain s x v))) :

∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (interior (lineDomain s x v)), DifferentiableWithinAt ℝ (rightDeriv (AleksandrovDifferentiability.lineRestriction u x v)) (interior (lineDomain s x v)) t

Restricted-measure version of ConvexOn.ae_lineRightDeriv_differentiableWithinAt_of_mem.

source

theorem AleksandrovDifferentiability.ConvexOn.ae_lineLeftDeriv_differentiableWithinAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x v : E} (hu : ConvexOn ℝ s u) (hline : MeasurableSet (interior (lineDomain s x v))) :

∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (interior (lineDomain s x v)), DifferentiableWithinAt ℝ (leftDeriv (AleksandrovDifferentiability.lineRestriction u x v)) (interior (lineDomain s x v)) t

Restricted-measure version of ConvexOn.ae_lineLeftDeriv_differentiableWithinAt_of_mem.

source

theorem AleksandrovDifferentiability.ConvexOn.ae_mem_lineOneSidedDerivDifferentiabilitySet_of_mem {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x v : E} (hu : ConvexOn ℝ s u) :

∀ᵐ (t : ℝ), t ∈ interior (lineDomain s x v) → t ∈ oneSidedDerivDifferentiabilitySet (lineDomain s x v) (AleksandrovDifferentiability.lineRestriction u x v)

Both one-sided derivative functions of a convex affine-line restriction are differentiable almost everywhere on the interior of the line domain, in implication form.

source

theorem AleksandrovDifferentiability.ConvexOn.ae_mem_lineOneSidedDerivDifferentiabilitySet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x v : E} (hu : ConvexOn ℝ s u) (hline : MeasurableSet (interior (lineDomain s x v))) :

∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (interior (lineDomain s x v)), t ∈ oneSidedDerivDifferentiabilitySet (lineDomain s x v) (AleksandrovDifferentiability.lineRestriction u x v)

Restricted-measure version of ConvexOn.ae_mem_lineOneSidedDerivDifferentiabilitySet_of_mem.

source

theorem AleksandrovDifferentiability.ConvexOn.measure_interior_lineDomain_diff_rightDerivDifferentiabilitySet_eq_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x v : E} (hu : ConvexOn ℝ s u) :

MeasureTheory.volume (interior (lineDomain s x v) \ rightDerivDifferentiabilitySet (lineDomain s x v) (AleksandrovDifferentiability.lineRestriction u x v)) = 0

The right-derivative differentiability good set for a convex affine-line restriction has full measure in the interior of the line domain.

source

theorem AleksandrovDifferentiability.ConvexOn.measure_interior_lineDomain_diff_leftDerivDifferentiabilitySet_eq_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x v : E} (hu : ConvexOn ℝ s u) :

MeasureTheory.volume (interior (lineDomain s x v) \ leftDerivDifferentiabilitySet (lineDomain s x v) (AleksandrovDifferentiability.lineRestriction u x v)) = 0

The left-derivative differentiability good set for a convex affine-line restriction has full measure in the interior of the line domain.

source

theorem AleksandrovDifferentiability.ConvexOn.measure_lineInterior_diff_oneSidedDerivDifferentiabilitySet_eq_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x v : E} (hu : ConvexOn ℝ s u) :

MeasureTheory.volume (interior (lineDomain s x v) \ oneSidedDerivDifferentiabilitySet (lineDomain s x v) (AleksandrovDifferentiability.lineRestriction u x v)) = 0

The combined one-sided-derivative differentiability good set for a convex affine-line restriction has full measure in the interior of the line domain.

source

theorem AleksandrovDifferentiability.ConvexOn.lineRestriction_subgradientOn_iff_deriv_bounds {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x v : E} {q : ℝ} (hu : ConvexOn ℝ s u) (h0 : 0 ∈ interior (lineDomain s x v)) :

SubgradientOn (lineDomain s x v) (AleksandrovDifferentiability.lineRestriction u x v) 0 q ↔ leftDeriv (AleksandrovDifferentiability.lineRestriction u x v) 0 ≤ q ∧ q ≤ rightDeriv (AleksandrovDifferentiability.lineRestriction u x v) 0

On a line restriction of a convex function, a slope is a one-dimensional subgradient at 0 exactly when it lies between the left and right derivatives there.

source

theorem AleksandrovDifferentiability.ConvexOn.lineRestriction_subgradientOn_iff_deriv_bounds_of_mem_interior {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x v : E} {q : ℝ} (hu : ConvexOn ℝ s u) (hx : x ∈ interior s) :

Interior-domain version of the derivative-bound characterization of subgradients on a line restriction.

source

theorem AleksandrovDifferentiability.ConvexOn.lineRestriction_rightDeriv_subgradientOn_at {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x v : E} {t : ℝ} (hu : ConvexOn ℝ s u) (ht : t ∈ interior (lineDomain s x v)) :

SubgradientOn (lineDomain s x v) (AleksandrovDifferentiability.lineRestriction u x v) t (rightDeriv (AleksandrovDifferentiability.lineRestriction u x v) t)

For a convex affine-line restriction, the right derivative at an interior line parameter is itself a one-dimensional subgradient. This is the one-dimensional half of the source-document identity d⁺/dt u(x + t z) = sup {p · z | p ∈ ∂u(x + t z)}.

source

theorem AleksandrovDifferentiability.ConvexOn.lineRestriction_rightDeriv_subgradientOn_at_of_line_mem_interior {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x v : E} {t : ℝ} (hu : ConvexOn ℝ s u) (ht : x + t • v ∈ interior s) :

SubgradientOn (lineDomain s x v) (AleksandrovDifferentiability.lineRestriction u x v) t (rightDeriv (AleksandrovDifferentiability.lineRestriction u x v) t)

Ambient-interior version of ConvexOn.lineRestriction_rightDeriv_subgradientOn_at.

source

theorem AleksandrovDifferentiability.ConvexOn.lineRestriction_leftDeriv_subgradientOn_at {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x v : E} {t : ℝ} (hu : ConvexOn ℝ s u) (ht : t ∈ interior (lineDomain s x v)) :

SubgradientOn (lineDomain s x v) (AleksandrovDifferentiability.lineRestriction u x v) t (leftDeriv (AleksandrovDifferentiability.lineRestriction u x v) t)

For a convex affine-line restriction, the left derivative at an interior line parameter is itself a one-dimensional subgradient.

source

theorem AleksandrovDifferentiability.ConvexOn.lineRestriction_leftDeriv_subgradientOn_at_of_line_mem_interior {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x v : E} {t : ℝ} (hu : ConvexOn ℝ s u) (ht : x + t • v ∈ interior s) :

SubgradientOn (lineDomain s x v) (AleksandrovDifferentiability.lineRestriction u x v) t (leftDeriv (AleksandrovDifferentiability.lineRestriction u x v) t)

Ambient-interior version of ConvexOn.lineRestriction_leftDeriv_subgradientOn_at.

Documentation

LeanPool.ViscositySolutionTheory.AleksandrovDifferentiability.Analysis.LineRestriction.Basic

Restrictions to affine lines #