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

Second order expansions on affine lines

This file connects the ambient second-order expansion predicate to one-dimensional restrictions along affine lines.

theorem AleksandrovDifferentiability.HasSecondOrderExpansionAt.lineRestriction_isLittleO {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x p : E} {B : E →L[ℝ] E} (h : HasSecondOrderExpansionAt u x p B) (v : E) : (fun (t : ℝ) => lineRestriction u x v t - u x - inner ℝ p v * t - 1 / 2 * inner ℝ v (B v) * t ^ 2) =o[nhds 0] fun (t : ℝ) => ‖t • v‖ ^ 2

An ambient second-order expansion restricts to a second-order expansion along every affine line, with the expected directional first and second coefficients.

theorem AleksandrovDifferentiability.HasSecondOrderExpansionAt.lineRestriction_isLittleO_of_norm_eq_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x p v : E} {B : E →L[ℝ] E} (h : HasSecondOrderExpansionAt u x p B) (hv : ‖v‖ = 1) : (fun (t : ℝ) => lineRestriction u x v t - u x - inner ℝ p v * t - 1 / 2 * inner ℝ v (B v) * t ^ 2) =o[nhds 0] fun (t : ℝ) => ‖t‖ ^ 2

Unit-direction version of HasSecondOrderExpansionAt.lineRestriction_isLittleO, with the standard one-dimensional denominator.

theorem AleksandrovDifferentiability.HasSecondOrderExpansionAt.lineRestriction_isLittleO_standard {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x p : E} {B : E →L[ℝ] E} (h : HasSecondOrderExpansionAt u x p B) (v : E) : (fun (t : ℝ) => lineRestriction u x v t - u x - inner ℝ p v * t - 1 / 2 * inner ℝ v (B v) * t ^ 2) =o[nhds 0] fun (t : ℝ) => ‖t‖ ^ 2

An ambient second-order expansion restricts to an affine line with the standard one-dimensional little-o denominator.

theorem AleksandrovDifferentiability.HasSecondOrderExpansionAt.lineRestriction_hasSecondOrderExpansionAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x p : E} {B : E →L[ℝ] E} (h : HasSecondOrderExpansionAt u x p B) (v : E) : HasSecondOrderExpansionAt (lineRestriction u x v) 0 (inner ℝ p v) (inner ℝ v (B v) • 1)

Ambient second-order expansions restrict to project-level second-order expansions of one-dimensional line restrictions.

theorem AleksandrovDifferentiability.HasSecondOrderExpansionAt.lineRestriction_at_hasSecondOrderExpansionAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x p v : E} {B : E →L[ℝ] E} {t : ℝ} (h : HasSecondOrderExpansionAt u (x + t • v) p B) : HasSecondOrderExpansionAt (lineRestriction u x v) t (inner ℝ p v) (inner ℝ v (B v) • 1)

Ambient second-order expansions restrict to affine lines at arbitrary line parameters.

theorem AleksandrovDifferentiability.HasSecondOrderExpansionAtCLM.lineRestriction_isLittleO {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x : E} {ℓ : E →L[ℝ] ℝ} {B : E →L[ℝ] E} (h : HasSecondOrderExpansionAtCLM u x ℓ B) (v : E) : (fun (t : ℝ) => lineRestriction u x v t - u x - ℓ v * t - 1 / 2 * inner ℝ v (B v) * t ^ 2) =o[nhds 0] fun (t : ℝ) => ‖t • v‖ ^ 2

An ambient CLM-gradient second-order expansion restricts to a second-order expansion along every affine line, with the expected directional first and second coefficients.

theorem AleksandrovDifferentiability.HasSecondOrderExpansionAtCLM.lineRestriction_isLittleO_of_norm_eq_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x v : E} {ℓ : E →L[ℝ] ℝ} {B : E →L[ℝ] E} (h : HasSecondOrderExpansionAtCLM u x ℓ B) (hv : ‖v‖ = 1) : (fun (t : ℝ) => lineRestriction u x v t - u x - ℓ v * t - 1 / 2 * inner ℝ v (B v) * t ^ 2) =o[nhds 0] fun (t : ℝ) => ‖t‖ ^ 2

Unit-direction version of HasSecondOrderExpansionAtCLM.lineRestriction_isLittleO, with the standard one-dimensional denominator.

theorem AleksandrovDifferentiability.HasSecondOrderExpansionAtCLM.lineRestriction_isLittleO_standard {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x : E} {ℓ : E →L[ℝ] ℝ} {B : E →L[ℝ] E} (h : HasSecondOrderExpansionAtCLM u x ℓ B) (v : E) : (fun (t : ℝ) => lineRestriction u x v t - u x - ℓ v * t - 1 / 2 * inner ℝ v (B v) * t ^ 2) =o[nhds 0] fun (t : ℝ) => ‖t‖ ^ 2

An ambient CLM-gradient second-order expansion restricts to an affine line with the standard one-dimensional little-o denominator.

theorem AleksandrovDifferentiability.HasSecondOrderExpansionAtCLM.lineRestriction_hasSecondOrderExpansionAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x : E} {ℓ : E →L[ℝ] ℝ} {B : E →L[ℝ] E} (h : HasSecondOrderExpansionAtCLM u x ℓ B) (v : E) : HasSecondOrderExpansionAt (lineRestriction u x v) 0 (ℓ v) (inner ℝ v (B v) • 1)

Ambient CLM-gradient second-order expansions restrict to project-level second-order expansions of one-dimensional line restrictions.

