Exact linear harmonic residual

Every differential operator uses an actual Fréchet derivative. The coefficient field supplied to the linearization is arbitrary, so the formula also applies to a curl-corrected coefficient without replacing it by its tangent principal part. The angular direction is unscaled.

noncomputable def NavierStokes.LinearWaveResidual.timeDirection {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (ε : ℝ) (Vf Vs : E → E) (x : E) : E

Time direction, given by Vf x - ε • Vs x.

Equations

• NavierStokes.LinearWaveResidual.timeDirection ε Vf Vs x = Vf x - ε • Vs x

theorem NavierStokes.LinearWaveResidual.along_timeDirection {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (ε : ℝ) (Vf Vs : E → E) (f : E → ℂ) (x : E) : HarmonicCalculus.along (timeDirection ε Vf Vs) f x = HarmonicCalculus.along Vf f x - ↑ε * HarmonicCalculus.along Vs f x

theorem NavierStokes.LinearWaveResidual.along_mul_real {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : E → E) {f g : E → ℝ} {x : E} (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) : HarmonicCalculus.along V (fun (y : E) => f y * g y) x = HarmonicCalculus.along V f x * g x + f x * HarmonicCalculus.along V g x

noncomputable def NavierStokes.LinearWaveResidual.base {E : Type u_1} (R b F G : E → ℝ) (x : E) : Fin 3 → ℝ

The real base components, with angular velocity V=R F.

Equations

• NavierStokes.LinearWaveResidual.base R b F G x = ![b x, R x * F x, G x]

noncomputable def NavierStokes.LinearWaveResidual.complexBase {E : Type u_1} (R b F G : E → ℝ) (x : E) : HarmonicCalculus.ComplexVector

Complex base, defined pointwise by (base R b F G x i : ℂ).

Equations

• NavierStokes.LinearWaveResidual.complexBase R b F G x i = ↑(NavierStokes.LinearWaveResidual.base R b F G x i)

noncomputable def NavierStokes.LinearWaveResidual.transport {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R : E → ℝ) (Vr Vθ Vz : E → E) (u v : E → HarmonicCalculus.ComplexVector) (x : E) : HarmonicCalculus.ComplexVector

Cylindrical bilinear advection, including the derivative of the frame.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.LinearWaveResidual.gradient {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R : E → ℝ) (Vr Vθ Vz : E → E) (p : E → ℂ) (x : E) : HarmonicCalculus.ComplexVector

Gradient, given by ![along Vr p x, (R x)⁻¹ • along Vθ p x, along Vz p x].

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.LinearWaveResidual.linearResidual {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (ε : ℝ) (R : E → ℝ) (Vr Vθ Vz Vt : E → E) (B a : E → HarmonicCalculus.ComplexVector) (p : E → ℂ) (x : E) : HarmonicCalculus.ComplexVector

The genuine differential linearization with viscosity ε.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.LinearWaveResidual.shear {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R F G : E → ℝ) (Vr : E → E) (a : E → HarmonicCalculus.ComplexVector) (x : E) : HarmonicCalculus.ComplexVector

Matrix K from (27), with its radial coefficients actually differentiated.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.LinearWaveResidual.baseDerivativeRemainder {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R b F G : E → ℝ) (Vr Vz : E → E) (a : E → HarmonicCalculus.ComplexVector) (x : E) : HarmonicCalculus.ComplexVector

The base derivative and radial-flow connection terms outside K.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.LinearWaveResidual.materialPhaseDefect {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (_R b F G : E → ℝ) (Vr Vθ Vz Vt : E → E) (Φ : E → ℝ) (x : E) : ℝ

Material phase defect, given by along Vt Φ x + b x * along Vr Φ x + F x * along Vθ Φ x + G x * along Vz Φ x.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.LinearWaveResidual.slowTransport {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (ε : ℝ) (b G : E → ℝ) (Vs Vr Vz : E → E) (a : E → HarmonicCalculus.ComplexVector) (x : E) : HarmonicCalculus.ComplexVector

Slow transport, defined pointwise by -(ε : ℂ) * along Vs (fun y => a y i) x + (b x : ℂ) * along Vr (fun y => a y i) x + (G x : ℂ) * along Vz (fun y => a y i) x.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.LinearWaveResidual.strippedPressureGradient {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (Vr Vz : E → E) (p : E → ℂ) (x : E) : HarmonicCalculus.ComplexVector

Stripped pressure gradient, given by ![along Vr p x, 0, along Vz p x].

Equations

• NavierStokes.LinearWaveResidual.strippedPressureGradient Vr Vz p x = ![NavierStokes.HarmonicCalculus.along Vr p x, 0, NavierStokes.HarmonicCalculus.along Vz p x]

noncomputable def NavierStokes.LinearWaveResidual.viscousRemainder {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R : E → ℝ) (Vr Vθ Vz : E → E) (κ : ℝ) (Φ : E → ℝ) (a : E → HarmonicCalculus.ComplexVector) (x : E) : HarmonicCalculus.ComplexVector

The complete viscous braces in (31), after removal of phase-square damping.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.LinearWaveResidual.principal {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (ε κ : ℝ) (R F G : E → ℝ) (Vr Vθ Vz Vf : E → E) (Φ : E → ℝ) (a : E → HarmonicCalculus.ComplexVector) (p : E → ℂ) (x : E) : HarmonicCalculus.ComplexVector

Principal as an element of ComplexVector.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.LinearWaveResidual.remainder {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (ε κ : ℝ) (R b F G : E → ℝ) (Vr Vθ Vz Vf Vs : E → E) (Φ : E → ℝ) (a : E → HarmonicCalculus.ComplexVector) (p : E → ℂ) (x : E) : HarmonicCalculus.ComplexVector

Remainder as an element of ComplexVector.

Equations

• One or more equations did not get rendered due to their size.

theorem NavierStokes.LinearWaveResidual.differentiableAt_base {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {R b F G : E → ℝ} {x : E} (hR : DifferentiableAt ℝ R x) (hb : DifferentiableAt ℝ b x) (hF : DifferentiableAt ℝ F x) (hG : DifferentiableAt ℝ G x) (i : Fin 3) : DifferentiableAt ℝ (fun (y : E) => base R b F G y i) x

theorem NavierStokes.LinearWaveResidual.along_complexBase {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : E → E) {R b F G : E → ℝ} {x : E} (hR : DifferentiableAt ℝ R x) (hb : DifferentiableAt ℝ b x) (hF : DifferentiableAt ℝ F x) (hG : DifferentiableAt ℝ G x) (i : Fin 3) : HarmonicCalculus.along V (fun (y : E) => complexBase R b F G y i) x = ↑(HarmonicCalculus.along V (fun (y : E) => base R b F G y i) x)

theorem NavierStokes.LinearWaveResidual.gradient_mode {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R : E → ℝ) (Vr Vθ Vz : E → E) (κ : ℝ) {Φ : E → ℝ} {p : E → ℂ} {x : E} (hΦ : DifferentiableAt ℝ Φ x) (hp : DifferentiableAt ℝ p x) (hpθ : HarmonicCalculus.along Vθ p x = 0) : gradient R Vr Vθ Vz (HarmonicCalculus.mode κ Φ p) x = fun (i : Fin 3) => (strippedPressureGradient Vr Vz p x i + HarmonicCalculus.phaseFactor κ * ↑((HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ x).ofLp i) * p x) * HarmonicCalculus.carrier κ Φ x

theorem NavierStokes.LinearWaveResidual.linearAdvection_mode {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R b F G : E → ℝ) (Vr Vθ Vz : E → E) (κ : ℝ) {Φ : E → ℝ} {a : E → HarmonicCalculus.ComplexVector} {x : E} (hR : DifferentiableAt ℝ R x) (hb : DifferentiableAt ℝ b x) (hF : DifferentiableAt ℝ F x) (hG : DifferentiableAt ℝ G x) (hRx : R x ≠ 0) (hDr : HarmonicCalculus.along Vr R x = 1) (hBθ : ∀ (i : Fin 3), HarmonicCalculus.along Vθ (fun (y : E) => base R b F G y i) x = 0) (hΦ : DifferentiableAt ℝ Φ x) (ha : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : E) => a y i) x) (haθ : ∀ (i : Fin 3), HarmonicCalculus.along Vθ (fun (y : E) => a y i) x = 0) : (fun (i : Fin 3) => transport R Vr Vθ Vz (complexBase R b F G) (HarmonicCalculus.vectorMode κ Φ a) x i + transport R Vr Vθ Vz (HarmonicCalculus.vectorMode κ Φ a) (complexBase R b F G) x i) = fun (i : Fin 3) => (↑(b x) * HarmonicCalculus.along Vr (fun (y : E) => a y i) x + ↑(G x) * HarmonicCalculus.along Vz (fun (y : E) => a y i) x + shear R F G Vr a x i + baseDerivativeRemainder R b F G Vr Vz a x i + HarmonicCalculus.phaseFactor κ * ↑(b x * HarmonicCalculus.along Vr Φ x + F x * HarmonicCalculus.along Vθ Φ x + G x * HarmonicCalculus.along Vz Φ x) * a x i) * HarmonicCalculus.carrier κ Φ x

The two linear advection terms produce K and exactly the displayed base-derivative and radial-flow connection terms.

theorem NavierStokes.LinearWaveResidual.vectorLaplacian_mode_split {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set E} (R : E → ℝ) {Vr Vθ Vz : E → E} (κ : ℝ) {Φ : E → ℝ} {a : E → HarmonicCalculus.ComplexVector} {pθ : ℝ} {x : E} (hU : IsOpen U) (hr : ContDiffOn ℝ (↑⊤) Vr U) (hθ : ContDiffOn ℝ (↑⊤) Vθ U) (hz : ContDiffOn ℝ (↑⊤) Vz U) (hΦ : ContDiffOn ℝ (↑⊤) Φ U) (ha : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : E) => a y i) U) (haθ : ∀ (i : Fin 3), Set.EqOn (HarmonicCalculus.along Vθ fun (y : E) => a y i) (fun (x : E) => 0) U) (hΦθ : Set.EqOn (HarmonicCalculus.along Vθ Φ) (fun (x : E) => pθ) U) (hx : x ∈ U) : HarmonicCalculus.cylindricalVectorLaplacian R Vr Vθ Vz (HarmonicCalculus.vectorMode κ Φ a) x = fun (i : Fin 3) => (viscousRemainder R Vr Vθ Vz κ Φ a x i - ↑κ ^ 2 * ↑(‖HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ x‖ ^ 2) * a x i) * HarmonicCalculus.carrier κ Φ x

The scalar and frame Laplacian identities assembled into the viscous braces of (31), with the phase-square term separated.

theorem NavierStokes.LinearWaveResidual.linearResidual_mode_split {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set E} (ε κ : ℝ) (R b F G : E → ℝ) {Vr Vθ Vz : E → E} (Vf Vs : E → E) {Φ : E → ℝ} {a : E → HarmonicCalculus.ComplexVector} {p : E → ℂ} {pθ : ℝ} {x : E} (hU : IsOpen U) (hr : ContDiffOn ℝ (↑⊤) Vr U) (hθ : ContDiffOn ℝ (↑⊤) Vθ U) (hz : ContDiffOn ℝ (↑⊤) Vz U) (hΦ : ContDiffOn ℝ (↑⊤) Φ U) (ha : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : E) => a y i) U) (hR : DifferentiableAt ℝ R x) (hb : DifferentiableAt ℝ b x) (hF : DifferentiableAt ℝ F x) (hG : DifferentiableAt ℝ G x) (hRx : R x ≠ 0) (hDr : HarmonicCalculus.along Vr R x = 1) (hBθ : ∀ (i : Fin 3), HarmonicCalculus.along Vθ (fun (y : E) => base R b F G y i) x = 0) (haθ : ∀ (i : Fin 3), Set.EqOn (HarmonicCalculus.along Vθ fun (y : E) => a y i) (fun (x : E) => 0) U) (hΦθ : Set.EqOn (HarmonicCalculus.along Vθ Φ) (fun (x : E) => pθ) U) (hp : DifferentiableAt ℝ p x) (hpθ : HarmonicCalculus.along Vθ p x = 0) (hx : x ∈ U) : linearResidual ε R Vr Vθ Vz (timeDirection ε Vf Vs) (complexBase R b F G) (HarmonicCalculus.vectorMode κ Φ a) (HarmonicCalculus.mode κ Φ p) x = fun (i : Fin 3) => (principal ε κ R F G Vr Vθ Vz Vf Φ a p x i + remainder ε κ R b F G Vr Vθ Vz Vf Vs Φ a p x i) * HarmonicCalculus.carrier κ Φ x

Full identity (31) for the actual amplitude supplied to the linear operator. The principal and remainder are both explicitly defined above.

Actual slot phase and projected pressure

theorem NavierStokes.LinearWaveResidual.along_scaled_direction {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (c : ℝ) (V : E → E) (f : E → ℂ) (x : E) : HarmonicCalculus.along (fun (y : E) => c • V y) f x = ↑c * HarmonicCalculus.along V f x

Scaling a prescribed fast direction produces exactly the manuscript's prefactor, for example c = Q^(1+h) multiplying Nabs.

theorem NavierStokes.LinearWaveResidual.materialPhaseDefect_slot (ε p pz x₀ : ℝ) (b F G : PhaseCalculus.Slow → ℝ) (q : PhaseCalculus.Slot) (hR : q.1.1 ≠ 0) : materialPhaseDefect (fun (y : PhaseCalculus.Slot) => y.1.1) (fun (y : PhaseCalculus.Slot) => b y.1) (fun (y : PhaseCalculus.Slot) => F y.1) (fun (y : PhaseCalculus.Slot) => G y.1) (fun (x : PhaseCalculus.Slot) => PhaseCalculus.eR) (fun (x : PhaseCalculus.Slot) => PhaseCalculus.eTheta) (fun (x : PhaseCalculus.Slot) => ε • PhaseCalculus.eZ) (timeDirection ε (fun (x : PhaseCalculus.Slot) => PhaseCalculus.eV) fun (x : PhaseCalculus.Slot) => PhaseCalculus.eT) (PhaseCalculus.phase ε p pz x₀ F G) q = PhaseCalculus.backwardMaterialOp ε b F G (PhaseCalculus.phase ε p pz x₀ F G) q

The material defect used in the residual is the actual backward-time material derivative already computed in PhaseCalculus.

theorem NavierStokes.LinearWaveResidual.materialPhaseDefect_slot_formula (ε p pz x₀ : ℝ) (b F G : PhaseCalculus.Slow → ℝ) (q : PhaseCalculus.Slot) (hε : ε ≠ 0) (hR : 0 < q.1.1) (hF : DifferentiableAt ℝ F q.1) (hG : DifferentiableAt ℝ G q.1) : materialPhaseDefect (fun (y : PhaseCalculus.Slot) => y.1.1) (fun (y : PhaseCalculus.Slot) => b y.1) (fun (y : PhaseCalculus.Slot) => F y.1) (fun (y : PhaseCalculus.Slot) => G y.1) (fun (x : PhaseCalculus.Slot) => PhaseCalculus.eR) (fun (x : PhaseCalculus.Slot) => PhaseCalculus.eTheta) (fun (x : PhaseCalculus.Slot) => ε • PhaseCalculus.eZ) (timeDirection ε (fun (x : PhaseCalculus.Slot) => PhaseCalculus.eV) fun (x : PhaseCalculus.Slot) => PhaseCalculus.eT) (PhaseCalculus.phase ε p pz x₀ F G) q = b q.1 * x₀ - q.2.2 * (b q.1 * (p * PhaseCalculus.slowR F q.1 + pz * PhaseCalculus.slowR G q.1) - ε * (p * PhaseCalculus.slowT F q.1 + pz * PhaseCalculus.slowT G q.1) + ε * G q.1 * (p * PhaseCalculus.slowZ F q.1 + pz * PhaseCalculus.slowZ G q.1))

Explicit formula for the phase material defect, including the sign of the slow-time term. No estimate for this term is assumed.

theorem NavierStokes.LinearWaveResidual.slot_base_derivative (f : PhaseCalculus.Slow → ℝ) (q w : PhaseCalculus.Slot) (hf : DifferentiableAt ℝ f q.1) : HarmonicCalculus.along (fun (x : PhaseCalculus.Slot) => w) (fun (y : PhaseCalculus.Slot) => f y.1) q = (fderiv ℝ f q.1) w.1

A base coefficient depending only on slow coordinates has precisely the slow differential along a slot direction.

theorem NavierStokes.LinearWaveResidual.slot_base_radial (f : PhaseCalculus.Slow → ℝ) (q : PhaseCalculus.Slot) (hf : DifferentiableAt ℝ f q.1) : HarmonicCalculus.along (fun (x : PhaseCalculus.Slot) => PhaseCalculus.eR) (fun (y : PhaseCalculus.Slot) => f y.1) q = PhaseCalculus.slowR f q.1

theorem NavierStokes.LinearWaveResidual.slot_base_angular (f : PhaseCalculus.Slow → ℝ) (q : PhaseCalculus.Slot) (hf : DifferentiableAt ℝ f q.1) : HarmonicCalculus.along (fun (x : PhaseCalculus.Slot) => PhaseCalculus.eTheta) (fun (y : PhaseCalculus.Slot) => f y.1) q = 0

noncomputable def NavierStokes.LinearWaveResidual.projectionNumerator {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (Vf : E → E) (n : E → EuclideanSpace ℝ (Fin 3)) (a Ka f : E → HarmonicCalculus.ComplexVector) (x : E) : ℂ

Numerator in the pressure from the projected equation. The derivative of n is the actual derivative in the fast direction.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.LinearWaveResidual.projectedPressure {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (κ : ℝ) (Vf : E → E) (n : E → EuclideanSpace ℝ (Fin 3)) (a Ka f : E → HarmonicCalculus.ComplexVector) (x : E) : ℂ

Projected pressure, given by (Complex.I / (κ : ℂ)) * projectionNumerator Vf n a Ka f x / Complex.ofReal (‖n x‖ ^ 2).

Equations

• NavierStokes.LinearWaveResidual.projectedPressure κ Vf n a Ka f x = Complex.I / ↑κ * NavierStokes.LinearWaveResidual.projectionNumerator Vf n a Ka f x / ↑(‖n x‖ ^ 2)

theorem NavierStokes.LinearWaveResidual.projectedPressure_force {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (κ : ℝ) (Vf : E → E) (n : E → EuclideanSpace ℝ (Fin 3)) (a Ka f : E → HarmonicCalculus.ComplexVector) (x : E) (hκ : κ ≠ 0) (i : Fin 3) : HarmonicCalculus.phaseFactor κ * ↑((n x).ofLp i) * projectedPressure κ Vf n a Ka f x = -↑((n x).ofLp i) * projectionNumerator Vf n a Ka f x / ↑(‖n x‖ ^ 2)

theorem NavierStokes.LinearWaveResidual.principal_projectedPressure {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (ε κ : ℝ) (R F G : E → ℝ) (Vr Vθ Vz Vf : E → E) (Φ : E → ℝ) (a f : E → HarmonicCalculus.ComplexVector) (x : E) (hκ : κ ≠ 0) : principal ε κ R F G Vr Vθ Vz Vf Φ a (projectedPressure κ Vf (HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ) a (shear R F G Vr a) f) x = fun (i : Fin 3) => HarmonicCalculus.along Vf (fun (y : E) => a y i) x + shear R F G Vr a x i + ↑(ε * κ ^ 2 * ‖HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ x‖ ^ 2) * a x i - ↑((HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ x).ofLp i) * projectionNumerator Vf (HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ) a (shear R F G Vr a) f x / ↑(‖HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ x‖ ^ 2)

Substituting the projected pressure into the principal part is an exact identity for arbitrary amplitudes; no tangent ODE is imposed on the actual coefficient supplied to the residual.

theorem NavierStokes.LinearWaveResidual.contDiffOn_normalDot {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set E} {n : E → EuclideanSpace ℝ (Fin 3)} {a : E → HarmonicCalculus.ComplexVector} (hn : ContDiffOn ℝ (↑⊤) n U) (ha : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : E) => a y i) U) : ContDiffOn ℝ (↑⊤) (fun (y : E) => HarmonicCalculus.normalDot (n y) (a y)) U

theorem NavierStokes.LinearWaveResidual.contDiffOn_projectedPressure {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set E} (κ : ℝ) {Vf : E → E} {n : E → EuclideanSpace ℝ (Fin 3)} {a Ka f : E → HarmonicCalculus.ComplexVector} (hU : IsOpen U) (hVf : ContDiffOn ℝ (↑⊤) Vf U) (hn : ContDiffOn ℝ (↑⊤) n U) (hn₀ : ∀ x ∈ U, n x ≠ 0) (ha : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : E) => a y i) U) (hKa : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : E) => Ka y i) U) (hf : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : E) => f y i) U) : ContDiffOn ℝ (↑⊤) (projectedPressure κ Vf n a Ka f) U

