Quantitative bounds for the actual five-row matching debt

The vanishing rescaled prefix and the drift of the held axial endpoint are estimated separately. All parameter derivatives below are actual derivatives of the constructed fields and their moment integrals.

@[reducible, inline]

abbrev NavierStokes.MatchingDebtBounds.Point : Type

Point: an abbreviation for ℝ × ℝ.

Equations

• NavierStokes.MatchingDebtBounds.Point = (ℝ × ℝ)

@[reducible, inline]

abbrev NavierStokes.MatchingDebtBounds.Field : Type

Field: an abbreviation for Point → ℝ.

Equations

• NavierStokes.MatchingDebtBounds.Field = (NavierStokes.MatchingDebtBounds.Point → ℝ)

@[reducible, inline]

abbrev NavierStokes.MatchingDebtBounds.Debt : Type

Debt: an abbreviation for FiveProfileMoments.Debt.

Equations

• NavierStokes.MatchingDebtBounds.Debt = NavierStokes.FiveProfileMoments.Debt

Smooth extensions which preserve the entire parameter germ

The incoming fields are smooth on their natural open strip. These explicit retractions allow the global smooth integral estimates to be used without assuming a global extension as additional data.

noncomputable def NavierStokes.MatchingDebtBounds.parameterClamp (eta : ℝ) : ℝ

Parameter clamp, given by eta * (1 - OutgoingSchedule.sigma (20 * (eta ^ 2 - 1) - 1)).

Equations

• NavierStokes.MatchingDebtBounds.parameterClamp eta = eta * (1 - NavierStokes.OutgoingSchedule.sigma (20 * (eta ^ 2 - 1) - 1))

theorem NavierStokes.MatchingDebtBounds.parameterClamp_smooth : ContDiff ℝ (↑⊤) parameterClamp

theorem NavierStokes.MatchingDebtBounds.parameterClamp_eq {eta : ℝ} (h : eta ^ 2 ≤ 21 / 20) : parameterClamp eta = eta

theorem NavierStokes.MatchingDebtBounds.parameterClamp_mem (eta : ℝ) : parameterClamp eta ∈ ReferencePath.parameterInterval

theorem NavierStokes.MatchingDebtBounds.parameterClamp_eventuallyEq {eta : ℝ} (hη : eta ∈ Set.Icc (-1) 1) : parameterClamp =ᶠ[nhds eta] id

noncomputable def NavierStokes.MatchingDebtBounds.radialClamp (scale X : ℝ) : ℝ

Radial clamp, given by X * OutgoingSchedule.sigma (scale * X + 2).

Equations

• NavierStokes.MatchingDebtBounds.radialClamp scale X = X * NavierStokes.OutgoingSchedule.sigma (scale * X + 2)

theorem NavierStokes.MatchingDebtBounds.radialClamp_smooth (scale : ℝ) : ContDiff ℝ (↑⊤) (radialClamp scale)

theorem NavierStokes.MatchingDebtBounds.radialClamp_eq {scale X : ℝ} (hscale : 0 < scale) (hX : 0 ≤ X) : radialClamp scale X = X

theorem NavierStokes.MatchingDebtBounds.radialClamp_mem {scale : ℝ} (hscale : 0 < scale) (X : ℝ) : -20 < scale * radialClamp scale X

noncomputable def NavierStokes.MatchingDebtBounds.strip (scale : ℝ) : Set Point

Strip, given by {p | -20 < scale * p.1 ∧ p.2 ∈ ReferencePath.parameterInterval}.

Equations

• NavierStokes.MatchingDebtBounds.strip scale = {p : NavierStokes.MatchingDebtBounds.Point | -20 < scale * p.1 ∧ p.2 ∈ NavierStokes.ReferencePath.parameterInterval}

theorem NavierStokes.MatchingDebtBounds.strip_open (scale : ℝ) : IsOpen (strip scale)

noncomputable def NavierStokes.MatchingDebtBounds.extendParameter (g : ℝ → ℝ) (eta : ℝ) : ℝ

Extend parameter, given by g (parameterClamp eta).

Equations

• NavierStokes.MatchingDebtBounds.extendParameter g eta = g (NavierStokes.MatchingDebtBounds.parameterClamp eta)

noncomputable def NavierStokes.MatchingDebtBounds.extendField (scale : ℝ) (f : Field) (p : Point) : ℝ

Extend field, given by f (radialClamp scale p.1, parameterClamp p.2).

Equations

• NavierStokes.MatchingDebtBounds.extendField scale f p = f (NavierStokes.MatchingDebtBounds.radialClamp scale p.1, NavierStokes.MatchingDebtBounds.parameterClamp p.2)

