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

Directional quadratic operators

Rank-one and mixed directional quadratic operators, together with finite sums.

theorem AleksandrovDifferentiability.isSymmetricOperator_sum {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {s : Finset ι} {B : ι → E →L[ℝ] E} (hB : ∀ i ∈ s, IsSymmetricOperator (B i)) : IsSymmetricOperator (∑ i ∈ s, B i)

Symmetric operators are closed under finite sums.

noncomputable def AleksandrovDifferentiability.directionalQuadraticOperator {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (v : E) : E →L[ℝ] E

The symmetric rank-one operator associated to a direction v, namely z ↦ inner ℝ v z • v.

Equations

• AleksandrovDifferentiability.directionalQuadraticOperator v = ((InnerProductSpace.rankOne ℝ) v) v

@[simp]

theorem AleksandrovDifferentiability.directionalQuadraticOperator_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (v z : E) : (directionalQuadraticOperator v) z = inner ℝ v z • v

theorem AleksandrovDifferentiability.isSymmetricOperator_directionalQuadraticOperator {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (v : E) : IsSymmetricOperator (directionalQuadraticOperator v)

The directional rank-one operator is symmetric.

theorem AleksandrovDifferentiability.inner_directionalQuadraticOperator_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (v z : E) : inner ℝ z ((directionalQuadraticOperator v) z) = inner ℝ v z ^ 2

The quadratic form associated to a directional rank-one operator is the square of the directional coordinate.

noncomputable def AleksandrovDifferentiability.mixedDirectionalQuadraticOperator {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (v w : E) : E →L[ℝ] E

The symmetric mixed rank-two operator associated to directions v and w. Its quadratic form is the product of the two directional coordinates.

Equations

• AleksandrovDifferentiability.mixedDirectionalQuadraticOperator v w = (1 / 2) • (((InnerProductSpace.rankOne ℝ) v) w + ((InnerProductSpace.rankOne ℝ) w) v)

@[simp]

theorem AleksandrovDifferentiability.mixedDirectionalQuadraticOperator_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (v w z : E) : (mixedDirectionalQuadraticOperator v w) z = (1 / 2) • (inner ℝ w z • v + inner ℝ v z • w)

theorem AleksandrovDifferentiability.isSymmetricOperator_mixedDirectionalQuadraticOperator {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (v w : E) : IsSymmetricOperator (mixedDirectionalQuadraticOperator v w)

The mixed directional operator is symmetric.

theorem AleksandrovDifferentiability.mixedDirectionalQuadraticOperator_comm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (v w : E) : mixedDirectionalQuadraticOperator v w = mixedDirectionalQuadraticOperator w v

The mixed directional operator is symmetric in its two direction arguments.

theorem AleksandrovDifferentiability.inner_mixedDirectionalQuadraticOperator_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (v w z : E) : inner ℝ z ((mixedDirectionalQuadraticOperator v w) z) = inner ℝ v z * inner ℝ w z

The quadratic form of the mixed directional operator is the product of the corresponding directional coordinates.

theorem AleksandrovDifferentiability.inner_mixedDirectionalQuadraticOperator_self_eq_half_sub {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (v w z : E) : inner ℝ z ((mixedDirectionalQuadraticOperator v w) z) = 1 / 2 * (inner ℝ z ((directionalQuadraticOperator (v + w)) z) - inner ℝ z ((directionalQuadraticOperator v) z) - inner ℝ z ((directionalQuadraticOperator w) z))

Quadratic-form polarization for the mixed directional operator.

theorem AleksandrovDifferentiability.mixedDirectionalQuadraticOperator_eq_half_sub {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (v w : E) : mixedDirectionalQuadraticOperator v w = (1 / 2) • (directionalQuadraticOperator (v + w) - directionalQuadraticOperator v - directionalQuadraticOperator w)

Operator-level polarization for the mixed directional operator.

theorem AleksandrovDifferentiability.mixedDirectionalQuadraticOperator_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (v : E) : mixedDirectionalQuadraticOperator v v = directionalQuadraticOperator v

The mixed operator with the same direction twice is the pure directional rank-one operator.

noncomputable def AleksandrovDifferentiability.directionalQuadraticSum {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} (s : Finset ι) (v : ι → E) (q : ι → ℝ) : E →L[ℝ] E

A finite weighted sum of directional rank-one operators.

Equations

• AleksandrovDifferentiability.directionalQuadraticSum s v q = ∑ i ∈ s, q i • AleksandrovDifferentiability.directionalQuadraticOperator (v i)

theorem AleksandrovDifferentiability.isSymmetricOperator_directionalQuadraticSum {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} (s : Finset ι) (v : ι → E) (q : ι → ℝ) : IsSymmetricOperator (directionalQuadraticSum s v q)

Finite weighted sums of directional rank-one operators are symmetric.

theorem AleksandrovDifferentiability.inner_directionalQuadraticSum_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} (s : Finset ι) (v : ι → E) (q : ι → ℝ) (z : E) : inner ℝ z ((directionalQuadraticSum s v q) z) = ∑ i ∈ s, q i * inner ℝ (v i) z ^ 2

The quadratic form of a finite weighted directional sum is the corresponding weighted sum of squared directional coordinates.

noncomputable def AleksandrovDifferentiability.mixedDirectionalQuadraticSum {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} (s : Finset ι) (v : ι → E) (a : ι → ι → ℝ) : E →L[ℝ] E

A finite matrix of mixed directional quadratic operators. The coefficient a i j multiplies the operator with quadratic form inner ℝ (v i) z * inner ℝ (v j) z.

Equations

• AleksandrovDifferentiability.mixedDirectionalQuadraticSum s v a = ∑ i ∈ s, ∑ j ∈ s, a i j • AleksandrovDifferentiability.mixedDirectionalQuadraticOperator (v i) (v j)

@[simp]

theorem AleksandrovDifferentiability.mixedDirectionalQuadraticSum_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} (s : Finset ι) (v : ι → E) : (mixedDirectionalQuadraticSum s v fun (x x_1 : ι) => 0) = 0

The mixed-directional sum is zero for the zero coefficient matrix.

theorem AleksandrovDifferentiability.mixedDirectionalQuadraticSum_add {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} (s : Finset ι) (v : ι → E) (a b : ι → ι → ℝ) : (mixedDirectionalQuadraticSum s v fun (i j : ι) => a i j + b i j) = mixedDirectionalQuadraticSum s v a + mixedDirectionalQuadraticSum s v b

The mixed-directional sum is additive in the coefficient matrix.

theorem AleksandrovDifferentiability.mixedDirectionalQuadraticSum_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} (s : Finset ι) (v : ι → E) (c : ℝ) (a : ι → ι → ℝ) : (mixedDirectionalQuadraticSum s v fun (i j : ι) => c * a i j) = c • mixedDirectionalQuadraticSum s v a

The mixed-directional sum is homogeneous in the coefficient matrix.

theorem AleksandrovDifferentiability.isSymmetricOperator_mixedDirectionalQuadraticSum {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} (s : Finset ι) (v : ι → E) (a : ι → ι → ℝ) : IsSymmetricOperator (mixedDirectionalQuadraticSum s v a)

Finite coefficient matrices of mixed directional quadratic operators are symmetric.

theorem AleksandrovDifferentiability.inner_mixedDirectionalQuadraticSum_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} (s : Finset ι) (v : ι → E) (a : ι → ι → ℝ) (z : E) : inner ℝ z ((mixedDirectionalQuadraticSum s v a) z) = ∑ i ∈ s, ∑ j ∈ s, a i j * inner ℝ (v i) z * inner ℝ (v j) z

The quadratic form of a finite mixed directional sum is the corresponding coefficient matrix expression in the directional coordinates.

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

A finite mixed-directional quadratic form is bounded by the sum of the absolute coefficient values times ‖z‖ ^ 2 on a finite orthonormal spanning family.

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

Constant-bound form of abs_inner_mixedDirectionalQuadraticSum_self_le.

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

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

theorem AleksandrovDifferentiability.mixedDirectionalQuadraticSum_transpose {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} (s : Finset ι) (v : ι → E) (a : ι → ι → ℝ) : (mixedDirectionalQuadraticSum s v fun (i j : ι) => a j i) = mixedDirectionalQuadraticSum s v a

Transposing the finite mixed-directional coefficient matrix does not change the resulting operator.

theorem AleksandrovDifferentiability.mixedDirectionalQuadraticSum_symmetrized {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} (s : Finset ι) (v : ι → E) (a : ι → ι → ℝ) : (mixedDirectionalQuadraticSum s v fun (i j : ι) => 1 / 2 * (a i j + a j i)) = mixedDirectionalQuadraticSum s v a

Replacing a coefficient matrix by its symmetric part does not change the assembled mixed-directional quadratic operator.

theorem AleksandrovDifferentiability.mixedDirectionalQuadraticSum_diagonal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] (s : Finset ι) (v : ι → E) (q : ι → ℝ) : (mixedDirectionalQuadraticSum s v fun (i j : ι) => if i = j then q i else 0) = directionalQuadraticSum s v q

A diagonal mixed-directional coefficient matrix gives the corresponding pure directional quadratic sum.

noncomputable def AleksandrovDifferentiability.polarizedMixedCoefficient {ι : Type u_2} [DecidableEq ι] (q : ι → ℝ) (r : ι → ι → ℝ) : ι → ι → ℝ

The coefficient matrix recovered from pure directional quadratic coefficients q i and pairwise-sum coefficients r i j by the usual polarization formula. The diagonal is kept equal to the pure coefficient, and off-diagonal entries use (r i j - q i - q j) / 2.

Equations

• AleksandrovDifferentiability.polarizedMixedCoefficient q r i j = if i = j then q i else (r i j - q i - q j) / 2

@[simp]

theorem AleksandrovDifferentiability.polarizedMixedCoefficient_self {ι : Type u_2} [DecidableEq ι] (q : ι → ℝ) (r : ι → ι → ℝ) (i : ι) : polarizedMixedCoefficient q r i i = q i

theorem AleksandrovDifferentiability.polarizedMixedCoefficient_of_ne {ι : Type u_2} [DecidableEq ι] (q : ι → ℝ) (r : ι → ι → ℝ) {i j : ι} (hij : i ≠ j) : polarizedMixedCoefficient q r i j = (r i j - q i - q j) / 2

theorem AleksandrovDifferentiability.polarizedMixedCoefficient_symm_on {ι : Type u_2} [DecidableEq ι] {s : Finset ι} (q : ι → ℝ) (r : ι → ι → ℝ) (hr : ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → r j i = r i j) {i j : ι} (hi : i ∈ s) (hj : j ∈ s) : polarizedMixedCoefficient q r j i = polarizedMixedCoefficient q r i j

The polarized mixed coefficient matrix is symmetric on a finite set when the supplied pairwise-sum coefficients are symmetric there.

noncomputable def AleksandrovDifferentiability.polarizedMixedQuadraticSum {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] (s : Finset ι) (v : ι → E) (q : ι → ℝ) (r : ι → ι → ℝ) : E →L[ℝ] E

The mixed-directional quadratic operator assembled from pure coefficients q i and pairwise-sum coefficients r i j by polarization.

Equations

• AleksandrovDifferentiability.polarizedMixedQuadraticSum s v q r = AleksandrovDifferentiability.mixedDirectionalQuadraticSum s v (AleksandrovDifferentiability.polarizedMixedCoefficient q r)

@[simp]

theorem AleksandrovDifferentiability.polarizedMixedQuadraticSum_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] (s : Finset ι) (v : ι → E) (q : ι → ℝ) (r : ι → ι → ℝ) : polarizedMixedQuadraticSum s v q r = mixedDirectionalQuadraticSum s v (polarizedMixedCoefficient q r)

theorem AleksandrovDifferentiability.isSymmetricOperator_polarizedMixedQuadraticSum {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] (s : Finset ι) (v : ι → E) (q : ι → ℝ) (r : ι → ι → ℝ) : IsSymmetricOperator (polarizedMixedQuadraticSum s v q r)

The polarized mixed-directional quadratic operator is symmetric.

theorem AleksandrovDifferentiability.inner_polarizedMixedQuadraticSum_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] (s : Finset ι) (v : ι → E) (q : ι → ℝ) (r : ι → ι → ℝ) (z : E) : inner ℝ z ((polarizedMixedQuadraticSum s v q r) z) = ∑ i ∈ s, ∑ j ∈ s, polarizedMixedCoefficient q r i j * inner ℝ (v i) z * inner ℝ (v j) z

Quadratic form of the polarized mixed-directional model.