Tangent projection and pressure cancellation

This file checks the algebra in manuscript Lemma 8.4, equation (27), and Appendix A.3. The vectors are in an arbitrary real inner-product space; Kt denotes the value of the matrix K on t. No assertion about the existence, size, or differentiated estimates of a pulse is made here.

noncomputable def NavierStokes.TangentProjection.tangentProj {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (n f : E) : E

Orthogonal projection onto the hyperplane perpendicular to n, for n ≠ 0.

Equations

• NavierStokes.TangentProjection.tangentProj n f = f - (inner ℝ n f / inner ℝ n n) • n

noncomputable def NavierStokes.TangentProjection.projectedRhs {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (n n' t Kt f : E) (δ : ℝ) : E

The right-hand side of equation (27), with the viscous coefficient δ.

Equations

• NavierStokes.TangentProjection.projectedRhs n n' t Kt f δ = -Kt + ((inner ℝ n Kt - inner ℝ n' t) / inner ℝ n n) • n - δ • t - NavierStokes.TangentProjection.tangentProj n f

noncomputable def NavierStokes.TangentProjection.pressureCoefficient {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (n n' t Kt f : E) : ℝ

The real coefficient of the normal vector canceled by pressure.

Equations

• NavierStokes.TangentProjection.pressureCoefficient n n' t Kt f = (inner ℝ n Kt - inner ℝ n' t + inner ℝ n f) / inner ℝ n n

theorem NavierStokes.TangentProjection.tangentProj_normal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : E} (hn : n ≠ 0) (f : E) : inner ℝ n (tangentProj n f) = 0

theorem NavierStokes.TangentProjection.tangentProj_of_tangent {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (n f : E) (hf : inner ℝ n f = 0) : tangentProj n f = f

theorem NavierStokes.TangentProjection.tangentProj_idempotent {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : E} (hn : n ≠ 0) (f : E) : tangentProj n (tangentProj n f) = tangentProj n f

theorem NavierStokes.TangentProjection.normal_projectedRhs {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : E} (hn : n ≠ 0) (n' t Kt f : E) (δ : ℝ) : inner ℝ n (projectedRhs n n' t Kt f δ) = -inner ℝ n' t - δ * inner ℝ n t

The full normal identity includes the damping of an existing tangency defect.

theorem NavierStokes.TangentProjection.normal_projectedRhs_of_tangent {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : E} (hn : n ≠ 0) (n' t Kt f : E) (δ : ℝ) (ht : inner ℝ n t = 0) : inner ℝ n (projectedRhs n n' t Kt f δ) = -inner ℝ n' t

In particular the projected vector field has the normal derivative required by tangency.

theorem NavierStokes.TangentProjection.projected_balance {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (n n' t Kt f : E) (δ : ℝ) : projectedRhs n n' t Kt f δ + Kt + δ • t + f = pressureCoefficient n n' t Kt f • n

Rearranging the projected equation leaves exactly this normal vector.

theorem NavierStokes.TangentProjection.pressure_cancellation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (n n' t Kt f : E) (δ : ℝ) : projectedRhs n n' t Kt f δ + Kt + δ • t - pressureCoefficient n n' t Kt f • n = -f

A pressure force with the opposite normal coefficient cancels the residual exactly.

theorem NavierStokes.TangentProjection.differentiated_tangency {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n t : ℝ → E} {n' t' : E} {x : ℝ} (hn : HasDerivAt n n' x) (ht : HasDerivAt t t' x) (htangent : ∀ (y : ℝ), inner ℝ (n y) (t y) = 0) : inner ℝ (n x) t' = -inner ℝ n' (t x)

Actual differentiation of tangency gives the normal derivative in Appendix A.3.

theorem NavierStokes.TangentProjection.tangency_defect_derivative {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n t : ℝ → E} {n' : E} {x : ℝ} {Kt f : E} {δ : ℝ} (hn0 : n x ≠ 0) (hn : HasDerivAt n n' x) (ht : HasDerivAt t (projectedRhs (n x) n' (t x) Kt f δ) x) : HasDerivAt (fun (y : ℝ) => inner ℝ (n y) (t y)) (-δ * inner ℝ (n x) (t x)) x

Along any differentiable solution of (27), the tangency defect solves h' = -δ h.

theorem NavierStokes.TangentProjection.scalar_defect_zero (h δ D : ℝ → ℝ) (hD : ∀ (x : ℝ), HasDerivAt D (δ x) x) (hh : ∀ (x : ℝ), HasDerivAt h (-δ x * h x) x) (x₀ : ℝ) (hzero : h x₀ = 0) (x : ℝ) : h x = 0

Integrating-factor proof of zero-data uniqueness for the scalar defect equation. The primitive D is explicit, so no existence assumption is hidden in this statement.

theorem NavierStokes.TangentProjection.tangency_preserved {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (n n' t Kt f : ℝ → E) (δ D : ℝ → ℝ) (hn0 : ∀ (x : ℝ), n x ≠ 0) (hn : ∀ (x : ℝ), HasDerivAt n (n' x) x) (ht : ∀ (x : ℝ), HasDerivAt t (projectedRhs (n x) (n' x) (t x) (Kt x) (f x) (δ x)) x) (hD : ∀ (x : ℝ), HasDerivAt D (δ x) x) (x₀ : ℝ) (hzero : inner ℝ (n x₀) (t x₀) = 0) (x : ℝ) : inner ℝ (n x) (t x) = 0

Initial tangency persists for a differentiable solution of the projected equation. This version is global in slot time and assumes an explicit primitive of the damping.

theorem NavierStokes.TangentProjection.viscous_coefficient_nonneg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (ε k j : ℝ) (n : E) (hε : 0 ≤ ε) : 0 ≤ ε * k ^ 2 * j ^ 2 * inner ℝ n n

Nonnegative viscosity gives a nonnegative scalar damping coefficient.

theorem NavierStokes.TangentProjection.damping_dissipative {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (δ : ℝ) (t : E) (hδ : 0 ≤ δ) : inner ℝ t (-δ • t) ≤ 0

The damping term has nonpositive contribution to the energy derivative.

theorem NavierStokes.TangentProjection.complex_pressure_sign (A c : ℂ) (hc : c ≠ 0) : Complex.I * c * (Complex.I * A / c) = -A

With c = k j' ≠ 0, the manuscript's pressure is i A / c. Multiplication by the Fourier gradient i c yields -A, fixing the sign.