The explicit shape transition and its reset-prefix debts

The cutoff and target shape are the actual functions from OutgoingSchedule. Input field bounds are pointwise bounds, not assumptions on the five row debts. All constants in the estimates may be chosen before the final large C.

noncomputable def NavierStokes.ShapeTransition.logShape (eta : ℝ) : ℝ

Log shape, given by Real.log (OutgoingSchedule.shape eta).

Equations

• NavierStokes.ShapeTransition.logShape eta = Real.log (NavierStokes.OutgoingSchedule.shape eta)

theorem NavierStokes.ShapeTransition.logShape_contDiff : ContDiff ℝ (↑⊤) logShape

theorem NavierStokes.ShapeTransition.exp_logShape (eta : ℝ) : Real.exp (logShape eta) = OutgoingSchedule.shape eta

noncomputable def NavierStokes.ShapeTransition.blend (T : ℝ) (li : ℝ → ℝ) (p : ℝ × ℝ) : ℝ

Blend, given by (1 - OutgoingSchedule.sigma (p.1 / T)) * li p.2 + OutgoingSchedule.sigma (p.1 / T) * logShape p.2.

Equations

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

noncomputable def NavierStokes.ShapeTransition.logProfile (C T : ℝ) (li : ℝ → ℝ) (p : ℝ × ℝ) : ℝ

Log profile, given by -Real.log C + p.1 / 10 + blend T li p.

Equations

• NavierStokes.ShapeTransition.logProfile C T li p = -Real.log C + p.1 / 10 + NavierStokes.ShapeTransition.blend T li p

noncomputable def NavierStokes.ShapeTransition.amplitude (T : ℝ) (li : ℝ → ℝ) (p : ℝ × ℝ) : ℝ

Amplitude, given by Real.exp (p.1 / 10 + blend T li p).

Equations

• NavierStokes.ShapeTransition.amplitude T li p = Real.exp (p.1 / 10 + NavierStokes.ShapeTransition.blend T li p)

noncomputable def NavierStokes.ShapeTransition.angular (C T : ℝ) (li : ℝ → ℝ) (p : ℝ × ℝ) : ℝ

Angular, given by Real.exp (logProfile C T li p).

Equations

• NavierStokes.ShapeTransition.angular C T li p = Real.exp (NavierStokes.ShapeTransition.logProfile C T li p)

noncomputable def NavierStokes.ShapeTransition.axial (Gi : ℝ → ℝ) (p : ℝ × ℝ) : ℝ

Axial, given by Gi p.2.

Equations

• NavierStokes.ShapeTransition.axial Gi p = Gi p.2

theorem NavierStokes.ShapeTransition.blend_contDiff (T : ℝ) {li : ℝ → ℝ} (hli : ContDiff ℝ (↑⊤) li) : ContDiff ℝ (↑⊤) (blend T li)

theorem NavierStokes.ShapeTransition.logProfile_contDiff (C T : ℝ) {li : ℝ → ℝ} (hli : ContDiff ℝ (↑⊤) li) : ContDiff ℝ (↑⊤) (logProfile C T li)

theorem NavierStokes.ShapeTransition.amplitude_contDiff (T : ℝ) {li : ℝ → ℝ} (hli : ContDiff ℝ (↑⊤) li) : ContDiff ℝ (↑⊤) (amplitude T li)

theorem NavierStokes.ShapeTransition.angular_contDiff (C T : ℝ) {li : ℝ → ℝ} (hli : ContDiff ℝ (↑⊤) li) : ContDiff ℝ (↑⊤) (angular C T li)

theorem NavierStokes.ShapeTransition.axial_contDiff {Gi : ℝ → ℝ} (hGi : ContDiff ℝ (↑⊤) Gi) : ContDiff ℝ (↑⊤) (axial Gi)

theorem NavierStokes.ShapeTransition.angular_pos (C T : ℝ) (li : ℝ → ℝ) (p : ℝ × ℝ) : 0 < angular C T li p

theorem NavierStokes.ShapeTransition.log_angular (C T : ℝ) (li : ℝ → ℝ) (p : ℝ × ℝ) : Real.log (angular C T li p) = logProfile C T li p

theorem NavierStokes.ShapeTransition.angular_eq_inv_mul {C : ℝ} (hC : 0 < C) (T : ℝ) (li : ℝ → ℝ) (p : ℝ × ℝ) : angular C T li p = C⁻¹ * amplitude T li p

theorem NavierStokes.ShapeTransition.angular_before {C T y : ℝ} (hC : 0 < C) (hT : 0 < T) (hy : y ≤ 0) (li : ℝ → ℝ) (eta : ℝ) : angular C T li (y, eta) = C⁻¹ * Real.exp (y / 10 + li eta)

theorem NavierStokes.ShapeTransition.angular_after {C T y : ℝ} (hC : 0 < C) (hT : 0 < T) (hy : T ≤ y) (li : ℝ → ℝ) (eta : ℝ) : angular C T li (y, eta) = C⁻¹ * Real.exp (y / 10) * OutgoingSchedule.shape eta

theorem NavierStokes.ShapeTransition.angular_initial {C T : ℝ} (hC : 0 < C) (hT : 0 < T) (li : ℝ → ℝ) (eta : ℝ) : angular C T li (0, eta) = C⁻¹ * Real.exp (li eta)

Smoothness above and exact equalities on both closed half-lines give the actual smooth gluing. The following statement records all radial jets on the open constant-profile regions as well.

theorem NavierStokes.ShapeTransition.angular_jets_before {C T y : ℝ} (hC : 0 < C) (hT : 0 < T) (hy : y < 0) (li : ℝ → ℝ) (eta : ℝ) (n : ℕ) : iteratedDeriv n (fun (s : ℝ) => angular C T li (s, eta)) y = iteratedDeriv n (fun (s : ℝ) => C⁻¹ * Real.exp (s / 10 + li eta)) y

theorem NavierStokes.ShapeTransition.angular_jets_after {C T y : ℝ} (hC : 0 < C) (hT : 0 < T) (hy : T < y) (li : ℝ → ℝ) (eta : ℝ) (n : ℕ) : iteratedDeriv n (fun (s : ℝ) => angular C T li (s, eta)) y = iteratedDeriv n (fun (s : ℝ) => C⁻¹ * Real.exp (s / 10) * OutgoingSchedule.shape eta) y

A duration chosen before C

theorem NavierStokes.ShapeTransition.sigma_deriv_zero_left {x : ℝ} (hx : x < 0) : deriv OutgoingSchedule.sigma x = 0

theorem NavierStokes.ShapeTransition.sigma_deriv_zero_right {x : ℝ} (hx : 1 < x) : deriv OutgoingSchedule.sigma x = 0

theorem NavierStokes.ShapeTransition.sigma_deriv_bounded : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (x : ℝ), |deriv OutgoingSchedule.sigma x| ≤ K

noncomputable def NavierStokes.ShapeTransition.logarithmicSlope (T : ℝ) (li : ℝ → ℝ) (p : ℝ × ℝ) : ℝ

Logarithmic slope, given by 3 / 5 + deriv OutgoingSchedule.sigma (p.1 / T) / T * (logShape p.2 - li p.2).

Equations

• NavierStokes.ShapeTransition.logarithmicSlope T li p = 3 / 5 + deriv NavierStokes.OutgoingSchedule.sigma (p.1 / T) / T * (NavierStokes.ShapeTransition.logShape p.2 - li p.2)

theorem NavierStokes.ShapeTransition.logProfile_hasDerivAt (C T : ℝ) (li : ℝ → ℝ) (y eta : ℝ) : HasDerivAt (fun (s : ℝ) => logProfile C T li (s, eta)) (logarithmicSlope T li (y, eta) - 1 / 2) y

