noncomputable def VectorCalculus.ckNorm (k : ℕ) (Ω : Set ℝ) (f : ℝ → ℝ) : ℝ

The $C^k$ norm on $\Omega \subset \mathbb{R}$ (Definition 7.1.1): $\|f\|_{C^k(\Omega)} = \sum_{a=0}^{k} \sup_{x \in \Omega} |f^{(a)}(x)|$.

noncomputable def VectorCalculus.lpNorm {n : ℕ} (p : ℝ) (Ω : Set (Fin n → ℝ)) (f : (Fin n → ℝ) → ℝ) (μ : MeasureTheory.Measure (Fin n → ℝ) := by volume_tac) : ℝ

The $L^p$ norm of $f$ on $\Omega \subset \mathbb{R}^n$ (Definition 7.1.2): $\|f\|_{L^p(\Omega)} = \left(\int_\Omega |f(x)|^p\, d^n x\right)^{1/p}$.

def VectorCalculus.VectorField (n : ℕ) : Type

A vector field on $\mathbb{R}^n$ (Definition 7.2.1): an $\mathbb{R}^n$-valued function $\mathbf{F} : \mathbb{R}^n \to \mathbb{R}^n$.

noncomputable def VectorCalculus.divergence {n : ℕ} (F : (Fin n → ℝ) → Fin n → ℝ) (x : Fin n → ℝ) : ℝ

The divergence of a vector field $\mathbf{F}$ on $\mathbb{R}^n$ (Definition 7.2.2): $\nabla \cdot \mathbf{F}(x) = \sum_{i=1}^n \partial_i F^i(x)$.

opaque VectorCalculus.outwardUnitNormal {n : ℕ} (Ω : Set (Fin n → ℝ)) (σ : Fin n → ℝ) : Fin n → ℝ

The (opaque) outward unit normal vector $\hat{\mathbf{N}}(\sigma)$ to the boundary $\partial \Omega$ at a point $\sigma$, used in the statement of the divergence theorem.

opaque VectorCalculus.surfaceMeasure {n : ℕ} (Ω : Set (Fin n → ℝ)) : MeasureTheory.Measure (Fin n → ℝ)

The (opaque) surface measure $d\sigma$ on the boundary of $\Omega$, used in the statement of the divergence theorem.

noncomputable def VectorCalculus.boundaryFluxIntegral {n : ℕ} (Ω : Set (Fin n → ℝ)) (F : (Fin n → ℝ) → Fin n → ℝ) : ℝ

The boundary flux integral $\int_{\partial \Omega} \mathbf{F}(\sigma) \cdot \hat{\mathbf{N}}(\sigma)\, d\sigma$ appearing on the right-hand side of the divergence theorem.

theorem VectorCalculus.divergence_theorem {n : ℕ} (Ω : Set (Fin n → ℝ)) (F : (Fin n → ℝ) → Fin n → ℝ) (hΩ : IsOpen Ω) (hΩc : IsConnected Ω) (hF : ContDiff ℝ 1 F) : ∫ (x : Fin n → ℝ) in Ω, divergence F x = boundaryFluxIntegral Ω F

Divergence theorem (Theorem 7.1): for a sufficiently regular domain $\Omega$ and a $C^1$ vector field $\mathbf{F}$, $\int_\Omega \nabla \cdot \mathbf{F}\, d^n x = \int_{\partial \Omega} \mathbf{F}(\sigma) \cdot \hat{\mathbf{N}}(\sigma)\, d\sigma$.