Residual flatness from quantitative finite-stage data

The finite approximation used in the proof depends on the requested jet order and decay power. Stage constants and neighborhoods may depend on that stage; the loss of powers in the background estimates must not. All jet estimates refer to actual iterated Fréchet derivatives of the displayed fields.

@[instance_reducible]

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

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

Equations

• NavierStokes.DiagonalResidual.instDiagonalResidual1 = inferInstance

@[instance_reducible]

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

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

Equations

• NavierStokes.DiagonalResidual.instDiagonalResidual2 = inferInstance

def NavierStokes.DiagonalResidual.JetRate {D : Type u_1} {V : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup V] [NormedSpace ℝ V] (l : Filter D) (q : D → ℝ) (f : D → V) (m : ℕ) (r : ℝ) : Prop

A single quantitative order for one actual derivative.

Equations

• NavierStokes.DiagonalResidual.JetRate l q f m r = ∃ (C : ℝ), 0 ≤ C ∧ ∀ᶠ (x : D) in l, ‖iteratedFDeriv ℝ m f x‖ ≤ C * q x ^ r

def NavierStokes.DiagonalResidual.FiniteJetRate {D : Type u_1} {V : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup V] [NormedSpace ℝ V] (l : Filter D) (q : D → ℝ) (f : D → V) (M : ℕ) (r : ℝ) : Prop

A common constant and neighborhood for a finite list of actual jets.

Equations

• NavierStokes.DiagonalResidual.FiniteJetRate l q f M r = ∃ (C : ℝ), 0 ≤ C ∧ ∀ᶠ (x : D) in l, ∀ m ≤ M, ‖iteratedFDeriv ℝ m f x‖ ≤ C * q x ^ r

theorem NavierStokes.DiagonalResidual.JetRate.weaken {D : Type u_1} {V : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup V] [NormedSpace ℝ V] {l : Filter D} {q : D → ℝ} {f : D → V} {m : ℕ} {r s : ℝ} (hf : JetRate l q f m r) (hq : ∀ᶠ (x : D) in l, 0 < q x ∧ q x ≤ 1) (hsr : s ≤ r) : JetRate l q f m s

theorem NavierStokes.DiagonalResidual.finiteJetRate_of_jetRate {D : Type u_1} {V : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup V] [NormedSpace ℝ V] {l : Filter D} {q : D → ℝ} {f : D → V} {r : ℝ} (hq : ∀ᶠ (x : D) in l, 0 < q x) (M : ℕ) : (∀ m ≤ M, JetRate l q f m r) → FiniteJetRate l q f M r

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

theorem NavierStokes.DiagonalResidual.JetRate.congr_on {D : Type u_1} {V : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup V] [NormedSpace ℝ V] {l : Filter D} {q : D → ℝ} {f g : D → V} {m : ℕ} {r : ℝ} {U : Set D} (hf : JetRate l q f m r) (hU : IsOpen U) (hlU : ∀ᶠ (x : D) in l, x ∈ U) (hfg : Set.EqOn f g U) : JetRate l q g m r

def NavierStokes.DiagonalResidual.maxJetLoss (L : ℕ → ℝ) (M : ℕ) : ℝ

A nonnegative upper bound for every loss in a finite derivative list.

Equations

