Constructed primary pulse solutions

The operator and forcing are defined from the actual moving tangent frame. The solution is the finite-interval Volterra solution, with its differentiable extension. Reconstruction into ambient coordinates satisfies the projected equation exactly. Estimates are derived for this constructed solution.

@[reducible, inline]

abbrev NavierStokes.PrimaryODE.State : Type

State: an abbreviation for MovingFrameODE.Plane.

Equations

• NavierStokes.PrimaryODE.State = NavierStokes.MovingFrameODE.Plane

@[reducible, inline]

abbrev NavierStokes.PrimaryODE.Space : Type

Space: an abbreviation for MovingFrameODE.Space.

Equations

• NavierStokes.PrimaryODE.Space = NavierStokes.MovingFrameODE.Space

@[reducible, inline]

abbrev NavierStokes.PrimaryODE.Frame : Type

Frame: an abbreviation for MovingFrameODE.Frame.

Equations

• NavierStokes.PrimaryODE.Frame = NavierStokes.MovingFrameODE.Frame

structure NavierStokes.PrimaryODE.FrameData (Q : Type) : Type

Smooth input quantities before any solution is constructed. eigenvector is the scalar h in x=p+q, y=h(p-q); its logarithmic derivative is eigenRate. viscosity is the fundamental scalar damping.

• beta : Q × ℝ → ℝ

  Beta of FrameData, of type Q × ℝ → ℝ.

• betaDot : Q × ℝ → ℝ

  Beta dot of FrameData, of type Q × ℝ → ℝ.

• rho : Q × ℝ → ℝ

  Rho of FrameData, of type Q × ℝ → ℝ.

• rhoDot : Q × ℝ → ℝ

  Rho dot of FrameData, of type Q × ℝ → ℝ.

• rotation : Q × ℝ → ℝ

  Rotation of FrameData, of type Q × ℝ → ℝ.

• F : Q × ℝ → ℝ

  F of FrameData, of type Q × ℝ → ℝ.

• shear : Q × ℝ → State

  Shear of FrameData, of type Q × ℝ → State.

• frame : Q × ℝ → Frame

  Frame of FrameData, of type Q × ℝ → Frame.

• eigenvalue : Q × ℝ → ℝ

  Eigenvalue of FrameData, of type Q × ℝ → ℝ.

• eigenvector : Q × ℝ → ℝ

  Eigenvector of FrameData, of type Q × ℝ → ℝ.

• eigenRate : Q × ℝ → ℝ

  Eigen rate of FrameData, of type Q × ℝ → ℝ.

• viscosity : Q × ℝ → ℝ

  Viscosity of FrameData, of type Q × ℝ → ℝ.

noncomputable def NavierStokes.PrimaryODE.FrameData.errorA {Q : Type} (d : FrameData Q) (z : Q × ℝ) : ℝ

Error A, given by MovingFrameODE.coeff11 (d.rho z) (d.rhoDot z) ⟪d.frame z 0, d.shear z⟫_ℝ.

Equations

• d.errorA z = NavierStokes.MovingFrameODE.coeff11 (d.rho z) (d.rhoDot z) (inner ℝ ((d.frame z) 0) (d.shear z))

noncomputable def NavierStokes.PrimaryODE.FrameData.errorB {Q : Type} (d : FrameData Q) (z : Q × ℝ) : ℝ

Error B, given by MovingFrameODE.coeff12 (d.F z) (d.frame z 1 0) (d.rho z) (d.rotation z) - d.eigenvalue z / d.eigenvector z.

Equations

• d.errorB z = NavierStokes.MovingFrameODE.coeff12 (d.F z) (((d.frame z) 1).ofLp 0) (d.rho z) (d.rotation z) - d.eigenvalue z / d.eigenvector z

noncomputable def NavierStokes.PrimaryODE.FrameData.errorC {Q : Type} (d : FrameData Q) (z : Q × ℝ) : ℝ

Error C, constructed using MovingFrameODE.coeff21.

Equations

• d.errorC z = NavierStokes.MovingFrameODE.coeff21 (d.F z) (((d.frame z) 1).ofLp 0) (inner ℝ ((d.frame z) 1) (d.shear z)) (d.rho z) (d.rotation z) - d.eigenvalue z * d.eigenvector z

noncomputable def NavierStokes.PrimaryODE.FrameData.error11 {Q : Type} (d : FrameData Q) (z : Q × ℝ) : ℝ

Error11, given by MovingFrameODE.modal11 (d.errorA z) (d.errorB z) (d.errorC z) (d.eigenvector z) (d.eigenRate z).

Equations

• d.error11 z = NavierStokes.MovingFrameODE.modal11 (d.errorA z) (d.errorB z) (d.errorC z) (d.eigenvector z) (d.eigenRate z)

noncomputable def NavierStokes.PrimaryODE.FrameData.error12 {Q : Type} (d : FrameData Q) (z : Q × ℝ) : ℝ

Error12, given by MovingFrameODE.modal12 (d.errorA z) (d.errorB z) (d.errorC z) (d.eigenvector z) (d.eigenRate z).

Equations

• d.error12 z = NavierStokes.MovingFrameODE.modal12 (d.errorA z) (d.errorB z) (d.errorC z) (d.eigenvector z) (d.eigenRate z)

noncomputable def NavierStokes.PrimaryODE.FrameData.error21 {Q : Type} (d : FrameData Q) (z : Q × ℝ) : ℝ

Error21, given by MovingFrameODE.modal21 (d.errorA z) (d.errorB z) (d.errorC z) (d.eigenvector z) (d.eigenRate z).

Equations

• d.error21 z = NavierStokes.MovingFrameODE.modal21 (d.errorA z) (d.errorB z) (d.errorC z) (d.eigenvector z) (d.eigenRate z)

noncomputable def NavierStokes.PrimaryODE.FrameData.error22 {Q : Type} (d : FrameData Q) (z : Q × ℝ) : ℝ

Error22, given by MovingFrameODE.modal22 (d.errorA z) (d.errorB z) (d.errorC z) (d.eigenvector z) (d.eigenRate z).

Equations

• d.error22 z = NavierStokes.MovingFrameODE.modal22 (d.errorA z) (d.errorB z) (d.errorC z) (d.eigenvector z) (d.eigenRate z)

noncomputable def NavierStokes.PrimaryODE.FrameData.damping {Q : Type} (d : FrameData Q) (j : ℤ) (z : Q × ℝ) : ℝ

Damping, given by (j : ℝ) ^ 2 * d.viscosity z.

Equations

• d.damping j z = ↑j ^ 2 * d.viscosity z

noncomputable def NavierStokes.PrimaryODE.FrameData.coefficient {Q : Type} (d : FrameData Q) (j : ℤ) (z : Q × ℝ) : State →L[ℝ] State

Coefficient, given by GrowingMode.modalOperator (d.eigenvalue z) (d.damping j z) (d.error11 z) (d.error12 z) (d.error21 z) (d.error22 z).

Equations

• d.coefficient j z = NavierStokes.GrowingMode.modalOperator (d.eigenvalue z) (d.damping j z) (d.error11 z) (d.error12 z) (d.error21 z) (d.error22 z)

noncomputable def NavierStokes.PrimaryODE.FrameData.forceX {Q : Type} (d : FrameData Q) (f : Q × ℝ → Space) (z : Q × ℝ) : ℝ

Force X, given by -(f z 0 - d.rho z * ⟪d.frame z 0, MovingFrameODE.tail (f z)⟫_ℝ) / (1 + d.rho z ^ 2).

Equations

• d.forceX f z = -((f z).ofLp 0 - d.rho z * inner ℝ ((d.frame z) 0) (NavierStokes.MovingFrameODE.tail (f z))) / (1 + d.rho z ^ 2)