theorem NavierStokes.MatchingDebtBounds.extendParameter_smooth {g : ℝ → ℝ} (hg : ContDiffOn ℝ (↑⊤) g ReferencePath.parameterInterval) : ContDiff ℝ (↑⊤) (extendParameter g)

theorem NavierStokes.MatchingDebtBounds.extendField_smooth {scale : ℝ} (hscale : 0 < scale) {f : Field} (hf : ContDiffOn ℝ (↑⊤) f (strip scale)) : ContDiff ℝ (↑⊤) (extendField scale f)

theorem NavierStokes.MatchingDebtBounds.extendParameter_eventuallyEq {eta : ℝ} (hη : eta ∈ Set.Icc (-1) 1) (g : ℝ → ℝ) : extendParameter g =ᶠ[nhds eta] g

theorem NavierStokes.MatchingDebtBounds.extendField_slice_eventuallyEq {scale X eta : ℝ} (hscale : 0 < scale) (hX : 0 ≤ X) (hη : eta ∈ Set.Icc (-1) 1) (f : Field) : (fun (e : ℝ) => extendField scale f (X, e)) =ᶠ[nhds eta] fun (e : ℝ) => f (X, e)

The actual five-row vector and its jets

noncomputable def NavierStokes.MatchingDebtBounds.resetVector (R r b : ℝ) (u f : Field) (Gi A : ℝ → ℝ) (eta : ℝ) : Debt

Reset vector as an element of Debt.

Equations

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

theorem NavierStokes.MatchingDebtBounds.resetVector_smooth {R r b : ℝ} (hR : 0 ≤ R) (hr : 0 < r) (hrb : r ≤ b) {u f : Field} {Gi A : ℝ → ℝ} (hu : ContDiff ℝ (↑⊤) u) (hf : ContDiff ℝ (↑⊤) f) (hGi : ContDiff ℝ (↑⊤) Gi) (hA : ContDiff ℝ (↑⊤) A) : ContDiff ℝ (↑⊤) (resetVector R r b u f Gi A)

theorem NavierStokes.MatchingDebtBounds.iteratedDeriv_component {d : ℝ → Debt} (hd : ContDiff ℝ (↑⊤) d) (n : ℕ) (eta : ℝ) (i : Fin 5) : iteratedDeriv n d eta i = iteratedDeriv n (fun (e : ℝ) => d e i) eta

theorem NavierStokes.MatchingDebtBounds.vector_jet_le_sum {d : ℝ → Debt} (hd : ContDiff ℝ (↑⊤) d) (n : ℕ) (eta : ℝ) : ‖iteratedFDeriv ℝ n d eta‖ ≤ ∑ i : Fin 5, |iteratedDeriv n (fun (e : ℝ) => d e i) eta|

theorem NavierStokes.MatchingDebtBounds.resetVector_jet_bound {R r b : ℝ} (hR : 0 ≤ R) (hr : 0 < r) (hrb : r ≤ b) {u f : Field} {Gi A : ℝ → ℝ} (hu : ContDiff ℝ (↑⊤) u) (hf : ContDiff ℝ (↑⊤) f) (hGi : ContDiff ℝ (↑⊤) Gi) (hA : ContDiff ℝ (↑⊤) A) (n : ℕ) (eta : ℝ) : ‖iteratedFDeriv ℝ n (resetVector R r b u f Gi A) eta‖ ≤ ShapeTransition.resetDebtJetSize n R r b u f Gi A eta

theorem NavierStokes.MatchingDebtBounds.resetVector_congr {R r b eta : ℝ} (hr : 0 ≤ r) {u₁ u₂ f₁ f₂ : Field} {Gi₁ Gi₂ A : ℝ → ℝ} (hu : ∀ x ∈ Set.Icc 0 r, u₁ (x, eta) = u₂ (x, eta)) (hf : ∀ x ∈ Set.Icc 0 r, f₁ (x, eta) = f₂ (x, eta)) (hG : Gi₁ eta = Gi₂ eta) : resetVector R r b u₁ f₁ Gi₁ A eta = resetVector R r b u₂ f₂ Gi₂ A eta

noncomputable def NavierStokes.MatchingDebtBounds.extendedU {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) : Field

Extended U, given by ShapeTransition.scaledFamily c.radius (extendField A.scale c.seedU).

Equations

• NavierStokes.MatchingDebtBounds.extendedU c = NavierStokes.ShapeTransition.scaledFamily c.radius (NavierStokes.MatchingDebtBounds.extendField A.scale c.seedU)

noncomputable def NavierStokes.MatchingDebtBounds.extendedF {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) : Field

Extended F, constructed using ShapeTransition.scaledFamily.

Equations

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

noncomputable def NavierStokes.MatchingDebtBounds.extendedDebt {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) : ℝ → Debt

