Stability of the actual Navier--Stokes residual under flat perturbations

Flatness and power growth below are bounds on norms of actual iterated Fréchet derivatives. The differential and bilinear closure lemmas are proved from the derivative identities and Leibniz estimates, not assumed.

Scalar flatness and fixed power losses

This file isolates the scalar asymptotic argument used in Lemmas 11.2--11.5 of the candidate manuscript. It proves neither the asserted bounds for physical jets nor the existence, compatibility, or smooth extension of those jets.

All powers here have natural exponents. Constants and neighborhoods may depend on the requested power, as they do in a flatness statement.

def NavierStokes.Flatness.PowerFlat {α : Type u_1} (l : Filter α) (q f : α → ℝ) : Prop

Along l, f is eventually bounded by a constant times every natural power of the absolute value of the scale q.

Equations

• NavierStokes.Flatness.PowerFlat l q f = ∀ (n : ℕ), ∃ (C : ℝ), 0 ≤ C ∧ ∀ᶠ (x : α) in l, |f x| ≤ C * |q x| ^ n

theorem NavierStokes.Flatness.fixed_power_loss_bound {x scale C : ℝ} {n loss : ℕ} (hscale : scale ≠ 0) (hx : |x| ≤ C * |scale| ^ (n + loss)) : |x / scale ^ loss| ≤ C * |scale| ^ n

An exact scalar estimate: n + loss powers of smallness absorb loss powers in a nonzero denominator. No assumption that the scale is small is needed for this algebraic step.

theorem NavierStokes.Flatness.PowerFlat.div_pow {α : Type u_1} {l : Filter α} {q f : α → ℝ} (hf : PowerFlat l q f) (hq : ∀ᶠ (x : α) in l, q x ≠ 0) (loss : ℕ) : PowerFlat l q fun (x : α) => f x / q x ^ loss

Arbitrary power decay persists after any fixed inverse-power loss.

theorem NavierStokes.Flatness.PowerFlat.add {α : Type u_1} {l : Filter α} {q f g : α → ℝ} (hf : PowerFlat l q f) (hg : PowerFlat l q g) : PowerFlat l q fun (x : α) => f x + g x

Flat estimates are stable under finite addition.

theorem NavierStokes.Flatness.PowerFlat.mul {α : Type u_1} {l : Filter α} {q f g : α → ℝ} (hf : PowerFlat l q f) (hg : PowerFlat l q g) : PowerFlat l q fun (x : α) => f x * g x

Flat estimates are stable under multiplication. Only boundedness of the second factor, the n = 0 case of its flatness, is used.

theorem NavierStokes.Flatness.PowerFlat.mul_of_power_bound {α : Type u_1} {l : Filter α} {q f g : α → ℝ} (hf : PowerFlat l q f) (hq : ∀ᶠ (x : α) in l, q x ≠ 0) (loss : ℕ) {D : ℝ} (hD : 0 ≤ D) (hg : ∀ᶠ (x : α) in l, |g x| ≤ D / |q x| ^ loss) : PowerFlat l q fun (x : α) => f x * g x

A flat scalar times a scalar with a fixed power loss remains flat. This models one factor in the residual product estimates, provided the stated bounds have already been established for the actual factors.

theorem NavierStokes.Flatness.powerFlat_of_stage_bounds {α : Type u_1} {l : Filter α} {q f : α → ℝ} {exponent : ℕ → ℕ} (loss : ℕ) (hexponent : ∀ (n : ℕ), ∃ (j : ℕ), n ≤ exponent j) (hq : ∀ᶠ (x : α) in l, |q x| ≤ 1) (hstage : ∀ (j : ℕ), ∃ (C : ℝ), 0 ≤ C ∧ ∀ᶠ (x : α) in l, |f x| ≤ C * |q x| ^ (exponent j - loss)) : PowerFlat l q f

Stage bounds with unbounded natural exponents imply flatness even after subtracting a fixed natural loss. Each stage has its own constant and eventual neighborhood; no uniformity of these quantities in the stage is assumed.

theorem NavierStokes.Flatness.PowerFlat.tendsto_zero {α : Type u_1} {l : Filter α} {q f : α → ℝ} (hf : PowerFlat l q f) (hq : Filter.Tendsto q l (nhds 0)) : Filter.Tendsto f l (nhds 0)

