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

Directional quadratic operators

This file records small finite-dimensional-algebra helpers for rebuilding symmetric quadratic candidates from directional second-order coefficients. The analytic slicing argument will later produce scalar coefficients along selected directions; these definitions package the corresponding rank-one symmetric operators.

def AleksandrovDifferentiability.FiniteOrthonormalOn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] (s : Finset ι) (v : ι → E) : Prop

A finite list of directions is orthonormal on the selected index set. This lightweight finite-set predicate is convenient for the slicing reconstruction layer, where the directions are usually carried by a Finset rather than by a global basis object.

Equations

• AleksandrovDifferentiability.FiniteOrthonormalOn s v = ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → inner ℝ (v i) (v j) = if i = j then 1 else 0

def AleksandrovDifferentiability.FiniteSpanningOn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} (s : Finset ι) (v : ι → E) : Prop

A finite list of directions spans the ambient space on the selected index set.

Equations

• AleksandrovDifferentiability.FiniteSpanningOn s v = ∀ (z : E), z ∈ Submodule.span ℝ (v '' ↑s)

def AleksandrovDifferentiability.FiniteOrthonormalSpanningOn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] (s : Finset ι) (v : ι → E) : Prop

A finite orthonormal spanning family on the selected index set. This is the finite-frame condition expected for the eventual directional reconstruction step.

Equations

• AleksandrovDifferentiability.FiniteOrthonormalSpanningOn s v = (AleksandrovDifferentiability.FiniteOrthonormalOn s v ∧ AleksandrovDifferentiability.FiniteSpanningOn s v)

theorem AleksandrovDifferentiability.FiniteOrthonormalOn.of_orthonormal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → E} (hv : Orthonormal ℝ v) : FiniteOrthonormalOn s v

theorem AleksandrovDifferentiability.FiniteOrthonormalOn.mono {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] {s t : Finset ι} {v : ι → E} (hv : FiniteOrthonormalOn s v) (hts : t ⊆ s) : FiniteOrthonormalOn t v

theorem AleksandrovDifferentiability.FiniteOrthonormalOn.image_linearIsometryEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {ι : Type u_3} [DecidableEq ι] {s : Finset ι} {v : ι → E} (hv : FiniteOrthonormalOn s v) (e : E ≃ₗᵢ[ℝ] F) : FiniteOrthonormalOn s fun (i : ι) => e (v i)

Linear isometry equivalences preserve finite orthonormal families.

theorem AleksandrovDifferentiability.FiniteOrthonormalOn.univ_iff_orthonormal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {v : ι → E} : FiniteOrthonormalOn Finset.univ v ↔ Orthonormal ℝ v

theorem AleksandrovDifferentiability.FiniteOrthonormalOn.inner_eq_ite {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → E} (hv : FiniteOrthonormalOn s v) {i j : ι} (hi : i ∈ s) (hj : j ∈ s) : inner ℝ (v i) (v j) = if i = j then 1 else 0

theorem AleksandrovDifferentiability.FiniteOrthonormalOn.inner_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → E} (hv : FiniteOrthonormalOn s v) {i : ι} (hi : i ∈ s) : inner ℝ (v i) (v i) = 1

theorem AleksandrovDifferentiability.FiniteOrthonormalOn.norm_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → E} (hv : FiniteOrthonormalOn s v) {i : ι} (hi : i ∈ s) : ‖v i‖ ^ 2 = 1

Every member of a finite orthonormal family has squared norm one.

theorem AleksandrovDifferentiability.FiniteOrthonormalOn.inner_ne {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → E} (hv : FiniteOrthonormalOn s v) {i j : ι} (hi : i ∈ s) (hj : j ∈ s) (hij : i ≠ j) : inner ℝ (v i) (v j) = 0

theorem AleksandrovDifferentiability.FiniteOrthonormalOn.inner_sum_inner_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → E} (hv : FiniteOrthonormalOn s v) {k : ι} (hk : k ∈ s) (z : E) : inner ℝ (v k) (∑ i ∈ s, inner ℝ (v i) z • v i) = inner ℝ (v k) z

