@[reducible, inline]

abbrev Eℝ (n : ℕ) : Type

Shorthand for $n$-dimensional Euclidean space $\mathbb{R}^n$ with its standard inner product.

def EuclideanΩ (n p : ℕ) : Type

The space $\Omega^p(\mathbb{R}^n)$ of (not-necessarily-smooth) differential $p$-forms on $\mathbb{R}^n$: pointwise alternating $\mathbb{R}$-multilinear maps $(\mathbb{R}^n)^p \to \mathbb{R}$.

def EuclideanVF (n : ℕ) : Type

The space of vector fields $\mathfrak{X}(\mathbb{R}^n)$ on Euclidean space: arbitrary maps $\mathbb{R}^n \to \mathbb{R}^n$.

@[implicit_reducible]

noncomputable instance EuclideanΩ.instAddCommGroup {n p : ℕ} : AddCommGroup (EuclideanΩ n p)

Pointwise abelian-group structure on $\Omega^p(\mathbb{R}^n)$.

@[implicit_reducible]

instance EuclideanΩ.instModule {n p : ℕ} : Module ℝ (EuclideanΩ n p)

Pointwise $\mathbb{R}$-module structure on $\Omega^p(\mathbb{R}^n)$.

theorem EuclideanΩ.ext {n p : ℕ} {α β : EuclideanΩ n p} (h : ∀ (x : Eℝ n), α x = β x) : α = β

Extensionality for Euclidean $p$-forms: two forms agreeing pointwise are equal.

theorem EuclideanΩ.ext_iff {n p : ℕ} {α β : EuclideanΩ n p} : α = β ↔ ∀ (x : Eℝ n), α x = β x

@[simp]

theorem EuclideanΩ.add_apply {n p : ℕ} (α β : EuclideanΩ n p) (x : Eℝ n) : (α + β) x = α x + β x

Pointwise evaluation of an addition of forms.

@[simp]

theorem EuclideanΩ.neg_apply' {n p : ℕ} (α : EuclideanΩ n p) (x : Eℝ n) : (-α) x = -α x

Pointwise evaluation of a negated form.

@[simp]

theorem EuclideanΩ.smul_apply' {n p : ℕ} (r : ℝ) (α : EuclideanΩ n p) (x : Eℝ n) : (r • α) x = r • α x

Pointwise evaluation of a scalar multiple.

@[simp]

theorem EuclideanΩ.zero_apply' {n p : ℕ} (x : Eℝ n) : 0 x = 0

Pointwise evaluation of the zero form.

@[reducible, inline]

abbrev EuclideanΩ.CEuclideanΩ (n p : ℕ) : Type

Continuous-fibre version of EuclideanΩ: pointwise continuous alternating multilinear maps. This is the regularity needed for the differential to be defined via fderiv.

noncomputable def EuclideanΩ.zeroFormScalar {n : ℕ} (α : EuclideanΩ n 0) : Eℝ n → ℝ

Identify a $0$-form $\alpha : \mathbb{R}^n \to \mathrm{Alt}^0(\mathbb{R}^n;\mathbb{R})$ with its underlying scalar function $x \mapsto \alpha(x)()$.

noncomputable def EuclideanΩ.euclideanD0 {n : ℕ} (α : EuclideanΩ n 0) : EuclideanΩ n 1

Exterior derivative of a $0$-form: $d f$ as the $1$-form whose value at $x$ is the linear map $v \mapsto Df(x)(v)$.

noncomputable def EuclideanΩ.fderivToAltMap {n p : ℕ} (α : CEuclideanΩ n p) (x : Eℝ n) : Eℝ n →ₗ[ℝ] Eℝ n [⋀^Fin p]→ₗ[ℝ] ℝ

Auxiliary helper: the Fréchet derivative $D\alpha(x)$ of a continuous-fibre $p$-form viewed as a linear map $\mathbb{R}^n \to \mathrm{Alt}^p(\mathbb{R}^n; \mathbb{R})$.

noncomputable def EuclideanΩ.fderivToMMap {n p : ℕ} (α : CEuclideanΩ n p) (x : Eℝ n) : Eℝ n →ₗ[ℝ] MultilinearMap ℝ (fun (x : Fin p) => Eℝ n) ℝ