Extended debt, constructed using resetVector.

Equations

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

theorem NavierStokes.MatchingDebtBounds.extendedU_smooth {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) : ContDiff ℝ (↑⊤) (extendedU c)

theorem NavierStokes.MatchingDebtBounds.extendedF_smooth {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) : ContDiff ℝ (↑⊤) (extendedF c)

theorem NavierStokes.MatchingDebtBounds.extendedDebt_smooth {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) (hsep : c.separation ≤ Real.exp (-8)) : ContDiff ℝ (↑⊤) (extendedDebt c)

theorem NavierStokes.MatchingDebtBounds.extendedDebt_eventuallyEq {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) {eta : ℝ} (hη : eta ∈ Set.Icc (-1) 1) : extendedDebt c =ᶠ[nhds eta] c.manuscriptDebt

theorem NavierStokes.MatchingDebtBounds.debt_eventuallyEq_negative_extended {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) (hsep : c.separation ≤ Real.exp (-8)) {eta : ℝ} (hη : eta ∈ Set.Icc (-1) 1) : c.debt =ᶠ[nhds eta] fun (e : ℝ) => -extendedDebt c e

structure NavierStokes.MatchingDebtBounds.SeedJets {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) (N : ℕ) (B K BJ : ℝ) : Prop

Bounds on actual seed fields, before the shape modification or any moment integration. They are supplied below by ordered_seed_bounds.

• axial (X : ℝ) : 0 ≤ X → ∀ eta ∈ Set.Icc (-1) 1, ∀ n ≤ N, |iteratedDeriv n (fun (e : ℝ) => c.seedU (X, e)) eta| ≤ B
• angular (X : ℝ) : 0 ≤ X → ∀ eta ∈ Set.Icc (-1) 1, ∀ n ≤ N, |iteratedDeriv n (fun (e : ℝ) => c.seedF (X, e)) eta| ≤ K / A.normalization
• logarithm (eta : ℝ) : eta ∈ Set.Icc (-1) 1 → ∀ n ≤ N, |iteratedDeriv n c.initialShape eta| ≤ BJ

theorem NavierStokes.MatchingDebtBounds.radius_mul_separation {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) : c.radius * c.separation = NominalProfile.Xi * Real.exp c.shapeTime

theorem NavierStokes.MatchingDebtBounds.extendedU_jets {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) {N : ℕ} {B K BJ : ℝ} (hj : SeedJets c N B K BJ) {eta x : ℝ} (hη : eta ∈ Set.Icc (-1) 1) (hx : 0 ≤ x) {n : ℕ} (hn : n ≤ N) : |iteratedDeriv n (fun (e : ℝ) => extendedU c (x, e)) eta| ≤ B

theorem NavierStokes.MatchingDebtBounds.extendedF_jets {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) {N : ℕ} {B K BJ : ℝ} (hj : SeedJets c N B K BJ) (hBJ : 1 ≤ BJ) (hK : 0 ≤ K) (hshape : ∀ eta ∈ Set.Icc (-1) 1, ∀ n ≤ N, |iteratedDeriv n ShapeTransition.logShape eta| ≤ BJ) {eta x : ℝ} (hη : eta ∈ Set.Icc (-1) 1) (hx : x ∈ Set.Icc 0 c.separation) {n : ℕ} (hn : n ≤ N) : |iteratedDeriv n (fun (e : ℝ) => extendedF c (x, e)) eta| ≤ ShapeTransition.shapeJetConstant N NominalProfile.Xi c.shapeTime BJ K / A.normalization

theorem NavierStokes.MatchingDebtBounds.extendedDebt_bound {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) {N : ℕ} {B K BJ BG KA delta : ℝ} (hj : SeedJets c N B K BJ) (hB : 0 ≤ B) (hK : 0 ≤ K) (hBJ : 1 ≤ BJ) (hBG : 0 ≤ BG) (hKA : 0 ≤ KA) (hd : 0 ≤ delta) (hC : 1 ≤ A.normalization) (hsep : c.separation ≤ Real.exp (-8)) (hshape : ∀ eta ∈ Set.Icc (-1) 1, ∀ n ≤ N, |iteratedDeriv n ShapeTransition.logShape eta| ≤ BJ) (hG : ∀ eta ∈ Set.Icc (-1) 1, ∀ n ≤ N, |iteratedDeriv n (fun (e : ℝ) => 4 * e) eta| ≤ BG) (hA : ∀ eta ∈ Set.Icc (-1) 1, ∀ n ≤ N, |iteratedDeriv n (NominalProfile.idealAmplitude F) eta| ≤ KA) (hdef : ∀ eta ∈ Set.Icc (-1) 1, ∀ n ≤ N, |iteratedDeriv n (fun (e : ℝ) => c.initialAxial e - 4 * e) eta| ≤ delta) {n : ℕ} (hn : n ≤ N) {eta : ℝ} (hη : eta ∈ Set.Icc (-1) 1) : ‖iteratedFDeriv ℝ n (extendedDebt c) eta‖ ≤ ShapeTransition.vanishingDebtBound n B (ShapeTransition.shapeJetConstant N NominalProfile.Xi c.shapeTime BJ K) (NominalProfile.Xi * Real.exp c.shapeTime) BG KA c.separation A.normalization + ShapeTransition.restorationBound n BG KA delta

