The Poincaré lemma for 2-forms on a ball

Category: 1-Mathlib (CSD-free; upstream target Mathlib.Analysis.Calculus.DifferentialForm).

A closed C¹ 2-form on a ball is exact, with an explicit primitive: the radial primitive β x = ∫₀¹ t · ι_{x − x₀} ω(x₀ + t (x − x₀)) dt, the homotopy operator of the classical proof. Differentiating under the integral and using closedness (extDeriv ω = 0) at the segment points, the exterior derivative of β at x is ∫₀¹ (d/dt)(t² ω(x₀ + t (x − x₀))) dt = ω x.

Every integral here is a scalar one: radialPrimitiveVal ω x₀ x v is the value of the primitive on v, its x-derivative is a covector-valued integral, and the primitive is packaged as a covector (radialPrimitive) and as an alternating 1-form (radialPrimitiveForm) by linearity in v and finite dimension. (At this Mathlib pin the operator spaces over operator or alternating spaces do not carry the measurability instances the parametric integrals need, so the covector- and form-valued objects are never integrated.)

• isBoundedBilinearMap_apply_vecCons — (ξ, h) ↦ ξ ![h, v] is bounded bilinear; evalPair ω v (y, h) = ω y ![h, v], hasFDerivAt_evalPair;
• radialPrimitiveVal, radialPrimitiveIntegrand, radialPrimitiveDerivIntegrand, radialPrimitiveDerivVal — the scalar primitive β x v and its x-derivative ∫₀¹ t · D(evalPair ω v)(y_t, x − x₀) ∘ (t·1, 1);
• ★ hasFDerivAt_radialPrimitiveVal — β · v is differentiable on the ball (Mathlib's hasFDerivAt_integral_of_dominated_of_fderiv_le on the interval), and continuousOn_radialPrimitiveDerivVal, contDiffOn_radialPrimitiveVal — it is C¹ (continuousAt_of_dominated_interval);
• radialPrimitive ω x₀ x, radialPrimitiveForm ω x₀ x — the primitive as a covector and as a 1-form (radialPrimitiveForm_apply, radialPrimitiveForm_self), with ★ contDiffOn_radialPrimitive, ★ contDiffOn_radialPrimitiveForm and hasFDerivAt_radialPrimitiveForm (through a basis of E);
• fderiv_radialPrimitive_self, hasFDerivAt_radialPrimitiveForm_self — if ω x₀ = 0 then Dβ(x₀) = 0: the primitive of a form vanishing at the centre vanishes to second order there (what makes Moser's vector field small);
• ★★ extDeriv_radialPrimitiveForm — the Poincaré lemma: for ω closed on the ball, d β = ω on the ball.

Honest scope

⚠️ Degree 2 only, real-valued, on a ball. The homotopy operator in every degree and on every star-shaped set is the same computation with more indices; only the case Darboux's theorem needs is written.

⚠️ C¹. The form is assumed C¹ on the ball, and the primitive is shown C¹; higher regularity of the primitive (which the parametric integral inherits) is not stated.

References: Mathlib/Analysis/Calculus/ParametricIntervalIntegral.lean (hasFDerivAt_integral_of_dominated_of_fderiv_le); Mathlib/MeasureTheory/Integral/DominatedConvergence.lean (continuousAt_of_dominated_interval); Mathlib/Analysis/Calculus/DifferentialForm/Basic.lean (extDeriv_apply); Geometry/Manifold/HamiltonianLieDerivative.lean (the Fin 2/Fin 3 exterior-derivative idioms); intended consumer: Darboux's theorem by Moser's trick, specs/BACKLOG.md ▶ OPEN QUEUE #8 (the assembly that remains).

Evaluating a 2-form on a pair

theorem Matrix.update_vecCons_zero {α : Type u_2} (a b c : α) : Function.update ![a, b] 0 c = ![c, b]

theorem Matrix.update_vecCons_one {α : Type u_2} (a b c : α) : Function.update ![a, b] 1 c = ![a, c]

theorem isBoundedBilinearMap_apply_vecCons {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (v : E) : IsBoundedBilinearMap ℝ fun (p : E [⋀^Fin 2]→L[ℝ] ℝ × E) => p.1 ![p.2, v]

(ξ, h) ↦ ξ ![h, v] is bounded bilinear.

def evalPair {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (ω : E → E [⋀^Fin 2]→L[ℝ] ℝ) (v : E) (p : E × E) : ℝ

The scalar function (y, h) ↦ ω y ![h, v] on E × E.

Equations

• evalPair ω v p = (ω p.1) ![p.2, v]

theorem evalPair_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (ω : E → E [⋀^Fin 2]→L[ℝ] ℝ) (v y h : E) : evalPair ω v (y, h) = (ω y) ![h, v]

theorem hasFDerivAt_evalPair {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ω : E → E [⋀^Fin 2]→L[ℝ] ℝ} (v : E) {y : E} (hω : DifferentiableAt ℝ ω y) (h : E) : HasFDerivAt (evalPair ω v) (⋯.deriv (ω y, h) ∘SL (fderiv ℝ ω y ∘SL ContinuousLinearMap.fst ℝ E E).prod (ContinuousLinearMap.snd ℝ E E)) (y, h)

The derivative of evalPair: D(evalPair ω v)(y, h) (a, b) = Dω(y) a ![h, v] + ω y ![b, v].

theorem fderiv_evalPair_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ω : E → E [⋀^Fin 2]→L[ℝ] ℝ} (v : E) {y : E} (hω : DifferentiableAt ℝ ω y) (h a b : E) : (fderiv ℝ (evalPair ω v) (y, h)) (a, b) = ((fderiv ℝ ω y) a) ![h, v] + (ω y) ![b, v]

theorem contDiffOn_evalPair {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ω : E → E [⋀^Fin 2]→L[ℝ] ℝ} {x₀ : E} {R : ℝ} (hω : ContDiffOn ℝ 1 ω (Metric.ball x₀ R)) (v : E) : ContDiffOn ℝ 1 (evalPair ω v) (Metric.ball x₀ R ×ˢ Set.univ)

theorem contDiffOn_evalPair' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ω : E → E [⋀^Fin 2]→L[ℝ] ℝ} {x₀ : E} {R : ℝ} {n : ℕ∞} (hω : ContDiffOn ℝ (↑n) ω (Metric.ball x₀ R)) (v : E) : ContDiffOn ℝ (↑n) (evalPair ω v) (Metric.ball x₀ R ×ˢ Set.univ)

evalPair ω v is C^n where ω is.

The segment

@[reducible, inline]

abbrev segPt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (x₀ x : E) (t : ℝ) : E

The point at parameter t on the segment from x₀ to x.

Equations

• segPt x₀ x t = x₀ + t • (x - x₀)

theorem segPt_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (x₀ x : E) : segPt x₀ x 0 = x₀

theorem segPt_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (x₀ x : E) : segPt x₀ x 1 = x

theorem segPt_self {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (x₀ : E) (t : ℝ) : segPt x₀ x₀ t = x₀

theorem norm_segPt_sub_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x₀ x : E} {t : ℝ} (ht : t ∈ Set.Icc 0 1) : ‖segPt x₀ x t - x₀‖ ≤ ‖x - x₀‖

theorem segPt_mem_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x₀ x : E} {R : ℝ} (hx : x ∈ Metric.ball x₀ R) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : segPt x₀ x t ∈ Metric.ball x₀ R

theorem segPt_mem_closedBall {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x₀ x : E} {r : ℝ} (hx : x ∈ Metric.closedBall x₀ r) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : segPt x₀ x t ∈ Metric.closedBall x₀ r

theorem hasFDerivAt_segPt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (x₀ : E) (t : ℝ) (x : E) : HasFDerivAt (fun (x : E) => segPt x₀ x t) (t • ContinuousLinearMap.id ℝ E) x

theorem continuous_segPt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (x₀ x : E) : Continuous (segPt x₀ x)

theorem continuous_segPt_left {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (x₀ : E) (t : ℝ) : Continuous fun (x : E) => segPt x₀ x t

theorem hasDerivAt_segPt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (x₀ x : E) (t : ℝ) : HasDerivAt (segPt x₀ x) (x - x₀) t

The scalar primitive and its derivative

def radialPrimitiveIntegrand {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (ω : E → E [⋀^Fin 2]→L[ℝ] ℝ) (x₀ v x : E) (t : ℝ) : ℝ

The integrand of the radial primitive evaluated on v: t · ω(x₀ + t (x − x₀)) ![x − x₀, v].

Equations

• radialPrimitiveIntegrand ω x₀ v x t = t * evalPair ω v (segPt x₀ x t, x - x₀)

noncomputable def radialPrimitiveVal {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (ω : E → E [⋀^Fin 2]→L[ℝ] ℝ) (x₀ x v : E) : ℝ

The radial primitive evaluated on v: β x v = ∫₀¹ t · ω(x₀ + t (x − x₀)) ![x − x₀, v] dt.

Equations

• radialPrimitiveVal ω x₀ x v = ∫ (t : ℝ) in 0..1, radialPrimitiveIntegrand ω x₀ v x t

noncomputable def radialPrimitiveDerivIntegrand {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (ω : E → E [⋀^Fin 2]→L[ℝ] ℝ) (x₀ v x : E) (t : ℝ) : E →L[ℝ] ℝ

The x-derivative of the integrand.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def radialPrimitiveDerivVal {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (ω : E → E [⋀^Fin 2]→L[ℝ] ℝ) (x₀ x v : E) : E →L[ℝ] ℝ

The x-derivative of β · v: the integral of the derivative of the integrand.

Equations

• radialPrimitiveDerivVal ω x₀ x v = ∫ (t : ℝ) in 0..1, radialPrimitiveDerivIntegrand ω x₀ v x t

theorem radialPrimitiveIntegrand_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ω : E → E [⋀^Fin 2]→L[ℝ] ℝ} {x₀ : E} (v x : E) (t : ℝ) : radialPrimitiveIntegrand ω x₀ v x t = t * (ω (segPt x₀ x t)) ![x - x₀, v]

theorem radialPrimitiveDerivIntegrand_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ω : E → E [⋀^Fin 2]→L[ℝ] ℝ} {x₀ : E} (v x : E) (t : ℝ) (u : E) : (radialPrimitiveDerivIntegrand ω x₀ v x t) u = t * (fderiv ℝ (evalPair ω v) (segPt x₀ x t, x - x₀)) (t • u, u)

theorem radialPrimitiveVal_self {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ω : E → E [⋀^Fin 2]→L[ℝ] ℝ} {x₀ : E} (v : E) : radialPrimitiveVal ω x₀ x₀ v = 0

β x₀ v = 0.

theorem hasFDerivAt_radialPrimitiveIntegrand {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ω : E → E [⋀^Fin 2]→L[ℝ] ℝ} {x₀ : E} (v : E) {x : E} {t : ℝ} (hω : DifferentiableAt ℝ ω (segPt x₀ x t)) : HasFDerivAt (fun (x : E) => radialPrimitiveIntegrand ω x₀ v x t) (radialPrimitiveDerivIntegrand ω x₀ v x t) x

The integrand is differentiable in x wherever ω is differentiable at the segment point.

Differentiability and continuity, by dominated convergence

theorem continuousOn_radialPrimitiveIntegrand {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ω : E → E [⋀^Fin 2]→L[ℝ] ℝ} {x₀ : E} {R : ℝ} (hω : ContDiffOn ℝ 1 ω (Metric.ball x₀ R)) (v : E) {x : E} (hx : x ∈ Metric.ball x₀ R) : ContinuousOn (radialPrimitiveIntegrand ω x₀ v x) (Set.Icc 0 1)

Continuity of the integrand in t on [0, 1], for x in the ball.

theorem continuousOn_radialPrimitiveDerivIntegrand {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ω : E → E [⋀^Fin 2]→L[ℝ] ℝ} {x₀ : E} {R : ℝ} (hω : ContDiffOn ℝ 1 ω (Metric.ball x₀ R)) (v : E) {x : E} (hx : x ∈ Metric.ball x₀ R) : ContinuousOn (radialPrimitiveDerivIntegrand ω x₀ v x) (Set.Icc 0 1)

Continuity of the derivative integrand in t on [0, 1], for x in the ball.

theorem exists_bound_radialPrimitiveDerivIntegrand {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ω : E → E [⋀^Fin 2]→L[ℝ] ℝ} {x₀ : E} {R : ℝ} [FiniteDimensional ℝ E] (hω : ContDiffOn ℝ 1 ω (Metric.ball x₀ R)) (v : E) {r : ℝ} (hr : r < R) : ∃ (B : ℝ), ∀ x ∈ Metric.closedBall x₀ r, ∀ t ∈ Set.Icc 0 1, ‖radialPrimitiveDerivIntegrand ω x₀ v x t‖ ≤ B

A uniform bound on the derivative integrand on a closed ball inside the ball of definition.

theorem hasFDerivAt_radialPrimitiveVal {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ω : E → E [⋀^Fin 2]→L[ℝ] ℝ} {x₀ : E} {R : ℝ} [FiniteDimensional ℝ E] (hω : ContDiffOn ℝ 1 ω (Metric.ball x₀ R)) (v : E) {x : E} (hx : x ∈ Metric.ball x₀ R) : HasFDerivAt (fun (x : E) => radialPrimitiveVal ω x₀ x v) (radialPrimitiveDerivVal ω x₀ x v) x

★ β · v is differentiable on the ball, with derivative the integral of the derivative of the integrand.

theorem continuousOn_radialPrimitiveDerivVal {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ω : E → E [⋀^Fin 2]→L[ℝ] ℝ} {x₀ : E} {R : ℝ} [FiniteDimensional ℝ E] (hω : ContDiffOn ℝ 1 ω (Metric.ball x₀ R)) (v : E) : ContinuousOn (fun (x : E) => radialPrimitiveDerivVal ω x₀ x v) (Metric.ball x₀ R)

The derivative of β · v is continuous on the ball.

theorem contDiffOn_radialPrimitiveVal {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ω : E → E [⋀^Fin 2]→L[ℝ] ℝ} {x₀ : E} {R : ℝ} [FiniteDimensional ℝ E] (hω : ContDiffOn ℝ 1 ω (Metric.ball x₀ R)) (v : E) : ContDiffOn ℝ 1 (fun (x : E) => radialPrimitiveVal ω x₀ x v) (Metric.ball x₀ R)

★ β · v is C¹ on the ball.

theorem contDiffOn_radialPrimitiveIntegrand_uncurry {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ω : E → E [⋀^Fin 2]→L[ℝ] ℝ} {x₀ : E} {R : ℝ} {n : ℕ∞} (hω : ContDiffOn ℝ (↑n) ω (Metric.ball x₀ R)) (v : E) : ContDiffOn ℝ (↑n) (Function.uncurry fun (x : E) (t : ℝ) => radialPrimitiveIntegrand ω x₀ v x t) {p : E × ℝ | segPt x₀ p.1 p.2 ∈ Metric.ball x₀ R}

The integrand of the radial primitive is jointly C^n in (x, t) where the segment point lies in the ball, for ω of class C^n.

theorem contDiffOn_radialPrimitiveVal' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ω : E → E [⋀^Fin 2]→L[ℝ] ℝ} {x₀ : E} {R : ℝ} [FiniteDimensional ℝ E] {n : ℕ∞} (hω : ContDiffOn ℝ (↑n) ω (Metric.ball x₀ R)) (v : E) : ContDiffOn ℝ (↑n) (fun (x : E) => radialPrimitiveVal ω x₀ x v) (Metric.ball x₀ R)

★ β · v is C^n on the ball for ω of class C^n (n ≤ ∞): the parametric interval integral of a jointly C^n integrand (contDiffOn_intervalIntegral_of_contDiffOn).

The primitive as a covector and as a 1-form

theorem radialPrimitiveIntegrand_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (ω : E → E [⋀^Fin 2]→L[ℝ] ℝ) (x₀ x : E) (t : ℝ) (v w : E) : radialPrimitiveIntegrand ω x₀ (v + w) x t = radialPrimitiveIntegrand ω x₀ v x t + radialPrimitiveIntegrand ω x₀ w x t

The integrand is additive in v.

theorem radialPrimitiveIntegrand_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (ω : E → E [⋀^Fin 2]→L[ℝ] ℝ) (x₀ x : E) (t c : ℝ) (v : E) : radialPrimitiveIntegrand ω x₀ (c • v) x t = c * radialPrimitiveIntegrand ω x₀ v x t

The integrand is homogeneous in v.

theorem radialPrimitiveVal_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ω : E → E [⋀^Fin 2]→L[ℝ] ℝ} {x₀ : E} {R : ℝ} (hω : ContDiffOn ℝ 1 ω (Metric.ball x₀ R)) {x : E} (hx : x ∈ Metric.ball x₀ R) (v w : E) : radialPrimitiveVal ω x₀ x (v + w) = radialPrimitiveVal ω x₀ x v + radialPrimitiveVal ω x₀ x w

theorem radialPrimitiveVal_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ω : E → E [⋀^Fin 2]→L[ℝ] ℝ} {x₀ x : E} (c : ℝ) (v : E) : radialPrimitiveVal ω x₀ x (c • v) = c * radialPrimitiveVal ω x₀ x v

theorem radialPrimitiveVal_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ω : E → E [⋀^Fin 2]→L[ℝ] ℝ} {x₀ x : E} : radialPrimitiveVal ω x₀ x 0 = 0

noncomputable def radialPrimitive {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (ω : E → E [⋀^Fin 2]→L[ℝ] ℝ) (x₀ : E) (R : ℝ) (x : E) : E →L[ℝ] ℝ

The radial primitive as a covector, on the ball (0 off it).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def radialPrimitiveForm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (ω : E → E [⋀^Fin 2]→L[ℝ] ℝ) (x₀ : E) (R : ℝ) (x : E) : E [⋀^Fin 1]→L[ℝ] ℝ

The radial primitive as an alternating 1-form.

Equations

• radialPrimitiveForm ω x₀ R x = (ContinuousAlternatingMap.ofSubsingletonLIE 0) (radialPrimitive ω x₀ R x)

theorem radialPrimitive_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {ω : E → E [⋀^Fin 2]→L[ℝ] ℝ} {x₀ : E} {R : ℝ} (hω : ContDiffOn ℝ 1 ω (Metric.ball x₀ R)) {x : E} (hx : x ∈ Metric.ball x₀ R) (v : E) : (radialPrimitive ω x₀ R x) v = radialPrimitiveVal ω x₀ x v

theorem radialPrimitiveForm_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {ω : E → E [⋀^Fin 2]→L[ℝ] ℝ} {x₀ : E} {R : ℝ} (hω : ContDiffOn ℝ 1 ω (Metric.ball x₀ R)) {x : E} (hx : x ∈ Metric.ball x₀ R) (m : Fin 1 → E) : (radialPrimitiveForm ω x₀ R x) m = radialPrimitiveVal ω x₀ x (m 0)

theorem radialPrimitiveForm_self {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {ω : E → E [⋀^Fin 2]→L[ℝ] ℝ} {x₀ : E} {R : ℝ} (hω : ContDiffOn ℝ 1 ω (Metric.ball x₀ R)) (hR : 0 < R) : radialPrimitiveForm ω x₀ R x₀ = 0

theorem radialPrimitive_eq_sum {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {ω : E → E [⋀^Fin 2]→L[ℝ] ℝ} {x₀ : E} {R : ℝ} (hω : ContDiffOn ℝ 1 ω (Metric.ball x₀ R)) {x : E} (hx : x ∈ Metric.ball x₀ R) (b : Module.Basis (Fin (Module.finrank ℝ E)) ℝ E) : radialPrimitive ω x₀ R x = ∑ i : Fin (Module.finrank ℝ E), radialPrimitiveVal ω x₀ x (b i) • LinearMap.toContinuousLinearMap (b.coord i)

The covector β x expanded in a basis of E: β x = ∑ᵢ β x (bᵢ) • bᵢ*.

theorem radialPrimitiveForm_eq_sum {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {ω : E → E [⋀^Fin 2]→L[ℝ] ℝ} {x₀ : E} {R : ℝ} (hω : ContDiffOn ℝ 1 ω (Metric.ball x₀ R)) {x : E} (hx : x ∈ Metric.ball x₀ R) (b : Module.Basis (Fin (Module.finrank ℝ E)) ℝ E) : radialPrimitiveForm ω x₀ R x = ∑ i : Fin (Module.finrank ℝ E), radialPrimitiveVal ω x₀ x (b i) • (ContinuousAlternatingMap.ofSubsingletonLIE 0) (LinearMap.toContinuousLinearMap (b.coord i))

The 1-form β x expanded in a basis of E.

theorem contDiffOn_radialPrimitive {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {ω : E → E [⋀^Fin 2]→L[ℝ] ℝ} {x₀ : E} {R : ℝ} (hω : ContDiffOn ℝ 1 ω (Metric.ball x₀ R)) : ContDiffOn ℝ 1 (radialPrimitive ω x₀ R) (Metric.ball x₀ R)

★ The radial primitive is C¹ on the ball (as a covector field).

theorem contDiffOn_radialPrimitiveForm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {ω : E → E [⋀^Fin 2]→L[ℝ] ℝ} {x₀ : E} {R : ℝ} (hω : ContDiffOn ℝ 1 ω (Metric.ball x₀ R)) : ContDiffOn ℝ 1 (radialPrimitiveForm ω x₀ R) (Metric.ball x₀ R)

★ The radial primitive is C¹ on the ball (as a 1-form).

theorem contDiffOn_radialPrimitive' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {ω : E → E [⋀^Fin 2]→L[ℝ] ℝ} {x₀ : E} {R : ℝ} {n : ℕ∞} (hn : 1 ≤ n) (hω : ContDiffOn ℝ (↑n) ω (Metric.ball x₀ R)) : ContDiffOn ℝ (↑n) (radialPrimitive ω x₀ R) (Metric.ball x₀ R)

★ The radial primitive is C^n on the ball (as a covector field), for ω of class C^n, 1 ≤ n ≤ ∞.

theorem contDiffOn_radialPrimitiveForm' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {ω : E → E [⋀^Fin 2]→L[ℝ] ℝ} {x₀ : E} {R : ℝ} {n : ℕ∞} (hn : 1 ≤ n) (hω : ContDiffOn ℝ (↑n) ω (Metric.ball x₀ R)) : ContDiffOn ℝ (↑n) (radialPrimitiveForm ω x₀ R) (Metric.ball x₀ R)

★ The radial primitive is C^n on the ball (as a 1-form), for ω of class C^n, 1 ≤ n ≤ ∞.

theorem hasFDerivAt_radialPrimitiveForm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {ω : E → E [⋀^Fin 2]→L[ℝ] ℝ} {x₀ : E} {R : ℝ} (hω : ContDiffOn ℝ 1 ω (Metric.ball x₀ R)) {x : E} (hx : x ∈ Metric.ball x₀ R) (b : Module.Basis (Fin (Module.finrank ℝ E)) ℝ E) : HasFDerivAt (radialPrimitiveForm ω x₀ R) (∑ i : Fin (Module.finrank ℝ E), (radialPrimitiveDerivVal ω x₀ x (b i)).smulRight ((ContinuousAlternatingMap.ofSubsingletonLIE 0) (LinearMap.toContinuousLinearMap (b.coord i)))) x

The derivative of the 1-form β, through a basis.

theorem radialPrimitiveDerivVal_self {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ω : E → E [⋀^Fin 2]→L[ℝ] ℝ} {x₀ : E} {R : ℝ} (hω : ContDiffOn ℝ 1 ω (Metric.ball x₀ R)) (hR : 0 < R) (h0 : ω x₀ = 0) (v : E) : radialPrimitiveDerivVal ω x₀ x₀ v = 0

If the form vanishes at the centre, its radial primitive vanishes to second order there: D(β · v)(x₀) = 0.

theorem hasFDerivAt_radialPrimitiveForm_self {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {ω : E → E [⋀^Fin 2]→L[ℝ] ℝ} {x₀ : E} {R : ℝ} (hω : ContDiffOn ℝ 1 ω (Metric.ball x₀ R)) (hR : 0 < R) (h0 : ω x₀ = 0) : HasFDerivAt (radialPrimitiveForm ω x₀ R) 0 x₀

If the form vanishes at the centre, the 1-form β has derivative 0 at x₀.

theorem fderiv_radialPrimitive_self {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {ω : E → E [⋀^Fin 2]→L[ℝ] ℝ} {x₀ : E} {R : ℝ} (hω : ContDiffOn ℝ 1 ω (Metric.ball x₀ R)) (hR : 0 < R) (h0 : ω x₀ = 0) : fderiv ℝ (radialPrimitive ω x₀ R) x₀ = 0

If the form vanishes at the centre, Dβ(x₀) = 0.

The Poincaré lemma

theorem radialPrimitiveDerivVal_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ω : E → E [⋀^Fin 2]→L[ℝ] ℝ} {x₀ : E} {R : ℝ} (hω : ContDiffOn ℝ 1 ω (Metric.ball x₀ R)) (v : E) {x : E} (hx : x ∈ Metric.ball x₀ R) (u : E) : (radialPrimitiveDerivVal ω x₀ x v) u = ∫ (t : ℝ) in 0..1, t ^ 2 * ((fderiv ℝ ω (segPt x₀ x t)) u) ![x - x₀, v] + t * (ω (segPt x₀ x t)) ![u, v]

The value of the derivative of β · v on u: the integral of the derivative integrand's values.

theorem extDeriv_radialPrimitiveForm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {ω : E → E [⋀^Fin 2]→L[ℝ] ℝ} {x₀ : E} {R : ℝ} (hω : ContDiffOn ℝ 1 ω (Metric.ball x₀ R)) (hclosed : ∀ y ∈ Metric.ball x₀ R, extDeriv ω y = 0) {x : E} (hx : x ∈ Metric.ball x₀ R) : extDeriv (radialPrimitiveForm ω x₀ R) x = ω x

★★ The Poincaré lemma for 2-forms on a ball: if ω is C¹ and closed on the ball, the exterior derivative of its radial primitive is ω.