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

Polarized directional quadratic coefficients

Coordinate identities for recovering mixed quadratic models from finite directional data.

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

Mapping all directions and the increment through a linear isometry equivalence preserves the mixed quadratic form.

theorem AleksandrovDifferentiability.inner_polarizedMixedQuadraticSum_self_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) (q : ι → ℝ) (r : ι → ι → ℝ) (e : E ≃ₗᵢ[ℝ] F) (z : E) : inner ℝ (e z) ((polarizedMixedQuadraticSum s (fun (i : ι) => e (v i)) q r) (e z)) = inner ℝ z ((polarizedMixedQuadraticSum s v q r) z)

Mapping all directions and the increment through a linear isometry equivalence preserves the polarized mixed quadratic form.

theorem AleksandrovDifferentiability.abs_inner_polarizedMixedQuadraticSum_self_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_3} [DecidableEq ι] {s : Finset ι} {v : ι → E} (hv : FiniteOrthonormalSpanningOn s v) (q : ι → ℝ) (r : ι → ι → ℝ) (z : E) : |inner ℝ z ((polarizedMixedQuadraticSum s v q r) z)| ≤ (∑ i ∈ s, ∑ j ∈ s, |polarizedMixedCoefficient q r i j|) * ‖z‖ ^ 2

Bound for the polarized mixed-directional quadratic form in terms of the sum of absolute polarized coefficients.

theorem AleksandrovDifferentiability.exists_const_abs_inner_polarizedMixedQuadraticSum_self_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_3} [DecidableEq ι] {s : Finset ι} {v : ι → E} (hv : FiniteOrthonormalSpanningOn s v) (q : ι → ℝ) (r : ι → ι → ℝ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (z : E), |inner ℝ z ((polarizedMixedQuadraticSum s v q r) z)| ≤ C * ‖z‖ ^ 2

Constant-bound form of abs_inner_polarizedMixedQuadraticSum_self_le.

theorem AleksandrovDifferentiability.exists_const_norm_half_inner_polarizedMixedQuadraticSum_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_3} [DecidableEq ι] {s : Finset ι} {v : ι → E} (hv : FiniteOrthonormalSpanningOn s v) (q : ι → ℝ) (r : ι → ι → ℝ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (z : E), ‖1 / 2 * inner ℝ z ((polarizedMixedQuadraticSum s v q r) z)‖ ≤ C * ‖z‖ ^ 2

Constant-bound form for the polarized half-quadratic term used in second-order expansions.

theorem AleksandrovDifferentiability.inner_mixedDirectionalQuadraticSum_self_apply_of_finite_orthonormal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_3} [DecidableEq ι] {s : Finset ι} {v : ι → E} (a : ι → ι → ℝ) (hinner : ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → inner ℝ (v i) (v j) = if i = j then 1 else 0) {k : ι} (hk : k ∈ s) : inner ℝ (v k) ((mixedDirectionalQuadraticSum s v a) (v k)) = a k k

A finite orthonormal coordinate family collapses the quadratic form of a mixed-directional sum on one of its coordinate directions to the corresponding diagonal coefficient. The orthonormality hypothesis is written only on the finite set s, which is the form needed for finite slicing.

theorem AleksandrovDifferentiability.FiniteOrthonormalOn.inner_mixedDirectionalQuadraticSum_self_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_3} [DecidableEq ι] {s : Finset ι} {v : ι → E} (hv : FiniteOrthonormalOn s v) (a : ι → ι → ℝ) {k : ι} (hk : k ∈ s) : inner ℝ (v k) ((mixedDirectionalQuadraticSum s v a) (v k)) = a k k

Predicate-wrapper form of inner_mixedDirectionalQuadraticSum_self_apply_of_finite_orthonormal.

theorem AleksandrovDifferentiability.inner_mixedDirectionalQuadraticSum_polarized_self_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_3} [DecidableEq ι] {s : Finset ι} {v : ι → E} (q : ι → ℝ) (r : ι → ι → ℝ) (hinner : ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → inner ℝ (v i) (v j) = if i = j then 1 else 0) {k : ι} (hk : k ∈ s) : inner ℝ (v k) ((mixedDirectionalQuadraticSum s v (polarizedMixedCoefficient q r)) (v k)) = q k

The polarized coefficient matrix has the prescribed pure directional quadratic coefficient on each selected orthonormal direction.