A finite-order budget, with separate vanishing and drift terms

noncomputable def NavierStokes.MatchingDebtBounds.vanishingSum (N : ℕ) (B K L BG KA T P C : ℝ) : ℝ

Vanishing sum, given by ∑ n ∈ Finset.range (N + 1), |ShapeTransition.vanishingDebtBound n B K L BG KA (ShapeTransition.separation T C P) C|.

Equations

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

theorem NavierStokes.MatchingDebtBounds.vanishingSum_nonneg (N : ℕ) (B K L BG KA T P C : ℝ) : 0 ≤ vanishingSum N B K L BG KA T P C

theorem NavierStokes.MatchingDebtBounds.vanishing_le_sum {N n : ℕ} (hn : n ≤ N) (B K L BG KA T P C : ℝ) : ShapeTransition.vanishingDebtBound n B K L BG KA (ShapeTransition.separation T C P) C ≤ vanishingSum N B K L BG KA T P C

theorem NavierStokes.MatchingDebtBounds.vanishingSum_tendsto (N : ℕ) (B K L BG KA T : ℝ) {P : ℝ} (hP : P ≠ 0) : Filter.Tendsto (vanishingSum N B K L BG KA T P) Filter.atTop (nhds 0)

noncomputable def NavierStokes.MatchingDebtBounds.driftFactor (N : ℕ) (BG KA : ℝ) : ℝ

Drift factor, given by 1 + 2 * (2 ^ N * KA) + 2 ^ N * (1 + 2 * BG).

Equations

• NavierStokes.MatchingDebtBounds.driftFactor N BG KA = 1 + 2 * (2 ^ N * KA) + 2 ^ N * (1 + 2 * BG)

theorem NavierStokes.MatchingDebtBounds.driftFactor_pos (N : ℕ) {BG KA : ℝ} (hBG : 0 ≤ BG) (hKA : 0 ≤ KA) : 0 < driftFactor N BG KA

theorem NavierStokes.MatchingDebtBounds.restoration_le_linear {N n : ℕ} (hn : n ≤ N) {BG KA delta : ℝ} (hBG : 0 ≤ BG) (hKA : 0 ≤ KA) (hd : 0 ≤ delta) (hd1 : delta ≤ 1) : ShapeTransition.restorationBound n BG KA delta ≤ delta * driftFactor N BG KA

theorem NavierStokes.MatchingDebtBounds.compact_scalar_jets {g : ℝ → ℝ} (hg : ContDiff ℝ (↑⊤) g) (N : ℕ) : ∃ (B : ℝ), 1 ≤ B ∧ ∀ eta ∈ Set.Icc (-1) 1, ∀ n ≤ N, |iteratedDeriv n g eta| ≤ B

structure NavierStokes.MatchingDebtBounds.FixedBounds (F : OutgoingProfile.Profile) (N : ℕ) : Type

These constants depend only on the already fixed outgoing witness and the requested finite order. In particular they precede j, Λ, and C.

• normalizer : ℝ

  Normalizer of FixedBounds, of type ℝ.

• normalizer_pos : 0 < self.normalizer
• normalize (d : ℝ → Debt) : ContDiff ℝ (↑⊤) d → ∀ (D : ℝ), 0 ≤ D → JetBounds.FiniteJetBound N d (Set.Icc (-1) 1) D → JetBounds.FiniteJetBound N (NominalProfile.normalizedDebt F d) (Set.Icc (-1) 1) (self.normalizer * D)
• axial : ℝ

  Axial of FixedBounds, of type ℝ.

• angular : ℝ

  Angular of FixedBounds, of type ℝ.

• logarithm : ℝ

  Logarithm of FixedBounds, of type ℝ.