noncomputable def NavierStokes.PrimaryODE.FrameData.forceY {Q : Type} (d : FrameData Q) (f : Q × ℝ → Space) (z : Q × ℝ) : ℝ

Force Y, given by -⟪d.frame z 1, MovingFrameODE.tail (f z)⟫_ℝ.

Equations

• d.forceY f z = -inner ℝ ((d.frame z) 1) (NavierStokes.MovingFrameODE.tail (f z))

noncomputable def NavierStokes.PrimaryODE.FrameData.forcing {Q : Type} (d : FrameData Q) (f : Q × ℝ → Space) (z : Q × ℝ) : State

Forcing, given by !₂[(d.forceX f z + d.forceY f z / d.eigenvector z) / 2, (d.forceX f z - d.forceY f z / d.eigenvector z) / 2].

Equations

• d.forcing f z = !₂[(d.forceX f z + d.forceY f z / d.eigenvector z) / 2, (d.forceX f z - d.forceY f z / d.eigenvector z) / 2]

noncomputable def NavierStokes.PrimaryODE.FrameData.ambient {Q : Type} (d : FrameData Q) (z : Q × ℝ) (w : State) : Space

Ambient, given by `MovingFrameODE.tangent (d.rho z) (d.frame z) (w 0 + w 1) (d.eigenvector z

• (w 0 - w 1))`.

Equations

• d.ambient z w = NavierStokes.MovingFrameODE.tangent (d.rho z) (d.frame z) (w.ofLp 0 + w.ofLp 1) (d.eigenvector z * (w.ofLp 0 - w.ofLp 1))

noncomputable def NavierStokes.PrimaryODE.FrameData.normal {Q : Type} (d : FrameData Q) (z : Q × ℝ) : Space

Normal, given by MovingFrameODE.normal (d.beta z) (d.rho z) (d.frame z).

Equations

• d.normal z = NavierStokes.MovingFrameODE.normal (d.beta z) (d.rho z) (d.frame z)

noncomputable def NavierStokes.PrimaryODE.FrameData.normalMotion {Q : Type} (d : FrameData Q) (z : Q × ℝ) : Space

Normal motion, given by MovingFrameODE.normalMotion (d.beta z) (d.betaDot z) (d.rho z) (d.rhoDot z) (d.rotation z) (d.frame z).

Equations

• d.normalMotion z = NavierStokes.MovingFrameODE.normalMotion (d.beta z) (d.betaDot z) (d.rho z) (d.rhoDot z) (d.rotation z) (d.frame z)

@[simp]

theorem NavierStokes.PrimaryODE.FrameData.forcing_zero {Q : Type} (d : FrameData Q) (z : Q × ℝ) : d.forcing (fun (x : Q × ℝ) => 0) z = 0

@[simp]

theorem NavierStokes.PrimaryODE.FrameData.forcing_zero_function {Q : Type} (d : FrameData Q) : (d.forcing fun (x : Q × ℝ) => 0) = fun (x : Q × ℝ) => 0

@[simp]

theorem NavierStokes.PrimaryODE.FrameData.damping_one {Q : Type} (d : FrameData Q) (z : Q × ℝ) : d.damping 1 z = d.viscosity z

theorem NavierStokes.PrimaryODE.FrameData.ambient_tangent {Q : Type} (d : FrameData Q) (z : Q × ℝ) (w : State) : inner ℝ (d.normal z) (d.ambient z w) = 0

structure NavierStokes.PrimaryODE.FrameData.Kinematics {Q : Type} (d : FrameData Q) (p : Q) (I : Set ℝ) : Prop

Actual derivatives of the supplied frame data, without assumptions about any ODE solution.

• beta_ne_zero (v : ℝ) : v ∈ I → d.beta (p, v) ≠ 0
• eigenvector_ne_zero (v : ℝ) : v ∈ I → d.eigenvector (p, v) ≠ 0
• beta_deriv (v : ℝ) : v ∈ I → HasDerivAt (fun (t : ℝ) => d.beta (p, t)) (d.betaDot (p, v)) v
• rho_deriv (v : ℝ) : v ∈ I → HasDerivAt (fun (t : ℝ) => d.rho (p, t)) (d.rhoDot (p, v)) v
• eigenvector_deriv (v : ℝ) : v ∈ I → HasDerivAt (fun (t : ℝ) => d.eigenvector (p, t)) (d.eigenRate (p, v) * d.eigenvector (p, v)) v
• frameK_deriv (v : ℝ) : v ∈ I → HasDerivAt (fun (t : ℝ) => (d.frame (p, t)) 0) (d.rotation (p, v) • (d.frame (p, v)) 1) v
• frameN_deriv (v : ℝ) : v ∈ I → HasDerivAt (fun (t : ℝ) => (d.frame (p, t)) 1) (-d.rotation (p, v) • (d.frame (p, v)) 0) v

noncomputable def NavierStokes.PrimaryODE.extendedFamily {Q : Type} {a b : ℝ} (hab : a ≤ b) (A : Q × ℝ → State →L[ℝ] State) (x₀ : Q → State) (f : Q × ℝ → State) (p : Q) : ℝ → State

The differentiable extension of the actual Volterra solution.

Equations

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

theorem NavierStokes.PrimaryODE.extendedFamily_eq_path {Q : Type} {a b : ℝ} (hab : a ≤ b) (A : Q × ℝ → State →L[ℝ] State) (x₀ : Q → State) (f : Q × ℝ → State) (p : Q) (v : ↑(Set.Icc a b)) : extendedFamily hab A x₀ f p ↑v = (SmoothPathFamily.odeFamily hab A x₀ f p) v

theorem NavierStokes.PrimaryODE.extendedFamily_initial {Q : Type} {a b : ℝ} (hab : a ≤ b) (A : Q × ℝ → State →L[ℝ] State) (x₀ : Q → State) (f : Q × ℝ → State) (p : Q) : extendedFamily hab A x₀ f p a = x₀ p

theorem NavierStokes.PrimaryODE.extendedFamily_hasDerivAt {Q : Type} [NormedAddCommGroup Q] {a b : ℝ} (hab : a ≤ b) {U : Set Q} (A : Q × ℝ → State →L[ℝ] State) (x₀ : Q → State) (f : Q × ℝ → State) (hA : ContinuousOn A (U ×ˢ Set.Icc a b)) (hf : ContinuousOn f (U ×ˢ Set.Icc a b)) {p : Q} (hp : p ∈ U) {v : ℝ} (hv : v ∈ Set.Icc a b) : HasDerivAt (extendedFamily hab A x₀ f p) ((A (p, v)) (extendedFamily hab A x₀ f p v) + f (p, v)) v

noncomputable def NavierStokes.PrimaryODE.solution {Q : Type} {a b : ℝ} (hab : a ≤ b) (d : FrameData Q) (j : ℤ) (x₀ : Q → State) (f : Q × ℝ → Space) (p : Q) : ℝ → State

Solution, given by extendedFamily hab (d.coefficient j) x₀ (d.forcing f) p.

Equations

• NavierStokes.PrimaryODE.solution hab d j x₀ f p = NavierStokes.PrimaryODE.extendedFamily hab (d.coefficient j) x₀ (d.forcing f) p

noncomputable def NavierStokes.PrimaryODE.ambientSolution {Q : Type} {a b : ℝ} (hab : a ≤ b) (d : FrameData Q) (j : ℤ) (x₀ : Q → State) (f : Q × ℝ → Space) (p : Q) (v : ℝ) : Space

Ambient solution, given by d.ambient (p, v) (solution hab d j x₀ f p v).

Equations

