The oriented integration current of a Euclidean open set #

Let E be a real vector space of finite dimension m with an orientation o, and let Ω be an open subset of E. The integration current [[Ω]] of Ω is the top-degree current ω ↦ ∫_Ω ω, a continuous linear functional on the test m-forms 𝓓^{n}(Ω, E [⋀^Fin m]→L[ℝ] ℝ). In coordinates, for any basis b of E with orientation o, [[Ω]] ω = ∫ x, ω x b ∂b.addHaar, the integral of the coefficient of ω in the basis b against the Haar measure normalized by b. This does not depend on the choice of b: the factor b.det b' by which the coefficient changes and the factor |b.det b'|⁻¹ by which the measure changes cancel for bases of the same orientation (Module.Basis.integral_signed_apply_eq). No inner product or choice of measure on E is needed to define [[Ω]]; only the Borel structure enters. Continuity comes from Mathlib's TestFunction.integralAgainstBilinCLM.

This is the comparison current of the constancy theorem: on a connected open set, a top-degree current with zero boundary is a constant multiple of [[Ω]]. Here we prove that [[Ω]] itself has zero boundary, [[Ω]] (d ω) = 0, which is Stokes' theorem for compactly supported forms on an open set; that reversing the orientation negates it; that it is compatible with extending test forms by zero from a smaller open set; and its normalizations in degree zero and on inner product spaces.

The integration current is natural under changes of coordinates. If Φ : E → E is smooth on Ω, maps Ω injectively onto Ω', and is proper from Ω to Ω', then the pushforward Φ_# [[Ω]] = [[Ω]] ∘ Φ^* along the pullback of test forms TestFunction.pullbackCLM is [[Ω']] when the Jacobian determinant of Φ is nonnegative on Ω, and -[[Ω']] when it is nonpositive. This is the change of variables formula ∫_Ω Φ^* ω = ± ∫_{Ω'} ω for compactly supported top-degree forms. The Jacobian may vanish at some points, as for x ↦ x ^ 3. On a preconnected Ω on which the Jacobian does not vanish, its sign is constant, so Φ_# [[Ω]] = ± [[Ω']]. The maps are self-maps of E, as are the transition maps between charts with values in a model space.

Main declarations #

Orientation.integrationCurrent o Ω: the oriented integration current [[Ω]].
Orientation.integrationCurrent_apply: [[Ω]] ω = ∫ x, ω x b ∂b.addHaar for every basis b of orientation o; Orientation.integrationCurrent_apply_eq_signBasis_mul computes it in an arbitrary basis.
Orientation.integrationCurrent_apply_eq_integral_volume: on an inner product space, [[Ω]] ω = ∫ x, ω x b against the volume for every positively oriented orthonormal basis b.
Orientation.integrationCurrent_neg: [[Ω]] changes sign with the orientation.
Orientation.integrationCurrent_comp_extDerivCLM: [[Ω]] has zero boundary, [[Ω]] ∘ d = 0.
Orientation.integrationCurrent_monoCLM: restriction to a smaller open set.
Orientation.integrationCurrent_positiveOrientation_apply: in dimension zero, the positively oriented point is the Dirac current at the origin.
Orientation.integrationCurrent_pullbackCLM: change of variables, [[Ω]] (Φ^* ω) = ε [[Ω']] ω when the Jacobian determinant of Φ has the sign ε = ±1 on Ω; Orientation.integrationCurrent_pullbackCLM_of_nonneg and Orientation.integrationCurrent_pullbackCLM_of_nonpos are the two cases.
Orientation.integrationCurrent_comp_pullbackCLM: the pushforward Φ_# [[Ω]] is ε [[Ω']].
Orientation.exists_integrationCurrent_comp_pullbackCLM_eq_smul: on a preconnected Ω with nonvanishing Jacobian, Φ_# [[Ω]] = ± [[Ω']].

References #

H. Federer, Geometric Measure Theory, §4.1.7.
J. M. Lee, Introduction to Smooth Manifolds, second edition, Chapter 16 (including the diffeomorphism invariance of the integral of a form).