PhysLean Documentation

PhysLean.Mathematics.Calculus.Divergence

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 : EE) (x : E) :
𝕜

The divergence of a map f : E → E where E is a normed space over 𝕜.

Equations
Instances For
    @[simp]
    theorem divergence_zero {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] :
    (divergence 𝕜 fun (x : E) => 0) = fun (x : E) => 0
    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 : EE} :
    divergence 𝕜 f = fun (x : E) => i : { x : E // x s }, (b.repr ((fderiv 𝕜 f x) (b i))) i
    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 : EE} :
    divergence 𝕜 f = fun (x : E) => i : ι, (b.repr ((fderiv 𝕜 f x) (b i))) i
    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 × FE} {g : E × FF} {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 : EE} {x : E} (hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x) :
    divergence 𝕜 (fun (x : E) => f x + g x) x = divergence 𝕜 f x + divergence 𝕜 g x
    theorem divergence_neg {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : EE} {x : E} :
    divergence 𝕜 (fun (x : E) => -f x) x = -divergence 𝕜 f x
    theorem divergence_sub {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f g : EE} {x : E} (hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x) :
    divergence 𝕜 (fun (x : E) => f x - g x) x = divergence 𝕜 f x - divergence 𝕜 g x
    theorem divergence_const_smul {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : EE} {x : E} {c : 𝕜} (hf : DifferentiableAt 𝕜 f x) :
    divergence 𝕜 (fun (x : E) => c f x) x = c * divergence 𝕜 f x
    theorem divergence_smul {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] {f : E𝕜} {g : EE} {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)