• NavierStokes.PrimaryODE.ambientSolution hab d j x₀ f p v = d.ambient (p, v) (NavierStokes.PrimaryODE.solution hab d j x₀ f p v)

theorem NavierStokes.PrimaryODE.solution_initial {Q : Type} {a b : ℝ} (hab : a ≤ b) (d : FrameData Q) (j : ℤ) (x₀ : Q → State) (f : Q × ℝ → Space) (p : Q) : solution hab d j x₀ f p a = x₀ p

theorem NavierStokes.PrimaryODE.solution_hasDerivAt {Q : Type} [NormedAddCommGroup Q] {a b : ℝ} (hab : a ≤ b) (d : FrameData Q) (j : ℤ) (x₀ : Q → State) (f : Q × ℝ → Space) {U : Set Q} (hA : ContinuousOn (d.coefficient j) (U ×ˢ Set.Icc a b)) (hf : ContinuousOn (d.forcing f) (U ×ˢ Set.Icc a b)) {p : Q} (hp : p ∈ U) {v : ℝ} (hv : v ∈ Set.Icc a b) : HasDerivAt (solution hab d j x₀ f p) ((d.coefficient j (p, v)) (solution hab d j x₀ f p v) + d.forcing f (p, v)) v

theorem NavierStokes.PrimaryODE.ambientSolution_tangent {Q : Type} {a b : ℝ} (hab : a ≤ b) (d : FrameData Q) (j : ℤ) (x₀ : Q → State) (f : Q × ℝ → Space) (p : Q) (v : ℝ) : inner ℝ (d.normal (p, v)) (ambientSolution hab d j x₀ f p v) = 0

theorem NavierStokes.PrimaryODE.ambientSolution_hasDerivAt {Q : Type} [NormedAddCommGroup Q] {a b : ℝ} (hab : a ≤ b) (d : FrameData Q) (j : ℤ) (x₀ : Q → State) (f : Q × ℝ → Space) {U : Set Q} (hA : ContinuousOn (d.coefficient j) (U ×ˢ Set.Icc a b)) (hf : ContinuousOn (d.forcing f) (U ×ˢ Set.Icc a b)) {p : Q} (hp : p ∈ U) (hk : d.Kinematics p (Set.Icc a b)) {v : ℝ} (hv : v ∈ Set.Icc a b) : HasDerivAt (ambientSolution hab d j x₀ f p) (TangentProjection.projectedRhs (d.normal (p, v)) (d.normalMotion (p, v)) (ambientSolution hab d j x₀ f p v) (MovingFrameODE.baseAction (d.F (p, v)) (d.shear (p, v)) (ambientSolution hab d j x₀ f p v)) (f (p, v)) (d.damping j (p, v))) v

Exact reconstruction into equation (27), including the projected physical forcing and harmonic-dependent scalar viscosity.

structure NavierStokes.PrimaryODE.FrameData.SmoothOn {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] (d : FrameData Q) (Ω : Set (Q × ℝ)) : Prop

Smoothness of the explicit input fields. Frame smoothness means smoothness of each ambient basis vector, avoiding an arbitrary manifold structure on the space of orthonormal bases.

• beta : ContDiffOn ℝ (↑⊤) d.beta Ω
• betaDot : ContDiffOn ℝ (↑⊤) d.betaDot Ω
• rho : ContDiffOn ℝ (↑⊤) d.rho Ω
• rhoDot : ContDiffOn ℝ (↑⊤) d.rhoDot Ω
• rotation : ContDiffOn ℝ (↑⊤) d.rotation Ω
• F : ContDiffOn ℝ (↑⊤) d.F Ω
• shear : ContDiffOn ℝ (↑⊤) d.shear Ω
• frame (i : Fin 2) : ContDiffOn ℝ (↑⊤) (fun (z : Q × ℝ) => (d.frame z) i) Ω
• eigenvalue : ContDiffOn ℝ (↑⊤) d.eigenvalue Ω
• eigenvector : ContDiffOn ℝ (↑⊤) d.eigenvector Ω
• eigenRate : ContDiffOn ℝ (↑⊤) d.eigenRate Ω
• viscosity : ContDiffOn ℝ (↑⊤) d.viscosity Ω
• eigenvector_ne_zero (z : Q × ℝ) : z ∈ Ω → d.eigenvector z ≠ 0

