The one-form x dy on the real plane

This file defines the linear-coefficient form realPlaneXDy = x dy and proves its exterior derivative identity. The constant coordinate forms and their identities are in TauCeti.Analysis.Calculus.DifferentialForm.Plane.

Contracting d(x dy) with the vector field Z = x ∂_x + ∂_y gives x dy - dx (Prod.curryLeft_extDeriv_realPlaneXDy), which differs from x dy (Prod.curryLeft_extDeriv_realPlaneXDy_ne).

The computation of d(x dy) reuses the radial primitive calculation for a continuous bilinear form from TauCeti.Geometry.Symplectic.Liouville.Linear.

def Prod.realPlaneXDy (p : ℝ × ℝ) : (ℝ × ℝ) [⋀^Fin 1]→L[ℝ] ℝ

The coordinate one-form x dy on ℝ × ℝ.

@[simp]

theorem Prod.realPlaneXDy_apply (p : ℝ × ℝ) (v : Fin 1 → ℝ × ℝ) : p.realPlaneXDy v = p.1 * (v 0).2

The coordinate one-form x dy evaluates to the first coordinate of the base point times the second component of its argument.

theorem Prod.contDiff_realPlaneXDy {n : WithTop ℕ∞} : ContDiff ℝ n realPlaneXDy

The coordinate one-form x dy is smooth, being linear in the base point.

@[simp]

theorem Prod.extDeriv_realPlaneXDy (p : ℝ × ℝ) : extDeriv realPlaneXDy p = p.realPlaneDx.wedge p.realPlaneDy

The exterior derivative of x dy is the standard area form dx ∧ dy.

theorem Prod.curryLeft_extDeriv_realPlaneXDy (p : ℝ × ℝ) : (extDeriv realPlaneXDy p).curryLeft (p.1, 1) = p.realPlaneXDy - p.realPlaneDx

For the vector field Z = x ∂_x + ∂_y, ι_Z d(x dy) = x dy - dx.

theorem Prod.curryLeft_extDeriv_realPlaneXDy_ne (p : ℝ × ℝ) : (extDeriv realPlaneXDy p).curryLeft (p.1, 1) ≠ p.realPlaneXDy

The vector field Z = x ∂_x + ∂_y is not the Liouville field of the primitive x dy of dx ∧ dy: ι_Z d(x dy) ≠ x dy at every point.