Angular invariance of constructed stripped copy and curl coefficients

Only primitive translation identities are assumed. The actual copy solve, its pressure, and the stripped cylindrical curl inherit those identities. The oscillatory carrier retains its separate angular character.

noncomputable def NavierStokes.CopyAngularInvariance.Invariant {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (θ : D) {E : Type} (f : D → E) : Prop

Invariant, given by ∀ (x : D) (t : ℝ), f (x + t • θ) = f x.

Equations

• NavierStokes.CopyAngularInvariance.Invariant θ f = ∀ (x : D) (t : ℝ), f (x + t • θ) = f x

noncomputable def NavierStokes.CopyAngularInvariance.AffinePhase {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (θ : D) (m : ℝ) (Φ : D → ℝ) : Prop

Affine phase, given by ∀ (x : D) (t : ℝ), Φ (x + t • θ) = Φ x + m * t.

Equations

• NavierStokes.CopyAngularInvariance.AffinePhase θ m Φ = ∀ (x : D) (t : ℝ), Φ (x + t • θ) = Φ x + m * t

theorem NavierStokes.CopyAngularInvariance.Invariant.const {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {θ : D} {E : Type} (e : E) : Invariant θ fun (x : D) => e

theorem NavierStokes.CopyAngularInvariance.Invariant.map {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {θ : D} {E F : Type} {f : D → E} (hf : Invariant θ f) (T : E → F) : Invariant θ fun (x : D) => T (f x)

theorem NavierStokes.CopyAngularInvariance.Invariant.map₂ {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {θ : D} {E F G : Type} {f : D → E} {g : D → F} (hf : Invariant θ f) (hg : Invariant θ g) (T : E → F → G) : Invariant θ fun (x : D) => T (f x) (g x)

theorem NavierStokes.CopyAngularInvariance.Invariant.component {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {θ : D} {ι : Type} {F : ι → Type} {f : D → (i : ι) → F i} (hf : Invariant θ f) (i : ι) : Invariant θ fun (x : D) => f x i

theorem NavierStokes.CopyAngularInvariance.Invariant.tsum_invariant {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {θ : D} {E : Type} [NormedAddCommGroup E] {ι : Type} {f : ι → D → E} (hf : ∀ (i : ι), Invariant θ (f i)) : Invariant θ fun (x : D) => ∑' (i : ι), f i x

theorem NavierStokes.CopyAngularInvariance.Invariant.fderiv_invariant {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {θ : D} {E : Type} {f : D → E} [NormedAddCommGroup E] [NormedSpace ℝ E] (hf : Invariant θ f) : Invariant θ (fderiv ℝ f)

Translation covariance of the actual Fréchet derivative, including its canonical zero value when the original function is not differentiable.

theorem NavierStokes.CopyAngularInvariance.Invariant.iteratedFDeriv_invariant {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {θ : D} {E : Type} {f : D → E} [NormedAddCommGroup E] [NormedSpace ℝ E] (hf : Invariant θ f) (j : ℕ) : Invariant θ (iteratedFDeriv ℝ j f)

theorem NavierStokes.CopyAngularInvariance.Invariant.along {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {θ : D} {E : Type} {f : D → E} [NormedAddCommGroup E] [NormedSpace ℝ E] {V : D → D} (hf : Invariant θ f) (hV : Invariant θ V) : Invariant θ (HarmonicCalculus.along V f)

theorem NavierStokes.CopyAngularInvariance.Invariant.directional_zero {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {θ : D} {E : Type} {f : D → E} [NormedAddCommGroup E] [NormedSpace ℝ E] (hf : Invariant θ f) (x : D) : (fderiv ℝ f x) θ = 0

theorem NavierStokes.CopyAngularInvariance.Invariant.along_zero {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {θ : D} {E : Type} {f : D → E} [NormedAddCommGroup E] [NormedSpace ℝ E] (hf : Invariant θ f) (x : D) : HarmonicCalculus.along (fun (x : D) => θ) f x = 0

theorem NavierStokes.CopyAngularInvariance.AffinePhase.fderiv_invariant {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {θ : D} {m : ℝ} {Φ : D → ℝ} (hΦ : AffinePhase θ m Φ) : Invariant θ (fderiv ℝ Φ)

theorem NavierStokes.CopyAngularInvariance.AffinePhase.along_invariant {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {θ : D} {m : ℝ} {Φ : D → ℝ} (hΦ : AffinePhase θ m Φ) {V : D → D} (hV : Invariant θ V) : Invariant θ (HarmonicCalculus.along V Φ)

theorem NavierStokes.CopyAngularInvariance.AffinePhase.directional_eq {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {θ : D} {m : ℝ} {Φ : D → ℝ} (hΦ : AffinePhase θ m Φ) {x : D} (hd : DifferentiableAt ℝ Φ x) : (fderiv ℝ Φ x) θ = m

Actual copy solves under angular translation of the slow parameter

theorem NavierStokes.CopyAngularInvariance.slow_shift_apply {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {F : Type} {f : P × TorusInverse.Plane → F} {θ : P} (hf : Invariant (θ, 0) f) (p : P) (Y : TorusInverse.Plane) (t : ℝ) : f (p + t • θ, Y) = f (p, Y)

theorem NavierStokes.CopyAngularInvariance.anchoredSolve_invariant {P V E : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : CommonCoverSolve.LinearData P V E) (g : CommonCoverSolve.Geometry) (hab : a ≤ b) (θ : P) (hA : Invariant (θ, 0) d.coefficient) (hB : Invariant (θ, 0) d.forcingMap) (hf : Invariant (θ, 0) d.source) (j : TorusInverse.Frequency) (s : ℝ) : Invariant (θ, 0) fun (x : P × TorusInverse.Plane) => d.anchoredSolve g hab j x s

theorem NavierStokes.CopyAngularInvariance.copySolve_invariant {P V E : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : CommonCoverSolve.LinearData P V E) (g : CommonCoverSolve.Geometry) (hab : a ≤ b) (θ : P) (hA : Invariant (θ, 0) d.coefficient) (hB : Invariant (θ, 0) d.forcingMap) (hf : Invariant (θ, 0) d.source) (j : TorusInverse.Frequency) : Invariant (θ, 0) (d.copySolve g hab j)

theorem NavierStokes.CopyAngularInvariance.localizedCopy_invariant {P V E : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : CommonCoverSolve.LinearData P V E) (g : CommonCoverSolve.Geometry) (hab : a ≤ b) (θ : P) (hA : Invariant (θ, 0) d.coefficient) (hB : Invariant (θ, 0) d.forcingMap) (hf : Invariant (θ, 0) d.source) (κ : TorusInverse.Plane → ℝ) (j : TorusInverse.Frequency) : Invariant (θ, 0) (d.localizedCopy g hab κ j)

theorem NavierStokes.CopyAngularInvariance.commonSolve_invariant {P V E : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : CommonCoverSolve.LinearData P V E) (g : CommonCoverSolve.Geometry) (hab : a ≤ b) (θ : P) (hA : Invariant (θ, 0) d.coefficient) (hB : Invariant (θ, 0) d.forcingMap) (hf : Invariant (θ, 0) d.source) (κ : TorusInverse.Plane → ℝ) : Invariant (θ, 0) (d.commonSolve g hab κ)

theorem NavierStokes.CopyAngularInvariance.copySolve_angular_zero {P V E : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : CommonCoverSolve.LinearData P V E) (g : CommonCoverSolve.Geometry) (hab : a ≤ b) (θ : P) (hA : Invariant (θ, 0) d.coefficient) (hB : Invariant (θ, 0) d.forcingMap) (hf : Invariant (θ, 0) d.source) (j : TorusInverse.Frequency) (x : P × TorusInverse.Plane) : HarmonicCalculus.along (fun (x : P × TorusInverse.Plane) => (θ, 0)) (d.copySolve g hab j) x = 0

Tangent data and the actual pressure formula

structure NavierStokes.CopyAngularInvariance.TangentInvariant {P H : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup H] [InnerProductSpace ℝ H] (θ : P) (d : CommonCoverSolve.TangentData P H) : Prop

Tangent invariant data, collecting normal, normalDot, action, damping, source.

• normal : Invariant (θ, 0) d.normal
• normalDot : Invariant (θ, 0) d.normalDot
• action : Invariant (θ, 0) d.action
• damping : Invariant (θ, 0) d.damping
• source : Invariant (θ, 0) d.source

theorem NavierStokes.CopyAngularInvariance.TangentInvariant.coefficient {P H : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup H] [InnerProductSpace ℝ H] {θ : P} {d : CommonCoverSolve.TangentData P H} (h : TangentInvariant θ d) : Invariant (θ, 0) d.linearData.coefficient

theorem NavierStokes.CopyAngularInvariance.TangentInvariant.forcingMap {P H : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup H] [InnerProductSpace ℝ H] {θ : P} {d : CommonCoverSolve.TangentData P H} (h : TangentInvariant θ d) : Invariant (θ, 0) d.linearData.forcingMap

theorem NavierStokes.CopyAngularInvariance.TangentInvariant.copySolve_invariant {P H : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {a b : ℝ} {θ : P} {d : CommonCoverSolve.TangentData P H} (h : TangentInvariant θ d) (g : CommonCoverSolve.Geometry) (hab : a ≤ b) (j : TorusInverse.Frequency) : Invariant (θ, 0) (d.linearData.copySolve g hab j)

noncomputable def NavierStokes.CopyAngularInvariance.copyNativePoint {P : Type} (g : CommonCoverSolve.Geometry) (j : TorusInverse.Frequency) (x : P × TorusInverse.Plane) : P × TorusInverse.Plane

Copy native point, given by (x.1, g.coordinates j x.2).

Equations

• NavierStokes.CopyAngularInvariance.copyNativePoint g j x = (x.1, g.coordinates j x.2)

theorem NavierStokes.CopyAngularInvariance.native_invariant {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {F : Type} {θ : P} {f : P × TorusInverse.Plane → F} (hf : Invariant (θ, 0) f) (g : CommonCoverSolve.Geometry) (j : TorusInverse.Frequency) : Invariant (θ, 0) fun (x : P × TorusInverse.Plane) => f (copyNativePoint g j x)

noncomputable def NavierStokes.CopyAngularInvariance.copyPressureReal {P H : Type} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {a b : ℝ} (d : CommonCoverSolve.TangentData P H) (g : CommonCoverSolve.Geometry) (hab : a ≤ b) (j : TorusInverse.Frequency) (x : P × TorusInverse.Plane) : ℝ

Same scalar formula as the particular-wave pressure, evaluated on the constructed copy solve and the actual source at the current common point.

Equations

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

noncomputable def NavierStokes.CopyAngularInvariance.copyPressure {P H : Type} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {a b : ℝ} (d : CommonCoverSolve.TangentData P H) (g : CommonCoverSolve.Geometry) (hab : a ≤ b) (j : TorusInverse.Frequency) (K : ℝ) (x : P × TorusInverse.Plane) : ℂ

Copy pressure, given by Complex.I * (copyPressureReal d g hab j x : ℂ) / (K : ℂ).

Equations

• NavierStokes.CopyAngularInvariance.copyPressure d g hab j K x = Complex.I * ↑(NavierStokes.CopyAngularInvariance.copyPressureReal d g hab j x) / ↑K

theorem NavierStokes.CopyAngularInvariance.TangentInvariant.copyPressureReal_invariant {P H : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {a b : ℝ} {θ : P} {d : CommonCoverSolve.TangentData P H} (h : TangentInvariant θ d) (g : CommonCoverSolve.Geometry) (hab : a ≤ b) (j : TorusInverse.Frequency) : Invariant (θ, 0) (copyPressureReal d g hab j)

theorem NavierStokes.CopyAngularInvariance.TangentInvariant.copyPressure_invariant {P H : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {a b : ℝ} {θ : P} {d : CommonCoverSolve.TangentData P H} (h : TangentInvariant θ d) (g : CommonCoverSolve.Geometry) (hab : a ≤ b) (j : TorusInverse.Frequency) (K : ℝ) : Invariant (θ, 0) (copyPressure d g hab j K)

theorem NavierStokes.CopyAngularInvariance.TangentInvariant.copyPressure_angular_zero {P H : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {a b : ℝ} {θ : P} {d : CommonCoverSolve.TangentData P H} (h : TangentInvariant θ d) (g : CommonCoverSolve.Geometry) (hab : a ≤ b) (j : TorusInverse.Frequency) (K : ℝ) (x : P × TorusInverse.Plane) : HarmonicCalculus.along (fun (x : P × TorusInverse.Plane) => (θ, 0)) (copyPressure d g hab j K) x = 0

theorem NavierStokes.CopyAngularInvariance.nativeCutoff_invariant {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (θ : P) (g : CommonCoverSolve.Geometry) (κ : TorusInverse.Plane → ℝ) (j : TorusInverse.Frequency) : Invariant (θ, 0) fun (x : P × TorusInverse.Plane) => κ (g.coordinates j x.2)

noncomputable def NavierStokes.CopyAngularInvariance.commonPressure {P H : Type} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {a b : ℝ} (d : CommonCoverSolve.TangentData P H) (g : CommonCoverSolve.Geometry) (hab : a ≤ b) (κ : TorusInverse.Plane → ℝ) (K : ℝ) (x : P × TorusInverse.Plane) : ℂ

Common pressure, given by ∑' j : Frequency, (κ (g.coordinates j x.2) : ℂ) * copyPressure d g hab j K x.

Equations

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

theorem NavierStokes.CopyAngularInvariance.TangentInvariant.commonPressure_invariant {P H : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {a b : ℝ} {θ : P} {d : CommonCoverSolve.TangentData P H} (h : TangentInvariant θ d) (g : CommonCoverSolve.Geometry) (hab : a ≤ b) (κ : TorusInverse.Plane → ℝ) (K : ℝ) : Invariant (θ, 0) (commonPressure d g hab κ K)

theorem NavierStokes.CopyAngularInvariance.TangentInvariant.commonPressure_angular_zero {P H : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {a b : ℝ} {θ : P} {d : CommonCoverSolve.TangentData P H} (h : TangentInvariant θ d) (g : CommonCoverSolve.Geometry) (hab : a ≤ b) (κ : TorusInverse.Plane → ℝ) (K : ℝ) (x : P × TorusInverse.Plane) : HarmonicCalculus.along (fun (x : P × TorusInverse.Plane) => (θ, 0)) (commonPressure d g hab κ K) x = 0

Invariance of the actual stripped cylindrical curl

theorem NavierStokes.CopyAngularInvariance.phaseNormal_invariant {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {θ : D} {R : D → ℝ} {Vr Vθ Vz : D → D} {Φ : D → ℝ} {m : ℝ} (hR : Invariant θ R) (hr : Invariant θ Vr) (hθ : Invariant θ Vθ) (hz : Invariant θ Vz) (hΦ : AffinePhase θ m Φ) : Invariant θ (HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ)

theorem NavierStokes.CopyAngularInvariance.coefficient_invariant {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {θ : D} {R : D → ℝ} {Vr Vθ Vz : D → D} {Φ : D → ℝ} {m : ℝ} {a : D → CurlClassBounds.ComplexVector} (hR : Invariant θ R) (hr : Invariant θ Vr) (hθ : Invariant θ Vθ) (hz : Invariant θ Vz) (hΦ : AffinePhase θ m Φ) (ha : Invariant θ a) : Invariant θ (CurlClassBounds.coefficient R Vr Vθ Vz Φ a)

theorem NavierStokes.CopyAngularInvariance.cylindricalCurl_invariant {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {θ : D} {R : D → ℝ} {Vr Vθ Vz : D → D} {a : D → CurlClassBounds.ComplexVector} (hR : Invariant θ R) (hr : Invariant θ Vr) (hθ : Invariant θ Vθ) (hz : Invariant θ Vz) (ha : Invariant θ a) : Invariant θ (CurlClassBounds.cylindricalCurl R Vr Vθ Vz a)

theorem NavierStokes.CopyAngularInvariance.curlRemainder_invariant {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {θ : D} {R : D → ℝ} {Vr Vθ Vz : D → D} {a : D → CurlClassBounds.ComplexVector} (hR : Invariant θ R) (hr : Invariant θ Vr) (hθ : Invariant θ Vθ) (hz : Invariant θ Vz) (ha : Invariant θ a) (K : ℝ) : Invariant θ (CurlClassBounds.curlRemainder K R Vr Vθ Vz a)

theorem NavierStokes.CopyAngularInvariance.realizedCoefficient_invariant {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {θ : D} {R : D → ℝ} {Vr Vθ Vz : D → D} {Φ : D → ℝ} {m : ℝ} {a : D → CurlClassBounds.ComplexVector} (hR : Invariant θ R) (hr : Invariant θ Vr) (hθ : Invariant θ Vθ) (hz : Invariant θ Vz) (hΦ : AffinePhase θ m Φ) (ha : Invariant θ a) (K : ℝ) : Invariant θ (CurlClassBounds.realizedCoefficient K R Vr Vθ Vz Φ a)

theorem NavierStokes.CopyAngularInvariance.realizedCoefficient_angular_zero {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {θ : D} {R : D → ℝ} {Vr Vθ Vz : D → D} {Φ : D → ℝ} {m : ℝ} {a : D → CurlClassBounds.ComplexVector} (hR : Invariant θ R) (hr : Invariant θ Vr) (hθ : Invariant θ Vθ) (hz : Invariant θ Vz) (hΦ : AffinePhase θ m Φ) (ha : Invariant θ a) (K : ℝ) (i : Fin 3) (x : D) : HarmonicCalculus.along (fun (x : D) => θ) (fun (y : D) => CurlClassBounds.realizedCoefficient K R Vr Vθ Vz Φ a y i) x = 0

theorem NavierStokes.CopyAngularInvariance.actualCopy_realizedCoefficient_invariant {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {θ : P} {d : CommonCoverSolve.TangentData P CurlClassBounds.RealVector} {a b : ℝ} (hd : TangentInvariant θ d) (g : CommonCoverSolve.Geometry) (hab : a ≤ b) (j : TorusInverse.Frequency) {R ψ : P × TorusInverse.Plane → ℝ} {Vr Vz : P × TorusInverse.Plane → P × TorusInverse.Plane} {Φ : P × TorusInverse.Plane → ℝ} {m : ℝ} (hR : Invariant (θ, 0) R) (hψ : Invariant (θ, 0) ψ) (hr : Invariant (θ, 0) Vr) (hz : Invariant (θ, 0) Vz) (hΦ : AffinePhase (θ, 0) m Φ) (K : ℝ) : Invariant (θ, 0) (CurlClassBounds.realizedCoefficient K R Vr (fun (x : P × TorusInverse.Plane) => (θ, 0)) Vz Φ fun (x : P × TorusInverse.Plane) => ψ x • CurlClassBounds.complexify (d.linearData.copySolve g hab j x))

The amplitude premise of the curl invariance theorem is discharged by the actual tangent copy solve and invariant scalar mask.

The carrier has its angular character; only the coefficient is invariant

theorem NavierStokes.CopyAngularInvariance.carrier_translate {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {θ : D} {Φ : D → ℝ} {m : ℝ} (hΦ : AffinePhase θ m Φ) (K : ℝ) (x : D) (t : ℝ) : HarmonicCalculus.carrier K Φ (x + t • θ) = Complex.exp (HarmonicCalculus.phaseFactor K * ↑(m * t)) * HarmonicCalculus.carrier K Φ x

theorem NavierStokes.CopyAngularInvariance.mode_translate {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {θ : D} {Φ : D → ℝ} {m : ℝ} {a : D → ℂ} (ha : Invariant θ a) (hΦ : AffinePhase θ m Φ) (K : ℝ) (x : D) (t : ℝ) : HarmonicCalculus.mode K Φ a (x + t • θ) = Complex.exp (HarmonicCalculus.phaseFactor K * ↑(m * t)) * HarmonicCalculus.mode K Φ a x

theorem NavierStokes.CopyAngularInvariance.vectorMode_translate {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {θ : D} {Φ : D → ℝ} {m : ℝ} {a : D → HarmonicCalculus.ComplexVector} (ha : Invariant θ a) (hΦ : AffinePhase θ m Φ) (K : ℝ) (x : D) (t : ℝ) : HarmonicCalculus.vectorMode K Φ a (x + t • θ) = Complex.exp (HarmonicCalculus.phaseFactor K * ↑(m * t)) • HarmonicCalculus.vectorMode K Φ a x

theorem NavierStokes.CopyAngularInvariance.mode_eq_field_along {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {θ : D} {Φ : D → ℝ} {m : ℝ} {P : Type} {f : D → ℂ} (hf : Invariant θ f) (hΦ : AffinePhase θ m Φ) (σ : P → D) (k : ℝ) (j kp : ℤ) (hkp : ↑kp = k * m) (p : P) (t : ℝ) : HarmonicCalculus.mode (↑j * k) Φ f (σ p + t • θ) = HarmonicFields.field (AddMonoidAlgebra.single j fun (p : P) => f (σ p)) k (fun (p : P) => Φ (σ p)) kp (p, t)

This version works with any chosen angular section, independently of where the angular coordinate is stored in a product type.

theorem NavierStokes.CopyAngularInvariance.vectorMode_eq_field_along_component {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {θ : D} {Φ : D → ℝ} {m : ℝ} {P : Type} {a : D → HarmonicCalculus.ComplexVector} (ha : Invariant θ a) (hΦ : AffinePhase θ m Φ) (σ : P → D) (k : ℝ) (j kp : ℤ) (hkp : ↑kp = k * m) (p : P) (t : ℝ) (i : Fin 3) : HarmonicCalculus.vectorMode (↑j * k) Φ a (σ p + t • θ) i = HarmonicFields.field (AddMonoidAlgebra.single j fun (p : P) => a (σ p) i) k (fun (p : P) => Φ (σ p)) kp (p, t)

theorem NavierStokes.CopyAngularInvariance.invariant_eq_zeroSlice {P E : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {f : P × ℝ → E} (hf : Invariant (0, 1) f) (p : P) (t : ℝ) : f (p, t) = f (p, 0)

theorem NavierStokes.CopyAngularInvariance.affinePhase_eq_zeroSlice {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {Φ : P × ℝ → ℝ} {m : ℝ} (hΦ : AffinePhase (0, 1) m Φ) (p : P) (t : ℝ) : Φ (p, t) = Φ (p, 0) + m * t

theorem NavierStokes.CopyAngularInvariance.mode_eq_field_single {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {f : P × ℝ → ℂ} {Φ : P × ℝ → ℝ} {m : ℝ} (hf : Invariant (0, 1) f) (hΦ : AffinePhase (0, 1) m Φ) (k : ℝ) (j kp : ℤ) (hkp : ↑kp = k * m) (p : P) (t : ℝ) : HarmonicCalculus.mode (↑j * k) Φ f (p, t) = HarmonicFields.field (AddMonoidAlgebra.single j fun (p : P) => f (p, 0)) k (fun (p : P) => Φ (p, 0)) kp (p, t)

The true full coefficient is equal to its zero-angle slice. The carrier then agrees exactly with the existing finite-harmonic field constructor.

ExactConditions for the actual corrected coefficient

theorem NavierStokes.CopyAngularInvariance.base_invariant {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {θ : D} {R b F G : D → ℝ} (hR : Invariant θ R) (hb : Invariant θ b) (hF : Invariant θ F) (hG : Invariant θ G) : Invariant θ (LinearWaveResidual.base R b F G)

theorem NavierStokes.CopyAngularInvariance.exactConditions_of_invariants {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {d : LinearWaveBounds.GraphDirections D} {a : LinearWaveBounds.WaveCoefficients D} (hΦs : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (a.phase n) s.domain) (hRne : ∀ (n : ℕ), ∀ x ∈ s.domain, a.radius n x ≠ 0) (hDrR : ∀ (n : ℕ), ∀ x ∈ s.domain, HarmonicCalculus.along (d.radialField n) (a.radius n) x = 1) (hR : ∀ (n : ℕ), Invariant d.angular (a.radius n)) (hb : ∀ (n : ℕ), Invariant d.angular (a.radialBase n)) (hF : ∀ (n : ℕ), Invariant d.angular (a.frequencyBase n)) (hG : ∀ (n : ℕ), Invariant d.angular (a.axialBase n)) (hΦ : ∀ (n : ℕ), ∃ (m : ℝ), AffinePhase d.angular m (a.phase n)) (ha : ∀ (n : ℕ), Invariant d.angular (a.amplitude n)) (hp : ∀ (n : ℕ), Invariant d.angular (a.pressure n)) : LinearWaveBounds.ExactConditions s d a

theorem NavierStokes.CopyAngularInvariance.corrected_amplitude_invariant {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {d : LinearWaveBounds.GraphDirections D} {a : LinearWaveBounds.WaveCoefficients D} (ψ : ℕ → D → ℝ) (hR : ∀ (n : ℕ), Invariant d.angular (a.radius n)) (hr : ∀ (n : ℕ), Invariant d.angular (d.radialField n)) (hz : ∀ (n : ℕ), Invariant d.angular (d.axialField s n)) (hΦ : ∀ (n : ℕ), ∃ (m : ℝ), AffinePhase d.angular m (a.phase n)) (ha : ∀ (n : ℕ), Invariant d.angular (a.amplitude n)) (hψ : ∀ (n : ℕ), Invariant d.angular (ψ n)) (n : ℕ) : Invariant d.angular ((a.corrected s d ψ).amplitude n)

theorem NavierStokes.CopyAngularInvariance.corrected_pressure_invariant {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {d : LinearWaveBounds.GraphDirections D} {a : LinearWaveBounds.WaveCoefficients D} (ψ : ℕ → D → ℝ) (hp : ∀ (n : ℕ), Invariant d.angular (a.pressure n)) (hψ : ∀ (n : ℕ), Invariant d.angular (ψ n)) (n : ℕ) : Invariant d.angular ((a.corrected s d ψ).pressure n)

theorem NavierStokes.CopyAngularInvariance.exactConditions_corrected_of_invariants {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {d : LinearWaveBounds.GraphDirections D} {a : LinearWaveBounds.WaveCoefficients D} (ψ : ℕ → D → ℝ) (hΦs : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (a.phase n) s.domain) (hRne : ∀ (n : ℕ), ∀ x ∈ s.domain, a.radius n x ≠ 0) (hDrR : ∀ (n : ℕ), ∀ x ∈ s.domain, HarmonicCalculus.along (d.radialField n) (a.radius n) x = 1) (hR : ∀ (n : ℕ), Invariant d.angular (a.radius n)) (hb : ∀ (n : ℕ), Invariant d.angular (a.radialBase n)) (hF : ∀ (n : ℕ), Invariant d.angular (a.frequencyBase n)) (hG : ∀ (n : ℕ), Invariant d.angular (a.axialBase n)) (hr : ∀ (n : ℕ), Invariant d.angular (d.radialField n)) (hz : ∀ (n : ℕ), Invariant d.angular (d.axialField s n)) (hΦ : ∀ (n : ℕ), ∃ (m : ℝ), AffinePhase d.angular m (a.phase n)) (ha : ∀ (n : ℕ), Invariant d.angular (a.amplitude n)) (hp : ∀ (n : ℕ), Invariant d.angular (a.pressure n)) (hψ : ∀ (n : ℕ), Invariant d.angular (ψ n)) : LinearWaveBounds.ExactConditions s d (a.corrected s d ψ)