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

Ambient quadratic estimates

Ambient quadratic remainder estimate predicates and their connection to second-order expansions.

theorem AleksandrovDifferentiability.hasSecondOrderExpansionAt_iff_affineRemainder {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x p : E} {B : E →L[ℝ] E} : HasSecondOrderExpansionAt u x p B ↔ (fun (z : E) => affineRemainder u x p (x + z) - 1 / 2 * inner ℝ z (B z)) =o[nhds 0] fun (z : E) => ‖z‖ ^ 2

The second-order expansion predicate can be read as a quadratic expansion of the affine remainder after subtracting the first-order slope.

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

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

theorem AleksandrovDifferentiability.eventually_norm_sum_le_sum_mul {α : Type u_3} {V : Type u_4} {ι : Type u_5} [SeminormedAddCommGroup V] {l : Filter α} (s : Finset ι) (F : ι → α → V) (c : ι → ℝ) (φ : α → ℝ) (h : ∀ i ∈ s, ∀ᶠ (x : α) in l, ‖F i x‖ ≤ c i * φ x) : ∀ᶠ (x : α) in l, ‖∑ i ∈ s, F i x‖ ≤ (∑ i ∈ s, c i) * φ x

Finite eventually-valid norm bounds can be summed on a common neighborhood. This packages the filter bookkeeping needed when several one-dimensional remainder estimates are combined.

theorem AleksandrovDifferentiability.eventually_norm_sum_le_card_mul {α : Type u_3} {V : Type u_4} {ι : Type u_5} [SeminormedAddCommGroup V] {l : Filter α} (s : Finset ι) (F : ι → α → V) (c : ℝ) (φ : α → ℝ) (h : ∀ i ∈ s, ∀ᶠ (x : α) in l, ‖F i x‖ ≤ c * φ x) : ∀ᶠ (x : α) in l, ‖∑ i ∈ s, F i x‖ ≤ ↑s.card * c * φ x

Common-constant version of eventually_norm_sum_le_sum_mul.

theorem AleksandrovDifferentiability.eventually_norm_sum_div_le_sum {α : Type u_3} {V : Type u_4} {ι : Type u_5} [SeminormedAddCommGroup V] {l : Filter α} (s : Finset ι) (F : ι → α → V) (c : ι → ℝ) (φ : α → ℝ) (hφ : ∀ᶠ (x : α) in l, 0 < φ x) (h : ∀ i ∈ s, ∀ᶠ (x : α) in l, ‖F i x‖ / φ x ≤ c i) : ∀ᶠ (x : α) in l, ‖∑ i ∈ s, F i x‖ / φ x ≤ ∑ i ∈ s, c i

Finite summation for punctured normalized quotient bounds.

theorem AleksandrovDifferentiability.affineRemainder_sub_quadratic_isLittleO_of_eventually_norm_le_mul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x p : E} {B : E →L[ℝ] E} (h : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (z : E) in nhds 0, ‖affineRemainder u x p (x + z) - 1 / 2 * inner ℝ z (B z)‖ ≤ ε * ‖z‖ ^ 2) : (fun (z : E) => affineRemainder u x p (x + z) - 1 / 2 * inner ℝ z (B z)) =o[nhds 0] fun (z : E) => ‖z‖ ^ 2

A neighborhood family of quadratic norm bounds for the remainder after subtracting a proposed quadratic part is exactly the estimate needed for the project second-order expansion predicate.

theorem AleksandrovDifferentiability.hasSecondOrderExpansionAt_of_eventually_norm_affineRemainder_sub_quadratic_le_mul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x p : E} {B : E →L[ℝ] E} (h : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (z : E) in nhds 0, ‖affineRemainder u x p (x + z) - 1 / 2 * inner ℝ z (B z)‖ ≤ ε * ‖z‖ ^ 2) : HasSecondOrderExpansionAt u x p B

Local quadratic norm estimates after subtracting a proposed quadratic part give the corresponding second-order expansion.

theorem AleksandrovDifferentiability.secondOrderDifferentiableAt_of_eventually_norm_affineRemainder_sub_quadratic_le_mul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x p : E} {B : E →L[ℝ] E} (hB : IsSymmetricOperator B) (h : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (z : E) in nhds 0, ‖affineRemainder u x p (x + z) - 1 / 2 * inner ℝ z (B z)‖ ≤ ε * ‖z‖ ^ 2) : SecondOrderDifferentiableAt u x

