The exact ordinary transport energy cancellation on noncompact smooth L² fields. Products and all required pairings are actual L²/L¹ objects.

theorem EulerOrdinarySobolev.field_toLp_zero (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : A.field = 0) : A.toLp = 0

theorem EulerOrdinarySobolev.scalarProduct_inner_shift (A : EulerLpTranslation.SmoothL2Field ℝ) (B C : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : inner ℝ (scalarProduct A B).toLp C.toLp = inner ℝ (scalarProduct A C).toLp B.toLp

theorem EulerOrdinarySobolev.scalar_transport_pair (A : EulerLpTranslation.SmoothL2Field ℝ) (B : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (v : EulerSmoothLimit.Space) : 2 * inner ℝ (scalarProduct A (B.directionalField v)).toLp B.toLp = -inner ℝ (scalarProduct (A.directionalField v) B).toLp B.toLp

theorem EulerOrdinarySobolev.coordinate_directional_field (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (i : Fin 3) (v x : EulerSmoothLimit.Space) : ((EulerLpTranslation.SmoothL2Field.mapField (EuclideanSpace.proj i) A).directionalField v).field x = ((fderiv ℝ A.field x) v).ofLp i

theorem EulerOrdinarySobolev.advection_inner_zero (A B : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence A.field x = 0) : inner ℝ (advectionField A B).toLp B.toLp = 0