Real-linear transfer of the complex calculation

theorem NavierStokes.LinearWaveResidual.along_map {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F₁ : Type u_2} {F₂ : Type u_3} [NormedAddCommGroup F₁] [NormedSpace ℝ F₁] [NormedAddCommGroup F₂] [NormedSpace ℝ F₂] (L : F₁ →L[ℝ] F₂) (V : E → E) {f : E → F₁} {x : E} (hf : DifferentiableAt ℝ f x) : HarmonicCalculus.along V (fun (y : E) => L (f y)) x = L (HarmonicCalculus.along V f x)

theorem NavierStokes.LinearWaveResidual.along_along_map {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F₁ : Type u_2} {F₂ : Type u_3} [NormedAddCommGroup F₁] [NormedSpace ℝ F₁] [NormedAddCommGroup F₂] [NormedSpace ℝ F₂] (L : F₁ →L[ℝ] F₂) {U : Set E} {V : E → E} {f : E → F₁} {x : E} (hU : IsOpen U) (hV : ContDiffOn ℝ (↑⊤) V U) (hf : ContDiffOn ℝ (↑⊤) f U) (hx : x ∈ U) : HarmonicCalculus.along V (HarmonicCalculus.along V fun (y : E) => L (f y)) x = L (HarmonicCalculus.along V (HarmonicCalculus.along V f) x)