Local quadratic norm estimates after subtracting a symmetric proposed quadratic part give second-order differentiability.

theorem AleksandrovDifferentiability.affineRemainder_sub_quadratic_isLittleO_of_eventually_norm_div_norm_sq_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x p : E} {B : E →L[ℝ] E} (h : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (z : E) in nhdsWithin 0 {z : E | z ≠ 0}, ‖affineRemainder u x p (x + z) - 1 / 2 * inner ℝ z (B z)‖ / ‖z‖ ^ 2 ≤ ε) : (fun (z : E) => affineRemainder u x p (x + z) - 1 / 2 * inner ℝ z (B z)) =o[nhds 0] fun (z : E) => ‖z‖ ^ 2

A punctured-neighborhood normalized quotient bound after subtracting a proposed quadratic part gives the little-o estimate for the project second-order expansion predicate.

theorem AleksandrovDifferentiability.hasSecondOrderExpansionAt_of_eventually_norm_affineRemainder_sub_quadratic_div_norm_sq_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x p : E} {B : E →L[ℝ] E} (h : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (z : E) in nhdsWithin 0 {z : E | z ≠ 0}, ‖affineRemainder u x p (x + z) - 1 / 2 * inner ℝ z (B z)‖ / ‖z‖ ^ 2 ≤ ε) : HasSecondOrderExpansionAt u x p B

A punctured-neighborhood normalized quotient bound after subtracting a proposed quadratic part gives the corresponding second-order expansion.

theorem AleksandrovDifferentiability.secondOrderDifferentiableAt_of_eventually_norm_affineRemainder_sub_quadratic_div_norm_sq_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x p : E} {B : E →L[ℝ] E} (hB : IsSymmetricOperator B) (h : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (z : E) in nhdsWithin 0 {z : E | z ≠ 0}, ‖affineRemainder u x p (x + z) - 1 / 2 * inner ℝ z (B z)‖ / ‖z‖ ^ 2 ≤ ε) : SecondOrderDifferentiableAt u x

A punctured-neighborhood normalized quotient bound after subtracting a symmetric proposed quadratic part gives second-order differentiability.

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

Pointwise ambient quadratic estimate data: a first-order slope, a symmetric Hessian candidate, and local ε * ‖z‖ ^ 2 control of the quadratic remainder.

Equations

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

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

Punctured normalized quotient version of QuadraticEstimateAt.

Equations

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

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

Points carrying ambient quadratic estimate data.

Equations

• AleksandrovDifferentiability.quadraticEstimateSet u = {x : E | AleksandrovDifferentiability.QuadraticEstimateAt u x}

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

Points carrying punctured normalized ambient quadratic estimate data.

Equations

• AleksandrovDifferentiability.quadraticQuotientEstimateSet u = {x : E | AleksandrovDifferentiability.QuadraticQuotientEstimateAt u x}

@[simp]

theorem AleksandrovDifferentiability.mem_quadraticEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x : E} : x ∈ quadraticEstimateSet u ↔ QuadraticEstimateAt u x

@[simp]

theorem AleksandrovDifferentiability.mem_quadraticQuotientEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x : E} : x ∈ quadraticQuotientEstimateSet u ↔ QuadraticQuotientEstimateAt u x

