Normal, clock and amplitude rescaling in the tangent equation

The normal scales by s, its clock derivative by s * rate, and the velocity amplitude by amp. The projected equation then scales by rate * amp, whereas the scalar pressure coefficient scales by rate * amp / s. These are identities of the actual operators, including the totalized zero-normal case.

theorem NavierStokes.NormalScaling.tangentProj_smul_normal {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (n f : H) {s : ℝ} (hs : s ≠ 0) : TangentProjection.tangentProj (s • n) f = TangentProjection.tangentProj n f

theorem NavierStokes.NormalScaling.tangentProj_smul_right {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (n f : H) (amp : ℝ) : TangentProjection.tangentProj n (amp • f) = amp • TangentProjection.tangentProj n f

theorem NavierStokes.NormalScaling.negativeTangentProjection_smul {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (n : H) {s : ℝ} (hs : s ≠ 0) : CommonCoverSolve.negativeTangentProjection (s • n) = CommonCoverSolve.negativeTangentProjection n

theorem NavierStokes.NormalScaling.pressureCoefficient_rescale {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (n nDot u Ku f : H) (rate amp : ℝ) {s : ℝ} (hs : s ≠ 0) : TangentProjection.pressureCoefficient (s • n) ((s * rate) • nDot) (amp • u) ((rate * amp) • Ku) ((rate * amp) • f) = rate * amp / s * TangentProjection.pressureCoefficient n nDot u Ku f

theorem NavierStokes.NormalScaling.projectedRhs_eq_pressure {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (n nDot u Ku f : H) (δ : ℝ) : TangentProjection.projectedRhs n nDot u Ku f δ = TangentProjection.pressureCoefficient n nDot u Ku f • n - (Ku + δ • u + f)

theorem NavierStokes.NormalScaling.projectedRhs_rescale {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (n nDot u Ku f : H) (rate amp δ : ℝ) {s : ℝ} (hs : s ≠ 0) : TangentProjection.projectedRhs (s • n) ((s * rate) • nDot) (amp • u) ((rate * amp) • Ku) ((rate * amp) • f) (rate * δ) = (rate * amp) • TangentProjection.projectedRhs n nDot u Ku f δ

theorem NavierStokes.NormalScaling.projectedOperator_rescale {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (n nDot : H) (K : H →L[ℝ] H) (rate δ : ℝ) {s : ℝ} (hs : s ≠ 0) : TangentODE.projectedOperator (s • n) ((s * rate) • nDot) (rate • K) (rate * δ) = rate • TangentODE.projectedOperator n nDot K δ