theorem AleksandrovDifferentiability.inner_polarizedMixedQuadraticSum_self_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_3} [DecidableEq ι] {s : Finset ι} {v : ι → E} (q : ι → ℝ) (r : ι → ι → ℝ) (hinner : ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → inner ℝ (v i) (v j) = if i = j then 1 else 0) {k : ι} (hk : k ∈ s) : inner ℝ (v k) ((polarizedMixedQuadraticSum s v q r) (v k)) = q k

Named-model version of inner_mixedDirectionalQuadraticSum_polarized_self_apply.

theorem AleksandrovDifferentiability.FiniteOrthonormalOn.inner_mixedDirectionalQuadraticSum_polarized_self_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_3} [DecidableEq ι] {s : Finset ι} {v : ι → E} (hv : FiniteOrthonormalOn s v) (q : ι → ℝ) (r : ι → ι → ℝ) {k : ι} (hk : k ∈ s) : inner ℝ (v k) ((mixedDirectionalQuadraticSum s v (polarizedMixedCoefficient q r)) (v k)) = q k

Predicate-wrapper form of inner_mixedDirectionalQuadraticSum_polarized_self_apply.

theorem AleksandrovDifferentiability.FiniteOrthonormalOn.inner_polarizedMixedQuadraticSum_self_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_3} [DecidableEq ι] {s : Finset ι} {v : ι → E} (hv : FiniteOrthonormalOn s v) (q : ι → ℝ) (r : ι → ι → ℝ) {k : ι} (hk : k ∈ s) : inner ℝ (v k) ((polarizedMixedQuadraticSum s v q r) (v k)) = q k

Predicate-wrapper form of inner_polarizedMixedQuadraticSum_self_apply.

theorem AleksandrovDifferentiability.finset_sum_eq_add_of_eq_zero_off_two {ι : Type u_3} {α : Type u_4} [AddCommMonoid α] {s : Finset ι} {f : ι → α} {i j : ι} (hi : i ∈ s) (hj : j ∈ s) (hij : i ≠ j) (hzero : ∀ ⦃k : ι⦄, k ∈ s → k ≠ i → k ≠ j → f k = 0) : ∑ k ∈ s, f k = f i + f j

A finite sum whose support is contained in two selected points is the sum of the two selected values.

theorem AleksandrovDifferentiability.inner_add_pair_of_finite_orthonormal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_3} [DecidableEq ι] {s : Finset ι} {v : ι → E} (hinner : ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → inner ℝ (v i) (v j) = if i = j then 1 else 0) {i j k : ι} (hi : i ∈ s) (hj : j ∈ s) (hk : k ∈ s) (hij : i ≠ j) : inner ℝ (v k) (v i + v j) = if k = i then 1 else if k = j then 1 else 0

Coordinates of the sum of two selected orthonormal directions against a finite orthonormal family.

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

Predicate-wrapper form of inner_add_pair_of_finite_orthonormal.

theorem AleksandrovDifferentiability.inner_mixedDirectionalQuadraticSum_self_add_of_finite_orthonormal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_3} [DecidableEq ι] {s : Finset ι} {v : ι → E} (a : ι → ι → ℝ) (hinner : ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → inner ℝ (v i) (v j) = if i = j then 1 else 0) {i j : ι} (hi : i ∈ s) (hj : j ∈ s) (hij : i ≠ j) : inner ℝ (v i + v j) ((mixedDirectionalQuadraticSum s v a) (v i + v j)) = a i i + a i j + a j i + a j j

On the sum of two selected orthonormal directions, the quadratic form of a mixed-directional sum is the four-entry combination expected from polarization.

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

Predicate-wrapper form of inner_mixedDirectionalQuadraticSum_self_add_of_finite_orthonormal.

theorem AleksandrovDifferentiability.inner_mixedDirectionalQuadraticSum_polarized_self_add {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_3} [DecidableEq ι] {s : Finset ι} {v : ι → E} (q : ι → ℝ) (r : ι → ι → ℝ) (hinner : ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → inner ℝ (v i) (v j) = if i = j then 1 else 0) (hr : ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → r j i = r i j) {i j : ι} (hi : i ∈ s) (hj : j ∈ s) (hij : i ≠ j) : inner ℝ (v i + v j) ((mixedDirectionalQuadraticSum s v (polarizedMixedCoefficient q r)) (v i + v j)) = r i j

The polarized coefficient matrix has the prescribed pairwise-sum quadratic coefficient on selected orthonormal directions, provided the supplied pairwise coefficients are symmetric.