Variant of fderivToAltMap landing in plain MultilinearMaps, used in the explicit uncurryMid construction of $d\alpha$.

noncomputable def EuclideanΩ.euclideanD_M0 {n p : ℕ} (α : CEuclideanΩ n p) (x : Eℝ n) : MultilinearMap ℝ (fun (x : Fin (p + 1)) => Eℝ n) ℝ

Intermediate non-alternated $(p+1)$-multilinear map obtained by uncurrying the derivative $D\alpha(x)$ in the first slot.

noncomputable def EuclideanΩ.euclideanD {n p : ℕ} (α : CEuclideanΩ n p) : EuclideanΩ n (p + 1)

Exterior derivative $d : \Omega^p \to \Omega^{p+1}$ on continuous-fibre forms, defined pointwise as the antisymmetrisation of the uncurried Fréchet derivative.

theorem EuclideanΩ.AlternatingMap.continuous_of_euclidean {n p : ℕ} (f : Eℝ n [⋀^Fin p]→ₗ[ℝ] ℝ) : Continuous ⇑f

Every alternating multilinear form $f : (\mathbb{R}^n)^p \to \mathbb{R}$ is automatically continuous, since on the finite-dimensional Euclidean space $\mathbb{R}^n$ it is a finite polynomial in the coordinates of its arguments.

def EuclideanΩ.toCAlt {n p : ℕ} (f : Eℝ n [⋀^Fin p]→ₗ[ℝ] ℝ) : Eℝ n [⋀^Fin p]→L[ℝ] ℝ

Lift an algebraic alternating map on $\mathbb{R}^n$ to its continuous counterpart, using the automatic continuity established above.

noncomputable def EuclideanΩ.fromCAlt {n p : ℕ} (g : Eℝ n [⋀^Fin p]→L[ℝ] ℝ) : Eℝ n [⋀^Fin p]→ₗ[ℝ] ℝ

Forget continuity of an alternating multilinear map.

@[simp]

theorem EuclideanΩ.fromCAlt_toCAlt {n p : ℕ} (f : Eℝ n [⋀^Fin p]→ₗ[ℝ] ℝ) : fromCAlt (toCAlt f) = f

Round-trip identity: forgetting continuity after adding it returns the original map.

@[simp]

theorem EuclideanΩ.toCAlt_fromCAlt {n p : ℕ} (g : Eℝ n [⋀^Fin p]→L[ℝ] ℝ) : toCAlt (fromCAlt g) = g

Round-trip identity: re-adding continuity after forgetting it recovers the original map.

@[simp]

theorem EuclideanΩ.toCAlt_apply {n p : ℕ} (f : Eℝ n [⋀^Fin p]→ₗ[ℝ] ℝ) (v : Fin p → Eℝ n) : (toCAlt f) v = f v

Evaluating the continuous lift of $f$ on a tuple gives the same value as evaluating $f$.

def EuclideanΩ.toCEuclideanΩ {n p : ℕ} (α : EuclideanΩ n p) : CEuclideanΩ n p

Pointwise lift of $\alpha \in \Omega^p(\mathbb{R}^n)$ to a continuous-fibre form.

theorem EuclideanΩ.contDiff_toCEuclideanΩ {n p : ℕ} (α : EuclideanΩ n p) : ContDiff ℝ ⊤ α.toCEuclideanΩ

The continuous-fibre lift of any Euclidean $p$-form is smooth ($C^\infty$).

theorem EuclideanΩ.differentiable_toCEuclideanΩ {n p : ℕ} (α : EuclideanΩ n p) : Differentiable ℝ α.toCEuclideanΩ

Corollary of smoothness: the continuous lift is in particular differentiable.

noncomputable def EuclideanΩ.CEuclideanΩ.toEuclideanΩ' {n p : ℕ} (α : CEuclideanΩ n p) : EuclideanΩ n p

Pointwise forgetful map from continuous-fibre forms back to algebraic ones.

theorem EuclideanΩ.EuclideanΩ_toCEuclideanΩ_toEuclideanΩ' {n p : ℕ} (α : CEuclideanΩ n p) : α.toEuclideanΩ'.toCEuclideanΩ = α