theorem NavierStokes.LinearWaveResidual.cylindricalLaplacian_map {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F₁ : Type u_2} {F₂ : Type u_3} [NormedAddCommGroup F₁] [NormedSpace ℝ F₁] [NormedAddCommGroup F₂] [NormedSpace ℝ F₂] (L : F₁ →L[ℝ] F₂) {U : Set E} (R : E → ℝ) {Vr Vθ Vz : E → E} {f : E → F₁} {x : E} (hU : IsOpen U) (hr : ContDiffOn ℝ (↑⊤) Vr U) (hθ : ContDiffOn ℝ (↑⊤) Vθ U) (hz : ContDiffOn ℝ (↑⊤) Vz U) (hf : ContDiffOn ℝ (↑⊤) f U) (hx : x ∈ U) : HarmonicCalculus.cylindricalLaplacian R Vr Vθ Vz (fun (y : E) => L (f y)) x = L (HarmonicCalculus.cylindricalLaplacian R Vr Vθ Vz f x)

noncomputable def NavierStokes.LinearWaveResidual.realLift {E : Type u_1} (a : E → Fin 3 → ℝ) (x : E) : HarmonicCalculus.ComplexVector

Real lift, defined pointwise by (a x i : ℂ).

Equations

• NavierStokes.LinearWaveResidual.realLift a x i = ↑(a x i)