• axial_one : 1 ≤ self.axial
• angular_one : 1 ≤ self.angular
• logarithm_one : 1 ≤ self.logarithm
• axial_jets (eta : ℝ) : eta ∈ Set.Icc (-1) 1 → ∀ n ≤ N, |iteratedDeriv n (fun (e : ℝ) => 4 * e) eta| ≤ self.axial
• angular_jets (eta : ℝ) : eta ∈ Set.Icc (-1) 1 → ∀ n ≤ N, |iteratedDeriv n (NominalProfile.idealAmplitude F) eta| ≤ self.angular
• logarithm_jets (eta : ℝ) : eta ∈ Set.Icc (-1) 1 → ∀ n ≤ N, |iteratedDeriv n ShapeTransition.logShape eta| ≤ self.logarithm

theorem NavierStokes.MatchingDebtBounds.fixedBounds_exists (F : OutgoingProfile.Profile) (N : ℕ) : Nonempty (FixedBounds F N)

noncomputable def NavierStokes.MatchingDebtBounds.fixedBounds (F : OutgoingProfile.Profile) (N : ℕ) : FixedBounds F N

Fixed bounds, given by Classical.choice (fixedBounds_exists F N).

Equations

• NavierStokes.MatchingDebtBounds.fixedBounds F N = Classical.choice ⋯

noncomputable def NavierStokes.MatchingDebtBounds.prefixBudget {F : OutgoingProfile.Profile} {N : ℕ} (q : FixedBounds F N) (B K BJ T C : ℝ) : ℝ

Prefix budget, constructed using vanishingSum.

Equations

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

theorem NavierStokes.MatchingDebtBounds.prefixBudget_nonneg {F : OutgoingProfile.Profile} {N : ℕ} (q : FixedBounds F N) (B K BJ T C : ℝ) : 0 ≤ prefixBudget q B K BJ T C

theorem NavierStokes.MatchingDebtBounds.prefixBudget_tendsto {F : OutgoingProfile.Profile} {N : ℕ} (q : FixedBounds F N) (B K BJ T : ℝ) : Filter.Tendsto (prefixBudget q B K BJ T) Filter.atTop (nhds 0)

theorem NavierStokes.MatchingDebtBounds.normalized_actual_debt_bound {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) {N : ℕ} (q : FixedBounds F N) {B K BJ delta : ℝ} (hj : SeedJets c N B K BJ) (hB : 0 ≤ B) (hK : 0 ≤ K) (hBJ : 1 ≤ BJ) (hqJ : q.logarithm ≤ BJ) (hd : 0 ≤ delta) (hd1 : delta ≤ 1) (hC : 1 ≤ A.normalization) (hsep : c.separation ≤ Real.exp (-8)) (hdef : ∀ eta ∈ Set.Icc (-1) 1, ∀ n ≤ N, |iteratedDeriv n (fun (e : ℝ) => c.initialAxial e - 4 * e) eta| ≤ delta) : JetBounds.FiniteJetBound N (NominalProfile.normalizedDebt F c.debt) (Set.Icc (-1) 1) (q.normalizer * (prefixBudget q B K BJ c.shapeTime A.normalization + delta * driftFactor N q.axial q.angular))

noncomputable def NavierStokes.MatchingDebtBounds.SmallControl {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) (N : ℕ) (eps : ℝ) : Prop

Small control, given by c.reference.SmallLogControl (Icc (-1 : ℝ) 1) N eps c.activationTime c.kappa c.axialWidth c.angularWidth.

Equations

• NavierStokes.MatchingDebtBounds.SmallControl c N eps = c.reference.SmallLogControl (Set.Icc (-1) 1) N eps c.activationTime c.kappa c.axialWidth c.angularWidth

theorem NavierStokes.MatchingDebtBounds.SmallControl.mono {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} {c : NominalProfile.Controls A} {N : ℕ} {eps eps' : ℝ} (hc : SmallControl c N eps) (he : eps ≤ eps') : SmallControl c N eps'

theorem NavierStokes.MatchingDebtBounds.SmallControl.of_le {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} {c : NominalProfile.Controls A} {N M : ℕ} {eps : ℝ} (hc : SmallControl c M eps) (hNM : N ≤ M) : SmallControl c N eps

theorem NavierStokes.MatchingDebtBounds.actual_endpoint_drift {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) {N : ℕ} {eps : ℝ} (hc : SmallControl c N eps) {eta : ℝ} (hη : eta ∈ Set.Icc (-1) 1) {n : ℕ} (hn : n ≤ N) : |iteratedDeriv n (fun (e : ℝ) => c.initialAxial e - 4 * e) eta| ≤ ReferenceJetBounds.jetConstant A.preparation.inputs.coefficients 0 n / A.scale + eps + |A.j|

noncomputable def NavierStokes.MatchingDebtBounds.driftBudget {F : OutgoingProfile.Profile} {N : ℕ} (q : FixedBounds F N) (rho : ℝ) : ℝ

Drift budget, given by min 1 (rho / (4 * (q.normalizer * driftFactor N q.axial q.angular))).