Round-trip: lifting back to continuous-fibre after forgetting gives the original form.

noncomputable def EuclideanΩ.euclideanD_lifted {n p : ℕ} (α : EuclideanΩ n p) : EuclideanΩ n (p + 1)

Exterior derivative on $\Omega^p(\mathbb{R}^n)$: lift $\alpha$ to a continuous-fibre form, take $d$ there, and forget continuity. This is the exterior derivative used by the Euclidean differential form space instance.

noncomputable def euclideanFMul {n p : ℕ} (f : EuclideanΩ n 0) (α : EuclideanΩ n p) : EuclideanΩ n p

Pointwise multiplication of a $p$-form by a $0$-form (scalar function): $(f \cdot \alpha)(x) = f(x) \cdot \alpha(x)$.

@[simp]

theorem euclideanFMul_apply {n p : ℕ} (f : EuclideanΩ n 0) (α : EuclideanΩ n p) (x : Eℝ n) : euclideanFMul f α x = (f x) Fin.elim0 • α x

Definitional pointwise formula for function-form multiplication.

noncomputable def dx_i {n : ℕ} (i : Fin n) : EuclideanΩ n 1

The constant coordinate $1$-form $dx_i$ on $\mathbb{R}^n$: at every point $x$ it sends $v \in \mathbb{R}^n$ to its $i$-th component $v_i$.

noncomputable def euclideanIota {n : ℕ} (X : EuclideanVF n) {p : ℕ} (α : EuclideanΩ n (p + 1)) : EuclideanΩ n p

Interior product (contraction) $\iota_X \alpha$ of a $(p+1)$-form with a vector field $X$: at each point $x$, it is the $p$-form $v \mapsto \alpha(x)(X(x), v_1, \ldots, v_p)$.

theorem euclideanIota_add {n : ℕ} (X : EuclideanVF n) {p : ℕ} (α β : EuclideanΩ n (p + 1)) : euclideanIota X (α + β) = euclideanIota X α + euclideanIota X β

Contraction is additive in the form argument: $\iota_X(\alpha + \beta) = \iota_X\alpha + \iota_X\beta$.

theorem euclideanIota_smul {n : ℕ} (X : EuclideanVF n) {p : ℕ} (r : ℝ) (α : EuclideanΩ n (p + 1)) : euclideanIota X (r • α) = r • euclideanIota X α

Contraction commutes with scalar multiplication: $\iota_X(r\,\alpha) = r\,\iota_X\alpha$.

noncomputable def oneFormLinear {n : ℕ} (ω_x : Eℝ n [⋀^Fin 1]→ₗ[ℝ] ℝ) : Eℝ n →ₗ[ℝ] ℝ

Identify a pointwise $1$-form with the underlying linear functional $\mathbb{R}^n \to \mathbb{R}$.

noncomputable def wedgePointwise {n p : ℕ} (ω_x : Eℝ n [⋀^Fin 1]→ₗ[ℝ] ℝ) (α_x : Eℝ n [⋀^Fin p]→ₗ[ℝ] ℝ) : Eℝ n [⋀^Fin (p + 1)]→ₗ[ℝ] ℝ

Pointwise wedge product $\omega \wedge \alpha$ where $\omega$ is a $1$-form and $\alpha$ is a $p$-form: antisymmetrise the tensor product $\omega \otimes \alpha$ via the uncurry-and-alternate construction.

noncomputable def euclideanWedge1 {n : ℕ} (ω : EuclideanΩ n 1) {p : ℕ} (α : EuclideanΩ n p) : EuclideanΩ n (p + 1)

Wedge product of a Euclidean $1$-form $\omega$ with a $p$-form $\alpha$, defined pointwise via wedgePointwise.

theorem euclideanWedge1_add_right {n : ℕ} (ω : EuclideanΩ n 1) {p : ℕ} (α β : EuclideanΩ n p) : euclideanWedge1 ω (α + β) = euclideanWedge1 ω α + euclideanWedge1 ω β