Flatness gives an actual zero limit when the scale tends to zero. This is a scalar limit theorem, not a theorem about differentiability.

theorem NavierStokes.Flatness.PowerFlat.div_pow_tendsto_zero {α : Type u_1} {l : Filter α} {q f : α → ℝ} (hf : PowerFlat l q f) (hq : Filter.Tendsto q l (nhds 0)) (hq_ne : ∀ᶠ (x : α) in l, q x ≠ 0) (loss : ℕ) : Filter.Tendsto (fun (x : α) => f x / q x ^ loss) l (nhds 0)

The zero limit survives every fixed inverse-power loss.

theorem NavierStokes.ResidualStability.scalarFlat_mono {X : Type u_1} {l : Filter X} {q f g : X → ℝ} (hf : Flatness.PowerFlat l q f) (hgf : ∀ᶠ (x : X) in l, |g x| ≤ |f x|) : Flatness.PowerFlat l q g

theorem NavierStokes.ResidualStability.scalarFlat_const_mul {X : Type u_1} {l : Filter X} {q f : X → ℝ} (c : ℝ) (hf : Flatness.PowerFlat l q f) : Flatness.PowerFlat l q fun (x : X) => c * f x

theorem NavierStokes.ResidualStability.scalarFlat_zero {X : Type u_1} {l : Filter X} {q : X → ℝ} : Flatness.PowerFlat l q fun (x : X) => 0

theorem NavierStokes.ResidualStability.scalarFlat_sum {X : Type u_1} {l : Filter X} {q : X → ℝ} {ι : Type u_2} (s : Finset ι) (f : ι → X → ℝ) (hf : ∀ i ∈ s, Flatness.PowerFlat l q (f i)) : Flatness.PowerFlat l q fun (x : X) => ∑ i ∈ s, f i x