theorem NavierStokes.ShapeTransition.logarithmicSlope_eq (C T : ℝ) (li : ℝ → ℝ) (y eta : ℝ) : logarithmicSlope T li (y, eta) = 1 / 2 + deriv (fun (s : ℝ) => logProfile C T li (s, eta)) y

theorem NavierStokes.ShapeTransition.logarithmicSlope_eq_actual (C T : ℝ) (li : ℝ → ℝ) (y eta : ℝ) : logarithmicSlope T li (y, eta) = 1 / 2 + deriv (fun (s : ℝ) => Real.log (angular C T li (s, eta))) y

theorem NavierStokes.ShapeTransition.logarithmicSlope_bounds {T K B : ℝ} {li : ℝ → ℝ} (hT : 0 < T) (hK : 0 ≤ K) : 0 ≤ B → ∀ (hSigma : ∀ (x : ℝ), |deriv OutgoingSchedule.sigma x| ≤ K) (hDuration : 20 * K * B ≤ T) {y eta : ℝ} (hData : |logShape eta - li eta| ≤ B), 11 / 20 ≤ logarithmicSlope T li (y, eta) ∧ logarithmicSlope T li (y, eta) ≤ 13 / 20

theorem NavierStokes.ShapeTransition.exists_duration (B : ℝ) (hB : 0 ≤ B) : ∃ (T : ℝ), 0 < T ∧ ∀ (li : ℝ → ℝ) (C y eta : ℝ), |logShape eta - li eta| ≤ B → 11 / 20 ≤ 1 / 2 + deriv (fun (s : ℝ) => logProfile C T li (s, eta)) y ∧ 1 / 2 + deriv (fun (s : ℝ) => logProfile C T li (s, eta)) y ≤ 13 / 20

theorem NavierStokes.ShapeTransition.blend_abs_le {T B : ℝ} {li : ℝ → ℝ} {y eta : ℝ} (hli : |li eta| ≤ B) (hf : |logShape eta| ≤ B) : |blend T li (y, eta)| ≤ B

theorem NavierStokes.ShapeTransition.amplitude_le {T B : ℝ} {li : ℝ → ℝ} {y eta : ℝ} (hy : y ≤ T) (hli : |li eta| ≤ B) (hf : |logShape eta| ≤ B) : amplitude T li (y, eta) ≤ Real.exp (T / 10 + B)

Uniform finite parameter jets from the input jets

theorem NavierStokes.ShapeTransition.blend_iteratedDeriv (T y : ℝ) {li : ℝ → ℝ} (hli : ContDiff ℝ (↑⊤) li) (n : ℕ) (eta : ℝ) : iteratedDeriv n (fun (e : ℝ) => blend T li (y, e)) eta = (1 - OutgoingSchedule.sigma (y / T)) * iteratedDeriv n li eta + OutgoingSchedule.sigma (y / T) * iteratedDeriv n logShape eta

theorem NavierStokes.ShapeTransition.convex_abs_le {s a b B : ℝ} (hs0 : 0 ≤ s) (hs1 : s ≤ 1) (ha : |a| ≤ B) (hb : |b| ≤ B) : |(1 - s) * a + s * b| ≤ B

theorem NavierStokes.ShapeTransition.blend_jet_bound (T y : ℝ) {li : ℝ → ℝ} (hli : ContDiff ℝ (↑⊤) li) (n : ℕ) {eta B : ℝ} (hl : |iteratedDeriv n li eta| ≤ B) (hf : |iteratedDeriv n logShape eta| ≤ B) : |iteratedDeriv n (fun (e : ℝ) => blend T li (y, e)) eta| ≤ B

theorem NavierStokes.ShapeTransition.amplitude_jet_bound {T y B : ℝ} {li : ℝ → ℝ} (hli : ContDiff ℝ (↑⊤) li) (hB : 1 ≤ B) (hy : y ≤ T) (n : ℕ) (eta : ℝ) (hl : ∀ i ≤ n, |iteratedDeriv i li eta| ≤ B) (hf : ∀ i ≤ n, |iteratedDeriv i logShape eta| ≤ B) : |iteratedDeriv n (fun (e : ℝ) => amplitude T li (y, e)) eta| ≤ ↑n.factorial * Real.exp (T / 10 + B) * B ^ n

theorem NavierStokes.ShapeTransition.angular_iteratedDeriv {C : ℝ} (hC : 0 < C) (T y : ℝ) {li : ℝ → ℝ} (hli : ContDiff ℝ (↑⊤) li) (n : ℕ) (eta : ℝ) : iteratedDeriv n (fun (e : ℝ) => angular C T li (y, e)) eta = C⁻¹ * iteratedDeriv n (fun (e : ℝ) => amplitude T li (y, e)) eta

theorem NavierStokes.ShapeTransition.angular_jet_bound {C T y B : ℝ} (hC : 0 < C) {li : ℝ → ℝ} (hli : ContDiff ℝ (↑⊤) li) (hB : 1 ≤ B) (hy : y ≤ T) (n : ℕ) (eta : ℝ) (hl : ∀ i ≤ n, |iteratedDeriv i li eta| ≤ B) (hf : ∀ i ≤ n, |iteratedDeriv i logShape eta| ≤ B) : |iteratedDeriv n (fun (e : ℝ) => angular C T li (y, e)) eta| ≤ ↑n.factorial * Real.exp (T / 10 + B) * B ^ n / C

The reset clock and exact ideal matching

noncomputable def NavierStokes.ShapeTransition.resetRadius (Xi C P : ℝ) : ℝ

Reset radius, given by Xi * (C * P) ^ 10.

Equations

• NavierStokes.ShapeTransition.resetRadius Xi C P = Xi * (C * P) ^ 10

noncomputable def NavierStokes.ShapeTransition.separation (T C P : ℝ) : ℝ

Separation, given by Real.exp T / (C * P) ^ 10.

Equations

• NavierStokes.ShapeTransition.separation T C P = Real.exp T / (C * P) ^ 10

noncomputable def NavierStokes.ShapeTransition.resetClock (C P y : ℝ) : ℝ

Reset clock, given by y - 10 * Real.log (C * P).

Equations

• NavierStokes.ShapeTransition.resetClock C P y = y - 10 * Real.log (C * P)

noncomputable def NavierStokes.ShapeTransition.idealAngular (P : ℝ) (p : ℝ × ℝ) : ℝ

Ideal angular, given by P * OutgoingSchedule.shape p.2 * Real.exp (p.1 / 10).

Equations

• NavierStokes.ShapeTransition.idealAngular P p = P * NavierStokes.OutgoingSchedule.shape p.2 * Real.exp (p.1 / 10)

theorem NavierStokes.ShapeTransition.idealAngular_contDiff (P : ℝ) : ContDiff ℝ (↑⊤) (idealAngular P)

theorem NavierStokes.ShapeTransition.angular_after_reset_clock {C P T y : ℝ} (hC : 0 < C) (hP : 0 < P) (hT : 0 < T) (hy : T ≤ y) (li : ℝ → ℝ) (eta : ℝ) : angular C T li (y, eta) = idealAngular P (resetClock C P y, eta)

theorem NavierStokes.ShapeTransition.separation_pos (T : ℝ) {C P : ℝ} (hC : 0 < C) (hP : 0 < P) : 0 < separation T C P

theorem NavierStokes.ShapeTransition.resetRadius_mul_separation (Xi T C P : ℝ) (hCP : C * P ≠ 0) : resetRadius Xi C P * separation T C P = Xi * Real.exp T

theorem NavierStokes.ShapeTransition.separation_tendsto (T : ℝ) {P : ℝ} : P ≠ 0 → Filter.Tendsto (fun (C : ℝ) => separation T C P) Filter.atTop (nhds 0)

