Physlib.SpaceAndTime.Space.Derivatives.MatrixDiv — Physlib

Imports

/-
Copyright (c) 2025 Florian Wiesner. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Florian Wiesner
-/
module

public import Physlib.SpaceAndTime.Space.Derivatives.Div

Matrix divergence on Space

i. Overview

In this module we define the matrix divergence operator on matrix-valued functions from Space d.

For a field T : Space d → Matrix (Fin d) (Fin d) ℝ, the matrix divergence is the vector field whose ith component is

∑ j, ∂[j] (fun x => T x i j) x.

ii. Key results

matrixDiv : The divergence of a matrix-valued function on Space d.

iii. Table of contents

A. The matrix divergence on functions

A.1. Basic equalities

A.2. The matrix divergence on the zero function

A.3. The matrix divergence on a constant function

A.4. The matrix divergence distributes over addition

A.5. The matrix divergence distributes over scalar multiplication

iv. References

@[expose] public section

A. The matrix divergence on functions

A.1. Basic equalities

@[simp]
lemma matrixDiv_apply (d : ℕ) (T : Space d → Matrix (Fin d) (Fin d) ℝ)
    (x : Space d) (i : Fin d) :
    matrixDiv d T x i = ∑ j, ∂[j] (fun x => T x i j) x := byd:ℕT:Space d → Matrix (Fin d) (Fin d) ℝx:Space di:Fin d⊢ (matrixDiv d T x).ofLp i = ∑ j, deriv j (fun x => T x i j) x
  simp [matrixDiv, div]All goals completed! 🐙

A.2. The matrix divergence on the zero function

@[simp]
lemma matrixDiv_zero (d : ℕ) :
    matrixDiv d (0 : Space d → Matrix (Fin d) (Fin d) ℝ) = 0 := byd:ℕ⊢ matrixDiv d 0 = 0
  ext x id:ℕx:Space di:Fin d⊢ (matrixDiv d 0 x).ofLp i = (0 x).ofLp i
  change (∑ j : Fin d, ∂[j] (fun _ : Space d => (0 : ℝ)) x) = 0d:ℕx:Space di:Fin d⊢ ∑ j, deriv j (fun x => 0) x = 0
  simpAll goals completed! 🐙

A.3. The matrix divergence on a constant function

@[simp]
lemma matrixDiv_const (d : ℕ) (T : Matrix (Fin d) (Fin d) ℝ) :
    matrixDiv d (fun _ : Space d => T) = 0 := byd:ℕT:Matrix (Fin d) (Fin d) ℝ⊢ (matrixDiv d fun x => T) = 0
  ext x id:ℕT:Matrix (Fin d) (Fin d) ℝx:Space di:Fin d⊢ (matrixDiv d (fun x => T) x).ofLp i = (0 x).ofLp i
  change (∑ j : Fin d, ∂[j] (fun _ : Space d => T i j) x) = 0d:ℕT:Matrix (Fin d) (Fin d) ℝx:Space di:Fin d⊢ ∑ j, deriv j (fun x => T i j) x = 0
  simpAll goals completed! 🐙

A.4. The matrix divergence distributes over addition