noncomputable def NavierStokes.LinearWaveResidual.realAngularGenerator (a : Fin 3 → ℝ) : Fin 3 → ℝ

Real angular generator, given by ![-a 1, a 0, 0].

Equations

• NavierStokes.LinearWaveResidual.realAngularGenerator a = ![-a 1, a 0, 0]

noncomputable def NavierStokes.LinearWaveResidual.realTransport {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R : E → ℝ) (Vr Vθ Vz : E → E) (u v : E → Fin 3 → ℝ) (x : E) : Fin 3 → ℝ

Real transport as an element of Fin 3 → ℝ.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.LinearWaveResidual.realFrameLaplacian {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R : E → ℝ) (Vr Vθ Vz : E → E) (a : E → Fin 3 → ℝ) (x : E) : Fin 3 → ℝ

Real frame laplacian as an element of Fin 3 → ℝ.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.LinearWaveResidual.realComponentLinearResidual {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (ε : ℝ) (R : E → ℝ) (Vr Vθ Vz Vt : E → E) (B a : E → Fin 3 → ℝ) (p : E → ℝ) (x : E) : Fin 3 → ℝ

Real component form of the same differential linearization.

Equations

• One or more equations did not get rendered due to their size.

theorem NavierStokes.LinearWaveResidual.map_ofReal_mul (L : ℂ →L[ℝ] ℝ) (r : ℝ) (z : ℂ) : L (↑r * z) = r * L z

theorem NavierStokes.LinearWaveResidual.map_mul_ofReal (L : ℂ →L[ℝ] ℝ) (r : ℝ) (z : ℂ) : L (z * ↑r) = L z * r

theorem NavierStokes.LinearWaveResidual.map_div_ofReal (L : ℂ →L[ℝ] ℝ) (r : ℝ) (z : ℂ) : L (z / ↑r) = L z / r

theorem NavierStokes.LinearWaveResidual.map_two_mul (L : ℂ →L[ℝ] ℝ) (z : ℂ) : L (2 * z) = 2 * L z

theorem NavierStokes.LinearWaveResidual.realMap_linearResidual {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set E} (L : ℂ →L[ℝ] ℝ) (ε : ℝ) (R : E → ℝ) {Vr Vθ Vz : E → E} (Vt : E → E) {B : E → Fin 3 → ℝ} {a : E → HarmonicCalculus.ComplexVector} {p : E → ℂ} {x : E} (hU : IsOpen U) (hr : ContDiffOn ℝ (↑⊤) Vr U) (hθ : ContDiffOn ℝ (↑⊤) Vθ U) (hz : ContDiffOn ℝ (↑⊤) Vz U) (ha : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : E) => a y i) U) (hB : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : E) => B y i) x) (hp : DifferentiableAt ℝ p x) (hx : x ∈ U) : (fun (i : Fin 3) => L (linearResidual ε R Vr Vθ Vz Vt (realLift B) a p x i)) = realComponentLinearResidual ε R Vr Vθ Vz Vt B (fun (y : E) (i : Fin 3) => L (a y i)) (fun (y : E) => L (p y)) x

