Naturality of the actual lifted residual coefficients

The hypotheses in this file concern the full free auxiliary-variable lift. Equality only on the physical graph is deliberately insufficient. The source is always the literal HarmonicResidual.residualBlock, including its real projection and its Gaussian and alias subtractions.

noncomputable def NavierStokes.PhysicalResidualNaturality.scalarEquiv (F : Type) [NormedAddCommGroup F] [NormedSpace ℝ F] (a : ℝ) (ha : a ≠ 0) : F ≃L[ℝ] F

Scalar multiplication by a nonzero real number, with its actual inverse.

Equations

• NavierStokes.PhysicalResidualNaturality.scalarEquiv F a ha = { toLinearEquiv := LinearEquiv.smulOfNeZero ℝ F a ha, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem NavierStokes.PhysicalResidualNaturality.scalarEquiv_apply {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] (a : ℝ) (ha : a ≠ 0) (x : F) : (scalarEquiv F a ha) x = a • x

theorem NavierStokes.PhysicalResidualNaturality.fderiv_scalar {D F : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup F] [NormedSpace ℝ F] (a : ℝ) (f : D → F) (x : D) : fderiv ℝ (fun (y : D) => a • f y) x = a • fderiv ℝ f x

This version also handles non-differentiable functions and the zero scalar.

theorem NavierStokes.PhysicalResidualNaturality.along_pull {D E F : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (e : D ≃L[ℝ] E) (a b : ℝ) (V : D → D) (W : E → E) (f : E → F) (x : D) (hV : e (V x) = b • W (e x)) : HarmonicCalculus.along V (fun (y : D) => a • f (e y)) x = (a * b) • HarmonicCalculus.along W f (e x)

def NavierStokes.PhysicalResidualNaturality.CoefficientsOn {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (U : Set D) (e : D ≃L[ℝ] E) (a : ℝ) (c : HarmonicFields.Coefficients D) (d : HarmonicFields.Coefficients E) : Prop

Equality of every coefficient on a full lifted open set, with one weight.

Equations

• NavierStokes.PhysicalResidualNaturality.CoefficientsOn U e a c d = ∀ (j : ℤ), ∀ x ∈ U, c.coeff j x = a • d.coeff j (e x)

theorem NavierStokes.PhysicalResidualNaturality.CoefficientsOn.reweight {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {a b : ℝ} {c : HarmonicFields.Coefficients D} {d : HarmonicFields.Coefficients E} (hc : CoefficientsOn U e a c d) (hab : a = b) : CoefficientsOn U e b c d

theorem NavierStokes.PhysicalResidualNaturality.CoefficientsOn.zero {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (U : Set D) (e : D ≃L[ℝ] E) (a : ℝ) : CoefficientsOn U e a 0 0

theorem NavierStokes.PhysicalResidualNaturality.CoefficientsOn.add {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {a : ℝ} {c₁ c₂ : HarmonicFields.Coefficients D} {d₁ d₂ : HarmonicFields.Coefficients E} (h₁ : CoefficientsOn U e a c₁ d₁) (h₂ : CoefficientsOn U e a c₂ d₂) : CoefficientsOn U e a (c₁ + c₂) (d₁ + d₂)

theorem NavierStokes.PhysicalResidualNaturality.CoefficientsOn.sub {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {a : ℝ} {c₁ c₂ : HarmonicFields.Coefficients D} {d₁ d₂ : HarmonicFields.Coefficients E} (h₁ : CoefficientsOn U e a c₁ d₁) (h₂ : CoefficientsOn U e a c₂ d₂) : CoefficientsOn U e a (c₁ - c₂) (d₁ - d₂)

theorem NavierStokes.PhysicalResidualNaturality.CoefficientsOn.neg {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {a : ℝ} {c : HarmonicFields.Coefficients D} {d : HarmonicFields.Coefficients E} (hc : CoefficientsOn U e a c d) : CoefficientsOn U e a (-c) (-d)

theorem NavierStokes.PhysicalResidualNaturality.CoefficientsOn.boundConstant {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {a : ℝ} {f : D → ℂ} {g : E → ℂ} (h : ∀ x ∈ U, f x = a • g (e x)) : CoefficientsOn U e a (HarmonicFields.constantCoefficient f) (HarmonicFields.constantCoefficient g)

theorem NavierStokes.PhysicalResidualNaturality.CoefficientsOn.convolution_sum {A : Type} (c d : HarmonicFields.Coefficients A) (S : Finset ℤ) (hS : c.support ⊆ S) (j : ℤ) (x : A) : (c * d).coeff j x = ∑ k ∈ S, c.coeff k x * d.coeff (j - k) x

theorem NavierStokes.PhysicalResidualNaturality.CoefficientsOn.mul {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {a b : ℝ} {c₁ c₂ : HarmonicFields.Coefficients D} {d₁ d₂ : HarmonicFields.Coefficients E} (h₁ : CoefficientsOn U e a c₁ d₁) (h₂ : CoefficientsOn U e b c₂ d₂) : CoefficientsOn U e (a * b) (c₁ * c₂) (d₁ * d₂)

theorem NavierStokes.PhysicalResidualNaturality.CoefficientsOn.scale {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {a : ℝ} {c : HarmonicFields.Coefficients D} {d : HarmonicFields.Coefficients E} (hc : CoefficientsOn U e a c d) (b : ℝ) : CoefficientsOn U e (b * a) (b • c) d

theorem NavierStokes.PhysicalResidualNaturality.CoefficientsOn.angular {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {a : ℝ} {c : HarmonicFields.Coefficients D} {d : HarmonicFields.Coefficients E} (hc : CoefficientsOn U e a c d) (k : ℤ) : CoefficientsOn U e a (HarmonicFields.angularDifferentiate k c) (HarmonicFields.angularDifferentiate k d)

theorem NavierStokes.PhysicalResidualNaturality.CoefficientsOn.realCoefficients {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {a : ℝ} {c : HarmonicFields.Coefficients D} {d : HarmonicFields.Coefficients E} (hc : CoefficientsOn U e a c d) : CoefficientsOn U e a (HarmonicResidual.realCoefficients c) (HarmonicResidual.realCoefficients d)

theorem NavierStokes.PhysicalResidualNaturality.CoefficientsOn.nonconstant {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {a : ℝ} {c : HarmonicFields.Coefficients D} {d : HarmonicFields.Coefficients E} (hc : CoefficientsOn U e a c d) : CoefficientsOn U e a (HarmonicResidual.nonconstant c) (HarmonicResidual.nonconstant d)

theorem NavierStokes.PhysicalResidualNaturality.CoefficientsOn.differentiate {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} (hU : IsOpen U) {e : D ≃L[ℝ] E} {a b k kr : ℝ} {c : HarmonicFields.Coefficients D} {d : HarmonicFields.Coefficients E} {V : D → D} {W : E → E} {Phi : D → ℝ} {Psi : E → ℝ} (hc : CoefficientsOn U e a c d) (hV : ∀ x ∈ U, e (V x) = b • W (e x)) (hphase : Set.EqOn (fun (x : D) => k * Phi x) (fun (x : D) => kr * Psi (e x)) U) : CoefficientsOn U e (a * b) (HarmonicFields.differentiate V k Phi c) (HarmonicFields.differentiate W kr Psi d)

Carrier compatibility is an equality before restriction to the graph.

The actual cylindrical operator, including its frame terms

structure NavierStokes.PhysicalResidualNaturality.FrameOn {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (U : Set D) (e : D ≃L[ℝ] E) (c l : ℝ) (g : HarmonicResidual.Frame D) (r : HarmonicResidual.Frame E) : Prop

Primitive chart identities. The time and viscosity identities include the slow-time sign and the physical viscosity normalization.

• radial (x : D) : x ∈ U → e (g.radial x) = l • r.radial (e x)
• axial (x : D) : x ∈ U → e (g.axial x) = l • r.axial (e x)
• time (x : D) : x ∈ U → e (g.time x) = (c * l) • r.time (e x)
• radius (x : D) : x ∈ U → r.radius (e x) = l * g.radius x
• viscosity : g.viscosity * l = c * r.viscosity

theorem NavierStokes.PhysicalResidualNaturality.FrameOn.inverseRadius {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {c l : ℝ} {g : HarmonicResidual.Frame D} {r : HarmonicResidual.Frame E} (H : FrameOn U e c l g r) (hl : l ≠ 0) : CoefficientsOn U e l (HarmonicFields.constantCoefficient fun (x : D) => ↑(g.radius x)⁻¹) (HarmonicFields.constantCoefficient fun (x : E) => ↑(r.radius x)⁻¹)

theorem NavierStokes.PhysicalResidualNaturality.FrameOn.inverseRadiusSq {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {c l : ℝ} {g : HarmonicResidual.Frame D} {r : HarmonicResidual.Frame E} (H : FrameOn U e c l g r) (hl : l ≠ 0) : CoefficientsOn U e (l * l) (HarmonicFields.constantCoefficient fun (x : D) => ↑(g.radius x ^ 2)⁻¹) (HarmonicFields.constantCoefficient fun (x : E) => ↑(r.radius x ^ 2)⁻¹)

theorem NavierStokes.PhysicalResidualNaturality.FrameOn.scalarLaplacian {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {c l : ℝ} {g : HarmonicResidual.Frame D} {r : HarmonicResidual.Frame E} (H : FrameOn U e c l g r) (hU : IsOpen U) (hl : l ≠ 0) {a k kr : ℝ} {Phi : D → ℝ} {Psi : E → ℝ} (kp : ℤ) {f : HarmonicFields.Coefficients D} {q : HarmonicFields.Coefficients E} (hf : CoefficientsOn U e a f q) (hp : Set.EqOn (fun (x : D) => k * Phi x) (fun (x : D) => kr * Psi (e x)) U) : CoefficientsOn U e (a * (l * l)) (HarmonicResidual.scalarLaplacian g k Phi kp f) (HarmonicResidual.scalarLaplacian r kr Psi kp q)

theorem NavierStokes.PhysicalResidualNaturality.FrameOn.rotate {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {a : ℝ} {f : HarmonicResidual.VectorCoefficients D} {q : HarmonicResidual.VectorCoefficients E} (hf : ∀ (i : Fin 3), CoefficientsOn U e a (f i) (q i)) (i : Fin 3) : CoefficientsOn U e a (HarmonicResidual.rotate f i) (HarmonicResidual.rotate q i)

theorem NavierStokes.PhysicalResidualNaturality.FrameOn.vectorLaplacian {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {c l : ℝ} {g : HarmonicResidual.Frame D} {r : HarmonicResidual.Frame E} (H : FrameOn U e c l g r) (hU : IsOpen U) (hl : l ≠ 0) {a k kr : ℝ} {Phi : D → ℝ} {Psi : E → ℝ} (kp : ℤ) {f : HarmonicResidual.VectorCoefficients D} {q : HarmonicResidual.VectorCoefficients E} (hf : ∀ (i : Fin 3), CoefficientsOn U e a (f i) (q i)) (hp : Set.EqOn (fun (x : D) => k * Phi x) (fun (x : D) => kr * Psi (e x)) U) (i : Fin 3) : CoefficientsOn U e (a * (l * l)) (HarmonicResidual.vectorLaplacian g k Phi kp f i) (HarmonicResidual.vectorLaplacian r kr Psi kp q i)

theorem NavierStokes.PhysicalResidualNaturality.FrameOn.transport {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {c l : ℝ} {g : HarmonicResidual.Frame D} {r : HarmonicResidual.Frame E} (H : FrameOn U e c l g r) (hU : IsOpen U) (hl : l ≠ 0) {a b k kr : ℝ} {Phi : D → ℝ} {Psi : E → ℝ} (kp : ℤ) {f v : HarmonicResidual.VectorCoefficients D} {q w : HarmonicResidual.VectorCoefficients E} (hf : ∀ (i : Fin 3), CoefficientsOn U e a (f i) (q i)) (hv : ∀ (i : Fin 3), CoefficientsOn U e b (v i) (w i)) (hp : Set.EqOn (fun (x : D) => k * Phi x) (fun (x : D) => kr * Psi (e x)) U) (i : Fin 3) : CoefficientsOn U e (a * b * l) (HarmonicResidual.transport g k Phi kp f v i) (HarmonicResidual.transport r kr Psi kp q w i)

theorem NavierStokes.PhysicalResidualNaturality.FrameOn.gradient {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {c l : ℝ} {g : HarmonicResidual.Frame D} {r : HarmonicResidual.Frame E} (H : FrameOn U e c l g r) (hU : IsOpen U) (hl : l ≠ 0) {a k kr : ℝ} {Phi : D → ℝ} {Psi : E → ℝ} (kp : ℤ) {f : HarmonicFields.Coefficients D} {q : HarmonicFields.Coefficients E} (hf : CoefficientsOn U e a f q) (hp : Set.EqOn (fun (x : D) => k * Phi x) (fun (x : D) => kr * Psi (e x)) U) (i : Fin 3) : CoefficientsOn U e (a * l) (HarmonicResidual.gradient g k Phi kp f i) (HarmonicResidual.gradient r kr Psi kp q i)

theorem NavierStokes.PhysicalResidualNaturality.FrameOn.linearResidual {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {c l : ℝ} {g : HarmonicResidual.Frame D} {r : HarmonicResidual.Frame E} (H : FrameOn U e c l g r) (hU : IsOpen U) (hl : l ≠ 0) {k kr : ℝ} {Phi : D → ℝ} {Psi : E → ℝ} (kp : ℤ) {B f : HarmonicResidual.VectorCoefficients D} {Br q : HarmonicResidual.VectorCoefficients E} {p : HarmonicFields.Coefficients D} {pr : HarmonicFields.Coefficients E} (hB : ∀ (i : Fin 3), CoefficientsOn U e c (B i) (Br i)) (hf : ∀ (i : Fin 3), CoefficientsOn U e c (f i) (q i)) (hp : CoefficientsOn U e (c * c) p pr) (hphase : Set.EqOn (fun (x : D) => k * Phi x) (fun (x : D) => kr * Psi (e x)) U) (i : Fin 3) : CoefficientsOn U e (c * c * l) (HarmonicResidual.linearResidual g k Phi kp B f p i) (HarmonicResidual.linearResidual r kr Psi kp Br q pr i)

theorem NavierStokes.PhysicalResidualNaturality.FrameOn.nonlinearResidual {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {c l : ℝ} {g : HarmonicResidual.Frame D} {r : HarmonicResidual.Frame E} (H : FrameOn U e c l g r) (hU : IsOpen U) (hl : l ≠ 0) {k kr : ℝ} {Phi : D → ℝ} {Psi : E → ℝ} (kp : ℤ) {B f : HarmonicResidual.VectorCoefficients D} {Br q : HarmonicResidual.VectorCoefficients E} {p : HarmonicFields.Coefficients D} {pr : HarmonicFields.Coefficients E} (hB : ∀ (i : Fin 3), CoefficientsOn U e c (B i) (Br i)) (hf : ∀ (i : Fin 3), CoefficientsOn U e c (f i) (q i)) (hp : CoefficientsOn U e (c * c) p pr) (hphase : Set.EqOn (fun (x : D) => k * Phi x) (fun (x : D) => kr * Psi (e x)) U) (i : Fin 3) : CoefficientsOn U e (c * c * l) (HarmonicResidual.nonlinearResidual g k Phi kp B f p i) (HarmonicResidual.nonlinearResidual r kr Psi kp Br q pr i)

Recovering the source from actual field compatibility

theorem NavierStokes.PhysicalResidualNaturality.coefficient_of_field {D E : Type} {a k kr : ℝ} {Phi : D → ℝ} {Psi : E → ℝ} {kp : ℤ} (hkp : kp ≠ 0) (f : HarmonicFields.Coefficients D) (q : HarmonicFields.Coefficients E) (x : D) (y : E) (hphase : k * Phi x = kr * Psi y) (hfield : ∀ (theta : ℝ), HarmonicFields.field f k Phi kp (x, theta) = a • HarmonicFields.field q kr Psi kp (y, theta)) (j : ℤ) : f.coeff j x = a • q.coeff j y

Uniqueness at one full angular fiber. Frequencies may differ, but the integer angular carrier and the complete slow carrier agree.

theorem NavierStokes.PhysicalResidualNaturality.CoefficientsOn.of_fields {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {a k kr : ℝ} {Phi : D → ℝ} {Psi : E → ℝ} {kp : ℤ} (hkp : kp ≠ 0) {f : HarmonicFields.Coefficients D} {q : HarmonicFields.Coefficients E} (hp : Set.EqOn (fun (x : D) => k * Phi x) (fun (x : D) => kr * Psi (e x)) U) (hf : ∀ x ∈ U, ∀ (theta : ℝ), HarmonicFields.field f k Phi kp (x, theta) = a • HarmonicFields.field q kr Psi kp (e x, theta)) : CoefficientsOn U e a f q

theorem NavierStokes.PhysicalResidualNaturality.CoefficientsOn.of_real_fields {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {a k kr : ℝ} {Phi : D → ℝ} {Psi : E → ℝ} {kp : ℤ} (hkp : kp ≠ 0) {f : HarmonicFields.Coefficients D} {q : HarmonicFields.Coefficients E} (hp : Set.EqOn (fun (x : D) => k * Phi x) (fun (x : D) => kr * Psi (e x)) U) (hf : ∀ x ∈ U, ∀ (theta : ℝ), (HarmonicFields.field f k Phi kp (x, theta)).re = a * (HarmonicFields.field q kr Psi kp (e x, theta)).re) : CoefficientsOn U e a (HarmonicResidual.realCoefficients f) (HarmonicResidual.realCoefficients q)

theorem NavierStokes.PhysicalResidualNaturality.realCoefficients_sub {D : Type} (a b : HarmonicFields.Coefficients D) : HarmonicResidual.realCoefficients (a - b) = HarmonicResidual.realCoefficients a - HarmonicResidual.realCoefficients b

structure NavierStokes.PhysicalResidualNaturality.LabelOn {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (U : Set D) (e : D ≃L[ℝ] E) (c l : ℝ) (d : HarmonicResidual.LabelData D) (r : HarmonicResidual.LabelData E) : Prop

Compatibility of a label's primitive fields. Gaussian and alias inputs are compared as real fields, exactly as in the physical residual.

• phase : Set.EqOn (fun (x : D) => d.frequency * d.phase x) (fun (x : D) => r.frequency * r.phase (e x)) U
• angular : d.angularFrequency = r.angularFrequency
• velocity (i : Fin 3) : CoefficientsOn U e c (d.velocity i) (r.velocity i)
• pressure : CoefficientsOn U e (c * c) d.pressure r.pressure
• gaussian (i : Fin 3) : CoefficientsOn U e (c * c * l) (HarmonicResidual.realCoefficients (d.gaussian i)) (HarmonicResidual.realCoefficients (r.gaussian i))
• aliasError (i : Fin 3) : CoefficientsOn U e (c * c * l) (HarmonicResidual.realCoefficients (d.aliasError i)) (HarmonicResidual.realCoefficients (r.aliasError i))

theorem NavierStokes.PhysicalResidualNaturality.LabelOn.residualCoefficients {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {c l : ℝ} {d : HarmonicResidual.LabelData D} {r : HarmonicResidual.LabelData E} (H : LabelOn U e c l d r) (hU : IsOpen U) (hl : l ≠ 0) {g : HarmonicResidual.Frame D} {gr : HarmonicResidual.Frame E} (hg : FrameOn U e c l g gr) {B M : D → HarmonicCalculus.ComplexVector} {Br Mr : E → HarmonicCalculus.ComplexVector} (hB : ∀ x ∈ U, B x = c • Br (e x)) (hM : ∀ x ∈ U, M x = c • Mr (e x)) (i : Fin 3) : CoefficientsOn U e (c * c * l) (d.residualCoefficients g B M i) (r.residualCoefficients gr Br Mr i)

theorem NavierStokes.PhysicalResidualNaturality.LabelOn.waveResidualCoefficients {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {c l : ℝ} {d : HarmonicResidual.LabelData D} {r : HarmonicResidual.LabelData E} (H : LabelOn U e c l d r) (hU : IsOpen U) (hl : l ≠ 0) {g : HarmonicResidual.Frame D} {gr : HarmonicResidual.Frame E} (hg : FrameOn U e c l g gr) {B M : D → HarmonicCalculus.ComplexVector} {Br Mr : E → HarmonicCalculus.ComplexVector} (hB : ∀ x ∈ U, B x = c • Br (e x)) (hM : ∀ x ∈ U, M x = c • Mr (e x)) (i : Fin 3) : CoefficientsOn U e (c * c * l) (d.waveResidualCoefficients g B M i) (r.waveResidualCoefficients gr Br Mr i)

structure NavierStokes.PhysicalResidualNaturality.BlockFieldsOn {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (U : Set D) (e : D ≃L[ℝ] E) (c l : ℝ) (b : CorrectionState.HarmonicBlock D) (br : CorrectionState.HarmonicBlock E) (G A : HarmonicResidual.BlockCoefficients D) (Gr Ar : HarmonicResidual.BlockCoefficients E) (n nr : ℕ) : Prop

Only actual full-lift fields and their carrier are compared here. In particular, this does not assume compatibility of an already computed source.

• phase : Set.EqOn (fun (x : D) => b.frequency n * b.phase n x) (fun (x : D) => br.frequency nr * br.phase nr (e x)) U
• angular : b.angularFrequency n = br.angularFrequency nr
• angular_ne : b.angularFrequency n ≠ 0
• velocity (x : D) : x ∈ U → ∀ (theta : ℝ) (i : Fin 3), b.oscillation n (x, theta) i = c * br.oscillation nr (e x, theta) i
• pressure (x : D) : x ∈ U → ∀ (theta : ℝ), b.oscillatoryPressure n (x, theta) = c * c * br.oscillatoryPressure nr (e x, theta)
• gaussian (x : D) : x ∈ U → ∀ (theta : ℝ) (i : Fin 3), (HarmonicFields.field (G n i) (b.frequency n) (b.phase n) (b.angularFrequency n) (x, theta)).re = c * c * l * (HarmonicFields.field (Gr nr i) (br.frequency nr) (br.phase nr) (br.angularFrequency nr) (e x, theta)).re
• aliasError (x : D) : x ∈ U → ∀ (theta : ℝ) (i : Fin 3), (HarmonicFields.field (A n i) (b.frequency n) (b.phase n) (b.angularFrequency n) (x, theta)).re = c * c * l * (HarmonicFields.field (Ar nr i) (br.frequency nr) (br.phase nr) (br.angularFrequency nr) (e x, theta)).re

theorem NavierStokes.PhysicalResidualNaturality.BlockFieldsOn.labelOn {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {c l : ℝ} {b : CorrectionState.HarmonicBlock D} {br : CorrectionState.HarmonicBlock E} {G A : HarmonicResidual.BlockCoefficients D} {Gr Ar : HarmonicResidual.BlockCoefficients E} {n nr : ℕ} (H : BlockFieldsOn U e c l b br G A Gr Ar n nr) : LabelOn U e c l (HarmonicResidual.ofBlock b G A n) (HarmonicResidual.ofBlock br Gr Ar nr)

theorem NavierStokes.PhysicalResidualNaturality.residualSource_naturality {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} (hU : IsOpen U) {e : D ≃L[ℝ] E} {c l : ℝ} (hl : l ≠ 0) {C : CorrectionState.Context D} {Cr : CorrectionState.Context E} {s : CorrectionState.State D} {sr : CorrectionState.State E} {b : CorrectionState.HarmonicBlock D} {br : CorrectionState.HarmonicBlock E} {G A : HarmonicResidual.BlockCoefficients D} {Gr Ar : HarmonicResidual.BlockCoefficients E} {n nr : ℕ} (hg : FrameOn U e c l (HarmonicResidual.contextFrame C n) (HarmonicResidual.contextFrame Cr nr)) (hB : ∀ x ∈ U, HarmonicResidual.contextBase C n x = c • HarmonicResidual.contextBase Cr nr (e x)) (hM : ∀ x ∈ U, HarmonicResidual.stateMean s n x = c • HarmonicResidual.stateMean sr nr (e x)) (H : BlockFieldsOn U e c l b br G A Gr Ar n nr) (j : ℤ) {x : D} (hx : x ∈ U) : ParticularWaveAssembly.residualSource C s b G A j n x = (c * c * l) • ParticularWaveAssembly.residualSource Cr sr br Gr Ar j nr (e x)

Exact naturality of the literal source supplied to the Volterra solve.

The concrete common-cover chart

@[reducible, inline]

abbrev NavierStokes.PhysicalResidualNaturality.Lift : Type

Lift: an abbreviation for PhysicalResidualBridge.Lift.

Equations

• NavierStokes.PhysicalResidualNaturality.Lift = NavierStokes.PhysicalResidualBridge.Lift

@[reducible, inline]

abbrev NavierStokes.PhysicalResidualNaturality.Associated : Type

Associated: an abbreviation for PhysicalParticularWave.Parameter × TorusInverse.Plane.

Equations

• NavierStokes.PhysicalResidualNaturality.Associated = (NavierStokes.PhysicalParticularWave.Parameter × NavierStokes.TorusInverse.Plane)

noncomputable def NavierStokes.PhysicalResidualNaturality.chartEquiv (h : ℝ) {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (gap : ℕ) : Lift ≃L[ℝ] Lift

The invertible real-lift map underlying the integer torus cover.

Equations

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

@[simp]

theorem NavierStokes.PhysicalResidualNaturality.chartEquiv_apply (h : ℝ) {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (gap : ℕ) (x : Lift) : (chartEquiv h hQ hQr gap) x = (PhysicalParticularWave.chartChange h Q Qr gap) x

noncomputable def NavierStokes.PhysicalResidualNaturality.commonFrame (h Q : ℝ) (i : ℕ) : HarmonicResidual.Frame Lift

Actual graph directions on the free lift, before adjoining the angle.

Equations

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

theorem NavierStokes.PhysicalResidualNaturality.weight_time {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (h : ℝ) : PhysicalParticularWave.velocityWeight h Q Qr * PhysicalParticularWave.ratioPower Q Qr (1 / 2) = PhysicalParticularWave.clockWeight h Q Qr

theorem NavierStokes.PhysicalResidualNaturality.weight_pressure {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (h : ℝ) : PhysicalParticularWave.velocityWeight h Q Qr * PhysicalParticularWave.velocityWeight h Q Qr = PhysicalParticularWave.pressureWeight h Q Qr

theorem NavierStokes.PhysicalResidualNaturality.weight_source {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (h : ℝ) : PhysicalParticularWave.velocityWeight h Q Qr * PhysicalParticularWave.velocityWeight h Q Qr * PhysicalParticularWave.ratioPower Q Qr (1 / 2) = PhysicalParticularWave.sourceWeight h Q Qr

theorem NavierStokes.PhysicalResidualNaturality.weight_viscosity {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (h : ℝ) : Q ^ h * PhysicalParticularWave.ratioPower Q Qr (1 / 2) = PhysicalParticularWave.velocityWeight h Q Qr * Qr ^ h

theorem NavierStokes.PhysicalResidualNaturality.commonFrame_chart (h : ℝ) {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (i gap : ℕ) : FrameOn {x : Lift | 0 < x.1} (chartEquiv h hQ hQr gap) (PhysicalParticularWave.velocityWeight h Q Qr) (PhysicalParticularWave.ratioPower Q Qr (1 / 2)) (commonFrame h Q i) (commonFrame h Qr (i + gap))

noncomputable def NavierStokes.PhysicalResidualNaturality.associatedToLift : Associated ≃ₗᵢ[ℝ] Lift

Association and the (T,Z) order used by the correction state.

Equations

• NavierStokes.PhysicalResidualNaturality.associatedToLift = (NavierStokes.ParticularWaveBounds.liftAssoc NavierStokes.TorusInverse.Plane).symm.trans NavierStokes.PhysicalResidualTZ.swapSlow

@[simp]

theorem NavierStokes.PhysicalResidualNaturality.associatedToLift_apply (x : Associated) : associatedToLift x = (x.1.1, (x.1.2.2, x.1.2.1), x.2)

noncomputable def NavierStokes.PhysicalResidualNaturality.associatedChart (h : ℝ) {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (gap : ℕ) : Associated ≃L[ℝ] Associated

Associated chart, given by (associatedToLift.toContinuousLinearEquiv.trans (chartEquiv h hQ hQr gap)).trans associatedToLift.symm.toContinuousLinearEquiv.

Equations

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

@[simp]

theorem NavierStokes.PhysicalResidualNaturality.associatedChart_apply (h : ℝ) {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (gap : ℕ) (x : Associated) : (associatedChart h hQ hQr gap) x = (PhysicalParticularWave.parameterChange h Q Qr x.1, (CommonCoverSolve.coverPower gap) x.2)

noncomputable def NavierStokes.PhysicalResidualNaturality.associatedFrame (h Q : ℝ) (i : ℕ) : HarmonicResidual.Frame Associated

Associated frame, given by StateReindex.frame associatedToLift (commonFrame h Q i).

Equations

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

theorem NavierStokes.PhysicalResidualNaturality.associatedFrame_chart (h : ℝ) {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (i gap : ℕ) : FrameOn {x : Associated | 0 < x.1.1} (associatedChart h hQ hQr gap) (PhysicalParticularWave.velocityWeight h Q Qr) (PhysicalParticularWave.ratioPower Q Qr (1 / 2)) (associatedFrame h Q i) (associatedFrame h Qr (i + gap))

def NavierStokes.PhysicalResidualNaturality.positiveLift : Set Associated

The positive-radius free lift. Every auxiliary variable remains free.

Equations

• NavierStokes.PhysicalResidualNaturality.positiveLift = {x : NavierStokes.PhysicalResidualNaturality.Associated | 0 < x.1.1}

theorem NavierStokes.PhysicalResidualNaturality.positiveLift_open : IsOpen positiveLift

structure NavierStokes.PhysicalResidualNaturality.BandCoherence (D : ParticularWaveAssembly.AssemblyData PhysicalParticularWave.Parameter) (h : ℝ) {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (i gap n : ℕ) : Prop

Concrete primitive coherence needed by a band solve. These are field, phase, and explicit operator identities, never an identity of residuals or of solved waves.

• targetFrame : HarmonicResidual.contextFrame D.context n = associatedFrame h Q i
• referenceFrame : HarmonicResidual.contextFrame D.context D.reference.band = associatedFrame h Qr (i + gap)
• base (x : Associated) : x ∈ positiveLift → HarmonicResidual.contextBase D.context n x = PhysicalParticularWave.velocityWeight h Q Qr • HarmonicResidual.contextBase D.context D.reference.band ((associatedChart h hQ hQr gap) x)
• mean (x : Associated) : x ∈ positiveLift → HarmonicResidual.stateMean D.state n x = PhysicalParticularWave.velocityWeight h Q Qr • HarmonicResidual.stateMean D.state D.reference.band ((associatedChart h hQ hQr gap) x)
• block : BlockFieldsOn positiveLift (associatedChart h hQ hQr gap) (PhysicalParticularWave.velocityWeight h Q Qr) (PhysicalParticularWave.ratioPower Q Qr (1 / 2)) D.carrierBlock D.carrierBlock D.gaussianInput D.aliasInput D.gaussianInput D.aliasInput n D.reference.band

theorem NavierStokes.PhysicalResidualNaturality.BandCoherence.source_on {D : ParticularWaveAssembly.AssemblyData PhysicalParticularWave.Parameter} {h Q Qr : ℝ} {hQ : 0 < Q} {hQr : 0 < Qr} {i gap n : ℕ} (H : BandCoherence D h hQ hQr i gap n) (j : ℤ) {x : Associated} (hx : x ∈ positiveLift) : ParticularWaveAssembly.residualSource D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j n x = PhysicalParticularWave.transportedResidualSource D h Q Qr gap j x

structure NavierStokes.PhysicalResidualNaturality.PositiveSupport (b : CorrectionState.HarmonicBlock Associated) (G A : HarmonicResidual.BlockCoefficients Associated) (n : ℕ) : Type

Primitive support assumptions, allowing arbitrary zero-mode aliases.

• supportSet : Set Associated

  Support set of PositiveSupport, of type Set Associated.

• closed : IsClosed self.supportSet
• positive : self.supportSet ⊆ positiveLift
• velocity (i : Fin 3) : HarmonicSourceSupport.NonzeroSupported self.supportSet (HarmonicResidual.realCoefficients (b.velocity n i))
• pressure : HarmonicSourceSupport.NonzeroSupported self.supportSet (HarmonicResidual.realCoefficients (b.pressure n))
• gaussian (i : Fin 3) : HarmonicSourceSupport.NonzeroSupported self.supportSet (HarmonicResidual.realCoefficients (G n i))
• aliasError (i : Fin 3) : HarmonicSourceSupport.NonzeroSupported self.supportSet (HarmonicResidual.realCoefficients (A n i))

theorem NavierStokes.PhysicalResidualNaturality.PositiveSupport.source_zero {b : CorrectionState.HarmonicBlock Associated} {G A : HarmonicResidual.BlockCoefficients Associated} {n : ℕ} (H : PositiveSupport b G A n) (C : CorrectionState.Context Associated) (s : CorrectionState.State Associated) (j : ℤ) {x : Associated} (hx : x ∉ positiveLift) : ParticularWaveAssembly.residualSource C s b G A j n x = 0

theorem NavierStokes.PhysicalResidualNaturality.BandCoherence.source_eq {D : ParticularWaveAssembly.AssemblyData PhysicalParticularWave.Parameter} {h Q Qr : ℝ} {hQ : 0 < Q} {hQr : 0 < Qr} {i gap n : ℕ} (H : BandCoherence D h hQ hQr i gap n) (hn : PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput n) (hr : PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput D.reference.band) (j : ℤ) : ParticularWaveAssembly.residualSource D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j n = PhysicalParticularWave.transportedResidualSource D h Q Qr gap j

Full free-variable equality, including the complement of the annular cells, derived from primitive field coherence and primitive support.

theorem NavierStokes.PhysicalResidualNaturality.BandCoherence.residualBandAmplitude_eq {D : ParticularWaveAssembly.AssemblyData PhysicalParticularWave.Parameter} {h Q Qr : ℝ} {hQ : 0 < Q} {hQr : 0 < Qr} {i gap n : ℕ} (H : BandCoherence D h hQ hQr i gap n) (hn : PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput n) (hr : PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput D.reference.band) (K : ℝ) (j : ℤ) : PhysicalParticularWave.residualBandAmplitude D h hQ hQr gap K j n = PhysicalParticularWave.bandAmplitude D h hQ hQr gap K j

The actual target-source Volterra solve is the coherently transported one; no equality of outputs is supplied as an assumption.

theorem NavierStokes.PhysicalResidualNaturality.BandCoherence.residualBandPressure_eq {D : ParticularWaveAssembly.AssemblyData PhysicalParticularWave.Parameter} {h Q Qr : ℝ} {hQ : 0 < Q} {hQr : 0 < Qr} {i gap n : ℕ} (H : BandCoherence D h hQ hQr i gap n) (hn : PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput n) (hr : PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput D.reference.band) (K : ℝ) (j : ℤ) : PhysicalParticularWave.residualBandPressure D h hQ hQr gap K j n = PhysicalParticularWave.bandPressure D h hQ hQr gap K j

A lift-coherence invariant preserved by actual state addition

def NavierStokes.PhysicalResidualNaturality.ScalarOn {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (U : Set D) (e : D ≃L[ℝ] E) (a : ℝ) (f : D → ℝ) (g : E → ℝ) : Prop

Scalar on, given by ∀ x ∈ U, f x = a * g (e x).

Equations

• NavierStokes.PhysicalResidualNaturality.ScalarOn U e a f g = ∀ x ∈ U, f x = a * g (e x)

theorem NavierStokes.PhysicalResidualNaturality.ScalarOn.reweight {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {a b : ℝ} {f : D → ℝ} {g : E → ℝ} (hf : ScalarOn U e a f g) (hab : a = b) : ScalarOn U e b f g

theorem NavierStokes.PhysicalResidualNaturality.ScalarOn.add {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {a : ℝ} {f v : D → ℝ} {g w : E → ℝ} (hf : ScalarOn U e a f g) (hv : ScalarOn U e a v w) : ScalarOn U e a (f + v) (g + w)

theorem NavierStokes.PhysicalResidualNaturality.ScalarOn.sub {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {a : ℝ} {f v : D → ℝ} {g w : E → ℝ} (hf : ScalarOn U e a f g) (hv : ScalarOn U e a v w) : ScalarOn U e a (f - v) (g - w)

theorem NavierStokes.PhysicalResidualNaturality.ScalarOn.mul {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {a b : ℝ} {f v : D → ℝ} {g w : E → ℝ} (hf : ScalarOn U e a f g) (hv : ScalarOn U e b v w) : ScalarOn U e (a * b) (f * v) (g * w)

theorem NavierStokes.PhysicalResidualNaturality.ScalarOn.smul {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {a : ℝ} {f : D → ℝ} {g : E → ℝ} (hf : ScalarOn U e a f g) (b : ℝ) : ScalarOn U e a (b • f) (b • g)

theorem NavierStokes.PhysicalResidualNaturality.ScalarOn.along {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} (hU : IsOpen U) {e : D ≃L[ℝ] E} {a b : ℝ} {f : D → ℝ} {g : E → ℝ} {V : D → D} {W : E → E} (hf : ScalarOn U e a f g) (hV : ∀ x ∈ U, e (V x) = b • W (e x)) : ScalarOn U e (a * b) (HarmonicCalculus.along V f) (HarmonicCalculus.along W g)

structure NavierStokes.PhysicalResidualNaturality.TripleOn {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (U : Set D) (e : D ≃L[ℝ] E) (a : ℝ) (f : MeanIncrementBounds.Triple D) (g : MeanIncrementBounds.Triple E) (n nr : ℕ) : Prop

Triple on data, collecting radial, angular, axial.

• radial : ScalarOn U e a (f.radial n) (g.radial nr)
• angular : ScalarOn U e a (f.angular n) (g.angular nr)
• axial : ScalarOn U e a (f.axial n) (g.axial nr)

theorem NavierStokes.PhysicalResidualNaturality.TripleOn.updated {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {a : ℝ} {f v : MeanIncrementBounds.Triple D} {g w : MeanIncrementBounds.Triple E} {n nr : ℕ} (hf : TripleOn U e a f g n nr) (hv : TripleOn U e a v w n nr) : TripleOn U e a (MeanIncrementBounds.updated f v) (MeanIncrementBounds.updated g w) n nr

structure NavierStokes.PhysicalResidualNaturality.StateOn {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (U : Set D) (e : D ≃L[ℝ] E) (c l : ℝ) (s : CorrectionState.State D) (r : CorrectionState.State E) (n nr : ℕ) : Prop

A full free-lift invariant on the actual state fields. It is stronger than graph-only physical representation and is closed under addition.

• mean : TripleOn U e c s.mean r.mean n nr
• pressure : ScalarOn U e (c * c) (s.pressure n) (r.pressure nr)
• oscillation (x : D) : x ∈ U → ∀ (theta : ℝ) (i : Fin 3), s.oscillation n (x, theta) i = c * r.oscillation nr (e x, theta) i
• oscillatoryPressure (x : D) : x ∈ U → ∀ (theta : ℝ), s.oscillatoryPressure n (x, theta) = c * c * r.oscillatoryPressure nr (e x, theta)
• baseError (x : D) : x ∈ U → ∀ (theta : ℝ) (i : Fin 3), s.errors.base n (x, theta) i = c * c * l * r.errors.base nr (e x, theta) i
• gaussian (x : D) : x ∈ U → ∀ (theta : ℝ) (i : Fin 3), s.errors.gaussian n (x, theta) i = c * c * l * r.errors.gaussian nr (e x, theta) i
• aliasError (x : D) : x ∈ U → ∀ (theta : ℝ) (i : Fin 3), s.errors.aliasError n (x, theta) i = c * c * l * r.errors.aliasError nr (e x, theta) i

theorem NavierStokes.PhysicalResidualNaturality.StateOn.addIncrement {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {c l : ℝ} {s v : CorrectionState.State D} {r w : CorrectionState.State E} {n nr : ℕ} (hs : StateOn U e c l s r n nr) (hv : StateOn U e c l v w n nr) : StateOn U e c l (s.addIncrement v.mean v.pressure v.oscillation v.oscillatoryPressure v.errors) (r.addIncrement w.mean w.pressure w.oscillation w.oscillatoryPressure w.errors) n nr

theorem NavierStokes.PhysicalResidualNaturality.StateOn.covariance {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {c l : ℝ} {s : CorrectionState.State D} {r : CorrectionState.State E} {n nr : ℕ} (H : StateOn U e c l s r n nr) (i j : Fin 3) : ScalarOn U e (c * c) (s.covariance i j n) (r.covariance i j nr)

theorem NavierStokes.PhysicalResidualNaturality.dr_eq_along {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (C : CorrectionState.Context D) (f : MeanIncrementBounds.Field D) (n : ℕ) (x : D) : C.operators.dr f n x = HarmonicCalculus.along (HarmonicResidual.contextFrame C n).radial (f n) x

theorem NavierStokes.PhysicalResidualNaturality.dz_eq_along {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (C : CorrectionState.Context D) (f : MeanIncrementBounds.Field D) (n : ℕ) (x : D) : C.operators.dz f n x = HarmonicCalculus.along (HarmonicResidual.contextFrame C n).axial (f n) x

theorem NavierStokes.PhysicalResidualNaturality.time_eq_along {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (C : CorrectionState.Context D) (f : MeanIncrementBounds.Field D) (n : ℕ) (x : D) : C.operators.time f n x = HarmonicCalculus.along (HarmonicResidual.contextFrame C n).time (f n) x

theorem NavierStokes.PhysicalResidualNaturality.FrameOn.scalarDr {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {c l : ℝ} {C : CorrectionState.Context D} {Cr : CorrectionState.Context E} {n nr : ℕ} (H : FrameOn U e c l (HarmonicResidual.contextFrame C n) (HarmonicResidual.contextFrame Cr nr)) (hU : IsOpen U) {a : ℝ} {f : MeanIncrementBounds.Field D} {g : MeanIncrementBounds.Field E} (hf : ScalarOn U e a (f n) (g nr)) : ScalarOn U e (a * l) (C.operators.dr f n) (Cr.operators.dr g nr)

theorem NavierStokes.PhysicalResidualNaturality.FrameOn.scalarDz {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {c l : ℝ} {C : CorrectionState.Context D} {Cr : CorrectionState.Context E} {n nr : ℕ} (H : FrameOn U e c l (HarmonicResidual.contextFrame C n) (HarmonicResidual.contextFrame Cr nr)) (hU : IsOpen U) {a : ℝ} {f : MeanIncrementBounds.Field D} {g : MeanIncrementBounds.Field E} (hf : ScalarOn U e a (f n) (g nr)) : ScalarOn U e (a * l) (C.operators.dz f n) (Cr.operators.dz g nr)

theorem NavierStokes.PhysicalResidualNaturality.FrameOn.scalarTime {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {c l : ℝ} {C : CorrectionState.Context D} {Cr : CorrectionState.Context E} {n nr : ℕ} (H : FrameOn U e c l (HarmonicResidual.contextFrame C n) (HarmonicResidual.contextFrame Cr nr)) (hU : IsOpen U) {a : ℝ} {f : MeanIncrementBounds.Field D} {g : MeanIncrementBounds.Field E} (hf : ScalarOn U e a (f n) (g nr)) : ScalarOn U e (a * (c * l)) (C.operators.time f n) (Cr.operators.time g nr)

theorem NavierStokes.PhysicalResidualNaturality.FrameOn.scalarInvRadius {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {c l : ℝ} {C : CorrectionState.Context D} {Cr : CorrectionState.Context E} {n nr : ℕ} (H : FrameOn U e c l (HarmonicResidual.contextFrame C n) (HarmonicResidual.contextFrame Cr nr)) (hl : l ≠ 0) : ScalarOn U e l (C.operators.invRadius n) (Cr.operators.invRadius nr)

theorem NavierStokes.PhysicalResidualNaturality.FrameOn.scalarRadialDiv {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {c l : ℝ} {C : CorrectionState.Context D} {Cr : CorrectionState.Context E} {n nr : ℕ} (H : FrameOn U e c l (HarmonicResidual.contextFrame C n) (HarmonicResidual.contextFrame Cr nr)) (hU : IsOpen U) (hl : l ≠ 0) {a : ℝ} {f : MeanIncrementBounds.Field D} {g : MeanIncrementBounds.Field E} (hf : ScalarOn U e a (f n) (g nr)) (b : ℝ) : ScalarOn U e (a * l) (C.operators.radialDiv b f n) (Cr.operators.radialDiv b g nr)

theorem NavierStokes.PhysicalResidualNaturality.FrameOn.scalarViscosity {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {c l : ℝ} {C : CorrectionState.Context D} {Cr : CorrectionState.Context E} {n nr : ℕ} (H : FrameOn U e c l (HarmonicResidual.contextFrame C n) (HarmonicResidual.contextFrame Cr nr)) (hU : IsOpen U) (hl : l ≠ 0) {a : ℝ} {f : MeanIncrementBounds.Field D} {g : MeanIncrementBounds.Field E} (hf : ScalarOn U e a (f n) (g nr)) (b : ℝ) : ScalarOn U e (a * c * l) (C.operators.viscosity b f n) (Cr.operators.viscosity b g nr)

theorem NavierStokes.PhysicalResidualNaturality.TripleOn.thetaRadial {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {c : ℝ} {n nr : ℕ} {b m : MeanIncrementBounds.Triple D} {br mr : MeanIncrementBounds.Triple E} (hb : TripleOn U e c b br n nr) (hm : TripleOn U e c m mr n nr) : ScalarOn U e (c * c) (MeanIncrementBounds.thetaRadial b m n) (MeanIncrementBounds.thetaRadial br mr nr)

theorem NavierStokes.PhysicalResidualNaturality.TripleOn.thetaAxial {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {c : ℝ} {n nr : ℕ} {b m : MeanIncrementBounds.Triple D} {br mr : MeanIncrementBounds.Triple E} (hb : TripleOn U e c b br n nr) (hm : TripleOn U e c m mr n nr) : ScalarOn U e (c * c) (MeanIncrementBounds.thetaAxial b m n) (MeanIncrementBounds.thetaAxial br mr nr)

theorem NavierStokes.PhysicalResidualNaturality.TripleOn.axialRadial {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {c : ℝ} {n nr : ℕ} {b m : MeanIncrementBounds.Triple D} {br mr : MeanIncrementBounds.Triple E} (hb : TripleOn U e c b br n nr) (hm : TripleOn U e c m mr n nr) : ScalarOn U e (c * c) (MeanIncrementBounds.axialRadial b m n) (MeanIncrementBounds.axialRadial br mr nr)

theorem NavierStokes.PhysicalResidualNaturality.TripleOn.axialAxial {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {c : ℝ} {n nr : ℕ} {b m : MeanIncrementBounds.Triple D} {br mr : MeanIncrementBounds.Triple E} (hb : TripleOn U e c b br n nr) (hm : TripleOn U e c m mr n nr) : ScalarOn U e (c * c) (MeanIncrementBounds.axialAxial b m n) (MeanIncrementBounds.axialAxial br mr nr)

theorem NavierStokes.PhysicalResidualNaturality.TripleOn.radialRadial {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {c : ℝ} {n nr : ℕ} {b m : MeanIncrementBounds.Triple D} {br mr : MeanIncrementBounds.Triple E} (hb : TripleOn U e c b br n nr) (hm : TripleOn U e c m mr n nr) : ScalarOn U e (c * c) (MeanIncrementBounds.radialRadial b m n) (MeanIncrementBounds.radialRadial br mr nr)

theorem NavierStokes.PhysicalResidualNaturality.TripleOn.radialAngular {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {c : ℝ} {n nr : ℕ} {b m : MeanIncrementBounds.Triple D} {br mr : MeanIncrementBounds.Triple E} (hb : TripleOn U e c b br n nr) (hm : TripleOn U e c m mr n nr) : ScalarOn U e (c * c) (MeanIncrementBounds.radialAngular b m n) (MeanIncrementBounds.radialAngular br mr nr)

theorem NavierStokes.PhysicalResidualNaturality.TripleOn.complexValue {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {c : ℝ} {n nr : ℕ} {b : MeanIncrementBounds.Triple D} {br : MeanIncrementBounds.Triple E} (H : TripleOn U e c b br n nr) (x : D) (hx : x ∈ U) : ![↑(b.radial n x), ↑(b.angular n x), ↑(b.axial n x)] = c • ![↑(br.radial nr (e x)), ↑(br.angular nr (e x)), ↑(br.axial nr (e x))]

structure NavierStokes.PhysicalResidualNaturality.ContextOn {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (U : Set D) (e : D ≃L[ℝ] E) (c l : ℝ) (C : CorrectionState.Context D) (Cr : CorrectionState.Context E) (n nr : ℕ) : Prop

Context coherence includes the actual virtual stress fields, not just the velocity carried by a state.

• frame : FrameOn U e c l (HarmonicResidual.contextFrame C n) (HarmonicResidual.contextFrame Cr nr)
• base : TripleOn U e c C.base Cr.base n nr
• virtualTheta : ScalarOn U e (c * c) (C.virtualTheta n) (Cr.virtualTheta nr)
• virtualAxial : ScalarOn U e (c * c) (C.virtualAxial n) (Cr.virtualAxial nr)

theorem NavierStokes.PhysicalResidualNaturality.StateOn.thetaResidual {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {c l : ℝ} {C : CorrectionState.Context D} {Cr : CorrectionState.Context E} {s : CorrectionState.State D} {r : CorrectionState.State E} {n nr : ℕ} (H : StateOn U e c l s r n nr) (G : ContextOn U e c l C Cr n nr) (hU : IsOpen U) (hl : l ≠ 0) : ScalarOn U e (c * c * l) (s.thetaResidual C n) (r.thetaResidual Cr nr)

Naturality of the genuine angular mean residual, including the recomputed covariance and virtual stress divergence.

theorem NavierStokes.PhysicalResidualNaturality.StateOn.axialResidual {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {c l : ℝ} {C : CorrectionState.Context D} {Cr : CorrectionState.Context E} {s : CorrectionState.State D} {r : CorrectionState.State E} {n nr : ℕ} (H : StateOn U e c l s r n nr) (G : ContextOn U e c l C Cr n nr) (hU : IsOpen U) (hl : l ≠ 0) : ScalarOn U e (c * c * l) (s.axialResidual C n) (r.axialResidual Cr nr)

Naturality of the genuine axial mean residual, with pressure retained.

theorem NavierStokes.PhysicalResidualNaturality.StateOn.gr {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {c l : ℝ} {C : CorrectionState.Context D} {Cr : CorrectionState.Context E} {s : CorrectionState.State D} {r : CorrectionState.State E} {n nr : ℕ} (H : StateOn U e c l s r n nr) (G : ContextOn U e c l C Cr n nr) (hU : IsOpen U) (hl : l ≠ 0) : ScalarOn U e (c * c * l) (s.gr C n) (r.gr Cr nr)

theorem NavierStokes.PhysicalResidualNaturality.StateOn.radialResidual {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {c l : ℝ} {C : CorrectionState.Context D} {Cr : CorrectionState.Context E} {s : CorrectionState.State D} {r : CorrectionState.State E} {n nr : ℕ} (H : StateOn U e c l s r n nr) (G : ContextOn U e c l C Cr n nr) (hU : IsOpen U) (hl : l ≠ 0) : ScalarOn U e (c * c * l) (s.radialResidual C n) (r.radialResidual Cr nr)

theorem NavierStokes.PhysicalResidualNaturality.StateOn.reducedMeanResidual {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {c l : ℝ} {C : CorrectionState.Context D} {Cr : CorrectionState.Context E} {s : CorrectionState.State D} {r : CorrectionState.State E} {n nr : ℕ} (H : StateOn U e c l s r n nr) (G : ContextOn U e c l C Cr n nr) (hU : IsOpen U) (hl : l ≠ 0) (i : Fin 3) : ScalarOn U e (c * c * l) (fun (x : D) => s.reducedMeanResidual C n x i) fun (x : E) => r.reducedMeanResidual Cr nr x i

theorem NavierStokes.PhysicalResidualNaturality.StateOn.source {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {c l : ℝ} {C : CorrectionState.Context D} {Cr : CorrectionState.Context E} {s : CorrectionState.State D} {r : CorrectionState.State E} {n nr : ℕ} (H : StateOn U e c l s r n nr) (G : ContextOn U e c l C Cr n nr) (hU : IsOpen U) (hl : l ≠ 0) {b : CorrectionState.HarmonicBlock D} {br : CorrectionState.HarmonicBlock E} {ga al : HarmonicResidual.BlockCoefficients D} {gar alr : HarmonicResidual.BlockCoefficients E} (hb : BlockFieldsOn U e c l b br ga al gar alr n nr) (j : ℤ) {x : D} (hx : x ∈ U) : ParticularWaveAssembly.residualSource C s b ga al j n x = (c * c * l) • ParticularWaveAssembly.residualSource Cr r br gar alr j nr (e x)

theorem NavierStokes.PhysicalResidualNaturality.angularAverage_on {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {a : ℝ} {f : CorrectionState.OscillatoryScalar D} {g : CorrectionState.OscillatoryScalar E} {n nr : ℕ} (hf : ∀ x ∈ U, ∀ (theta : ℝ), f n (x, theta) = a * g nr (e x, theta)) : ScalarOn U e a (CorrectionState.angularAverage f n) (CorrectionState.angularAverage g nr)

theorem NavierStokes.PhysicalResidualNaturality.StateOn.meanBaseError {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {c l : ℝ} {s : CorrectionState.State D} {r : CorrectionState.State E} {n nr : ℕ} (H : StateOn U e c l s r n nr) (i : Fin 3) : ScalarOn U e (c * c * l) (fun (x : D) => s.meanBaseError n x i) fun (x : E) => r.meanBaseError nr x i

theorem NavierStokes.PhysicalResidualNaturality.StateOn.meanExcluded {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {c l : ℝ} {s : CorrectionState.State D} {r : CorrectionState.State E} {n nr : ℕ} (H : StateOn U e c l s r n nr) (i : Fin 3) : ScalarOn U e (c * c * l) (fun (x : D) => s.meanExcluded n x i) fun (x : E) => r.meanExcluded nr x i

theorem NavierStokes.PhysicalResidualNaturality.StateOn.meanResidual {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {c l : ℝ} {C : CorrectionState.Context D} {Cr : CorrectionState.Context E} {s : CorrectionState.State D} {r : CorrectionState.State E} {n nr : ℕ} (H : StateOn U e c l s r n nr) (G : ContextOn U e c l C Cr n nr) (hU : IsOpen U) (hl : l ≠ 0) (i : Fin 3) : ScalarOn U e (c * c * l) (fun (x : D) => s.meanResidual C n x i) fun (x : E) => r.meanResidual Cr nr x i

theorem NavierStokes.PhysicalResidualNaturality.StateOn.meanGoodResidual {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {e : D ≃L[ℝ] E} {c l : ℝ} {C : CorrectionState.Context D} {Cr : CorrectionState.Context E} {s : CorrectionState.State D} {r : CorrectionState.State E} {n nr : ℕ} (H : StateOn U e c l s r n nr) (G : ContextOn U e c l C Cr n nr) (hU : IsOpen U) (hl : l ≠ 0) (i : Fin 3) : ScalarOn U e (c * c * l) (fun (x : D) => s.meanGoodResidual C n x i) fun (x : E) => r.meanGoodResidual Cr nr x i

Literal reference views of one state

noncomputable def NavierStokes.PhysicalResidualNaturality.stateView {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : ℕ → D ≃L[ℝ] E) (c l : ℕ → ℝ) (r : CorrectionState.State E) (nr : ℕ) : CorrectionState.State D

The state is stored once on the reference lift. Band values are constructed by pullback, rather than chosen independently.

Equations

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

theorem NavierStokes.PhysicalResidualNaturality.stateView_coherent {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : ℕ → D ≃L[ℝ] E) (c l : ℕ → ℝ) (r : CorrectionState.State E) (nr n : ℕ) (U : Set D) : StateOn U (e n) (c n) (l n) (stateView e c l r nr) r n nr

theorem NavierStokes.PhysicalResidualNaturality.stateView_addIncrement {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : ℕ → D ≃L[ℝ] E) (c l : ℕ → ℝ) (r w : CorrectionState.State E) (nr : ℕ) : stateView e c l (r.addIncrement w.mean w.pressure w.oscillation w.oscillatoryPressure w.errors) nr = (stateView e c l r nr).addIncrement (stateView e c l w nr).mean (stateView e c l w nr).pressure (stateView e c l w nr).oscillation (stateView e c l w nr).oscillatoryPressure (stateView e c l w nr).errors

Pullback commutes with the actual additive state update.