lemma matrixDiv_add (d : ℕ) (T1 T2 : Space d → Matrix (Fin d) (Fin d) ℝ)
    (hT1 : Differentiable ℝ T1) (hT2 : Differentiable ℝ T2) :
    matrixDiv d (T1 + T2) = matrixDiv d T1 + matrixDiv d T2 := byd:ℕT1:Space d → Matrix (Fin d) (Fin d) ℝT2:Space d → Matrix (Fin d) (Fin d) ℝhT1:Differentiable ℝ T1hT2:Differentiable ℝ T2⊢ matrixDiv d (T1 + T2) = matrixDiv d T1 + matrixDiv d T2
  ext x id:ℕT1:Space d → Matrix (Fin d) (Fin d) ℝT2:Space d → Matrix (Fin d) (Fin d) ℝhT1:Differentiable ℝ T1hT2:Differentiable ℝ T2x:Space di:Fin d⊢ (matrixDiv d (T1 + T2) x).ofLp i = ((matrixDiv d T1 + matrixDiv d T2) x).ofLp i
  change (∑ j, ∂[j] (fun x => (T1 x + T2 x) i j) x) =
    (∑ j, ∂[j] (fun x => T1 x i j) x) +
      ∑ j, ∂[j] (fun x => T2 x i j) xd:ℕT1:Space d → Matrix (Fin d) (Fin d) ℝT2:Space d → Matrix (Fin d) (Fin d) ℝhT1:Differentiable ℝ T1hT2:Differentiable ℝ T2x:Space di:Fin d⊢ ∑ j, deriv j (fun x => (T1 x + T2 x) i j) x = ∑ j, deriv j (fun x => T1 x i j) x + ∑ j, deriv j (fun x => T2 x i j) x
  rw [← Finset.sum_add_distribd:ℕT1:Space d → Matrix (Fin d) (Fin d) ℝT2:Space d → Matrix (Fin d) (Fin d) ℝhT1:Differentiable ℝ T1hT2:Differentiable ℝ T2x:Space di:Fin d⊢ ∑ j, deriv j (fun x => (T1 x + T2 x) i j) x =
  ∑ x_1, (deriv x_1 (fun x => T1 x i x_1) x + deriv x_1 (fun x => T2 x i x_1) x)d:ℕT1:Space d → Matrix (Fin d) (Fin d) ℝT2:Space d → Matrix (Fin d) (Fin d) ℝhT1:Differentiable ℝ T1hT2:Differentiable ℝ T2x:Space di:Fin d⊢ ∑ j, deriv j (fun x => (T1 x + T2 x) i j) x =
  ∑ x_1, (deriv x_1 (fun x => T1 x i x_1) x + deriv x_1 (fun x => T2 x i x_1) x)]d:ℕT1:Space d → Matrix (Fin d) (Fin d) ℝT2:Space d → Matrix (Fin d) (Fin d) ℝhT1:Differentiable ℝ T1hT2:Differentiable ℝ T2x:Space di:Fin d⊢ ∑ j, deriv j (fun x => (T1 x + T2 x) i j) x =
  ∑ x_1, (deriv x_1 (fun x => T1 x i x_1) x + deriv x_1 (fun x => T2 x i x_1) x)
  congre_fd:ℕT1:Space d → Matrix (Fin d) (Fin d) ℝT2:Space d → Matrix (Fin d) (Fin d) ℝhT1:Differentiable ℝ T1hT2:Differentiable ℝ T2x:Space di:Fin d⊢ (fun j => deriv j (fun x => (T1 x + T2 x) i j) x) = fun x_1 =>
  deriv x_1 (fun x => T1 x i x_1) x + deriv x_1 (fun x => T2 x i x_1) x
  funext je_fd:ℕT1:Space d → Matrix (Fin d) (Fin d) ℝT2:Space d → Matrix (Fin d) (Fin d) ℝhT1:Differentiable ℝ T1hT2:Differentiable ℝ T2x:Space di:Fin dj:Fin d⊢ deriv j (fun x => (T1 x + T2 x) i j) x = deriv j (fun x => T1 x i j) x + deriv j (fun x => T2 x i j) x
  change ∂[j] ((fun x => T1 x i j) + fun x => T2 x i j) x =
    ∂[j] (fun x => T1 x i j) x + ∂[j] (fun x => T2 x i j) xe_fd:ℕT1:Space d → Matrix (Fin d) (Fin d) ℝT2:Space d → Matrix (Fin d) (Fin d) ℝhT1:Differentiable ℝ T1hT2:Differentiable ℝ T2x:Space di:Fin dj:Fin d⊢ deriv j ((fun x => T1 x i j) + fun x => T2 x i j) x = deriv j (fun x => T1 x i j) x + deriv j (fun x => T2 x i j) x
  rw [deriv_adde_fd:ℕT1:Space d → Matrix (Fin d) (Fin d) ℝT2:Space d → Matrix (Fin d) (Fin d) ℝhT1:Differentiable ℝ T1hT2:Differentiable ℝ T2x:Space di:Fin dj:Fin d⊢ ((deriv j fun x => T1 x i j) + deriv j fun x => T2 x i j) x =
  deriv j (fun x => T1 x i j) x + deriv j (fun x => T2 x i j) xe_f.hf1d:ℕT1:Space d → Matrix (Fin d) (Fin d) ℝT2:Space d → Matrix (Fin d) (Fin d) ℝhT1:Differentiable ℝ T1hT2:Differentiable ℝ T2x:Space di:Fin dj:Fin d⊢ Differentiable ℝ fun x => T1 x i je_f.hf2d:ℕT1:Space d → Matrix (Fin d) (Fin d) ℝT2:Space d → Matrix (Fin d) (Fin d) ℝhT1:Differentiable ℝ T1hT2:Differentiable ℝ T2x:Space di:Fin dj:Fin d⊢ Differentiable ℝ fun x => T2 x i je_fd:ℕT1:Space d → Matrix (Fin d) (Fin d) ℝT2:Space d → Matrix (Fin d) (Fin d) ℝhT1:Differentiable ℝ T1hT2:Differentiable ℝ T2x:Space di:Fin dj:Fin d⊢ ((deriv j fun x => T1 x i j) + deriv j fun x => T2 x i j) x =
  deriv j (fun x => T1 x i j) x + deriv j (fun x => T2 x i j) xe_f.hf1d:ℕT1:Space d → Matrix (Fin d) (Fin d) ℝT2:Space d → Matrix (Fin d) (Fin d) ℝhT1:Differentiable ℝ T1hT2:Differentiable ℝ T2x:Space di:Fin dj:Fin d⊢ Differentiable ℝ fun x => T1 x i je_f.hf2d:ℕT1:Space d → Matrix (Fin d) (Fin d) ℝT2:Space d → Matrix (Fin d) (Fin d) ℝhT1:Differentiable ℝ T1hT2:Differentiable ℝ T2x:Space di:Fin dj:Fin d⊢ Differentiable ℝ fun x => T2 x i j]e_fd:ℕT1:Space d → Matrix (Fin d) (Fin d) ℝT2:Space d → Matrix (Fin d) (Fin d) ℝhT1:Differentiable ℝ T1hT2:Differentiable ℝ T2x:Space di:Fin dj:Fin d⊢ ((deriv j fun x => T1 x i j) + deriv j fun x => T2 x i j) x =
  deriv j (fun x => T1 x i j) x + deriv j (fun x => T2 x i j) xe_f.hf1d:ℕT1:Space d → Matrix (Fin d) (Fin d) ℝT2:Space d → Matrix (Fin d) (Fin d) ℝhT1:Differentiable ℝ T1hT2:Differentiable ℝ T2x:Space di:Fin dj:Fin d⊢ Differentiable ℝ fun x => T1 x i je_f.hf2d:ℕT1:Space d → Matrix (Fin d) (Fin d) ℝT2:Space d → Matrix (Fin d) (Fin d) ℝhT1:Differentiable ℝ T1hT2:Differentiable ℝ T2x:Space di:Fin dj:Fin d⊢ Differentiable ℝ fun x => T2 x i j
  ·e_fd:ℕT1:Space d → Matrix (Fin d) (Fin d) ℝT2:Space d → Matrix (Fin d) (Fin d) ℝhT1:Differentiable ℝ T1hT2:Differentiable ℝ T2x:Space di:Fin dj:Fin d⊢ ((deriv j fun x => T1 x i j) + deriv j fun x => T2 x i j) x =
  deriv j (fun x => T1 x i j) x + deriv j (fun x => T2 x i j) x rflAll goals completed! 🐙
  ·e_f.hf1d:ℕT1:Space d → Matrix (Fin d) (Fin d) ℝT2:Space d → Matrix (Fin d) (Fin d) ℝhT1:Differentiable ℝ T1hT2:Differentiable ℝ T2x:Space di:Fin dj:Fin d⊢ Differentiable ℝ fun x => T1 x i j exact differentiable_pi.mp (differentiable_pi.mp hT1 i) jAll goals completed! 🐙
  ·e_f.hf2d:ℕT1:Space d → Matrix (Fin d) (Fin d) ℝT2:Space d → Matrix (Fin d) (Fin d) ℝhT1:Differentiable ℝ T1hT2:Differentiable ℝ T2x:Space di:Fin dj:Fin d⊢ Differentiable ℝ fun x => T2 x i j exact differentiable_pi.mp (differentiable_pi.mp hT2 i) jAll goals completed! 🐙