• NavierStokes.DiagonalResidual.maxJetLoss L M = max 0 ((Finset.range (M + 1)).sup' ⋯ L)

theorem NavierStokes.DiagonalResidual.maxJetLoss_nonneg (L : ℕ → ℝ) (M : ℕ) : 0 ≤ maxJetLoss L M

theorem NavierStokes.DiagonalResidual.le_maxJetLoss (L : ℕ → ℝ) {m M : ℕ} (hm : m ≤ M) : L m ≤ maxJetLoss L M

theorem NavierStokes.DiagonalResidual.power_product_le {q A B r s n : ℝ} (hq : 0 < q) (hq1 : q ≤ 1) (hA : 0 ≤ A) (hB : 0 ≤ B) (hn : n ≤ r + s) : A * q ^ r * (B * q ^ s) ≤ A * B * q ^ n

theorem NavierStokes.DiagonalResidual.perturbation_majorant_le {q A W P b n t d p k : ℝ} (hq : 0 < q) (hq1 : q ≤ 1) (hA : 0 ≤ A) (hW : 0 ≤ W) (hP : 0 ≤ P) (hb : 0 ≤ b) (hn : 0 ≤ n) (ht : 0 ≤ t) (hd : 0 ≤ d) (hp : 0 ≤ p) (hk : 0 ≤ k) : t * (W * q ^ (n + b)) + d * (W * q ^ (n + b)) + p * (P * q ^ (n + b)) + k * (A * q ^ (-b)) * (W * q ^ (n + b)) + k * (W * q ^ (n + b)) * (A * q ^ (-b)) + k * (W * q ^ (n + b)) * (W * q ^ (n + b)) ≤ (t * W + d * W + p * P + k * A * W + k * W * A + k * W * W) * q ^ n

A scalar version of the six-term residual estimate. Taking the tail order at least n+b absorbs background growth q^(-b) and the quadratic tail term, with constants allowed to depend on the chosen stage.

theorem NavierStokes.DiagonalResidual.residualDifference_jetRate {U : Set ProblemStatement.SpaceTime} {l : Filter ProblemStatement.SpaceTime} {q : ProblemStatement.SpaceTime → ℝ} {u w : ProblemStatement.VelocityField} {p r : ProblemStatement.PressureField} (hU : IsOpen U) (hlU : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, z ∈ U) (hq : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, 0 < q z ∧ q z ≤ 1) (hu : ContDiffOn ℝ (↑⊤) u U) (hw : ContDiffOn ℝ (↑⊤) w U) (hp : ContDiffOn ℝ (↑⊤) p U) (hr : ContDiffOn ℝ (↑⊤) r U) (m : ℕ) {b n : ℝ} (hb : 0 ≤ b) (hn : 0 ≤ n) (hbg : FiniteJetRate l q u (m + 1) (-b)) (hwu : FiniteJetRate l q w (m + 2) (n + b)) (hpr : FiniteJetRate l q r (m + 1) (n + b)) : JetRate l q (ResidualStability.residualDifference u w p r) m n

Quantitative residual stability packaged as an eventual power estimate. The background exponent b is paid for by selecting tail order n+b.

theorem NavierStokes.DiagonalResidual.residual_jetRate_of_stages {U : Set ProblemStatement.SpaceTime} {l : Filter ProblemStatement.SpaceTime} {q : ProblemStatement.SpaceTime → ℝ} {u : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} {uStage : ℕ → ProblemStatement.VelocityField} {pStage : ℕ → ProblemStatement.PressureField} {g Lbg Ltail Lres : ℕ → ℝ} (hU : IsOpen U) (hlU : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, z ∈ U) (hq : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, 0 < q z ∧ q z ≤ 1) (hu : ContDiffOn ℝ (↑⊤) u U) (hp : ContDiffOn ℝ (↑⊤) p U) (hus : ∀ (J : ℕ), ContDiffOn ℝ (↑⊤) (uStage J) U) (hps : ∀ (J : ℕ), ContDiffOn ℝ (↑⊤) (pStage J) U) (hg : Filter.Tendsto g Filter.atTop Filter.atTop) (hbg : ∀ (J m : ℕ), JetRate l q (uStage J) m (-Lbg m)) (htu : ∀ (J m : ℕ), m ≤ J → JetRate l q (fun (z : ProblemStatement.SpaceTime) => u z - uStage J z) m (g J - Ltail m)) (htp : ∀ (J m : ℕ), m ≤ J → JetRate l q (fun (z : ProblemStatement.SpaceTime) => p z - pStage J z) m (g J - Ltail m)) (hres : ∀ (J m : ℕ), JetRate l q (fun (z : ProblemStatement.SpaceTime) => ProblemStatement.navierStokesResidual (uStage J) (pStage J) z.1 z.2) m (g J - Lres m)) (m : ℕ) (n : ℝ) (hn : 0 ≤ n) : JetRate l q (fun (z : ProblemStatement.SpaceTime) => ProblemStatement.navierStokesResidual u p z.1 z.2) m n

For each requested order choose a single sufficiently advanced stage. Only the jets through m+2 of its tail are used, and the background power losses are independent of the stage. Constants and neighborhoods may depend on the stage and derivative order.

theorem NavierStokes.DiagonalResidual.allJetsFlat_residual_of_stages {U : Set ProblemStatement.SpaceTime} {l : Filter ProblemStatement.SpaceTime} {q : ProblemStatement.SpaceTime → ℝ} {u : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} {uStage : ℕ → ProblemStatement.VelocityField} {pStage : ℕ → ProblemStatement.PressureField} {g Lbg Ltail Lres : ℕ → ℝ} (hU : IsOpen U) (hlU : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, z ∈ U) (hq : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, 0 < q z ∧ q z ≤ 1) (hu : ContDiffOn ℝ (↑⊤) u U) (hp : ContDiffOn ℝ (↑⊤) p U) (hus : ∀ (J : ℕ), ContDiffOn ℝ (↑⊤) (uStage J) U) (hps : ∀ (J : ℕ), ContDiffOn ℝ (↑⊤) (pStage J) U) (hg : Filter.Tendsto g Filter.atTop Filter.atTop) (hbg : ∀ (J m : ℕ), JetRate l q (uStage J) m (-Lbg m)) (htu : ∀ (J m : ℕ), m ≤ J → JetRate l q (fun (z : ProblemStatement.SpaceTime) => u z - uStage J z) m (g J - Ltail m)) (htp : ∀ (J m : ℕ), m ≤ J → JetRate l q (fun (z : ProblemStatement.SpaceTime) => p z - pStage J z) m (g J - Ltail m)) (hres : ∀ (J m : ℕ), JetRate l q (fun (z : ProblemStatement.SpaceTime) => ProblemStatement.navierStokesResidual (uStage J) (pStage J) z.1 z.2) m (g J - Lres m)) : ResidualStability.AllJetsFlat l q fun (z : ProblemStatement.SpaceTime) => ProblemStatement.navierStokesResidual u p z.1 z.2

Every actual residual jet is flat. This follows by choosing a different finite stage for each requested derivative and decay order; no fixed tail is assumed or proved flat to all orders.

theorem NavierStokes.DiagonalResidual.jetRate_diagonal_tail {D : Type u_1} {V : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℕ → ℝ} (ha : Filter.Tendsto a Filter.atTop Filter.atTop) {q : D → ℝ} {A : ℕ → D → V} {g L : ℕ → ℝ} {U : Set D} {l : Filter D} (hU : IsOpen U) (hq : ContDiffOn ℝ (↑⊤) q U) (hA : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (A j) U) (hg : Monotone g) (hb : DiagonalJetBounds.CutStageBounds a q A g L U) (hlU : ∀ᶠ (x : D) in l, x ∈ U) (hlq : ∀ᶠ (x : D) in l, 0 < q x ∧ q x ≤ 1) (hqzero : Filter.Tendsto q l (nhds 0)) (J m : ℕ) (hm : m ≤ J + 3) : JetRate l q (fun (x : D) => SolenoidalDiagonal.potentialSum a q A x - DiagonalJetBounds.uncutPrefix A (J + 1) x) m (g (J + 1) - L m)

The actual diagonal tail provides the JetRate used in the residual theorem. This is a fixed-prefix rate, not all-order flatness of that tail.

theorem NavierStokes.DiagonalResidual.JetRate.spatialCurl {U : Set ProblemStatement.SpaceTime} {l : Filter ProblemStatement.SpaceTime} {q : ProblemStatement.SpaceTime → ℝ} {A : ProblemStatement.VelocityField} {m : ℕ} {r : ℝ} (hbound : JetRate l q A (m + 1) r) (hU : IsOpen U) (hlU : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, z ∈ U) (hA : ContDiffOn ℝ (↑⊤) A U) : JetRate l q (SpatialCurl.spatialCurl A) m r

A spatial curl costs one actual full derivative and a fixed operator norm, independently of the chosen diagonal prefix.

theorem NavierStokes.DiagonalResidual.spatialCurl_sub_on {U : Set ProblemStatement.SpaceTime} {A B : ProblemStatement.VelocityField} (hU : IsOpen U) (hA : ContDiffOn ℝ (↑⊤) A U) (hB : ContDiffOn ℝ (↑⊤) B U) : Set.EqOn (SpatialCurl.spatialCurl fun (z : ProblemStatement.SpaceTime) => A z - B z) (fun (z : ProblemStatement.SpaceTime) => SpatialCurl.spatialCurl A z - SpatialCurl.spatialCurl B z) U

theorem NavierStokes.DiagonalResidual.jetRate_diagonal_velocity_tail {a : ℕ → ℝ} (ha : Filter.Tendsto a Filter.atTop Filter.atTop) {q : ProblemStatement.SpaceTime → ℝ} {A : ℕ → ProblemStatement.VelocityField} {g L : ℕ → ℝ} {U : Set ProblemStatement.SpaceTime} {l : Filter ProblemStatement.SpaceTime} (hU : IsOpen U) (hqpos : ∀ z ∈ U, 0 < q z) (hq : ContDiffOn ℝ (↑⊤) q U) (hA : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (A j) U) (hg : Monotone g) (hb : DiagonalJetBounds.CutStageBounds a q A g L U) (hlU : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, z ∈ U) (hlq : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, 0 < q z ∧ q z ≤ 1) (hqzero : Filter.Tendsto q l (nhds 0)) (J m : ℕ) (hm : m + 1 ≤ J + 3) : JetRate l q (fun (z : ProblemStatement.SpaceTime) => SolenoidalDiagonal.velocitySum a q A z - SpatialCurl.spatialCurl (DiagonalJetBounds.uncutPrefix A (J + 1)) z) m (g (J + 1) - L (m + 1))

The velocity tail of the actual solenoidal diagonal construction has a fixed-prefix jet rate, obtained from one higher potential derivative.

theorem NavierStokes.DiagonalResidual.allJetsFlat_diagonal_residual {a : ℕ → ℝ} (ha : Filter.Tendsto a Filter.atTop Filter.atTop) {q : ProblemStatement.SpaceTime → ℝ} {A : ℕ → ProblemStatement.VelocityField} {P : ℕ → ProblemStatement.PressureField} {g LA LP Lbg Lres : ℕ → ℝ} {U : Set ProblemStatement.SpaceTime} {l : Filter ProblemStatement.SpaceTime} (hU : IsOpen U) (hqpos : ∀ z ∈ U, 0 < q z) (hq : ContDiffOn ℝ (↑⊤) q U) (hA : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (A j) U) (hP : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (P j) U) (hgmono : Monotone g) (hgtop : Filter.Tendsto g Filter.atTop Filter.atTop) (hbA : DiagonalJetBounds.CutStageBounds a q A g LA U) (hbP : DiagonalJetBounds.CutStageBounds a q P g LP U) (hlU : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, z ∈ U) (hqzero : Filter.Tendsto q l (nhds 0)) (hbg : ∀ (J m : ℕ), JetRate l q (SpatialCurl.spatialCurl (DiagonalJetBounds.uncutPrefix A (J + 1))) m (-Lbg m)) (hres : ∀ (J m : ℕ), JetRate l q (fun (z : ProblemStatement.SpaceTime) => ProblemStatement.navierStokesResidual (SpatialCurl.spatialCurl (DiagonalJetBounds.uncutPrefix A (J + 1))) (DiagonalJetBounds.uncutPrefix P (J + 1)) z.1 z.2) m (g J - Lres m)) : ResidualStability.AllJetsFlat l q fun (z : ProblemStatement.SpaceTime) => ProblemStatement.navierStokesResidual (SolenoidalDiagonal.velocitySum a q A) (SolenoidalDiagonal.potentialSum a q P) z.1 z.2

Explicit diagonal-sum corollary. Velocity is the curl of the constructed potential sum and pressure is the constructed scalar sum. Their tail assumptions are discharged by DiagonalJetBounds; the background growth and finite-stage residual estimates remain the genuine construction inputs.