The coordinate projection onto a finite orthonormal family has the expected coordinate in each selected direction.

theorem AleksandrovDifferentiability.FiniteSpanningOn.univ_of_basis {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [Fintype ι] (b : Module.Basis ι ℝ E) : FiniteSpanningOn Finset.univ ⇑b

theorem AleksandrovDifferentiability.FiniteSpanningOn.univ_of_orthonormalBasis {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [Fintype ι] (b : OrthonormalBasis ι ℝ E) : FiniteSpanningOn Finset.univ ⇑b

theorem AleksandrovDifferentiability.FiniteSpanningOn.image_linearIsometryEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {ι : Type u_3} {s : Finset ι} {v : ι → E} (hv : FiniteSpanningOn s v) (e : E ≃ₗᵢ[ℝ] F) : FiniteSpanningOn s fun (i : ι) => e (v i)

Linear isometry equivalences preserve finite spanning families.

theorem AleksandrovDifferentiability.FiniteOrthonormalSpanningOn.univ_of_orthonormalBasis {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (b : OrthonormalBasis ι ℝ E) : FiniteOrthonormalSpanningOn Finset.univ ⇑b

theorem AleksandrovDifferentiability.FiniteOrthonormalSpanningOn.image_linearIsometryEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {ι : Type u_3} [DecidableEq ι] {s : Finset ι} {v : ι → E} (hv : FiniteOrthonormalSpanningOn s v) (e : E ≃ₗᵢ[ℝ] F) : FiniteOrthonormalSpanningOn s fun (i : ι) => e (v i)

Linear isometry equivalences preserve finite orthonormal spanning families.

theorem AleksandrovDifferentiability.FiniteOrthonormalSpanningOn.univ_of_stdOrthonormalBasis (E : Type u_2) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] : FiniteOrthonormalSpanningOn Finset.univ ⇑(stdOrthonormalBasis ℝ E)

Mathlib's standard orthonormal basis is a finite orthonormal spanning family.

theorem AleksandrovDifferentiability.FiniteOrthonormalSpanningOn.sum_inner_smul_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → E} (hv : FiniteOrthonormalSpanningOn s v) (z : E) : ∑ i ∈ s, inner ℝ (v i) z • v i = z

Coordinate reconstruction in a finite orthonormal spanning family.

theorem AleksandrovDifferentiability.FiniteOrthonormalSpanningOn.exists_ne_zero_of_nonzero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → E} (hv : FiniteOrthonormalSpanningOn s v) {z : E} (hz : z ≠ 0) : ∃ i ∈ s, v i ≠ 0

A finite orthonormal spanning family contains a nonzero selected vector whenever the ambient space contains a nonzero vector.

theorem AleksandrovDifferentiability.FiniteOrthonormalSpanningOn.sum_inner_sq_eq_norm_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → E} (hv : FiniteOrthonormalSpanningOn s v) (z : E) : ∑ i ∈ s, inner ℝ (v i) z ^ 2 = ‖z‖ ^ 2

Pythagorean identity for coordinates in a finite orthonormal spanning family.

theorem AleksandrovDifferentiability.FiniteOrthonormalSpanningOn.inner_sq_le_norm_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → E} (hv : FiniteOrthonormalSpanningOn s v) {i : ι} (hi : i ∈ s) (z : E) : inner ℝ (v i) z ^ 2 ≤ ‖z‖ ^ 2

Each coordinate square is bounded by the squared norm in a finite orthonormal spanning family.

theorem AleksandrovDifferentiability.FiniteOrthonormalSpanningOn.abs_inner_le_norm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → E} (hv : FiniteOrthonormalSpanningOn s v) {i : ι} (hi : i ∈ s) (z : E) : |inner ℝ (v i) z| ≤ ‖z‖

Absolute-value form of the coordinate bound in a finite orthonormal spanning family.