Equations

• NavierStokes.MatchingDebtBounds.driftBudget q rho = min 1 (rho / (4 * (q.normalizer * NavierStokes.MatchingDebtBounds.driftFactor N q.axial q.angular)))

theorem NavierStokes.MatchingDebtBounds.driftBudget_pos {F : OutgoingProfile.Profile} {N : ℕ} (q : FixedBounds F N) {rho : ℝ} (hrho : 0 < rho) : 0 < driftBudget q rho

theorem NavierStokes.MatchingDebtBounds.driftBudget_le_one {F : OutgoingProfile.Profile} {N : ℕ} (q : FixedBounds F N) (rho : ℝ) : driftBudget q rho ≤ 1

theorem NavierStokes.MatchingDebtBounds.driftBudget_weighted {F : OutgoingProfile.Profile} {N : ℕ} (q : FixedBounds F N) (rho : ℝ) : q.normalizer * (driftBudget q rho * driftFactor N q.axial q.angular) ≤ rho / 4

theorem NavierStokes.MatchingDebtBounds.normalized_debt_small_of_budgets {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) {N : ℕ} (q : FixedBounds F N) {B K BJ rho : ℝ} (hj : SeedJets c N B K BJ) (hB : 0 ≤ B) (hK : 0 ≤ K) (hBJ : 1 ≤ BJ) (hqJ : q.logarithm ≤ BJ) (hrho : 0 < rho) (hC : 1 ≤ A.normalization) (hsep : c.separation ≤ Real.exp (-8)) (hp : prefixBudget q B K BJ c.shapeTime A.normalization < rho / (4 * q.normalizer)) (hdef : ∀ eta ∈ Set.Icc (-1) 1, ∀ n ≤ N, |iteratedDeriv n (fun (e : ℝ) => c.initialAxial e - 4 * e) eta| ≤ driftBudget q rho) (n : ℕ) : n ≤ N → ∀ eta ∈ Set.Icc (-1) 1, ‖iteratedFDeriv ℝ n (NominalProfile.normalizedDebt F c.debt) eta‖ < rho

structure NavierStokes.MatchingDebtBounds.MatchingBounds {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) (N : ℕ) (rho : ℝ) : Prop

Matching bounds data, collecting separation, normalized_jets, shape_slope.

• separation : c.separation < Real.exp (-8)
• normalized_jets (n : ℕ) : n ≤ N → ∀ eta ∈ Set.Icc (-1) 1, ‖iteratedFDeriv ℝ n (NominalProfile.normalizedDebt F c.debt) eta‖ < rho
• shape_slope (y eta : ℝ) : eta ∈ Set.Icc (-1) 1 → 11 / 20 ≤ 1 / 2 + deriv (fun (s : ℝ) => ShapeTransition.logProfile A.normalization c.shapeTime c.initialShape (s, eta)) y ∧ 1 / 2 + deriv (fun (s : ℝ) => ShapeTransition.logProfile A.normalization c.shapeTime c.initialShape (s, eta)) y ≤ 13 / 20

theorem NavierStokes.MatchingDebtBounds.MatchingBounds.smallDebt {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} {c : NominalProfile.Controls A} {N : ℕ} {rho : ℝ} (hb : MatchingBounds c N rho) (hr : rho ≤ NominalProfile.resetSolver.radius) {eta : ℝ} (hη : eta ∈ Set.Icc (-1) 1) : NominalProfile.SmallDebt F c.debt eta

theorem NavierStokes.MatchingDebtBounds.MatchingBounds.of_heq {F : OutgoingProfile.Profile} {A B : NominalProfile.AxisStage F} {c : NominalProfile.Controls A} {d : NominalProfile.Controls B} {N : ℕ} {rho : ℝ} (hb : MatchingBounds c N rho) (hA : B = A) (hc : d ≍ c) : MatchingBounds d N rho

theorem NavierStokes.MatchingDebtBounds.shapeTime_eq_of_heq {F : OutgoingProfile.Profile} {A B : NominalProfile.AxisStage F} {c : NominalProfile.Controls A} {d : NominalProfile.Controls B} (hA : B = A) (hc : d ≍ c) : d.shapeTime = c.shapeTime

theorem NavierStokes.MatchingDebtBounds.resetCoefficients_jet_control (N : ℕ) : ∃ (K : ℝ), 0 < K ∧ ∀ {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A), c.separation ≤ Real.exp (-8) → ∀ (tau : ℝ), 0 < tau → tau ≤ min 1 (NominalProfile.resetSolver.radius / 2) → JetBounds.FiniteJetBound N (NominalProfile.normalizedDebt F c.debt) (Set.Icc (-1) 1) (tau ^ (N + 1)) → JetBounds.FiniteJetBound N (NominalProfile.resetCoefficients F c.debt) (Set.Icc (-1) 1) (K * tau)

