Particular waves from the actual forced copy-path solve

The estimates below apply to the Volterra solution itself. Endpoint rescaling proves bounds for full joint derivatives, so no fixed-time to joint-smoothness inference or assumed output class is used. The source envelope stays explicit along the whole integration path.

The reconstructed forced solution is the actual copy solve

The frame is reindexed along the native transverse coordinate of each copy, while the physical source is evaluated on the lifted earlier path. Uniqueness identifies the two constructed solutions from their common zero entry value. No energy inequality for the ambient projected operator is assumed.

@[reducible, inline]

abbrev NavierStokes.PrimaryCopyBridge.Plane : Type

Plane: an abbreviation for TorusInverse.Plane.

Equations

• NavierStokes.PrimaryCopyBridge.Plane = NavierStokes.TorusInverse.Plane

@[reducible, inline]

abbrev NavierStokes.PrimaryCopyBridge.Frequency : Type

Frequency: an abbreviation for TorusInverse.Frequency.

Equations

• NavierStokes.PrimaryCopyBridge.Frequency = NavierStokes.TorusInverse.Frequency

@[reducible, inline]

abbrev NavierStokes.PrimaryCopyBridge.State : Type

State: an abbreviation for PrimaryODE.State.

Equations

• NavierStokes.PrimaryCopyBridge.State = NavierStokes.PrimaryODE.State

@[reducible, inline]

abbrev NavierStokes.PrimaryCopyBridge.Space : Type

Space: an abbreviation for PrimaryODE.Space /-! ## Exact reindexing of primitive frame data -/.

Equations

• NavierStokes.PrimaryCopyBridge.Space = NavierStokes.PrimaryODE.Space

Exact reindexing of primitive frame data

noncomputable def NavierStokes.PrimaryCopyBridge.reindex {P Q : Type} (d : PrimaryODE.FrameData P) (φ : Q → P) : PrimaryODE.FrameData Q

Reindex, bundling beta, betaDot, rho, rhoDot and the required compatibility proofs.

Equations

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

theorem NavierStokes.PrimaryCopyBridge.reindex_kinematics {P Q : Type} (d : PrimaryODE.FrameData P) (φ : Q → P) {q : Q} {I : Set ℝ} (h : d.Kinematics (φ q) I) : (reindex d φ).Kinematics q I

noncomputable def NavierStokes.PrimaryCopyBridge.copyParameter {P : Type} (g : CommonCoverSolve.Geometry) (k : Frequency) (q : P × Plane) : P × ℝ

Copy parameter, given by (q.1, (g.coordinates k q.2).1).

Equations

• NavierStokes.PrimaryCopyBridge.copyParameter g k q = (q.1, (g.coordinates k q.2).1)

noncomputable def NavierStokes.PrimaryCopyBridge.copyFrame {P : Type} (d : PrimaryODE.FrameData (P × ℝ)) (g : CommonCoverSolve.Geometry) (k : Frequency) : PrimaryODE.FrameData (P × Plane)

Copy frame, given by reindex d (copyParameter g k).

Equations

• NavierStokes.PrimaryCopyBridge.copyFrame d g k = NavierStokes.PrimaryCopyBridge.reindex d (NavierStokes.PrimaryCopyBridge.copyParameter g k)

noncomputable def NavierStokes.PrimaryCopyBridge.copySource {P : Type} (f : P × Plane → Space) (g : CommonCoverSolve.Geometry) (k : Frequency) (z : (P × Plane) × ℝ) : Space

Copy source, given by f (z.1.1, g.path k z.1.2 z.2).

Equations

• NavierStokes.PrimaryCopyBridge.copySource f g k z = f (z.1.1, g.path k z.1.2 z.2)

@[simp]

theorem NavierStokes.PrimaryCopyBridge.copyFrame_normal {P : Type} (d : PrimaryODE.FrameData (P × ℝ)) (g : CommonCoverSolve.Geometry) (k : Frequency) (z : (P × Plane) × ℝ) : (copyFrame d g k).normal z = d.normal (copyParameter g k z.1, z.2)

@[simp]

theorem NavierStokes.PrimaryCopyBridge.copyFrame_normalMotion {P : Type} (d : PrimaryODE.FrameData (P × ℝ)) (g : CommonCoverSolve.Geometry) (k : Frequency) (z : (P × Plane) × ℝ) : (copyFrame d g k).normalMotion z = d.normalMotion (copyParameter g k z.1, z.2)

@[simp]

theorem NavierStokes.PrimaryCopyBridge.copyFrame_ambient {P : Type} (d : PrimaryODE.FrameData (P × ℝ)) (g : CommonCoverSolve.Geometry) (k : Frequency) (z : (P × Plane) × ℝ) (w : State) : (copyFrame d g k).ambient z w = d.ambient (copyParameter g k z.1, z.2) w

theorem NavierStokes.PrimaryCopyBridge.ambient_zero {P : Type} (d : PrimaryODE.FrameData P) (z : P × ℝ) : d.ambient z 0 = 0

The native tangent data can be built directly from the frame

noncomputable def NavierStokes.PrimaryCopyBridge.baseOperator (F : ℝ) (g : State) : Space →L[ℝ] Space

Base operator, constructed using MovingFrameODE.packCLM.comp.

Equations

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

@[simp]

theorem NavierStokes.PrimaryCopyBridge.baseOperator_apply (F : ℝ) (g : State) (x : Space) : (baseOperator F g) x = MovingFrameODE.baseAction F g x

noncomputable def NavierStokes.PrimaryCopyBridge.nativePoint {P : Type} (z : P × Plane) : (P × ℝ) × ℝ

Native point, given by ((z.1, z.2.1), z.2.2).

Equations

• NavierStokes.PrimaryCopyBridge.nativePoint z = ((z.1, z.2.1), z.2.2)

noncomputable def NavierStokes.PrimaryCopyBridge.frameTangentData {P : Type} (d : PrimaryODE.FrameData (P × ℝ)) (j : ℤ) (f : P × Plane → Space) : CommonCoverSolve.TangentData P Space

Frame tangent data, bundling normal, normalDot, action, damping and the required compatibility proofs.

Equations

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

structure NavierStokes.PrimaryCopyBridge.FrameMatchesAt {P : Type} (d : PrimaryODE.FrameData (P × ℝ)) (t : CommonCoverSolve.TangentData P Space) (j : ℤ) (q : P × ℝ) (I : Set ℝ) : Prop

Only primitive input fields are compared. The structure contains no equation, estimate, or identity concerning either output solution.

• normal (v : ℝ) : v ∈ I → t.normal (q.1, q.2, v) = d.normal (q, v)
• normalMotion (v : ℝ) : v ∈ I → t.normalDot (q.1, q.2, v) = d.normalMotion (q, v)
• action (v : ℝ) : v ∈ I → ∀ (x : Space), (t.action (q.1, q.2, v)) x = MovingFrameODE.baseAction (d.F (q, v)) (d.shear (q, v)) x
• damping (v : ℝ) : v ∈ I → t.damping (q.1, q.2, v) = d.damping j (q, v)

theorem NavierStokes.PrimaryCopyBridge.frameTangentData_matches {P : Type} (d : PrimaryODE.FrameData (P × ℝ)) (j : ℤ) (f : P × Plane → Space) (q : P × ℝ) (I : Set ℝ) : FrameMatchesAt d (frameTangentData d j f) j q I

Uniqueness with continuity only along the actual finite copy paths

theorem NavierStokes.PrimaryCopyBridge.anchoredSolve_hasDerivAt_along {P V H : Type} [NormedAddCommGroup P] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup H] [NormedSpace ℝ H] [CompleteSpace H] {a b : ℝ} (d : CommonCoverSolve.LinearData P V H) (g : CommonCoverSolve.Geometry) (hab : a ≤ b) (k : Frequency) {Ω : Set (P × Plane)} (hA : ContinuousOn (d.coefficientAlong g k) (Ω ×ˢ Set.Icc a b)) (hf : ContinuousOn (d.forcingAlong g k) (Ω ×ˢ Set.Icc a b)) {q : P × Plane} (hq : q ∈ Ω) {v : ℝ} (hv : v ∈ Set.Icc a b) : HasDerivAt (d.anchoredSolve g hab k q) ((d.coefficientAlong g k (q, v)) (d.anchoredSolve g hab k q v) + d.forcingAlong g k (q, v)) v

theorem NavierStokes.PrimaryCopyBridge.anchoredSolve_unique_along {P V H : Type} [NormedAddCommGroup P] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup H] [NormedSpace ℝ H] [CompleteSpace H] {a b : ℝ} (d : CommonCoverSolve.LinearData P V H) (g : CommonCoverSolve.Geometry) (hab : a ≤ b) (k : Frequency) {Ω : Set (P × Plane)} (hA : ContinuousOn (d.coefficientAlong g k) (Ω ×ˢ Set.Icc a b)) (hf : ContinuousOn (d.forcingAlong g k) (Ω ×ˢ Set.Icc a b)) {q : P × Plane} (hq : q ∈ Ω) {u : ℝ → H} (hu0 : u a = 0) (hu : ∀ v ∈ Set.Icc a b, HasDerivAt u ((d.coefficientAlong g k (q, v)) (u v) + d.forcingAlong g k (q, v)) v) : Set.EqOn u (d.anchoredSolve g hab k q) (Set.Icc a b)

structure NavierStokes.PrimaryCopyBridge.Inputs {P : Type} [NormedAddCommGroup P] (d : PrimaryODE.FrameData (P × ℝ)) (t : CommonCoverSolve.TangentData P Space) (j : ℤ) (g : CommonCoverSolve.Geometry) (k : Frequency) (Ω : Set (P × Plane)) (a b : ℝ) : Prop

All analytic assumptions are on actual input fields on the finite paths. There is deliberately no ambient reference-energy or output-bound hypothesis.

• modal_coefficient : ContinuousOn ((copyFrame d g k).coefficient j) (Ω ×ˢ Set.Icc a b)
• modal_forcing : ContinuousOn ((copyFrame d g k).forcing (copySource t.source g k)) (Ω ×ˢ Set.Icc a b)
• ambient_coefficient : ContinuousOn (t.linearData.coefficientAlong g k) (Ω ×ˢ Set.Icc a b)
• ambient_forcing : ContinuousOn (t.linearData.forcingAlong g k) (Ω ×ˢ Set.Icc a b)
• kinematics (q : P × Plane) : q ∈ Ω → d.Kinematics (copyParameter g k q) (Set.Icc a b)
• compatibility (q : P × Plane) : q ∈ Ω → FrameMatchesAt d t j (copyParameter g k q) (Set.Icc a b)

noncomputable def NavierStokes.PrimaryCopyBridge.reconstructedPath {P : Type} (d : PrimaryODE.FrameData (P × ℝ)) (t : CommonCoverSolve.TangentData P Space) (j : ℤ) (g : CommonCoverSolve.Geometry) (k : Frequency) {a b : ℝ} (hab : a ≤ b) (q : P × Plane) : ℝ → Space

Reconstructed path, given by PrimaryODE.ambientSolution hab (copyFrame d g k) j (fun _ => 0) (copySource t.source g k) q.

Equations

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

noncomputable def NavierStokes.PrimaryCopyBridge.reconstructedCopy {P : Type} (d : PrimaryODE.FrameData (P × ℝ)) (t : CommonCoverSolve.TangentData P Space) (j : ℤ) (g : CommonCoverSolve.Geometry) (k : Frequency) {a b : ℝ} (hab : a ≤ b) (q : P × Plane) : Space

Reconstructed copy, given by reconstructedPath d t j g k hab q (g.coordinates k q.2).2.

Equations

• NavierStokes.PrimaryCopyBridge.reconstructedCopy d t j g k hab q = NavierStokes.PrimaryCopyBridge.reconstructedPath d t j g k hab q (g.coordinates k q.2).2

theorem NavierStokes.PrimaryCopyBridge.reconstructedPath_initial {P : Type} (d : PrimaryODE.FrameData (P × ℝ)) (t : CommonCoverSolve.TangentData P Space) (j : ℤ) (g : CommonCoverSolve.Geometry) (k : Frequency) {a b : ℝ} (hab : a ≤ b) (q : P × Plane) : reconstructedPath d t j g k hab q a = 0

theorem NavierStokes.PrimaryCopyBridge.linear_rhs_eq_projected {P : Type} (d : PrimaryODE.FrameData (P × ℝ)) (t : CommonCoverSolve.TangentData P Space) (j : ℤ) (g : CommonCoverSolve.Geometry) (k : Frequency) {q : P × Plane} {v : ℝ} {I : Set ℝ} (hm : FrameMatchesAt d t j (copyParameter g k q) I) (hv : v ∈ I) (x : Space) : (t.linearData.coefficientAlong g k (q, v)) x + t.linearData.forcingAlong g k (q, v) = TangentProjection.projectedRhs ((copyFrame d g k).normal (q, v)) ((copyFrame d g k).normalMotion (q, v)) x (MovingFrameODE.baseAction ((copyFrame d g k).F (q, v)) ((copyFrame d g k).shear (q, v)) x) (copySource t.source g k (q, v)) ((copyFrame d g k).damping j (q, v))

theorem NavierStokes.PrimaryCopyBridge.reconstructedPath_hasDerivAt {P : Type} [NormedAddCommGroup P] (d : PrimaryODE.FrameData (P × ℝ)) (t : CommonCoverSolve.TangentData P Space) (j : ℤ) (g : CommonCoverSolve.Geometry) (k : Frequency) {a b : ℝ} (hab : a ≤ b) {Ω : Set (P × Plane)} (h : Inputs d t j g k Ω a b) {q : P × Plane} (hq : q ∈ Ω) {v : ℝ} (hv : v ∈ Set.Icc a b) : HasDerivAt (reconstructedPath d t j g k hab q) ((t.linearData.coefficientAlong g k (q, v)) (reconstructedPath d t j g k hab q v) + t.linearData.forcingAlong g k (q, v)) v

theorem NavierStokes.PrimaryCopyBridge.reconstructedPath_eq_anchoredSolve {P : Type} [NormedAddCommGroup P] (d : PrimaryODE.FrameData (P × ℝ)) (t : CommonCoverSolve.TangentData P Space) (j : ℤ) (g : CommonCoverSolve.Geometry) (k : Frequency) {a b : ℝ} (hab : a ≤ b) {Ω : Set (P × Plane)} (h : Inputs d t j g k Ω a b) {q : P × Plane} (hq : q ∈ Ω) : Set.EqOn (reconstructedPath d t j g k hab q) (t.linearData.anchoredSolve g hab k q) (Set.Icc a b)

Equality on the closed interval follows from the actual forced equation and the common zero initial value, with no ambient energy estimate.

theorem NavierStokes.PrimaryCopyBridge.reconstructedPath_tangent {P : Type} [NormedAddCommGroup P] (d : PrimaryODE.FrameData (P × ℝ)) (t : CommonCoverSolve.TangentData P Space) (j : ℤ) (g : CommonCoverSolve.Geometry) (k : Frequency) {a b : ℝ} (hab : a ≤ b) {Ω : Set (P × Plane)} (h : Inputs d t j g k Ω a b) {q : P × Plane} (hq : q ∈ Ω) {v : ℝ} (hv : v ∈ Set.Icc a b) : inner ℝ (t.normal (q.1, (g.coordinates k q.2).1, v)) (reconstructedPath d t j g k hab q v) = 0

theorem NavierStokes.PrimaryCopyBridge.reconstructedCopy_eq_copySolve {P : Type} [NormedAddCommGroup P] (d : PrimaryODE.FrameData (P × ℝ)) (t : CommonCoverSolve.TangentData P Space) (j : ℤ) (g : CommonCoverSolve.Geometry) (k : Frequency) {a b : ℝ} (hab : a ≤ b) {Ω : Set (P × Plane)} (h : Inputs d t j g k Ω a b) {q : P × Plane} (hq : q ∈ Ω) (hv : (g.coordinates k q.2).2 ∈ Set.Icc a b) : reconstructedCopy d t j g k hab q = t.linearData.copySolve g hab k q

The smooth endpoint-rescaled modal representative used by the jet estimates identifies with the very same copy solve.

noncomputable def NavierStokes.PrimaryCopyBridge.reparamPath {P : Type} (d : PrimaryODE.FrameData (P × ℝ)) (t : CommonCoverSolve.TangentData P Space) (j : ℤ) (g : CommonCoverSolve.Geometry) (k : Frequency) (a : ℝ) (z : (P × Plane) × ℝ) : Space

Reparam path as an element of Space.

Equations

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

noncomputable def NavierStokes.PrimaryCopyBridge.reparamCopy {P : Type} (d : PrimaryODE.FrameData (P × ℝ)) (t : CommonCoverSolve.TangentData P Space) (j : ℤ) (g : CommonCoverSolve.Geometry) (k : Frequency) (a : ℝ) (q : P × Plane) : Space

Reparam copy, given by reparamPath d t j g k a (q, (g.coordinates k q.2).2).

Equations

• NavierStokes.PrimaryCopyBridge.reparamCopy d t j g k a q = NavierStokes.PrimaryCopyBridge.reparamPath d t j g k a (q, (g.coordinates k q.2).2)

theorem NavierStokes.PrimaryCopyBridge.reparamPath_eq_reconstructedPath {P : Type} [NormedAddCommGroup P] (d : PrimaryODE.FrameData (P × ℝ)) (t : CommonCoverSolve.TangentData P Space) (j : ℤ) (g : CommonCoverSolve.Geometry) (k : Frequency) {a b : ℝ} (hab : a ≤ b) {Ω : Set (P × Plane)} (h : Inputs d t j g k Ω a b) {z : (P × Plane) × ℝ} (hz : z ∈ Ω ×ˢ Set.Icc a b) : reparamPath d t j g k a z = reconstructedPath d t j g k hab z.1 z.2

theorem NavierStokes.PrimaryCopyBridge.reparamPath_eq_anchoredSolve {P : Type} [NormedAddCommGroup P] (d : PrimaryODE.FrameData (P × ℝ)) (t : CommonCoverSolve.TangentData P Space) (j : ℤ) (g : CommonCoverSolve.Geometry) (k : Frequency) {a b : ℝ} (hab : a ≤ b) {Ω : Set (P × Plane)} (h : Inputs d t j g k Ω a b) {z : (P × Plane) × ℝ} (hz : z ∈ Ω ×ˢ Set.Icc a b) : reparamPath d t j g k a z = t.linearData.anchoredSolve g hab k z.1 z.2

theorem NavierStokes.PrimaryCopyBridge.reparamCopy_eq_copySolve {P : Type} [NormedAddCommGroup P] (d : PrimaryODE.FrameData (P × ℝ)) (t : CommonCoverSolve.TangentData P Space) (j : ℤ) (g : CommonCoverSolve.Geometry) (k : Frequency) {a b : ℝ} (hab : a ≤ b) {Ω : Set (P × Plane)} (h : Inputs d t j g k Ω a b) {q : P × Plane} (hq : q ∈ Ω) (hv : (g.coordinates k q.2).2 ∈ Set.Icc a b) : reparamCopy d t j g k a q = t.linearData.copySolve g hab k q

Local identity of all actual joint derivatives

noncomputable def NavierStokes.PrimaryCopyBridge.currentTime {P : Type} (g : CommonCoverSolve.Geometry) (k : Frequency) (q : P × Plane) : ℝ

Current time, given by (g.coordinates k q.2).2.

Equations

• NavierStokes.PrimaryCopyBridge.currentTime g k q = (g.coordinates k q.2).2

theorem NavierStokes.PrimaryCopyBridge.currentTime_contDiff {P : Type} [NormedAddCommGroup P] (g : CommonCoverSolve.Geometry) (k : Frequency) [NormedSpace ℝ P] : ContDiff ℝ (↑⊤) (currentTime g k)