The complex linearization transfers through any real continuous linear functional, in particular real and imaginary parts, because its base is real.

The actual Cartesian and cylindrical linearizations

noncomputable def NavierStokes.LinearWaveResidual.bilinearAdvection (u v : ProblemStatement.Space → ProblemStatement.Space) (q : ProblemStatement.Space) : ProblemStatement.Space

Bilinear advection, constructed using u.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.LinearWaveResidual.cylindricalLinearResidual (ε : ℝ) (B a : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) (t : ℝ) (q : ProblemStatement.Space) : ProblemStatement.Space

Cylindrical linear residual, constructed using temporalDerivative.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.LinearWaveResidual.cartesianLinearResidual (ε : ℝ) (B a : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) (t : ℝ) (x : ProblemStatement.Space) : ProblemStatement.Space

Linearization in the original Cartesian derivative definitions.

Equations

• One or more equations did not get rendered due to their size.

theorem NavierStokes.LinearWaveResidual.cartesianBilinearAdvection_components {u v : ProblemStatement.Space → ProblemStatement.Space} {q : ProblemStatement.Space} (hv : DifferentiableAt ℝ v (CylindricalResidual.chart q)) (hr : q.ofLp 0 ≠ 0) : (fderiv ℝ v (CylindricalResidual.chart q)) (u (CylindricalResidual.chart q)) = (CylindricalResidual.frame (q.ofLp 1)) (bilinearAdvection (CylindricalResidual.components u) (CylindricalResidual.components v) q)

