Ordinary integration by parts for genuine smooth L² fields. The identity needs no compact-support premise because all three pairings in the Haar-measure integration theorem are integrable.

theorem EulerOrdinarySobolev.field_inner_integrable {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (A B : EulerLpTranslation.SmoothL2Field V) : MeasureTheory.Integrable (fun (x : EulerSmoothLimit.Space) => inner ℝ (A.field x) (B.field x)) MeasureTheory.volume

theorem EulerOrdinarySobolev.field_inner {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (A B : EulerLpTranslation.SmoothL2Field V) : inner ℝ A.toLp B.toLp = ∫ (x : EulerSmoothLimit.Space), inner ℝ (A.field x) (B.field x)

theorem EulerOrdinarySobolev.field_directional_ibp {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (A B : EulerLpTranslation.SmoothL2Field V) (v : EulerSmoothLimit.Space) : ∫ (x : EulerSmoothLimit.Space), inner ℝ ((fderiv ℝ A.field x) v) (B.field x) = -∫ (x : EulerSmoothLimit.Space), inner ℝ (A.field x) ((fderiv ℝ B.field x) v)

theorem EulerOrdinarySobolev.field_directional_inner {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (A B : EulerLpTranslation.SmoothL2Field V) (v : EulerSmoothLimit.Space) : inner ℝ (A.directionalField v).toLp B.toLp = -inner ℝ A.toLp (B.directionalField v).toLp

theorem EulerOrdinarySobolev.field_zero_of_toLp_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (A : EulerLpTranslation.SmoothL2Field V) (h : A.toLp = 0) : A.field = 0

theorem EulerOrdinarySobolev.field_zero_of_derivative_zero (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hD : ∀ (x : EulerSmoothLimit.Space), fderiv ℝ A.field x = 0) : A.field = 0

theorem EulerOrdinarySobolev.field_zero_of_laplacian_zero (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hΔ : ∀ (x : EulerSmoothLimit.Space), Laplacian.laplacian A.field x = 0) : A.field = 0