Divergence #
In this module we define and create an API around the divergence of a map f : E → E
where E
is a normed space over a field 𝕜
.
noncomputable def
divergence
(𝕜 : Type u_1)
[RCLike 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
(f : E → E)
(x : E)
:
𝕜
The divergence of a map f : E → E
where E
is a normed space over 𝕜
.
Equations
- divergence 𝕜 f x = (LinearMap.trace 𝕜 E) ↑(fderiv 𝕜 f x)
Instances For
@[simp]
theorem
divergence_zero
{𝕜 : Type u_1}
[RCLike 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
:
theorem
divergence_eq_sum_fderiv
{𝕜 : Type u_1}
[RCLike 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{s : Finset E}
(b : Module.Basis { x : E // x ∈ s } 𝕜 E)
{f : E → E}
:
theorem
divergence_eq_sum_fderiv'
{𝕜 : Type u_1}
[RCLike 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{ι : Type u_4}
[Fintype ι]
(b : Module.Basis ι 𝕜 E)
{f : E → E}
:
theorem
divergence_prodMk
{𝕜 : Type u_1}
[RCLike 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[FiniteDimensional 𝕜 E]
[FiniteDimensional 𝕜 F]
{f : E × F → E}
{g : E × F → F}
{xy : E × F}
(hf : DifferentiableAt 𝕜 f xy)
(hg : DifferentiableAt 𝕜 g xy)
:
divergence 𝕜 (fun (xy : E × F) => (f xy, g xy)) xy = divergence 𝕜 (fun (x' : E) => f (x', xy.2)) xy.1 + divergence 𝕜 (fun (y' : F) => g (xy.1, y')) xy.2
theorem
divergence_add
{𝕜 : Type u_1}
[RCLike 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{f g : E → E}
{x : E}
(hf : DifferentiableAt 𝕜 f x)
(hg : DifferentiableAt 𝕜 g x)
:
theorem
divergence_neg
{𝕜 : Type u_1}
[RCLike 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{f : E → E}
{x : E}
:
theorem
divergence_sub
{𝕜 : Type u_1}
[RCLike 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{f g : E → E}
{x : E}
(hf : DifferentiableAt 𝕜 f x)
(hg : DifferentiableAt 𝕜 g x)
:
theorem
divergence_const_smul
{𝕜 : Type u_1}
[RCLike 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{f : E → E}
{x : E}
{c : 𝕜}
(hf : DifferentiableAt 𝕜 f x)
:
theorem
divergence_smul
{𝕜 : Type u_1}
[RCLike 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[InnerProductSpace' 𝕜 E]
{f : E → 𝕜}
{g : E → E}
{x : E}
(hf : DifferentiableAt 𝕜 f x)
(hg : DifferentiableAt 𝕜 g x)
[FiniteDimensional 𝕜 E]
:
divergence 𝕜 (fun (x : E) => f x • g x) x = f x * divergence 𝕜 g x + inner 𝕜 (adjFDeriv 𝕜 f x 1) (g x)