theorem NavierStokes.LinearWaveResidual.cartesianLinearResidual_cylindrical (ε : ℝ) {B a : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} {t : ℝ} {q : ProblemStatement.Space} (ha : ContDiffAt ℝ 2 a (t, CylindricalResidual.chart q)) (hB : DifferentiableAt ℝ B (t, CylindricalResidual.chart q)) (hp : DifferentiableAt ℝ p (t, CylindricalResidual.chart q)) (hr : 0 < q.ofLp 0) : cartesianLinearResidual ε B a p t (CylindricalResidual.chart q) = (CylindricalResidual.frame (q.ofLp 1)) (cylindricalLinearResidual ε (CylindricalResidual.velocityComponents B) (CylindricalResidual.velocityComponents a) (CylindricalResidual.pressurePullback p) t q)

The real differential linearization is exactly conjugated by the cylindrical frame. Both cross-advections are derived from the actual Cartesian derivative, rather than from a postulated residual identity.

noncomputable def NavierStokes.LinearWaveResidual.spaceDirection (i : Fin 3) : ProblemStatement.SpaceTime → ProblemStatement.SpaceTime

Space direction, given by (0, coordinateVector i).

Equations

• NavierStokes.LinearWaveResidual.spaceDirection i x✝ = (0, NavierStokes.ProblemStatement.coordinateVector i)

