Coordinate trace and divergence on the physical three-dimensional Euclidean space.

@[reducible, inline]

abbrev EulerSmoothLimit.Space : Type

The physical three-dimensional Euclidean space.

Equations

• EulerSmoothLimit.Space = EuclideanSpace ℝ (Fin 3)

noncomputable def EulerSmoothLimit.coordinateTrace : (Space →L[ℝ] Space) →L[ℝ] ℝ

The trace of a continuous linear map, written in the standard Euclidean coordinates.

Equations

• EulerSmoothLimit.coordinateTrace = ∑ i : Fin 3, EuclideanSpace.proj i ∘SL (ContinuousLinearMap.apply ℝ EulerSmoothLimit.Space) (EuclideanSpace.single i 1)

theorem EulerSmoothLimit.coordinateTrace_eq_linearTrace (A : Space →L[ℝ] Space) : coordinateTrace A = (LinearMap.trace ℝ Space) ↑A

The coordinate formula is exactly the basis-independent linear-algebraic trace.

noncomputable def EulerSmoothLimit.divergence (f : Space → Space) (x : Space) : ℝ

Classical divergence, defined canonically as the trace of the Fréchet derivative.

Equations

• EulerSmoothLimit.divergence f x = (LinearMap.trace ℝ EulerSmoothLimit.Space) ↑(fderiv ℝ f x)

theorem EulerSmoothLimit.divergence_eq_coordinate_sum (f : Space → Space) (x : Space) : divergence f x = ∑ i : Fin 3, ((fderiv ℝ f x) (EuclideanSpace.single i 1)).ofLp i

theorem EulerSmoothLimit.divergence_eq_trace (f : Space → Space) (x : Space) : divergence f x = (LinearMap.trace ℝ Space) ↑(fderiv ℝ f x)