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

Second order expansion interfaces

This file contains the local formulation of second order differentiability used for the convex Aleksandrov theorem.

def AleksandrovDifferentiability.IsSymmetricOperator {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] (B : E →L[ℝ] E) : Prop

A continuous linear operator is symmetric with respect to the real inner product.

Equations

• AleksandrovDifferentiability.IsSymmetricOperator B = (↑B).IsSymmetric

def AleksandrovDifferentiability.HasSecondOrderExpansionAt {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] (u : E → ℝ) (x p : E) (B : E →L[ℝ] E) : Prop

The concrete quadratic second order expansion at x, written in increment coordinates.

The point p is the first-order vector and B is the Hessian candidate. The quadratic term is (1 / 2) * ⟪z, B z⟫_ℝ, the usual inner-product notation for z · B z / 2.

Equations

• AleksandrovDifferentiability.HasSecondOrderExpansionAt u x p B = (fun (z : E) => u (x + z) - u x - inner ℝ p z - 1 / 2 * inner ℝ z (B z)) =o[nhds 0] fun (z : E) => ‖z‖ ^ 2

def AleksandrovDifferentiability.HasSecondOrderExpansionAtCLM {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] (u : E → ℝ) (x : E) (ℓ : E →L[ℝ] ℝ) (B : E →L[ℝ] E) : Prop

A second-order expansion whose first-order term is a continuous linear functional.

Mathlib's Fréchet derivative of a scalar-valued map has this shape. The project theorem statement uses gradient vectors instead, so hasSecondOrderExpansionAt_of_clm below converts this interface through the Fréchet-Riesz representation theorem.

Equations

• AleksandrovDifferentiability.HasSecondOrderExpansionAtCLM u x ℓ B = (fun (z : E) => u (x + z) - u x - ℓ z - 1 / 2 * inner ℝ z (B z)) =o[nhds 0] fun (z : E) => ‖z‖ ^ 2

def AleksandrovDifferentiability.SecondOrderDifferentiableAt {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] (u : E → ℝ) (x : E) : Prop

Second order differentiability at a point, with a symmetric Hessian candidate.

Equations

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

def AleksandrovDifferentiability.secondOrderExpansionSet {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] (u : E → ℝ) (p : E) (B : E →L[ℝ] E) : Set E

Points where u has the prescribed second-order expansion data (p, B).

Equations

• AleksandrovDifferentiability.secondOrderExpansionSet u p B = {x : E | AleksandrovDifferentiability.HasSecondOrderExpansionAt u x p B}

def AleksandrovDifferentiability.secondOrderExpansionSetCLM {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] (u : E → ℝ) (ℓ : E →L[ℝ] ℝ) (B : E →L[ℝ] E) : Set E

Points where u has prescribed second-order expansion data whose first-order term is the continuous linear functional ℓ.

Equations

• AleksandrovDifferentiability.secondOrderExpansionSetCLM u ℓ B = {x : E | AleksandrovDifferentiability.HasSecondOrderExpansionAtCLM u x ℓ B}

def AleksandrovDifferentiability.secondOrderCLMExpansionDataSet {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] (u : E → ℝ) : Set E

Points where u carries some symmetric second-order expansion data whose first-order term is a continuous linear functional. In Hilbert spaces this is another route into secondOrderDifferentiabilitySet, via Fréchet-Riesz.

Equations

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

def AleksandrovDifferentiability.secondOrderDifferentiabilitySet {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] (u : E → ℝ) : Set E

Points where u is second-order differentiable in the project sense.

Equations

• AleksandrovDifferentiability.secondOrderDifferentiabilitySet u = {x : E | AleksandrovDifferentiability.SecondOrderDifferentiableAt u x}

@[simp]

theorem AleksandrovDifferentiability.mem_secondOrderExpansionSet {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x p : E} {B : E →L[ℝ] E} : x ∈ secondOrderExpansionSet u p B ↔ HasSecondOrderExpansionAt u x p B

@[simp]

theorem AleksandrovDifferentiability.mem_secondOrderExpansionSetCLM {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x : E} {ℓ : E →L[ℝ] ℝ} {B : E →L[ℝ] E} : x ∈ secondOrderExpansionSetCLM u ℓ B ↔ HasSecondOrderExpansionAtCLM u x ℓ B

@[simp]

theorem AleksandrovDifferentiability.mem_secondOrderCLMExpansionDataSet {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x : E} : x ∈ secondOrderCLMExpansionDataSet u ↔ ∃ (ℓ : E →L[ℝ] ℝ) (B : E →L[ℝ] E), IsSymmetricOperator B ∧ HasSecondOrderExpansionAtCLM u x ℓ B