noncomputable def NavierStokes.LinearWaveResidual.physicalTimeDirection : ProblemStatement.SpaceTime → ProblemStatement.SpaceTime

Physical time direction, given by (1, 0).

Equations

• NavierStokes.LinearWaveResidual.physicalTimeDirection x✝ = (1, 0)

noncomputable def NavierStokes.LinearWaveResidual.coordinateRadius (x : ProblemStatement.SpaceTime) : ℝ

Coordinate radius, given by x.2 0.

Equations

• NavierStokes.LinearWaveResidual.coordinateRadius x = x.2.ofLp 0

theorem NavierStokes.LinearWaveResidual.along_space_slice {W : Type u_2} [NormedAddCommGroup W] [NormedSpace ℝ W] {f : ProblemStatement.SpaceTime → W} {t : ℝ} {q : ProblemStatement.Space} (hf : DifferentiableAt ℝ f (t, q)) (i : Fin 3) : HarmonicCalculus.along (spaceDirection i) f (t, q) = CylindricalResidual.dCoord i (fun (y : ProblemStatement.Space) => f (t, y)) q

theorem NavierStokes.LinearWaveResidual.along_time_slice {W : Type u_2} [NormedAddCommGroup W] [NormedSpace ℝ W] {f : ProblemStatement.SpaceTime → W} {t : ℝ} {q : ProblemStatement.Space} (hf : DifferentiableAt ℝ f (t, q)) : HarmonicCalculus.along physicalTimeDirection f (t, q) = (fderiv ℝ (fun (s : ℝ) => f (s, q)) t) 1