def NavierStokes.ResidualStability.AllJetsFlat {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (l : Filter D) (q : D → ℝ) (f : D → E) : Prop

Every actual derivative decays faster than each fixed natural power.

Equations

• NavierStokes.ResidualStability.AllJetsFlat l q f = ∀ (m : ℕ), NavierStokes.Flatness.PowerFlat l q fun (x : D) => ‖iteratedFDeriv ℝ m f x‖

def NavierStokes.ResidualStability.AllJetsGrowth {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (l : Filter D) (q : D → ℝ) (f : D → E) : Prop

Each actual derivative has a fixed inverse-power bound. The power and constant may depend on the derivative order, but not on the point.

Equations

• NavierStokes.ResidualStability.AllJetsGrowth l q f = ∀ (m : ℕ), ∃ (K : ℕ) (C : ℝ), 0 ≤ C ∧ ∀ᶠ (x : D) in l, ‖iteratedFDeriv ℝ m f x‖ ≤ C / |q x| ^ K

theorem NavierStokes.ResidualStability.AllJetsFlat.fderiv {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {l : Filter D} {q : D → ℝ} {f : D → E} (hf : AllJetsFlat l q f) : AllJetsFlat l q (_root_.fderiv ℝ f)

theorem NavierStokes.ResidualStability.AllJetsGrowth.fderiv {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {l : Filter D} {q : D → ℝ} {f : D → E} (hf : AllJetsGrowth l q f) : AllJetsGrowth l q (_root_.fderiv ℝ f)

theorem NavierStokes.ResidualStability.AllJetsFlat.growth {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {l : Filter D} {q : D → ℝ} {f : D → E} (hf : AllJetsFlat l q f) : AllJetsGrowth l q f

theorem NavierStokes.ResidualStability.iteratedFDeriv_eqOn {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {f g : D → E} (hU : IsOpen U) (hfg : Set.EqOn f g U) (m : ℕ) : Set.EqOn (iteratedFDeriv ℝ m f) (iteratedFDeriv ℝ m g) U

theorem NavierStokes.ResidualStability.AllJetsFlat.congr_on {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {l : Filter D} {q : D → ℝ} {f : D → E} {U : Set D} {g : D → E} (hf : AllJetsFlat l q f) (hU : IsOpen U) (hl : ∀ᶠ (x : D) in l, x ∈ U) (hfg : Set.EqOn f g U) : AllJetsFlat l q g

theorem NavierStokes.ResidualStability.AllJetsGrowth.congr_on {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {l : Filter D} {q : D → ℝ} {f : D → E} {U : Set D} {g : D → E} (hf : AllJetsGrowth l q f) (hU : IsOpen U) (hl : ∀ᶠ (x : D) in l, x ∈ U) (hfg : Set.EqOn f g U) : AllJetsGrowth l q g

theorem NavierStokes.ResidualStability.norm_jet_linear_map {D : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : D → E} {U : Set D} (L : E →L[ℝ] F) (hU : IsOpen U) (hf : ContDiffOn ℝ (↑⊤) f U) {x : D} (hx : x ∈ U) (m : ℕ) : ‖iteratedFDeriv ℝ m (fun (y : D) => L (f y)) x‖ ≤ ‖L‖ * ‖iteratedFDeriv ℝ m f x‖

theorem NavierStokes.ResidualStability.AllJetsFlat.linear_map {D : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {l : Filter D} {q : D → ℝ} {f : D → E} {U : Set D} (hf : AllJetsFlat l q f) (L : E →L[ℝ] F) (hU : IsOpen U) (hl : ∀ᶠ (x : D) in l, x ∈ U) (hs : ContDiffOn ℝ (↑⊤) f U) : AllJetsFlat l q fun (x : D) => L (f x)

theorem NavierStokes.ResidualStability.AllJetsGrowth.linear_map {D : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {l : Filter D} {q : D → ℝ} {f : D → E} {U : Set D} (hf : AllJetsGrowth l q f) (L : E →L[ℝ] F) (hU : IsOpen U) (hl : ∀ᶠ (x : D) in l, x ∈ U) (hs : ContDiffOn ℝ (↑⊤) f U) : AllJetsGrowth l q fun (x : D) => L (f x)

theorem NavierStokes.ResidualStability.AllJetsFlat.add {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {l : Filter D} {q : D → ℝ} {f : D → E} {U : Set D} {g : D → E} (hf : AllJetsFlat l q f) (hg : AllJetsFlat l q g) (hU : IsOpen U) (hl : ∀ᶠ (x : D) in l, x ∈ U) (hsf : ContDiffOn ℝ (↑⊤) f U) (hsg : ContDiffOn ℝ (↑⊤) g U) : AllJetsFlat l q fun (x : D) => f x + g x

theorem NavierStokes.ResidualStability.AllJetsFlat.neg {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {l : Filter D} {q : D → ℝ} {f : D → E} {U : Set D} (hf : AllJetsFlat l q f) (hU : IsOpen U) (hl : ∀ᶠ (x : D) in l, x ∈ U) (hs : ContDiffOn ℝ (↑⊤) f U) : AllJetsFlat l q fun (x : D) => -f x

theorem NavierStokes.ResidualStability.AllJetsFlat.sub {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {l : Filter D} {q : D → ℝ} {f : D → E} {U : Set D} {g : D → E} (hf : AllJetsFlat l q f) (hg : AllJetsFlat l q g) (hU : IsOpen U) (hl : ∀ᶠ (x : D) in l, x ∈ U) (hsf : ContDiffOn ℝ (↑⊤) f U) (hsg : ContDiffOn ℝ (↑⊤) g U) : AllJetsFlat l q fun (x : D) => f x - g x

theorem NavierStokes.ResidualStability.AllJetsFlat.zero {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {l : Filter D} {q : D → ℝ} : AllJetsFlat l q fun (x : D) => 0

theorem NavierStokes.ResidualStability.AllJetsFlat.sum {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {l : Filter D} {q : D → ℝ} {U : Set D} {ι : Type u_5} (s : Finset ι) (f : ι → D → E) (hU : IsOpen U) (hl : ∀ᶠ (x : D) in l, x ∈ U) (hs : ∀ i ∈ s, ContDiffOn ℝ (↑⊤) (f i) U) (hf : ∀ i ∈ s, AllJetsFlat l q (f i)) : AllJetsFlat l q fun (x : D) => ∑ i ∈ s, f i x

theorem NavierStokes.ResidualStability.AllJetsFlat.bilinear_growth_left {D : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {l : Filter D} {q : D → ℝ} {f : D → E} {g : D → F} {U : Set D} (hg : AllJetsFlat l q g) (hf : AllJetsGrowth l q f) (L : E →L[ℝ] F →L[ℝ] G) (hU : IsOpen U) (hl : ∀ᶠ (x : D) in l, x ∈ U) (hq : ∀ᶠ (x : D) in l, q x ≠ 0) (hsf : ContDiffOn ℝ (↑⊤) f U) (hsg : ContDiffOn ℝ (↑⊤) g U) : AllJetsFlat l q fun (x : D) => (L (f x)) (g x)

Leibniz plus a fixed power loss in one factor gives flatness of the actual bilinear product. The bound uses only jets through the requested order.

theorem NavierStokes.ResidualStability.AllJetsFlat.bilinear_growth_right {D : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {l : Filter D} {q : D → ℝ} {f : D → E} {g : D → F} {U : Set D} (hf : AllJetsFlat l q f) (hg : AllJetsGrowth l q g) (L : E →L[ℝ] F →L[ℝ] G) (hU : IsOpen U) (hl : ∀ᶠ (x : D) in l, x ∈ U) (hq : ∀ᶠ (x : D) in l, q x ≠ 0) (hsf : ContDiffOn ℝ (↑⊤) f U) (hsg : ContDiffOn ℝ (↑⊤) g U) : AllJetsFlat l q fun (x : D) => (L (f x)) (g x)

noncomputable def NavierStokes.ResidualStability.spaceRestriction (V : Type u_2) [NormedAddCommGroup V] [NormedSpace ℝ V] : (ProblemStatement.SpaceTime →L[ℝ] V) →L[ℝ] ProblemStatement.Space →L[ℝ] V

Restrict a full spacetime derivative to the spatial directions.

Equations

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

theorem NavierStokes.ResidualStability.space_fderiv_eq_full {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : ProblemStatement.SpaceTime → V} {z : ProblemStatement.SpaceTime} (hf : DifferentiableAt ℝ f z) : fderiv ℝ (fun (y : ProblemStatement.Space) => f (z.1, y)) z.2 = (spaceRestriction V) (fderiv ℝ f z)

theorem NavierStokes.ResidualStability.temporalDerivative_eq_full {f : ProblemStatement.VelocityField} {z : ProblemStatement.SpaceTime} (hf : DifferentiableAt ℝ f z) : ProblemStatement.temporalDerivative f z.1 z.2 = (fderiv ℝ f z) (1, 0)

theorem NavierStokes.ResidualStability.AllJetsFlat.space_fderiv {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {l : Filter ProblemStatement.SpaceTime} {q : ProblemStatement.SpaceTime → ℝ} {U : Set ProblemStatement.SpaceTime} {f : ProblemStatement.SpaceTime → V} (hf : AllJetsFlat l q f) (hU : IsOpen U) (hl : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, z ∈ U) (hs : ContDiffOn ℝ (↑⊤) f U) : AllJetsFlat l q fun (z : ProblemStatement.SpaceTime) => _root_.fderiv ℝ (fun (y : ProblemStatement.Space) => f (z.1, y)) z.2

theorem NavierStokes.ResidualStability.AllJetsGrowth.space_fderiv {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {l : Filter ProblemStatement.SpaceTime} {q : ProblemStatement.SpaceTime → ℝ} {U : Set ProblemStatement.SpaceTime} {f : ProblemStatement.SpaceTime → V} (hf : AllJetsGrowth l q f) (hU : IsOpen U) (hl : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, z ∈ U) (hs : ContDiffOn ℝ (↑⊤) f U) : AllJetsGrowth l q fun (z : ProblemStatement.SpaceTime) => _root_.fderiv ℝ (fun (y : ProblemStatement.Space) => f (z.1, y)) z.2

theorem NavierStokes.ResidualStability.AllJetsFlat.temporalDerivative {l : Filter ProblemStatement.SpaceTime} {q : ProblemStatement.SpaceTime → ℝ} {U : Set ProblemStatement.SpaceTime} {f : ProblemStatement.VelocityField} (hf : AllJetsFlat l q f) (hU : IsOpen U) (hl : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, z ∈ U) (hs : ContDiffOn ℝ (↑⊤) f U) : AllJetsFlat l q fun (z : ProblemStatement.SpaceTime) => ProblemStatement.temporalDerivative f z.1 z.2

theorem NavierStokes.ResidualStability.AllJetsFlat.pressureGradient {l : Filter ProblemStatement.SpaceTime} {q : ProblemStatement.SpaceTime → ℝ} {U : Set ProblemStatement.SpaceTime} {p : ProblemStatement.PressureField} (hp : AllJetsFlat l q p) (hU : IsOpen U) (hl : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, z ∈ U) (hs : ContDiffOn ℝ (↑⊤) p U) : AllJetsFlat l q fun (z : ProblemStatement.SpaceTime) => ProblemStatement.pressureGradient p z.1 z.2

theorem NavierStokes.ResidualStability.AllJetsFlat.spatialLaplacian {l : Filter ProblemStatement.SpaceTime} {q : ProblemStatement.SpaceTime → ℝ} {U : Set ProblemStatement.SpaceTime} {f : ProblemStatement.VelocityField} (hf : AllJetsFlat l q f) (hU : IsOpen U) (hl : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, z ∈ U) (hs : ContDiffOn ℝ (↑⊤) f U) : AllJetsFlat l q fun (z : ProblemStatement.SpaceTime) => ProblemStatement.spatialLaplacian f z.1 z.2

theorem NavierStokes.ResidualStability.spatialSlice_differentiable {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {U : Set ProblemStatement.SpaceTime} {f : ProblemStatement.SpaceTime → V} (hU : IsOpen U) (hf : ContDiffOn ℝ (↑⊤) f U) {z : ProblemStatement.SpaceTime} (hz : z ∈ U) : DifferentiableAt ℝ (fun (y : ProblemStatement.Space) => f (z.1, y)) z.2

theorem NavierStokes.ResidualStability.timeSlice_differentiable {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {U : Set ProblemStatement.SpaceTime} {f : ProblemStatement.SpaceTime → V} (hU : IsOpen U) (hf : ContDiffOn ℝ (↑⊤) f U) {z : ProblemStatement.SpaceTime} (hz : z ∈ U) : DifferentiableAt ℝ (fun (t : ℝ) => f (t, z.2)) z.1

theorem NavierStokes.ResidualStability.spatialLaplacian_add_on {U : Set ProblemStatement.SpaceTime} {u w : ProblemStatement.VelocityField} (hU : IsOpen U) (hu : ContDiffOn ℝ (↑⊤) u U) (hw : ContDiffOn ℝ (↑⊤) w U) {z : ProblemStatement.SpaceTime} (hz : z ∈ U) : ProblemStatement.spatialLaplacian (fun (y : ProblemStatement.SpaceTime) => u y + w y) z.1 z.2 = ProblemStatement.spatialLaplacian u z.1 z.2 + ProblemStatement.spatialLaplacian w z.1 z.2

Local version of the Laplacian additivity used in ResidualCalculus. Only smoothness on the open domain is needed, not on an entire spatial slice.

theorem NavierStokes.ResidualStability.residual_add_sub_on {U : Set ProblemStatement.SpaceTime} {u w : ProblemStatement.VelocityField} {p r : ProblemStatement.PressureField} (hU : IsOpen U) (hu : ContDiffOn ℝ (↑⊤) u U) (hw : ContDiffOn ℝ (↑⊤) w U) (hp : ContDiffOn ℝ (↑⊤) p U) (hr : ContDiffOn ℝ (↑⊤) r U) {z : ProblemStatement.SpaceTime} (hz : z ∈ U) : ProblemStatement.navierStokesResidual (fun (y : ProblemStatement.SpaceTime) => u y + w y) (fun (y : ProblemStatement.SpaceTime) => p y + r y) z.1 z.2 - ProblemStatement.navierStokesResidual u p z.1 z.2 = ProblemStatement.temporalDerivative w z.1 z.2 - ProblemStatement.spatialLaplacian w z.1 z.2 + ProblemStatement.pressureGradient r z.1 z.2 + (ProblemStatement.spatialDerivative u z.1 z.2) (w z) + (ProblemStatement.spatialDerivative w z.1 z.2) (u z) + (ProblemStatement.spatialDerivative w z.1 z.2) (w z)

The exact perturbation identity now holds on an arbitrary open spacetime domain, using the concrete first-order identities from ResidualCalculus.

noncomputable def NavierStokes.ResidualStability.residualDifference (u w : ProblemStatement.VelocityField) (p r : ProblemStatement.PressureField) : ProblemStatement.VelocityField

The difference of the two actual viscosity-one Navier--Stokes residuals.

Equations

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

theorem NavierStokes.ResidualStability.allJetsFlat_residualDifference {l : Filter ProblemStatement.SpaceTime} {q : ProblemStatement.SpaceTime → ℝ} {U : Set ProblemStatement.SpaceTime} {u w : ProblemStatement.VelocityField} {p r : ProblemStatement.PressureField} (hU : IsOpen U) (hl : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, z ∈ U) (hq : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, q z ≠ 0) (hu : ContDiffOn ℝ (↑⊤) u U) (hw : ContDiffOn ℝ (↑⊤) w U) (hp : ContDiffOn ℝ (↑⊤) p U) (hr : ContDiffOn ℝ (↑⊤) r U) (hgrowth : AllJetsGrowth l q u) (hwflat : AllJetsFlat l q w) (hrflat : AllJetsFlat l q r) : AllJetsFlat l q (residualDifference u w p r)

Flat perturbations preserve all-jet residual flatness relative to any smooth background with fixed-power jet growth. No residual estimate is an input. The linear terms use at most two extra derivatives of the perturbation; the transport products use at most one extra derivative.

theorem NavierStokes.ResidualStability.norm_jet_add_le {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {f g : D → E} (hU : IsOpen U) (hf : ContDiffOn ℝ (↑⊤) f U) (hg : ContDiffOn ℝ (↑⊤) g U) {x : D} (hx : x ∈ U) (m : ℕ) : ‖iteratedFDeriv ℝ m (fun (y : D) => f y + g y) x‖ ≤ ‖iteratedFDeriv ℝ m f x‖ + ‖iteratedFDeriv ℝ m g x‖

theorem NavierStokes.ResidualStability.norm_jet_neg {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (f : D → E) (x : D) (m : ℕ) : ‖iteratedFDeriv ℝ m (fun (y : D) => -f y) x‖ = ‖iteratedFDeriv ℝ m f x‖

theorem NavierStokes.ResidualStability.norm_jet_sub_le {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set D} {f g : D → E} (hU : IsOpen U) (hf : ContDiffOn ℝ (↑⊤) f U) (hg : ContDiffOn ℝ (↑⊤) g U) {x : D} (hx : x ∈ U) (m : ℕ) : ‖iteratedFDeriv ℝ m (fun (y : D) => f y - g y) x‖ ≤ ‖iteratedFDeriv ℝ m f x‖ + ‖iteratedFDeriv ℝ m g x‖

theorem NavierStokes.ResidualStability.norm_jet_linear_map_fderiv {D : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (L : (D →L[ℝ] E) →L[ℝ] F) {U : Set D} {f : D → E} (hU : IsOpen U) (hf : ContDiffOn ℝ (↑⊤) f U) {x : D} (hx : x ∈ U) (m : ℕ) : ‖iteratedFDeriv ℝ m (fun (y : D) => L (fderiv ℝ f y)) x‖ ≤ ‖L‖ * ‖iteratedFDeriv ℝ (m + 1) f x‖

theorem NavierStokes.ResidualStability.norm_jet_bilinear_bound {D : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (L : E →L[ℝ] F →L[ℝ] G) {U : Set D} {f : D → E} {g : D → F} (hU : IsOpen U) (hf : ContDiffOn ℝ (↑⊤) f U) (hg : ContDiffOn ℝ (↑⊤) g U) {x : D} (hx : x ∈ U) (m : ℕ) {A B : ℝ} (hA : ∀ k ≤ m, ‖iteratedFDeriv ℝ k f x‖ ≤ A) (hB : ∀ k ≤ m, ‖iteratedFDeriv ℝ k g x‖ ≤ B) : ‖iteratedFDeriv ℝ m (fun (y : D) => (L (f y)) (g y)) x‖ ≤ ‖L‖ * 2 ^ m * A * B

The pointwise finite-order form of the Leibniz estimate. The majorants need only bound jets at this point; they may depend on the point and stage.

@[instance_reducible]

noncomputable def NavierStokes.ResidualStability.instResidualStability1 : NormedAddCommGroup (ProblemStatement.SpaceTime →L[ℝ] ProblemStatement.SpaceTime →L[ℝ] ProblemStatement.Space)

Cache the standard NormedAddCommGroup (SpaceTime →L[ℝ] SpaceTime →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• NavierStokes.ResidualStability.instResidualStability1 = inferInstance

@[instance_reducible]

noncomputable def NavierStokes.ResidualStability.instResidualStability2 : NormedSpace ℝ (ProblemStatement.SpaceTime →L[ℝ] ProblemStatement.SpaceTime →L[ℝ] ProblemStatement.Space)

Cache the standard NormedSpace ℝ (SpaceTime →L[ℝ] SpaceTime →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• NavierStokes.ResidualStability.instResidualStability2 = inferInstance

theorem NavierStokes.ResidualStability.norm_iteratedFDeriv_spatialCurl_le {U : Set ProblemStatement.SpaceTime} {A : ProblemStatement.VelocityField} (hU : IsOpen U) (hA : ContDiffOn ℝ (↑⊤) A U) {z : ProblemStatement.SpaceTime} (hz : z ∈ U) (m : ℕ) : ‖iteratedFDeriv ℝ m (SpatialCurl.spatialCurl A) z‖ ≤ ‖SpatialCurl.curlLinear ∘SL spaceRestriction ProblemStatement.Space‖ * ‖iteratedFDeriv ℝ (m + 1) A z‖

noncomputable def NavierStokes.ResidualStability.timeJet : (ProblemStatement.SpaceTime →L[ℝ] ProblemStatement.Space) →L[ℝ] ProblemStatement.Space

Time jet, given by ContinuousLinearMap.apply ℝ Space (1, 0).

Equations

• NavierStokes.ResidualStability.timeJet = (ContinuousLinearMap.apply ℝ NavierStokes.ProblemStatement.Space) (1, 0)

noncomputable def NavierStokes.ResidualStability.laplaceJet : (ProblemStatement.SpaceTime →L[ℝ] ProblemStatement.SpaceTime →L[ℝ] ProblemStatement.Space) →L[ℝ] ProblemStatement.Space

Laplace jet as an element of (SpaceTime →L[ℝ] SpaceTime →L[ℝ] Space) →L[ℝ] Space.

Equations

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

noncomputable def NavierStokes.ResidualStability.pressureJet : (ProblemStatement.SpaceTime →L[ℝ] ℝ) →L[ℝ] ProblemStatement.Space

Pressure jet as an element of (SpaceTime →L[ℝ] ℝ) →L[ℝ] Space.

Equations

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

@[simp]

theorem NavierStokes.ResidualStability.laplaceJet_apply (L : ProblemStatement.SpaceTime →L[ℝ] ProblemStatement.SpaceTime →L[ℝ] ProblemStatement.Space) : laplaceJet L = ∑ i : Fin 3, (L (0, ProblemStatement.coordinateVector i)) (0, ProblemStatement.coordinateVector i)

@[simp]

theorem NavierStokes.ResidualStability.pressureJet_apply (L : ProblemStatement.SpaceTime →L[ℝ] ℝ) : pressureJet L = ∑ i : Fin 3, L (0, ProblemStatement.coordinateVector i) • ProblemStatement.coordinateVector i

theorem NavierStokes.ResidualStability.spatialLaplacian_eq_full {U : Set ProblemStatement.SpaceTime} {w : ProblemStatement.VelocityField} (hU : IsOpen U) (hw : ContDiffOn ℝ (↑⊤) w U) {z : ProblemStatement.SpaceTime} (hz : z ∈ U) : ProblemStatement.spatialLaplacian w z.1 z.2 = laplaceJet (fderiv ℝ (fderiv ℝ w) z)

theorem NavierStokes.ResidualStability.pressureGradient_eq_full {U : Set ProblemStatement.SpaceTime} {r : ProblemStatement.PressureField} (hU : IsOpen U) (hr : ContDiffOn ℝ (↑⊤) r U) {z : ProblemStatement.SpaceTime} (hz : z ∈ U) : ProblemStatement.pressureGradient r z.1 z.2 = pressureJet (fderiv ℝ r z)

noncomputable def NavierStokes.ResidualStability.residualJetExpression (u w : ProblemStatement.VelocityField) (r : ProblemStatement.PressureField) : ProblemStatement.VelocityField

Residual jet expression as an element of VelocityField.

Equations

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

theorem NavierStokes.ResidualStability.residualDifference_eq_jetExpression {U : Set ProblemStatement.SpaceTime} {u w : ProblemStatement.VelocityField} {p r : ProblemStatement.PressureField} (hU : IsOpen U) (hu : ContDiffOn ℝ (↑⊤) u U) (hw : ContDiffOn ℝ (↑⊤) w U) (hp : ContDiffOn ℝ (↑⊤) p U) (hr : ContDiffOn ℝ (↑⊤) r U) : Set.EqOn (residualDifference u w p r) (residualJetExpression u w r) U

theorem NavierStokes.ResidualStability.residualDifference_jet_bound {U : Set ProblemStatement.SpaceTime} {u w : ProblemStatement.VelocityField} {p r : ProblemStatement.PressureField} (hU : IsOpen U) (hu : ContDiffOn ℝ (↑⊤) u U) (hw : ContDiffOn ℝ (↑⊤) w U) (hp : ContDiffOn ℝ (↑⊤) p U) (hr : ContDiffOn ℝ (↑⊤) r U) {z : ProblemStatement.SpaceTime} (hz : z ∈ U) (m : ℕ) {A W P : ℝ} (huBound : ∀ k ≤ m + 1, ‖iteratedFDeriv ℝ k u z‖ ≤ A) (hwBound : ∀ k ≤ m + 2, ‖iteratedFDeriv ℝ k w z‖ ≤ W) (hrBound : ∀ k ≤ m + 1, ‖iteratedFDeriv ℝ k r z‖ ≤ P) : ‖iteratedFDeriv ℝ m (residualDifference u w p r) z‖ ≤ ‖timeJet‖ * W + ‖laplaceJet‖ * W + ‖pressureJet‖ * P + ‖spaceRestriction ProblemStatement.Space‖ * 2 ^ m * A * W + ‖spaceRestriction ProblemStatement.Space‖ * 2 ^ m * W * A + ‖spaceRestriction ProblemStatement.Space‖ * 2 ^ m * W * W

Quantitative fixed-order stability, with only pointwise hypotheses on the actual jets. The background needs m+1 derivatives, the velocity perturbation m+2, and the pressure perturbation m+1. The three majorants may depend on the point and on a truncation stage. Every displayed operator norm is fixed independently of the fields, stage, and physical scale.

def NavierStokes.ResidualStability.scaleFilter (U : Set ProblemStatement.SpaceTime) (q : ProblemStatement.SpaceTime → ℝ) : Filter ProblemStatement.SpaceTime

Approach q = 0 through positive scales while staying in the domain.

Equations

• NavierStokes.ResidualStability.scaleFilter U q = Filter.principal U ⊓ Filter.comap q (nhdsWithin 0 (Set.Ioi 0))

theorem NavierStokes.ResidualStability.eventually_mem_scaleFilter (U : Set ProblemStatement.SpaceTime) (q : ProblemStatement.SpaceTime → ℝ) : ∀ᶠ (z : ProblemStatement.SpaceTime) in scaleFilter U q, z ∈ U

theorem NavierStokes.ResidualStability.tendsto_scaleFilter (U : Set ProblemStatement.SpaceTime) (q : ProblemStatement.SpaceTime → ℝ) : Filter.Tendsto q (scaleFilter U q) (nhdsWithin 0 (Set.Ioi 0))

theorem NavierStokes.ResidualStability.residualDifference_flat_at_scale {U : Set ProblemStatement.SpaceTime} {q : ProblemStatement.SpaceTime → ℝ} {u w : ProblemStatement.VelocityField} {p r : ProblemStatement.PressureField} (hU : IsOpen U) (hq : ∀ z ∈ U, 0 < q z) (hu : ContDiffOn ℝ (↑⊤) u U) (hw : ContDiffOn ℝ (↑⊤) w U) (hp : ContDiffOn ℝ (↑⊤) p U) (hr : ContDiffOn ℝ (↑⊤) r U) (hgrowth : AllJetsGrowth (scaleFilter U q) q u) (hwflat : AllJetsFlat (scaleFilter U q) q w) (hrflat : AllJetsFlat (scaleFilter U q) q r) : AllJetsFlat (scaleFilter U q) q (residualDifference u w p r)

Domain/scale form of the actual nonlinear stability theorem. All asymptotics concern the displayed norms of actual physical derivatives.