def AleksandrovDifferentiability.linearIsometryEquivConjCLM {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (e : E ≃ₗᵢ[ℝ] F) (B : F →L[ℝ] F) : E →L[ℝ] E

Conjugate a continuous linear operator by a linear isometry equivalence. This is the Hessian candidate obtained when pulling quadratic estimate data back from an isometric coordinate model.

Equations

• AleksandrovDifferentiability.linearIsometryEquivConjCLM e B = e.symm.toLinearIsometry.toContinuousLinearMap ∘SL B ∘SL e.toLinearIsometry.toContinuousLinearMap

theorem AleksandrovDifferentiability.isSymmetricOperator_linearIsometryEquivConjCLM {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (e : E ≃ₗᵢ[ℝ] F) {B : F →L[ℝ] F} (hB : IsSymmetricOperator B) : IsSymmetricOperator (linearIsometryEquivConjCLM e B)

Symmetry of a Hessian candidate is preserved by isometric coordinate conjugation.

theorem AleksandrovDifferentiability.inner_linearIsometryEquivConjCLM_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (e : E ≃ₗᵢ[ℝ] F) (B : F →L[ℝ] F) (z : E) : inner ℝ z ((linearIsometryEquivConjCLM e B) z) = inner ℝ (e z) (B (e z))

The quadratic form of a conjugated operator is the coordinate-model quadratic form.

theorem AleksandrovDifferentiability.QuadraticEstimateAt.of_image_linearIsometryEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {u : E → ℝ} (e : E ≃ₗᵢ[ℝ] F) {x : E} (h : QuadraticEstimateAt (u ∘ ⇑e.symm) (e x)) : QuadraticEstimateAt u x

Pull back ambient quadratic estimate data from an isometric coordinate model.

theorem AleksandrovDifferentiability.QuadraticQuotientEstimateAt.of_image_linearIsometryEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {u : E → ℝ} (e : E ≃ₗᵢ[ℝ] F) {x : E} (h : QuadraticQuotientEstimateAt (u ∘ ⇑e.symm) (e x)) : QuadraticQuotientEstimateAt u x

Pull back punctured normalized ambient quadratic estimate data from an isometric coordinate model.

theorem AleksandrovDifferentiability.quadraticEstimateAt_comp_linearIsometryEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (e : E ≃ₗᵢ[ℝ] F) {u : F → ℝ} {x : E} : QuadraticEstimateAt (u ∘ ⇑e) x ↔ QuadraticEstimateAt u (e x)

Pointwise transport of ambient quadratic estimate data through a linear isometry equivalence.

theorem AleksandrovDifferentiability.quadraticEstimateSet_comp_linearIsometryEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (e : E ≃ₗᵢ[ℝ] F) (u : F → ℝ) : quadraticEstimateSet (u ∘ ⇑e) = ⇑e ⁻¹' quadraticEstimateSet u

Set-level transport of ambient quadratic estimate data through a linear isometry equivalence.

theorem AleksandrovDifferentiability.quadraticQuotientEstimateAt_comp_linearIsometryEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (e : E ≃ₗᵢ[ℝ] F) {u : F → ℝ} {x : E} : QuadraticQuotientEstimateAt (u ∘ ⇑e) x ↔ QuadraticQuotientEstimateAt u (e x)

Pointwise transport of punctured normalized ambient quadratic estimate data through a linear isometry equivalence.

theorem AleksandrovDifferentiability.quadraticQuotientEstimateSet_comp_linearIsometryEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (e : E ≃ₗᵢ[ℝ] F) (u : F → ℝ) : quadraticQuotientEstimateSet (u ∘ ⇑e) = ⇑e ⁻¹' quadraticQuotientEstimateSet u

Set-level transport of punctured normalized ambient quadratic estimate data through a linear isometry equivalence.

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

Ambient quadratic estimate data implies project second-order differentiability.

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

Ambient quadratic quotient-estimate data implies project second-order differentiability.

theorem AleksandrovDifferentiability.QuadraticEstimateAt.quadraticQuotientEstimateAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x : E} (h : QuadraticEstimateAt u x) : QuadraticQuotientEstimateAt u x

A local ambient quadratic estimate implies the punctured normalized quotient estimate.

theorem AleksandrovDifferentiability.quadraticEstimateSet_subset_secondOrderDifferentiabilitySet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} : quadraticEstimateSet u ⊆ secondOrderDifferentiabilitySet u

The ambient quadratic estimate set is contained in the second-order differentiability locus.

theorem AleksandrovDifferentiability.quadraticQuotientEstimateSet_subset_secondOrderDifferentiabilitySet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} : quadraticQuotientEstimateSet u ⊆ secondOrderDifferentiabilitySet u

The ambient quadratic quotient-estimate set is contained in the second-order differentiability locus.

theorem AleksandrovDifferentiability.quadraticEstimateSet_subset_quadraticQuotientEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} : quadraticEstimateSet u ⊆ quadraticQuotientEstimateSet u

The local ambient quadratic estimate set is contained in the quotient-estimate set.