noncomputable def NavierStokes.PrimaryCopyBridge.copyInterior {P : Type} (g : CommonCoverSolve.Geometry) (k : Frequency) (Ω : Set (P × Plane)) (a b : ℝ) : Set (P × Plane)

Copy interior, given by Ω ∩ (currentTime (P := P) g k) ⁻¹' Ioo a b.

Equations

• NavierStokes.PrimaryCopyBridge.copyInterior g k Ω a b = Ω ∩ NavierStokes.PrimaryCopyBridge.currentTime g k ⁻¹' Set.Ioo a b

theorem NavierStokes.PrimaryCopyBridge.copyInterior_isOpen {P : Type} [NormedAddCommGroup P] (g : CommonCoverSolve.Geometry) (k : Frequency) [NormedSpace ℝ P] {Ω : Set (P × Plane)} (hΩ : IsOpen Ω) (a b : ℝ) : IsOpen (copyInterior g k Ω a b)

theorem NavierStokes.PrimaryCopyBridge.reparamCopy_eqOn {P : Type} [NormedAddCommGroup P] (d : PrimaryODE.FrameData (P × ℝ)) (t : CommonCoverSolve.TangentData P Space) (j : ℤ) (g : CommonCoverSolve.Geometry) (k : Frequency) {a b : ℝ} (hab : a ≤ b) {Ω : Set (P × Plane)} (h : Inputs d t j g k Ω a b) : Set.EqOn (reparamCopy d t j g k a) (t.linearData.copySolve g hab k) (copyInterior g k Ω a b)

theorem NavierStokes.PrimaryCopyBridge.reparamCopy_iteratedFDeriv_eq {P : Type} [NormedAddCommGroup P] (d : PrimaryODE.FrameData (P × ℝ)) (t : CommonCoverSolve.TangentData P Space) (j : ℤ) (g : CommonCoverSolve.Geometry) (k : Frequency) {a b : ℝ} [NormedSpace ℝ P] (hab : a ≤ b) {Ω : Set (P × Plane)} (hΩ : IsOpen Ω) (h : Inputs d t j g k Ω a b) {q : P × Plane} (hq : q ∈ copyInterior g k Ω a b) (n : ℕ) : iteratedFDeriv ℝ n (reparamCopy d t j g k a) q = iteratedFDeriv ℝ n (t.linearData.copySolve g hab k) q

This equality transfers bounds for modal reconstruction to actual full jets of the common-cover output; it introduces no energy estimate.

theorem NavierStokes.PrimaryCopyBridge.reparamPath_iteratedFDeriv_eq {P : Type} [NormedAddCommGroup P] (d : PrimaryODE.FrameData (P × ℝ)) (t : CommonCoverSolve.TangentData P Space) (j : ℤ) (g : CommonCoverSolve.Geometry) (k : Frequency) {a b : ℝ} [NormedSpace ℝ P] (hab : a ≤ b) {Ω : Set (P × Plane)} (hΩ : IsOpen Ω) (h : Inputs d t j g k Ω a b) {z : (P × Plane) × ℝ} (hz : z ∈ Ω ×ˢ Set.Ioo a b) (n : ℕ) : iteratedFDeriv ℝ n (reparamPath d t j g k a) z = iteratedFDeriv ℝ n (fun (w : (P × Plane) × ℝ) => t.linearData.anchoredSolve g hab k w.1 w.2) z

Smooth primitive data discharge the continuity requirements

noncomputable def NavierStokes.PrimaryCopyBridge.baseOperatorFamily : ℝ × State →L[ℝ] Space →L[ℝ] Space

Base operator family, constructed using LinearMap.toContinuousLinearMap.

Equations

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

@[simp]

theorem NavierStokes.PrimaryCopyBridge.baseOperatorFamily_apply (z : ℝ × State) : baseOperatorFamily z = baseOperator z.1 z.2

theorem NavierStokes.PrimaryCopyBridge.projectedOperator_continuousOn {X : Type u_1} {H : Type u_2} [TopologicalSpace X] [NormedAddCommGroup H] [InnerProductSpace ℝ H] {S : Set X} {n nd : X → H} {A : X → H →L[ℝ] H} {δ : X → ℝ} (hn : ContinuousOn n S) (hnd : ContinuousOn nd S) (hA : ContinuousOn A S) (hδ : ContinuousOn δ S) (hne : ∀ z ∈ S, n z ≠ 0) : ContinuousOn (fun (z : X) => TangentODE.projectedOperator (n z) (nd z) (A z) (δ z)) S

theorem NavierStokes.PrimaryCopyBridge.projectedForcing_continuousOn {X : Type u_1} [TopologicalSpace X] {S : Set X} {n f : X → Space} (hn : ContinuousOn n S) (hf : ContinuousOn f S) (hne : ∀ z ∈ S, n z ≠ 0) : ContinuousOn (fun (z : X) => -TangentProjection.tangentProj (n z) (f z)) S