Wedge with a fixed $1$-form is additive on the right: $\omega \wedge (\alpha + \beta) = \omega \wedge \alpha + \omega \wedge \beta$.

theorem euclideanWedge1_smul_right {n : ℕ} (ω : EuclideanΩ n 1) {p : ℕ} (r : ℝ) (α : EuclideanΩ n p) : euclideanWedge1 ω (r • α) = r • euclideanWedge1 ω α

Wedge with a fixed $1$-form commutes with scalar multiplication on the right: $\omega \wedge (r\,\alpha) = r\,(\omega \wedge \alpha)$.

noncomputable def cFMul {n p : ℕ} (g : Eℝ n → ℝ) (α : EuclideanΩ.CEuclideanΩ n p) : EuclideanΩ.CEuclideanΩ n p

Pointwise scalar-function multiplication on continuous-fibre forms: $(g \cdot \alpha)(x) = g(x) \cdot \alpha(x)$.

noncomputable def CEuclideanΩ.toEΩ {n p : ℕ} (α : EuclideanΩ.CEuclideanΩ n p) : EuclideanΩ n p

Forget the continuity data of a continuous-fibre form to get an algebraic Euclidean form.

noncomputable def euclideanD_scalar {n : ℕ} (g : Eℝ n → ℝ) : EuclideanΩ n 1

Exterior derivative of a raw scalar function $g : \mathbb{R}^n \to \mathbb{R}$, returning the $1$-form $dg$ with $dg(x)(v) = Dg(x)(v)$.

noncomputable def euclideanIotaC {n : ℕ} (X : EuclideanVF n) {p : ℕ} (α : EuclideanΩ.CEuclideanΩ n (p + 1)) : EuclideanΩ.CEuclideanΩ n p

Interior product $\iota_X$ on continuous-fibre forms (the same construction as euclideanIota but preserving continuity of the fibres).

theorem euclideanIotaC_add {n : ℕ} (X : EuclideanVF n) {p : ℕ} (α β : EuclideanΩ.CEuclideanΩ n (p + 1)) : euclideanIotaC X (α + β) = euclideanIotaC X α + euclideanIotaC X β

Additivity of contraction on continuous-fibre forms.

theorem euclideanIotaC_smul {n : ℕ} (X : EuclideanVF n) {p : ℕ} (r : ℝ) (α : EuclideanΩ.CEuclideanΩ n (p + 1)) : euclideanIotaC X (r • α) = r • euclideanIotaC X α

Compatibility of contraction with scalar multiplication on continuous-fibre forms.

theorem EuclideanΩ.euclideanD_add {n p : ℕ} (α β : CEuclideanΩ n p) (hα : Differentiable ℝ α) (hβ : Differentiable ℝ β) : euclideanD (α + β) = euclideanD α + euclideanD β

Additivity of the exterior derivative on continuous-fibre forms (assuming differentiability): $d(\alpha + \beta) = d\alpha + d\beta$.

theorem EuclideanΩ.euclideanD_smul {n p : ℕ} (r : ℝ) (α : CEuclideanΩ n p) (hα : Differentiable ℝ α) : euclideanD (r • α) = r • euclideanD α

Scalar compatibility of the exterior derivative on continuous-fibre forms: $d(r\,\alpha) = r\,d\alpha$.

noncomputable def euclideanL {n : ℕ} (X : EuclideanVF n) {p : ℕ} (α : EuclideanΩ.CEuclideanΩ n (p + 1)) : EuclideanΩ n (p + 1)

Lie derivative of a $(p+1)$-form along a vector field $X$ via Cartan's magic formula: $\mathcal{L}_X \alpha = d(\iota_X \alpha) + \iota_X(d\alpha)$.

noncomputable def euclideanL0 {n : ℕ} (X : EuclideanVF n) (f : EuclideanΩ n 0) : EuclideanΩ n 0

Lie derivative on $0$-forms: $\mathcal{L}_X f = Df \cdot X$, the directional derivative of the scalar function underlying $f$ in the direction $X(x)$.

noncomputable def euclideanLie {n : ℕ} (X : EuclideanVF n) {p : ℕ} (α : EuclideanΩ n p) : EuclideanΩ n p