A.5. The matrix divergence distributes over scalar multiplication



lemma matrixDiv_smul (d : ℕ) (T : Space d → Matrix (Fin d) (Fin d) ℝ) (k : ℝ)
    (hT : Differentiable ℝ T) :
    matrixDiv d (k • T) = k • matrixDiv d T := byd:ℕT:Space d → Matrix (Fin d) (Fin d) ℝk:ℝhT:Differentiable ℝ T⊢ matrixDiv d (k • T) = k • matrixDiv d T
  ext x id:ℕT:Space d → Matrix (Fin d) (Fin d) ℝk:ℝhT:Differentiable ℝ Tx:Space di:Fin d⊢ (matrixDiv d (k • T) x).ofLp i = ((k • matrixDiv d T) x).ofLp i
  change (∑ j, ∂[j] (fun x => (k • T x) i j) x) =
    k * ∑ j, ∂[j] (fun x => T x i j) xd:ℕT:Space d → Matrix (Fin d) (Fin d) ℝk:ℝhT:Differentiable ℝ Tx:Space di:Fin d⊢ ∑ j, deriv j (fun x => (k • T x) i j) x = k * ∑ j, deriv j (fun x => T x i j) x
  rw [Finset.mul_sumd:ℕT:Space d → Matrix (Fin d) (Fin d) ℝk:ℝhT:Differentiable ℝ Tx:Space di:Fin d⊢ ∑ j, deriv j (fun x => (k • T x) i j) x = ∑ i_1, k * deriv i_1 (fun x => T x i i_1) xd:ℕT:Space d → Matrix (Fin d) (Fin d) ℝk:ℝhT:Differentiable ℝ Tx:Space di:Fin d⊢ ∑ j, deriv j (fun x => (k • T x) i j) x = ∑ i_1, k * deriv i_1 (fun x => T x i i_1) x]d:ℕT:Space d → Matrix (Fin d) (Fin d) ℝk:ℝhT:Differentiable ℝ Tx:Space di:Fin d⊢ ∑ j, deriv j (fun x => (k • T x) i j) x = ∑ i_1, k * deriv i_1 (fun x => T x i i_1) x
  congre_fd:ℕT:Space d → Matrix (Fin d) (Fin d) ℝk:ℝhT:Differentiable ℝ Tx:Space di:Fin d⊢ (fun j => deriv j (fun x => (k • T x) i j) x) = fun i_1 => k * deriv i_1 (fun x => T x i i_1) x
  funext je_fd:ℕT:Space d → Matrix (Fin d) (Fin d) ℝk:ℝhT:Differentiable ℝ Tx:Space di:Fin dj:Fin d⊢ deriv j (fun x => (k • T x) i j) x = k * deriv j (fun x => T x i j) x
  change ∂[j] (k • fun x => T x i j) x = k • ∂[j] (fun x => T x i j) xe_fd:ℕT:Space d → Matrix (Fin d) (Fin d) ℝk:ℝhT:Differentiable ℝ Tx:Space di:Fin dj:Fin d⊢ deriv j (k • fun x => T x i j) x = k • deriv j (fun x => T x i j) x
  rw [deriv_const_smule_fd:ℕT:Space d → Matrix (Fin d) (Fin d) ℝk:ℝhT:Differentiable ℝ Tx:Space di:Fin dj:Fin d⊢ (k • deriv j fun x => T x i j) x = k • deriv j (fun x => T x i j) xe_f.hd:ℕT:Space d → Matrix (Fin d) (Fin d) ℝk:ℝhT:Differentiable ℝ Tx:Space di:Fin dj:Fin d⊢ Differentiable ℝ fun x => T x i je_fd:ℕT:Space d → Matrix (Fin d) (Fin d) ℝk:ℝhT:Differentiable ℝ Tx:Space di:Fin dj:Fin d⊢ (k • deriv j fun x => T x i j) x = k • deriv j (fun x => T x i j) xe_f.hd:ℕT:Space d → Matrix (Fin d) (Fin d) ℝk:ℝhT:Differentiable ℝ Tx:Space di:Fin dj:Fin d⊢ Differentiable ℝ fun x => T x i j]e_fd:ℕT:Space d → Matrix (Fin d) (Fin d) ℝk:ℝhT:Differentiable ℝ Tx:Space di:Fin dj:Fin d⊢ (k • deriv j fun x => T x i j) x = k • deriv j (fun x => T x i j) xe_f.hd:ℕT:Space d → Matrix (Fin d) (Fin d) ℝk:ℝhT:Differentiable ℝ Tx:Space di:Fin dj:Fin d⊢ Differentiable ℝ fun x => T x i j
  ·e_fd:ℕT:Space d → Matrix (Fin d) (Fin d) ℝk:ℝhT:Differentiable ℝ Tx:Space di:Fin dj:Fin d⊢ (k • deriv j fun x => T x i j) x = k • deriv j (fun x => T x i j) x rflAll goals completed! 🐙
  ·e_f.hd:ℕT:Space d → Matrix (Fin d) (Fin d) ℝk:ℝhT:Differentiable ℝ Tx:Space di:Fin dj:Fin d⊢ Differentiable ℝ fun x => T x i j exact differentiable_pi.mp (differentiable_pi.mp hT i) jAll goals completed! 🐙