theorem NavierStokes.PrimaryCopyBridge.frame_normal_continuousOn {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {d : PrimaryODE.FrameData Q} {S : Set (Q × ℝ)} (h : d.SmoothOn S) : ContinuousOn d.normal S

theorem NavierStokes.PrimaryCopyBridge.frame_normalMotion_continuousOn {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {d : PrimaryODE.FrameData Q} {S : Set (Q × ℝ)} (h : d.SmoothOn S) : ContinuousOn d.normalMotion S

theorem NavierStokes.PrimaryCopyBridge.frame_baseOperator_continuousOn {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {d : PrimaryODE.FrameData Q} {S : Set (Q × ℝ)} (h : d.SmoothOn S) : ContinuousOn (fun (z : Q × ℝ) => baseOperator (d.F z) (d.shear z)) S

theorem NavierStokes.PrimaryCopyBridge.reindex_smoothOn {P Q : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup Q] [NormedSpace ℝ Q] (d : PrimaryODE.FrameData P) (φ : Q → P) {S : Set (P × ℝ)} {Ω : Set (Q × ℝ)} (hd : d.SmoothOn S) (hφ : ContDiffOn ℝ (↑⊤) (fun (z : Q × ℝ) => (φ z.1, z.2)) Ω) (hmap : Set.MapsTo (fun (z : Q × ℝ) => (φ z.1, z.2)) Ω S) : (reindex d φ).SmoothOn Ω

theorem NavierStokes.PrimaryCopyBridge.copyParameter_contDiff {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (g : CommonCoverSolve.Geometry) (k : Frequency) : ContDiff ℝ (↑⊤) (copyParameter g k)

theorem NavierStokes.PrimaryCopyBridge.copyArgument_contDiff {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (g : CommonCoverSolve.Geometry) (k : Frequency) : ContDiff ℝ ↑⊤ fun (z : (P × Plane) × ℝ) => (copyParameter g k z.1, z.2)

theorem NavierStokes.PrimaryCopyBridge.copyFrame_smoothOn {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (d : PrimaryODE.FrameData (P × ℝ)) (g : CommonCoverSolve.Geometry) (k : Frequency) {S : Set ((P × ℝ) × ℝ)} {Ω : Set ((P × Plane) × ℝ)} (hd : d.SmoothOn S) (hmap : Set.MapsTo (fun (z : (P × Plane) × ℝ) => (copyParameter g k z.1, z.2)) Ω S) : (copyFrame d g k).SmoothOn Ω

theorem NavierStokes.PrimaryCopyBridge.copySource_contDiffOn {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (g : CommonCoverSolve.Geometry) (k : Frequency) {f : P × Plane → Space} {S : Set (P × Plane)} {Ω : Set ((P × Plane) × ℝ)} (hf : ContDiffOn ℝ (↑⊤) f S) (hmap : Set.MapsTo (fun (z : (P × Plane) × ℝ) => (z.1.1, g.path k z.1.2 z.2)) Ω S) : ContDiffOn ℝ (↑⊤) (copySource f g k) Ω

theorem NavierStokes.PrimaryCopyBridge.inputs_of_smooth_frame {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (d : PrimaryODE.FrameData (P × ℝ)) (g : CommonCoverSolve.Geometry) (k : Frequency) (j : ℤ) (f : P × Plane → Space) {Ω : Set (P × Plane)} {a b : ℝ} (hd : (copyFrame d g k).SmoothOn (Ω ×ˢ Set.Icc a b)) (hf : ContDiffOn ℝ (↑⊤) (copySource f g k) (Ω ×ˢ Set.Icc a b)) (hk : ∀ q ∈ Ω, d.Kinematics (copyParameter g k q) (Set.Icc a b)) : Inputs d (frameTangentData d j f) j g k Ω a b

For the concrete tangent datum built from the moving frame, no matching or ambient continuity obligation is left over: smooth inputs and the actual frame kinematics imply every bridge hypothesis.

theorem NavierStokes.PrimaryCopyBridge.frame_reconstructedCopy_eq_copySolve {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (d : PrimaryODE.FrameData (P × ℝ)) (g : CommonCoverSolve.Geometry) (k : Frequency) (j : ℤ) (f : P × Plane → Space) {Ω : Set (P × Plane)} {a b : ℝ} (hab : a ≤ b) (hd : (copyFrame d g k).SmoothOn (Ω ×ˢ Set.Icc a b)) (hf : ContDiffOn ℝ (↑⊤) (copySource f g k) (Ω ×ˢ Set.Icc a b)) (hk : ∀ q ∈ Ω, d.Kinematics (copyParameter g k q) (Set.Icc a b)) {q : P × Plane} (hq : q ∈ Ω) (hv : (g.coordinates k q.2).2 ∈ Set.Icc a b) : reconstructedCopy d (frameTangentData d j f) j g k hab q = (frameTangentData d j f).linearData.copySolve g hab k q

Direct canonical bridge, with assumptions only on smooth primitive frame and source data and their actual slot derivatives.

theorem NavierStokes.PrimaryCopyBridge.frame_reparamCopy_iteratedFDeriv_eq {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (d : PrimaryODE.FrameData (P × ℝ)) (g : CommonCoverSolve.Geometry) (k : Frequency) (j : ℤ) (f : P × Plane → Space) {Ω : Set (P × Plane)} {a b : ℝ} (hab : a ≤ b) (hΩ : IsOpen Ω) (hd : (copyFrame d g k).SmoothOn (Ω ×ˢ Set.Icc a b)) (hf : ContDiffOn ℝ (↑⊤) (copySource f g k) (Ω ×ˢ Set.Icc a b)) (hk : ∀ q ∈ Ω, d.Kinematics (copyParameter g k q) (Set.Icc a b)) {q : P × Plane} (hq : q ∈ copyInterior g k Ω a b) (n : ℕ) : iteratedFDeriv ℝ n (reparamCopy d (frameTangentData d j f) j g k a) q = iteratedFDeriv ℝ n ((frameTangentData d j f).linearData.copySolve g hab k) q

Exact transfer of all ordinary full tensors to the canonical copy solve. The interval endpoints retain the pointwise equality proved above.

Seeded primary paths: the same equation, with their own initial data

noncomputable def NavierStokes.PrimaryCopyBridge.seededReconstructedPath {P : Type} (d : PrimaryODE.FrameData (P × ℝ)) (t : CommonCoverSolve.TangentData P Space) (j : ℤ) (g : CommonCoverSolve.Geometry) (k : Frequency) {a b : ℝ} (hab : a ≤ b) (x₀ : P × Plane → State) (q : P × Plane) : ℝ → Space

Seeded reconstructed path, given by PrimaryODE.ambientSolution hab (copyFrame d g k) j x₀ (copySource t.source g k) q.

Equations

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

theorem NavierStokes.PrimaryCopyBridge.seededReconstructedPath_initial {P : Type} (d : PrimaryODE.FrameData (P × ℝ)) (t : CommonCoverSolve.TangentData P Space) (j : ℤ) (g : CommonCoverSolve.Geometry) (k : Frequency) {a b : ℝ} (hab : a ≤ b) (x₀ : P × Plane → State) (q : P × Plane) : seededReconstructedPath d t j g k hab x₀ q a = d.ambient (copyParameter g k q, a) (x₀ q)

theorem NavierStokes.PrimaryCopyBridge.seededReconstructedPath_hasDerivAt {P : Type} [NormedAddCommGroup P] (d : PrimaryODE.FrameData (P × ℝ)) (t : CommonCoverSolve.TangentData P Space) (j : ℤ) (g : CommonCoverSolve.Geometry) (k : Frequency) {a b : ℝ} (hab : a ≤ b) (x₀ : P × Plane → State) {Ω : Set (P × Plane)} (h : Inputs d t j g k Ω a b) {q : P × Plane} (hq : q ∈ Ω) {v : ℝ} (hv : v ∈ Set.Icc a b) : have z := (q.1, (g.coordinates k q.2).1, v); HasDerivAt (seededReconstructedPath d t j g k hab x₀ q) (TangentProjection.projectedRhs (t.normal z) (t.normalDot z) (seededReconstructedPath d t j g k hab x₀ q v) ((t.action z) (seededReconstructedPath d t j g k hab x₀ q v)) (t.source (q.1, g.path k q.2 v)) (t.damping z)) v

The reconstructed seeded path satisfies the actual tangent equation. This is not an identification with the zero-entry copy solve.

theorem NavierStokes.PrimaryCopyBridge.seededReconstructedPath_tangent {P : Type} [NormedAddCommGroup P] (d : PrimaryODE.FrameData (P × ℝ)) (t : CommonCoverSolve.TangentData P Space) (j : ℤ) (g : CommonCoverSolve.Geometry) (k : Frequency) {a b : ℝ} (hab : a ≤ b) (x₀ : P × Plane → State) {Ω : Set (P × Plane)} (h : Inputs d t j g k Ω a b) {q : P × Plane} (hq : q ∈ Ω) {v : ℝ} (hv : v ∈ Set.Icc a b) : inner ℝ (t.normal (q.1, (g.coordinates k q.2).1, v)) (seededReconstructedPath d t j g k hab x₀ q v) = 0

theorem NavierStokes.ParticularWaveBounds.forced_joint_jet_bound {Q H : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {L S K μ w : ℝ} (_hL : 0 < L) (hS : 1 ≤ S) (hK : 1 ≤ K) (hμ : 0 ≤ μ) (hw : 0 ≤ w) (hslot : L ≤ K * S) (hExp : Real.exp (μ * L) ≤ K) (U : Set Q) (V : Set ℝ) (hU : IsOpen U) (hV : IsOpen V) (hI : Set.Icc 0 L ⊆ V) (A : Q × ℝ → H →L[ℝ] H) (hA : ContDiffOn ℝ (↑⊤) A (U ×ˢ V)) (P rate : ℝ → ℝ) (hP : ∀ (t : ℝ), 0 < P t) (hdP : ∀ (t : ℝ), HasDerivAt P (rate t * P t) t) (f : Q × ℝ → H) (hf : ContDiffOn ℝ (↑⊤) f (U ×ˢ V)) {p : Q} (hp : p ∈ U) {t : ℝ} (ht : t ∈ Set.Icc 0 L) (henergy : ∀ v ∈ Set.Icc 0 L, ∀ (x : H), inner ℝ x ((A (p, v)) x) ≤ (rate v + μ) * ‖x‖ ^ 2) (m N : ℕ) (hjets : ∀ j ≤ N, ∀ v ∈ Set.Icc 0 L, ‖iteratedFDeriv ℝ j A (p, v)‖ ≤ K * S ^ m) (hfjets : ∀ j ≤ N, ∀ v ∈ Set.Icc 0 L, ‖iteratedFDeriv ℝ j f (p, v)‖ ≤ w * K * S ^ m * P v) (j : ℕ) (hj : j ≤ N) : ‖iteratedFDeriv ℝ j (JointODE.reparamSolution 0 A (fun (x : Q) => 0) f) (p, t)‖ ≤ w * (2 ^ (N + 1) * PrimaryPulseBounds.rescaleConstant N K ^ 3) ^ (j + 1) * S ^ ((m + 2) * (j + 1)) * P t

Full joint parameter and endpoint jets of the actual zero-entry forced solution. The factor w is frozen at the parameter being estimated; no regularity or derivative bound on this majorant is required.

theorem NavierStokes.ParticularWaveBounds.forced_family_envelope_jets {ι : Type u_1} {Q H : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (D : PhaseJetBounds.Domain ι Q) (V : ι → Set ℝ) (hV : ∀ (i : ι), IsOpen (V i)) (L μ : ι → ℝ) (hL : ∀ (i : ι), 0 < L i) (hI : ∀ (i : ι), Set.Icc 0 (L i) ⊆ V i) (A : ι → Q × ℝ → H →L[ℝ] H) (hA : PhaseJetBounds.PolynomialJets (PrimaryPulseBounds.productDomain D V hV) A) (P rate : ι → ℝ → ℝ) (hP : ∀ (i : ι) (t : ℝ), 0 < P i t) (hdP : ∀ (i : ι) (t : ℝ), HasDerivAt (P i) (rate i t * P i t) t) (w : ι → Q → ℝ) (hw : ∀ (i : ι), ∀ p ∈ D.carrier i, 0 ≤ w i p) (f : ι → Q × ℝ → H) (hf : PrimaryPulseBounds.EnvelopeJets (PrimaryPulseBounds.productDomain D V hV) (fun (i : ι) (z : Q × ℝ) => w i z.1 * P i z.2) f) {K₀ : ℝ} (hK₀ : 1 ≤ K₀) (hμ : ∀ (i : ι), 0 ≤ μ i) (hslot : ∀ (i : ι), L i ≤ K₀ * D.scale i) (hExp : ∀ (i : ι), Real.exp (μ i * L i) ≤ K₀) (henergy : ∀ (i : ι), ∀ p ∈ D.carrier i, ∀ v ∈ Set.Icc 0 (L i), ∀ (x : H), inner ℝ x ((A i (p, v)) x) ≤ (rate i v + μ i) * ‖x‖ ^ 2) : PrimaryPulseBounds.EnvelopeJets (PrimaryPulseBounds.productDomain D (fun (i : ι) => Set.Ioo 0 (L i)) ⋯) (fun (i : ι) (z : Q × ℝ) => w i z.1 * P i z.2) fun (i : ι) => JointODE.reparamSolution 0 (A i) (fun (x : Q) => 0) (f i)

A band-uniform family version of the joint forced estimate. Both input predicates refer to actual full derivatives of the coefficient and source.

theorem NavierStokes.ParticularWaveBounds.envelopeJets_congr {ι : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {D : PhaseJetBounds.Domain ι E} {w : ι → E → ℝ} {f g : ι → E → F} (hf : PrimaryPulseBounds.EnvelopeJets D w f) (he : ∀ (i : ι), Set.EqOn (f i) (g i) (D.carrier i)) : PrimaryPulseBounds.EnvelopeJets D w g

Local equality transfers the actual derivative estimates; no derivatives of an extension outside the open carrier are used.

theorem NavierStokes.ParticularWaveBounds.norm_jet_comp_affine {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {U : Set F} (hU : IsOpen U) {f : F → G} (hf : ContDiffOn ℝ (↑⊤) f U) (L : E →L[ℝ] F) (c : F) {x : E} (hx : c + L x ∈ U) (j : ℕ) : ‖iteratedFDeriv ℝ j (fun (y : E) => f (c + L y)) x‖ ≤ ‖iteratedFDeriv ℝ j f (c + L x)‖ * ‖L‖ ^ j

Relative version of the affine higher chain rule. The affine map need not be bounded at order zero, and f need only be smooth on its open domain.

theorem NavierStokes.ParticularWaveBounds.envelopeJets_precomp_affine {ι : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {D : PhaseJetBounds.Domain ι E} {D' : PhaseJetBounds.Domain ι F} {w : ι → F → ℝ} {f : ι → F → G} (hf : PrimaryPulseBounds.EnvelopeJets D' w f) (L : ι → E →L[ℝ] F) (c : ι → F) (hscale : ∀ (i : ι), D'.scale i = D.scale i) (hmap : ∀ (i : ι), Set.MapsTo (fun (x : E) => c i + (L i) x) (D.carrier i) (D'.carrier i)) {C : ℝ} {k : ℕ} (hC : 1 ≤ C) (hL : ∀ (i : ι), ‖L i‖ ≤ C * D.scale i ^ k) : PrimaryPulseBounds.EnvelopeJets D (fun (i : ι) (x : E) => w i (c i + (L i) x)) fun (i : ι) (x : E) => f i (c i + (L i) x)

theorem NavierStokes.ParticularWaveBounds.anchoredSolve_family_envelope_jets {ι P V H : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (D : PhaseJetBounds.Domain ι (P × TorusInverse.Plane)) (I : ι → Set ℝ) (hI : ∀ (i : ι), IsOpen (I i)) (L μ : ι → ℝ) (hL : ∀ (i : ι), 0 < L i) (hslotI : ∀ (i : ι), Set.Icc 0 (L i) ⊆ I i) (d : ι → CommonCoverSolve.LinearData P V H) (g : ι → CommonCoverSolve.Geometry) (copy : ι → TorusInverse.Frequency) (hA : PhaseJetBounds.PolynomialJets (PrimaryPulseBounds.productDomain D I hI) fun (i : ι) => (d i).coefficientAlong (g i) (copy i)) (W rate : ι → ℝ → ℝ) (hW : ∀ (i : ι) (t : ℝ), 0 < W i t) (hdW : ∀ (i : ι) (t : ℝ), HasDerivAt (W i) (rate i t * W i t) t) (w : ι → P × TorusInverse.Plane → ℝ) (hw : ∀ (i : ι), ∀ p ∈ D.carrier i, 0 ≤ w i p) (hf : PrimaryPulseBounds.EnvelopeJets (PrimaryPulseBounds.productDomain D I hI) (fun (i : ι) (z : (P × TorusInverse.Plane) × ℝ) => w i z.1 * W i z.2) fun (i : ι) => (d i).forcingAlong (g i) (copy i)) {K : ℝ} (hK : 1 ≤ K) (hμ : ∀ (i : ι), 0 ≤ μ i) (hslot : ∀ (i : ι), L i ≤ K * D.scale i) (hExp : ∀ (i : ι), Real.exp (μ i * L i) ≤ K) (henergy : ∀ (i : ι), ∀ p ∈ D.carrier i, ∀ v ∈ Set.Icc 0 (L i), ∀ (x : H), inner ℝ x (((d i).coefficientAlong (g i) (copy i) (p, v)) x) ≤ (rate i v + μ i) * ‖x‖ ^ 2) : PrimaryPulseBounds.EnvelopeJets (PrimaryPulseBounds.productDomain D (fun (i : ι) => Set.Ioo 0 (L i)) ⋯) (fun (i : ι) (z : (P × TorusInverse.Plane) × ℝ) => w i z.1 * W i z.2) fun (i : ι) (z : (P × TorusInverse.Plane) × ℝ) => (d i).anchoredSolve (g i) ⋯ (copy i) z.1 z.2

The same bound for the actual copy-path Volterra extension. Uniqueness identifies it with the endpoint-rescaled solve on an open slot.

theorem NavierStokes.ParticularWaveBounds.copySolve_envelope_of_anchored {ι P V H : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (D D' : PhaseJetBounds.Domain ι (P × TorusInverse.Plane)) (L : ι → ℝ) (hL : ∀ (i : ι), 0 < L i) (d : ι → CommonCoverSolve.LinearData P V H) (g : ι → CommonCoverSolve.Geometry) (copy : ι → TorusInverse.Frequency) (w : ι → P × TorusInverse.Plane → ℝ) (W : ι → ℝ → ℝ) (hs : PrimaryPulseBounds.EnvelopeJets (PrimaryPulseBounds.productDomain D (fun (i : ι) => Set.Ioo 0 (L i)) ⋯) (fun (i : ι) (z : (P × TorusInverse.Plane) × ℝ) => w i z.1 * W i z.2) fun (i : ι) (z : (P × TorusInverse.Plane) × ℝ) => (d i).anchoredSolve (g i) ⋯ (copy i) z.1 z.2) (hscale : ∀ (i : ι), D.scale i = D'.scale i) (hdom : ∀ (i : ι), D'.carrier i ⊆ D.carrier i) (hslot : ∀ (i : ι), ∀ p ∈ D'.carrier i, ((g i).coordinates (copy i) p.2).2 ∈ Set.Ioo 0 (L i)) {C : ℝ} {k : ℕ} (hC : 1 ≤ C) (hcost : ∀ (i : ι), CommonCoverClass.argumentCost (g i) ≤ C * D'.scale i ^ k) : PrimaryPulseBounds.EnvelopeJets D' (fun (i : ι) (p : P × TorusInverse.Plane) => w i p * W i ((g i).coordinates (copy i) p.2).2) fun (i : ι) => (d i).copySolve (g i) ⋯ (copy i)

Evaluation at the current native slot costs only the norm of the actual affine coordinate map. This statement is uniform over copy indices.

theorem NavierStokes.ParticularWaveBounds.copySolve_joint_jet_bound {P V H : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (d : CommonCoverSolve.LinearData P V H) (g : CommonCoverSolve.Geometry) (copy : TorusInverse.Frequency) {L S K μ w : ℝ} (hL : 0 < L) (hS : 1 ≤ S) (hK : 1 ≤ K) (hμ : 0 ≤ μ) (hw : 0 ≤ w) (hslot : L ≤ K * S) (hExp : Real.exp (μ * L) ≤ K) {U : Set P} (hU : IsOpen U) (hA : ContDiffOn ℝ (↑⊤) d.coefficient (U ×ˢ Set.univ)) (hB : ContDiffOn ℝ (↑⊤) d.forcingMap (U ×ˢ Set.univ)) (hf : ContDiffOn ℝ (↑⊤) d.source (U ×ˢ Set.univ)) (W rate : ℝ → ℝ) (hW : ∀ (t : ℝ), 0 < W t) (hdW : ∀ (t : ℝ), HasDerivAt W (rate t * W t) t) {p : P × TorusInverse.Plane} (hp : p.1 ∈ U) (heta : (g.coordinates copy p.2).2 ∈ Set.Ioo 0 L) (henergy : ∀ v ∈ Set.Icc 0 L, ∀ (x : H), inner ℝ x ((d.coefficientAlong g copy (p, v)) x) ≤ (rate v + μ) * ‖x‖ ^ 2) (m N : ℕ) (hAj : ∀ j ≤ N, ∀ v ∈ Set.Icc 0 L, ‖iteratedFDeriv ℝ j (d.coefficientAlong g copy) (p, v)‖ ≤ K * S ^ m) (hfj : ∀ j ≤ N, ∀ v ∈ Set.Icc 0 L, ‖iteratedFDeriv ℝ j (d.forcingAlong g copy) (p, v)‖ ≤ w * K * S ^ m * W v) (j : ℕ) (hj : j ≤ N) : ‖iteratedFDeriv ℝ j (d.copySolve g ⋯ copy) p‖ ≤ w * (2 ^ (N + 1) * PrimaryPulseBounds.rescaleConstant N K ^ 3) ^ (j + 1) * S ^ ((m + 2) * (j + 1)) * W (g.coordinates copy p.2).2 * CommonCoverClass.argumentCost g ^ j

Full derivatives of the actual current copy field. In particular the scale S may be the frozen spatial growth/edge factor at p; no uniform distance from a cutoff edge is required.

theorem NavierStokes.ParticularWaveBounds.copySolve_waveClass {P V H : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (s : WeightedClasses.StripData (P × TorusInverse.Plane)) (α : ℝ) (d : ℕ → CommonCoverSolve.LinearData P V H) (g : ℕ → CommonCoverSolve.Geometry) (copy : ℕ → TorusInverse.Frequency) (L μ : ℕ → ℝ) (hL : ∀ (n : ℕ), 0 < L n) (W rate : ℕ → ℝ → ℝ) (hW : ∀ (n : ℕ) (t : ℝ), 0 < W n t) (hdW : ∀ (n : ℕ) (t : ℝ), HasDerivAt (W n) (rate n t * W n t) t) {U : Set P} (hU : IsOpen U) (hdom : ∀ p ∈ s.domain, p.1 ∈ U) (hA : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (d n).coefficient (U ×ˢ Set.univ)) (hB : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (d n).forcingMap (U ×ˢ Set.univ)) (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (d n).source (U ×ˢ Set.univ)) (heta : ∀ (n : ℕ), ∀ p ∈ s.domain, ((g n).coordinates (copy n) p.2).2 ∈ Set.Ioo 0 (L n)) {K₀ : ℝ} {q : ℕ} (hK₀ : 1 ≤ K₀) (hμ : ∀ (n : ℕ), 0 ≤ μ n) (hslot : ∀ (n : ℕ), L n ≤ K₀ * s.slow n) (hExp : ∀ (n : ℕ), Real.exp (μ n * L n) ≤ K₀) (hcost : ∀ (n : ℕ), CommonCoverClass.argumentCost (g n) ≤ K₀ * s.slow n ^ q) (henergy : ∀ (n : ℕ), ∀ p ∈ s.domain, ∀ v ∈ Set.Icc 0 (L n), ∀ (x : H), inner ℝ x (((d n).coefficientAlong (g n) (copy n) (p, v)) x) ≤ (rate n v + μ n) * ‖x‖ ^ 2) (hinput : ∀ (N : ℕ), ∃ (C : ℝ), 0 ≤ C ∧ ∃ (m : ℕ), ∀ (n : ℕ), ∀ p ∈ s.domain, ∀ j ≤ N, ∀ v ∈ Set.Icc 0 (L n), ‖iteratedFDeriv ℝ j ((d n).coefficientAlong (g n) (copy n)) (p, v)‖ ≤ C * s.growth n p ^ m ∧ ‖iteratedFDeriv ℝ j ((d n).forcingAlong (g n) (copy n)) (p, v)‖ ≤ s.epsilon n ^ α * √(s.zeta p) * C * s.growth n p ^ m * W n v) : WeightedClasses.WaveClass s (fun (n : ℕ) (p : P × TorusInverse.Plane) => W n ((g n).coordinates (copy n) p.2).2) α fun (n : ℕ) => (d n).copySolve (g n) ⋯ (copy n)

The actual particular solution belongs to W_α. Input bounds are on the full joint derivatives of the pulled-back coefficient and source; the edge power may depend on the requested derivative order.

structure NavierStokes.ParticularWaveBounds.CopyControl {P V H : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] (s : WeightedClasses.StripData (P × TorusInverse.Plane)) (α : ℝ) (d : ℕ → CommonCoverSolve.LinearData P V H) (g : ℕ → CommonCoverSolve.Geometry) (copy : ℕ → TorusInverse.Frequency) (L : ℕ → ℝ) (W : ℕ → ℝ → ℝ) : Type

Primitive data for the direct weighted Volterra estimate. No field in this structure bounds a solution or assumes its differential equation.

• slowDomain : Set P

  Slow domain of CopyControl, of type Set P.

• open_slow : IsOpen self.slowDomain
• domain (p : P × TorusInverse.Plane) : p ∈ s.domain → p.1 ∈ self.slowDomain
• coefficient_smooth (n : ℕ) : ContDiffOn ℝ (↑⊤) (d n).coefficient (self.slowDomain ×ˢ Set.univ)
• forcingMap_smooth (n : ℕ) : ContDiffOn ℝ (↑⊤) (d n).forcingMap (self.slowDomain ×ˢ Set.univ)
• source_smooth (n : ℕ) : ContDiffOn ℝ (↑⊤) (d n).source (self.slowDomain ×ˢ Set.univ)
• length_pos (n : ℕ) : 0 < L n
• current_slot (n : ℕ) (p : P × TorusInverse.Plane) : p ∈ s.domain → ((g n).coordinates (copy n) p.2).2 ∈ Set.Ioo 0 (L n)
• rate : ℕ → ℝ → ℝ

  Rate of CopyControl, of type ℕ → ℝ → ℝ.

• envelope_pos (n : ℕ) (v : ℝ) : 0 < W n v
• envelope_deriv (n : ℕ) (v : ℝ) : HasDerivAt (W n) (self.rate n v * W n v) v
• errorRate : ℕ → ℝ

  Error rate of CopyControl, of type ℕ → ℝ.

• errorRate_nonneg (n : ℕ) : 0 ≤ self.errorRate n
• boundConstant : ℝ

  Bound constant of CopyControl, of type ℝ.

• constant_ge_one : 1 ≤ self.boundConstant
• coordinatePower : ℕ

  Coordinate power of CopyControl, of type ℕ.

• length_bound (n : ℕ) : L n ≤ self.boundConstant * s.slow n
• exponential_bound (n : ℕ) : Real.exp (self.errorRate n * L n) ≤ self.boundConstant
• coordinate_bound (n : ℕ) : CommonCoverClass.argumentCost (g n) ≤ self.boundConstant * s.slow n ^ self.coordinatePower
• energy (n : ℕ) (p : P × TorusInverse.Plane) : p ∈ s.domain → ∀ v ∈ Set.Icc 0 (L n), ∀ (x : H), inner ℝ x (((d n).coefficientAlong (g n) (copy n) (p, v)) x) ≤ (self.rate n v + self.errorRate n) * ‖x‖ ^ 2
• input_jets (N : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∃ (m : ℕ), ∀ (n : ℕ), ∀ p ∈ s.domain, ∀ j ≤ N, ∀ v ∈ Set.Icc 0 (L n), ‖iteratedFDeriv ℝ j ((d n).coefficientAlong (g n) (copy n)) (p, v)‖ ≤ C * s.growth n p ^ m ∧ ‖iteratedFDeriv ℝ j ((d n).forcingAlong (g n) (copy n)) (p, v)‖ ≤ s.epsilon n ^ α * √(s.zeta p) * C * s.growth n p ^ m * W n v

theorem NavierStokes.ParticularWaveBounds.CopyControl.waveClass {P V H : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {s : WeightedClasses.StripData (P × TorusInverse.Plane)} {α : ℝ} {d : ℕ → CommonCoverSolve.LinearData P V H} {g : ℕ → CommonCoverSolve.Geometry} {copy : ℕ → TorusInverse.Frequency} {L : ℕ → ℝ} {W : ℕ → ℝ → ℝ} (h : CopyControl s α d g copy L W) (hL : ∀ (n : ℕ), 0 < L n) : WeightedClasses.WaveClass s (fun (n : ℕ) (p : P × TorusInverse.Plane) => W n ((g n).coordinates (copy n) p.2).2) α fun (n : ℕ) => (d n).copySolve (g n) ⋯ (copy n)

noncomputable def NavierStokes.ParticularWaveBounds.slotDirection (g : CommonCoverSolve.Geometry) : TorusInverse.Plane

Direction of increasing native slot time in common coordinates.

Equations

• NavierStokes.ParticularWaveBounds.slotDirection g = (NavierStokes.CommonCoverSolve.coverPower g.gap).symm (g.basis (0, 1))

theorem NavierStokes.ParticularWaveBounds.path_hasDerivAt (g : CommonCoverSolve.Geometry) (k : TorusInverse.Frequency) (Y : TorusInverse.Plane) (s : ℝ) : HasDerivAt (g.path k Y) (slotDirection g) s

theorem NavierStokes.ParticularWaveBounds.along_copySolve {P V H : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (d : CommonCoverSolve.LinearData P V H) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) {U : Set P} (hU : IsOpen U) (k : TorusInverse.Frequency) (hA : ContDiffOn ℝ (↑⊤) d.coefficient (U ×ˢ Set.univ)) (hB : ContDiffOn ℝ (↑⊤) d.forcingMap (U ×ˢ Set.univ)) (hf : ContDiffOn ℝ (↑⊤) d.source (U ×ˢ Set.univ)) {p : P} (hp : p ∈ U) (Y : TorusInverse.Plane) (heta : (g.coordinates k Y).2 ∈ Set.Ioo a b) : HarmonicCalculus.along (fun (x : P × TorusInverse.Plane) => (0, slotDirection g)) (d.copySolve g hab k) (p, Y) = (d.coefficient (p, g.coordinates k Y)) (d.copySolve g hab k (p, Y)) + (d.forcingMap (p, g.coordinates k Y)) (d.source (p, Y))

Differentiation of the actual reanchored copy solve is differentiation along the fixed common-coordinate slot vector.

noncomputable def NavierStokes.ParticularWaveBounds.nativePoint {P : Type} (g : CommonCoverSolve.Geometry) (k : TorusInverse.Frequency) (p : P × TorusInverse.Plane) : P × TorusInverse.Plane

Native point, given by (p.1, g.coordinates k p.2).

Equations

• NavierStokes.ParticularWaveBounds.nativePoint g k p = (p.1, g.coordinates k p.2)

noncomputable def NavierStokes.ParticularWaveBounds.copyPressureReal {P H : Type} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (t : CommonCoverSolve.TangentData P H) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (k : TorusInverse.Frequency) (p : P × TorusInverse.Plane) : ℝ

The pressure coefficient is constructed from the solved tangent field, the actual normal motion, and the source at the current common point.

Equations

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

noncomputable def NavierStokes.ParticularWaveBounds.copyPressure {P H : Type} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (t : CommonCoverSolve.TangentData P H) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (k : TorusInverse.Frequency) (frequency : ℝ) (p : P × TorusInverse.Plane) : ℂ

Copy pressure, given by Complex.I * (copyPressureReal t g hab k p : ℂ) / (frequency : ℂ).

Equations

• NavierStokes.ParticularWaveBounds.copyPressure t g hab k frequency p = Complex.I * ↑(NavierStokes.ParticularWaveBounds.copyPressureReal t g hab k p) / ↑frequency

theorem NavierStokes.ParticularWaveBounds.copySolve_pressure_balance {P H : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (t : CommonCoverSolve.TangentData P H) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) {U : Set P} (hU : IsOpen U) (k : TorusInverse.Frequency) (hA : ContDiffOn ℝ (↑⊤) t.linearData.coefficient (U ×ˢ Set.univ)) (hB : ContDiffOn ℝ (↑⊤) t.linearData.forcingMap (U ×ˢ Set.univ)) (hf : ContDiffOn ℝ (↑⊤) t.source (U ×ˢ Set.univ)) {p : P} (hp : p ∈ U) (Y : TorusInverse.Plane) (heta : (g.coordinates k Y).2 ∈ Set.Ioo a b) : HarmonicCalculus.along (fun (x : P × TorusInverse.Plane) => (0, slotDirection g)) (t.linearData.copySolve g hab k) (p, Y) + (t.action (p, g.coordinates k Y)) (t.linearData.copySolve g hab k (p, Y)) + t.damping (p, g.coordinates k Y) • t.linearData.copySolve g hab k (p, Y) - copyPressureReal t g hab k (p, Y) • t.normal (p, g.coordinates k Y) = -t.source (p, Y)

Exact pressure cancellation for the constructed copy solution. This equation is derived from the ODE; it is not an assumption on an output.

theorem NavierStokes.ParticularWaveBounds.envelopeJets_memClass {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData E} {w : ℕ → E → ℝ} {α : ℝ} {f : ℕ → E → ProblemStatement.Space} (hf : PrimaryPulseBounds.EnvelopeJets (PrimaryPulseBounds.phaseDomain s) (fun (n : ℕ) (x : E) => s.epsilon n ^ α * w n x) f) (hw : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ w n x) : WeightedClasses.MemClass s w α f

The epsilon power retained in a constructed envelope is exactly the exponent in the manuscript's all-jet class.

theorem NavierStokes.ParticularWaveBounds.real_inner_class {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData E} {w : ℕ → E → ℝ} {α : ℝ} {u v : ℕ → E → ProblemStatement.Space} (hu : WeightedClasses.UnweightedClass s 0 u) (hv : WeightedClasses.MemClass s w α v) : WeightedClasses.MemClass s w α fun (n : ℕ) (x : E) => inner ℝ (u n x) (v n x)

theorem NavierStokes.ParticularWaveBounds.pressureCoefficient_class {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData E} {w : ℕ → E → ℝ} {α : ℝ} {N Ndot a f : ℕ → E → ProblemStatement.Space} {A : ℕ → E → ProblemStatement.Space →L[ℝ] ProblemStatement.Space} (hN : PhaseJetBounds.PolynomialJets (CurlClassBounds.phaseDomain s) N) (hNdot : WeightedClasses.UnweightedClass s 0 Ndot) (hA : WeightedClasses.UnweightedClass s 0 A) (ha : WeightedClasses.MemClass s w α a) (hf : WeightedClasses.MemClass s w α f) {b M : ℝ} (hb : 0 < b) (hlower : ∀ (n : ℕ), ∀ x ∈ s.domain, b ≤ ‖N n x‖) (hupper : ∀ (n : ℕ), ∀ x ∈ s.domain, ‖N n x‖ ≤ M) : WeightedClasses.MemClass s w α fun (n : ℕ) (x : E) => TangentProjection.pressureCoefficient (N n x) (Ndot n x) (a n x) ((A n x) (a n x)) (f n x)

Actual normal, normal-motion, action, and source jets give the pressure numerator and its inverse-normal normalization.

theorem NavierStokes.ParticularWaveBounds.pressure_class {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData E} {w : ℕ → E → ℝ} {α : ℝ} {N Ndot a f : ℕ → E → ProblemStatement.Space} {A : ℕ → E → ProblemStatement.Space →L[ℝ] ProblemStatement.Space} (hN : PhaseJetBounds.PolynomialJets (CurlClassBounds.phaseDomain s) N) (hNdot : WeightedClasses.UnweightedClass s 0 Ndot) (hA : WeightedClasses.UnweightedClass s 0 A) (ha : WeightedClasses.MemClass s w α a) (hf : WeightedClasses.MemClass s w α f) {b M : ℝ} (hb : 0 < b) (hlower : ∀ (n : ℕ), ∀ x ∈ s.domain, b ≤ ‖N n x‖) (hupper : ∀ (n : ℕ), ∀ x ∈ s.domain, ‖N n x‖ ≤ M) {frequency : ℕ → ℝ} (hfreq : WeightedClasses.BandBound s (1 / 2) fun (n : ℕ) => 1 / frequency n) : WeightedClasses.MemClass s w (α + 1 / 2) fun (n : ℕ) (x : E) => Complex.I * ↑(TangentProjection.pressureCoefficient (N n x) (Ndot n x) (a n x) ((A n x) (a n x)) (f n x)) / ↑(frequency n)

Multiplication by the actual inverse carrier supplies the half-power gain in the pressure; all derivatives are still the actual derivatives.

noncomputable def NavierStokes.ParticularWaveBounds.projectedPressure {E : Type u_1} (frequency : ℝ) (N Ndot u action source : E → ProblemStatement.Space) (x : E) : ℂ

Projected pressure, given by Complex.I * (TangentProjection.pressureCoefficient (N x) (Ndot x) (u x) (action x) (source x) : ℂ) / (frequency : ℂ).

Equations

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

theorem NavierStokes.ParticularWaveBounds.principal_eq_neg_source_of_projected {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (ε frequency : ℝ) (hfrequency : frequency ≠ 0) (R F G Φ : E → ℝ) (Vr Vθ Vz Vf : E → E) (u Ndot action source : E → ProblemStatement.Space) {x : E} (hu : DifferentiableAt ℝ u x) (hdu : HarmonicCalculus.along Vf u x = TangentProjection.projectedRhs (HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ x) (Ndot x) (u x) (action x) (source x) (ε * frequency ^ 2 * ‖HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ x‖ ^ 2)) (haction : CurlClassBounds.complexify (action x) = LinearWaveResidual.shear R F G Vr (fun (y : E) => CurlClassBounds.complexify (u y)) x) : LinearWaveResidual.principal ε frequency R F G Vr Vθ Vz Vf Φ (fun (y : E) => CurlClassBounds.complexify (u y)) (projectedPressure frequency (HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ) Ndot u action source) x = -CurlClassBounds.complexify (source x)

The actual projected directional equation implies the exact principal PDE cancellation. It works with any initial value and therefore also with the nonzero homogeneous primary seed.

noncomputable def NavierStokes.ParticularWaveBounds.copyVelocity {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (k : TorusInverse.Frequency) (p : P × TorusInverse.Plane) : HarmonicCalculus.ComplexVector

Copy velocity, given by CurlClassBounds.complexify (t.linearData.copySolve g hab k p).

Equations

• NavierStokes.ParticularWaveBounds.copyVelocity t g hab k p = NavierStokes.CurlClassBounds.complexify (t.linearData.copySolve g hab k p)

theorem NavierStokes.ParticularWaveBounds.normalDot_complexify (N a : ProblemStatement.Space) : HarmonicCalculus.normalDot N (CurlClassBounds.complexify a) = ↑(inner ℝ N a)

theorem NavierStokes.ParticularWaveBounds.copyVelocity_tangent {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) {U : Set P} (k : TorusInverse.Frequency) (hA : ContinuousOn t.linearData.coefficient (U ×ˢ Set.univ)) (hB : ContinuousOn t.linearData.forcingMap (U ×ˢ Set.univ)) (hf : ContinuousOn t.source (U ×ˢ Set.univ)) (hδ : ContinuousOn t.damping (U ×ˢ Set.univ)) {p : P} (hp : p ∈ U) (Y : TorusInverse.Plane) (hn0 : ∀ v ∈ Set.Icc a b, t.normal (p, (g.coordinates k Y).1, v) ≠ 0) (hn : ∀ v ∈ Set.Icc a b, HasDerivAt (fun (r : ℝ) => t.normal (p, (g.coordinates k Y).1, r)) (t.normalDot (p, (g.coordinates k Y).1, v)) v) (heta : (g.coordinates k Y).2 ∈ Set.Icc a b) : HarmonicCalculus.normalDot (t.normal (p, g.coordinates k Y)) (copyVelocity t g hab k (p, Y)) = 0

Tangency is propagated by the constructed ODE, then transferred to the complex coefficient used in the harmonic field.

theorem NavierStokes.ParticularWaveBounds.copySolve_principal {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) {U : Set P} (hU : IsOpen U) (k : TorusInverse.Frequency) (hA : ContDiffOn ℝ (↑⊤) t.linearData.coefficient (U ×ˢ Set.univ)) (hB : ContDiffOn ℝ (↑⊤) t.linearData.forcingMap (U ×ˢ Set.univ)) (hf : ContDiffOn ℝ (↑⊤) t.source (U ×ˢ Set.univ)) (ε frequency : ℝ) (hfrequency : frequency ≠ 0) (R F G Φ : P × TorusInverse.Plane → ℝ) (Vr Vθ Vz : P × TorusInverse.Plane → P × TorusInverse.Plane) {p : P} (hp : p ∈ U) (Y : TorusInverse.Plane) (heta : (g.coordinates k Y).2 ∈ Set.Ioo a b) (hN : HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ (p, Y) = t.normal (p, g.coordinates k Y)) (hδ : t.damping (p, g.coordinates k Y) = ε * frequency ^ 2 * ‖HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ (p, Y)‖ ^ 2) (hK : CurlClassBounds.complexify ((t.action (p, g.coordinates k Y)) (t.linearData.copySolve g hab k (p, Y))) = LinearWaveResidual.shear R F G Vr (copyVelocity t g hab k) (p, Y)) : LinearWaveResidual.principal ε frequency R F G Vr Vθ Vz (fun (x : P × TorusInverse.Plane) => (0, slotDirection g)) Φ (copyVelocity t g hab k) (copyPressure t g hab k frequency) (p, Y) = -CurlClassBounds.complexify (t.source (p, Y))

The pressure in copyPressure cancels the actual principal operator of the copy wave. The three matching hypotheses identify only primitive normal, damping, and base-action data with the displayed physical operator.

noncomputable def NavierStokes.ParticularWaveBounds.copyCoefficients {P : Type} (base : LinearWaveBounds.WaveCoefficients (P × TorusInverse.Plane)) (t : ℕ → CommonCoverSolve.TangentData P ProblemStatement.Space) (g : ℕ → CommonCoverSolve.Geometry) (copy : ℕ → TorusInverse.Frequency) (L : ℕ → ℝ) (hL : ∀ (n : ℕ), 0 < L n) : LinearWaveBounds.WaveCoefficients (P × TorusInverse.Plane)

The coefficient family to which the cutoff and exact-curl construction is applied; neither velocity nor pressure is supplied as an output input.

Equations

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

theorem NavierStokes.ParticularWaveBounds.copyVelocity_class {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {s : WeightedClasses.StripData (P × TorusInverse.Plane)} {W : ℕ → P × TorusInverse.Plane → ℝ} {α : ℝ} {t : ℕ → CommonCoverSolve.TangentData P ProblemStatement.Space} {g : ℕ → CommonCoverSolve.Geometry} {copy : ℕ → TorusInverse.Frequency} {L : ℕ → ℝ} {hL : ∀ (n : ℕ), 0 < L n} (hu : WeightedClasses.WaveClass s W α fun (n : ℕ) => (t n).linearData.copySolve (g n) ⋯ (copy n)) : WeightedClasses.WaveClass s W α fun (n : ℕ) => copyVelocity (t n) (g n) ⋯ (copy n)

theorem NavierStokes.ParticularWaveBounds.copyPressure_class {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {s : WeightedClasses.StripData (P × TorusInverse.Plane)} {W : ℕ → P × TorusInverse.Plane → ℝ} {α : ℝ} {t : ℕ → CommonCoverSolve.TangentData P ProblemStatement.Space} {g : ℕ → CommonCoverSolve.Geometry} {copy : ℕ → TorusInverse.Frequency} {L : ℕ → ℝ} {hL : ∀ (n : ℕ), 0 < L n} (hN : PhaseJetBounds.PolynomialJets (CurlClassBounds.phaseDomain s) fun (n : ℕ) (p : P × TorusInverse.Plane) => (t n).normal (nativePoint (g n) (copy n) p)) (hNdot : WeightedClasses.UnweightedClass s 0 fun (n : ℕ) (p : P × TorusInverse.Plane) => (t n).normalDot (nativePoint (g n) (copy n) p)) (hA : WeightedClasses.UnweightedClass s 0 fun (n : ℕ) (p : P × TorusInverse.Plane) => (t n).action (nativePoint (g n) (copy n) p)) (hu : WeightedClasses.WaveClass s W α fun (n : ℕ) => (t n).linearData.copySolve (g n) ⋯ (copy n)) (hf : WeightedClasses.WaveClass s W α fun (n : ℕ) => (t n).source) {b M : ℝ} (hb : 0 < b) (hlower : ∀ (n : ℕ), ∀ p ∈ s.domain, b ≤ ‖(t n).normal (nativePoint (g n) (copy n) p)‖) (hupper : ∀ (n : ℕ), ∀ p ∈ s.domain, ‖(t n).normal (nativePoint (g n) (copy n) p)‖ ≤ M) {frequency : ℕ → ℝ} (hfreq : WeightedClasses.BandBound s (1 / 2) fun (n : ℕ) => 1 / frequency n) : WeightedClasses.WaveClass s W (α + 1 / 2) fun (n : ℕ) => copyPressure (t n) (g n) ⋯ (copy n) (frequency n)

noncomputable def NavierStokes.ParticularWaveBounds.frameForcingLinear {Q : Type} (d : PrimaryODE.FrameData Q) (z : Q × ℝ) : PrimaryODE.Space →L[ℝ] PrimaryODE.State

The explicit source projection in the two-dimensional moving frame.

Equations

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

@[simp]

theorem NavierStokes.ParticularWaveBounds.frameForcingLinear_apply {Q : Type} (d : PrimaryODE.FrameData Q) (f : Q × ℝ → PrimaryODE.Space) (z : Q × ℝ) : (frameForcingLinear d z) (f z) = d.forcing f z

theorem NavierStokes.ParticularWaveBounds.forcing_eq_columns {Q : Type} (d : PrimaryODE.FrameData Q) (f : Q × ℝ → PrimaryODE.Space) (z : Q × ℝ) : d.forcing f z = ∑ i : Fin 3, (f z).ofLp i • d.forcing (fun (x : Q × ℝ) => ProblemStatement.coordinateVector i) z

theorem NavierStokes.ParticularWaveBounds.frame_forcing_envelope_jets {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {ι : Type u_1} {D : PhaseJetBounds.Domain ι (Q × ℝ)} {d : ι → PrimaryODE.FrameData Q} (hd : PhaseJetBounds.FrameJets D d) {w : ι → Q × ℝ → ℝ} {f : ι → Q × ℝ → PrimaryODE.Space} (hf : PrimaryPulseBounds.EnvelopeJets D w f) : PrimaryPulseBounds.EnvelopeJets D w fun (i : ι) => (d i).forcing (f i)

The actual moving-frame source projection preserves the entire source envelope, including its small prefactor.

theorem NavierStokes.ParticularWaveBounds.forced_modal_family_envelope_jets {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {ι : Type u_1} (D : PhaseJetBounds.Domain ι Q) (V : ι → Set ℝ) (hV : ∀ (i : ι), IsOpen (V i)) (L : ι → ℝ) (hL : ∀ (i : ι), 0 < L i) (hI : ∀ (i : ι), Set.Icc 0 (L i) ⊆ V i) (d : ι → PrimaryODE.FrameData Q) (hd : PhaseJetBounds.FrameJets (PrimaryPulseBounds.productDomain D V hV) d) (harmonic : ℤ) (hharmonic : harmonic ≠ 0) (W rate referenceDamping : ι → ℝ → ℝ) (hW : ∀ (i : ι) (t : ℝ), 0 < W i t) (hdW : ∀ (i : ι) (t : ℝ), HasDerivAt (W i) (rate i t * W i t) t) (w : ι → Q → ℝ) (hw : ∀ (i : ι), ∀ p ∈ D.carrier i, 0 ≤ w i p) (f : ι → Q × ℝ → PrimaryODE.Space) (hf : PrimaryPulseBounds.EnvelopeJets (PrimaryPulseBounds.productDomain D V hV) (fun (i : ι) (z : Q × ℝ) => w i z.1 * W i z.2) f) {K C E : ℝ} (hK : 1 ≤ K) (hC : 0 ≤ C) (hE : 0 ≤ E) (hslot : ∀ (i : ι), L i ≤ K * D.scale i) (href : ∀ (i : ι), ∀ p ∈ D.carrier i, ∀ v ∈ Set.Icc 0 (L i), rate i v = (d i).eigenvalue (p, v) - referenceDamping i v) (hlam : ∀ (i : ι), ∀ p ∈ D.carrier i, ∀ v ∈ Set.Icc 0 (L i), 0 ≤ (d i).eigenvalue (p, v)) (hvisc : ∀ (i : ι), ∀ p ∈ D.carrier i, ∀ v ∈ Set.Icc 0 (L i), 0 ≤ (d i).viscosity (p, v)) (hviscError : ∀ (i : ι), ∀ p ∈ D.carrier i, ∀ v ∈ Set.Icc 0 (L i), referenceDamping i v - E / D.scale i ≤ (d i).viscosity (p, v)) (herror : ∀ (i : ι), ∀ p ∈ D.carrier i, ∀ v ∈ Set.Icc 0 (L i), |(d i).error11 (p, v)| ≤ C / D.scale i ∧ |(d i).error12 (p, v)| ≤ C / D.scale i ∧ |(d i).error21 (p, v)| ≤ C / D.scale i ∧ |(d i).error22 (p, v)| ≤ C / D.scale i) : PrimaryPulseBounds.EnvelopeJets (PrimaryPulseBounds.productDomain D (fun (i : ι) => Set.Ioo 0 (L i)) ⋯) (fun (i : ι) (z : Q × ℝ) => w i z.1 * W i z.2) fun (i : ι) (z : Q × ℝ) => PrimaryODE.solution ⋯ (d i) harmonic (fun (x : Q) => 0) (f i) z.1 z.2

A forced family in the genuine modal coordinates. The energy estimate comes from the four explicit modal errors and nonnegative viscosity, rather than an energy hypothesis about the ambient projected operator.

theorem NavierStokes.ParticularWaveBounds.forced_ambient_family_envelope_jets {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {ι : Type u_1} (D : PhaseJetBounds.Domain ι Q) (V : ι → Set ℝ) (hV : ∀ (i : ι), IsOpen (V i)) (L : ι → ℝ) (hL : ∀ (i : ι), 0 < L i) (hI : ∀ (i : ι), Set.Icc 0 (L i) ⊆ V i) (d : ι → PrimaryODE.FrameData Q) (hd : PhaseJetBounds.FrameJets (PrimaryPulseBounds.productDomain D V hV) d) (harmonic : ℤ) (hharmonic : harmonic ≠ 0) (W rate referenceDamping : ι → ℝ → ℝ) (hW : ∀ (i : ι) (t : ℝ), 0 < W i t) (hdW : ∀ (i : ι) (t : ℝ), HasDerivAt (W i) (rate i t * W i t) t) (w : ι → Q → ℝ) (hw : ∀ (i : ι), ∀ p ∈ D.carrier i, 0 ≤ w i p) (f : ι → Q × ℝ → PrimaryODE.Space) (hf : PrimaryPulseBounds.EnvelopeJets (PrimaryPulseBounds.productDomain D V hV) (fun (i : ι) (z : Q × ℝ) => w i z.1 * W i z.2) f) {K C E : ℝ} (hK : 1 ≤ K) (hC : 0 ≤ C) (hE : 0 ≤ E) (hslot : ∀ (i : ι), L i ≤ K * D.scale i) (href : ∀ (i : ι), ∀ p ∈ D.carrier i, ∀ v ∈ Set.Icc 0 (L i), rate i v = (d i).eigenvalue (p, v) - referenceDamping i v) (hlam : ∀ (i : ι), ∀ p ∈ D.carrier i, ∀ v ∈ Set.Icc 0 (L i), 0 ≤ (d i).eigenvalue (p, v)) (hvisc : ∀ (i : ι), ∀ p ∈ D.carrier i, ∀ v ∈ Set.Icc 0 (L i), 0 ≤ (d i).viscosity (p, v)) (hviscError : ∀ (i : ι), ∀ p ∈ D.carrier i, ∀ v ∈ Set.Icc 0 (L i), referenceDamping i v - E / D.scale i ≤ (d i).viscosity (p, v)) (herror : ∀ (i : ι), ∀ p ∈ D.carrier i, ∀ v ∈ Set.Icc 0 (L i), |(d i).error11 (p, v)| ≤ C / D.scale i ∧ |(d i).error12 (p, v)| ≤ C / D.scale i ∧ |(d i).error21 (p, v)| ≤ C / D.scale i ∧ |(d i).error22 (p, v)| ≤ C / D.scale i) : PrimaryPulseBounds.EnvelopeJets (PrimaryPulseBounds.productDomain D (fun (i : ι) => Set.Ioo 0 (L i)) ⋯) (fun (i : ι) (z : Q × ℝ) => w i z.1 * W i z.2) fun (i : ι) (z : Q × ℝ) => PrimaryODE.ambientSolution ⋯ (d i) harmonic (fun (x : Q) => 0) (f i) z.1 z.2

The same forced estimate after actual moving-frame reconstruction. The reference energy bound is used only in the modal two-dimensional state.

noncomputable def NavierStokes.ParticularWaveBounds.ambientJetConstant (N : ℕ) : ℝ

Ambient jet constant, constructed using 2.

Equations

• NavierStokes.ParticularWaveBounds.ambientJetConstant N = 2 ^ N * (‖EuclideanSpace.proj 0‖ + ‖EuclideanSpace.proj 1‖)

theorem NavierStokes.ParticularWaveBounds.ambient_jet_bound {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] (d : PrimaryODE.FrameData Q) {T : Set (Q × ℝ)} (hT : IsOpen T) {u : Q × ℝ → PrimaryODE.State} (hu : ContDiffOn ℝ (↑⊤) u T) (hc : ∀ (i : Fin 2), ContDiffOn ℝ (↑⊤) (PrimaryPulseBounds.synthesisColumn d i) T) {x : Q × ℝ} (hx : x ∈ T) {A B : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) {N j : ℕ} (hj : j ≤ N) (huj : ∀ k ≤ N, ‖iteratedFDeriv ℝ k u x‖ ≤ A) (hcj : ∀ (i : Fin 2), ∀ k ≤ N, ‖iteratedFDeriv ℝ k (PrimaryPulseBounds.synthesisColumn d i) x‖ ≤ B) : ‖iteratedFDeriv ℝ j (fun (y : Q × ℝ) => d.ambient y (u y)) x‖ ≤ ambientJetConstant N * A * B

Finite full-jet bound for actual reconstruction, suitable for a source majorant whose edge exponent depends on the derivative order.

theorem NavierStokes.ParticularWaveBounds.copySolve_jet_bound_from_modal {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (d : PrimaryODE.FrameData (P × ℝ)) (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (harmonic : ℤ) (g : CommonCoverSolve.Geometry) (copy : TorusInverse.Frequency) {L S K μ w : ℝ} (hL : 0 < L) (hS : 1 ≤ S) (hK : 1 ≤ K) (hμ : 0 ≤ μ) (hw : 0 ≤ w) (hslot : L ≤ K * S) (hExp : Real.exp (μ * L) ≤ K) (Ω : Set (P × TorusInverse.Plane)) (I : Set ℝ) (hΩ : IsOpen Ω) (hI : IsOpen I) (hLI : Set.Icc 0 L ⊆ I) (bridge : PrimaryCopyBridge.Inputs d t harmonic g copy Ω 0 L) (hA : ContDiffOn ℝ (↑⊤) ((PrimaryCopyBridge.copyFrame d g copy).coefficient harmonic) (Ω ×ˢ I)) (hf : ContDiffOn ℝ (↑⊤) ((PrimaryCopyBridge.copyFrame d g copy).forcing (PrimaryCopyBridge.copySource t.source g copy)) (Ω ×ˢ I)) (hc : ∀ (i : Fin 2), ContDiffOn ℝ (↑⊤) (PrimaryPulseBounds.synthesisColumn (PrimaryCopyBridge.copyFrame d g copy) i) (Ω ×ˢ I)) (W rate : ℝ → ℝ) (hW : ∀ (v : ℝ), 0 < W v) (hdW : ∀ (v : ℝ), HasDerivAt W (rate v * W v) v) {p : P × TorusInverse.Plane} (hp : p ∈ Ω) (heta : (g.coordinates copy p.2).2 ∈ Set.Ioo 0 L) (henergy : ∀ v ∈ Set.Icc 0 L, ∀ (x : PrimaryODE.State), inner ℝ x (((PrimaryCopyBridge.copyFrame d g copy).coefficient harmonic (p, v)) x) ≤ (rate v + μ) * ‖x‖ ^ 2) (m N : ℕ) (hAj : ∀ j ≤ N, ∀ v ∈ Set.Icc 0 L, ‖iteratedFDeriv ℝ j ((PrimaryCopyBridge.copyFrame d g copy).coefficient harmonic) (p, v)‖ ≤ K * S ^ m) (hfj : ∀ j ≤ N, ∀ v ∈ Set.Icc 0 L, ‖iteratedFDeriv ℝ j ((PrimaryCopyBridge.copyFrame d g copy).forcing (PrimaryCopyBridge.copySource t.source g copy)) (p, v)‖ ≤ w * K * S ^ m * W v) (hcj : ∀ (i : Fin 2), ∀ j ≤ N, ∀ v ∈ Set.Icc 0 L, ‖iteratedFDeriv ℝ j (PrimaryPulseBounds.synthesisColumn (PrimaryCopyBridge.copyFrame d g copy) i) (p, v)‖ ≤ K * S ^ m) (j : ℕ) (hj : j ≤ N) : ‖iteratedFDeriv ℝ j (t.linearData.copySolve g ⋯ copy) p‖ ≤ ambientJetConstant N * (w * (2 ^ (N + 1) * PrimaryPulseBounds.rescaleConstant N K ^ 3) ^ (N + 1) * S ^ ((m + 2) * (N + 1)) * W (g.coordinates copy p.2).2) * (K * S ^ m) * CommonCoverClass.argumentCost g ^ j

Full current-copy derivatives from the modal ODE and genuine frame reconstruction. The reference-energy hypothesis concerns the actual two-dimensional modal coefficient, never the ambient projected operator.

theorem NavierStokes.ParticularWaveBounds.copySolve_contDiffOn_from_modal {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (d : PrimaryODE.FrameData (P × ℝ)) (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (harmonic : ℤ) (g : CommonCoverSolve.Geometry) (copy : TorusInverse.Frequency) {L : ℝ} (hL : 0 < L) {Ω : Set (P × TorusInverse.Plane)} {I : Set ℝ} (hΩ : IsOpen Ω) (hI : IsOpen I) (hLI : Set.Icc 0 L ⊆ I) (bridge : PrimaryCopyBridge.Inputs d t harmonic g copy Ω 0 L) (hA : ContDiffOn ℝ (↑⊤) ((PrimaryCopyBridge.copyFrame d g copy).coefficient harmonic) (Ω ×ˢ I)) (hf : ContDiffOn ℝ (↑⊤) ((PrimaryCopyBridge.copyFrame d g copy).forcing (PrimaryCopyBridge.copySource t.source g copy)) (Ω ×ˢ I)) (hc : ∀ (i : Fin 2), ContDiffOn ℝ (↑⊤) (PrimaryPulseBounds.synthesisColumn (PrimaryCopyBridge.copyFrame d g copy) i) (Ω ×ˢ I)) (heta : ∀ p ∈ Ω, (g.coordinates copy p.2).2 ∈ Set.Ioo 0 L) : ContDiffOn ℝ (↑⊤) (t.linearData.copySolve g ⋯ copy) Ω

Joint smoothness of the actual copy solve from local modal data on a neighborhood of the finite integration interval.

structure NavierStokes.ParticularWaveBounds.ModalCopyControl {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (s : WeightedClasses.StripData (P × TorusInverse.Plane)) (α : ℝ) (d : ℕ → PrimaryODE.FrameData (P × ℝ)) (t : ℕ → CommonCoverSolve.TangentData P ProblemStatement.Space) (harmonic : ℤ) (g : ℕ → CommonCoverSolve.Geometry) (copy : ℕ → TorusInverse.Frequency) (L : ℕ → ℝ) (W : ℕ → ℝ → ℝ) : Type

Input bounds for the genuine modal equation on every copy path. The energy bound is in the two-dimensional modal state. The edge exponent in input_jets may depend on the requested derivative order.

• interval : ℕ → Set ℝ

  Interval of ModalCopyControl, of type ℕ → Set ℝ.

• open_interval (n : ℕ) : IsOpen (self.interval n)
• length_pos (n : ℕ) : 0 < L n
• contains_interval (n : ℕ) : Set.Icc 0 (L n) ⊆ self.interval n
• bridge (n : ℕ) : PrimaryCopyBridge.Inputs (d n) (t n) harmonic (g n) (copy n) s.domain 0 (L n)
• coefficient_smooth (n : ℕ) : ContDiffOn ℝ (↑⊤) ((PrimaryCopyBridge.copyFrame (d n) (g n) (copy n)).coefficient harmonic) (s.domain ×ˢ self.interval n)
• forcing_smooth (n : ℕ) : ContDiffOn ℝ (↑⊤) ((PrimaryCopyBridge.copyFrame (d n) (g n) (copy n)).forcing (PrimaryCopyBridge.copySource (t n).source (g n) (copy n))) (s.domain ×ˢ self.interval n)
• columns_smooth (n : ℕ) (i : Fin 2) : ContDiffOn ℝ (↑⊤) (PrimaryPulseBounds.synthesisColumn (PrimaryCopyBridge.copyFrame (d n) (g n) (copy n)) i) (s.domain ×ˢ self.interval n)
• current_slot (n : ℕ) (p : P × TorusInverse.Plane) : p ∈ s.domain → ((g n).coordinates (copy n) p.2).2 ∈ Set.Ioo 0 (L n)
• rate : ℕ → ℝ → ℝ

  Rate of ModalCopyControl, of type ℕ → ℝ → ℝ.

• envelope_pos (n : ℕ) (v : ℝ) : 0 < W n v
• envelope_deriv (n : ℕ) (v : ℝ) : HasDerivAt (W n) (self.rate n v * W n v) v
• errorRate : ℕ → ℝ

  Error rate of ModalCopyControl, of type ℕ → ℝ.

• errorRate_nonneg (n : ℕ) : 0 ≤ self.errorRate n
• boundConstant : ℝ

  Bound constant of ModalCopyControl, of type ℝ.

• constant_ge_one : 1 ≤ self.boundConstant
• coordinatePower : ℕ

  Coordinate power of ModalCopyControl, of type ℕ.

• length_bound (n : ℕ) : L n ≤ self.boundConstant * s.slow n
• exponential_bound (n : ℕ) : Real.exp (self.errorRate n * L n) ≤ self.boundConstant
• coordinate_bound (n : ℕ) : CommonCoverClass.argumentCost (g n) ≤ self.boundConstant * s.slow n ^ self.coordinatePower
• energy (n : ℕ) (p : P × TorusInverse.Plane) : p ∈ s.domain → ∀ v ∈ Set.Icc 0 (L n), ∀ (x : PrimaryODE.State), inner ℝ x (((PrimaryCopyBridge.copyFrame (d n) (g n) (copy n)).coefficient harmonic (p, v)) x) ≤ (self.rate n v + self.errorRate n) * ‖x‖ ^ 2
• input_jets (N : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∃ (m : ℕ), ∀ (n : ℕ), ∀ p ∈ s.domain, ∀ j ≤ N, ∀ v ∈ Set.Icc 0 (L n), ‖iteratedFDeriv ℝ j ((PrimaryCopyBridge.copyFrame (d n) (g n) (copy n)).coefficient harmonic) (p, v)‖ ≤ C * s.growth n p ^ m ∧ ‖iteratedFDeriv ℝ j ((PrimaryCopyBridge.copyFrame (d n) (g n) (copy n)).forcing (PrimaryCopyBridge.copySource (t n).source (g n) (copy n))) (p, v)‖ ≤ s.epsilon n ^ α * √(s.zeta p) * C * s.growth n p ^ m * W n v ∧ ∀ (i : Fin 2), ‖iteratedFDeriv ℝ j (PrimaryPulseBounds.synthesisColumn (PrimaryCopyBridge.copyFrame (d n) (g n) (copy n)) i) (p, v)‖ ≤ C * s.growth n p ^ m

theorem NavierStokes.ParticularWaveBounds.ModalCopyControl.contDiffOn {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {s : WeightedClasses.StripData (P × TorusInverse.Plane)} {α : ℝ} {d : ℕ → PrimaryODE.FrameData (P × ℝ)} {t : ℕ → CommonCoverSolve.TangentData P ProblemStatement.Space} {harmonic : ℤ} {g : ℕ → CommonCoverSolve.Geometry} {copy : ℕ → TorusInverse.Frequency} {L : ℕ → ℝ} {W : ℕ → ℝ → ℝ} (h : ModalCopyControl s α d t harmonic g copy L W) (hL : ∀ (n : ℕ), 0 < L n) (n : ℕ) : ContDiffOn ℝ (↑⊤) ((t n).linearData.copySolve (g n) ⋯ (copy n)) s.domain

Local joint smoothness is obtained before any quantitative estimate.

theorem NavierStokes.ParticularWaveBounds.ModalCopyControl.waveClass {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {s : WeightedClasses.StripData (P × TorusInverse.Plane)} {α : ℝ} {d : ℕ → PrimaryODE.FrameData (P × ℝ)} {t : ℕ → CommonCoverSolve.TangentData P ProblemStatement.Space} {harmonic : ℤ} {g : ℕ → CommonCoverSolve.Geometry} {copy : ℕ → TorusInverse.Frequency} {L : ℕ → ℝ} {W : ℕ → ℝ → ℝ} (h : ModalCopyControl s α d t harmonic g copy L W) (hL : ∀ (n : ℕ), 0 < L n) : WeightedClasses.WaveClass s (fun (n : ℕ) (p : P × TorusInverse.Plane) => W n ((g n).coordinates (copy n) p.2).2) α fun (n : ℕ) => (t n).linearData.copySolve (g n) ⋯ (copy n)

The actual ambient copy solution belongs to W_α, with all edge losses retained and with no ambient reference-energy assumption.

theorem NavierStokes.ParticularWaveBounds.along_copySolve_of_path {P V H : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (d : CommonCoverSolve.LinearData P V H) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (k : TorusInverse.Frequency) {Ω : Set (P × TorusInverse.Plane)} (hA : ContinuousOn (d.coefficientAlong g k) (Ω ×ˢ Set.Icc a b)) (hf : ContinuousOn (d.forcingAlong g k) (Ω ×ˢ Set.Icc a b)) (p : P) (Y : TorusInverse.Plane) (hp : (p, Y) ∈ Ω) (heta : (g.coordinates k Y).2 ∈ Set.Icc a b) (hcopy : DifferentiableAt ℝ (d.copySolve g hab k) (p, Y)) : HarmonicCalculus.along (fun (x : P × TorusInverse.Plane) => (0, slotDirection g)) (d.copySolve g hab k) (p, Y) = (d.coefficient (p, g.coordinates k Y)) (d.copySolve g hab k (p, Y)) + (d.forcingMap (p, g.coordinates k Y)) (d.source (p, Y))

Local version of the copy derivative identity. Continuity is required only on the actual finite paths, and joint differentiability can be supplied by the modal reconstruction theorem.

theorem NavierStokes.ParticularWaveBounds.copySolve_principal_of_path {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (k : TorusInverse.Frequency) {Ω : Set (P × TorusInverse.Plane)} (hA : ContinuousOn (t.linearData.coefficientAlong g k) (Ω ×ˢ Set.Icc a b)) (hf : ContinuousOn (t.linearData.forcingAlong g k) (Ω ×ˢ Set.Icc a b)) (ε frequency : ℝ) (hfrequency : frequency ≠ 0) (R F G Φ : P × TorusInverse.Plane → ℝ) (Vr Vθ Vz : P × TorusInverse.Plane → P × TorusInverse.Plane) (p : P) (Y : TorusInverse.Plane) (hp : (p, Y) ∈ Ω) (heta : (g.coordinates k Y).2 ∈ Set.Icc a b) (hu : DifferentiableAt ℝ (t.linearData.copySolve g hab k) (p, Y)) (hN : HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ (p, Y) = t.normal (p, g.coordinates k Y)) (hδ : t.damping (p, g.coordinates k Y) = ε * frequency ^ 2 * ‖HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ (p, Y)‖ ^ 2) (hK : CurlClassBounds.complexify ((t.action (p, g.coordinates k Y)) (t.linearData.copySolve g hab k (p, Y))) = LinearWaveResidual.shear R F G Vr (copyVelocity t g hab k) (p, Y)) : LinearWaveResidual.principal ε frequency R F G Vr Vθ Vz (fun (x : P × TorusInverse.Plane) => (0, slotDirection g)) Φ (copyVelocity t g hab k) (copyPressure t g hab k frequency) (p, Y) = -CurlClassBounds.complexify (t.source (p, Y))

Principal cancellation using only continuity along finite paths and the actual local derivative of the copy solve.

theorem NavierStokes.ParticularWaveBounds.copyVelocity_tangent_of_modal {P : Type} [NormedAddCommGroup P] (d : PrimaryODE.FrameData (P × ℝ)) (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (harmonic : ℤ) (g : CommonCoverSolve.Geometry) (k : TorusInverse.Frequency) {a b : ℝ} (hab : a ≤ b) {Ω : Set (P × TorusInverse.Plane)} (bridge : PrimaryCopyBridge.Inputs d t harmonic g k Ω a b) {p : P × TorusInverse.Plane} (hp : p ∈ Ω) (heta : (g.coordinates k p.2).2 ∈ Set.Icc a b) : HarmonicCalculus.normalDot (t.normal (nativePoint g k p)) (copyVelocity t g hab k p) = 0

Tangency of the actual copy solve follows from frame reconstruction and uniqueness, including at both endpoints of the finite path.

noncomputable def NavierStokes.ParticularWaveBounds.realPart : HarmonicCalculus.ComplexVector →L[ℝ] ProblemStatement.Space

Real part, constructed using LinearMap.toContinuousLinearMap.

Equations

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

noncomputable def NavierStokes.ParticularWaveBounds.imagPart : HarmonicCalculus.ComplexVector →L[ℝ] ProblemStatement.Space

Imag part, constructed using LinearMap.toContinuousLinearMap.

Equations

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

@[simp]

theorem NavierStokes.ParticularWaveBounds.realPart_apply (a : HarmonicCalculus.ComplexVector) (i : Fin 3) : (realPart a).ofLp i = (a i).re

@[simp]

theorem NavierStokes.ParticularWaveBounds.imagPart_apply (a : HarmonicCalculus.ComplexVector) (i : Fin 3) : (imagPart a).ofLp i = (a i).im

noncomputable def NavierStokes.ParticularWaveBounds.complexScale (c : ℂ) : HarmonicCalculus.ComplexVector →L[ℝ] HarmonicCalculus.ComplexVector

Complex scale, given by ContinuousLinearMap.pi fun i => ((ContinuousLinearMap.mul ℝ ℂ) c).comp (ContinuousLinearMap.proj i).

Equations

• NavierStokes.ParticularWaveBounds.complexScale c = ContinuousLinearMap.pi fun (i : Fin 3) => (ContinuousLinearMap.mul ℝ ℂ) c ∘SL ContinuousLinearMap.proj i

@[simp]

theorem NavierStokes.ParticularWaveBounds.complexScale_apply (c : ℂ) (a : HarmonicCalculus.ComplexVector) : (complexScale c) a = c • a

theorem NavierStokes.ParticularWaveBounds.complex_parts (a : HarmonicCalculus.ComplexVector) : CurlClassBounds.complexify (realPart a) + Complex.I • CurlClassBounds.complexify (imagPart a) = a

noncomputable def NavierStokes.ParticularWaveBounds.realData {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (source : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) : CommonCoverSolve.TangentData P ProblemStatement.Space

Real data, given by { t with source := fun p => realPart (source p) }.

Equations

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

noncomputable def NavierStokes.ParticularWaveBounds.imagData {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (source : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) : CommonCoverSolve.TangentData P ProblemStatement.Space

Imag data, given by { t with source := fun p => imagPart (source p) }.

Equations

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

noncomputable def NavierStokes.ParticularWaveBounds.complexCopyVelocity {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (source : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (copy : TorusInverse.Frequency) (p : P × TorusInverse.Plane) : HarmonicCalculus.ComplexVector

The actual particular coefficient for an arbitrary complex harmonic source, obtained from two real Volterra solves with the same geometry.

Equations

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

noncomputable def NavierStokes.ParticularWaveBounds.complexCopyPressure {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (source : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (copy : TorusInverse.Frequency) (frequency : ℝ) (p : P × TorusInverse.Plane) : ℂ

Complex copy pressure, given by copyPressure (realData t source) g hab copy frequency p + Complex.I * copyPressure (imagData t source) g hab copy frequency p.

Equations

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

theorem NavierStokes.ParticularWaveBounds.complexCopyVelocity_eq_parts {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (source : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (copy : TorusInverse.Frequency) : complexCopyVelocity t source g hab copy = fun (x : P × TorusInverse.Plane) => copyVelocity (realData t source) g hab copy x + Complex.I • copyVelocity (imagData t source) g hab copy x

Function-level equations keep the finite-path solver opaque when the principal operator is assembled.

theorem NavierStokes.ParticularWaveBounds.complexCopyPressure_eq_parts {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (source : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (copy : TorusInverse.Frequency) (frequency : ℝ) : complexCopyPressure t source g hab copy frequency = fun (x : P × TorusInverse.Plane) => copyPressure (realData t source) g hab copy frequency x + Complex.I * copyPressure (imagData t source) g hab copy frequency x

theorem NavierStokes.ParticularWaveBounds.copyVelocity_component_differentiable {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (copy : TorusInverse.Frequency) {p : P × TorusInverse.Plane} (hu : DifferentiableAt ℝ (t.linearData.copySolve g hab copy) p) (i : Fin 3) : DifferentiableAt ℝ (fun (z : P × TorusInverse.Plane) => copyVelocity t g hab copy z i) p

noncomputable def NavierStokes.ParticularWaveBounds.complexCopyCoefficients {P : Type} (base : LinearWaveBounds.WaveCoefficients (P × TorusInverse.Plane)) (t : ℕ → CommonCoverSolve.TangentData P ProblemStatement.Space) (source : ℕ → P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : ℕ → CommonCoverSolve.Geometry) (copy : ℕ → TorusInverse.Frequency) (L : ℕ → ℝ) (hL : ∀ (n : ℕ), 0 < L n) : LinearWaveBounds.WaveCoefficients (P × TorusInverse.Plane)

Complex copy coefficients as an element of LinearWaveBounds.WaveCoefficients (P × Plane).

Equations

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

theorem NavierStokes.ParticularWaveBounds.complexCopyVelocity_class {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {s : WeightedClasses.StripData (P × TorusInverse.Plane)} {W : ℕ → P × TorusInverse.Plane → ℝ} {α : ℝ} {t : ℕ → CommonCoverSolve.TangentData P ProblemStatement.Space} {source : ℕ → P × TorusInverse.Plane → HarmonicCalculus.ComplexVector} {g : ℕ → CommonCoverSolve.Geometry} {copy : ℕ → TorusInverse.Frequency} {L : ℕ → ℝ} {hL : ∀ (n : ℕ), 0 < L n} (hr : WeightedClasses.WaveClass s W α fun (n : ℕ) => (realData (t n) (source n)).linearData.copySolve (g n) ⋯ (copy n)) (hi : WeightedClasses.WaveClass s W α fun (n : ℕ) => (imagData (t n) (source n)).linearData.copySolve (g n) ⋯ (copy n)) : WeightedClasses.WaveClass s W α fun (n : ℕ) => complexCopyVelocity (t n) (source n) (g n) ⋯ (copy n)

theorem NavierStokes.ParticularWaveBounds.principal_add_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (ε frequency : ℝ) (R F G Φ : E → ℝ) (Vr Vθ Vz Vf : E → E) (a b : E → HarmonicCalculus.ComplexVector) (p q : E → ℂ) (c : ℂ) {x : E} (ha : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : E) => a y i) x) (hb : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : E) => b y i) x) : LinearWaveResidual.principal ε frequency R F G Vr Vθ Vz Vf Φ (fun (y : E) => a y + c • b y) (fun (y : E) => p y + c * q y) x = LinearWaveResidual.principal ε frequency R F G Vr Vθ Vz Vf Φ a p x + c • LinearWaveResidual.principal ε frequency R F G Vr Vθ Vz Vf Φ b q x

Complex linearity of the displayed principal operator. The directional derivative terms are differentiated before the algebraic combination.

theorem NavierStokes.ParticularWaveBounds.complexCopy_principal {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (source : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) {U : Set P} (hU : IsOpen U) (copy : TorusInverse.Frequency) (hA : ContDiffOn ℝ (↑⊤) t.linearData.coefficient (U ×ˢ Set.univ)) (hB : ContDiffOn ℝ (↑⊤) t.linearData.forcingMap (U ×ˢ Set.univ)) (hf : ContDiffOn ℝ (↑⊤) source (U ×ˢ Set.univ)) (ε frequency : ℝ) (hfrequency : frequency ≠ 0) (R F G Φ : P × TorusInverse.Plane → ℝ) (Vr Vθ Vz : P × TorusInverse.Plane → P × TorusInverse.Plane) {p : P} (hp : p ∈ U) (Y : TorusInverse.Plane) (heta : (g.coordinates copy Y).2 ∈ Set.Ioo a b) (hN : HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ (p, Y) = t.normal (p, g.coordinates copy Y)) (hδ : t.damping (p, g.coordinates copy Y) = ε * frequency ^ 2 * ‖HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ (p, Y)‖ ^ 2) (hK : ∀ (v : ProblemStatement.Space), CurlClassBounds.complexify ((t.action (p, g.coordinates copy Y)) v) = LinearWaveResidual.shear R F G Vr (fun (x : P × TorusInverse.Plane) => CurlClassBounds.complexify v) (p, Y)) : LinearWaveResidual.principal ε frequency R F G Vr Vθ Vz (fun (x : P × TorusInverse.Plane) => (0, slotDirection g)) Φ (complexCopyVelocity t source g hab copy) (complexCopyPressure t source g hab copy frequency) (p, Y) = -source (p, Y)

Exact cancellation for an arbitrary complex source, obtained from the two actual real copy solves.

theorem NavierStokes.ParticularWaveBounds.complexCopy_principal_of_path {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (source : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (copy : TorusInverse.Frequency) {Ω : Set (P × TorusInverse.Plane)} (hA : ContinuousOn (t.linearData.coefficientAlong g copy) (Ω ×ˢ Set.Icc a b)) (hfr : ContinuousOn ((realData t source).linearData.forcingAlong g copy) (Ω ×ˢ Set.Icc a b)) (hfi : ContinuousOn ((imagData t source).linearData.forcingAlong g copy) (Ω ×ˢ Set.Icc a b)) (ε frequency : ℝ) (hfrequency : frequency ≠ 0) (R F G Φ : P × TorusInverse.Plane → ℝ) (Vr Vθ Vz : P × TorusInverse.Plane → P × TorusInverse.Plane) (p : P) (Y : TorusInverse.Plane) (hp : (p, Y) ∈ Ω) (heta : (g.coordinates copy Y).2 ∈ Set.Icc a b) (hur : DifferentiableAt ℝ ((realData t source).linearData.copySolve g hab copy) (p, Y)) (hui : DifferentiableAt ℝ ((imagData t source).linearData.copySolve g hab copy) (p, Y)) (hN : HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ (p, Y) = t.normal (p, g.coordinates copy Y)) (hδ : t.damping (p, g.coordinates copy Y) = ε * frequency ^ 2 * ‖HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ (p, Y)‖ ^ 2) (hK : ∀ (v : ProblemStatement.Space), CurlClassBounds.complexify ((t.action (p, g.coordinates copy Y)) v) = LinearWaveResidual.shear R F G Vr (fun (x : P × TorusInverse.Plane) => CurlClassBounds.complexify v) (p, Y)) : LinearWaveResidual.principal ε frequency R F G Vr Vθ Vz (fun (x : P × TorusInverse.Plane) => (0, slotDirection g)) Φ (complexCopyVelocity t source g hab copy) (complexCopyPressure t source g hab copy frequency) (p, Y) = -source (p, Y)

The same exact cancellation with regularity required only along the actual finite copy paths.

noncomputable def NavierStokes.ParticularWaveBounds.zeroAmplitudes {P : Type} (base : LinearWaveBounds.WaveCoefficients (P × TorusInverse.Plane)) : LinearWaveBounds.WaveCoefficients (P × TorusInverse.Plane)

Zero amplitudes, given by { base with amplitude := fun _ _ => 0, pressure := fun _ _ => 0 }.

Equations

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

structure NavierStokes.ParticularWaveBounds.CopyGeometryMatch {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (s : WeightedClasses.StripData (P × TorusInverse.Plane)) (dirs : LinearWaveBounds.GraphDirections (P × TorusInverse.Plane)) (base : LinearWaveBounds.WaveCoefficients (P × TorusInverse.Plane)) (t : ℕ → CommonCoverSolve.TangentData P ProblemStatement.Space) (g : ℕ → CommonCoverSolve.Geometry) (copy : ℕ → TorusInverse.Frequency) : Prop

Matches of primitive physical geometry with the native projected ODE. The action equality is required for every vector, not just the solution.

• normal (n : ℕ) (x : P × TorusInverse.Plane) : x ∈ s.domain → base.normal s dirs n x = (t n).normal (nativePoint (g n) (copy n) x)
• damping (n : ℕ) (x : P × TorusInverse.Plane) : x ∈ s.domain → (t n).damping (nativePoint (g n) (copy n) x) = s.epsilon n * base.frequency n ^ 2 * ‖base.normal s dirs n x‖ ^ 2
• fast (n : ℕ) : dirs.fastScale n • dirs.fast = (0, slotDirection (g n))
• action (n : ℕ) (x : P × TorusInverse.Plane) : x ∈ s.domain → ∀ (v : ProblemStatement.Space), CurlClassBounds.complexify (((t n).action (nativePoint (g n) (copy n) x)) v) = LinearWaveResidual.shear (base.radius n) (base.frequencyBase n) (base.axialBase n) (dirs.radialField n) (fun (x : P × TorusInverse.Plane) => CurlClassBounds.complexify v) x

theorem NavierStokes.ParticularWaveBounds.complexCopy_inputBounds {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {s : WeightedClasses.StripData (P × TorusInverse.Plane)} {α κ : ℝ} {dirs : LinearWaveBounds.GraphDirections (P × TorusInverse.Plane)} (base : LinearWaveBounds.WaveCoefficients (P × TorusInverse.Plane)) (t : ℕ → CommonCoverSolve.TangentData P ProblemStatement.Space) (source : ℕ → P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : ℕ → CommonCoverSolve.Geometry) (copy : ℕ → TorusInverse.Frequency) (L : ℕ → ℝ) (hL : ∀ (n : ℕ), 0 < L n) (W : ℕ → ℝ → ℝ) (hr : CopyControl s α (fun (n : ℕ) => (realData (t n) (source n)).linearData) g copy L W) (hi : CopyControl s α (fun (n : ℕ) => (imagData (t n) (source n)).linearData) g copy L W) (hb : LinearWaveBounds.InputBounds s (fun (n : ℕ) (p : P × TorusInverse.Plane) => W n ((g n).coordinates (copy n) p.2).2) α κ dirs (zeroAmplitudes base)) (hN : PhaseJetBounds.PolynomialJets (CurlClassBounds.phaseDomain s) fun (n : ℕ) (p : P × TorusInverse.Plane) => (t n).normal (nativePoint (g n) (copy n) p)) (hNdot : WeightedClasses.UnweightedClass s 0 fun (n : ℕ) (p : P × TorusInverse.Plane) => (t n).normalDot (nativePoint (g n) (copy n) p)) (hA : WeightedClasses.UnweightedClass s 0 fun (n : ℕ) (p : P × TorusInverse.Plane) => (t n).action (nativePoint (g n) (copy n) p)) (hf : WeightedClasses.WaveClass s (fun (n : ℕ) (p : P × TorusInverse.Plane) => W n ((g n).coordinates (copy n) p.2).2) α source) {b M : ℝ} (hpos : 0 < b) (hlower : ∀ (n : ℕ), ∀ p ∈ s.domain, b ≤ ‖(t n).normal (nativePoint (g n) (copy n) p)‖) (hupper : ∀ (n : ℕ), ∀ p ∈ s.domain, ‖(t n).normal (nativePoint (g n) (copy n) p)‖ ≤ M) (hfrequency : WeightedClasses.BandBound s (1 / 2) fun (n : ℕ) => 1 / base.frequency n) : LinearWaveBounds.InputBounds s (fun (n : ℕ) (p : P × TorusInverse.Plane) => W n ((g n).coordinates (copy n) p.2).2) α κ dirs (complexCopyCoefficients base t source g copy L hL)

Every amplitude and pressure hypothesis of the linear-wave estimate is obtained from the actual forced solves and their primitive input bounds.

theorem NavierStokes.ParticularWaveBounds.complexCopy_inputBounds_of_modal {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {s : WeightedClasses.StripData (P × TorusInverse.Plane)} {α κ : ℝ} {dirs : LinearWaveBounds.GraphDirections (P × TorusInverse.Plane)} (base : LinearWaveBounds.WaveCoefficients (P × TorusInverse.Plane)) (t : ℕ → CommonCoverSolve.TangentData P ProblemStatement.Space) (source : ℕ → P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : ℕ → CommonCoverSolve.Geometry) (copy : ℕ → TorusInverse.Frequency) (L : ℕ → ℝ) (hL : ∀ (n : ℕ), 0 < L n) (W : ℕ → ℝ → ℝ) (d : ℕ → PrimaryODE.FrameData (P × ℝ)) (harmonic : ℤ) (hr : ModalCopyControl s α d (fun (n : ℕ) => realData (t n) (source n)) harmonic g copy L W) (hi : ModalCopyControl s α d (fun (n : ℕ) => imagData (t n) (source n)) harmonic g copy L W) (hb : LinearWaveBounds.InputBounds s (fun (n : ℕ) (p : P × TorusInverse.Plane) => W n ((g n).coordinates (copy n) p.2).2) α κ dirs (zeroAmplitudes base)) (hN : PhaseJetBounds.PolynomialJets (CurlClassBounds.phaseDomain s) fun (n : ℕ) (p : P × TorusInverse.Plane) => (t n).normal (nativePoint (g n) (copy n) p)) (hNdot : WeightedClasses.UnweightedClass s 0 fun (n : ℕ) (p : P × TorusInverse.Plane) => (t n).normalDot (nativePoint (g n) (copy n) p)) (hA : WeightedClasses.UnweightedClass s 0 fun (n : ℕ) (p : P × TorusInverse.Plane) => (t n).action (nativePoint (g n) (copy n) p)) (hf : WeightedClasses.WaveClass s (fun (n : ℕ) (p : P × TorusInverse.Plane) => W n ((g n).coordinates (copy n) p.2).2) α source) {b M : ℝ} (hpos : 0 < b) (hlower : ∀ (n : ℕ), ∀ p ∈ s.domain, b ≤ ‖(t n).normal (nativePoint (g n) (copy n) p)‖) (hupper : ∀ (n : ℕ), ∀ p ∈ s.domain, ‖(t n).normal (nativePoint (g n) (copy n) p)‖ ≤ M) (hfrequency : WeightedClasses.BandBound s (1 / 2) fun (n : ℕ) => 1 / base.frequency n) : LinearWaveBounds.InputBounds s (fun (n : ℕ) (p : P × TorusInverse.Plane) => W n ((g n).coordinates (copy n) p.2).2) α κ dirs (complexCopyCoefficients base t source g copy L hL)

Every amplitude and pressure hypothesis of the linear-wave estimate is obtained from the actual forced solves and their primitive input bounds.

theorem NavierStokes.ParticularWaveBounds.complexCopyCoefficients_principal {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {s : WeightedClasses.StripData (P × TorusInverse.Plane)} {dirs : LinearWaveBounds.GraphDirections (P × TorusInverse.Plane)} (base : LinearWaveBounds.WaveCoefficients (P × TorusInverse.Plane)) (t : ℕ → CommonCoverSolve.TangentData P ProblemStatement.Space) (source : ℕ → P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : ℕ → CommonCoverSolve.Geometry) (copy : ℕ → TorusInverse.Frequency) (L : ℕ → ℝ) (hL : ∀ (n : ℕ), 0 < L n) {U : Set P} (hU : IsOpen U) (hdom : ∀ p ∈ s.domain, p.1 ∈ U) (hA : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (t n).linearData.coefficient (U ×ˢ Set.univ)) (hB : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (t n).linearData.forcingMap (U ×ˢ Set.univ)) (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (source n) (U ×ˢ Set.univ)) (hslot : ∀ (n : ℕ), ∀ p ∈ s.domain, ((g n).coordinates (copy n) p.2).2 ∈ Set.Ioo 0 (L n)) (hgeometry : CopyGeometryMatch s dirs base t g copy) (hfrequency : ∀ (n : ℕ), base.frequency n ≠ 0) (n : ℕ) (x : P × TorusInverse.Plane) : x ∈ s.domain → (complexCopyCoefficients base t source g copy L hL).principal s dirs n x = -source n x

The constructed complex coefficient satisfies the principal cancellation needed by the exact residual decomposition. No cancellation hypothesis is accepted as an input.

theorem NavierStokes.ParticularWaveBounds.complexCopyCoefficients_principal_of_modal {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {s : WeightedClasses.StripData (P × TorusInverse.Plane)} {α : ℝ} {dirs : LinearWaveBounds.GraphDirections (P × TorusInverse.Plane)} (base : LinearWaveBounds.WaveCoefficients (P × TorusInverse.Plane)) (t : ℕ → CommonCoverSolve.TangentData P ProblemStatement.Space) (source : ℕ → P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : ℕ → CommonCoverSolve.Geometry) (copy : ℕ → TorusInverse.Frequency) (L : ℕ → ℝ) (hL : ∀ (n : ℕ), 0 < L n) (W : ℕ → ℝ → ℝ) (d : ℕ → PrimaryODE.FrameData (P × ℝ)) (harmonic : ℤ) (hr : ModalCopyControl s α d (fun (n : ℕ) => realData (t n) (source n)) harmonic g copy L W) (hi : ModalCopyControl s α d (fun (n : ℕ) => imagData (t n) (source n)) harmonic g copy L W) (hgeometry : CopyGeometryMatch s dirs base t g copy) (hfrequency : ∀ (n : ℕ), base.frequency n ≠ 0) (n : ℕ) (x : P × TorusInverse.Plane) : x ∈ s.domain → (complexCopyCoefficients base t source g copy L hL).principal s dirs n x = -source n x

The principal equation for the actual modal construction. All required regularity is local to the finite integration interval.

theorem NavierStokes.ParticularWaveBounds.complexCopyCoefficients_tangent_of_modal {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {s : WeightedClasses.StripData (P × TorusInverse.Plane)} {α : ℝ} {dirs : LinearWaveBounds.GraphDirections (P × TorusInverse.Plane)} (base : LinearWaveBounds.WaveCoefficients (P × TorusInverse.Plane)) (t : ℕ → CommonCoverSolve.TangentData P ProblemStatement.Space) (source : ℕ → P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : ℕ → CommonCoverSolve.Geometry) (copy : ℕ → TorusInverse.Frequency) (L : ℕ → ℝ) (hL : ∀ (n : ℕ), 0 < L n) (W : ℕ → ℝ → ℝ) (d : ℕ → PrimaryODE.FrameData (P × ℝ)) (harmonic : ℤ) (hr : ModalCopyControl s α d (fun (n : ℕ) => realData (t n) (source n)) harmonic g copy L W) (hi : ModalCopyControl s α d (fun (n : ℕ) => imagData (t n) (source n)) harmonic g copy L W) (hgeometry : CopyGeometryMatch s dirs base t g copy) (n : ℕ) (x : P × TorusInverse.Plane) : x ∈ s.domain → HarmonicCalculus.normalDot (base.normal s dirs n x) ((complexCopyCoefficients base t source g copy L hL).amplitude n x) = 0

The complex tangent condition comes from the two reconstructed modal solutions, before applying any cutoff or exact curl.

theorem NavierStokes.ParticularWaveBounds.constructed_particular_wave {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {s : WeightedClasses.StripData (P × TorusInverse.Plane)} {α κ : ℝ} {dirs : LinearWaveBounds.GraphDirections (P × TorusInverse.Plane)} (base : LinearWaveBounds.WaveCoefficients (P × TorusInverse.Plane)) (t : ℕ → CommonCoverSolve.TangentData P ProblemStatement.Space) (source : ℕ → P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : ℕ → CommonCoverSolve.Geometry) (copy : ℕ → TorusInverse.Frequency) (L : ℕ → ℝ) (hL : ∀ (n : ℕ), 0 < L n) (W : ℕ → ℝ → ℝ) (hr : CopyControl s α (fun (n : ℕ) => (realData (t n) (source n)).linearData) g copy L W) (hi : CopyControl s α (fun (n : ℕ) => (imagData (t n) (source n)).linearData) g copy L W) (hb : LinearWaveBounds.InputBounds s (fun (n : ℕ) (p : P × TorusInverse.Plane) => W n ((g n).coordinates (copy n) p.2).2) α κ dirs (zeroAmplitudes base)) (hN : PhaseJetBounds.PolynomialJets (CurlClassBounds.phaseDomain s) fun (n : ℕ) (p : P × TorusInverse.Plane) => (t n).normal (nativePoint (g n) (copy n) p)) (hNdot : WeightedClasses.UnweightedClass s 0 fun (n : ℕ) (p : P × TorusInverse.Plane) => (t n).normalDot (nativePoint (g n) (copy n) p)) (hA : WeightedClasses.UnweightedClass s 0 fun (n : ℕ) (p : P × TorusInverse.Plane) => (t n).action (nativePoint (g n) (copy n) p)) (hf : WeightedClasses.WaveClass s (fun (n : ℕ) (p : P × TorusInverse.Plane) => W n ((g n).coordinates (copy n) p.2).2) α source) {b M : ℝ} (hpos : 0 < b) (hlower : ∀ (n : ℕ), ∀ p ∈ s.domain, b ≤ ‖(t n).normal (nativePoint (g n) (copy n) p)‖) (hupper : ∀ (n : ℕ), ∀ p ∈ s.domain, ‖(t n).normal (nativePoint (g n) (copy n) p)‖ ≤ M) (hfrequency : WeightedClasses.BandBound s (1 / 2) fun (n : ℕ) => 1 / base.frequency n) (hgeometry : CopyGeometryMatch s dirs base t g copy) (hfrequency_ne : ∀ (n : ℕ), base.frequency n ≠ 0) (hsource_smooth : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (source n) (hr.slowDomain ×ˢ Set.univ)) (hκ : κ ≤ 1 / 2) (ψ : ℕ → P × TorusInverse.Plane → ℝ) (hψ : WeightedClasses.UnweightedClass s 0 ψ) {R : P × TorusInverse.Plane → ℝ} (hR : base.radius = fun (x : ℕ) => R) (hg : LinearWaveBounds.ExactConditions s dirs ((complexCopyCoefficients base t source g copy L hL).corrected s dirs ψ)) : have a := complexCopyCoefficients base t source g copy L hL; have P_1 := fun (n : ℕ) (p : P × TorusInverse.Plane) => W n ((g n).coordinates (copy n) p.2).2; WeightedClasses.WaveClass s P_1 α a.amplitude ∧ WeightedClasses.WaveClass s P_1 α (a.corrected s dirs ψ).amplitude ∧ WeightedClasses.WaveClass s P_1 (α + 1 / 2) (a.corrected s dirs ψ).pressure ∧ WeightedClasses.WaveClass s P_1 (α + 1 / 2 - 3 * κ) (a.constructedGood s dirs ψ) ∧ ∀ (n : ℕ), ∀ x ∈ s.domain, ((a.corrected s dirs ψ).harmonicResidual s dirs n x + fun (i : Fin 3) => source n x i * HarmonicCalculus.carrier (a.frequency n) (a.phase n) x) = fun (i : Fin 3) => (a.constructedGood s dirs ψ n x i + LinearWaveBounds.excludedSlotError dirs ψ a.amplitude source n x i) * HarmonicCalculus.carrier (a.frequency n) (a.phase n) x

Complete class and actual residual statements for the constructed complex particular wave. Both Gaussian cutoff terms remain on the right-hand side.

theorem NavierStokes.ParticularWaveBounds.constructed_particular_wave_with_flat_error {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {s : WeightedClasses.StripData (P × TorusInverse.Plane)} {α κ : ℝ} {dirs : LinearWaveBounds.GraphDirections (P × TorusInverse.Plane)} (base : LinearWaveBounds.WaveCoefficients (P × TorusInverse.Plane)) (t : ℕ → CommonCoverSolve.TangentData P ProblemStatement.Space) (source : ℕ → P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : ℕ → CommonCoverSolve.Geometry) (copy : ℕ → TorusInverse.Frequency) (L : ℕ → ℝ) (hL : ∀ (n : ℕ), 0 < L n) (W : ℕ → ℝ → ℝ) (hr : CopyControl s α (fun (n : ℕ) => (realData (t n) (source n)).linearData) g copy L W) (hi : CopyControl s α (fun (n : ℕ) => (imagData (t n) (source n)).linearData) g copy L W) (hb : LinearWaveBounds.InputBounds s (fun (n : ℕ) (p : P × TorusInverse.Plane) => W n ((g n).coordinates (copy n) p.2).2) α κ dirs (zeroAmplitudes base)) (hN : PhaseJetBounds.PolynomialJets (CurlClassBounds.phaseDomain s) fun (n : ℕ) (p : P × TorusInverse.Plane) => (t n).normal (nativePoint (g n) (copy n) p)) (hNdot : WeightedClasses.UnweightedClass s 0 fun (n : ℕ) (p : P × TorusInverse.Plane) => (t n).normalDot (nativePoint (g n) (copy n) p)) (hA : WeightedClasses.UnweightedClass s 0 fun (n : ℕ) (p : P × TorusInverse.Plane) => (t n).action (nativePoint (g n) (copy n) p)) (hf : WeightedClasses.WaveClass s (fun (n : ℕ) (p : P × TorusInverse.Plane) => W n ((g n).coordinates (copy n) p.2).2) α source) {b M : ℝ} (hpos : 0 < b) (hlower : ∀ (n : ℕ), ∀ p ∈ s.domain, b ≤ ‖(t n).normal (nativePoint (g n) (copy n) p)‖) (hupper : ∀ (n : ℕ), ∀ p ∈ s.domain, ‖(t n).normal (nativePoint (g n) (copy n) p)‖ ≤ M) (hfrequency : WeightedClasses.BandBound s (1 / 2) fun (n : ℕ) => 1 / base.frequency n) (hgeometry : CopyGeometryMatch s dirs base t g copy) (hfrequency_ne : ∀ (n : ℕ), base.frequency n ≠ 0) (hsource_smooth : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (source n) (hr.slowDomain ×ˢ Set.univ)) (hκ : κ ≤ 1 / 2) (slot : GaussianTailFlat.SlotFamily s) (hfast : ∀ (n : ℕ), (slot.linear n) (dirs.fastScale n • dirs.fast) = (slot.length n)⁻¹) (edges : GaussianTailFlat.FlatEdges s) (scales : GaussianTailFlat.BandScaleControl s) {c : ℝ} (hc : 0 < c) (hW : ∀ (n : ℕ), ∀ x ∈ s.domain, W n ((g n).coordinates (copy n) x.2).2 ≤ Real.exp (-c * (slot.coordinate n x - 1 / 2) ^ 2 * slot.length n)) {R : P × TorusInverse.Plane → ℝ} (hR : base.radius = fun (x : ℕ) => R) (hg : LinearWaveBounds.ExactConditions s dirs ((complexCopyCoefficients base t source g copy L hL).corrected s dirs slot.cutoff)) : have a := complexCopyCoefficients base t source g copy L hL; have P_1 := fun (n : ℕ) (p : P × TorusInverse.Plane) => W n ((g n).coordinates (copy n) p.2).2; WeightedClasses.WaveClass s P_1 (α + 1 / 2 - 3 * κ) (a.constructedGood s dirs slot.cutoff) ∧ (∀ (β : ℝ), WeightedClasses.UnweightedClass s β (LinearWaveBounds.excludedSlotError dirs slot.cutoff a.amplitude source)) ∧ ∀ (n : ℕ), ∀ x ∈ s.domain, ((a.corrected s dirs slot.cutoff).harmonicResidual s dirs n x + fun (i : Fin 3) => source n x i * HarmonicCalculus.carrier (a.frequency n) (a.phase n) x) = fun (i : Fin 3) => (a.constructedGood s dirs slot.cutoff n x i + LinearWaveBounds.excludedSlotError dirs slot.cutoff a.amplitude source n x i) * HarmonicCalculus.carrier (a.frequency n) (a.phase n) x

The cutoff remainder is both retained in the exact equation and proved smaller than every prescribed epsilon power under the Gaussian envelope.

theorem NavierStokes.ParticularWaveBounds.constructed_modal_particular_wave {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {s : WeightedClasses.StripData (P × TorusInverse.Plane)} {α κ : ℝ} {dirs : LinearWaveBounds.GraphDirections (P × TorusInverse.Plane)} (base : LinearWaveBounds.WaveCoefficients (P × TorusInverse.Plane)) (t : ℕ → CommonCoverSolve.TangentData P ProblemStatement.Space) (source : ℕ → P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : ℕ → CommonCoverSolve.Geometry) (copy : ℕ → TorusInverse.Frequency) (L : ℕ → ℝ) (hL : ∀ (n : ℕ), 0 < L n) (W : ℕ → ℝ → ℝ) (d : ℕ → PrimaryODE.FrameData (P × ℝ)) (harmonic : ℤ) (hr : ModalCopyControl s α d (fun (n : ℕ) => realData (t n) (source n)) harmonic g copy L W) (hi : ModalCopyControl s α d (fun (n : ℕ) => imagData (t n) (source n)) harmonic g copy L W) (hb : LinearWaveBounds.InputBounds s (fun (n : ℕ) (p : P × TorusInverse.Plane) => W n ((g n).coordinates (copy n) p.2).2) α κ dirs (zeroAmplitudes base)) (hN : PhaseJetBounds.PolynomialJets (CurlClassBounds.phaseDomain s) fun (n : ℕ) (p : P × TorusInverse.Plane) => (t n).normal (nativePoint (g n) (copy n) p)) (hNdot : WeightedClasses.UnweightedClass s 0 fun (n : ℕ) (p : P × TorusInverse.Plane) => (t n).normalDot (nativePoint (g n) (copy n) p)) (hA : WeightedClasses.UnweightedClass s 0 fun (n : ℕ) (p : P × TorusInverse.Plane) => (t n).action (nativePoint (g n) (copy n) p)) (hf : WeightedClasses.WaveClass s (fun (n : ℕ) (p : P × TorusInverse.Plane) => W n ((g n).coordinates (copy n) p.2).2) α source) {b M : ℝ} (hpos : 0 < b) (hlower : ∀ (n : ℕ), ∀ p ∈ s.domain, b ≤ ‖(t n).normal (nativePoint (g n) (copy n) p)‖) (hupper : ∀ (n : ℕ), ∀ p ∈ s.domain, ‖(t n).normal (nativePoint (g n) (copy n) p)‖ ≤ M) (hfrequency : WeightedClasses.BandBound s (1 / 2) fun (n : ℕ) => 1 / base.frequency n) (hgeometry : CopyGeometryMatch s dirs base t g copy) (hfrequency_ne : ∀ (n : ℕ), base.frequency n ≠ 0) (hκ : κ ≤ 1 / 2) (ψ : ℕ → P × TorusInverse.Plane → ℝ) (hψ : WeightedClasses.UnweightedClass s 0 ψ) {R : P × TorusInverse.Plane → ℝ} (hR : base.radius = fun (x : ℕ) => R) (hg : LinearWaveBounds.ExactConditions s dirs ((complexCopyCoefficients base t source g copy L hL).corrected s dirs ψ)) : have a := complexCopyCoefficients base t source g copy L hL; have P_1 := fun (n : ℕ) (p : P × TorusInverse.Plane) => W n ((g n).coordinates (copy n) p.2).2; WeightedClasses.WaveClass s P_1 α a.amplitude ∧ WeightedClasses.WaveClass s P_1 α (a.corrected s dirs ψ).amplitude ∧ WeightedClasses.WaveClass s P_1 (α + 1 / 2) (a.corrected s dirs ψ).pressure ∧ WeightedClasses.WaveClass s P_1 (α + 1 / 2 - 3 * κ) (a.constructedGood s dirs ψ) ∧ ∀ (n : ℕ), ∀ x ∈ s.domain, ((a.corrected s dirs ψ).harmonicResidual s dirs n x + fun (i : Fin 3) => source n x i * HarmonicCalculus.carrier (a.frequency n) (a.phase n) x) = fun (i : Fin 3) => (a.constructedGood s dirs ψ n x i + LinearWaveBounds.excludedSlotError dirs ψ a.amplitude source n x i) * HarmonicCalculus.carrier (a.frequency n) (a.phase n) x

Complete class and actual residual statements for the constructed complex particular wave. Both Gaussian cutoff terms remain on the right-hand side.

theorem NavierStokes.ParticularWaveBounds.constructed_modal_particular_wave_with_flat_error {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {s : WeightedClasses.StripData (P × TorusInverse.Plane)} {α κ : ℝ} {dirs : LinearWaveBounds.GraphDirections (P × TorusInverse.Plane)} (base : LinearWaveBounds.WaveCoefficients (P × TorusInverse.Plane)) (t : ℕ → CommonCoverSolve.TangentData P ProblemStatement.Space) (source : ℕ → P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : ℕ → CommonCoverSolve.Geometry) (copy : ℕ → TorusInverse.Frequency) (L : ℕ → ℝ) (hL : ∀ (n : ℕ), 0 < L n) (W : ℕ → ℝ → ℝ) (d : ℕ → PrimaryODE.FrameData (P × ℝ)) (harmonic : ℤ) (hr : ModalCopyControl s α d (fun (n : ℕ) => realData (t n) (source n)) harmonic g copy L W) (hi : ModalCopyControl s α d (fun (n : ℕ) => imagData (t n) (source n)) harmonic g copy L W) (hb : LinearWaveBounds.InputBounds s (fun (n : ℕ) (p : P × TorusInverse.Plane) => W n ((g n).coordinates (copy n) p.2).2) α κ dirs (zeroAmplitudes base)) (hN : PhaseJetBounds.PolynomialJets (CurlClassBounds.phaseDomain s) fun (n : ℕ) (p : P × TorusInverse.Plane) => (t n).normal (nativePoint (g n) (copy n) p)) (hNdot : WeightedClasses.UnweightedClass s 0 fun (n : ℕ) (p : P × TorusInverse.Plane) => (t n).normalDot (nativePoint (g n) (copy n) p)) (hA : WeightedClasses.UnweightedClass s 0 fun (n : ℕ) (p : P × TorusInverse.Plane) => (t n).action (nativePoint (g n) (copy n) p)) (hf : WeightedClasses.WaveClass s (fun (n : ℕ) (p : P × TorusInverse.Plane) => W n ((g n).coordinates (copy n) p.2).2) α source) {b M : ℝ} (hpos : 0 < b) (hlower : ∀ (n : ℕ), ∀ p ∈ s.domain, b ≤ ‖(t n).normal (nativePoint (g n) (copy n) p)‖) (hupper : ∀ (n : ℕ), ∀ p ∈ s.domain, ‖(t n).normal (nativePoint (g n) (copy n) p)‖ ≤ M) (hfrequency : WeightedClasses.BandBound s (1 / 2) fun (n : ℕ) => 1 / base.frequency n) (hgeometry : CopyGeometryMatch s dirs base t g copy) (hfrequency_ne : ∀ (n : ℕ), base.frequency n ≠ 0) (hκ : κ ≤ 1 / 2) (slot : GaussianTailFlat.SlotFamily s) (hfast : ∀ (n : ℕ), (slot.linear n) (dirs.fastScale n • dirs.fast) = (slot.length n)⁻¹) (edges : GaussianTailFlat.FlatEdges s) (scales : GaussianTailFlat.BandScaleControl s) {c : ℝ} (hc : 0 < c) (hW : ∀ (n : ℕ), ∀ x ∈ s.domain, W n ((g n).coordinates (copy n) x.2).2 ≤ Real.exp (-c * (slot.coordinate n x - 1 / 2) ^ 2 * slot.length n)) {R : P × TorusInverse.Plane → ℝ} (hR : base.radius = fun (x : ℕ) => R) (hg : LinearWaveBounds.ExactConditions s dirs ((complexCopyCoefficients base t source g copy L hL).corrected s dirs slot.cutoff)) : have a := complexCopyCoefficients base t source g copy L hL; have P_1 := fun (n : ℕ) (p : P × TorusInverse.Plane) => W n ((g n).coordinates (copy n) p.2).2; WeightedClasses.WaveClass s P_1 (α + 1 / 2 - 3 * κ) (a.constructedGood s dirs slot.cutoff) ∧ (∀ (β : ℝ), WeightedClasses.UnweightedClass s β (LinearWaveBounds.excludedSlotError dirs slot.cutoff a.amplitude source)) ∧ ∀ (n : ℕ), ∀ x ∈ s.domain, ((a.corrected s dirs slot.cutoff).harmonicResidual s dirs n x + fun (i : Fin 3) => source n x i * HarmonicCalculus.carrier (a.frequency n) (a.phase n) x) = fun (i : Fin 3) => (a.constructedGood s dirs slot.cutoff n x i + LinearWaveBounds.excludedSlotError dirs slot.cutoff a.amplitude source n x i) * HarmonicCalculus.carrier (a.frequency n) (a.phase n) x

The cutoff remainder is both retained in the exact equation and proved smaller than every prescribed epsilon power under the Gaussian envelope.

theorem NavierStokes.ParticularWaveBounds.complexCopyCoefficients_invariant {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (base : LinearWaveBounds.WaveCoefficients (P × TorusInverse.Plane)) (t : ℕ → CommonCoverSolve.TangentData P ProblemStatement.Space) (source : ℕ → P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : ℕ → CommonCoverSolve.Geometry) (copy : ℕ → TorusInverse.Frequency) (L : ℕ → ℝ) (hL : ∀ (n : ℕ), 0 < L n) (θ : P) (hr : ∀ (n : ℕ), CopyAngularInvariance.TangentInvariant θ (realData (t n) (source n))) (hi : ∀ (n : ℕ), CopyAngularInvariance.TangentInvariant θ (imagData (t n) (source n))) (n : ℕ) : CopyAngularInvariance.Invariant (θ, 0) ((complexCopyCoefficients base t source g copy L hL).amplitude n) ∧ CopyAngularInvariance.Invariant (θ, 0) ((complexCopyCoefficients base t source g copy L hL).pressure n)

Primitive angular invariance of the real geometry and source is preserved by both actual complex outputs. The carrier remains equivariant.

theorem NavierStokes.ParticularWaveBounds.modal_corrected_is_curl_and_divergence_zero {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {s : WeightedClasses.StripData (P × TorusInverse.Plane)} {α : ℝ} {dirs : LinearWaveBounds.GraphDirections (P × TorusInverse.Plane)} (base : LinearWaveBounds.WaveCoefficients (P × TorusInverse.Plane)) (t : ℕ → CommonCoverSolve.TangentData P ProblemStatement.Space) (source : ℕ → P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : ℕ → CommonCoverSolve.Geometry) (copy : ℕ → TorusInverse.Frequency) (L : ℕ → ℝ) (hL : ∀ (n : ℕ), 0 < L n) (W : ℕ → ℝ → ℝ) (d : ℕ → PrimaryODE.FrameData (P × ℝ)) (harmonic : ℤ) (hr : ModalCopyControl s α d (fun (n : ℕ) => realData (t n) (source n)) harmonic g copy L W) (hi : ModalCopyControl s α d (fun (n : ℕ) => imagData (t n) (source n)) harmonic g copy L W) (hgeometry : CopyGeometryMatch s dirs base t g copy) (ψ : ℕ → P × TorusInverse.Plane → ℝ) (n : ℕ) (hψ : ContDiffOn ℝ (↑⊤) (ψ n) s.domain) (G : CurlClassBounds.CylindricalGeometry s.domain (base.radius n) (dirs.radialField n) (fun (x : P × TorusInverse.Plane) => dirs.angular) (dirs.axialField s n)) (hK : base.frequency n ≠ 0) (hΦ : ContDiffOn ℝ (↑⊤) (base.phase n) s.domain) (hn : ∀ x ∈ s.domain, base.normal s dirs n x ≠ 0) {x : P × TorusInverse.Plane} (hx : x ∈ s.domain) : have a := complexCopyCoefficients base t source g copy L hL; CurlClassBounds.cylindricalCurl (base.radius n) (dirs.radialField n) (fun (x : P × TorusInverse.Plane) => dirs.angular) (dirs.axialField s n) ((a.withCutoff ψ).curlPotential s dirs n) x = HarmonicCalculus.vectorMode (base.frequency n) (base.phase n) ((a.corrected s dirs ψ).amplitude n) x ∧ HarmonicCalculus.cylindricalDivergence (base.radius n) (dirs.radialField n) (fun (x : P × TorusInverse.Plane) => dirs.angular) (dirs.axialField s n) (HarmonicCalculus.vectorMode (base.frequency n) (base.phase n) ((a.corrected s dirs ψ).amplitude n)) x = 0

The modal construction really realizes the corrected field as a curl, and its actual harmonic divergence vanishes. No output tangency or smoothness hypothesis is used.

theorem NavierStokes.ParticularWaveBounds.correctedCurl_tsupport_subset {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (dirs : LinearWaveBounds.GraphDirections D) (a : LinearWaveBounds.WaveCoefficients D) (ψ : ℕ → D → ℝ) (n : ℕ) : tsupport (CurlClassBounds.cylindricalCurl (a.radius n) (dirs.radialField n) (fun (x : D) => dirs.angular) (dirs.axialField s n) ((a.withCutoff ψ).curlPotential s dirs n)) ⊆ tsupport (ψ n) ∩ tsupport (a.amplitude n)

Localization is retained after taking the actual curl, including on the cutoff boundary.

noncomputable def NavierStokes.ParticularWaveBounds.scaleTangentSource {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (c : ℝ) : CommonCoverSolve.TangentData P ProblemStatement.Space

Scale tangent source, given by { t with source := fun p => c • t.source p }.

Equations

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

theorem NavierStokes.ParticularWaveBounds.copyVelocity_scaleSource {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (c : ℝ) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (k : TorusInverse.Frequency) (p : P × TorusInverse.Plane) : copyVelocity (scaleTangentSource t c) g hab k p = c • copyVelocity t g hab k p

theorem NavierStokes.ParticularWaveBounds.copyPressureReal_scaleSource {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (c : ℝ) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (k : TorusInverse.Frequency) (p : P × TorusInverse.Plane) : copyPressureReal (scaleTangentSource t c) g hab k p = c * copyPressureReal t g hab k p

theorem NavierStokes.ParticularWaveBounds.copyPressure_scaleSource {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (c : ℝ) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (k : TorusInverse.Frequency) (frequency : ℝ) (p : P × TorusInverse.Plane) : copyPressure (scaleTangentSource t c) g hab k frequency p = c • copyPressure t g hab k frequency p

noncomputable def NavierStokes.ParticularWaveBounds.conjugateSource {P : Type} (f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector

Conjugate source, defined pointwise by star (f p i).

Equations

• NavierStokes.ParticularWaveBounds.conjugateSource f p i = star (f p i)

theorem NavierStokes.ParticularWaveBounds.realData_conjugate {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) : realData t (conjugateSource f) = realData t f

theorem NavierStokes.ParticularWaveBounds.imagData_conjugate {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) : imagData t (conjugateSource f) = scaleTangentSource (imagData t f) (-1)

theorem NavierStokes.ParticularWaveBounds.complexCopyVelocity_conjugate {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (k : TorusInverse.Frequency) (p : P × TorusInverse.Plane) : complexCopyVelocity t (conjugateSource f) g hab k p = fun (i : Fin 3) => star (complexCopyVelocity t f g hab k p i)

Conjugation of a source conjugates the actual zero-entry velocity.

theorem NavierStokes.ParticularWaveBounds.complexCopyPressure_conjugate {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (k : TorusInverse.Frequency) (frequency : ℝ) (p : P × TorusInverse.Plane) : complexCopyPressure t (conjugateSource f) g hab k (-frequency) p = star (complexCopyPressure t f g hab k frequency p)

The sign change of the harmonic frequency is essential to pressure conjugation. This proves the symmetry required for a real paired wave.

theorem NavierStokes.ParticularWaveBounds.complexCopyVelocity_at_entry {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (k : TorusInverse.Frequency) (p : P) (ξ : ℝ) : complexCopyVelocity t f g hab k (p, g.point k (ξ, a)) = 0

theorem NavierStokes.ParticularWaveBounds.complexCopyVelocity_zero_of_path {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (k : TorusInverse.Frequency) (p : P) (Y : TorusInverse.Plane) (hf : ∀ v ∈ Set.Icc a b, f (p, g.path k Y v) = 0) : complexCopyVelocity t f g hab k (p, Y) = 0

Support is propagated along the actual earlier-point path. Pointwise vanishing of the source at only the current point is not used.

theorem NavierStokes.ParticularWaveBounds.copyPressure_zero_of_path {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (k : TorusInverse.Frequency) (frequency : ℝ) (p : P) (Y : TorusInverse.Plane) (hf : ∀ v ∈ Set.Icc a b, t.source (p, g.path k Y v) = 0) (hcurrent : t.source (p, Y) = 0) : copyPressure t g hab k frequency (p, Y) = 0

theorem NavierStokes.ParticularWaveBounds.complexCopyPressure_zero_of_path {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (k : TorusInverse.Frequency) (frequency : ℝ) (p : P) (Y : TorusInverse.Plane) (hf : ∀ v ∈ Set.Icc a b, f (p, g.path k Y v) = 0) (heta : (g.coordinates k Y).2 ∈ Set.Icc a b) : complexCopyPressure t f g hab k frequency (p, Y) = 0

theorem NavierStokes.ParticularWaveBounds.copyVelocity_deck {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (k m : TorusInverse.Frequency) (p : P) (hp : CommonCoverSolve.PeriodicAt t.source p) (Y : TorusInverse.Plane) : copyVelocity t g hab (k + CommonCoverSolve.coverIndex g.gap m) (p, Y + TorusAverages.latticePoint m) = copyVelocity t g hab k (p, Y)

theorem NavierStokes.ParticularWaveBounds.copyPressure_deck {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (k m : TorusInverse.Frequency) (frequency : ℝ) (p : P) (hp : CommonCoverSolve.PeriodicAt t.source p) (Y : TorusInverse.Plane) : copyPressure t g hab (k + CommonCoverSolve.coverIndex g.gap m) frequency (p, Y + TorusAverages.latticePoint m) = copyPressure t g hab k frequency (p, Y)

theorem NavierStokes.ParticularWaveBounds.complexCopyVelocity_deck {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (k m : TorusInverse.Frequency) (p : P) (hp : CommonCoverSolve.PeriodicAt f p) (Y : TorusInverse.Plane) : complexCopyVelocity t f g hab (k + CommonCoverSolve.coverIndex g.gap m) (p, Y + TorusAverages.latticePoint m) = complexCopyVelocity t f g hab k (p, Y)

theorem NavierStokes.ParticularWaveBounds.complexCopyPressure_deck {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (k m : TorusInverse.Frequency) (frequency : ℝ) (p : P) (hp : CommonCoverSolve.PeriodicAt f p) (Y : TorusInverse.Plane) : complexCopyPressure t f g hab (k + CommonCoverSolve.coverIndex g.gap m) frequency (p, Y + TorusAverages.latticePoint m) = complexCopyPressure t f g hab k frequency (p, Y)

noncomputable def NavierStokes.ParticularWaveBounds.periodizedCopies {P H : Type} [NormedAddCommGroup H] [NormedSpace ℝ H] (g : CommonCoverSolve.Geometry) (κ : TorusInverse.Plane → ℝ) (F : TorusInverse.Frequency → P × TorusInverse.Plane → H) (p : P × TorusInverse.Plane) : H

Periodized copies, given by ∑' k : Frequency, κ (g.coordinates k p.2) • F k p.

Equations

• NavierStokes.ParticularWaveBounds.periodizedCopies g κ F p = ∑' (k : NavierStokes.TorusInverse.Frequency), κ (g.coordinates k p.2) • F k p

theorem NavierStokes.ParticularWaveBounds.periodizedCopies_eq_finite_sum {P H : Type} [NormedAddCommGroup H] [NormedSpace ℝ H] (g : CommonCoverSolve.Geometry) {κ : TorusInverse.Plane → ℝ} (hκ : HasCompactSupport κ) (F : TorusInverse.Frequency → P × TorusInverse.Plane → H) (p : P × TorusInverse.Plane) : ∃ (I : Finset TorusInverse.Frequency), periodizedCopies g κ F p = ∑ k ∈ I, κ (g.coordinates k p.2) • F k p

Compact localization makes the displayed series an actual finite sum at each point; no summability fallback is used by the construction.

theorem NavierStokes.ParticularWaveBounds.periodizedCopies_eq_single {P H : Type} [NormedAddCommGroup H] [NormedSpace ℝ H] (g : CommonCoverSolve.Geometry) (κ : TorusInverse.Plane → ℝ) (F : TorusInverse.Frequency → P × TorusInverse.Plane → H) (k : TorusInverse.Frequency) (p : P × TorusInverse.Plane) (hk : κ (g.coordinates k p.2) = 1) (hother : ∀ (l : TorusInverse.Frequency), l ≠ k → κ (g.coordinates l p.2) = 0) : periodizedCopies g κ F p = F k p

On a plateau occupied by exactly one copy, periodization gives that actual copy. No summability convention enters this equality.

theorem NavierStokes.ParticularWaveBounds.periodizedCopies_eventuallyEq_single {P : Type} [NormedAddCommGroup P] {H : Type} [NormedAddCommGroup H] [NormedSpace ℝ H] (g : CommonCoverSolve.Geometry) (κ : TorusInverse.Plane → ℝ) (F : TorusInverse.Frequency → P × TorusInverse.Plane → H) (k : TorusInverse.Frequency) (p : P × TorusInverse.Plane) (hκ : ∀ᶠ (y : P × TorusInverse.Plane) in nhds p, κ (g.coordinates k y.2) = 1 ∧ ∀ (l : TorusInverse.Frequency), l ≠ k → κ (g.coordinates l y.2) = 0) : periodizedCopies g κ F =ᶠ[nhds p] F k

theorem NavierStokes.ParticularWaveBounds.periodizedCopies_iteratedFDeriv_eq_single {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {H : Type} [NormedAddCommGroup H] [NormedSpace ℝ H] (g : CommonCoverSolve.Geometry) (κ : TorusInverse.Plane → ℝ) (F : TorusInverse.Frequency → P × TorusInverse.Plane → H) (k : TorusInverse.Frequency) (p : P × TorusInverse.Plane) (hκ : ∀ᶠ (y : P × TorusInverse.Plane) in nhds p, κ (g.coordinates k y.2) = 1 ∧ ∀ (l : TorusInverse.Frequency), l ≠ k → κ (g.coordinates l y.2) = 0) (m : ℕ) : iteratedFDeriv ℝ m (periodizedCopies g κ F) p = iteratedFDeriv ℝ m (F k) p

Germ agreement preserves every actual Fréchet derivative, including mixed derivatives in the slow and torus variables.

theorem NavierStokes.ParticularWaveBounds.periodizedCopies_periodic {P H : Type} [NormedAddCommGroup H] [NormedSpace ℝ H] (g : CommonCoverSolve.Geometry) (κ : TorusInverse.Plane → ℝ) (F : TorusInverse.Frequency → P × TorusInverse.Plane → H) (p : P) (hF : ∀ (k m : TorusInverse.Frequency) (Y : TorusInverse.Plane), F (k + CommonCoverSolve.coverIndex g.gap m) (p, Y + TorusAverages.latticePoint m) = F k (p, Y)) : CommonCoverSolve.PeriodicAt (periodizedCopies g κ F) p

noncomputable def NavierStokes.ParticularWaveBounds.commonVelocity {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (κ : TorusInverse.Plane → ℝ) : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector

Common velocity, given by periodizedCopies g κ (fun k => complexCopyVelocity t f g hab k).

Equations

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

noncomputable def NavierStokes.ParticularWaveBounds.commonPressure {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (κ : TorusInverse.Plane → ℝ) (frequency : ℝ) : P × TorusInverse.Plane → ℂ

Common pressure, given by periodizedCopies g κ (fun k => complexCopyPressure t f g hab k frequency).

Equations

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

theorem NavierStokes.ParticularWaveBounds.commonVelocity_periodic {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (κ : TorusInverse.Plane → ℝ) (p : P) (hp : CommonCoverSolve.PeriodicAt f p) : CommonCoverSolve.PeriodicAt (commonVelocity t f g hab κ) p

theorem NavierStokes.ParticularWaveBounds.commonPressure_periodic {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (κ : TorusInverse.Plane → ℝ) (frequency : ℝ) (p : P) (hp : CommonCoverSolve.PeriodicAt f p) : CommonCoverSolve.PeriodicAt (commonPressure t f g hab κ frequency) p

noncomputable def NavierStokes.ParticularWaveBounds.reindexStrip {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (e : E ≃ₗᵢ[ℝ] F) (s : WeightedClasses.StripData F) : WeightedClasses.StripData E

Reindex strip, bundling domain, isOpen_domain, epsilon, epsilon_pos and the required compatibility proofs.

Equations

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

theorem NavierStokes.ParticularWaveBounds.memClass_reindex {E : Type u_1} {F : Type u_2} {H : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup H] [NormedSpace ℝ H] (e : E ≃ₗᵢ[ℝ] F) {s : WeightedClasses.StripData F} {w : ℕ → F → ℝ} {α : ℝ} {f : ℕ → F → H} (hf : WeightedClasses.MemClass s w α f) : WeightedClasses.MemClass (reindexStrip e s) (fun (n : ℕ) (x : E) => w n (e x)) α fun (n : ℕ) (x : E) => f n (e x)

Reassociation of coordinates preserves every actual derivative norm.

theorem NavierStokes.ParticularWaveBounds.waveClass_reindex {E : Type u_1} {F : Type u_2} {H : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup H] [NormedSpace ℝ H] (e : E ≃ₗᵢ[ℝ] F) {s : WeightedClasses.StripData F} {W : ℕ → F → ℝ} {α : ℝ} {f : ℕ → F → H} (hf : WeightedClasses.WaveClass s W α f) : WeightedClasses.WaveClass (reindexStrip e s) (fun (n : ℕ) (x : E) => W n (e x)) α fun (n : ℕ) (x : E) => f n (e x)

noncomputable def NavierStokes.ParticularWaveBounds.reindexVector {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (e : E ≃ₗᵢ[ℝ] F) (V : F → F) : E → E

Reindex vector, defined pointwise by e.symm (V (e x)).

Equations

• NavierStokes.ParticularWaveBounds.reindexVector e V x = e.symm (V (e x))

theorem NavierStokes.ParticularWaveBounds.along_reindex {E : Type u_1} {F : Type u_2} {H : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup H] [NormedSpace ℝ H] (e : E ≃ₗᵢ[ℝ] F) (V : F → F) {f : F → H} {x : E} (hf : DifferentiableAt ℝ f (e x)) : HarmonicCalculus.along (reindexVector e V) (fun (y : E) => f (e y)) x = HarmonicCalculus.along V f (e x)

theorem NavierStokes.ParticularWaveBounds.phaseNormal_reindex {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (e : E ≃ₗᵢ[ℝ] F) (R : F → ℝ) (Vr Vθ Vz : F → F) {Φ : F → ℝ} {x : E} (hΦ : DifferentiableAt ℝ Φ (e x)) : HarmonicCalculus.phaseNormal (fun (y : E) => R (e y)) (reindexVector e Vr) (reindexVector e Vθ) (reindexVector e Vz) (fun (y : E) => Φ (e y)) x = HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ (e x)

theorem NavierStokes.ParticularWaveBounds.principal_reindex {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (e : E ≃ₗᵢ[ℝ] F) (ε frequency : ℝ) (R F₀ G Φ : F → ℝ) (Vr Vθ Vz Vf : F → F) (a : F → HarmonicCalculus.ComplexVector) (p : F → ℂ) {x : E} (hF : DifferentiableAt ℝ F₀ (e x)) (hG : DifferentiableAt ℝ G (e x)) (hΦ : DifferentiableAt ℝ Φ (e x)) (ha : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : F) => a y i) (e x)) : LinearWaveResidual.principal ε frequency (fun (y : E) => R (e y)) (fun (y : E) => F₀ (e y)) (fun (y : E) => G (e y)) (reindexVector e Vr) (reindexVector e Vθ) (reindexVector e Vz) (reindexVector e Vf) (fun (y : E) => Φ (e y)) (fun (y : E) => a (e y)) (fun (y : E) => p (e y)) x = LinearWaveResidual.principal ε frequency R F₀ G Vr Vθ Vz Vf Φ a p (e x)

noncomputable def NavierStokes.ParticularWaveBounds.reindexCoefficients {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (e : E ≃ₗᵢ[ℝ] F) (a : LinearWaveBounds.WaveCoefficients F) : LinearWaveBounds.WaveCoefficients E

Reindex coefficients, bundling radius, radialBase, frequencyBase, axialBase and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.ParticularWaveBounds.reindexDirections {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (e : E ≃ₗᵢ[ℝ] F) (d : LinearWaveBounds.GraphDirections F) : LinearWaveBounds.GraphDirections E

Reindex directions, bundling radial, auxiliary, axial, angular and the required compatibility proofs.

Equations

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

theorem NavierStokes.ParticularWaveBounds.reindex_radialField {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (e : E ≃ₗᵢ[ℝ] F) (d : LinearWaveBounds.GraphDirections F) (n : ℕ) : (reindexDirections e d).radialField n = reindexVector e (d.radialField n)

theorem NavierStokes.ParticularWaveBounds.reindex_axialField {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (e : E ≃ₗᵢ[ℝ] F) (d : LinearWaveBounds.GraphDirections F) (s : WeightedClasses.StripData F) (n : ℕ) : (reindexDirections e d).axialField (reindexStrip e s) n = reindexVector e (d.axialField s n)

theorem NavierStokes.ParticularWaveBounds.reindex_fastField {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (e : E ≃ₗᵢ[ℝ] F) (d : LinearWaveBounds.GraphDirections F) (n : ℕ) : (reindexDirections e d).fastField n = reindexVector e (d.fastField n)

noncomputable def NavierStokes.ParticularWaveBounds.liftAssoc (S : Type u_4) [NormedAddCommGroup S] [NormedSpace ℝ S] : ℝ × S × TorusInverse.Plane ≃ₗᵢ[ℝ] (ℝ × S) × TorusInverse.Plane

Explicit associator from PressureStream.Lift S to the common-copy domain with slow parameter P = ℝ × S.

Equations

• NavierStokes.ParticularWaveBounds.liftAssoc S = (LinearIsometryEquiv.prodAssoc ℝ ℝ S NavierStokes.TorusInverse.Plane).symm

@[simp]

theorem NavierStokes.ParticularWaveBounds.liftAssoc_apply (S : Type u_4) [NormedAddCommGroup S] [NormedSpace ℝ S] (x : ℝ × S × TorusInverse.Plane) : (liftAssoc S) x = ((x.1, x.2.1), x.2.2)