theorem AleksandrovDifferentiability.FiniteOrthonormalSpanningOn.abs_inner_mul_inner_le_norm_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → E} (hv : FiniteOrthonormalSpanningOn s v) {i j : ι} (hi : i ∈ s) (hj : j ∈ s) (z : E) : |inner ℝ (v i) z * inner ℝ (v j) z| ≤ ‖z‖ ^ 2

Products of two frame coordinates are bounded by the squared norm.

theorem AleksandrovDifferentiability.FiniteOrthonormalSpanningOn.sum_const_mul_inner_sq_eq_mul_norm_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → E} (hv : FiniteOrthonormalSpanningOn s v) (c : ℝ) (z : E) : ∑ i ∈ s, c * inner ℝ (v i) z ^ 2 = c * ‖z‖ ^ 2

Uniformly weighted coordinate-square sum in a finite orthonormal spanning family.

theorem AleksandrovDifferentiability.FiniteOrthonormalSpanningOn.eq_zero_of_quadraticForm_eq_zero_on_frame_and_add {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → E} (hv : FiniteOrthonormalSpanningOn s v) {B : E →L[ℝ] E} (hB : IsSymmetricOperator B) (hpure : ∀ ⦃i : ι⦄, i ∈ s → inner ℝ (v i) (B (v i)) = 0) (hpair : ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → inner ℝ (v i + v j) (B (v i + v j)) = 0) : B = 0

If a symmetric operator has zero quadratic form on each frame direction and on each pairwise sum of frame directions, then the operator is zero. This is the algebraic uniqueness input for recovering a Hessian candidate from pure and pairwise-sum directional coefficients.

theorem AleksandrovDifferentiability.FiniteOrthonormalSpanningOn.ext_of_quadraticForm_eq_on_frame_and_add {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → E} (hv : FiniteOrthonormalSpanningOn s v) {B C : E →L[ℝ] E} (hB : IsSymmetricOperator B) (hC : IsSymmetricOperator C) (hpure : ∀ ⦃i : ι⦄, i ∈ s → inner ℝ (v i) (B (v i)) = inner ℝ (v i) (C (v i))) (hpair : ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → inner ℝ (v i + v j) (B (v i + v j)) = inner ℝ (v i + v j) (C (v i + v j))) : B = C

Two symmetric operators are equal if their quadratic forms agree on each frame direction and on each pairwise sum of frame directions.

theorem AleksandrovDifferentiability.FiniteOrthonormalSpanningOn.eq_zero_of_quadraticForm_eq_zero_on_frame_and_add_offDiagonal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → E} (hv : FiniteOrthonormalSpanningOn s v) {B : E →L[ℝ] E} (hB : IsSymmetricOperator B) (hpure : ∀ ⦃i : ι⦄, i ∈ s → inner ℝ (v i) (B (v i)) = 0) (hpair : ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → i ≠ j → inner ℝ (v i + v j) (B (v i + v j)) = 0) : B = 0

Off-diagonal version of FiniteOrthonormalSpanningOn.eq_zero_of_quadraticForm_eq_zero_on_frame_and_add. The diagonal pairwise-sum directions carry no additional information beyond the pure directions.

theorem AleksandrovDifferentiability.FiniteOrthonormalSpanningOn.ext_of_quadraticForm_eq_on_frame_and_add_offDiagonal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → E} (hv : FiniteOrthonormalSpanningOn s v) {B C : E →L[ℝ] E} (hB : IsSymmetricOperator B) (hC : IsSymmetricOperator C) (hpure : ∀ ⦃i : ι⦄, i ∈ s → inner ℝ (v i) (B (v i)) = inner ℝ (v i) (C (v i))) (hpair : ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → i ≠ j → inner ℝ (v i + v j) (B (v i + v j)) = inner ℝ (v i + v j) (C (v i + v j))) : B = C

Off-diagonal version of FiniteOrthonormalSpanningOn.ext_of_quadraticForm_eq_on_frame_and_add.