The ordinary Euclidean cross product as an actual bounded linear operator.

def EulerPacketCrossProduct.cross (a b : EulerSmoothLimit.Space) : EulerSmoothLimit.Space

Cross, given by toLp 2 (crossProduct (ofLp a) (ofLp b)).

Equations

• EulerPacketCrossProduct.cross a b = WithLp.toLp 2 ((crossProduct a.ofLp) b.ofLp)

theorem EulerPacketCrossProduct.cross_norm_le (a b : EulerSmoothLimit.Space) : ‖cross a b‖ ≤ ‖a‖ * ‖b‖

def EulerPacketCrossProduct.crossLinear (a : EulerSmoothLimit.Space) : EulerSmoothLimit.Space →ₗ[ℝ] EulerSmoothLimit.Space

Cross linear, bundling toFun, map_add, map_smul.

Equations

• EulerPacketCrossProduct.crossLinear a = { toFun := EulerPacketCrossProduct.cross a, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def EulerPacketCrossProduct.crossLeft (a : EulerSmoothLimit.Space) : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space

Cross left, given by (crossLinear a).mkContinuous ‖a‖ (cross_norm_le a).

Equations

• EulerPacketCrossProduct.crossLeft a = (EulerPacketCrossProduct.crossLinear a).mkContinuous ‖a‖ ⋯

theorem EulerPacketCrossProduct.crossLeft_apply (a b : EulerSmoothLimit.Space) : (crossLeft a) b = cross a b

theorem EulerPacketCrossProduct.crossLeft_norm_le (a : EulerSmoothLimit.Space) : ‖crossLeft a‖ ≤ ‖a‖

theorem EulerPacketCrossProduct.dot_eq_inner (a b : EulerSmoothLimit.Space) : a.ofLp ⬝ᵥ b.ofLp = inner ℝ a b

theorem EulerPacketCrossProduct.cross_cross (m a : EulerSmoothLimit.Space) : cross m (cross m a) = inner ℝ m a • m - ‖m‖ ^ 2 • a

theorem EulerPacketCrossProduct.cross_negative_normalized (m a : EulerSmoothLimit.Space) (hm : m ≠ 0) (ha : inner ℝ m a = 0) : cross m (-(‖m‖ ^ 2)⁻¹ • cross m a) = a

noncomputable def EulerPacketCrossProduct.potentialMultiplier (m : EulerSmoothLimit.Space) : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space

Its normalization is exactly the linear map used inside the angular primitive for Q.

Equations

• EulerPacketCrossProduct.potentialMultiplier m = -(‖m‖ ^ 2)⁻¹ • EulerPacketCrossProduct.crossLeft m

theorem EulerPacketCrossProduct.potentialMultiplier_apply (m a : EulerSmoothLimit.Space) : (potentialMultiplier m) a = -(‖m‖ ^ 2)⁻¹ • cross m a

theorem EulerPacketCrossProduct.cross_potentialMultiplier (m a : EulerSmoothLimit.Space) (hm : m ≠ 0) (ha : inner ℝ m a = 0) : cross m ((potentialMultiplier m) a) = a