Lie derivative $\mathcal{L}_X : \Omega^p \to \Omega^p$ on Euclidean forms, defined via Cartan's magic formula. On $0$-forms it reduces to $\iota_X d\alpha$, and on $(p+1)$-forms to $d(\iota_X\alpha) + \iota_X(d\alpha)$.

theorem euclideanFMul_add_left {n p : ℕ} (f g : EuclideanΩ n 0) (α : EuclideanΩ n p) : euclideanFMul (f + g) α = euclideanFMul f α + euclideanFMul g α

Function-form multiplication is additive in the function: $(f + g)\,\alpha = f\,\alpha + g\,\alpha$.

theorem euclideanFMul_add_right {n p : ℕ} (f : EuclideanΩ n 0) (α β : EuclideanΩ n p) : euclideanFMul f (α + β) = euclideanFMul f α + euclideanFMul f β

Function-form multiplication is additive in the form: $f\,(\alpha + \beta) = f\,\alpha + f\,\beta$.

theorem euclideanFMul_smul {n p : ℕ} (r : ℝ) (f : EuclideanΩ n 0) (α : EuclideanΩ n p) : euclideanFMul (r • f) α = r • euclideanFMul f α

Scalar multiplication of the function commutes with function-form multiplication: $(r\,f)\,\alpha = r\,(f\,\alpha)$.

theorem euclideanIota_fMul {n : ℕ} (X : EuclideanVF n) {p : ℕ} (f : EuclideanΩ n 0) (α : EuclideanΩ n (p + 1)) : euclideanIota X (euclideanFMul f α) = euclideanFMul f (euclideanIota X α)

Contraction commutes with multiplication by a scalar function: $\iota_X(f \cdot \alpha) = f \cdot \iota_X \alpha$.

theorem euclideanD_lifted_add {n p : ℕ} (α β : EuclideanΩ n p) : (α + β).euclideanD_lifted = α.euclideanD_lifted + β.euclideanD_lifted

Additivity of the exterior derivative on Euclidean forms: $d(\alpha + \beta) = d\alpha + d\beta$.

theorem euclideanD_lifted_smul {n p : ℕ} (r : ℝ) (α : EuclideanΩ n p) : (r • α).euclideanD_lifted = r • α.euclideanD_lifted

Scalar compatibility of the exterior derivative on Euclidean forms: $d(r\,\alpha) = r\,d\alpha$.

theorem euclideanLie_add {n : ℕ} (X : EuclideanVF n) {p : ℕ} (α β : EuclideanΩ n p) : euclideanLie X (α + β) = euclideanLie X α + euclideanLie X β

Additivity of the Lie derivative in the form argument: $\mathcal{L}_X(\alpha + \beta) = \mathcal{L}_X\alpha + \mathcal{L}_X\beta$.

theorem euclideanLie_smul {n : ℕ} (X : EuclideanVF n) {p : ℕ} (r : ℝ) (α : EuclideanΩ n p) : euclideanLie X (r • α) = r • euclideanLie X α

Compatibility of the Lie derivative with scalar multiplication: $\mathcal{L}_X(r\,\alpha) = r\,\mathcal{L}_X\alpha$.

theorem euclideanD_eq_extDeriv_toAlternatingMap {n p : ℕ} (α : EuclideanΩ.CEuclideanΩ n p) (x : Eℝ n) : EuclideanΩ.euclideanD α x = (extDeriv α x).toAlternatingMap

The pointwise value of euclideanD α agrees with extDeriv α x after forgetting continuity. This bridges the local definition here with Mathlib's extDeriv.

theorem toCEuclideanΩ_euclideanD {n p : ℕ} (α : EuclideanΩ.CEuclideanΩ n p) : (EuclideanΩ.euclideanD α).toCEuclideanΩ = extDeriv α

The continuous-fibre lift of euclideanD α is exactly Mathlib's extDeriv α.

theorem euclideanD_lifted_d_squared {n p : ℕ} (α : EuclideanΩ n p) : α.euclideanD_lifted.euclideanD_lifted = 0

The fundamental identity $d \circ d = 0$ for the lifted Euclidean exterior derivative.