@[simp]

theorem AleksandrovDifferentiability.mem_secondOrderDifferentiabilitySet {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x : E} : x ∈ secondOrderDifferentiabilitySet u ↔ SecondOrderDifferentiableAt u x

theorem AleksandrovDifferentiability.secondOrderDifferentiableAt_of_hasSecondOrderExpansionAt {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x p : E} {B : E →L[ℝ] E} (hB : IsSymmetricOperator B) (h : HasSecondOrderExpansionAt u x p B) : SecondOrderDifferentiableAt u x

noncomputable def AleksandrovDifferentiability.symmetricPartCLM {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (B : H →L[ℝ] H) : H →L[ℝ] H

The symmetric part of a continuous linear operator. The quadratic form z ↦ inner ℝ z (B z) only depends on this symmetric part.

Equations

• AleksandrovDifferentiability.symmetricPartCLM B = (1 / 2) • (B + ContinuousLinearMap.adjoint B)

theorem AleksandrovDifferentiability.isSymmetricOperator_symmetricPartCLM {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (B : H →L[ℝ] H) : IsSymmetricOperator (symmetricPartCLM B)

The symmetric part is symmetric.

theorem AleksandrovDifferentiability.inner_symmetricPartCLM_self {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (B : H →L[ℝ] H) (z : H) : inner ℝ z ((symmetricPartCLM B) z) = inner ℝ z (B z)

The quadratic form of an operator agrees with that of its symmetric part.

theorem AleksandrovDifferentiability.HasSecondOrderExpansionAt.symmetricPart {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {u : H → ℝ} {x p : H} {B : H →L[ℝ] H} (h : HasSecondOrderExpansionAt u x p B) : HasSecondOrderExpansionAt u x p (symmetricPartCLM B)

A second-order expansion may always be rewritten with the symmetric part of its quadratic operator.

theorem AleksandrovDifferentiability.secondOrderDifferentiableAt_of_hasSecondOrderExpansionAt_symmetricPart {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {u : H → ℝ} {x p : H} {B : H →L[ℝ] H} (h : HasSecondOrderExpansionAt u x p B) : SecondOrderDifferentiableAt u x

A second-order expansion with any continuous linear quadratic operator gives second-order differentiability by replacing the operator with its symmetric part.

@[simp]

theorem AleksandrovDifferentiability.isSymmetricOperator_zero_operator {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] : IsSymmetricOperator 0

theorem AleksandrovDifferentiability.hasSecondOrderExpansionAt_const {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] (c : ℝ) (x : E) : HasSecondOrderExpansionAt (fun (x : E) => c) x 0 0

Constant functions have zero second-order expansion everywhere.

theorem AleksandrovDifferentiability.secondOrderDifferentiableAt_const {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] (c : ℝ) (x : E) : SecondOrderDifferentiableAt (fun (x : E) => c) x

Constant functions are second-order differentiable everywhere.

theorem AleksandrovDifferentiability.hasSecondOrderExpansionAt_inner_add_const {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] (p : E) (c : ℝ) (x : E) : HasSecondOrderExpansionAt (fun (y : E) => inner ℝ p y + c) x p 0

Affine functions represented by an inner-product slope have zero Hessian everywhere.

theorem AleksandrovDifferentiability.secondOrderDifferentiableAt_inner_add_const {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] (p : E) (c : ℝ) (x : E) : SecondOrderDifferentiableAt (fun (y : E) => inner ℝ p y + c) x

Affine functions represented by an inner-product slope are second-order differentiable everywhere.

theorem AleksandrovDifferentiability.IsSymmetricOperator.smul {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {B : E →L[ℝ] E} (hB : IsSymmetricOperator B) (c : ℝ) : IsSymmetricOperator (c • B)

Symmetry is preserved by scalar multiplication of the operator.

theorem AleksandrovDifferentiability.HasSecondOrderExpansionAt.of_comp_add_smul {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {a z p : E} {B : E →L[ℝ] E} {r : ℝ} (hr : r ≠ 0) (h : HasSecondOrderExpansionAt (fun (y : E) => u (a + r • y)) z p B) : HasSecondOrderExpansionAt u (a + r • z) (r⁻¹ • p) (r⁻¹ ^ 2 • B)

Pull a second-order expansion back across a nonzero scalar dilation and translation.

If z ↦ u (a + r • z) has expansion data (p, B) at z, then u has expansion data (r⁻¹ • p, (r⁻¹)^2 • B) at a + r • z. This is the local transport step needed for the source-cube-to-open-domain localization.

theorem AleksandrovDifferentiability.SecondOrderDifferentiableAt.of_comp_add_smul {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {a z : E} {r : ℝ} (hr : r ≠ 0) (h : SecondOrderDifferentiableAt (fun (y : E) => u (a + r • y)) z) : SecondOrderDifferentiableAt u (a + r • z)

Second-order differentiability is transported back across a nonzero scalar dilation and translation.

theorem AleksandrovDifferentiability.secondOrderDifferentiableAt_of_subsingleton {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [Subsingleton E] (u : E → ℝ) (x : E) : SecondOrderDifferentiableAt u x

On a subsingleton inner product space every function is second-order differentiable at every point. This records the degenerate finite-dimensional endpoint used as a sanity check for the theorem-boundary statements.

theorem AleksandrovDifferentiability.secondOrderDifferentiableAt_of_finrank_eq_zero {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (hE : Module.finrank ℝ E = 0) (u : E → ℝ) (x : E) : SecondOrderDifferentiableAt u x

Finite-dimensional rank-zero version of secondOrderDifferentiableAt_of_subsingleton.

theorem AleksandrovDifferentiability.hasSecondOrderExpansionAt_of_clm_eq_inner {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x p : E} {ℓ : E →L[ℝ] ℝ} {B : E →L[ℝ] E} (hℓ : ∀ (z : E), ℓ z = inner ℝ p z) (h : HasSecondOrderExpansionAtCLM u x ℓ B) : HasSecondOrderExpansionAt u x p B

Convert a scalar first-order continuous-linear-map expansion into the project expansion format when the linear functional is represented by inner product with p.

theorem AleksandrovDifferentiability.secondOrderDifferentiableAt_of_hasSecondOrderExpansionAtCLM_eq_inner {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x p : E} {ℓ : E →L[ℝ] ℝ} {B : E →L[ℝ] E} (hℓ : ∀ (z : E), ℓ z = inner ℝ p z) (hB : IsSymmetricOperator B) (h : HasSecondOrderExpansionAtCLM u x ℓ B) : SecondOrderDifferentiableAt u x

A continuous-linear-map first-order expansion with a symmetric Hessian candidate gives second-order differentiability in the project sense, provided the linear functional is represented by inner product with p.

theorem AleksandrovDifferentiability.hasSecondOrderExpansionAt_of_clm {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {u : H → ℝ} {x : H} {ℓ : H →L[ℝ] ℝ} {B : H →L[ℝ] H} (h : HasSecondOrderExpansionAtCLM u x ℓ B) : HasSecondOrderExpansionAt u x ((InnerProductSpace.toDual ℝ H).symm ℓ) B

In a real Hilbert space, convert a scalar first-order continuous-linear-map expansion into the project expansion format by representing the functional via Fréchet-Riesz.

theorem AleksandrovDifferentiability.secondOrderDifferentiableAt_of_hasSecondOrderExpansionAtCLM {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {u : H → ℝ} {x : H} {ℓ : H →L[ℝ] ℝ} {B : H →L[ℝ] H} (hB : IsSymmetricOperator B) (h : HasSecondOrderExpansionAtCLM u x ℓ B) : SecondOrderDifferentiableAt u x

A continuous-linear-map first-order expansion with a symmetric Hessian candidate gives second-order differentiability in a real Hilbert space.

theorem AleksandrovDifferentiability.secondOrderExpansionSetCLM_subset_secondOrderDifferentiabilitySet {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {u : H → ℝ} {ℓ : H →L[ℝ] ℝ} {B : H →L[ℝ] H} (hB : IsSymmetricOperator B) : secondOrderExpansionSetCLM u ℓ B ⊆ secondOrderDifferentiabilitySet u

A fixed CLM expansion locus with symmetric Hessian lies inside the project differentiability locus in a real Hilbert space.

theorem AleksandrovDifferentiability.secondOrderCLMExpansionDataSet_subset_secondOrderDifferentiabilitySet {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {u : H → ℝ} : secondOrderCLMExpansionDataSet u ⊆ secondOrderDifferentiabilitySet u

The CLM expansion-data locus lies inside the project differentiability locus in a real Hilbert space.

theorem AleksandrovDifferentiability.secondOrderExpansionSet_subset_secondOrderDifferentiabilitySet {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {p : E} {B : E →L[ℝ] E} (hB : IsSymmetricOperator B) : secondOrderExpansionSet u p B ⊆ secondOrderDifferentiabilitySet u