theorem NavierStokes.ShapeTransition.separation_eventually_before (T : ℝ) {P : ℝ} (hP : 0 < P) (clock : ℝ) : ∀ᶠ (C : ℝ) in Filter.atTop, separation T C P < Real.exp clock

Actual restoration on reset-clock times -8 to -7

noncomputable def NavierStokes.ShapeTransition.restore (Gi : ℝ → ℝ) (p : ℝ × ℝ) : ℝ

Restore, given by (1 - OutgoingSchedule.sigma (p.1 + 8)) * Gi p.2 + OutgoingSchedule.sigma (p.1 + 8) * (4 * p.2).

Equations

• NavierStokes.ShapeTransition.restore Gi p = (1 - NavierStokes.OutgoingSchedule.sigma (p.1 + 8)) * Gi p.2 + NavierStokes.OutgoingSchedule.sigma (p.1 + 8) * (4 * p.2)

theorem NavierStokes.ShapeTransition.restore_contDiff {Gi : ℝ → ℝ} (hGi : ContDiff ℝ (↑⊤) Gi) : ContDiff ℝ (↑⊤) (restore Gi)

theorem NavierStokes.ShapeTransition.restore_before {z : ℝ} (hz : z ≤ -8) (Gi : ℝ → ℝ) (eta : ℝ) : restore Gi (z, eta) = Gi eta

theorem NavierStokes.ShapeTransition.restore_after {z : ℝ} (hz : -7 ≤ z) (Gi : ℝ → ℝ) (eta : ℝ) : restore Gi (z, eta) = 4 * eta

theorem NavierStokes.ShapeTransition.restore_sub (Gi : ℝ → ℝ) (z eta : ℝ) : restore Gi (z, eta) - 4 * eta = (1 - OutgoingSchedule.sigma (z + 8)) * (Gi eta - 4 * eta)

theorem NavierStokes.ShapeTransition.restore_error_le (Gi : ℝ → ℝ) (z eta : ℝ) : |restore Gi (z, eta) - 4 * eta| ≤ |Gi eta - 4 * eta|

theorem NavierStokes.ShapeTransition.restore_error_jet (Gi : ℝ → ℝ) (hGi : ContDiff ℝ (↑⊤) Gi) (z eta : ℝ) (n : ℕ) : iteratedDeriv n (fun (e : ℝ) => restore Gi (z, e) - 4 * e) eta = (1 - OutgoingSchedule.sigma (z + 8)) * iteratedDeriv n (fun (e : ℝ) => Gi e - 4 * e) eta

theorem NavierStokes.ShapeTransition.restore_error_jet_le (Gi : ℝ → ℝ) (hGi : ContDiff ℝ (↑⊤) Gi) (z eta : ℝ) (n : ℕ) : |iteratedDeriv n (fun (e : ℝ) => restore Gi (z, e) - 4 * e) eta| ≤ |iteratedDeriv n (fun (e : ℝ) => Gi e - 4 * e) eta|

A smooth physical-radius implementation, including the old axis piece

noncomputable def NavierStokes.ShapeTransition.radialSwitch (Xi T X : ℝ) : ℝ

The harmless zero extension avoids evaluating the logarithmic clock at the axis. On every positive radius this is exactly the cutoff in (19).

Equations

• NavierStokes.ShapeTransition.radialSwitch Xi T X = if X ≤ Xi / 2 then 0 else NavierStokes.OutgoingSchedule.sigma (Real.log (X / Xi) / T)

theorem NavierStokes.ShapeTransition.radialSwitch_zero {Xi T X : ℝ} (hXi : 0 < Xi) (hT : 0 < T) (hX : X ≤ Xi) : radialSwitch Xi T X = 0

theorem NavierStokes.ShapeTransition.radialSwitch_eq {Xi T X : ℝ} (hXi : 0 < Xi) (hT : 0 < T) (hX : 0 < X) : radialSwitch Xi T X = OutgoingSchedule.sigma (Real.log (X / Xi) / T)

theorem NavierStokes.ShapeTransition.radialSwitch_contDiff {Xi T : ℝ} (hXi : 0 < Xi) (hT : 0 < T) : ContDiff ℝ (↑⊤) (radialSwitch Xi T)

noncomputable def NavierStokes.ShapeTransition.shapeField (Xi T : ℝ) (li : ℝ → ℝ) (old : ℝ × ℝ → ℝ) (p : ℝ × ℝ) : ℝ

The supplied old normalized field is continued by its held power law past Xi. Multiplication by this explicit smooth factor performs the transition.

Equations

• NavierStokes.ShapeTransition.shapeField Xi T li old p = old p * Real.exp (NavierStokes.ShapeTransition.radialSwitch Xi T p.1 * (NavierStokes.ShapeTransition.logShape p.2 - li p.2))

theorem NavierStokes.ShapeTransition.shapeField_contDiff {Xi T : ℝ} (hXi : 0 < Xi) (hT : 0 < T) {li : ℝ → ℝ} {old : ℝ × ℝ → ℝ} (hli : ContDiff ℝ (↑⊤) li) (hold : ContDiff ℝ (↑⊤) old) : ContDiff ℝ (↑⊤) (shapeField Xi T li old)

theorem NavierStokes.ShapeTransition.shapeField_before {Xi T X : ℝ} (hXi : 0 < Xi) (hT : 0 < T) (hX : X ≤ Xi) (li : ℝ → ℝ) (old : ℝ × ℝ → ℝ) (eta : ℝ) : shapeField Xi T li old (X, eta) = old (X, eta)

theorem NavierStokes.ShapeTransition.shapeField_eq_profile {Xi C T X : ℝ} (hXi : 0 < Xi) (hC : 0 < C) (hT : 0 < T) (hX : 0 < X) (li : ℝ → ℝ) (old : ℝ × ℝ → ℝ) (eta : ℝ) (hold : old (X, eta) = C⁻¹ * Real.exp (Real.log (X / Xi) / 10 + li eta) / √(2 * X)) : shapeField Xi T li old (X, eta) = angular C T li (Real.log (X / Xi), eta) / √(2 * X)

theorem NavierStokes.ShapeTransition.shapeField_jet_bound {Xi C T X B K : ℝ} (hXi : 0 < Xi) (hC : 0 < C) (hT : 0 < T) : 0 ≤ X → ∀ (hXL : X ≤ Xi * Real.exp T) {li : ℝ → ℝ} {old : ℝ × ℝ → ℝ} (hli : ContDiff ℝ (↑⊤) li) (hB : 1 ≤ B) (hK : 0 ≤ K) (n : ℕ) (eta : ℝ) (hAxis : X ≤ Xi → |iteratedDeriv n (fun (e : ℝ) => old (X, e)) eta| ≤ K / C) (hHold : Xi ≤ X → ∀ (e : ℝ), old (X, e) = C⁻¹ * Real.exp (Real.log (X / Xi) / 10 + li e) / √(2 * X)) (hl : ∀ i ≤ n, |iteratedDeriv i li eta| ≤ B) (hf : ∀ i ≤ n, |iteratedDeriv i logShape eta| ≤ B), |iteratedDeriv n (fun (e : ℝ) => shapeField Xi T li old (X, e)) eta| ≤ (K + ↑n.factorial * Real.exp (T / 10 + B) * B ^ n / √(2 * Xi)) / C

Actual compact integrals and their parameter jets

theorem NavierStokes.ShapeTransition.partial_jet_continuous {F : ℝ × ℝ → ℝ} (hF : ContDiff ℝ (↑⊤) F) (n : ℕ) : Continuous fun (p : ℝ × ℝ) => iteratedDeriv n (fun (e : ℝ) => F (p.1, e)) p.2