Actual finite jets of the coefficients produced by the fixed nonlinear inverse. The constant depends only on the requested order and that inverse. The debt hypothesis is fulfilled by the ordered construction below, with the target chosen to be tau^(N+1).

theorem NavierStokes.MatchingDebtBounds.exists_ordered_matching_threshold (F : OutgoingProfile.Profile) (N : ℕ) {rho : ℝ} (hrho : 0 < rho) : ∃ (eps : ℝ), 0 < eps ∧ eps ≤ 1 ∧ ∀ (j : ℝ), |j| ≤ eps → ∀ (hj : NaturalAxisData.SmallParameters F.data.h j) (prep : NominalProfile.AxisPreparation F j), ∃ (Λ0 : ℝ), 1 ≤ Λ0 ∧ prep.scaleBound ≤ Λ0 ∧ ∀ (Λ : ℝ) (hΛlarge : prep.scaleBound ≤ Λ), Λ0 ≤ Λ → ∃ (T : ℝ), 0 < T ∧ ∃ (C0 : ℝ), 1 ≤ C0 ∧ NaturalEntrance.entranceNormalization prep.inputs Λ prep.delta ≤ C0 ∧ ∀ (C : ℝ) (hClarge : NaturalEntrance.entranceNormalization prep.inputs Λ prep.delta ≤ C), C0 ≤ C → ∀ (E : NaturalEntrance.EntranceProfile prep.inputs Λ C) (c : NominalProfile.Controls (NominalProfile.AxisStage.ofEntrance hj prep Λ C hΛlarge hClarge E)), c.shapeTime = T → SmallControl c N eps → MatchingBounds c N rho

The thresholds hold for every incoming coefficient solution and every later control choice satisfying the displayed actual log-control estimate. Thus no new incoming profile is selected when a smaller control tolerance is required by another part of the construction.

theorem NavierStokes.MatchingDebtBounds.exists_ordered_matching_continuation (F : OutgoingProfile.Profile) (N : ℕ) {rho : ℝ} (hrho : 0 < rho) (hradius : rho ≤ NominalProfile.resetSolver.radius) : ∃ (eps : ℝ), 0 < eps ∧ eps ≤ 1 ∧ ∀ (j : ℝ), |j| ≤ eps → ∀ (hj : NaturalAxisData.SmallParameters F.data.h j) (prep : NominalProfile.AxisPreparation F j) (nu : ℝ), 0 < nu → (∀ eta ∈ Set.Icc (-1) 1, |NaturalAxisData.Z F.data.h j F.axisDatum eta| ≤ nu → 99 / 100 < NaturalAxisData.chi F.data.h j prep.sigma eta) → ∃ (Λ0 : ℝ), 1 ≤ Λ0 ∧ ∀ (Λ : ℝ) (hΛ : 0 < Λ), Λ0 ≤ Λ → ∃ (T : ℝ) (hT : 0 < T) (C0 : ℝ), 1 ≤ C0 ∧ ∀ (C : ℝ), C0 ≤ C → ∃ (hΛlarge : prep.scaleBound ≤ Λ) (hClarge : NaturalEntrance.entranceNormalization prep.inputs Λ prep.delta ≤ C) (E : NaturalEntrance.EntranceProfile prep.inputs Λ C), ∀ (J : ℕ) (epsilon : ℝ), 0 < epsilon → ∃ (w : ActivationContinuation.ContinuationWitness E hΛ hj ⋯ (max N J) (min eps epsilon)), let A := NominalProfile.AxisStage.ofEntrance hj prep Λ C hΛlarge hClarge E; have c := NominalProfile.Controls.ofContinuation A w T hT; MatchingBounds c N rho ∧ ∀ eta ∈ Set.Icc (-1) 1, NominalProfile.SmallDebt F c.debt eta

Ordered existence with the exact entrance profile produced by the actual activation-continuation theorem. The profile is chosen before the final control order and tolerance. The same controls retain the continuation cone, the physical and logarithmic estimates, and the matching-debt bounds.

