Contracting an endomorphism of ℝⁿ with a matrix

For a real n × n matrix A, the contraction H ↦ ∑ᵢⱼ Aᵢⱼ ⟪H eᵢ, eⱼ⟫ of endomorphisms H of ℝⁿ is a continuous linear functional. Applied to the Hessian of a function u, it is the non-divergence-form operator ∑ᵢⱼ Aᵢⱼ ∂ᵢ∂ⱼu with constant coefficients A.

Main declarations

• Matrix.contraction: the contraction with A, as a continuous linear functional.
• Matrix.contraction_add, Matrix.contraction_sub, Matrix.contraction_smul: the contraction is linear in the matrix.
• Matrix.contraction_one: contraction with the identity matrix is the trace.
• Matrix.abs_contraction_le: if every entry of M is at most ε in absolute value, then the contraction of H with M is at most n² ε ‖H‖ in absolute value.
• Matrix.abs_sum_sum_mul_apply_single_single_le: the same bound for the contraction ∑ᵢⱼ Mᵢⱼ B eᵢ eⱼ of a continuous bilinear form B, such as a second derivative.
• Matrix.abs_sum_sum_mul_apply_single_le: the contraction ∑ᵢⱼ Aᵢⱼ (T eⱼ)ᵢ of an endomorphism T is at most (∑ᵢⱼ |Aᵢⱼ|) ‖T‖ in absolute value.

noncomputable def Matrix.contraction {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) : (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n)) →L[ℝ] ℝ

The contraction H ↦ ∑ᵢⱼ Aᵢⱼ ⟪H eᵢ, eⱼ⟫ of an endomorphism of ℝⁿ with a matrix A, as a continuous linear functional.

@[simp]

theorem Matrix.contraction_apply {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (H : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n)) : A.contraction H = ∑ i : Fin n, ∑ j : Fin n, A i j * inner ℝ (H (EuclideanSpace.single i 1)) (EuclideanSpace.single j 1)

Matrix.contraction A evaluates to ∑ᵢⱼ Aᵢⱼ ⟪H eᵢ, eⱼ⟫.

@[simp]

theorem Matrix.contraction_add {n : ℕ} (A B : Matrix (Fin n) (Fin n) ℝ) : (A + B).contraction = A.contraction + B.contraction

The contraction is additive in the matrix.

@[simp]

theorem Matrix.contraction_sub {n : ℕ} (A B : Matrix (Fin n) (Fin n) ℝ) : (A - B).contraction = A.contraction - B.contraction

The contraction commutes with subtraction of matrices.

@[simp]

theorem Matrix.contraction_smul {n : ℕ} (c : ℝ) (A : Matrix (Fin n) (Fin n) ℝ) : (c • A).contraction = c • A.contraction

The contraction is homogeneous in the matrix.

theorem Matrix.contraction_one {n : ℕ} : contraction 1 = TauCeti.traceCLM ℝ (EuclideanSpace ℝ (Fin n))

Contraction with the identity matrix is the trace.

theorem Matrix.abs_contraction_le {n : ℕ} {M : Matrix (Fin n) (Fin n) ℝ} {ε : ℝ} (hM : ∀ (i j : Fin n), |M i j| ≤ ε) (H : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n)) : |M.contraction H| ≤ ↑n ^ 2 * ε * ‖H‖

If every entry of M is at most ε in absolute value, then |∑ᵢⱼ Mᵢⱼ ⟪H eᵢ, eⱼ⟫| ≤ n² ε ‖H‖.

theorem Matrix.abs_sum_sum_mul_apply_single_single_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {M : Matrix ι ι ℝ} {ε : ℝ} (hM : ∀ (i j : ι), |M i j| ≤ ε) (B : EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι →L[ℝ] ℝ) : |∑ i : ι, ∑ j : ι, M i j * (B (EuclideanSpace.single i 1)) (EuclideanSpace.single j 1)| ≤ ↑(Fintype.card ι) ^ 2 * ε * ‖B‖

If every entry of M is at most ε in absolute value, then for a continuous bilinear form B on EuclideanSpace ℝ ι, |∑ᵢⱼ Mᵢⱼ B eᵢ eⱼ| ≤ (card ι)² ε ‖B‖. Applied to the second derivative of a function, this bounds the principal part ∑ᵢⱼ Mᵢⱼ ∂ᵢ∂ⱼh of a non-divergence-form operator by the operator norm of the Hessian.

theorem Matrix.abs_sum_sum_mul_apply_single_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] (A : Matrix ι ι ℝ) (T : EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) : |∑ i : ι, ∑ j : ι, A i j * (T (EuclideanSpace.single j 1)).ofLp i| ≤ (∑ i : ι, ∑ j : ι, |A i j|) * ‖T‖

For an endomorphism T of EuclideanSpace ℝ ι, the contraction ∑ᵢⱼ Aᵢⱼ (T eⱼ)ᵢ, such as the principal part ∑ᵢⱼ aⁱʲ ∂ᵢ∂ⱼu with T a Hessian operator, is at most (∑ᵢⱼ |Aᵢⱼ|) ‖T‖ in absolute value.