structure StokesIntegration {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] : Type u_1

An integration structure on a differential form space supporting Stokes' theorem: provides a top dimension $n$, a wedge-pairing $\langle \alpha, \beta \rangle$ on $p$-forms, an integral $\int : \Omega^n \to \mathbb{R}$, and the Leibniz/integration-by-parts identity $\int (d\alpha) \wedge \beta = (-1)^{p+1} \int \alpha \wedge d\beta$.

• n : ℕ
• wedge_star (p : ℕ) : Ω p → Ω p → Ω self.n
• integrate : Ω self.n → ℝ
• linear_integrate : Ω self.n →ₗ[ℝ] ℝ
• linear_integrate_eq (ω : Ω self.n) : self.linear_integrate ω = self.integrate ω
• wedge_star_linear_left (p : ℕ) (r : ℝ) (α₁ α₂ β : Ω p) : self.wedge_star p (r • α₁ + α₂) β = r • self.wedge_star p α₁ β + self.wedge_star p α₂ β
• wedge_star_linear_right (p : ℕ) (r : ℝ) (α β₁ β₂ : Ω p) : self.wedge_star p α (r • β₁ + β₂) = r • self.wedge_star p α β₁ + self.wedge_star p α β₂
• d_top (_p : ℕ) : Ω _p → Ω _p → Ω self.n
• stokes_on_exact (p : ℕ) (α β : Ω p) : self.integrate (self.d_top p α β) = 0
• wedge_star_d (_p : ℕ) : Ω _p → Ω (_p + 1) → Ω self.n
• leibniz_rule (p : ℕ) (α : Ω p) (β : Ω (p + 1)) : self.integrate (self.wedge_star (p + 1) (DifferentialFormSpace.d VF α) β) = (-1) ^ (p + 1) • self.integrate (self.wedge_star_d p α β)

def StokesIntegration.inner_prod {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (S : StokesIntegration) (p : ℕ) (α β : Ω p) : ℝ

The $L^2$ inner product on $p$-forms induced by the Hodge-star pairing: $\langle \alpha, \beta \rangle = \int \alpha \wedge \star \beta$.

theorem StokesIntegration.inner_product_linear {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (S : StokesIntegration) (p : ℕ) (r : ℝ) (α₁ α₂ β : Ω p) : S.inner_prod p (r • α₁ + α₂) β = r * S.inner_prod p α₁ β + S.inner_prod p α₂ β

Linearity of the inner product in the first argument: $\langle r\alpha_1 + \alpha_2, \beta \rangle = r\langle \alpha_1, \beta \rangle + \langle \alpha_2, \beta \rangle$.

theorem StokesIntegration.stokes_adjoint_identity {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (S : StokesIntegration) (p : ℕ) (α : Ω p) (β : Ω (p + 1)) : S.inner_prod (p + 1) (DifferentialFormSpace.d VF α) β = (-1) ^ (p + 1) • S.integrate (S.wedge_star_d p α β)

Adjointness from Stokes' theorem: $\langle d\alpha, \beta \rangle = (-1)^{p+1} \int \alpha \wedge d\beta$, identifying $d$ as (up to sign) the formal adjoint to itself in the pairing.