theorem AleksandrovDifferentiability.inner_polarizedMixedQuadraticSum_self_add {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_3} [DecidableEq ι] {s : Finset ι} {v : ι → E} (q : ι → ℝ) (r : ι → ι → ℝ) (hinner : ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → inner ℝ (v i) (v j) = if i = j then 1 else 0) (hr : ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → r j i = r i j) {i j : ι} (hi : i ∈ s) (hj : j ∈ s) (hij : i ≠ j) : inner ℝ (v i + v j) ((polarizedMixedQuadraticSum s v q r) (v i + v j)) = r i j

Named-model version of inner_mixedDirectionalQuadraticSum_polarized_self_add.

theorem AleksandrovDifferentiability.FiniteOrthonormalOn.inner_mixedDirectionalQuadraticSum_polarized_self_add {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_3} [DecidableEq ι] {s : Finset ι} {v : ι → E} (hv : FiniteOrthonormalOn s v) (q : ι → ℝ) (r : ι → ι → ℝ) (hr : ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → r j i = r i j) {i j : ι} (hi : i ∈ s) (hj : j ∈ s) (hij : i ≠ j) : inner ℝ (v i + v j) ((mixedDirectionalQuadraticSum s v (polarizedMixedCoefficient q r)) (v i + v j)) = r i j

Predicate-wrapper form of inner_mixedDirectionalQuadraticSum_polarized_self_add.

theorem AleksandrovDifferentiability.FiniteOrthonormalOn.inner_polarizedMixedQuadraticSum_self_add {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_3} [DecidableEq ι] {s : Finset ι} {v : ι → E} (hv : FiniteOrthonormalOn s v) (q : ι → ℝ) (r : ι → ι → ℝ) (hr : ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → r j i = r i j) {i j : ι} (hi : i ∈ s) (hj : j ∈ s) (hij : i ≠ j) : inner ℝ (v i + v j) ((polarizedMixedQuadraticSum s v q r) (v i + v j)) = r i j

Predicate-wrapper form of inner_polarizedMixedQuadraticSum_self_add.

theorem AleksandrovDifferentiability.FiniteOrthonormalSpanningOn.inner_mixedDirectionalQuadraticSum_polarized_self_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_3} [DecidableEq ι] {s : Finset ι} {v : ι → E} (hv : FiniteOrthonormalSpanningOn s v) (q : ι → ℝ) (r : ι → ι → ℝ) {k : ι} (hk : k ∈ s) : inner ℝ (v k) ((mixedDirectionalQuadraticSum s v (polarizedMixedCoefficient q r)) (v k)) = q k

Spanning-frame wrapper for the pure-direction polarized quadratic coefficient identity.

theorem AleksandrovDifferentiability.FiniteOrthonormalSpanningOn.inner_polarizedMixedQuadraticSum_self_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_3} [DecidableEq ι] {s : Finset ι} {v : ι → E} (hv : FiniteOrthonormalSpanningOn s v) (q : ι → ℝ) (r : ι → ι → ℝ) {k : ι} (hk : k ∈ s) : inner ℝ (v k) ((polarizedMixedQuadraticSum s v q r) (v k)) = q k

Spanning-frame wrapper for the pure-direction named polarized quadratic coefficient identity.

theorem AleksandrovDifferentiability.FiniteOrthonormalSpanningOn.inner_mixedDirectionalQuadraticSum_polarized_self_add {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_3} [DecidableEq ι] {s : Finset ι} {v : ι → E} (hv : FiniteOrthonormalSpanningOn s v) (q : ι → ℝ) (r : ι → ι → ℝ) (hr : ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → r j i = r i j) {i j : ι} (hi : i ∈ s) (hj : j ∈ s) (hij : i ≠ j) : inner ℝ (v i + v j) ((mixedDirectionalQuadraticSum s v (polarizedMixedCoefficient q r)) (v i + v j)) = r i j

Spanning-frame wrapper for the pairwise-sum polarized quadratic coefficient identity.

theorem AleksandrovDifferentiability.FiniteOrthonormalSpanningOn.inner_polarizedMixedQuadraticSum_self_add {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_3} [DecidableEq ι] {s : Finset ι} {v : ι → E} (hv : FiniteOrthonormalSpanningOn s v) (q : ι → ℝ) (r : ι → ι → ℝ) (hr : ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → r j i = r i j) {i j : ι} (hi : i ∈ s) (hj : j ∈ s) (hij : i ≠ j) : inner ℝ (v i + v j) ((polarizedMixedQuadraticSum s v q r) (v i + v j)) = r i j

Spanning-frame wrapper for the pairwise-sum named polarized quadratic coefficient identity.

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

A symmetric operator is the polarized mixed-directional model determined by its pure and off-diagonal pairwise-sum quadratic coefficients on a finite orthonormal spanning frame.