theorem curryLeft_alternatizeUncurryFin_smulRight {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {m : ℕ} (L : M →ₗ[R] R) (β : M [⋀^Fin (m + 1)]→ₗ[R] N) (v : M) : (AlternatingMap.alternatizeUncurryFin (L.smulRight β)).curryLeft v = L v • β - AlternatingMap.alternatizeUncurryFin (L.smulRight (β.curryLeft v))

Technical identity describing how curryLeft interacts with the antisymmetrisation of L.smulRight β for a linear functional $L$ and an alternating $(m+1)$-multilinear map $\beta$. Used to prove the Cartan formula relating $\iota_X$ and wedge product.

theorem oneFormLinear_apply_eq {n : ℕ} (ω_x : Eℝ n [⋀^Fin 1]→ₗ[ℝ] ℝ) (v : Eℝ n) : (oneFormLinear ω_x) v = ω_x (Matrix.vecCons v Fin.elim0)

Evaluation formula for oneFormLinear: applying it to $v$ equals applying the original $1$-form $\omega_x$ to the length-$1$ tuple containing $v$.

theorem euclideanIota_wedge1 {n : ℕ} (X : EuclideanVF n) {p : ℕ} (ω : EuclideanΩ n 1) (α : EuclideanΩ n (p + 1)) : euclideanIota X (euclideanWedge1 ω α) = euclideanFMul (euclideanIota X ω) α - euclideanWedge1 ω (euclideanIota X α)

Leibniz rule for contraction across a wedge with a $1$-form (the degree-$1$ case of $\iota_X(\omega \wedge \alpha) = (\iota_X\omega) \wedge \alpha - \omega \wedge (\iota_X\alpha)$, with the leading wedge becoming function-form multiplication since $\iota_X\omega$ is a $0$-form).

theorem euclidean_form_fdα_generation {n p : ℕ} (β : EuclideanΩ n (p + 1)) : ∃ (k : ℕ) (f : Fin k → EuclideanΩ n 0) (α : Fin k → EuclideanΩ n p), β = ∑ i : Fin k, euclideanFMul (f i) (α i).euclideanD_lifted

Generation principle: every $(p+1)$-form $\beta$ on $\mathbb{R}^n$ can be written as a finite sum $\sum_i f_i \cdot d\alpha_i$ with $f_i$ a $0$-form and $\alpha_i$ a $p$-form. This is the local analogue of the fact that $\Omega^\bullet$ is generated by $f \cdot dx_{i_1} \wedge \cdots \wedge dx_{i_p}$.

theorem euclideanD_lifted_fMul {n p : ℕ} (f : EuclideanΩ n 0) (α : EuclideanΩ n p) : (euclideanFMul f α).euclideanD_lifted = euclideanWedge1 f.euclideanD_lifted α + euclideanFMul f α.euclideanD_lifted

Leibniz rule for the exterior derivative across function-form multiplication: $d(f \cdot \alpha) = df \wedge \alpha + f \cdot d\alpha$.

theorem euclideanLie_fMul {n p : ℕ} (X : EuclideanVF n) (f : EuclideanΩ n 0) (α : EuclideanΩ n p) : euclideanLie X (euclideanFMul f α) = euclideanFMul (euclideanLie X f) α + euclideanFMul f (euclideanLie X α)

Leibniz rule for the Lie derivative across function-form multiplication: $\mathcal{L}_X(f \cdot \alpha) = (\mathcal{L}_X f) \cdot \alpha + f \cdot \mathcal{L}_X \alpha$.

@[implicit_reducible]

noncomputable instance euclideanDFS (n : ℕ) : DifferentialFormSpace (EuclideanΩ n) (EuclideanVF n)

The Euclidean differential form space instance for $\mathbb{R}^n$: collects the data $(\Omega^\bullet(\mathbb{R}^n), \mathfrak{X}(\mathbb{R}^n), \cdot, \wedge, d, \iota, \mathcal{L})$ together with all required compatibility identities (Leibniz, Cartan, $d^2 = 0$, anticommutativity of $\iota$, non-degeneracy). This is the concrete model on Euclidean space that scaffolds the abstract DifferentialFormSpace interface.