Research proof index

The conservative and convective Cauchy momentum equations are equivalent when the classical continuity equation holds. The differentiability assumptions are exactly the product-rule assumptions used to rewrite partial_t (rho u) and matrixDiv (rho u ⊗ u).

The matrix divergence of rho u ⊗ u split into continuity and convective parts.

The conservative momentum transport terms equal mass density times material acceleration plus the continuity residual times velocity.

Product rule for one spatial derivative of one component of rho u ⊗ u.

Product rule for the time derivative of a scalar field times a velocity field.

The unbounded momentum operator, whose domain is Schwartz maps. -/ def momentumOperatorUnbounded : UnboundedOperator schwartzIncl schwartzIncl_injective := UnboundedOperator.ofSelfCLM momentumOperatorSchwartz /-! ## Generalized eigenvectors of the momentum operator -/ lemma planeWaveFunctional_generalized_eigenvector_momentumOperatorUnbounded (k : ℝ) : mo...