Physical jet estimates for the actual diagonal cutoff stages

The cutoff is the constructed SmoothCutoffs.scaledCutoff. Its derivatives are estimated before choosing the diagonal scales. All estimates concern ordinary Fréchet derivatives on an open smooth domain; the estimate carrier itself need not be open.

noncomputable def NavierStokes.CutStageEstimates.finiteBound (f : ℕ → ℝ) (m : ℕ) : ℝ

A concrete finite bound, used only for constants and derivative losses.

Equations

• NavierStokes.CutStageEstimates.finiteBound f m = 1 + ∑ k ∈ Finset.range (m + 1), |f k|

theorem NavierStokes.CutStageEstimates.finiteBound_one_le (f : ℕ → ℝ) (m : ℕ) : 1 ≤ finiteBound f m

theorem NavierStokes.CutStageEstimates.le_finiteBound (f : ℕ → ℝ) {k m : ℕ} (hkm : k ≤ m) : f k ≤ finiteBound f m

theorem NavierStokes.CutStageEstimates.scaledCutoff_jet_one_bounded (k : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (a : ℝ), 0 ≤ a → ‖iteratedFDeriv ℝ k (SmoothCutoffs.scaledCutoff a) 1‖ ≤ C

At the normalized argument 1, every derivative of every nonnegative scale has a common bound. Derivative support removes the scale parameter.

theorem NavierStokes.CutStageEstimates.scaledCutoff_finite_jets_one_bounded (m : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (a : ℝ), 0 ≤ a → ∀ k ≤ m, ‖iteratedFDeriv ℝ k (SmoothCutoffs.scaledCutoff a) 1‖ ≤ C

theorem NavierStokes.CutStageEstimates.cutoff_jets_zero_of_one_le (m : ℕ) {x : ℝ} (hx : 1 ≤ x) : iteratedFDeriv ℝ m SmoothCutoffs.cutoff x = 0

The scalar cutoff is flat at its support boundary, including order zero. Continuity of each actual derivative supplies the boundary value.

theorem NavierStokes.CutStageEstimates.composition_jet_bound {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {f : E → ℝ} {g : ℝ → V} {U : Set E} (hU : IsOpen U) (hf : ContDiffOn ℝ (↑⊤) f U) (hg : ContDiff ℝ (↑⊤) g) {x : E} (hx : x ∈ U) (m : ℕ) {C D : ℝ} (hC : ∀ k ≤ m, ‖iteratedFDeriv ℝ k g (f x)‖ ≤ C) (hD : ∀ (k : ℕ), 1 ≤ k → k ≤ m → ‖iteratedFDeriv ℝ k f x‖ ≤ D ^ k) : ‖iteratedFDeriv ℝ m (g ∘ f) x‖ ≤ ↑m.factorial * C * D ^ m

The ordinary chain-rule bound on an open domain, with a global outer map.

theorem NavierStokes.CutStageEstimates.cutoff_jet_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U S : Set E} (hU : IsOpen U) (hSU : S ⊆ U) {q : E → ℝ} (hq : ContDiffOn ℝ (↑⊤) q U) (hpos : ∀ x ∈ S, 0 < q x) (B : ℕ → ℝ) (hB : ∀ (k : ℕ), ∀ x ∈ S, ‖iteratedFDeriv ℝ k q x‖ ≤ B k * q x ^ (1 - ↑k)) (m : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (a : ℝ), 0 ≤ a → ∀ x ∈ S, ‖iteratedFDeriv ℝ m (fun (y : E) => SmoothCutoffs.scaledCutoff a (q y)) x‖ ≤ C * q x ^ (-↑m)

Sharp scale-independent cutoff loss. The relative coordinate q/q(x) has value one at the evaluation point, so the preceding scalar estimate absorbs every power of the arbitrary cutoff scale.

theorem NavierStokes.CutStageEstimates.smul_jet_bound {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {f : E → ℝ} {g : E → V} {U : Set E} (hU : IsOpen U) (hf : ContDiffOn ℝ (↑⊤) f U) (hg : ContDiffOn ℝ (↑⊤) g U) {x : E} (hx : x ∈ U) (m : ℕ) : ‖iteratedFDeriv ℝ m (fun (y : E) => f y • g y) x‖ ≤ ∑ i ∈ Finset.range (m + 1), ↑(m.choose i) * ‖iteratedFDeriv ℝ i f x‖ * ‖iteratedFDeriv ℝ (m - i) g x‖

theorem NavierStokes.CutStageEstimates.composedCutoff_jets_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set E} (hU : IsOpen U) {q : E → ℝ} (hq : ContDiffOn ℝ (↑⊤) q U) {x : E} (hx : x ∈ U) (a : ℝ) (haq : 1 ≤ a * q x) (m : ℕ) : iteratedFDeriv ℝ m (fun (y : E) => SmoothCutoffs.scaledCutoff a (q y)) x = 0

All jets of the composed cutoff vanish on and beyond its boundary. This does not require the coordinate to cross that boundary locally.

theorem NavierStokes.CutStageEstimates.cut_product_jets_zero {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {U : Set E} (hU : IsOpen U) {q : E → ℝ} (hq : ContDiffOn ℝ (↑⊤) q U) {A : E → V} (hA : ContDiffOn ℝ (↑⊤) A U) {x : E} (hx : x ∈ U) (a : ℝ) (haq : 1 ≤ a * q x) (m : ℕ) : iteratedFDeriv ℝ m (fun (y : E) => SmoothCutoffs.scaledCutoff a (q y) • A y) x = 0

noncomputable def NavierStokes.CutStageEstimates.cutLoss (L : ℕ → ℝ) (m : ℕ) : ℝ

The loss depends only on derivative order and the original loss function. It is deliberately allowed to overestimate the finite maximum.

Equations

• NavierStokes.CutStageEstimates.cutLoss L m = NavierStokes.CutStageEstimates.finiteBound L m + ↑m

noncomputable def NavierStokes.CutStageEstimates.cutLog (p : ℕ → ℕ → ℝ) (j m : ℕ) : ℝ

The logarithmic exponent can depend on the stage, but never on its cutoff.

Equations

• NavierStokes.CutStageEstimates.cutLog p j m = NavierStokes.CutStageEstimates.finiteBound (p j) m

def NavierStokes.CutStageEstimates.RawStageBounds {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (q : E → ℝ) (A : ℕ → E → V) (g L : ℕ → ℝ) (C p : ℕ → ℕ → ℝ) (S : Set E) : Prop

Actual uncut jets, only on the portion q ≤ 1 of the estimate carrier. No condition is imposed on order zero of the stage sequence.

Equations

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

theorem NavierStokes.CutStageEstimates.cut_product_bound {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {U S : Set E} (hU : IsOpen U) (hSU : S ⊆ U) {q : E → ℝ} (hq : ContDiffOn ℝ (↑⊤) q U) (hpos : ∀ x ∈ S, 0 < q x) {A : E → V} (hA : ContDiffOn ℝ (↑⊤) A U) (Q C p L : ℕ → ℝ) (g : ℝ) (hcut : ∀ (k : ℕ) (a : ℝ), 0 ≤ a → ∀ x ∈ S, q x ≤ 1 → ‖iteratedFDeriv ℝ k (fun (y : E) => SmoothCutoffs.scaledCutoff a (q y)) x‖ ≤ Q k * q x ^ (-↑k)) (hraw : ∀ (k : ℕ), ∀ x ∈ S, q x ≤ 1 → ‖iteratedFDeriv ℝ k A x‖ ≤ C k * (1 + |Real.log (q x)|) ^ p k * q x ^ (g - L k)) (m : ℕ) : ∃ (K : ℝ), 0 < K ∧ ∀ (a : ℝ), 0 ≤ a → ∀ x ∈ S, q x ≤ 1 → ‖iteratedFDeriv ℝ m (fun (y : E) => SmoothCutoffs.scaledCutoff a (q y) • A y) x‖ ≤ K * (1 + |Real.log (q x)|) ^ finiteBound p m * q x ^ (g - cutLoss L m)

Leibniz's formula converts the genuine raw jet bounds into uniform cut-stage bounds. The constant and logarithmic exponent are independent of the arbitrary nonnegative cutoff parameter.

theorem NavierStokes.CutStageEstimates.exists_cut_stage_constants {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {U S : Set E} (hU : IsOpen U) (hSU : S ⊆ U) {q : E → ℝ} (hq : ContDiffOn ℝ (↑⊤) q U) (hpos : ∀ x ∈ S, 0 < q x) (B : ℕ → ℝ) (hB : ∀ (k : ℕ), ∀ x ∈ S, q x ≤ 1 → ‖iteratedFDeriv ℝ k q x‖ ≤ B k * q x ^ (1 - ↑k)) {A : ℕ → E → V} (hA : ∀ (j : ℕ), 1 ≤ j → ContDiffOn ℝ (↑⊤) (A j) U) (g L : ℕ → ℝ) (C p : ℕ → ℕ → ℝ) (hraw : RawStageBounds q A g L C p S) : ∃ (K : ℕ → ℕ → ℝ), (∀ (j m : ℕ), 0 < K j m) ∧ ∀ (j : ℕ), 1 ≤ j → ∀ (m : ℕ) (a : ℝ), 0 ≤ a → ∀ x ∈ S, q x ≤ 1 → ‖iteratedFDeriv ℝ m (fun (y : E) => SmoothCutoffs.scaledCutoff a (q y) • A j y) x‖ ≤ K j m * (1 + |Real.log (q x)|) ^ cutLog p j m * q x ^ (g j - cutLoss L m)

One family of constants works for every possible choice of cutoff parameters; these are derived from the uncut jets, not supplied as data.

theorem NavierStokes.CutStageEstimates.cut_product_bound_of_threshold {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {U S : Set E} (hU : IsOpen U) (hSU : S ⊆ U) {q : E → ℝ} (hq : ContDiffOn ℝ (↑⊤) q U) (hpos : ∀ x ∈ S, 0 < q x) {A : E → V} (hA : ContDiffOn ℝ (↑⊤) A U) (m : ℕ) {K P g L a ε : ℝ} (ha : 1 ≤ a) (hε : 0 ≤ ε) (hcut : ∀ (c : ℝ), 0 ≤ c → ∀ x ∈ S, q x ≤ 1 → ‖iteratedFDeriv ℝ m (fun (y : E) => SmoothCutoffs.scaledCutoff c (q y) • A y) x‖ ≤ K * (1 + |Real.log (q x)|) ^ P * q x ^ (g - L)) (hsmall : ∀ (r : ℝ), 0 < r → r ≤ 1 / a → |DiagonalScale.logPowerWeight K P (g / 2) r| ≤ ε) (x : E) : x ∈ S → ‖iteratedFDeriv ℝ m (fun (y : E) => SmoothCutoffs.scaledCutoff a (q y) • A y) x‖ ≤ ε * q x ^ (g / 2 - L)

The scalar threshold estimate now applies to the actual differentiated product. Outside the threshold its jets vanish, including at the boundary.

theorem NavierStokes.CutStageEstimates.exists_diagonal_cut_bounds {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {U S : Set E} (hU : IsOpen U) (hSU : S ⊆ U) {q : E → ℝ} (hq : ContDiffOn ℝ (↑⊤) q U) (hpos : ∀ x ∈ S, 0 < q x) (Bq : ℕ → ℝ) (hBq : ∀ (k : ℕ), ∀ x ∈ S, q x ≤ 1 → ‖iteratedFDeriv ℝ k q x‖ ≤ Bq k * q x ^ (1 - ↑k)) {A : ℕ → E → V} (hA : ∀ (j : ℕ), 1 ≤ j → ContDiffOn ℝ (↑⊤) (A j) U) (g L : ℕ → ℝ) (C p : ℕ → ℕ → ℝ) (hraw : RawStageBounds q A g L C p S) (hg : ∀ (j : ℕ), 1 ≤ j → 0 < g j) (lower : ℕ) : ∃ (a : ℕ → ℕ), lower ≤ a 0 ∧ (∀ (j : ℕ), 0 < a j) ∧ (∀ (j : ℕ), 2 * a j ≤ a (j + 1)) ∧ StrictMono a ∧ Filter.Tendsto (fun (j : ℕ) => ↑(a j)) Filter.atTop Filter.atTop ∧ DiagonalJetBounds.CutStageBounds (fun (j : ℕ) => ↑(a j)) q A (fun (j : ℕ) => g j / 2) (cutLoss L) S

One numeric scale sequence controls every derivative budget m ≤ j+2 of every positive stage. The actual cut-stage estimate is proved from the raw estimates and the coordinate estimates.

theorem NavierStokes.CutStageEstimates.exists_finite_diagonal_cut_bounds {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ι : Type u_3} {W : ι → Type u_4} [(i : ι) → NormedAddCommGroup (W i)] [(i : ι) → NormedSpace ℝ (W i)] [Finite ι] {U S : Set E} (hU : IsOpen U) (hSU : S ⊆ U) {q : E → ℝ} (hq : ContDiffOn ℝ (↑⊤) q U) (hpos : ∀ x ∈ S, 0 < q x) (Bq : ℕ → ℝ) (hBq : ∀ (k : ℕ), ∀ x ∈ S, q x ≤ 1 → ‖iteratedFDeriv ℝ k q x‖ ≤ Bq k * q x ^ (1 - ↑k)) {A : (i : ι) → ℕ → E → W i} (hA : ∀ (i : ι) (j : ℕ), 1 ≤ j → ContDiffOn ℝ (↑⊤) (A i j) U) (g L : ℕ → ℝ) (C p : ι → ℕ → ℕ → ℝ) (hraw : ∀ (i : ι), RawStageBounds q (A i) g L (C i) (p i) S) (hg : ∀ (j : ℕ), 1 ≤ j → 0 < g j) (lower : ℕ) : ∃ (a : ℕ → ℕ), lower ≤ a 0 ∧ (∀ (j : ℕ), 0 < a j) ∧ (∀ (j : ℕ), 2 * a j ≤ a (j + 1)) ∧ StrictMono a ∧ Filter.Tendsto (fun (j : ℕ) => ↑(a j)) Filter.atTop Filter.atTop ∧ ∀ (i : ι), DiagonalJetBounds.CutStageBounds (fun (j : ℕ) => ↑(a j)) q (A i) (fun (j : ℕ) => g j / 2) (cutLoss L) S

A single doubling schedule for a finite heterogeneous family, such as Cartesian stream potentials, direct angular fields, and scalar pressures. The cutoff is applied directly to every component; no extra derivative is introduced for components that are already velocity fields.

noncomputable def NavierStokes.CutStageEstimates.positiveStages {E : Type u_1} {V : Type u_2} [NormedAddCommGroup V] (A : ℕ → E → V) (j : ℕ) (x : E) : V

Remove the unused zeroth correction without imposing any regularity or decay hypothesis on the value supplied at that index.

Equations

• NavierStokes.CutStageEstimates.positiveStages A j x = if j = 0 then 0 else A j x

@[simp]

theorem NavierStokes.CutStageEstimates.positiveStages_zero {E : Type u_1} {V : Type u_2} [NormedAddCommGroup V] (A : ℕ → E → V) : positiveStages A 0 = 0

theorem NavierStokes.CutStageEstimates.positiveStages_of_pos {E : Type u_1} {V : Type u_2} [NormedAddCommGroup V] {A : ℕ → E → V} {j : ℕ} (hj : 1 ≤ j) : positiveStages A j = A j

theorem NavierStokes.CutStageEstimates.positiveStages_smooth {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {U : Set E} {A : ℕ → E → V} (hA : ∀ (j : ℕ), 1 ≤ j → ContDiffOn ℝ (↑⊤) (A j) U) (j : ℕ) : ContDiffOn ℝ (↑⊤) (positiveStages A j) U

theorem NavierStokes.CutStageEstimates.positiveStages_cut_bounds {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {q : E → ℝ} {A : ℕ → E → V} {a g L : ℕ → ℝ} {S : Set E} (hb : DiagonalJetBounds.CutStageBounds a q A g L S) : DiagonalJetBounds.CutStageBounds a q (positiveStages A) g L S

theorem NavierStokes.CutStageEstimates.positive_sum_smooth {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {U : Set E} (hU : IsOpen U) {q : E → ℝ} (hq : ContDiffOn ℝ (↑⊤) q U) (hpos : ∀ x ∈ U, 0 < q x) {A : ℕ → E → V} (hA : ∀ (j : ℕ), 1 ≤ j → ContDiffOn ℝ (↑⊤) (A j) U) {a : ℕ → ℕ} (ha : StrictMono a) : ContDiffOn ℝ (↑⊤) (SolenoidalDiagonal.potentialSum (fun (j : ℕ) => ↑(a j)) q (positiveStages A)) U

The selected positive-stage series is the actual locally finite sum and is smooth on the full positive-coordinate domain.

theorem NavierStokes.CutStageEstimates.cut_product_eventually_zero {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup V] [NormedSpace ℝ V] {q : E → ℝ} {x : E} (hq : ContinuousAt q x) (A : E → V) (a : ℝ) (haq : 1 < a * q x) : (fun (y : E) => SmoothCutoffs.scaledCutoff a (q y) • A y) =ᶠ[nhds x] fun (x : E) => 0

Beyond strict cutoff support the product has a zero germ, regardless of any arbitrary totalization of the raw field there.

theorem NavierStokes.CutStageEstimates.cut_product_smooth_of_sublevel {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {U : Set E} (hU : IsOpen U) {q : E → ℝ} (hq : ContDiffOn ℝ (↑⊤) q U) {A : E → V} {qbig a : ℝ} (hA : ContDiffOn ℝ (↑⊤) A (U ∩ {x : E | q x < qbig})) (ha : 0 < a) (hgap : 1 < a * qbig) : ContDiffOn ℝ (↑⊤) (fun (y : E) => SmoothCutoffs.scaledCutoff a (q y) • A y) U

Cutting strictly inside the valid q-domain gives an actual smooth zero extension. Smoothness of the uncut totalization outside it is unused.

noncomputable def NavierStokes.CutStageEstimates.physicalProjection : ProblemStatement.SpaceTime →L[ℝ] PhysicalCoordinateBounds.Point

q is independent of the radial coordinate. Using this linear map avoids charging spurious derivatives of the squared physical radius.

Equations

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

@[simp]

theorem NavierStokes.CutStageEstimates.physicalProjection_apply (w : ProblemStatement.SpaceTime) : physicalProjection w = (w.1, 0, w.2.ofLp 2)

theorem NavierStokes.CutStageEstimates.physicalQ_linear_composition (h : ℝ) : PhysicalWaveSum.physicalQ h = PhysicalCoordinateBounds.physicalQ (2 * h) ∘ ⇑physicalProjection

theorem NavierStokes.CutStageEstimates.physicalQ_jet_bound {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (m : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ w ∈ PhysicalWaveSum.preterminal, PhysicalWaveSum.physicalQ h w ≤ 1 → ‖iteratedFDeriv ℝ m (PhysicalWaveSum.physicalQ h) w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ (1 - ↑m)

The actual Cartesian implicit similarity coordinate has one power of loss per derivative. No bound on the physical radius is required.

theorem NavierStokes.CutStageEstimates.physical_cutoff_jet_bound {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (m : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (a : ℝ), 0 ≤ a → ∀ w ∈ PhysicalWaveSum.preterminal, PhysicalWaveSum.physicalQ h w ≤ 1 → ‖iteratedFDeriv ℝ m (fun (z : ProblemStatement.SpaceTime) => SmoothCutoffs.scaledCutoff a (PhysicalWaveSum.physicalQ h z)) w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ (-↑m)

theorem NavierStokes.CutStageEstimates.exists_physical_diagonal_cut_bounds {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {S : Set ProblemStatement.SpaceTime} (hS : S ⊆ PhysicalWaveSum.preterminal) {A : ℕ → ProblemStatement.SpaceTime → V} (hA : ∀ (j : ℕ), 1 ≤ j → ContDiffOn ℝ (↑⊤) (A j) PhysicalWaveSum.preterminal) (g L : ℕ → ℝ) (C p : ℕ → ℕ → ℝ) (hraw : RawStageBounds (PhysicalWaveSum.physicalQ h) A g L C p S) (hg : ∀ (j : ℕ), 1 ≤ j → 0 < g j) (lower : ℕ) : ∃ (a : ℕ → ℕ), lower ≤ a 0 ∧ (∀ (j : ℕ), 0 < a j) ∧ (∀ (j : ℕ), 2 * a j ≤ a (j + 1)) ∧ StrictMono a ∧ Filter.Tendsto (fun (j : ℕ) => ↑(a j)) Filter.atTop Filter.atTop ∧ DiagonalJetBounds.CutStageBounds (fun (j : ℕ) => ↑(a j)) (PhysicalWaveSum.physicalQ h) A (fun (j : ℕ) => g j / 2) (cutLoss L) S

Actual physical cutoff stages and their single selected schedule. The only stage estimate premise concerns uncut physical derivatives.

theorem NavierStokes.CutStageEstimates.exists_physical_finite_diagonal_cut_bounds {ι : Type u_2} {W : ι → Type u_3} [(i : ι) → NormedAddCommGroup (W i)] [(i : ι) → NormedSpace ℝ (W i)] [Finite ι] {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {S : Set ProblemStatement.SpaceTime} (hS : S ⊆ PhysicalWaveSum.preterminal) {A : (i : ι) → ℕ → ProblemStatement.SpaceTime → W i} (hA : ∀ (i : ι) (j : ℕ), 1 ≤ j → ContDiffOn ℝ (↑⊤) (A i j) PhysicalWaveSum.preterminal) (g L : ℕ → ℝ) (C p : ι → ℕ → ℕ → ℝ) (hraw : ∀ (i : ι), RawStageBounds (PhysicalWaveSum.physicalQ h) (A i) g L (C i) (p i) S) (hg : ∀ (j : ℕ), 1 ≤ j → 0 < g j) (lower : ℕ) : ∃ (a : ℕ → ℕ), lower ≤ a 0 ∧ (∀ (j : ℕ), 0 < a j) ∧ (∀ (j : ℕ), 2 * a j ≤ a (j + 1)) ∧ StrictMono a ∧ Filter.Tendsto (fun (j : ℕ) => ↑(a j)) Filter.atTop Filter.atTop ∧ ∀ (i : ι), DiagonalJetBounds.CutStageBounds (fun (j : ℕ) => ↑(a j)) (PhysicalWaveSum.physicalQ h) (A i) (fun (j : ℕ) => g j / 2) (cutLoss L) S

The same actual implicit coordinate and one unchanged schedule for all finite stream, direct-field, and pressure components.

theorem NavierStokes.CutStageEstimates.exists_physical_positive_sums_of_power {ι : Type u_2} {W : ι → Type u_3} [(i : ι) → NormedAddCommGroup (W i)] [(i : ι) → NormedSpace ℝ (W i)] [Finite ι] {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {S : Set ProblemStatement.SpaceTime} (hS : S ⊆ PhysicalWaveSum.preterminal) {A : (i : ι) → ℕ → ProblemStatement.SpaceTime → W i} (hA : ∀ (i : ι) (j : ℕ), 1 ≤ j → ContDiffOn ℝ (↑⊤) (A i j) PhysicalWaveSum.preterminal) (g L : ℕ → ℝ) (hraw : ∀ (i : ι) (j : ℕ), 1 ≤ j → ∀ (m : ℕ), ∃ (C : ℝ), ∀ w ∈ S, PhysicalWaveSum.physicalQ h w ≤ 1 → ‖iteratedFDeriv ℝ m (A i j) w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ (g j - L m)) (hg : ∀ (j : ℕ), 1 ≤ j → 0 < g j) (lower : ℕ) : ∃ (a : ℕ → ℕ), lower ≤ a 0 ∧ (∀ (j : ℕ), 0 < a j) ∧ (∀ (j : ℕ), 2 * a j ≤ a (j + 1)) ∧ StrictMono a ∧ Filter.Tendsto (fun (j : ℕ) => ↑(a j)) Filter.atTop Filter.atTop ∧ ∀ (i : ι), DiagonalJetBounds.CutStageBounds (fun (j : ℕ) => ↑(a j)) (PhysicalWaveSum.physicalQ h) (positiveStages (A i)) (fun (j : ℕ) => g j / 2) (cutLoss L) S ∧ ContDiffOn ℝ (↑⊤) (SolenoidalDiagonal.potentialSum (fun (j : ℕ) => ↑(a j)) (PhysicalWaveSum.physicalQ h) (positiveStages (A i))) PhysicalWaveSum.preterminal

The common case supplied by physical-copy estimates: the uncut bounds have no logarithmic factor and their constants are existential. The same constructed sequence controls all positive components and gives smooth actual sums on the entire preterminal spacetime domain.

noncomputable def NavierStokes.CutStageEstimates.physicalSublevel (h qbig : ℝ) : Set ProblemStatement.SpaceTime

The genuine open validity region for locally constructed raw stages.

Equations

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

theorem NavierStokes.CutStageEstimates.physicalSublevel_open {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (qbig : ℝ) : IsOpen (physicalSublevel h qbig)

theorem NavierStokes.CutStageEstimates.exists_physical_local_diagonal_cut_bounds {ι : Type u_2} {W : ι → Type u_3} [(i : ι) → NormedAddCommGroup (W i)] [(i : ι) → NormedSpace ℝ (W i)] [Finite ι] {h qbig : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hqbig : 0 < qbig) {S : Set ProblemStatement.SpaceTime} (hS : S ⊆ PhysicalWaveSum.preterminal) {A : (i : ι) → ℕ → ProblemStatement.SpaceTime → W i} (hA : ∀ (i : ι) (j : ℕ), 1 ≤ j → ContDiffOn ℝ (↑⊤) (A i j) (physicalSublevel h qbig)) (g L : ℕ → ℝ) (C p : ι → ℕ → ℕ → ℝ) (hraw : ∀ (i : ι), RawStageBounds (PhysicalWaveSum.physicalQ h) (A i) g L (C i) (p i) (S ∩ physicalSublevel h qbig)) (hg : ∀ (j : ℕ), 1 ≤ j → 0 < g j) (lower : ℕ) : ∃ (a : ℕ → ℕ), lower ≤ a 0 ∧ (∀ (j : ℕ), 0 < a j) ∧ (∀ (j : ℕ), 2 * a j ≤ a (j + 1)) ∧ StrictMono a ∧ Filter.Tendsto (fun (j : ℕ) => ↑(a j)) Filter.atTop Filter.atTop ∧ (∀ (j : ℕ), 1 / ↑(a j) < qbig) ∧ ∀ (i : ι), DiagonalJetBounds.CutStageBounds (fun (j : ℕ) => ↑(a j)) (PhysicalWaveSum.physicalQ h) (positiveStages (A i)) (fun (j : ℕ) => g j / 2) (cutLoss L) S ∧ ContDiffOn ℝ (↑⊤) (SolenoidalDiagonal.potentialSum (fun (j : ℕ) => ↑(a j)) (PhysicalWaveSum.physicalQ h) (positiveStages (A i))) PhysicalWaveSum.preterminal

Local raw stages suffice. The initial scale is chosen so every support lies strictly inside q < qbig; the same actual cut products then extend smoothly by zero to all preterminal points. This is the support extension used in the manuscript before diagonal summation.