theorem NavierStokes.LinearWaveResidual.along_space_space_slice {W : Type u_2} [NormedAddCommGroup W] [NormedSpace ℝ W] {U : Set ProblemStatement.SpaceTime} {f : ProblemStatement.SpaceTime → W} {t : ℝ} {q : ProblemStatement.Space} (hU : IsOpen U) (hf : ContDiffOn ℝ (↑⊤) f U) (hx : (t, q) ∈ U) (i : Fin 3) : HarmonicCalculus.along (spaceDirection i) (HarmonicCalculus.along (spaceDirection i) f) (t, q) = CylindricalResidual.dCoord i (CylindricalResidual.dCoord i fun (y : ProblemStatement.Space) => f (t, y)) q

theorem NavierStokes.LinearWaveResidual.laplacian_space_slice {W : Type u_2} [NormedAddCommGroup W] [NormedSpace ℝ W] {U : Set ProblemStatement.SpaceTime} {f : ProblemStatement.SpaceTime → W} {t : ℝ} {q : ProblemStatement.Space} (hU : IsOpen U) (hf : ContDiffOn ℝ (↑⊤) f U) (hx : (t, q) ∈ U) : HarmonicCalculus.cylindricalLaplacian coordinateRadius (spaceDirection 0) (spaceDirection 1) (spaceDirection 2) f (t, q) = CylindricalResidual.scalarLaplacian (fun (y : ProblemStatement.Space) => f (t, y)) q

theorem NavierStokes.LinearWaveResidual.realComponentLinearResidual_eq_cylindrical {U : Set ProblemStatement.SpaceTime} (ε : ℝ) {B a : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} {t : ℝ} {q : ProblemStatement.Space} (hU : IsOpen U) (hB : ContDiffOn ℝ (↑⊤) B U) (ha : ContDiffOn ℝ (↑⊤) a U) (hp : ContDiffOn ℝ (↑⊤) p U) (hx : (t, q) ∈ U) : realComponentLinearResidual ε coordinateRadius (spaceDirection 0) (spaceDirection 1) (spaceDirection 2) physicalTimeDirection (fun (z : ProblemStatement.SpaceTime) (i : Fin 3) => (B z).ofLp i) (fun (z : ProblemStatement.SpaceTime) (i : Fin 3) => (a z).ofLp i) p (t, q) = fun (i : Fin 3) => (cylindricalLinearResidual ε B a p t q).ofLp i

The generic real component operator used for the harmonic calculation is the actual cylindrical linearization when its directions are the physical spacetime coordinate directions.