theorem NavierStokes.ShapeTransition.integral_iteratedDeriv {F : ℝ × ℝ → ℝ} (hF : ContDiff ℝ (↑⊤) F) {r : ℝ} (hr : 0 ≤ r) (n : ℕ) (eta : ℝ) : iteratedDeriv n (fun (e : ℝ) => ∫ (x : ℝ) in 0..r, F (x, e)) eta = ∫ (x : ℝ) in 0..r, iteratedDeriv n (fun (e : ℝ) => F (x, e)) eta

theorem NavierStokes.ShapeTransition.integral_jet_bound {F : ℝ × ℝ → ℝ} (hF : ContDiff ℝ (↑⊤) F) {r B : ℝ} (hr : 0 ≤ r) (n : ℕ) (eta : ℝ) (hB : ∀ x ∈ Set.Ioc 0 r, |iteratedDeriv n (fun (e : ℝ) => F (x, e)) eta| ≤ B) : |iteratedDeriv n (fun (e : ℝ) => ∫ (x : ℝ) in 0..r, F (x, e)) eta| ≤ B * r

theorem NavierStokes.ShapeTransition.product_jet_bound {f g : ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (n : ℕ) (eta : ℝ) {A B : ℝ} (hA : 0 ≤ A) : 0 ≤ B → ∀ (hfb : ∀ k ≤ n, |iteratedDeriv k f eta| ≤ A) (hgb : ∀ k ≤ n, |iteratedDeriv k g eta| ≤ B), |iteratedDeriv n (fun (e : ℝ) => f e * g e) eta| ≤ 2 ^ n * A * B

The five actual scaled history rows

noncomputable def NavierStokes.ShapeTransition.scaledE (R : ℝ) (f : ℝ × ℝ → ℝ) (p : ℝ × ℝ) : ℝ

Scaled E, given by Real.sqrt (2 * R * p.1) * f p.

Equations

• NavierStokes.ShapeTransition.scaledE R f p = √(2 * R * p.1) * f p

noncomputable def NavierStokes.ShapeTransition.rowM (u : ℝ × ℝ → ℝ) (r eta : ℝ) : ℝ

Row M, given by ∫ x in (0 : ℝ)..r, u (x, eta).

Equations

• NavierStokes.ShapeTransition.rowM u r eta = ∫ (x : ℝ) in 0..r, u (x, eta)

noncomputable def NavierStokes.ShapeTransition.rowI (R : ℝ) (f : ℝ × ℝ → ℝ) (r eta : ℝ) : ℝ

Row I, given by ∫ x in (0 : ℝ)..r, Real.sqrt (2 * x) * scaledE R f (x, eta).

Equations

• NavierStokes.ShapeTransition.rowI R f r eta = ∫ (x : ℝ) in 0..r, √(2 * x) * NavierStokes.ShapeTransition.scaledE R f (x, eta)

noncomputable def NavierStokes.ShapeTransition.rowJ (R : ℝ) (u f : ℝ × ℝ → ℝ) (r eta : ℝ) : ℝ

Row J, given by ∫ x in (0 : ℝ)..r, u (x, eta) * Real.sqrt (2 * x) * scaledE R f (x, eta).

Equations

• NavierStokes.ShapeTransition.rowJ R u f r eta = ∫ (x : ℝ) in 0..r, u (x, eta) * √(2 * x) * NavierStokes.ShapeTransition.scaledE R f (x, eta)

noncomputable def NavierStokes.ShapeTransition.rowS (R : ℝ) (u f : ℝ × ℝ → ℝ) (r eta : ℝ) : ℝ

Row S, given by ∫ x in (0 : ℝ)..r, u (x, eta) ^ 2 - scaledE R f (x, eta) ^ 2 / 2.

Equations

• NavierStokes.ShapeTransition.rowS R u f r eta = ∫ (x : ℝ) in 0..r, u (x, eta) ^ 2 - NavierStokes.ShapeTransition.scaledE R f (x, eta) ^ 2 / 2

noncomputable def NavierStokes.ShapeTransition.rowP (R : ℝ) (f : ℝ × ℝ → ℝ) (r eta : ℝ) : ℝ

Row P, given by ∫ x in (0 : ℝ)..r, scaledE R f (x, eta) ^ 2 / (2 * x).

Equations

• NavierStokes.ShapeTransition.rowP R f r eta = ∫ (x : ℝ) in 0..r, NavierStokes.ShapeTransition.scaledE R f (x, eta) ^ 2 / (2 * x)

theorem NavierStokes.ShapeTransition.sqrt_scaled_product {R x : ℝ} (hR : 0 ≤ R) (hx : 0 ≤ x) : √(2 * x) * √(2 * R * x) = 2 * √R * x

theorem NavierStokes.ShapeTransition.scaledE_sq {R x : ℝ} (hR : 0 ≤ R) (hx : 0 ≤ x) (f : ℝ × ℝ → ℝ) (eta : ℝ) : scaledE R f (x, eta) ^ 2 = 2 * R * x * f (x, eta) ^ 2

theorem NavierStokes.ShapeTransition.rowI_normalized {R r : ℝ} (hR : 0 ≤ R) (hr : 0 ≤ r) (f : ℝ × ℝ → ℝ) (eta : ℝ) : rowI R f r eta = ∫ (x : ℝ) in 0..r, 2 * √R * x * f (x, eta)

theorem NavierStokes.ShapeTransition.rowJ_normalized {R r : ℝ} (hR : 0 ≤ R) (hr : 0 ≤ r) (u f : ℝ × ℝ → ℝ) (eta : ℝ) : rowJ R u f r eta = ∫ (x : ℝ) in 0..r, 2 * √R * x * (u (x, eta) * f (x, eta))

theorem NavierStokes.ShapeTransition.rowS_normalized {R r : ℝ} (hR : 0 ≤ R) (hr : 0 ≤ r) (u f : ℝ × ℝ → ℝ) (eta : ℝ) : rowS R u f r eta = ∫ (x : ℝ) in 0..r, u (x, eta) ^ 2 - R * x * f (x, eta) ^ 2

theorem NavierStokes.ShapeTransition.rowP_normalized {R r : ℝ} (hR : 0 ≤ R) (hr : 0 ≤ r) (f : ℝ × ℝ → ℝ) (eta : ℝ) : rowP R f r eta = ∫ (x : ℝ) in 0..r, R * f (x, eta) ^ 2

theorem NavierStokes.ShapeTransition.rows_jet_bounds {R r B K C : ℝ} (hR : 0 ≤ R) (hr : 0 ≤ r) (hB : 0 ≤ B) (hK : 0 ≤ K) (hC : 0 < C) {u f : ℝ × ℝ → ℝ} (hu : ContDiff ℝ (↑⊤) u) (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (eta : ℝ) (hub : ∀ x ∈ Set.Ioc 0 r, ∀ k ≤ n, |iteratedDeriv k (fun (e : ℝ) => u (x, e)) eta| ≤ B) (hfb : ∀ x ∈ Set.Ioc 0 r, ∀ k ≤ n, |iteratedDeriv k (fun (e : ℝ) => f (x, e)) eta| ≤ K / C) : |iteratedDeriv n (rowM u r) eta| ≤ B * r ∧ |iteratedDeriv n (rowI R f r) eta| ≤ 2 * √R * (K / C) * r ^ 2 ∧ |iteratedDeriv n (rowJ R u f r) eta| ≤ 2 * √R * (2 ^ n * B * (K / C)) * r ^ 2 ∧ |iteratedDeriv n (rowS R u f r) eta| ≤ (2 ^ n * B ^ 2 + R * r * (2 ^ n * (K / C) ^ 2)) * r ∧ |iteratedDeriv n (rowP R f r) eta| ≤ R * (2 ^ n * (K / C) ^ 2) * r

All five finite-jet estimates are estimates of the actual row integrals. Only the parameter jets of the two input fields are bounded in the hypotheses.

The following coefficient contains only fixed upstream data.

noncomputable def NavierStokes.ShapeTransition.prefixCoefficient (n : ℕ) (B K L : ℝ) : ℝ

Prefix coefficient, given by B + 2 * (L + 1) * K + 2 * (L + 1) * (2 ^ n * B * K) + 2 ^ n * (B ^ 2 + L * K ^ 2).

Equations

• NavierStokes.ShapeTransition.prefixCoefficient n B K L = B + 2 * (L + 1) * K + 2 * (L + 1) * (2 ^ n * B * K) + 2 ^ n * (B ^ 2 + L * K ^ 2)

noncomputable def NavierStokes.ShapeTransition.prefixJetSize (n : ℕ) (R r : ℝ) (u f : ℝ × ℝ → ℝ) (eta : ℝ) : ℝ

Prefix jet size as an element of ℝ.

Equations

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

theorem NavierStokes.ShapeTransition.prefixJetSize_bound {R r L B K C : ℝ} (hR : 0 ≤ R) (hr : 0 ≤ r) (hr1 : r ≤ 1) (hRL : R * r = L) (hB : 0 ≤ B) (hK : 0 ≤ K) (hC : 1 ≤ C) {u f : ℝ × ℝ → ℝ} (hu : ContDiff ℝ (↑⊤) u) (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (eta : ℝ) (hub : ∀ x ∈ Set.Ioc 0 r, ∀ k ≤ n, |iteratedDeriv k (fun (e : ℝ) => u (x, e)) eta| ≤ B) (hfb : ∀ x ∈ Set.Ioc 0 r, ∀ k ≤ n, |iteratedDeriv k (fun (e : ℝ) => f (x, e)) eta| ≤ K / C) : prefixJetSize n R r u f eta ≤ prefixCoefficient n B K L * r + 2 ^ n * L * K ^ 2 / C ^ 2

theorem NavierStokes.ShapeTransition.prefix_bound_tendsto (n : ℕ) (B K L T P : ℝ) : Filter.Tendsto (fun (C : ℝ) => prefixCoefficient n B K L * separation T C P + 2 ^ n * L * K ^ 2 / C ^ 2) Filter.atTop (nhds 0)

theorem NavierStokes.ShapeTransition.eventually_small_prefix (n : ℕ) {B K Xi T P : ℝ} (hB : 0 ≤ B) (hK : 0 ≤ K) (hXi : 0 < Xi) (hP : 0 < P) (S : Set ℝ) (u f : ℝ → ℝ × ℝ → ℝ) (hu : ∀ (C : ℝ), 1 ≤ C → ContDiff ℝ (↑⊤) (u C)) (hf : ∀ (C : ℝ), 1 ≤ C → ContDiff ℝ (↑⊤) (f C)) (hub : ∀ (C : ℝ), 1 ≤ C → ∀ eta ∈ S, ∀ x ∈ Set.Ioc 0 (separation T C P), ∀ k ≤ n, |iteratedDeriv k (fun (e : ℝ) => u C (x, e)) eta| ≤ B) (hfb : ∀ (C : ℝ), 1 ≤ C → ∀ eta ∈ S, ∀ x ∈ Set.Ioc 0 (separation T C P), ∀ k ≤ n, |iteratedDeriv k (fun (e : ℝ) => f C (x, e)) eta| ≤ K / C) {eps : ℝ} (heps : 0 < eps) : ∀ᶠ (C : ℝ) in Filter.atTop, ∀ eta ∈ S, prefixJetSize n (resetRadius Xi C P) (separation T C P) (u C) (f C) eta < eps

Uniformity in the external parameter is obtained from uniform input-jet bounds. The fixed duration, data bounds, and physical prefix length precede C.

The ideal prefix has small rows too

noncomputable def NavierStokes.ShapeTransition.idealWeightI (r : ℝ) : ℝ

Ideal weight I, given by ∫ x in (0 : ℝ)..r, Real.sqrt (2 * x) * x ^ (1 / 10 : ℝ).

Equations

• NavierStokes.ShapeTransition.idealWeightI r = ∫ (x : ℝ) in 0..r, √(2 * x) * x ^ (1 / 10)

noncomputable def NavierStokes.ShapeTransition.idealWeightS (r : ℝ) : ℝ

Ideal weight S, given by ∫ x in (0 : ℝ)..r, x ^ (1 / 5 : ℝ) / 2.

Equations

• NavierStokes.ShapeTransition.idealWeightS r = ∫ (x : ℝ) in 0..r, x ^ (1 / 5) / 2

noncomputable def NavierStokes.ShapeTransition.idealWeightP (r : ℝ) : ℝ

Ideal weight P, given by ∫ x in (0 : ℝ)..r, x ^ (1 / 5 : ℝ) / (2 * x).

Equations

• NavierStokes.ShapeTransition.idealWeightP r = ∫ (x : ℝ) in 0..r, x ^ (1 / 5) / (2 * x)

theorem NavierStokes.ShapeTransition.idealWeightI_bound {r : ℝ} (hr : 0 ≤ r) (hr1 : r ≤ 1) : |idealWeightI r| ≤ 2 * r

theorem NavierStokes.ShapeTransition.idealWeightS_bound {r : ℝ} (hr : 0 ≤ r) (hr1 : r ≤ 1) : |idealWeightS r| ≤ r / 2

theorem NavierStokes.ShapeTransition.idealWeightP_eq {r : ℝ} (hr : 0 ≤ r) : idealWeightP r = 5 / 2 * r ^ (1 / 5)

noncomputable def NavierStokes.ShapeTransition.idealM (G : ℝ → ℝ) (r eta : ℝ) : ℝ

Ideal M, given by r * G eta.

Equations

• NavierStokes.ShapeTransition.idealM G r eta = r * G eta

noncomputable def NavierStokes.ShapeTransition.idealI (A : ℝ → ℝ) (r eta : ℝ) : ℝ

Ideal I, given by idealWeightI r * A eta.

Equations

• NavierStokes.ShapeTransition.idealI A r eta = NavierStokes.ShapeTransition.idealWeightI r * A eta

noncomputable def NavierStokes.ShapeTransition.idealJ (G A : ℝ → ℝ) (r eta : ℝ) : ℝ

Ideal J, given by idealWeightI r * (G eta * A eta).

Equations

• NavierStokes.ShapeTransition.idealJ G A r eta = NavierStokes.ShapeTransition.idealWeightI r * (G eta * A eta)

noncomputable def NavierStokes.ShapeTransition.idealS (G A : ℝ → ℝ) (r eta : ℝ) : ℝ

Ideal S, given by r * G eta ^ 2 - idealWeightS r * A eta ^ 2.

Equations

• NavierStokes.ShapeTransition.idealS G A r eta = r * G eta ^ 2 - NavierStokes.ShapeTransition.idealWeightS r * A eta ^ 2

noncomputable def NavierStokes.ShapeTransition.idealP (A : ℝ → ℝ) (r eta : ℝ) : ℝ

Ideal P, given by idealWeightP r * A eta ^ 2.

Equations

• NavierStokes.ShapeTransition.idealP A r eta = NavierStokes.ShapeTransition.idealWeightP r * A eta ^ 2

theorem NavierStokes.ShapeTransition.ideal_power_square {x : ℝ} (hx : 0 ≤ x) : (x ^ (1 / 10)) ^ 2 = x ^ (1 / 5)

theorem NavierStokes.ShapeTransition.ideal_rows_are_integrals {r : ℝ} (hr : 0 ≤ r) (G A : ℝ → ℝ) (eta : ℝ) : idealM G r eta = ∫ (_x : ℝ) in 0..r, G eta ∧ idealI A r eta = ∫ (x : ℝ) in 0..r, √(2 * x) * (A eta * x ^ (1 / 10)) ∧ idealJ G A r eta = ∫ (x : ℝ) in 0..r, G eta * √(2 * x) * (A eta * x ^ (1 / 10)) ∧ idealS G A r eta = ∫ (x : ℝ) in 0..r, G eta ^ 2 - (A eta * x ^ (1 / 10)) ^ 2 / 2 ∧ idealP A r eta = ∫ (x : ℝ) in 0..r, (A eta * x ^ (1 / 10)) ^ 2 / (2 * x)

noncomputable def NavierStokes.ShapeTransition.idealPrefixJetSize (n : ℕ) (r : ℝ) (G A : ℝ → ℝ) (eta : ℝ) : ℝ

Ideal prefix jet size as an element of ℝ.

Equations

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

noncomputable def NavierStokes.ShapeTransition.idealPrefixCoefficient (n : ℕ) (B K : ℝ) : ℝ

Ideal prefix coefficient, given by `B + 2 * K + 2 * (2 ^ n * B * K) + 2 ^ n * B ^ 2 + (2 ^ n

• K ^ 2) / 2`.

Equations

• NavierStokes.ShapeTransition.idealPrefixCoefficient n B K = B + 2 * K + 2 * (2 ^ n * B * K) + 2 ^ n * B ^ 2 + 2 ^ n * K ^ 2 / 2

theorem NavierStokes.ShapeTransition.idealPrefixJetSize_bound {r B K : ℝ} (hr : 0 ≤ r) (hr1 : r ≤ 1) (hB : 0 ≤ B) (hK : 0 ≤ K) {G A : ℝ → ℝ} (hG : ContDiff ℝ (↑⊤) G) (hA : ContDiff ℝ (↑⊤) A) (n : ℕ) (eta : ℝ) (hGb : ∀ k ≤ n, |iteratedDeriv k G eta| ≤ B) (hAb : ∀ k ≤ n, |iteratedDeriv k A eta| ≤ K) : idealPrefixJetSize n r G A eta ≤ idealPrefixCoefficient n B K * r + 5 / 2 * (2 ^ n * K ^ 2) * r ^ (1 / 5)

theorem NavierStokes.ShapeTransition.separation_fifth_tendsto (T : ℝ) {P : ℝ} (hP : P ≠ 0) : Filter.Tendsto (fun (C : ℝ) => separation T C P ^ (1 / 5)) Filter.atTop (nhds 0)

Genuine restoration debts on a positive compact interval

theorem NavierStokes.ShapeTransition.smooth_parameter_interval {a b : ℝ} (hab : a ≤ b) {F : ℝ × ℝ → ℝ} (hF : ∀ x ∈ Set.Icc a b, ∀ (e : ℝ), ContDiffAt ℝ (↑⊤) F (x, e)) : (ContDiff ℝ ↑⊤ fun (e : ℝ) => ∫ (x : ℝ) in a..b, F (x, e)) ∧ ∀ (n : ℕ) (e : ℝ), iteratedDeriv n (fun (q : ℝ) => ∫ (x : ℝ) in a..b, F (x, q)) e = ∫ (x : ℝ) in a..b, iteratedDeriv n (fun (q : ℝ) => F (x, q)) e

theorem NavierStokes.ShapeTransition.integral_jet_bound_on {a b B : ℝ} (hab : a ≤ b) {F : ℝ × ℝ → ℝ} (hF : ∀ x ∈ Set.Icc a b, ∀ (e : ℝ), ContDiffAt ℝ (↑⊤) F (x, e)) (n : ℕ) (eta : ℝ) (hB : ∀ x ∈ Set.Ioc a b, |iteratedDeriv n (fun (e : ℝ) => F (x, e)) eta| ≤ B) : |iteratedDeriv n (fun (e : ℝ) => ∫ (x : ℝ) in a..b, F (x, e)) eta| ≤ B * (b - a)

noncomputable def NavierStokes.ShapeTransition.restoreDefect (Gi : ℝ → ℝ) (p : ℝ × ℝ) : ℝ

Restore defect, given by restore Gi (Real.log p.1, p.2) - 4 * p.2.

Equations

• NavierStokes.ShapeTransition.restoreDefect Gi p = NavierStokes.ShapeTransition.restore Gi (Real.log p.1, p.2) - 4 * p.2

noncomputable def NavierStokes.ShapeTransition.restoreDensityJ (Gi A : ℝ → ℝ) (p : ℝ × ℝ) : ℝ

Restore density J, given by (Real.sqrt (2 * p.1) * p.1 ^ (1 / 10 : ℝ)) * (restoreDefect Gi p * A p.2).

Equations

• NavierStokes.ShapeTransition.restoreDensityJ Gi A p = √(2 * p.1) * p.1 ^ (1 / 10) * (NavierStokes.ShapeTransition.restoreDefect Gi p * A p.2)

noncomputable def NavierStokes.ShapeTransition.restoreDensityS (Gi : ℝ → ℝ) (p : ℝ × ℝ) : ℝ

Restore density S, given by restoreDefect Gi p * (restore Gi (Real.log p.1, p.2) + 4 * p.2).

Equations

• NavierStokes.ShapeTransition.restoreDensityS Gi p = NavierStokes.ShapeTransition.restoreDefect Gi p * (NavierStokes.ShapeTransition.restore Gi (Real.log p.1, p.2) + 4 * p.2)

theorem NavierStokes.ShapeTransition.restoreDensityJ_eq (Gi A : ℝ → ℝ) (p : ℝ × ℝ) : restoreDensityJ Gi A p = restore Gi (Real.log p.1, p.2) * √(2 * p.1) * (A p.2 * p.1 ^ (1 / 10)) - 4 * p.2 * √(2 * p.1) * (A p.2 * p.1 ^ (1 / 10))

theorem NavierStokes.ShapeTransition.restoreDensityS_eq (Gi : ℝ → ℝ) (p : ℝ × ℝ) : restoreDensityS Gi p = restore Gi (Real.log p.1, p.2) ^ 2 - (4 * p.2) ^ 2

theorem NavierStokes.ShapeTransition.restore_local_smooth {Gi A : ℝ → ℝ} (hGi : ContDiff ℝ (↑⊤) Gi) (hA : ContDiff ℝ (↑⊤) A) {x : ℝ} (hx : 0 < x) (eta : ℝ) : ContDiffAt ℝ (↑⊤) (restoreDefect Gi) (x, eta) ∧ ContDiffAt ℝ (↑⊤) (restoreDensityJ Gi A) (x, eta) ∧ ContDiffAt ℝ (↑⊤) (restoreDensityS Gi) (x, eta)

noncomputable def NavierStokes.ShapeTransition.restoreDebtM (Gi : ℝ → ℝ) (a b eta : ℝ) : ℝ

Restore debt M, given by ∫ x in a..b, restoreDefect Gi (x, eta).

Equations

• NavierStokes.ShapeTransition.restoreDebtM Gi a b eta = ∫ (x : ℝ) in a..b, NavierStokes.ShapeTransition.restoreDefect Gi (x, eta)

noncomputable def NavierStokes.ShapeTransition.restoreDebtJ (Gi A : ℝ → ℝ) (a b eta : ℝ) : ℝ

Restore debt J, given by ∫ x in a..b, restoreDensityJ Gi A (x, eta).

Equations

• NavierStokes.ShapeTransition.restoreDebtJ Gi A a b eta = ∫ (x : ℝ) in a..b, NavierStokes.ShapeTransition.restoreDensityJ Gi A (x, eta)

noncomputable def NavierStokes.ShapeTransition.restoreDebtS (Gi : ℝ → ℝ) (a b eta : ℝ) : ℝ

Restore debt S, given by ∫ x in a..b, restoreDensityS Gi (x, eta).

Equations

• NavierStokes.ShapeTransition.restoreDebtS Gi a b eta = ∫ (x : ℝ) in a..b, NavierStokes.ShapeTransition.restoreDensityS Gi (x, eta)

noncomputable def NavierStokes.ShapeTransition.restoreJetSize (n : ℕ) (Gi A : ℝ → ℝ) (a b eta : ℝ) : ℝ

Restore jet size as an element of ℝ.

Equations

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

theorem NavierStokes.ShapeTransition.restoreJetSize_bound {a b B K delta : ℝ} (ha : 0 < a) (hab : a ≤ b) (hb : b ≤ 1) (hB : 0 ≤ B) (hK : 0 ≤ K) (hd : 0 ≤ delta) {Gi A : ℝ → ℝ} (hGi : ContDiff ℝ (↑⊤) Gi) (hA : ContDiff ℝ (↑⊤) A) (n : ℕ) (eta : ℝ) (hgb : ∀ k ≤ n, |iteratedDeriv k (fun (e : ℝ) => 4 * e) eta| ≤ B) (habound : ∀ k ≤ n, |iteratedDeriv k A eta| ≤ K) (hdef : ∀ k ≤ n, |iteratedDeriv k (fun (e : ℝ) => Gi e - 4 * e) eta| ≤ delta) : restoreJetSize n Gi A a b eta ≤ delta * (1 + 2 * (2 ^ n * K) + 2 ^ n * (delta + 2 * B))

The angular field is unchanged during restoration; its two pure-angular rows have zero restoration debt. These are the other three actual row debts.

Subtracting the ideal rows and including restoration

theorem NavierStokes.ShapeTransition.rows_contDiff {R r : ℝ} (hR : 0 ≤ R) (hr : 0 ≤ r) {u f : ℝ × ℝ → ℝ} (hu : ContDiff ℝ (↑⊤) u) (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (rowM u r) ∧ ContDiff ℝ (↑⊤) (rowI R f r) ∧ ContDiff ℝ (↑⊤) (rowJ R u f r) ∧ ContDiff ℝ (↑⊤) (rowS R u f r) ∧ ContDiff ℝ (↑⊤) (rowP R f r)

theorem NavierStokes.ShapeTransition.ideal_rows_contDiff (r : ℝ) {G A : ℝ → ℝ} (hG : ContDiff ℝ (↑⊤) G) (hA : ContDiff ℝ (↑⊤) A) : ContDiff ℝ (↑⊤) (idealM G r) ∧ ContDiff ℝ (↑⊤) (idealI A r) ∧ ContDiff ℝ (↑⊤) (idealJ G A r) ∧ ContDiff ℝ (↑⊤) (idealS G A r) ∧ ContDiff ℝ (↑⊤) (idealP A r)

theorem NavierStokes.ShapeTransition.abs_jet_sub_add_le {F G H : ℝ → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hG : ContDiff ℝ (↑⊤) G) (hH : ContDiff ℝ (↑⊤) H) (n : ℕ) (eta : ℝ) : |iteratedDeriv n (fun (e : ℝ) => F e - G e + H e) eta| ≤ |iteratedDeriv n F eta| + |iteratedDeriv n G eta| + |iteratedDeriv n H eta|

theorem NavierStokes.ShapeTransition.abs_jet_sub_le {F G : ℝ → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hG : ContDiff ℝ (↑⊤) G) (n : ℕ) (eta : ℝ) : |iteratedDeriv n (fun (e : ℝ) => F e - G e) eta| ≤ |iteratedDeriv n F eta| + |iteratedDeriv n G eta|

noncomputable def NavierStokes.ShapeTransition.resetDebtM (u : ℝ × ℝ → ℝ) (Gi : ℝ → ℝ) (r b eta : ℝ) : ℝ

Reset debt M, given by rowM u r eta - idealM (fun e => 4 * e) r eta + restoreDebtM Gi r b eta.

Equations

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

noncomputable def NavierStokes.ShapeTransition.resetDebtI (R : ℝ) (f : ℝ × ℝ → ℝ) (A : ℝ → ℝ) (r eta : ℝ) : ℝ

Reset debt I, given by rowI R f r eta - idealI A r eta.

Equations

• NavierStokes.ShapeTransition.resetDebtI R f A r eta = NavierStokes.ShapeTransition.rowI R f r eta - NavierStokes.ShapeTransition.idealI A r eta

noncomputable def NavierStokes.ShapeTransition.resetDebtJ (R : ℝ) (u f : ℝ × ℝ → ℝ) (Gi A : ℝ → ℝ) (r b eta : ℝ) : ℝ

Reset debt J, given by rowJ R u f r eta - idealJ (fun e => 4 * e) A r eta + restoreDebtJ Gi A r b eta.

Equations

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

noncomputable def NavierStokes.ShapeTransition.resetDebtS (R : ℝ) (u f : ℝ × ℝ → ℝ) (Gi A : ℝ → ℝ) (r b eta : ℝ) : ℝ

Reset debt S, given by rowS R u f r eta - idealS (fun e => 4 * e) A r eta + restoreDebtS Gi r b eta.

Equations

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

noncomputable def NavierStokes.ShapeTransition.resetDebtP (R : ℝ) (f : ℝ × ℝ → ℝ) (A : ℝ → ℝ) (r eta : ℝ) : ℝ

Reset debt P, given by rowP R f r eta - idealP A r eta.

Equations

• NavierStokes.ShapeTransition.resetDebtP R f A r eta = NavierStokes.ShapeTransition.rowP R f r eta - NavierStokes.ShapeTransition.idealP A r eta

noncomputable def NavierStokes.ShapeTransition.resetDebtJetSize (n : ℕ) (R r b : ℝ) (u f : ℝ × ℝ → ℝ) (Gi A : ℝ → ℝ) (eta : ℝ) : ℝ

Reset debt jet size as an element of ℝ.

Equations

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

theorem NavierStokes.ShapeTransition.resetDebtJetSize_le_parts {R r b : ℝ} (hR : 0 ≤ R) (hr : 0 < r) (hrb : r ≤ b) {u f : ℝ × ℝ → ℝ} {Gi A : ℝ → ℝ} (hu : ContDiff ℝ (↑⊤) u) (hf : ContDiff ℝ (↑⊤) f) (hGi : ContDiff ℝ (↑⊤) Gi) (hA : ContDiff ℝ (↑⊤) A) (n : ℕ) (eta : ℝ) : resetDebtJetSize n R r b u f Gi A eta ≤ prefixJetSize n R r u f eta + idealPrefixJetSize n r (fun (e : ℝ) => 4 * e) A eta + restoreJetSize n Gi A r b eta

noncomputable def NavierStokes.ShapeTransition.vanishingDebtBound (n : ℕ) (B K L BG KA r C : ℝ) : ℝ

Vanishing debt bound as an element of ℝ.

Equations

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

noncomputable def NavierStokes.ShapeTransition.restorationBound (n : ℕ) (BG KA delta : ℝ) : ℝ

Restoration bound, given by delta * (1 + 2 * (2 ^ n * KA) + 2 ^ n * (delta + 2 * BG)).

Equations

• NavierStokes.ShapeTransition.restorationBound n BG KA delta = delta * (1 + 2 * (2 ^ n * KA) + 2 ^ n * (delta + 2 * BG))

theorem NavierStokes.ShapeTransition.resetDebtJetSize_bound {R r b L B K C BG KA delta : ℝ} (hR : 0 ≤ R) (hr : 0 < r) (hrb : r ≤ b) (hb : b ≤ 1) (hRL : R * r = L) (hB : 0 ≤ B) (hK : 0 ≤ K) (hC : 1 ≤ C) (hBG : 0 ≤ BG) (hKA : 0 ≤ KA) (hd : 0 ≤ delta) {u f : ℝ × ℝ → ℝ} {Gi A : ℝ → ℝ} (hu : ContDiff ℝ (↑⊤) u) (hf : ContDiff ℝ (↑⊤) f) (hGi : ContDiff ℝ (↑⊤) Gi) (hA : ContDiff ℝ (↑⊤) A) (n : ℕ) (eta : ℝ) (hub : ∀ x ∈ Set.Ioc 0 r, ∀ k ≤ n, |iteratedDeriv k (fun (e : ℝ) => u (x, e)) eta| ≤ B) (hfb : ∀ x ∈ Set.Ioc 0 r, ∀ k ≤ n, |iteratedDeriv k (fun (e : ℝ) => f (x, e)) eta| ≤ K / C) (hgb : ∀ k ≤ n, |iteratedDeriv k (fun (e : ℝ) => 4 * e) eta| ≤ BG) (habound : ∀ k ≤ n, |iteratedDeriv k A eta| ≤ KA) (hdef : ∀ k ≤ n, |iteratedDeriv k (fun (e : ℝ) => Gi e - 4 * e) eta| ≤ delta) : resetDebtJetSize n R r b u f Gi A eta ≤ vanishingDebtBound n B K L BG KA r C + restorationBound n BG KA delta

theorem NavierStokes.ShapeTransition.vanishingDebtBound_tendsto (n : ℕ) (B K L BG KA T : ℝ) {P : ℝ} (hP : P ≠ 0) : Filter.Tendsto (fun (C : ℝ) => vanishingDebtBound n B K L BG KA (separation T C P) C) Filter.atTop (nhds 0)

theorem NavierStokes.ShapeTransition.eventually_vanishingDebtBound_lt (n : ℕ) (B K L BG KA T : ℝ) {P eps : ℝ} (hP : P ≠ 0) (heps : 0 < eps) : ∀ᶠ (C : ℝ) in Filter.atTop, vanishingDebtBound n B K L BG KA (separation T C P) C < eps

Increasing C removes only the prefix term. The explicit restoration term is retained, so the upstream smallness choice is not silently changed.

Direct adapter from axis and entry jets to the constructed prefix

noncomputable def NavierStokes.ShapeTransition.shapeJetConstant (n : ℕ) (Xi T B K : ℝ) : ℝ

Shape jet constant, given by K + (n.factorial * Real.exp (T / 10 + B) * B ^ n) / Real.sqrt (2 * Xi).

Equations

• NavierStokes.ShapeTransition.shapeJetConstant n Xi T B K = K + ↑n.factorial * Real.exp (T / 10 + B) * B ^ n / √(2 * Xi)

theorem NavierStokes.ShapeTransition.shapeJetConstant_nonneg (n : ℕ) {Xi T B K : ℝ} (hB : 0 ≤ B) (hK : 0 ≤ K) : 0 ≤ shapeJetConstant n Xi T B K

theorem NavierStokes.ShapeTransition.shapeField_jets_uniform {Xi C T X B K : ℝ} (hXi : 0 < Xi) (hC : 0 < C) (hT : 0 < T) (hX : 0 ≤ X) (hXL : X ≤ Xi * Real.exp T) {li : ℝ → ℝ} {old : ℝ × ℝ → ℝ} (hli : ContDiff ℝ (↑⊤) li) (hB : 1 ≤ B) (hK : 0 ≤ K) (n : ℕ) (eta : ℝ) (hAxis : X ≤ Xi → ∀ k ≤ n, |iteratedDeriv k (fun (e : ℝ) => old (X, e)) eta| ≤ K / C) (hHold : Xi ≤ X → ∀ (e : ℝ), old (X, e) = C⁻¹ * Real.exp (Real.log (X / Xi) / 10 + li e) / √(2 * X)) (hl : ∀ i ≤ n, |iteratedDeriv i li eta| ≤ B) (hf : ∀ i ≤ n, |iteratedDeriv i logShape eta| ≤ B) (k : ℕ) : k ≤ n → |iteratedDeriv k (fun (e : ℝ) => shapeField Xi T li old (X, e)) eta| ≤ shapeJetConstant n Xi T B K / C

noncomputable def NavierStokes.ShapeTransition.scaledFamily (R : ℝ) (F : ℝ × ℝ → ℝ) (p : ℝ × ℝ) : ℝ

Scaled family, given by F (R * p.1, p.2).

Equations

• NavierStokes.ShapeTransition.scaledFamily R F p = F (R * p.1, p.2)

theorem NavierStokes.ShapeTransition.scaledFamily_contDiff (R : ℝ) {F : ℝ × ℝ → ℝ} (hF : ContDiff ℝ (↑⊤) F) : ContDiff ℝ (↑⊤) (scaledFamily R F)

theorem NavierStokes.ShapeTransition.constructed_prefix_bound {Xi C T P B BJ K : ℝ} (hXi : 0 < Xi) (hC : 1 ≤ C) (hT : 0 < T) (hP : 0 < P) (hB : 0 ≤ B) (hBJ : 1 ≤ BJ) (hK : 0 ≤ K) {li Gi : ℝ → ℝ} {oldU oldF : ℝ × ℝ → ℝ} (hli : ContDiff ℝ (↑⊤) li) (hU : ContDiff ℝ (↑⊤) oldU) (hF : ContDiff ℝ (↑⊤) oldF) (n : ℕ) (eta : ℝ) (hsep : separation T C P ≤ 1) (hAxisU : ∀ X ∈ Set.Icc 0 Xi, ∀ k ≤ n, |iteratedDeriv k (fun (e : ℝ) => oldU (X, e)) eta| ≤ B) (hGi : ∀ k ≤ n, |iteratedDeriv k Gi eta| ≤ B) (hHoldU : ∀ (X : ℝ), Xi ≤ X → ∀ (e : ℝ), oldU (X, e) = Gi e) (hAxisF : ∀ X ∈ Set.Icc 0 Xi, ∀ k ≤ n, |iteratedDeriv k (fun (e : ℝ) => oldF (X, e)) eta| ≤ K / C) (hHoldF : ∀ (X : ℝ), Xi ≤ X → ∀ (e : ℝ), oldF (X, e) = C⁻¹ * Real.exp (Real.log (X / Xi) / 10 + li e) / √(2 * X)) (hl : ∀ i ≤ n, |iteratedDeriv i li eta| ≤ BJ) (hshape : ∀ i ≤ n, |iteratedDeriv i logShape eta| ≤ BJ) : prefixJetSize n (resetRadius Xi C P) (separation T C P) (scaledFamily (resetRadius Xi C P) oldU) (scaledFamily (resetRadius Xi C P) (shapeField Xi T li oldF)) eta ≤ prefixCoefficient n B (shapeJetConstant n Xi T BJ K) (Xi * Real.exp T) * separation T C P + 2 ^ n * (Xi * Real.exp T) * shapeJetConstant n Xi T BJ K ^ 2 / C ^ 2

This theorem assumes axis-field jets and the held entry power law, then derives the actual constructed prefix-row estimates. No row-smallness hypothesis occurs. The constant shapeJetConstant is independent of C.

theorem NavierStokes.ShapeTransition.integral_debt_split {r b : ℝ} {F G : ℝ → ℝ} (hF0 : IntervalIntegrable F MeasureTheory.volume 0 r) (hFr : IntervalIntegrable F MeasureTheory.volume r b) (hG0 : IntervalIntegrable G MeasureTheory.volume 0 r) (hGr : IntervalIntegrable G MeasureTheory.volume r b) : ∫ (x : ℝ) in 0..b, F x - G x = ((∫ (x : ℝ) in 0..r, F x) - ∫ (x : ℝ) in 0..r, G x) + ∫ (x : ℝ) in r..b, F x - G x

The row-debt decomposition used above is the ordinary split of actual integrals at the separation radius.