Recovering the transverse normal residual

A residual annihilated by the adjoint of a frame spanning m⊥ is exactly its normal component. Applying this elementary Hilbert-space fact to the proved projected coordinate equation gives the pressure coefficient in equation (11).

noncomputable def EulerTransverseNormalResidual.normalCoefficient {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (m r : E) : ℝ

The literal scalar normal component, with the source denominator D_m.

Equations

• EulerTransverseNormalResidual.normalCoefficient m r = inner ℝ m r / ‖m‖ ^ 2

theorem EulerTransverseNormalResidual.eq_normal_of_tangent_orthogonal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (m r : E) (hm : m ≠ 0) (hr : ∀ (x : E), inner ℝ m x = 0 → inner ℝ r x = 0) : r = normalCoefficient m r • m

Orthogonality to the tangent hyperplane determines the normal component.

theorem EulerTransverseNormalResidual.eq_normal_of_adjoint_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {U : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [CompleteSpace E] (Q : U →L[ℝ] E) (m r : E) (hm : m ≠ 0) (hRange : ∀ (η : E), inner ℝ m η = 0 → ∃ (x : U), Q x = η) (hr : (ContinuousLinearMap.adjoint Q) r = 0) : r = normalCoefficient m r • m

A frame spanning the tangent hyperplane detects exactly the normal residual.

theorem EulerTransverseNormalResidual.physical_velocity_balance {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {U : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [CompleteSpace E] (Q Q₁ : U →L[ℝ] E) (M : E →L[ℝ] E) (m : E) (hm : m ≠ 0) (hTangent : ∀ (x : U), inner ℝ m (Q x) = 0) (hRange : ∀ (η : E), inner ℝ m η = 0 → ∃ (x : U), Q x = η) (hflow : Q₁ = M ∘SL Q) (v a : U) (f : E) (heq : (EulerTransverseGramInverse.gram Q) a = (ContinuousLinearMap.adjoint Q) (f - 2 • Q₁ v)) : Q₁ v + Q a + M (Q v) + ((inner ℝ m f - 2 * inner ℝ m (M (Q v))) / ‖m‖ ^ 2) • m = f

Equation (10), together with Q_t = M Q, gives the exact source pressure coefficient and velocity equation (11). No pressure residual is assumed.