Green's formula for bilinear pairings on rectangles and annuli

Let u : ℝ × ℝ → V be a C² map near a closed rectangle R = [a₁, b₁] × [a₂, b₂] and let B be a continuous bilinear map. Writing ∂s u and ∂t u for the derivatives of u in the directions (1, 0) and (0, 1),

∫_R (B (∂s u) (∂t u) - B (∂t u) (∂s u)) = ∮_{∂R} B (u) (du),

where the right-hand side is the integral over the positively oriented boundary of R, written out as four interval integrals. This is Green's theorem for the pullback along u of the one-form x ↦ B x, whose exterior derivative is the constant two-form (v, w) ↦ B v w - B w v. Both formulas below are TauCeti.integral_extDeriv_prod_Icc and TauCeti.integral_extDeriv_annulus applied to the pullback along u of the one-form x ↦ B x.

For a compactly supported map on the whole plane the boundary terms are absent and the integral vanishes (TauCeti.integral_bilinear_fderiv_apply_comm). With boundary, this is the formula that expresses the symplectic area of a map from a rectangle into an exact symplectic vector space by integrals of a primitive along its four sides.

For positive inner radius, neither the map nor its derivatives need be regular on the inner disc. At zero inner radius the inner boundary integral vanishes, giving Green's formula on a disc.

Main results

• ContinuousLinearMap.integral_bilinear_fderiv_sub_prod_Icc: Green's formula above, over Set.Icc a b for points a ≤ b of ℝ × ℝ.
• ContinuousLinearMap.integral_bilinear_fderiv_sub_annulus: the corresponding formula on a translated annulus of nonnegative inner radius, with outer minus inner circle boundary terms.

theorem ContinuousLinearMap.integral_bilinear_fderiv_sub_prod_Icc {V : Type u_2} {W : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (B : V →L[ℝ] V →L[ℝ] W) {u : ℝ × ℝ → V} {a b : ℝ × ℝ} (hle : a ≤ b) (hu : ∀ z ∈ Set.Icc a b, ContDiffAt ℝ 2 u z) : ∫ (z : ℝ × ℝ) in Set.Icc a b, (B ((fderiv ℝ u z) (1, 0))) ((fderiv ℝ u z) (0, 1)) - (B ((fderiv ℝ u z) (0, 1))) ((fderiv ℝ u z) (1, 0)) = ((∫ (t : ℝ) in a.2..b.2, (B (u (b.1, t))) ((fderiv ℝ u (b.1, t)) (0, 1))) - ∫ (t : ℝ) in a.2..b.2, (B (u (a.1, t))) ((fderiv ℝ u (a.1, t)) (0, 1))) - ((∫ (s : ℝ) in a.1..b.1, (B (u (s, b.2))) ((fderiv ℝ u (s, b.2)) (1, 0))) - ∫ (s : ℝ) in a.1..b.1, (B (u (s, a.2))) ((fderiv ℝ u (s, a.2)) (1, 0)))

Green's formula for a bilinear pairing of partial derivatives. If u is C² at every point of the rectangle Icc a b ⊆ ℝ × ℝ and B is a continuous bilinear map, the integral over the rectangle of B (∂s u) (∂t u) - B (∂t u) (∂s u) is the integral of the one-form B u (du) over the positively oriented boundary: the right side minus the left side of t ↦ B u (∂t u), minus the top side minus the bottom side of s ↦ B u (∂s u).

theorem ContinuousLinearMap.integral_bilinear_fderiv_sub_annulus {V : Type u_2} {W : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (B : V →L[ℝ] V →L[ℝ] W) {u : ℂ → V} (z₀ : ℂ) {a b : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) (hu : ∀ z ∈ {z : ℂ | a ≤ ‖z - z₀‖ ∧ ‖z - z₀‖ ≤ b}, ContDiffAt ℝ 2 u z) : ∫ (z : ℂ) in {z : ℂ | a ≤ ‖z - z₀‖ ∧ ‖z - z₀‖ ≤ b}, (B ((fderiv ℝ u z) 1)) ((fderiv ℝ u z) Complex.I) - (B ((fderiv ℝ u z) Complex.I)) ((fderiv ℝ u z) 1) = (∫ (θ : ℝ) in -Real.pi..Real.pi, (B (u (circleMap z₀ b θ))) ((fderiv ℝ u (circleMap z₀ b θ)) (circleMap 0 b θ * Complex.I))) - ∫ (θ : ℝ) in -Real.pi..Real.pi, (B (u (circleMap z₀ a θ))) ((fderiv ℝ u (circleMap z₀ a θ)) (circleMap 0 a θ * Complex.I))

Green's formula on a closed annulus. For a C² map near the annulus of radii 0 ≤ a ≤ b, the integral of the alternating part of a bilinear pairing of its derivatives equals the outer circle integral of B u du minus the inner circle integral. Both circles are parametrized counterclockwise; their difference gives the boundary orientation.