theorem AleksandrovDifferentiability.HasSecondOrderExpansionAtCLM.lineRestriction_at_hasSecondOrderExpansionAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x v : E} {ℓ : E →L[ℝ] ℝ} {B : E →L[ℝ] E} {t : ℝ} (h : HasSecondOrderExpansionAtCLM u (x + t • v) ℓ B) : HasSecondOrderExpansionAt (lineRestriction u x v) t (ℓ v) (inner ℝ v (B v) • 1)

Ambient CLM-gradient second-order expansions restrict to affine lines at arbitrary line parameters.

theorem AleksandrovDifferentiability.isSymmetricOperator_real_smul_one (c : ℝ) : IsSymmetricOperator (c • 1)

On the real line, every scalar multiple of the identity is a symmetric operator.

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

Second order differentiability restricts to every affine line.

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

Second order differentiability restricts to affine lines at arbitrary line parameters.

theorem AleksandrovDifferentiability.preimage_lineMap_secondOrderExpansionSet_subset {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x p v : E} {B : E →L[ℝ] E} : {t : ℝ | x + t • v ∈ secondOrderExpansionSet u p B} ⊆ secondOrderExpansionSet (lineRestriction u x v) (inner ℝ p v) (inner ℝ v (B v) • 1)

The preimage of a fixed ambient second-order expansion locus along a line is contained in the corresponding one-dimensional expansion locus.

theorem AleksandrovDifferentiability.preimage_lineMap_secondOrderExpansionSetCLM_subset {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x v : E} {ℓ : E →L[ℝ] ℝ} {B : E →L[ℝ] E} : {t : ℝ | x + t • v ∈ secondOrderExpansionSetCLM u ℓ B} ⊆ secondOrderExpansionSet (lineRestriction u x v) (ℓ v) (inner ℝ v (B v) • 1)

The preimage of a fixed ambient CLM expansion locus along a line is contained in the corresponding one-dimensional expansion locus.

theorem AleksandrovDifferentiability.preimage_lineMap_secondOrderDifferentiabilitySet_subset {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x v : E} : {t : ℝ | x + t • v ∈ secondOrderDifferentiabilitySet u} ⊆ secondOrderDifferentiabilitySet (lineRestriction u x v)

The preimage of the ambient second-order differentiability locus along a line is contained in the one-dimensional second-order differentiability locus of the line restriction.

theorem AleksandrovDifferentiability.preimage_lineMap_secondOrderCLMExpansionDataSet_subset {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x v : E} : {t : ℝ | x + t • v ∈ secondOrderCLMExpansionDataSet u} ⊆ secondOrderDifferentiabilitySet (lineRestriction u x v)

The preimage of the ambient CLM expansion-data locus along a line is contained in the one-dimensional second-order differentiability locus of the line restriction.

theorem AleksandrovDifferentiability.lineRestriction_secondOrderDifferentiabilitySet_subset_realScalarQuadraticEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x v : E} : secondOrderDifferentiabilitySet (lineRestriction u x v) ⊆ realScalarQuadraticEstimateSet (lineRestriction u x v)

On a line restriction, project-level one-dimensional second-order differentiability gives the scalar quadratic estimate format used by the one-dimensional assembly layer.

theorem AleksandrovDifferentiability.preimage_lineMap_secondOrderDifferentiabilitySet_subset_realScalarQuadraticEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x v : E} : {t : ℝ | x + t • v ∈ secondOrderDifferentiabilitySet u} ⊆ realScalarQuadraticEstimateSet (lineRestriction u x v)

Ambient second-order differentiability along a line implies scalar quadratic estimate data for the corresponding one-dimensional line restriction.

theorem AleksandrovDifferentiability.preimage_lineMap_secondOrderCLMExpansionDataSet_subset_realScalarQuadraticEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x v : E} : {t : ℝ | x + t • v ∈ secondOrderCLMExpansionDataSet u} ⊆ realScalarQuadraticEstimateSet (lineRestriction u x v)

Ambient CLM expansion data along a line implies scalar quadratic estimate data for the corresponding one-dimensional line restriction.

theorem AleksandrovDifferentiability.lineRestriction_secondOrderDifferentiabilitySet_subset_realScalarQuadraticQuotientSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x v : E} : secondOrderDifferentiabilitySet (lineRestriction u x v) ⊆ realScalarQuadraticQuotientEstimateSet (lineRestriction u x v)

On a line restriction, project-level one-dimensional second-order differentiability gives the punctured scalar quotient-estimate format used by the one-dimensional assembly layer.

theorem AleksandrovDifferentiability.preimage_lineMap_secondOrderDifferentiabilitySet_subset_realScalarQuadraticQuotientSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x v : E} : {t : ℝ | x + t • v ∈ secondOrderDifferentiabilitySet u} ⊆ realScalarQuadraticQuotientEstimateSet (lineRestriction u x v)

Ambient second-order differentiability along a line implies scalar quotient-estimate data for the corresponding one-dimensional line restriction.

theorem AleksandrovDifferentiability.preimage_lineMap_secondOrderCLMExpansionDataSet_subset_realScalarQuadraticQuotientSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x v : E} : {t : ℝ | x + t • v ∈ secondOrderCLMExpansionDataSet u} ⊆ realScalarQuadraticQuotientEstimateSet (lineRestriction u x v)

Ambient CLM expansion data along a line implies scalar quotient-estimate data for the corresponding one-dimensional line restriction.