theorem NavierStokes.MatchingDebtBounds.exists_ordered_assembled_profile {F : OutgoingProfile.Profile} {D : ℝ} (hF : OutgoingProfile.Specification F D) (N : ℕ) {rho : ℝ} (hrho : 0 < rho) (hradius : rho ≤ NominalProfile.resetSolver.radius) : ∃ (eps : ℝ), 0 < eps ∧ eps ≤ 1 ∧ ∀ (j : ℝ), |j| ≤ eps → ∀ (hj : NaturalAxisData.SmallParameters F.data.h j) (prep : NominalProfile.AxisPreparation F j) (nu : ℝ), 0 < nu → (∀ eta ∈ Set.Icc (-1) 1, |NaturalAxisData.Z F.data.h j F.axisDatum eta| ≤ nu → 99 / 100 < NaturalAxisData.chi F.data.h j prep.sigma eta) → ∃ (Λ0 : ℝ), 1 ≤ Λ0 ∧ ∀ (Λ : ℝ) (hΛ : 0 < Λ), Λ0 ≤ Λ → ∃ (T : ℝ) (hT : 0 < T) (C0 : ℝ), 1 ≤ C0 ∧ ∀ (C : ℝ), C0 ≤ C → ∃ (hΛlarge : prep.scaleBound ≤ Λ) (hClarge : NaturalEntrance.entranceNormalization prep.inputs Λ prep.delta ≤ C) (E : NaturalEntrance.EntranceProfile prep.inputs Λ C), ∀ (J : ℕ) (epsilon : ℝ), 0 < epsilon → ∃ (w : ActivationContinuation.ContinuationWitness E hΛ hj ⋯ (max N J) (min eps epsilon)) (W : NominalProfile.Witness F), let A := NominalProfile.AxisStage.ofEntrance hj prep Λ C hΛlarge hClarge E; have c := NominalProfile.Controls.ofContinuation A w T hT; W.axis = A ∧ W.controls ≍ c ∧ MatchingBounds W.controls N rho

The late heat-completion radius is met by increasing the same C before selecting the entrance profile. The assembled witness keeps that profile and its exact continuation controls. No separation or final-debt hypothesis is left as an input.

theorem NavierStokes.MatchingDebtBounds.exists_ordered_nominal_witness {F : OutgoingProfile.Profile} {D : ℝ} (hF : OutgoingProfile.Specification F D) (hP : 2 ≤ F.data.core.P) (N : ℕ) {rho : ℝ} (hrho : 0 < rho) (hradius : rho ≤ NominalProfile.resetSolver.radius) : ∃ (eps : ℝ), 0 < eps ∧ eps ≤ 1 ∧ ∀ (j : ℝ), |j| ≤ eps → NaturalAxisData.SmallParameters F.data.h j → ∃ (Λ0 : ℝ), 1 ≤ Λ0 ∧ ∀ (Λ : ℝ), 0 < Λ → Λ0 ≤ Λ → ∃ (T : ℝ), 0 < T ∧ ∃ (C0 : ℝ), 1 ≤ C0 ∧ ∀ (C : ℝ), C0 ≤ C → ∃ (W : NominalProfile.Witness F), W.axis.j = j ∧ W.axis.scale = Λ ∧ W.axis.normalization = C ∧ W.controls.shapeTime = T ∧ MatchingBounds W.controls N rho

The analytic preparation and its cutoff margin are now chosen together. The assembled witness has the prescribed scale and normalization; both may be increased in their displayed order.

theorem NavierStokes.MatchingDebtBounds.exists_nominal_witness {F : OutgoingProfile.Profile} {D : ℝ} (hF : OutgoingProfile.Specification F D) (hP : 2 ≤ F.data.core.P) (hh : F.data.h ≤ 1 / 1000) (N : ℕ) {rho : ℝ} (hrho : 0 < rho) (hradius : rho ≤ NominalProfile.resetSolver.radius) : ∃ (W : NominalProfile.Witness F), MatchingBounds W.controls N rho

Actual nominal-profile existence from the fixed outgoing profile. The positive axial perturbation is chosen small enough for the fixed inverse, and all five moments are then repaired by its actual normalized solver.

theorem NavierStokes.MatchingDebtBounds.exists_nominal_with_small_coefficients {F : OutgoingProfile.Profile} {D : ℝ} (hF : OutgoingProfile.Specification F D) (hP : 2 ≤ F.data.core.P) (hh : F.data.h ≤ 1 / 1000) (N : ℕ) : ∃ (K : ℝ), 0 < K ∧ ∀ (tau : ℝ), 0 < tau → tau ≤ min 1 (NominalProfile.resetSolver.radius / 2) → ∃ (W : NominalProfile.Witness F), MatchingBounds W.controls N (tau ^ (N + 1)) ∧ JetBounds.FiniteJetBound N (NominalProfile.resetCoefficients F W.controls.debt) (Set.Icc (-1) 1) (K * tau)

theorem NavierStokes.MatchingDebtBounds.nominal_witness_exists {F : OutgoingProfile.Profile} {D : ℝ} (hF : OutgoingProfile.Specification F D) (hP : 2 ≤ F.data.core.P) (hh : F.data.h ≤ 1 / 1000) : Nonempty (NominalProfile.Witness F)