theorem NavierStokes.PrimaryODE.FrameData.SmoothOn.errorA {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {d : FrameData Q} {Ω : Set (Q × ℝ)} (h : d.SmoothOn Ω) : ContDiffOn ℝ (↑⊤) d.errorA Ω

theorem NavierStokes.PrimaryODE.FrameData.SmoothOn.errorB {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {d : FrameData Q} {Ω : Set (Q × ℝ)} (h : d.SmoothOn Ω) : ContDiffOn ℝ (↑⊤) d.errorB Ω

theorem NavierStokes.PrimaryODE.FrameData.SmoothOn.errorC {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {d : FrameData Q} {Ω : Set (Q × ℝ)} (h : d.SmoothOn Ω) : ContDiffOn ℝ (↑⊤) d.errorC Ω

theorem NavierStokes.PrimaryODE.FrameData.SmoothOn.modal_errors {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {d : FrameData Q} {Ω : Set (Q × ℝ)} (h : d.SmoothOn Ω) : ContDiffOn ℝ (↑⊤) d.error11 Ω ∧ ContDiffOn ℝ (↑⊤) d.error12 Ω ∧ ContDiffOn ℝ (↑⊤) d.error21 Ω ∧ ContDiffOn ℝ (↑⊤) d.error22 Ω

theorem NavierStokes.PrimaryODE.FrameData.SmoothOn.coefficient {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {d : FrameData Q} {Ω : Set (Q × ℝ)} (h : d.SmoothOn Ω) (j : ℤ) : ContDiffOn ℝ (↑⊤) (d.coefficient j) Ω

theorem NavierStokes.PrimaryODE.FrameData.SmoothOn.forcing {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {d : FrameData Q} {Ω : Set (Q × ℝ)} (h : d.SmoothOn Ω) {f : Q × ℝ → Space} (hf : ContDiffOn ℝ (↑⊤) f Ω) : ContDiffOn ℝ (↑⊤) (d.forcing f) Ω

theorem NavierStokes.PrimaryODE.solutionPath_contDiffOn {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {a b : ℝ} (hab : a ≤ b) (d : FrameData Q) (U : Set Q) (V : Set ℝ) (hU : IsOpen U) (hV : IsOpen V) (hI : Set.Icc a b ⊆ V) (hd : d.SmoothOn (U ×ˢ V)) (j : ℤ) (x₀ : Q → State) (f : Q × ℝ → Space) (hx₀ : ContDiffOn ℝ (↑⊤) x₀ U) (hf : ContDiffOn ℝ (↑⊤) f (U ×ˢ V)) : ContDiffOn ℝ (↑⊤) (SmoothPathFamily.odeFamily hab (d.coefficient j) x₀ (d.forcing f)) U

Jointly smooth physical/frame inputs give an actually constructed smooth family of modal paths.

theorem NavierStokes.PrimaryODE.FrameData.modal_errors_of_geometry {Q : Type} (d : FrameData Q) (z : Q × ℝ) (B₀ : Frame) (g₀ : State) {F₀ s M η H κ : ℝ} (hM : 1 ≤ M) (hη : 0 ≤ η) (hH : 0 ≤ H) (hρ : |d.rho z| ≤ M) (hs : |s| ≤ M) (hF₀ : |F₀| ≤ M) (hg₀ : ‖g₀‖ ≤ M) (horth : inner ℝ (B₀ 0) g₀ = 0) (hF : |d.F z - F₀| ≤ η) (hg : ‖d.shear z - g₀‖ ≤ η) (hK : ‖(d.frame z) 0 - B₀ 0‖ ≤ η) (hN : ‖(d.frame z) 1 - B₀ 1‖ ≤ η) (hρd : |d.rho z - s| ≤ η) (hρ' : |d.rhoDot z| ≤ η) (hrot : |d.rotation z| ≤ η) (hpair₁ : d.eigenvalue z / d.eigenvector z = 2 * F₀ * (B₀ 1).ofLp 0 / (1 + s ^ 2)) (hpair₂ : d.eigenvalue z * d.eigenvector z = -(2 * F₀ * (B₀ 1).ofLp 0 + inner ℝ (B₀ 1) g₀)) (hh : |d.eigenvector z| ≤ H) (hhi : |1 / d.eigenvector z| ≤ H) (hrate : |d.eigenRate z| ≤ κ) : |d.error11 z| ≤ (1 + 2 * H) * (16 * M ^ 2 * (1 + M) * η) + κ ∧ |d.error12 z| ≤ (1 + 2 * H) * (16 * M ^ 2 * (1 + M) * η) + κ ∧ |d.error21 z| ≤ (1 + 2 * H) * (16 * M ^ 2 * (1 + M) * η) + κ ∧ |d.error22 z| ≤ (1 + 2 * H) * (16 * M ^ 2 * (1 + M) * η) + κ

Geometric perturbations of the actual frame produce the four modal error bounds. The two reference identities are the chosen eigenpair equations.

theorem NavierStokes.PrimaryODE.FrameData.energy_bound {Q : Type} (d : FrameData Q) (z : Q × ℝ) {j : ℤ} (hj : j ≠ 0) {referenceDamping C D S : ℝ} (hlam : 0 ≤ d.eigenvalue z) (hν : 0 ≤ d.viscosity z) (hνerr : referenceDamping - D / S ≤ d.viscosity z) (herr : |d.error11 z| ≤ C / S ∧ |d.error12 z| ≤ C / S ∧ |d.error21 z| ≤ C / S ∧ |d.error22 z| ≤ C / S) (w : State) : inner ℝ w ((d.coefficient j z) w) ≤ (d.eigenvalue z - referenceDamping + (D + 4 * C) / S) * ‖w‖ ^ 2

Scalar viscosity keeps the same sign at every nonzero integer harmonic. The modal energy estimate is derived from entrywise coefficient errors.

noncomputable def NavierStokes.PrimaryODE.primarySeed {Q : Type} (a : ℝ) (P : Q × ℝ → ℝ) (p : Q) : State

Primary seed, given by !₂[P (p, a), 0].

Equations

• NavierStokes.PrimaryODE.primarySeed a P p = !₂[P (p, a), 0]

noncomputable def NavierStokes.PrimaryODE.primary {Q : Type} {a b : ℝ} (hab : a ≤ b) (d : FrameData Q) (P : Q × ℝ → ℝ) (p : Q) : ℝ → State

Primary, given by solution hab d 1 (primarySeed a P) (fun _ => 0) p.

Equations

• NavierStokes.PrimaryODE.primary hab d P p = NavierStokes.PrimaryODE.solution hab d 1 (NavierStokes.PrimaryODE.primarySeed a P) (fun (x : Q × ℝ) => 0) p

noncomputable def NavierStokes.PrimaryODE.radialPrimary {Q : Type} {a b : ℝ} (hab : a ≤ b) (d : FrameData Q) (P : Q × ℝ → ℝ) (p : Q) (v : ℝ) : ℝ

Radial primary, given by primary hab d P p v 0 + primary hab d P p v 1.

Equations

• NavierStokes.PrimaryODE.radialPrimary hab d P p v = (NavierStokes.PrimaryODE.primary hab d P p v).ofLp 0 + (NavierStokes.PrimaryODE.primary hab d P p v).ofLp 1

noncomputable def NavierStokes.PrimaryODE.transversePrimary {Q : Type} {a b : ℝ} (hab : a ≤ b) (d : FrameData Q) (P : Q × ℝ → ℝ) (p : Q) (v : ℝ) : ℝ

Transverse primary, given by d.eigenvector (p, v) * (primary hab d P p v 0 - primary hab d P p v 1).

Equations

• NavierStokes.PrimaryODE.transversePrimary hab d P p v = d.eigenvector (p, v) * ((NavierStokes.PrimaryODE.primary hab d P p v).ofLp 0 - (NavierStokes.PrimaryODE.primary hab d P p v).ofLp 1)

theorem NavierStokes.PrimaryODE.primary_initial {Q : Type} {a b : ℝ} (hab : a ≤ b) (d : FrameData Q) (P : Q × ℝ → ℝ) (p : Q) : primary hab d P p a = !₂[P (p, a), 0]

theorem NavierStokes.PrimaryODE.primary_hasDerivAt {Q : Type} [NormedAddCommGroup Q] {a b : ℝ} (hab : a ≤ b) (d : FrameData Q) (P : Q × ℝ → ℝ) {U : Set Q} (hA : ContinuousOn (d.coefficient 1) (U ×ˢ Set.Icc a b)) {p : Q} (hp : p ∈ U) {v : ℝ} (hv : v ∈ Set.Icc a b) : HasDerivAt (primary hab d P p) ((d.coefficient 1 (p, v)) (primary hab d P p v)) v

theorem NavierStokes.PrimaryODE.primary_bounds {Q : Type} [NormedAddCommGroup Q] {a b : ℝ} (hab : a ≤ b) (d : FrameData Q) (P : Q × ℝ → ℝ) {U : Set Q} (hA : ContinuousOn (d.coefficient 1) (U ×ˢ Set.Icc a b)) {p : Q} (hp : p ∈ U) {S C D L lammin : ℝ} (hlammin : 0 < lammin) (hC : 0 ≤ C) (hD : 0 ≤ D) (hS : 0 < S) (hlarge : 2 * GrowingMode.coneConstant lammin C ≤ S) (hslot : b - a ≤ L * S) (referenceDamping : ℝ → ℝ) (hlam : ∀ v ∈ Set.Icc a b, lammin ≤ d.eigenvalue (p, v)) (herr : ∀ v ∈ Set.Icc a b, |d.error11 (p, v)| ≤ C / S ∧ |d.error12 (p, v)| ≤ C / S ∧ |d.error21 (p, v)| ≤ C / S ∧ |d.error22 (p, v)| ≤ C / S) (hν : ∀ v ∈ Set.Icc a b, |d.viscosity (p, v) - referenceDamping v| ≤ D / S) (hPpos : ∀ v ∈ Set.Icc a b, 0 < P (p, v)) (hP : ∀ v ∈ Set.Icc a b, HasDerivAt (fun (t : ℝ) => P (p, t)) ((d.eigenvalue (p, v) - referenceDamping v) * P (p, v)) v) (v : ℝ) : v ∈ Set.Icc a b → 0 < radialPrimary hab d P p v ∧ Real.exp (-(D + 2 * C) * L) / 2 * P (p, v) ≤ radialPrimary hab d P p v ∧ radialPrimary hab d P p v ≤ 3 * Real.exp ((D + 2 * C) * L) / 2 * P (p, v) ∧ |transversePrimary hab d P p v / radialPrimary hab d P p v - d.eigenvector (p, v)| ≤ 4 * |d.eigenvector (p, v)| * (GrowingMode.coneConstant lammin C / S)

The actual constructed real primary has positive radial component, two-sided reference-envelope comparison, and a small eigenvector ratio error. Only coefficient estimates and the scalar reference equation are inputs.

theorem NavierStokes.PrimaryODE.solution_forward_bound {Q : Type} [NormedAddCommGroup Q] {a b : ℝ} (hab : a ≤ b) (d : FrameData Q) {j : ℤ} (hj : j ≠ 0) (x₀ : Q → State) (f : Q × ℝ → Space) {U : Set Q} (hA : ContinuousOn (d.coefficient j) (U ×ˢ Set.Icc a b)) (hf : ContinuousOn (d.forcing f) (U ×ˢ Set.Icc a b)) {p : Q} (hp : p ∈ U) (referenceDamping rate P : ℝ → ℝ) {S C D : ℝ} (hS : 0 < S) (hC : 0 ≤ C) (hD : 0 ≤ D) (hPpos : ∀ (v : ℝ), 0 < P v) (hP : ∀ (v : ℝ), HasDerivAt P (rate v * P v) v) (hreference : ∀ v ∈ Set.Icc a b, rate v = d.eigenvalue (p, v) - referenceDamping v) (hlam : ∀ v ∈ Set.Icc a b, 0 ≤ d.eigenvalue (p, v)) (hν : ∀ v ∈ Set.Icc a b, 0 ≤ d.viscosity (p, v)) (hνerr : ∀ v ∈ Set.Icc a b, referenceDamping v - D / S ≤ d.viscosity (p, v)) (herr : ∀ v ∈ Set.Icc a b, |d.error11 (p, v)| ≤ C / S ∧ |d.error12 (p, v)| ≤ C / S ∧ |d.error21 (p, v)| ≤ C / S ∧ |d.error22 (p, v)| ≤ C / S) (v : ℝ) : v ∈ Set.Icc a b → ‖solution hab d j x₀ f p v‖ ≤ Real.exp ((D + 4 * C) / S * (v - a)) * P v * (‖x₀ p‖ / P a + ∫ (s : ℝ) in a..v, ‖d.forcing f (p, s)‖ / P s)

theorem NavierStokes.PrimaryODE.homogeneous_forward_bound {Q : Type} [NormedAddCommGroup Q] {a b : ℝ} (hab : a ≤ b) (d : FrameData Q) {j : ℤ} (hj : j ≠ 0) (x₀ : Q → State) {U : Set Q} (hA : ContinuousOn (d.coefficient j) (U ×ˢ Set.Icc a b)) {p : Q} (hp : p ∈ U) (referenceDamping rate P : ℝ → ℝ) {S C D L : ℝ} (hS : 0 < S) (hC : 0 ≤ C) (hD : 0 ≤ D) (hslot : b - a ≤ L * S) (hPpos : ∀ (v : ℝ), 0 < P v) (hP : ∀ (v : ℝ), HasDerivAt P (rate v * P v) v) (hreference : ∀ v ∈ Set.Icc a b, rate v = d.eigenvalue (p, v) - referenceDamping v) (hlam : ∀ v ∈ Set.Icc a b, 0 ≤ d.eigenvalue (p, v)) (hν : ∀ v ∈ Set.Icc a b, 0 ≤ d.viscosity (p, v)) (hνerr : ∀ v ∈ Set.Icc a b, referenceDamping v - D / S ≤ d.viscosity (p, v)) (herr : ∀ v ∈ Set.Icc a b, |d.error11 (p, v)| ≤ C / S ∧ |d.error12 (p, v)| ≤ C / S ∧ |d.error21 (p, v)| ≤ C / S ∧ |d.error22 (p, v)| ≤ C / S) (v : ℝ) : v ∈ Set.Icc a b → ‖solution hab d j x₀ (fun (x : Q × ℝ) => 0) p v‖ ≤ Real.exp ((D + 4 * C) * L) * (P v / P a) * ‖x₀ p‖

The same forward propagator constant applies to every nonzero harmonic. The start of the finite interval may be any earlier slot time.

theorem NavierStokes.PrimaryODE.zero_initial_source_bound {Q : Type} [NormedAddCommGroup Q] {a b : ℝ} (hab : a ≤ b) (d : FrameData Q) {j : ℤ} (hj : j ≠ 0) (f : Q × ℝ → Space) {U : Set Q} (hA : ContinuousOn (d.coefficient j) (U ×ˢ Set.Icc a b)) (hf : ContinuousOn (d.forcing f) (U ×ˢ Set.Icc a b)) {p : Q} (hp : p ∈ U) (referenceDamping rate P : ℝ → ℝ) {S C D K : ℝ} (hS : 0 < S) (hC : 0 ≤ C) (hD : 0 ≤ D) (hPpos : ∀ (v : ℝ), 0 < P v) (hP : ∀ (v : ℝ), HasDerivAt P (rate v * P v) v) (hreference : ∀ v ∈ Set.Icc a b, rate v = d.eigenvalue (p, v) - referenceDamping v) (hlam : ∀ v ∈ Set.Icc a b, 0 ≤ d.eigenvalue (p, v)) (hν : ∀ v ∈ Set.Icc a b, 0 ≤ d.viscosity (p, v)) (hνerr : ∀ v ∈ Set.Icc a b, referenceDamping v - D / S ≤ d.viscosity (p, v)) (herr : ∀ v ∈ Set.Icc a b, |d.error11 (p, v)| ≤ C / S ∧ |d.error12 (p, v)| ≤ C / S ∧ |d.error21 (p, v)| ≤ C / S ∧ |d.error22 (p, v)| ≤ C / S) (hsource : ∀ v ∈ Set.Icc a b, ‖d.forcing f (p, v)‖ ≤ K * P v) (v : ℝ) : v ∈ Set.Icc a b → ‖solution hab d j (fun (x : Q) => 0) f p v‖ ≤ Real.exp ((D + 4 * C) / S * (v - a)) * P v * (K * (v - a))

Zero-initial source solves are constructed by the same operator, and retain every prescribed small amplitude factor in the source bound.

noncomputable def NavierStokes.PrimaryODE.FrameData.ofNormal {Q : Type} (n nDot : Q × ℝ → Space) (hne : ∀ (z : Q × ℝ), MovingFrameODE.tail (n z) ≠ 0) (F : Q × ℝ → ℝ) (g : Q × ℝ → State) (lam h hRate viscosityScale : Q × ℝ → ℝ) : FrameData Q

Build the actual frame from a supplied phase covector. All frame rates are computed from its supplied derivative; viscosity is the physical scalar multiple of the squared phase norm.

Equations

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

theorem NavierStokes.PrimaryODE.FrameData.ofNormal_normal {Q : Type} (n nDot : Q × ℝ → Space) (hne : ∀ (z : Q × ℝ), MovingFrameODE.tail (n z) ≠ 0) (F : Q × ℝ → ℝ) (g : Q × ℝ → State) (lam h hRate viscosityScale : Q × ℝ → ℝ) (z : Q × ℝ) : (ofNormal n nDot hne F g lam h hRate viscosityScale).normal z = n z

theorem NavierStokes.PrimaryODE.FrameData.ofNormal_kinematics {Q : Type} (n nDot : Q × ℝ → Space) (hne : ∀ (z : Q × ℝ), MovingFrameODE.tail (n z) ≠ 0) (F : Q × ℝ → ℝ) (g : Q × ℝ → State) (lam h hRate viscosityScale : Q × ℝ → ℝ) (p : Q) (I : Set ℝ) (hn : ∀ v ∈ I, HasDerivAt (fun (t : ℝ) => n (p, t)) (nDot (p, v)) v) (hh : ∀ v ∈ I, h (p, v) ≠ 0) (hdh : ∀ v ∈ I, HasDerivAt (fun (t : ℝ) => h (p, t)) (hRate (p, v) * h (p, v)) v) : (ofNormal n nDot hne F g lam h hRate viscosityScale).Kinematics p I

theorem NavierStokes.PrimaryODE.FrameData.Kinematics.normal_hasDerivAt {Q : Type} {d : FrameData Q} {p : Q} {I : Set ℝ} (hk : d.Kinematics p I) {v : ℝ} (hv : v ∈ I) : HasDerivAt (fun (t : ℝ) => d.normal (p, t)) (d.normalMotion (p, v)) v

theorem NavierStokes.PrimaryODE.FrameData.ofNormal_normalMotion {Q : Type} (n nDot : Q × ℝ → Space) (hne : ∀ (z : Q × ℝ), MovingFrameODE.tail (n z) ≠ 0) (F : Q × ℝ → ℝ) (g : Q × ℝ → State) (lam h hRate viscosityScale : Q × ℝ → ℝ) {p : Q} {v : ℝ} (hn : HasDerivAt (fun (t : ℝ) => n (p, t)) (nDot (p, v)) v) : (ofNormal n nDot hne F g lam h hRate viscosityScale).normalMotion (p, v) = nDot (p, v)

theorem NavierStokes.PrimaryODE.norm_iteratedFDeriv_solution_le_polynomial {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {a b : ℝ} (hab : a ≤ b) (d : FrameData Q) (U : Set Q) (V : Set ℝ) (hU : IsOpen U) (hV : IsOpen V) (hI : Set.Icc a b ⊆ V) (hd : d.SmoothOn (U ×ˢ V)) {j : ℤ} (hj : j ≠ 0) (x₀ : Q → State) (f : Q × ℝ → Space) (hx₀ : ContDiffOn ℝ (↑⊤) x₀ U) (hf : ContDiffOn ℝ (↑⊤) f (U ×ˢ V)) {p : Q} (hp : p ∈ U) (referenceDamping rate W : ℝ → ℝ) {S C D K w : ℝ} (hS : 1 ≤ S) (hC : 0 ≤ C) (hD : 0 ≤ D) (hK : 1 ≤ K) (hw : 0 ≤ w) (hW : ∀ (v : ℝ), 0 < W v) (hdW : ∀ (v : ℝ), HasDerivAt W (rate v * W v) v) (hreference : ∀ v ∈ Set.Icc a b, rate v = d.eigenvalue (p, v) - referenceDamping v) (hlam : ∀ v ∈ Set.Icc a b, 0 ≤ d.eigenvalue (p, v)) (hν : ∀ v ∈ Set.Icc a b, 0 ≤ d.viscosity (p, v)) (hνerr : ∀ v ∈ Set.Icc a b, referenceDamping v - D / S ≤ d.viscosity (p, v)) (herr : ∀ v ∈ Set.Icc a b, |d.error11 (p, v)| ≤ C / S ∧ |d.error12 (p, v)| ≤ C / S ∧ |d.error21 (p, v)| ≤ C / S ∧ |d.error22 (p, v)| ≤ C / S) (hExp : Real.exp ((D + 4 * C) / S * (b - a)) ≤ K) (hslot : b - a ≤ K * S) (m N : ℕ) (hAj : ∀ k ≤ N, ∀ (v : ↑(Set.Icc a b)), ‖iteratedFDeriv ℝ k (fun (q : Q) => d.coefficient j (q, ↑v)) p‖ ≤ K * S ^ m) (hxj : ∀ k ≤ N, ‖iteratedFDeriv ℝ k x₀ p‖ ≤ w * K * S ^ m * W a) (hfj : ∀ k ≤ N, ∀ (v : ↑(Set.Icc a b)), ‖iteratedFDeriv ℝ k (fun (q : Q) => d.forcing f (q, ↑v)) p‖ ≤ w * K * S ^ m * W ↑v) (n : ℕ) (hn : n ≤ N) (v : ↑(Set.Icc a b)) : ‖iteratedFDeriv ℝ n (fun (q : Q) => solution hab d j x₀ f q ↑v) p‖ ≤ w * (2 ^ (N + 1) * K ^ 3) ^ (n + 1) * S ^ ((m + 1) * (n + 1)) * W ↑v

Full ordinary Fréchet jets of the same constructed solution. All numerical jet assumptions concern explicitly defined coefficients, initial data and forcing; the output jet bound is derived by the triangular variational ODE.

noncomputable def NavierStokes.PrimaryODE.referenceProfile (c₀ u ell v : ℝ) : ℝ

Reference profile, given by c₀ * Real.sqrt (1 + PulseGrowth.slotMagnitude u ell v ^ 2).

Equations

• NavierStokes.PrimaryODE.referenceProfile c₀ u ell v = c₀ * √(1 + NavierStokes.PulseGrowth.slotMagnitude u ell v ^ 2)

noncomputable def NavierStokes.PrimaryODE.referenceProfileRate (u ell v : ℝ) : ℝ

Reference profile rate, given by PulseGrowth.slotMagnitude u ell v * (u / ell) / (1 + PulseGrowth.slotMagnitude u ell v ^ 2).

Equations

• NavierStokes.PrimaryODE.referenceProfileRate u ell v = NavierStokes.PulseGrowth.slotMagnitude u ell v * (u / ell) / (1 + NavierStokes.PulseGrowth.slotMagnitude u ell v ^ 2)

theorem NavierStokes.PrimaryODE.hasDerivAt_referenceProfile (c₀ u ell v : ℝ) : HasDerivAt (referenceProfile c₀ u ell) (referenceProfileRate u ell v * referenceProfile c₀ u ell v) v

theorem NavierStokes.PrimaryODE.referenceProfile_ne_zero {c₀ : ℝ} (hc₀ : c₀ ≠ 0) (u ell v : ℝ) : referenceProfile c₀ u ell v ≠ 0

theorem NavierStokes.PrimaryODE.referenceEigenvalue_lower {lam u ell v : ℝ} (hlam : 0 < lam) (hu : 0 ≤ u) (hell : 0 < ell) (hv : v ∈ Set.Icc 0 ell) : lam / √(1 + (3 * u / 2) ^ 2) ≤ ViscousPropagator.referenceEigenvalue lam u ell v

noncomputable def NavierStokes.PrimaryODE.referenceEnvelope {Q : Type} (lam u : Q → ℝ) (ell : ℝ) (z : Q × ℝ) : ℝ

Reference envelope, given by GaussianEnvelope.envelope (GaussianEnvelope.referenceRate (lam z.1) (u z.1) ell) (ell / 2) z.2.

Equations

• NavierStokes.PrimaryODE.referenceEnvelope lam u ell z = NavierStokes.GaussianEnvelope.envelope (NavierStokes.GaussianEnvelope.referenceRate (lam z.1) (u z.1) ell) (ell / 2) z.2

theorem NavierStokes.PrimaryODE.primary_gaussian_bounds {Q : Type} [NormedAddCommGroup Q] {ell : ℝ} (hell : 0 < ell) (d : FrameData Q) (lam u c₀ : Q → ℝ) {U : Set Q} (hA : ContinuousOn (d.coefficient 1) (U ×ˢ Set.Icc 0 ell)) {p : Q} (hp : p ∈ U) (hlam : 0 < lam p) (hu : 0 < u p) {S C D L : ℝ} (hC : 0 ≤ C) (hD : 0 ≤ D) (hS : 0 < S) (hlarge : 2 * GrowingMode.coneConstant (lam p / √(1 + (3 * u p / 2) ^ 2)) C ≤ S) (hslot : ell ≤ L * S) (heigen : ∀ v ∈ Set.Icc 0 ell, d.eigenvalue (p, v) = ViscousPropagator.referenceEigenvalue (lam p) (u p) ell v) (hprofile : ∀ v ∈ Set.Icc 0 ell, d.eigenvector (p, v) = referenceProfile (c₀ p) (u p) ell v) (herr : ∀ v ∈ Set.Icc 0 ell, |d.error11 (p, v)| ≤ C / S ∧ |d.error12 (p, v)| ≤ C / S ∧ |d.error21 (p, v)| ≤ C / S ∧ |d.error22 (p, v)| ≤ C / S) (hν : ∀ v ∈ Set.Icc 0 ell, |d.viscosity (p, v) - ViscousPropagator.referenceViscosity (lam p) (u p) ell v| ≤ D / S) : ∃ (b : ℝ) (B : ℝ), 0 < b ∧ 0 < B ∧ ∀ v ∈ Set.Icc 0 ell, 0 < radialPrimary ⋯ d (referenceEnvelope lam u ell) p v ∧ Real.exp (-(D + 2 * C) * L) / 2 * Real.exp (-B * (v - ell / 2) ^ 2 / ell) ≤ radialPrimary ⋯ d (referenceEnvelope lam u ell) p v ∧ radialPrimary ⋯ d (referenceEnvelope lam u ell) p v ≤ 3 * Real.exp ((D + 2 * C) * L) / 2 * Real.exp (-b * (v - ell / 2) ^ 2 / ell) ∧ |transversePrimary ⋯ d (referenceEnvelope lam u ell) p v / radialPrimary ⋯ d (referenceEnvelope lam u ell) p v - referenceProfile (c₀ p) (u p) ell v| ≤ 4 * |referenceProfile (c₀ p) (u p) ell v| * (GrowingMode.coneConstant (lam p / √(1 + (3 * u p / 2) ^ 2)) C / S)

The actual primary is bounded above and below by the manuscript's Gaussian envelopes. The reference scalar equation and spectral gap are derived here from the displayed reference rate; they are not assumptions about a solution.

theorem NavierStokes.PrimaryODE.initialEnvelope_contDiffOn {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {a b : ℝ} (hab : a ≤ b) (U : Set Q) (V : Set ℝ) (hU : IsOpen U) (hV : IsOpen V) (hI : Set.Icc a b ⊆ V) (rate : Q × ℝ → ℝ) (hrate : ContDiffOn ℝ (↑⊤) rate (U ×ˢ V)) (midpoint : ↑(Set.Icc a b)) : ContDiffOn ℝ (↑⊤) (fun (p : Q) => GaussianEnvelope.envelope (fun (t : ℝ) => rate (p, t)) (↑midpoint) a) U

Smoothness of the actual initial envelope, proved using integration as a bounded linear map on the fixed compact time interval.

theorem NavierStokes.PrimaryODE.referenceRate_contDiffOn {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {U : Set Q} (V : Set ℝ) (lam u : Q → ℝ) (ell : ℝ) (hlam : ContDiffOn ℝ (↑⊤) lam U) (hu : ContDiffOn ℝ (↑⊤) u U) : ContDiffOn ℝ (↑⊤) (fun (z : Q × ℝ) => GaussianEnvelope.referenceRate (lam z.1) (u z.1) ell z.2) (U ×ˢ V)

theorem NavierStokes.PrimaryODE.primarySeed_reference_contDiffOn {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {ell : ℝ} (hell : 0 ≤ ell) (U : Set Q) (V : Set ℝ) (hU : IsOpen U) (hV : IsOpen V) (hI : Set.Icc 0 ell ⊆ V) (lam u : Q → ℝ) (hlam : ContDiffOn ℝ (↑⊤) lam U) (hu : ContDiffOn ℝ (↑⊤) u U) : ContDiffOn ℝ (↑⊤) (primarySeed 0 (referenceEnvelope lam u ell)) U

The manuscript normalization z₊(0)=P(0), z₋(0)=0 is itself a smooth parameter family, obtained from the explicit reference rate.

theorem NavierStokes.PrimaryODE.primary_reference_path_contDiffOn {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {ell : ℝ} (hell : 0 ≤ ell) (d : FrameData Q) (U : Set Q) (V : Set ℝ) (hU : IsOpen U) (hV : IsOpen V) (hI : Set.Icc 0 ell ⊆ V) (hd : d.SmoothOn (U ×ˢ V)) (lam u : Q → ℝ) (hlam : ContDiffOn ℝ (↑⊤) lam U) (hu : ContDiffOn ℝ (↑⊤) u U) : ContDiffOn ℝ (↑⊤) (SmoothPathFamily.odeFamily hell (d.coefficient 1) (primarySeed 0 (referenceEnvelope lam u ell)) (d.forcing fun (x : Q × ℝ) => 0)) U

theorem NavierStokes.PrimaryODE.solution_contDiffOn {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {a b : ℝ} (hab : a ≤ b) (d : FrameData Q) (U : Set Q) (V : Set ℝ) (hU : IsOpen U) (hV : IsOpen V) (hI : Set.Icc a b ⊆ V) (hd : d.SmoothOn (U ×ˢ V)) (j : ℤ) (x₀ : Q → State) (f : Q × ℝ → Space) (hx₀ : ContDiffOn ℝ (↑⊤) x₀ U) (hf : ContDiffOn ℝ (↑⊤) f (U ×ˢ V)) (v : ↑(Set.Icc a b)) : ContDiffOn ℝ (↑⊤) (fun (q : Q) => solution hab d j x₀ f q ↑v) U

Parameter smoothness of the constructed extension at every time in the closed slot, including its endpoints.

theorem NavierStokes.PrimaryODE.ambientSolution_contDiffOn {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {a b : ℝ} (hab : a ≤ b) (d : FrameData Q) (U : Set Q) (V : Set ℝ) (hU : IsOpen U) (hV : IsOpen V) (hI : Set.Icc a b ⊆ V) (hd : d.SmoothOn (U ×ˢ V)) (j : ℤ) (x₀ : Q → State) (f : Q × ℝ → Space) (hx₀ : ContDiffOn ℝ (↑⊤) x₀ U) (hf : ContDiffOn ℝ (↑⊤) f (U ×ˢ V)) (v : ↑(Set.Icc a b)) : ContDiffOn ℝ (↑⊤) (fun (q : Q) => ambientSolution hab d j x₀ f q ↑v) U

Reconstructed ambient tangent vectors inherit parameter smoothness from the same constructed modal path and the explicit smooth frame data.

theorem NavierStokes.PrimaryODE.solution_joint_contDiffOn {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {a b : ℝ} (hab : a ≤ b) (d : FrameData Q) (U : Set Q) (V : Set ℝ) (hU : IsOpen U) (hV : IsOpen V) (hI : Set.Icc a b ⊆ V) (hd : d.SmoothOn (U ×ˢ V)) (j : ℤ) (x₀ : Q → State) (f : Q × ℝ → Space) (hx₀ : ContDiffOn ℝ (↑⊤) x₀ U) (hf : ContDiffOn ℝ (↑⊤) f (U ×ˢ V)) : ContDiffOn ℝ (↑⊤) (fun (z : Q × ℝ) => solution hab d j x₀ f z.1 z.2) (U ×ˢ Set.Icc a b)

Genuine joint parameter/time smoothness of the constructed solution on the closed slot. The joint theorem constructs a smooth representative by time rescaling, rather than claiming the clamped extension smooth outside.

theorem NavierStokes.PrimaryODE.ambientSolution_joint_contDiffOn {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {a b : ℝ} (hab : a ≤ b) (d : FrameData Q) (U : Set Q) (V : Set ℝ) (hU : IsOpen U) (hV : IsOpen V) (hI : Set.Icc a b ⊆ V) (hd : d.SmoothOn (U ×ˢ V)) (j : ℤ) (x₀ : Q → State) (f : Q × ℝ → Space) (hx₀ : ContDiffOn ℝ (↑⊤) x₀ U) (hf : ContDiffOn ℝ (↑⊤) f (U ×ˢ V)) : ContDiffOn ℝ (↑⊤) (fun (z : Q × ℝ) => ambientSolution hab d j x₀ f z.1 z.2) (U ×ˢ Set.Icc a b)

theorem NavierStokes.PrimaryODE.viscosity_error_of_normal_comparison {n n₀ : Space} {κ η M : ℝ} (hκ : 0 ≤ κ) (hclose : ‖n - n₀‖ ≤ η) (hn₀ : ‖n₀‖ ≤ M) : |κ * ‖n‖ ^ 2 - κ * ‖n₀‖ ^ 2| ≤ κ * η * (2 * M + η)

The physical viscosity perturbation follows from closeness of the actual phase normal. This gives the damping input without assuming an ODE bound.

theorem NavierStokes.PrimaryODE.FrameData.forcing_norm_le {Q : Type} (d : FrameData Q) (f : Q × ℝ → Space) (z : Q × ℝ) {R H : ℝ} (hR : 0 ≤ R) (hH : 0 ≤ H) (hrho : |d.rho z| ≤ R) (hh : |1 / d.eigenvector z| ≤ H) : ‖d.forcing f z‖ ≤ (1 + R + H) * ‖f z‖

The source transformation has a uniform norm bound from elementary frame and eigenvector bounds, independently of the harmonic index.

theorem NavierStokes.PrimaryODE.FrameData.ambient_norm_le {Q : Type} (d : FrameData Q) (z : Q × ℝ) (w : State) {R H : ℝ} (hrho : |d.rho z| ≤ R) (hh : |d.eigenvector z| ≤ H) : ‖d.ambient z w‖ ≤ 2 * (1 + R + H) * ‖w‖

theorem NavierStokes.PrimaryODE.FrameData.norm_le_ambient {Q : Type} (d : FrameData Q) (z : Q × ℝ) (w : State) {H : ℝ} (hne : d.eigenvector z ≠ 0) (hh : |1 / d.eigenvector z| ≤ H) : ‖w‖ ≤ (1 + H) * ‖d.ambient z w‖

The inverse coordinate transformation is uniformly bounded too, so the modal forward estimate is a genuine ambient tangent propagator estimate.

theorem NavierStokes.PrimaryODE.ambient_homogeneous_forward_bound {Q : Type} [NormedAddCommGroup Q] {a b : ℝ} (hab : a ≤ b) (d : FrameData Q) {j : ℤ} (hj : j ≠ 0) (x₀ : Q → State) {U : Set Q} (hA : ContinuousOn (d.coefficient j) (U ×ˢ Set.Icc a b)) {p : Q} (hp : p ∈ U) (referenceDamping rate P : ℝ → ℝ) {S C D L R H : ℝ} (hS : 0 < S) (hC : 0 ≤ C) (hD : 0 ≤ D) (hslot : b - a ≤ L * S) (hPpos : ∀ (v : ℝ), 0 < P v) (hP : ∀ (v : ℝ), HasDerivAt P (rate v * P v) v) (hreference : ∀ v ∈ Set.Icc a b, rate v = d.eigenvalue (p, v) - referenceDamping v) (hlam : ∀ v ∈ Set.Icc a b, 0 ≤ d.eigenvalue (p, v)) (hν : ∀ v ∈ Set.Icc a b, 0 ≤ d.viscosity (p, v)) (hνerr : ∀ v ∈ Set.Icc a b, referenceDamping v - D / S ≤ d.viscosity (p, v)) (herr : ∀ v ∈ Set.Icc a b, |d.error11 (p, v)| ≤ C / S ∧ |d.error12 (p, v)| ≤ C / S ∧ |d.error21 (p, v)| ≤ C / S ∧ |d.error22 (p, v)| ≤ C / S) (hrho : ∀ v ∈ Set.Icc a b, |d.rho (p, v)| ≤ R) (hh : ∀ v ∈ Set.Icc a b, |d.eigenvector (p, v)| ≤ H) (hne : d.eigenvector (p, a) ≠ 0) (hhi : |1 / d.eigenvector (p, a)| ≤ H) (v : ℝ) : v ∈ Set.Icc a b → ‖ambientSolution hab d j x₀ (fun (x : Q × ℝ) => 0) p v‖ ≤ 2 * (1 + R + H) * (1 + H) * Real.exp ((D + 4 * C) * L) * (P v / P a) * ‖ambientSolution hab d j x₀ (fun (x : Q × ℝ) => 0) p a‖

The forward estimate in actual ambient tangent norm, with constants independent of the nonzero integer harmonic.

noncomputable def NavierStokes.PrimaryODE.localFrame (n : Space) : Frame

Total frame selection. The fallback is outside the nonvanishing phase chart and imposes no hypothesis on those unused parameter values.

Equations

• NavierStokes.PrimaryODE.localFrame n = if hn : NavierStokes.MovingFrameODE.tail n ≠ 0 then NavierStokes.MovingFrameODE.normalFrame n hn else EuclideanSpace.basisFun (Fin 2) ℝ

theorem NavierStokes.PrimaryODE.localFrame_eq {n : Space} (hn : MovingFrameODE.tail n ≠ 0) : localFrame n = MovingFrameODE.normalFrame n hn

noncomputable def NavierStokes.PrimaryODE.FrameData.ofNormalLocal {Q : Type} (n nDot : Q × ℝ → Space) (F : Q × ℝ → ℝ) (g : Q × ℝ → State) (lam h hRate viscosityScale : Q × ℝ → ℝ) : FrameData Q

The actual phase-derived coefficients require nonvanishing only on the chart where they are used.

Equations

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

theorem NavierStokes.PrimaryODE.FrameData.ofNormalLocal_normal {Q : Type} (n nDot : Q × ℝ → Space) (F : Q × ℝ → ℝ) (g : Q × ℝ → State) (lam h hRate viscosityScale : Q × ℝ → ℝ) {z : Q × ℝ} (hn : MovingFrameODE.tail (n z) ≠ 0) : (ofNormalLocal n nDot F g lam h hRate viscosityScale).normal z = n z

theorem NavierStokes.PrimaryODE.FrameData.ofNormalLocal_kinematics {Q : Type} (n nDot : Q × ℝ → Space) (F : Q × ℝ → ℝ) (g : Q × ℝ → State) (lam h hRate viscosityScale : Q × ℝ → ℝ) (p : Q) (I : Set ℝ) (hn : ∀ v ∈ I, HasDerivAt (fun (t : ℝ) => n (p, t)) (nDot (p, v)) v) (hne : ∀ v ∈ I, MovingFrameODE.tail (n (p, v)) ≠ 0) (hh : ∀ v ∈ I, h (p, v) ≠ 0) (hdh : ∀ v ∈ I, HasDerivAt (fun (t : ℝ) => h (p, t)) (hRate (p, v) * h (p, v)) v) : (ofNormalLocal n nDot F g lam h hRate viscosityScale).Kinematics p I

theorem NavierStokes.PrimaryODE.FrameData.ofNormalLocal_normalMotion {Q : Type} (n nDot : Q × ℝ → Space) (F : Q × ℝ → ℝ) (g : Q × ℝ → State) (lam h hRate viscosityScale : Q × ℝ → ℝ) {p : Q} {v : ℝ} (hn : HasDerivAt (fun (t : ℝ) => n (p, t)) (nDot (p, v)) v) (hne : MovingFrameODE.tail (n (p, v)) ≠ 0) : (ofNormalLocal n nDot F g lam h hRate viscosityScale).normalMotion (p, v) = nDot (p, v)