The stock-driven ACT continuation and its final two ramps

The controls below integrate the actual reference lag stocks. The axial control is turned off first; the angular control is then interpolated to 4 / 5. All profile values are defined by integrals, including at the joins. No cone inequality is assumed here.

noncomputable def NavierStokes.TransitionRamp.step (b w y : ℝ) : ℝ

A translated copy of the manuscript's flat step.

Equations

• NavierStokes.TransitionRamp.step b w y = NavierStokes.OutgoingSchedule.sigma ((y - b) / w)

theorem NavierStokes.TransitionRamp.step_smooth (b w : ℝ) : ContDiff ℝ (↑⊤) (step b w)

theorem NavierStokes.TransitionRamp.step_mem (b w y : ℝ) : step b w y ∈ Set.Icc 0 1

theorem NavierStokes.TransitionRamp.step_zero {b w y : ℝ} (hw : 0 < w) (hy : y ≤ b) : step b w y = 0

theorem NavierStokes.TransitionRamp.step_one {b w y : ℝ} (hw : 0 < w) (hy : b + w ≤ y) : step b w y = 1

theorem NavierStokes.TransitionRamp.damping_eq_constant {T : ℝ} (hT : 0 < T) (κ : ℝ) {y : ℝ} (hy : T ≤ y) : StressActivation.damping T κ y = κ

theorem NavierStokes.TransitionRamp.damping_mem (T : ℝ) {κ : ℝ} (hκ : κ ∈ Set.Icc 0 1) (y : ℝ) : StressActivation.damping T κ y ∈ Set.Icc 0 1

noncomputable def NavierStokes.TransitionRamp.integrate (initial : ℝ → ℝ) (slope : ProfileHistories.Field) : ProfileHistories.Field

A literal primitive, with an independently specified value at the axis of the logarithmic clock.

Equations

• NavierStokes.TransitionRamp.integrate initial slope p = initial p.2 + NavierStokes.ProfileHistories.primitive slope p

theorem NavierStokes.TransitionRamp.integrate_smooth {J : Set ℝ} (hJ : IsOpen J) {initial : ℝ → ℝ} {slope : ProfileHistories.Field} (hi : ContDiffOn ℝ (↑⊤) initial J) (hs : ContDiffOn ℝ (↑⊤) slope (StressActivation.logDomain J hJ).carrier) : ContDiffOn ℝ (↑⊤) (integrate initial slope) (StressActivation.logDomain J hJ).carrier

theorem NavierStokes.TransitionRamp.integrate_hasDerivAt {J : Set ℝ} (hJ : IsOpen J) (initial : ℝ → ℝ) {slope : ProfileHistories.Field} (hs : ContDiffOn ℝ (↑⊤) slope (StressActivation.logDomain J hJ).carrier) (y : ℝ) {η : ℝ} (hη : η ∈ J) : HasDerivAt (fun (x : ℝ) => integrate initial slope (x, η)) (slope (y, η)) y

@[simp]

theorem NavierStokes.TransitionRamp.integrate_initial (initial : ℝ → ℝ) (slope : ProfileHistories.Field) (η : ℝ) : integrate initial slope (0, η) = initial η

theorem NavierStokes.TransitionRamp.integrate_congr (initial : ℝ → ℝ) (slope₁ slope₂ : ProfileHistories.Field) (p : ProfileHistories.Point) (he : ∀ t ∈ Set.uIcc 0 p.1, slope₁ (t, p.2) = slope₂ (t, p.2)) : integrate initial slope₁ p = integrate initial slope₂ p

noncomputable def NavierStokes.TransitionRamp.baseSlope (T κ : ℝ) (stock : ProfileHistories.Field) : ProfileHistories.Field

The ordinary ACT control continues to multiply the REF lag stock, even when the REF derivative has already become zero.

Equations

• NavierStokes.TransitionRamp.baseSlope T κ stock p = -(NavierStokes.StressActivation.damping T κ p.1 * stock p) / 2

noncomputable def NavierStokes.TransitionRamp.angularSlope (T κ b w₁ w₂ : ℝ) (stock : ProfileHistories.Field) : ProfileHistories.Field

Angular slope, defined pointwise by (1 - step (b + w₁) w₂ p.1) * baseSlope T κ stock p - (2 / 5 : ℝ) * step (b + w₁) w₂ p.1.

Equations

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

noncomputable def NavierStokes.TransitionRamp.axialSlope (T κ b w₁ : ℝ) (stock : ProfileHistories.Field) : ProfileHistories.Field

Axial slope, defined pointwise by (1 - step b w₁ p.1) * baseSlope T κ stock p.

Equations

• NavierStokes.TransitionRamp.axialSlope T κ b w₁ stock p = (1 - NavierStokes.TransitionRamp.step b w₁ p.1) * NavierStokes.TransitionRamp.baseSlope T κ stock p

theorem NavierStokes.TransitionRamp.baseSlope_smooth (T κ : ℝ) {J : Set ℝ} (hJ : IsOpen J) {stock : ProfileHistories.Field} (hs : ContDiffOn ℝ (↑⊤) stock (StressActivation.logDomain J hJ).carrier) : ContDiffOn ℝ (↑⊤) (baseSlope T κ stock) (StressActivation.logDomain J hJ).carrier

theorem NavierStokes.TransitionRamp.angularSlope_smooth (T κ b w₁ w₂ : ℝ) {J : Set ℝ} (hJ : IsOpen J) {stock : ProfileHistories.Field} (hs : ContDiffOn ℝ (↑⊤) stock (StressActivation.logDomain J hJ).carrier) : ContDiffOn ℝ (↑⊤) (angularSlope T κ b w₁ w₂ stock) (StressActivation.logDomain J hJ).carrier

theorem NavierStokes.TransitionRamp.axialSlope_smooth (T κ b w₁ : ℝ) {J : Set ℝ} (hJ : IsOpen J) {stock : ProfileHistories.Field} (hs : ContDiffOn ℝ (↑⊤) stock (StressActivation.logDomain J hJ).carrier) : ContDiffOn ℝ (↑⊤) (axialSlope T κ b w₁ stock) (StressActivation.logDomain J hJ).carrier

theorem NavierStokes.TransitionRamp.angularSlope_before {T κ b w₁ w₂ : ℝ} (hw₂ : 0 < w₂) (stock : ProfileHistories.Field) {p : ProfileHistories.Point} (hp : p.1 ≤ b + w₁) : angularSlope T κ b w₁ w₂ stock p = baseSlope T κ stock p

theorem NavierStokes.TransitionRamp.axialSlope_before {T κ b w₁ : ℝ} (hw₁ : 0 < w₁) (stock : ProfileHistories.Field) {p : ProfileHistories.Point} (hp : p.1 ≤ b) : axialSlope T κ b w₁ stock p = baseSlope T κ stock p

theorem NavierStokes.TransitionRamp.angularSlope_after {T κ b w₁ w₂ : ℝ} (hw₂ : 0 < w₂) (stock : ProfileHistories.Field) {p : ProfileHistories.Point} (hp : b + w₁ + w₂ ≤ p.1) : angularSlope T κ b w₁ w₂ stock p = -(2 / 5)

theorem NavierStokes.TransitionRamp.axialSlope_after {T κ b w₁ : ℝ} (hw₁ : 0 < w₁) (stock : ProfileHistories.Field) {p : ProfileHistories.Point} (hp : b + w₁ ≤ p.1) : axialSlope T κ b w₁ stock p = 0

noncomputable def NavierStokes.TransitionRamp.logField (T κ b w₁ w₂ : ℝ) (initial : ℝ → ℝ) (stock : ProfileHistories.Field) : ProfileHistories.Field

The actual logarithm of the angular amplitude.

Equations

• NavierStokes.TransitionRamp.logField T κ b w₁ w₂ initial stock = NavierStokes.TransitionRamp.integrate initial (NavierStokes.TransitionRamp.angularSlope T κ b w₁ w₂ stock)

noncomputable def NavierStokes.TransitionRamp.axialField (T κ b w₁ : ℝ) (initial : ℝ → ℝ) (stock : ProfileHistories.Field) : ProfileHistories.Field

The actual axial velocity after the first, axial, shutoff.

Equations

• NavierStokes.TransitionRamp.axialField T κ b w₁ initial stock = NavierStokes.TransitionRamp.integrate initial (NavierStokes.TransitionRamp.axialSlope T κ b w₁ stock)

theorem NavierStokes.TransitionRamp.logField_smooth (T κ b w₁ w₂ : ℝ) {J : Set ℝ} (hJ : IsOpen J) {initial : ℝ → ℝ} {stock : ProfileHistories.Field} (hi : ContDiffOn ℝ (↑⊤) initial J) (hs : ContDiffOn ℝ (↑⊤) stock (StressActivation.logDomain J hJ).carrier) : ContDiffOn ℝ (↑⊤) (logField T κ b w₁ w₂ initial stock) (StressActivation.logDomain J hJ).carrier

theorem NavierStokes.TransitionRamp.axialField_smooth (T κ b w₁ : ℝ) {J : Set ℝ} (hJ : IsOpen J) {initial : ℝ → ℝ} {stock : ProfileHistories.Field} (hi : ContDiffOn ℝ (↑⊤) initial J) (hs : ContDiffOn ℝ (↑⊤) stock (StressActivation.logDomain J hJ).carrier) : ContDiffOn ℝ (↑⊤) (axialField T κ b w₁ initial stock) (StressActivation.logDomain J hJ).carrier

theorem NavierStokes.TransitionRamp.logField_before {T κ b w₁ w₂ : ℝ} (hb : 0 ≤ b + w₁) (hw₂ : 0 < w₂) (initial : ℝ → ℝ) (stock : ProfileHistories.Field) {p : ProfileHistories.Point} (hp : p.1 ≤ b + w₁) : logField T κ b w₁ w₂ initial stock p = integrate initial (baseSlope T κ stock) p

theorem NavierStokes.TransitionRamp.axialField_before {T κ b w₁ : ℝ} (hb : 0 ≤ b) (hw₁ : 0 < w₁) (initial : ℝ → ℝ) (stock : ProfileHistories.Field) {p : ProfileHistories.Point} (hp : p.1 ≤ b) : axialField T κ b w₁ initial stock p = integrate initial (baseSlope T κ stock) p

theorem NavierStokes.TransitionRamp.integrate_affine_after {J : Set ℝ} (hJ : IsOpen J) (initial : ℝ → ℝ) {slope : ProfileHistories.Field} (hs : ContDiffOn ℝ (↑⊤) slope (StressActivation.logDomain J hJ).carrier) {a y c η : ℝ} (hay : a ≤ y) (hη : η ∈ J) (hc : ∀ (t : ℝ), a ≤ t → slope (t, η) = c) : integrate initial slope (y, η) = integrate initial slope (a, η) + (y - a) * c

theorem NavierStokes.TransitionRamp.logField_hold {T κ b w₁ w₂ : ℝ} (hw₂ : 0 < w₂) {J : Set ℝ} (hJ : IsOpen J) (initial : ℝ → ℝ) {stock : ProfileHistories.Field} (hs : ContDiffOn ℝ (↑⊤) stock (StressActivation.logDomain J hJ).carrier) {a y η : ℝ} (ha : b + w₁ + w₂ ≤ a) (hay : a ≤ y) (hη : η ∈ J) : logField T κ b w₁ w₂ initial stock (y, η) = logField T κ b w₁ w₂ initial stock (a, η) - 2 / 5 * (y - a)

theorem NavierStokes.TransitionRamp.axialField_hold {T κ b w₁ : ℝ} (hw₁ : 0 < w₁) {J : Set ℝ} (hJ : IsOpen J) (initial : ℝ → ℝ) {stock : ProfileHistories.Field} (hs : ContDiffOn ℝ (↑⊤) stock (StressActivation.logDomain J hJ).carrier) {a y η : ℝ} (ha : b + w₁ ≤ a) (hay : a ≤ y) (hη : η ∈ J) : axialField T κ b w₁ initial stock (y, η) = axialField T κ b w₁ initial stock (a, η)

structure NavierStokes.TransitionRamp.StockReference (J : Set ℝ) : Type

Genuine reference profiles, with their positive-radius logarithmic chart. The two controls below are defined from their actual lag integrals.

• exponent : ℝ

  Exponent of StockReference, of type ℝ.

• radius0 : ℝ

  Radius0 of StockReference, of type ℝ.

• radius0_pos : 0 < self.radius0
• domain : ProfileHistories.RadialDomain

  Domain of StockReference, of type RadialDomain.

• profiles : ProfileHistories.Profiles self.domain

  Profiles of StockReference, of type Profiles domain.

• log_mem (y η : ℝ) : η ∈ J → (StressActivation.radius self.radius0 y, η) ∈ self.domain.carrier
• f_pos (y η : ℝ) : η ∈ J → 0 < self.profiles.f (StressActivation.radius self.radius0 y, η)
• L_ne_zero (η : ℝ) : η ∈ J → NaturalAxisData.L self.exponent η ≠ 0

noncomputable def NavierStokes.TransitionRamp.StockReference.chart {J : Set ℝ} (R : StockReference J) (p : ProfileHistories.Point) : ProfileHistories.Point

Chart, given by (radius R.radius0 p.1, p.2).

Equations

• R.chart p = (NavierStokes.StressActivation.radius R.radius0 p.1, p.2)

theorem NavierStokes.TransitionRamp.StockReference.chart_smooth {J : Set ℝ} (R : StockReference J) : ContDiff ℝ (↑⊤) R.chart

theorem NavierStokes.TransitionRamp.StockReference.chart_radius_pos {J : Set ℝ} (R : StockReference J) (p : ProfileHistories.Point) : 0 < (R.chart p).1

noncomputable def NavierStokes.TransitionRamp.StockReference.angularStock {J : Set ℝ} (R : StockReference J) : ProfileHistories.Field

Angular stock, defined pointwise by ActivationStocks.profileStockOne R.profiles R.exponent (R.chart p).

Equations

• R.angularStock p = NavierStokes.ActivationStocks.profileStockOne R.profiles R.exponent (R.chart p)

noncomputable def NavierStokes.TransitionRamp.StockReference.axialStock {J : Set ℝ} (R : StockReference J) : ProfileHistories.Field

This is X * ns_REF, including the radial factor in the axial ODE.

Equations

• R.axialStock p = (R.chart p).1 * R.profiles.axialLag R.exponent (R.chart p) / NavierStokes.NaturalAxisData.L R.exponent p.2

noncomputable def NavierStokes.TransitionRamp.StockReference.initialLog {J : Set ℝ} (R : StockReference J) (η : ℝ) : ℝ

Initial log, given by Real.log (R.profiles.f (R.radius0, η)).

Equations

• R.initialLog η = Real.log (R.profiles.f (R.radius0, η))

noncomputable def NavierStokes.TransitionRamp.StockReference.initialU {J : Set ℝ} (R : StockReference J) (η : ℝ) : ℝ

Initial U, given by R.profiles.U (R.radius0, η).

Equations

• R.initialU η = R.profiles.U (R.radius0, η)

theorem NavierStokes.TransitionRamp.StockReference.angularStock_smooth {J : Set ℝ} (R : StockReference J) (hJ : IsOpen J) : ContDiffOn ℝ (↑⊤) R.angularStock (StressActivation.logDomain J hJ).carrier

theorem NavierStokes.TransitionRamp.StockReference.axialStock_smooth {J : Set ℝ} (R : StockReference J) (hJ : IsOpen J) : ContDiffOn ℝ (↑⊤) R.axialStock (StressActivation.logDomain J hJ).carrier

theorem NavierStokes.TransitionRamp.StockReference.initialLog_smooth {J : Set ℝ} (R : StockReference J) (_hJ : IsOpen J) : ContDiffOn ℝ (↑⊤) R.initialLog J

theorem NavierStokes.TransitionRamp.StockReference.initialU_smooth {J : Set ℝ} (R : StockReference J) (_hJ : IsOpen J) : ContDiffOn ℝ (↑⊤) R.initialU J

noncomputable def NavierStokes.TransitionRamp.StockReference.bigTime {J : Set ℝ} (R : StockReference J) : ℝ

Big time, given by Real.log (100 / R.radius0).

Equations

• R.bigTime = Real.log (100 / R.radius0)

noncomputable def NavierStokes.TransitionRamp.StockReference.finalTime {J : Set ℝ} (R : StockReference J) : ℝ

Final time, given by Real.log (110 / R.radius0).

Equations

• R.finalTime = Real.log (110 / R.radius0)

noncomputable def NavierStokes.TransitionRamp.StockReference.logAmplitude {J : Set ℝ} (R : StockReference J) (T κ w₁ w₂ : ℝ) : ProfileHistories.Field

Log amplitude, given by logField T κ R.bigTime w₁ w₂ R.initialLog R.angularStock.

Equations

• R.logAmplitude T κ w₁ w₂ = NavierStokes.TransitionRamp.logField T κ R.bigTime w₁ w₂ R.initialLog R.angularStock

noncomputable def NavierStokes.TransitionRamp.StockReference.axialVelocity {J : Set ℝ} (R : StockReference J) (T κ w₁ : ℝ) : ProfileHistories.Field

Axial velocity, given by axialField T κ R.bigTime w₁ R.initialU R.axialStock.

Equations

• R.axialVelocity T κ w₁ = NavierStokes.TransitionRamp.axialField T κ R.bigTime w₁ R.initialU R.axialStock

theorem NavierStokes.TransitionRamp.StockReference.logAmplitude_smooth {J : Set ℝ} (R : StockReference J) (hJ : IsOpen J) (T κ w₁ w₂ : ℝ) : ContDiffOn ℝ (↑⊤) (R.logAmplitude T κ w₁ w₂) (StressActivation.logDomain J hJ).carrier

theorem NavierStokes.TransitionRamp.StockReference.axialVelocity_smooth {J : Set ℝ} (R : StockReference J) (hJ : IsOpen J) (T κ w₁ : ℝ) : ContDiffOn ℝ (↑⊤) (R.axialVelocity T κ w₁) (StressActivation.logDomain J hJ).carrier

theorem NavierStokes.TransitionRamp.StockReference.logAmplitude_hasDerivAt {J : Set ℝ} (R : StockReference J) (hJ : IsOpen J) (T κ w₁ w₂ y : ℝ) {η : ℝ} (hη : η ∈ J) : HasDerivAt (fun (x : ℝ) => R.logAmplitude T κ w₁ w₂ (x, η)) (angularSlope T κ R.bigTime w₁ w₂ R.angularStock (y, η)) y

theorem NavierStokes.TransitionRamp.StockReference.axialVelocity_hasDerivAt {J : Set ℝ} (R : StockReference J) (hJ : IsOpen J) (T κ w₁ y : ℝ) {η : ℝ} (hη : η ∈ J) : HasDerivAt (fun (x : ℝ) => R.axialVelocity T κ w₁ (x, η)) (axialSlope T κ R.bigTime w₁ R.axialStock (y, η)) y

theorem NavierStokes.TransitionRamp.StockReference.prescribed_angular_control {J : Set ℝ} (R : StockReference J) (hJ : IsOpen J) (T κ w₁ w₂ y : ℝ) {η : ℝ} (hη : η ∈ J) : -2 * deriv (fun (x : ℝ) => R.logAmplitude T κ w₁ w₂ (x, η)) y = (1 - step (R.bigTime + w₁) w₂ y) * StressActivation.damping T κ y * R.angularStock (y, η) + 4 / 5 * step (R.bigTime + w₁) w₂ y

theorem NavierStokes.TransitionRamp.StockReference.prescribed_axial_control {J : Set ℝ} (R : StockReference J) (hJ : IsOpen J) (T κ w₁ y : ℝ) {η : ℝ} (hη : η ∈ J) : deriv (fun (x : ℝ) => R.axialVelocity T κ w₁ (x, η)) y = -(1 - step R.bigTime w₁ y) * StressActivation.damping T κ y * R.axialStock (y, η) / 2

theorem NavierStokes.TransitionRamp.StockReference.final_logarithmic_slope {J : Set ℝ} (R : StockReference J) (hJ : IsOpen J) {T κ w₁ w₂ y η : ℝ} (hw₂ : 0 < w₂) (hy : R.bigTime + w₁ + w₂ ≤ y) (hη : η ∈ J) : 1 + deriv (fun (x : ℝ) => R.logAmplitude T κ w₁ w₂ (x, η)) y = 3 / 5

On the final hold the physical logarithmic slope l is exactly 3/5.

Actual parameter jets of the integral controls

noncomputable def NavierStokes.TransitionRamp.parameterJet : ℕ → ProfileHistories.Field → ProfileHistories.Field

Parameter jet as an element of ℕ → Field → Field | 0, F => F | n + 1, F => parameterPartial (parameterJet n F).

Equations

• NavierStokes.TransitionRamp.parameterJet 0 x✝ = x✝
• NavierStokes.TransitionRamp.parameterJet n.succ x✝ = NavierStokes.ProfileHistories.parameterPartial (NavierStokes.TransitionRamp.parameterJet n x✝)

theorem NavierStokes.TransitionRamp.parameterJet_smooth {J : Set ℝ} (hJ : IsOpen J) {F : ProfileHistories.Field} (hF : ContDiffOn ℝ (↑⊤) F (StressActivation.logDomain J hJ).carrier) (n : ℕ) : ContDiffOn ℝ (↑⊤) (parameterJet n F) (StressActivation.logDomain J hJ).carrier

theorem NavierStokes.TransitionRamp.parameterJet_eq_iteratedDeriv {J : Set ℝ} (hJ : IsOpen J) {F : ProfileHistories.Field} (hF : ContDiffOn ℝ (↑⊤) F (StressActivation.logDomain J hJ).carrier) (n : ℕ) {p : ProfileHistories.Point} (hp : p.2 ∈ J) : parameterJet n F p = iteratedDeriv n (fun (η : ℝ) => F (p.1, η)) p.2

theorem NavierStokes.TransitionRamp.parameterPartial_congr {J : Set ℝ} (hJ : IsOpen J) {F G : ProfileHistories.Field} (he : ∀ (p : ProfileHistories.Point), p.2 ∈ J → F p = G p) {p : ProfileHistories.Point} (hp : p.2 ∈ J) : ProfileHistories.parameterPartial F p = ProfileHistories.parameterPartial G p

theorem NavierStokes.TransitionRamp.parameterJet_primitive {J : Set ℝ} (hJ : IsOpen J) {F : ProfileHistories.Field} (hF : ContDiffOn ℝ (↑⊤) F (StressActivation.logDomain J hJ).carrier) (n : ℕ) {p : ProfileHistories.Point} (hp : p.2 ∈ J) : parameterJet n (ProfileHistories.primitive F) p = ProfileHistories.primitive (parameterJet n F) p

theorem NavierStokes.TransitionRamp.parameterJet_mul_radial {J : Set ℝ} (hJ : IsOpen J) {F : ProfileHistories.Field} (hF : ContDiffOn ℝ (↑⊤) F (StressActivation.logDomain J hJ).carrier) {g : ℝ → ℝ} (hg : ContDiff ℝ (↑⊤) g) (n : ℕ) {p : ProfileHistories.Point} (hp : p.2 ∈ J) : parameterJet n (fun (q : ProfileHistories.Point) => g q.1 * F q) p = g p.1 * parameterJet n F p

theorem NavierStokes.TransitionRamp.parameterJet_congr {J : Set ℝ} (hJ : IsOpen J) {F G : ProfileHistories.Field} (he : ∀ (p : ProfileHistories.Point), p.2 ∈ J → F p = G p) (n : ℕ) {p : ProfileHistories.Point} (hp : p.2 ∈ J) : parameterJet n F p = parameterJet n G p

theorem NavierStokes.TransitionRamp.parameterJet_sub {J : Set ℝ} (hJ : IsOpen J) {F G : ProfileHistories.Field} (hF : ContDiffOn ℝ (↑⊤) F (StressActivation.logDomain J hJ).carrier) (hG : ContDiffOn ℝ (↑⊤) G (StressActivation.logDomain J hJ).carrier) (n : ℕ) {p : ProfileHistories.Point} (hp : p.2 ∈ J) : parameterJet n (fun (q : ProfileHistories.Point) => F q - G q) p = parameterJet n F p - parameterJet n G p

theorem NavierStokes.TransitionRamp.parameterJet_radial {J : Set ℝ} (hJ : IsOpen J) {g : ℝ → ℝ} (hg : ContDiff ℝ (↑⊤) g) (n : ℕ) {p : ProfileHistories.Point} (hp : p.2 ∈ J) : parameterJet n (fun (q : ProfileHistories.Point) => g q.1) p = if n = 0 then g p.1 else 0

theorem NavierStokes.TransitionRamp.integral_norm_bound {F : ℝ → ℝ} {a b M : ℝ} (hab : a ≤ b) (hb : ∀ t ∈ Set.Icc a b, |F t| ≤ M) : |∫ (t : ℝ) in a..b, F t| ≤ M * (b - a)

theorem NavierStokes.TransitionRamp.initial_layer_bound {F : ℝ → ℝ} (hF : Continuous F) {T y M : ℝ} (hT : 0 ≤ T) (hy : 0 ≤ y) (hM : 0 ≤ M) (hb : ∀ t ∈ Set.Icc 0 y, |F t| ≤ M) (hz : ∀ t ∈ Set.Icc T y, F t = 0) : |∫ (t : ℝ) in 0..y, F t| ≤ M * T

An initial layer contributes only its width, even at later radii.

theorem NavierStokes.TransitionRamp.late_layer_bound {F : ℝ → ℝ} (hF : Continuous F) {a y w M : ℝ} (ha : 0 ≤ a) (hy : 0 ≤ y) (hyw : y ≤ a + w) (hw : 0 ≤ w) (hM : 0 ≤ M) (hb : ∀ t ∈ Set.Icc 0 y, |F t| ≤ M) (hz : ∀ t ∈ Set.Icc 0 a, F t = 0) : |∫ (t : ℝ) in 0..y, F t| ≤ M * w

A modification supported after a contributes only the traversed width; the estimate applies before, during, and at the end of its ramp.

theorem NavierStokes.TransitionRamp.parameterJet_baseSlope {J : Set ℝ} (hJ : IsOpen J) {stock : ProfileHistories.Field} (hs : ContDiffOn ℝ (↑⊤) stock (StressActivation.logDomain J hJ).carrier) (T κ : ℝ) (n : ℕ) {p : ProfileHistories.Point} (hp : p.2 ∈ J) : parameterJet n (baseSlope T κ stock) p = -(StressActivation.damping T κ p.1 * parameterJet n stock p) / 2

theorem NavierStokes.TransitionRamp.parameterJet_axialSlope {J : Set ℝ} (hJ : IsOpen J) {stock : ProfileHistories.Field} (hs : ContDiffOn ℝ (↑⊤) stock (StressActivation.logDomain J hJ).carrier) (T κ b w : ℝ) (n : ℕ) {p : ProfileHistories.Point} (hp : p.2 ∈ J) : parameterJet n (axialSlope T κ b w stock) p = (1 - step b w p.1) * (-(StressActivation.damping T κ p.1 * parameterJet n stock p) / 2)

theorem NavierStokes.TransitionRamp.parameterJet_angularSlope {J : Set ℝ} (hJ : IsOpen J) {stock : ProfileHistories.Field} (hs : ContDiffOn ℝ (↑⊤) stock (StressActivation.logDomain J hJ).carrier) (T κ b w₁ w₂ : ℝ) (n : ℕ) {p : ProfileHistories.Point} (hp : p.2 ∈ J) : parameterJet n (angularSlope T κ b w₁ w₂ stock) p = (1 - step (b + w₁) w₂ p.1) * (-(StressActivation.damping T κ p.1 * parameterJet n stock p) / 2) - if n = 0 then 2 / 5 * step (b + w₁) w₂ p.1 else 0

theorem NavierStokes.TransitionRamp.integrate_error_jet {J : Set ℝ} (hJ : IsOpen J) (initial : ℝ → ℝ) {slope : ProfileHistories.Field} (hs : ContDiffOn ℝ (↑⊤) slope (StressActivation.logDomain J hJ).carrier) (n : ℕ) (y : ℝ) {η : ℝ} (hη : η ∈ J) : iteratedDeriv n (fun (ξ : ℝ) => integrate initial slope (y, ξ) - initial ξ) η = ∫ (t : ℝ) in 0..y, parameterJet n slope (t, η)

theorem NavierStokes.TransitionRamp.damped_integral_bound {F : ℝ → ℝ} (hF : Continuous F) {T κ y M : ℝ} (hT : 0 < T) (hκ : κ ∈ Set.Icc 0 1) (hy : 0 ≤ y) (hM : 0 ≤ M) (hb : ∀ t ∈ Set.Icc 0 y, |F t| ≤ StressActivation.damping T κ t * M) : |∫ (t : ℝ) in 0..y, F t| ≤ M * (T + κ * y)

Integrating the actual damping gives a bound proportional to the activation width plus the retained constant control.

theorem NavierStokes.TransitionRamp.jet_slice_continuous {J : Set ℝ} (hJ : IsOpen J) {F : ProfileHistories.Field} (hF : ContDiffOn ℝ (↑⊤) F (StressActivation.logDomain J hJ).carrier) (n : ℕ) {η : ℝ} (hη : η ∈ J) : Continuous fun (t : ℝ) => parameterJet n F (t, η)

theorem NavierStokes.TransitionRamp.compact_stock_jet_bound {J K : Set ℝ} (hJ : IsOpen J) (hK : IsCompact K) (hKJ : K ⊆ J) {stock : ProfileHistories.Field} (hs : ContDiffOn ℝ (↑⊤) stock (StressActivation.logDomain J hJ).carrier) (R : ℝ) (N : ℕ) : ∃ M ≥ 0, ∀ n ≤ N, ∀ t ∈ Set.Icc 0 R, ∀ η ∈ K, |parameterJet n stock (t, η)| ≤ M

theorem NavierStokes.TransitionRamp.controlled_product_bound {a d z M : ℝ} (ha : a ∈ Set.Icc 0 1) (hd : 0 ≤ d) (hM : 0 ≤ M) (hz : |z| ≤ M) : |a * (-(d * z) / 2)| ≤ d * M

theorem NavierStokes.TransitionRamp.axialField_jet_error_bound {J : Set ℝ} (hJ : IsOpen J) {stock : ProfileHistories.Field} (hs : ContDiffOn ℝ (↑⊤) stock (StressActivation.logDomain J hJ).carrier) (initial : ℝ → ℝ) {T κ b w y η M : ℝ} (hT : 0 < T) (hκ : κ ∈ Set.Icc 0 1) (hy : 0 ≤ y) (hη : η ∈ J) (hM : 0 ≤ M) (n : ℕ) (hb : ∀ t ∈ Set.Icc 0 y, |parameterJet n stock (t, η)| ≤ M) : |iteratedDeriv n (fun (ξ : ℝ) => axialField T κ b w initial stock (y, ξ) - initial ξ) η| ≤ M * (T + κ * y)

theorem NavierStokes.TransitionRamp.logField_positive_jet_error_bound {J : Set ℝ} (hJ : IsOpen J) {stock : ProfileHistories.Field} (hs : ContDiffOn ℝ (↑⊤) stock (StressActivation.logDomain J hJ).carrier) (initial : ℝ → ℝ) {T κ b w₁ w₂ y η M : ℝ} (hT : 0 < T) (hκ : κ ∈ Set.Icc 0 1) (hy : 0 ≤ y) (hη : η ∈ J) (hM : 0 ≤ M) {n : ℕ} (hn : n ≠ 0) (hb : ∀ t ∈ Set.Icc 0 y, |parameterJet n stock (t, η)| ≤ M) : |iteratedDeriv n (fun (ξ : ℝ) => logField T κ b w₁ w₂ initial stock (y, ξ) - initial ξ) η| ≤ M * (T + κ * y)

theorem NavierStokes.TransitionRamp.logField_value_error_bound {J : Set ℝ} (hJ : IsOpen J) {stock : ProfileHistories.Field} (hs : ContDiffOn ℝ (↑⊤) stock (StressActivation.logDomain J hJ).carrier) (initial : ℝ → ℝ) {T κ b w₁ w₂ y η M : ℝ} (hT : 0 < T) (hκ : κ ∈ Set.Icc 0 1) (hb0 : 0 ≤ b) (hw₁ : 0 ≤ w₁) (hw₂ : 0 < w₂) (hy : 0 ≤ y) (hyend : y ≤ b + w₁ + w₂) (hη : η ∈ J) (hM : 0 ≤ M) (hb : ∀ t ∈ Set.Icc 0 y, |stock (t, η)| ≤ M) : |logField T κ b w₁ w₂ initial stock (y, η) - initial η| ≤ M * (T + κ * y) + 2 / 5 * (w₁ + w₂)

Instantiation by the constructed natural profiles

noncomputable def NavierStokes.TransitionRamp.StockReference.logTime {J : Set ℝ} (R : StockReference J) (X : ℝ) : ℝ

Log time, given by Real.log (X / R.radius0).

Equations

• R.logTime X = Real.log (X / R.radius0)

noncomputable def NavierStokes.TransitionRamp.StockReference.logPoint {J : Set ℝ} (R : StockReference J) (p : ProfileHistories.Point) : ProfileHistories.Point

Log point, given by (R.logTime p.1, p.2).

Equations

• R.logPoint p = (R.logTime p.1, p.2)

theorem NavierStokes.TransitionRamp.StockReference.logPoint_smoothAt {J : Set ℝ} (R : StockReference J) {p : ProfileHistories.Point} (hX : 0 < p.1) : ContDiffAt ℝ (↑⊤) R.logPoint p

theorem NavierStokes.TransitionRamp.StockReference.logTime_chart {J : Set ℝ} (R : StockReference J) (y : ℝ) : R.logTime (StressActivation.radius R.radius0 y) = y

theorem NavierStokes.TransitionRamp.StockReference.chart_logTime {J : Set ℝ} (R : StockReference J) {X η : ℝ} (hX : 0 < X) : R.chart (R.logTime X, η) = (X, η)

noncomputable def NavierStokes.TransitionRamp.StockReference.physicalF {J : Set ℝ} (R : StockReference J) (T κ w₁ w₂ : ℝ) : ProfileHistories.Field

Physical F, defined pointwise by if p.1 ≤ R.radius0 then R.profiles.f p else Real.exp (R.logAmplitude T κ w₁ w₂ (R.logPoint p)).

Equations

• R.physicalF T κ w₁ w₂ p = if p.1 ≤ R.radius0 then R.profiles.f p else Real.exp (R.logAmplitude T κ w₁ w₂ (R.logPoint p))

noncomputable def NavierStokes.TransitionRamp.StockReference.physicalU {J : Set ℝ} (R : StockReference J) (T κ w₁ : ℝ) : ProfileHistories.Field

Physical U, defined pointwise by if p.1 ≤ R.radius0 then R.profiles.U p else R.axialVelocity T κ w₁ (R.logPoint p).

Equations

• R.physicalU T κ w₁ p = if p.1 ≤ R.radius0 then R.profiles.U p else R.axialVelocity T κ w₁ (R.logPoint p)

theorem NavierStokes.TransitionRamp.StockReference.physicalF_before {J : Set ℝ} (R : StockReference J) (T κ w₁ w₂ : ℝ) {p : ProfileHistories.Point} (hp : p.1 ≤ R.radius0) : R.physicalF T κ w₁ w₂ p = R.profiles.f p

theorem NavierStokes.TransitionRamp.StockReference.physicalU_before {J : Set ℝ} (R : StockReference J) (T κ w₁ : ℝ) {p : ProfileHistories.Point} (hp : p.1 ≤ R.radius0) : R.physicalU T κ w₁ p = R.profiles.U p

noncomputable def NavierStokes.TransitionRamp.StockReference.endpointU {J : Set ℝ} (R : StockReference J) (T κ w₁ η : ℝ) : ℝ

Endpoint U, given by R.axialVelocity T κ w₁ (R.finalTime, η).

Equations

• R.endpointU T κ w₁ η = R.axialVelocity T κ w₁ (R.finalTime, η)

noncomputable def NavierStokes.TransitionRamp.StockReference.endpointLog {J : Set ℝ} (R : StockReference J) (T κ w₁ w₂ C η : ℝ) : ℝ

Endpoint log, given by Real.log C + Real.log 220 / 2 + R.logAmplitude T κ w₁ w₂ (R.finalTime, η).

Equations

• R.endpointLog T κ w₁ w₂ C η = Real.log C + Real.log 220 / 2 + R.logAmplitude T κ w₁ w₂ (R.finalTime, η)

theorem NavierStokes.TransitionRamp.StockReference.endpointU_smooth {J : Set ℝ} (R : StockReference J) (hJ : IsOpen J) (T κ w₁ : ℝ) : ContDiffOn ℝ (↑⊤) (R.endpointU T κ w₁) J

theorem NavierStokes.TransitionRamp.StockReference.endpointLog_smooth {J : Set ℝ} (R : StockReference J) (hJ : IsOpen J) (T κ w₁ w₂ C : ℝ) : ContDiffOn ℝ (↑⊤) (R.endpointLog T κ w₁ w₂ C) J

theorem NavierStokes.TransitionRamp.L_pos_parameterInterval {h j η : ℝ} (hs : NaturalAxisData.SmallParameters h j) (hη : η ∈ ReferencePath.parameterInterval) : 0 < NaturalAxisData.L h η

noncomputable def NavierStokes.TransitionRamp.ofNatural {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalProfile.ProfileFamily d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (hP0 : ContDiff ℝ (↑⊤) P0) : StockReference ReferencePath.parameterInterval

No stock or differential equation is postulated in this constructor: the underlying profiles and all five histories are the completed REF path.

Equations

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

theorem NavierStokes.TransitionRamp.natural_stock_identity {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalProfile.ProfileFamily d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (hP0 : ContDiff ℝ (↑⊤) P0) (y : ℝ) (hy : y ≤ δ) {η : ℝ} (hη : η ∈ ReferencePath.parameterInterval) : have N := ReferencePath.Input.ofNatural hΛ F; have p := N.fromLog (y, η); ActivationStocks.profileStockOne (N.histories hδ hδT P0 hP0) h p = NaturalEntrance.p1 F.f p ∧ ActivationStocks.profileStockTwo (N.histories hδ hδT P0 hP0) h p = NaturalEntrance.p2 F.f F.U p

theorem NavierStokes.TransitionRamp.refLog_radial_natural (N : ReferencePath.Input) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) {p : ProfileHistories.Point} (hp : p.2 ∈ ReferencePath.parameterInterval) (hy : p.1 ≤ δ) : ProfileHistories.radialPartial (StressActivation.FromReference.refLog N δ) p = ProfileHistories.radialPartial N.logF p

theorem NavierStokes.TransitionRamp.refAxial_radial_natural (N : ReferencePath.Input) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) {p : ProfileHistories.Point} (hp : p.2 ∈ ReferencePath.parameterInterval) (hy : p.1 ≤ δ) : ProfileHistories.radialPartial (StressActivation.FromReference.refAxial N δ) p = ProfileHistories.radialPartial N.logU p

theorem NavierStokes.TransitionRamp.ofNatural_stock_slopes {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalProfile.ProfileFamily d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (hP0 : ContDiff ℝ (↑⊤) P0) (y : ℝ) (hy : y ≤ δ) {η : ℝ} (hη : η ∈ ReferencePath.parameterInterval) : have R := ofNatural F hΛ hsmall hδ hδT hP0; have N := ReferencePath.Input.ofNatural hΛ F; R.angularStock (y, η) = -2 * ProfileHistories.radialPartial (StressActivation.FromReference.refLog N δ) (y, η) ∧ R.axialStock (y, η) = -2 * ProfileHistories.radialPartial (StressActivation.FromReference.refAxial N δ) (y, η)

theorem NavierStokes.TransitionRamp.ofNatural_initialLog {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalProfile.ProfileFamily d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (hP0 : ContDiff ℝ (↑⊤) P0) {η : ℝ} (hη : η ∈ ReferencePath.parameterInterval) : (ofNatural F hΛ hsmall hδ hδT hP0).initialLog η = StressActivation.FromReference.refLog (ReferencePath.Input.ofNatural hΛ F) δ (0, η)

theorem NavierStokes.TransitionRamp.ofNatural_initialU {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalProfile.ProfileFamily d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (hP0 : ContDiff ℝ (↑⊤) P0) {η : ℝ} (hη : η ∈ ReferencePath.parameterInterval) : (ofNatural F hΛ hsmall hδ hδT hP0).initialU η = StressActivation.FromReference.refAxial (ReferencePath.Input.ofNatural hΛ F) δ (0, η)

theorem NavierStokes.TransitionRamp.base_integrals_eq_activation {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalProfile.ProfileFamily d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (hP0 : ContDiff ℝ (↑⊤) P0) (T κ y : ℝ) (hy : y ≤ δ) {η : ℝ} (hη : η ∈ ReferencePath.parameterInterval) : have R := ofNatural F hΛ hsmall hδ hδT hP0; have N := ReferencePath.Input.ofNatural hΛ F; integrate R.initialLog (baseSlope T κ R.angularStock) (y, η) = StressActivation.controlled T κ (StressActivation.FromReference.refLog N δ) (y, η) ∧ integrate R.initialU (baseSlope T κ R.axialStock) (y, η) = StressActivation.controlled T κ (StressActivation.FromReference.refAxial N δ) (y, η)

theorem NavierStokes.TransitionRamp.log_fields_eq_activation {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalProfile.ProfileFamily d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (hP0 : ContDiff ℝ (↑⊤) P0) {T κ w₁ w₂ y : ℝ} (hb : δ ≤ (ofNatural F hΛ hsmall hδ hδT hP0).bigTime) (hw₁ : 0 < w₁) (hw₂ : 0 < w₂) (hy : y ≤ δ) {η : ℝ} (hη : η ∈ ReferencePath.parameterInterval) : have R := ofNatural F hΛ hsmall hδ hδT hP0; have N := ReferencePath.Input.ofNatural hΛ F; R.logAmplitude T κ w₁ w₂ (y, η) = StressActivation.controlled T κ (StressActivation.FromReference.refLog N δ) (y, η) ∧ R.axialVelocity T κ w₁ (y, η) = StressActivation.controlled T κ (StressActivation.FromReference.refAxial N δ) (y, η)

theorem NavierStokes.TransitionRamp.physicalF_eq_log {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalProfile.ProfileFamily d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (hP0 : ContDiff ℝ (↑⊤) P0) {T κ w₁ w₂ : ℝ} (hT : 0 < T) (hb : δ ≤ (ofNatural F hΛ hsmall hδ hδT hP0).bigTime) (hw₁ : 0 < w₁) (hw₂ : 0 < w₂) {p : ProfileHistories.Point} (hη : p.2 ∈ ReferencePath.parameterInterval) (hX : 0 < p.1) : have R := ofNatural F hΛ hsmall hδ hδT hP0; R.physicalF T κ w₁ w₂ p = Real.exp (R.logAmplitude T κ w₁ w₂ (R.logPoint p))

theorem NavierStokes.TransitionRamp.physicalU_eq_log {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalProfile.ProfileFamily d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (hP0 : ContDiff ℝ (↑⊤) P0) {T κ w₁ w₂ : ℝ} (hT : 0 < T) (hb : δ ≤ (ofNatural F hΛ hsmall hδ hδT hP0).bigTime) (hw₁ : 0 < w₁) (hw₂ : 0 < w₂) {p : ProfileHistories.Point} (hη : p.2 ∈ ReferencePath.parameterInterval) (hX : 0 < p.1) : have R := ofNatural F hΛ hsmall hδ hδT hP0; R.physicalU T κ w₁ p = R.axialVelocity T κ w₁ (R.logPoint p)

theorem NavierStokes.TransitionRamp.physicalF_smooth {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalProfile.ProfileFamily d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (hP0 : ContDiff ℝ (↑⊤) P0) {T κ w₁ w₂ : ℝ} (hT : 0 < T) (hb : δ ≤ (ofNatural F hΛ hsmall hδ hδT hP0).bigTime) (hw₁ : 0 < w₁) (hw₂ : 0 < w₂) : ContDiffOn ℝ (↑⊤) ((ofNatural F hΛ hsmall hδ hδT hP0).physicalF T κ w₁ w₂) (ReferencePath.Input.ofNatural hΛ F).radialDomain.carrier

theorem NavierStokes.TransitionRamp.physicalU_smooth {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalProfile.ProfileFamily d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (hP0 : ContDiff ℝ (↑⊤) P0) {T κ w₁ w₂ : ℝ} (hT : 0 < T) (hb : δ ≤ (ofNatural F hΛ hsmall hδ hδT hP0).bigTime) (hw₁ : 0 < w₁) (hw₂ : 0 < w₂) : ContDiffOn ℝ (↑⊤) ((ofNatural F hΛ hsmall hδ hδT hP0).physicalU T κ w₁) (ReferencePath.Input.ofNatural hΛ F).radialDomain.carrier

theorem NavierStokes.TransitionRamp.physicalF_positive {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalProfile.ProfileFamily d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (hP0 : ContDiff ℝ (↑⊤) P0) (T κ w₁ w₂ : ℝ) {p : ProfileHistories.Point} (hp : p ∈ (ReferencePath.Input.ofNatural hΛ F).radialDomain.carrier) (hX : 0 ≤ p.1) : 0 < (ofNatural F hΛ hsmall hδ hδT hP0).physicalF T κ w₁ w₂ p

noncomputable def NavierStokes.TransitionRamp.physicalProfiles {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalProfile.ProfileFamily d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (hP0 : ContDiff ℝ (↑⊤) P0) {T κ w₁ w₂ : ℝ} (hT : 0 < T) (hb : δ ≤ (ofNatural F hΛ hsmall hδ hδT hP0).bigTime) (hw₁ : 0 < w₁) (hw₂ : 0 < w₂) : ProfileHistories.Profiles (ReferencePath.Input.ofNatural hΛ F).radialDomain

The pressure and all moments are recomputed from these exact physical fields. This is the object used by the later cone and matching modules.

Equations

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

theorem NavierStokes.TransitionRamp.physical_fields_natural {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalProfile.ProfileFamily d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (hP0 : ContDiff ℝ (↑⊤) P0) (T κ w₁ w₂ : ℝ) {p : ProfileHistories.Point} (hp : p.1 ≤ (ReferencePath.Input.ofNatural hΛ F).endpoint) : (ofNatural F hΛ hsmall hδ hδT hP0).physicalF T κ w₁ w₂ p = F.f p ∧ (ofNatural F hΛ hsmall hδ hδT hP0).physicalU T κ w₁ p = F.U p

theorem NavierStokes.TransitionRamp.physical_fields_eq_activation {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalProfile.ProfileFamily d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (hP0 : ContDiff ℝ (↑⊤) P0) {T κ w₁ w₂ : ℝ} (hT : 0 < T) (hb : δ ≤ (ofNatural F hΛ hsmall hδ hδT hP0).bigTime) (hw₁ : 0 < w₁) (hw₂ : 0 < w₂) {p : ProfileHistories.Point} (hη : p.2 ∈ ReferencePath.parameterInterval) (hX : p.1 ≤ (ReferencePath.Input.ofNatural hΛ F).endpoint * Real.exp δ) : have R := ofNatural F hΛ hsmall hδ hδT hP0; have N := ReferencePath.Input.ofNatural hΛ F; R.physicalF T κ w₁ w₂ p = StressActivation.FromReference.f N T κ δ p ∧ R.physicalU T κ w₁ p = StressActivation.FromReference.U N T κ δ p

theorem NavierStokes.TransitionRamp.physicalF_hasDerivAt {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalProfile.ProfileFamily d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (hP0 : ContDiff ℝ (↑⊤) P0) {T κ w₁ w₂ : ℝ} (hT : 0 < T) (hb : δ ≤ (ofNatural F hΛ hsmall hδ hδT hP0).bigTime) (hw₁ : 0 < w₁) (hw₂ : 0 < w₂) {p : ProfileHistories.Point} (hη : p.2 ∈ ReferencePath.parameterInterval) (hX : 0 < p.1) : have R := ofNatural F hΛ hsmall hδ hδT hP0; HasDerivAt (fun (X : ℝ) => R.physicalF T κ w₁ w₂ (X, p.2)) (R.physicalF T κ w₁ w₂ p * angularSlope T κ R.bigTime w₁ w₂ R.angularStock (R.logPoint p) / p.1) p.1

theorem NavierStokes.TransitionRamp.physicalU_hasDerivAt {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalProfile.ProfileFamily d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (hP0 : ContDiff ℝ (↑⊤) P0) {T κ w₁ w₂ : ℝ} (hT : 0 < T) (hb : δ ≤ (ofNatural F hΛ hsmall hδ hδT hP0).bigTime) (hw₁ : 0 < w₁) (hw₂ : 0 < w₂) {p : ProfileHistories.Point} (hη : p.2 ∈ ReferencePath.parameterInterval) (hX : 0 < p.1) : have R := ofNatural F hΛ hsmall hδ hδT hP0; HasDerivAt (fun (X : ℝ) => R.physicalU T κ w₁ (X, p.2)) (axialSlope T κ R.bigTime w₁ R.axialStock (R.logPoint p) / p.1) p.1

theorem NavierStokes.TransitionRamp.physical_radial_equations {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalProfile.ProfileFamily d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (hP0 : ContDiff ℝ (↑⊤) P0) {T κ w₁ w₂ : ℝ} (hT : 0 < T) (hb : δ ≤ (ofNatural F hΛ hsmall hδ hδT hP0).bigTime) (hw₁ : 0 < w₁) (hw₂ : 0 < w₂) {p : ProfileHistories.Point} (hη : p.2 ∈ ReferencePath.parameterInterval) (hX : 0 < p.1) : have R := ofNatural F hΛ hsmall hδ hδT hP0; p.1 * ProfileHistories.radialPartial (R.physicalF T κ w₁ w₂) p / R.physicalF T κ w₁ w₂ p = angularSlope T κ R.bigTime w₁ w₂ R.angularStock (R.logPoint p) ∧ p.1 * ProfileHistories.radialPartial (R.physicalU T κ w₁) p = axialSlope T κ R.bigTime w₁ R.axialStock (R.logPoint p)

The actual physical radial derivatives satisfy the prescribed log-clock equations. The controls use the REF stocks after REF freezes.

theorem NavierStokes.TransitionRamp.StockReference.finalTime_sub_bigTime {J : Set ℝ} (R : StockReference J) : R.finalTime - R.bigTime = Real.log (11 / 10)

theorem NavierStokes.TransitionRamp.StockReference.finalTime_gt_bigTime {J : Set ℝ} (R : StockReference J) : R.bigTime < R.finalTime

theorem NavierStokes.TransitionRamp.StockReference.radius0_lt_100 {J : Set ℝ} (R : StockReference J) (hb : 0 < R.bigTime) : R.radius0 < 100

theorem NavierStokes.TransitionRamp.StockReference.logTime_sub_finalTime {J : Set ℝ} (R : StockReference J) {X : ℝ} (hX : 0 < X) : R.logTime X - R.finalTime = Real.log (X / 110)

theorem NavierStokes.TransitionRamp.StockReference.finalTime_le_logTime {J : Set ℝ} (R : StockReference J) {X : ℝ} (hX : 110 ≤ X) : R.finalTime ≤ R.logTime X

theorem NavierStokes.TransitionRamp.StockReference.physicalU_held {J : Set ℝ} (R : StockReference J) (hJ : IsOpen J) {T κ w₁ X η : ℝ} (hw₁ : 0 < w₁) (hstart : R.bigTime + w₁ ≤ R.finalTime) (hR : R.radius0 < 110) (hX : 110 ≤ X) (hη : η ∈ J) : R.physicalU T κ w₁ (X, η) = R.endpointU T κ w₁ η

theorem NavierStokes.TransitionRamp.StockReference.physicalF_held_log {J : Set ℝ} (R : StockReference J) (hJ : IsOpen J) {T κ w₁ w₂ X η : ℝ} (hw₂ : 0 < w₂) (hstart : R.bigTime + w₁ + w₂ ≤ R.finalTime) (hR : R.radius0 < 110) (hX : 110 ≤ X) (hη : η ∈ J) : R.physicalF T κ w₁ w₂ (X, η) = Real.exp (R.logAmplitude T κ w₁ w₂ (R.finalTime, η) - 2 / 5 * Real.log (X / 110))

theorem NavierStokes.TransitionRamp.StockReference.physicalF_held {J : Set ℝ} (R : StockReference J) (hJ : IsOpen J) {T κ w₁ w₂ C X η : ℝ} (hw₂ : 0 < w₂) (hstart : R.bigTime + w₁ + w₂ ≤ R.finalTime) (hR : R.radius0 < 110) (hC : 0 < C) (hX : 110 ≤ X) (hη : η ∈ J) : R.physicalF T κ w₁ w₂ (X, η) = C⁻¹ * Real.exp (Real.log (X / 110) / 10 + R.endpointLog T κ w₁ w₂ C η) / √(2 * X)

theorem NavierStokes.TransitionRamp.StockReference.endpointLog_eq_actual {J : Set ℝ} (R : StockReference J) (hJ : IsOpen J) {T κ w₁ w₂ C η : ℝ} (hw₂ : 0 < w₂) (hstart : R.bigTime + w₁ + w₂ ≤ R.finalTime) (hR : R.radius0 < 110) (hC : 0 < C) (hη : η ∈ J) : R.endpointLog T κ w₁ w₂ C η = Real.log (C * (√(2 * 110) * R.physicalF T κ w₁ w₂ (110, η)))

structure NavierStokes.TransitionRamp.StockReference.SmallLogControl {J : Set ℝ} (R : StockReference J) (K : Set ℝ) (N : ℕ) (ε T κ w₁ w₂ : ℝ) : Prop

Quantitative conclusions for the actual integral fields. The theorem below constructs one common set of parameter thresholds for all these jets.

• finish_before : R.bigTime + w₁ + w₂ < R.finalTime
• axial_jets (y : ℝ) : y ∈ Set.Icc 0 R.finalTime → ∀ η ∈ K, ∀ n ≤ N, |iteratedDeriv n (fun (ξ : ℝ) => R.axialVelocity T κ w₁ (y, ξ) - R.initialU ξ) η| < ε
• positive_log_jets (y : ℝ) : y ∈ Set.Icc 0 R.finalTime → ∀ η ∈ K, ∀ n ≤ N, 0 < n → |iteratedDeriv n (fun (ξ : ℝ) => R.logAmplitude T κ w₁ w₂ (y, ξ) - R.initialLog ξ) η| < ε
• log_value (y : ℝ) : y ∈ Set.Icc 0 (R.bigTime + w₁ + w₂) → ∀ η ∈ K, |R.logAmplitude T κ w₁ w₂ (y, η) - R.initialLog η| < ε

theorem NavierStokes.TransitionRamp.StockReference.exists_small_log_control {J : Set ℝ} (R : StockReference J) (hJ : IsOpen J) {K : Set ℝ} (hK : IsCompact K) (hKJ : K ⊆ J) (N : ℕ) (hb : 0 ≤ R.bigTime) {Tmax ε : ℝ} (hTmax : 0 < Tmax) (hε : 0 < ε) : ∃ T0 > 0, ∃ κ0 > 0, ∃ w0 > 0, T0 ≤ Tmax ∧ κ0 < 1 ∧ 2 * w0 < R.finalTime - R.bigTime ∧ ∀ T ∈ Set.Ioo 0 T0, ∀ κ ∈ Set.Ico 0 κ0, ∀ w₁ ∈ Set.Ioo 0 w0, ∀ w₂ ∈ Set.Ioo 0 w0, R.SmallLogControl K N ε T κ w₁ w₂

The compact constants are computed from the genuine REF stocks after the reference path is fixed. Then the activation width, retained control, and both final widths can be chosen independently below positive bounds.

structure NavierStokes.TransitionRamp.StockReference.SmallPhysicalControl {J : Set ℝ} (R : StockReference J) (K : Set ℝ) (N : ℕ) (ε T κ w₁ w₂ : ℝ) : Prop

The same estimates stated directly for the actual physical fields.

• finish_before : R.bigTime + w₁ + w₂ < R.finalTime
• axial_jets (X : ℝ) : X ∈ Set.Icc R.radius0 110 → ∀ η ∈ K, ∀ n ≤ N, |iteratedDeriv n (fun (ξ : ℝ) => R.physicalU T κ w₁ (X, ξ) - R.initialU ξ) η| < ε
• positive_log_jets (X : ℝ) : X ∈ Set.Icc R.radius0 110 → ∀ η ∈ K, ∀ n ≤ N, 0 < n → |iteratedDeriv n (fun (ξ : ℝ) => Real.log (R.physicalF T κ w₁ w₂ (X, ξ)) - R.initialLog ξ) η| < ε
• log_value (X : ℝ) : X ∈ Set.Icc R.radius0 (StressActivation.radius R.radius0 (R.bigTime + w₁ + w₂)) → ∀ η ∈ K, |Real.log (R.physicalF T κ w₁ w₂ (X, η)) - R.initialLog η| < ε

theorem NavierStokes.TransitionRamp.small_physical_of_log_control {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalProfile.ProfileFamily d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (hP0 : ContDiff ℝ (↑⊤) P0) {K : Set ℝ} (hKJ : K ⊆ ReferencePath.parameterInterval) {N : ℕ} {ε T κ w₁ w₂ : ℝ} (hT : 0 < T) (hb : δ ≤ (ofNatural F hΛ hsmall hδ hδT hP0).bigTime) (hw₁ : 0 < w₁) (hw₂ : 0 < w₂) (hc : (ofNatural F hΛ hsmall hδ hδT hP0).SmallLogControl K N ε T κ w₁ w₂) : (ofNatural F hΛ hsmall hδ hδT hP0).SmallPhysicalControl K N ε T κ w₁ w₂

theorem NavierStokes.TransitionRamp.exists_small_physical_control {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalProfile.ProfileFamily d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (hP0 : ContDiff ℝ (↑⊤) P0) {K : Set ℝ} (hK : IsCompact K) (hKJ : K ⊆ ReferencePath.parameterInterval) (N : ℕ) {ε : ℝ} (hε : 0 < ε) (hb : δ ≤ (ofNatural F hΛ hsmall hδ hδT hP0).bigTime) : have R := ofNatural F hΛ hsmall hδ hδT hP0; ∃ T0 > 0, ∃ κ0 > 0, ∃ w0 > 0, T0 ≤ δ ∧ κ0 < 1 ∧ 2 * w0 < R.finalTime - R.bigTime ∧ ∀ T ∈ Set.Ioo 0 T0, ∀ κ ∈ Set.Ico 0 κ0, ∀ w₁ ∈ Set.Ioo 0 w0, ∀ w₂ ∈ Set.Ioo 0 w0, R.SmallPhysicalControl K N ε T κ w₁ w₂

Direct physical error thresholds, with the reference cutoff already fixed. Setting N = 1 supplies the value and first-parameter estimates needed for all five histories and both lag stocks.

theorem NavierStokes.TransitionRamp.exists_joint_small_control {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalProfile.ProfileFamily d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (hP0 : ContDiff ℝ (↑⊤) P0) {K : Set ℝ} (hK : IsCompact K) (hKJ : K ⊆ ReferencePath.parameterInterval) (N : ℕ) {ε : ℝ} (hε : 0 < ε) (hb : δ ≤ (ofNatural F hΛ hsmall hδ hδT hP0).bigTime) : have R := ofNatural F hΛ hsmall hδ hδT hP0; ∃ T0 > 0, ∃ κ0 > 0, ∃ w0 > 0, T0 ≤ δ ∧ κ0 < 1 ∧ 2 * w0 < R.finalTime - R.bigTime ∧ ∀ T ∈ Set.Ioo 0 T0, ∀ κ ∈ Set.Ico 0 κ0, ∀ w₁ ∈ Set.Ioo 0 w0, ∀ w₂ ∈ Set.Ioo 0 w0, R.SmallLogControl K N ε T κ w₁ w₂ ∧ R.SmallPhysicalControl K N ε T κ w₁ w₂

theorem NavierStokes.TransitionRamp.initialLog_natural {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalProfile.ProfileFamily d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (hP0 : ContDiff ℝ (↑⊤) P0) (η : ℝ) : (ofNatural F hΛ hsmall hδ hδT hP0).initialLog η = Real.log (F.f ((ReferencePath.Input.ofNatural hΛ F).endpoint, η))

theorem NavierStokes.TransitionRamp.initialU_natural {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalProfile.ProfileFamily d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (hP0 : ContDiff ℝ (↑⊤) P0) (η : ℝ) : (ofNatural F hΛ hsmall hδ hδT hP0).initialU η = F.U ((ReferencePath.Input.ofNatural hΛ F).endpoint, η)

theorem NavierStokes.TransitionRamp.endpoint_rescale {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalProfile.ProfileFamily d Λ C) (hΛ : 0 < Λ) (η : ℝ) : NaturalProfile.rescalePoint Λ ((ReferencePath.Input.ofNatural hΛ F).endpoint, η) = (4, η)

theorem NavierStokes.TransitionRamp.exists_phase_bound {h j σ : ℝ} {P0 : ℝ → ℝ} (d : NaturalAxisCoefficients.AnalyticInputs h j σ P0) : ∃ B > 0, ∀ η ∈ Set.Icc (-1) 1, |NaturalAxisCoefficients.realPhase h j σ η| ≤ B

theorem NavierStokes.TransitionRamp.normalized_initialLog_formula {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (hP0 : ContDiff ℝ (↑⊤) P0) (E : NaturalEntrance.CoefficientProfile d Λ C) (hC : 0 < C) {η : ℝ} (hφ : AxisEvaluation.profile NaturalAxisCoefficients.window d.coefficients.epsilon E.coefficients.1 (4, η) ≠ 0) : Real.log C + (ofNatural E.family hΛ hsmall hδ hδT hP0).initialLog η = Λ * NaturalAxisCoefficients.realPhase h j σ η + Real.log (AxisEvaluation.profile NaturalAxisCoefficients.window d.coefficients.epsilon E.coefficients.1 (4, η))

theorem NavierStokes.TransitionRamp.exists_uniform_initialLog_bound {h j σ Λ : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) (hP0 : ContDiff ℝ (↑⊤) P0) (hσ : 0 < σ) (hscale : AxisReference.stabilityScale d.coefficients.epsilon (NaturalProfile.profileErrorConstant d) ≤ Λ) : ∃ B > 0, ∀ (C : ℝ), 0 < C → ∀ (E : NaturalEntrance.CoefficientProfile d Λ C) (δ : ℝ) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit), ∀ η ∈ Set.Icc (-1) 1, |Real.log C + (ofNatural E.family hΛ hsmall hδ hδT hP0).initialLog η| ≤ B

The bound precedes the choice of normalization C. Its only profile input is the uniform coefficient-space ball and the proved Phi > 1/8.

theorem NavierStokes.TransitionRamp.initialU_error_jet {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (hP0 : ContDiff ℝ (↑⊤) P0) (E : NaturalEntrance.CoefficientProfile d Λ C) (n : ℕ) {η : ℝ} (hη : η ∈ ReferencePath.parameterInterval) : iteratedDeriv n (fun (ξ : ℝ) => (ofNatural E.family hΛ hsmall hδ hδT hP0).initialU ξ - NaturalAxisData.U j ξ) η = 1 / Λ * AxisEvaluation.mixedSeries NaturalAxisCoefficients.window d.coefficients.epsilon E.coefficients.2 0 n (4, η)

theorem NavierStokes.TransitionRamp.initialU_error_jet_bound {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (hP0 : ContDiff ℝ (↑⊤) P0) (E : NaturalEntrance.CoefficientProfile d Λ C) (n : ℕ) {η : ℝ} (hη : η ∈ ReferencePath.parameterInterval) : |iteratedDeriv n (fun (ξ : ℝ) => (ofNatural E.family hΛ hsmall hδ hδT hP0).initialU ξ - NaturalAxisData.U j ξ) η| ≤ ReferenceJetBounds.jetConstant d.coefficients 0 n / Λ

Uniform higher jets before choosing the normalization

theorem NavierStokes.TransitionRamp.nat_le_infty (n : ℕ) : ↑n ≤ ↑⊤

theorem NavierStokes.TransitionRamp.compact_scalar_jets {J K : Set ℝ} (hJ : IsOpen J) (hK : IsCompact K) (hKJ : K ⊆ J) {g : ℝ → ℝ} (hg : ContDiffOn ℝ (↑⊤) g J) (N : ℕ) : ∃ M ≥ 0, ∀ n ≤ N, ∀ η ∈ K, |iteratedDeriv n g η| ≤ M

theorem NavierStokes.TransitionRamp.local_composition_jet_bound {S U : Set ℝ} (hS : IsOpen S) (hU : IsOpen U) {f g : ℝ → ℝ} (hf : ContDiffOn ℝ (↑⊤) f S) (hg : ContDiffOn ℝ (↑⊤) g U) (hmap : Set.MapsTo f S U) {x : ℝ} (hx : x ∈ S) (n : ℕ) {B D : ℝ} (hB : ∀ i ≤ n, |iteratedDeriv i g (f x)| ≤ B) (hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → |iteratedDeriv i f x| ≤ D ^ i) : |iteratedDeriv n (g ∘ f) x| ≤ ↑n.factorial * B * D ^ n

theorem NavierStokes.TransitionRamp.finite_majorant (v : ℕ → ℝ) (N : ℕ) : ∃ (B : ℝ), 1 ≤ B ∧ ∀ n ≤ N, v n ≤ B

theorem NavierStokes.TransitionRamp.phase_smooth {h j σ : ℝ} {P0 : ℝ → ℝ} (d : NaturalAxisCoefficients.AnalyticInputs h j σ P0) : ContDiffOn ℝ (↑⊤) (NaturalAxisCoefficients.realPhase h j σ) ReferencePath.parameterInterval

theorem NavierStokes.TransitionRamp.log_smooth_positive : ContDiffOn ℝ (↑⊤) Real.log (Set.Ioi 0)

theorem NavierStokes.TransitionRamp.exists_uniform_logPhi_jets {h j σ Λ : ℝ} {P0 : ℝ → ℝ} (d : NaturalAxisCoefficients.AnalyticInputs h j σ P0) (hσ : 0 < σ) (hscale : AxisReference.stabilityScale d.coefficients.epsilon (NaturalProfile.profileErrorConstant d) ≤ Λ) (N : ℕ) : ∃ B ≥ 0, ∀ (C : ℝ) (E : NaturalEntrance.CoefficientProfile d Λ C), ∀ Y ∈ Set.Icc 0 (41 / 10), ∀ n ≤ N, ∀ η ∈ ReferencePath.parameterInterval, |iteratedDeriv n (fun (ξ : ℝ) => Real.log (AxisEvaluation.profile NaturalAxisCoefficients.window d.coefficients.epsilon E.coefficients.1 (Y, ξ))) η| ≤ B

noncomputable def NavierStokes.TransitionRamp.normalizedNaturalLog {h j σ Λ : ℝ} {P0 : ℝ → ℝ} (d : NaturalAxisCoefficients.AnalyticInputs h j σ P0) {C : ℝ} (E : NaturalEntrance.CoefficientProfile d Λ C) (Y η : ℝ) : ℝ

Normalized natural log, given by Λ * realPhase h j σ η + Real.log (AxisEvaluation.profile window d.coefficients.epsilon E.coefficients.1 (Y, η)).

Equations

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

theorem NavierStokes.TransitionRamp.normalizedNaturalLog_smooth {h j σ Λ : ℝ} {P0 : ℝ → ℝ} (d : NaturalAxisCoefficients.AnalyticInputs h j σ P0) (hσ : 0 < σ) (hscale : AxisReference.stabilityScale d.coefficients.epsilon (NaturalProfile.profileErrorConstant d) ≤ Λ) {C : ℝ} (E : NaturalEntrance.CoefficientProfile d Λ C) {Y : ℝ} (hY : Y ∈ Set.Icc 0 (41 / 10)) : ContDiffOn ℝ (↑⊤) (normalizedNaturalLog d E Y) ReferencePath.parameterInterval

theorem NavierStokes.TransitionRamp.exists_normalized_natural_jets {h j σ Λ : ℝ} {P0 : ℝ → ℝ} (d : NaturalAxisCoefficients.AnalyticInputs h j σ P0) (hΛ : 0 < Λ) (hσ : 0 < σ) (hscale : AxisReference.stabilityScale d.coefficients.epsilon (NaturalProfile.profileErrorConstant d) ≤ Λ) (N : ℕ) : ∃ (B : ℝ), 1 ≤ B ∧ ∀ (C : ℝ) (E : NaturalEntrance.CoefficientProfile d Λ C), ∀ Y ∈ Set.Icc 0 (41 / 10), ∀ n ≤ N, ∀ η ∈ Set.Icc (-1) 1, |iteratedDeriv n (normalizedNaturalLog d E Y) η| ≤ B

theorem NavierStokes.TransitionRamp.natural_normalization_identity {h j σ Λ : ℝ} {P0 : ℝ → ℝ} (d : NaturalAxisCoefficients.AnalyticInputs h j σ P0) {C : ℝ} (E : NaturalEntrance.CoefficientProfile d Λ C) (hC : 0 < C) {X η : ℝ} (hφ : 0 < AxisEvaluation.profile NaturalAxisCoefficients.window d.coefficients.epsilon E.coefficients.1 (Λ * X, η)) : E.family.f (X, η) = C⁻¹ * Real.exp (normalizedNaturalLog d E (Λ * X) η)

theorem NavierStokes.TransitionRamp.exp_jet_bound_local {J : Set ℝ} (hJ : IsOpen J) {g : ℝ → ℝ} (hg : ContDiffOn ℝ (↑⊤) g J) {η : ℝ} (hη : η ∈ J) (n : ℕ) {B : ℝ} (hB : 1 ≤ B) (hb : ∀ i ≤ n, |iteratedDeriv i g η| ≤ B) : |iteratedDeriv n (fun (ξ : ℝ) => Real.exp (g ξ)) η| ≤ ↑n.factorial * Real.exp B * B ^ n

theorem NavierStokes.TransitionRamp.exp_jet_bound_local_of_upper {J : Set ℝ} (hJ : IsOpen J) {g : ℝ → ℝ} (hg : ContDiffOn ℝ (↑⊤) g J) {η : ℝ} (hη : η ∈ J) (n : ℕ) {B : ℝ} (hB : 1 ≤ B) (hvalue : g η ≤ B) (hb : ∀ (i : ℕ), 1 ≤ i → i ≤ n → |iteratedDeriv i g η| ≤ B) : |iteratedDeriv n (fun (ξ : ℝ) => Real.exp (g ξ)) η| ≤ ↑n.factorial * Real.exp B * B ^ n

theorem NavierStokes.TransitionRamp.jet_transfer {A B : ℝ → ℝ} {η M ε : ℝ} (n : ℕ) (hA : ContDiffAt ℝ (↑⊤) A η) (hB : ContDiffAt ℝ (↑⊤) B η) (he : |iteratedDeriv n (fun (ξ : ℝ) => A ξ - B ξ) η| ≤ ε) (hb : |iteratedDeriv n B η| ≤ M) : |iteratedDeriv n A η| ≤ M + ε

noncomputable def NavierStokes.TransitionRamp.StockReference.normalizedInitial {J : Set ℝ} (R : StockReference J) (C η : ℝ) : ℝ

Normalized initial, given by Real.log C + R.initialLog η.

Equations

• R.normalizedInitial C η = Real.log C + R.initialLog η

noncomputable def NavierStokes.TransitionRamp.StockReference.normalizedLog {J : Set ℝ} (R : StockReference J) (T κ w₁ w₂ C y η : ℝ) : ℝ

Normalized log, given by Real.log C + R.logAmplitude T κ w₁ w₂ (y, η).

Equations

• R.normalizedLog T κ w₁ w₂ C y η = Real.log C + R.logAmplitude T κ w₁ w₂ (y, η)

theorem NavierStokes.TransitionRamp.StockReference.normalizedInitial_smooth {J : Set ℝ} (R : StockReference J) (hJ : IsOpen J) (C : ℝ) : ContDiffOn ℝ (↑⊤) (R.normalizedInitial C) J

theorem NavierStokes.TransitionRamp.StockReference.normalizedLog_smooth {J : Set ℝ} (R : StockReference J) (hJ : IsOpen J) (T κ w₁ w₂ C y : ℝ) : ContDiffOn ℝ (↑⊤) (R.normalizedLog T κ w₁ w₂ C y) J

theorem NavierStokes.TransitionRamp.StockReference.normalizedLog_hold {J : Set ℝ} (R : StockReference J) (hJ : IsOpen J) {T κ w₁ w₂ C a y η : ℝ} (hw₂ : 0 < w₂) (ha : R.bigTime + w₁ + w₂ ≤ a) (hay : a ≤ y) (hη : η ∈ J) : R.normalizedLog T κ w₁ w₂ C y η = R.normalizedLog T κ w₁ w₂ C a η - 2 / 5 * (y - a)

theorem NavierStokes.TransitionRamp.StockReference.normalizedLog_hold_positive_jet {J : Set ℝ} (R : StockReference J) (hJ : IsOpen J) {T κ w₁ w₂ C a y η : ℝ} (hw₂ : 0 < w₂) (ha : R.bigTime + w₁ + w₂ ≤ a) (hay : a ≤ y) (hη : η ∈ J) {n : ℕ} (hn : 0 < n) : iteratedDeriv n (R.normalizedLog T κ w₁ w₂ C y) η = iteratedDeriv n (R.normalizedLog T κ w₁ w₂ C a) η

theorem NavierStokes.TransitionRamp.StockReference.normalizedLog_bounds_of_control {J : Set ℝ} (R : StockReference J) (hJ : IsOpen J) {K : Set ℝ} (hKJ : K ⊆ J) {N : ℕ} {T κ w₁ w₂ C B : ℝ} (hb : 0 ≤ R.bigTime) (hw₁ : 0 < w₁) (hw₂ : 0 < w₂) (hc : R.SmallLogControl K N 1 T κ w₁ w₂) (hi : ∀ n ≤ N, ∀ η ∈ K, |iteratedDeriv n (R.normalizedInitial C) η| ≤ B) (y : ℝ) : 0 ≤ y → ∀ η ∈ K, R.normalizedLog T κ w₁ w₂ C y η ≤ B + 1 ∧ ∀ n ≤ N, 0 < n → |iteratedDeriv n (R.normalizedLog T κ w₁ w₂ C y) η| ≤ B + 1

theorem NavierStokes.TransitionRamp.StockReference.endpointLog_jets_of_control {J : Set ℝ} (R : StockReference J) (hJ : IsOpen J) {K : Set ℝ} (hKJ : K ⊆ J) {N : ℕ} {T κ w₁ w₂ C B : ℝ} (hb : 0 ≤ R.bigTime) (hw₁ : 0 < w₁) (hw₂ : 0 < w₂) (hc : R.SmallLogControl K N 1 T κ w₁ w₂) (hi : ∀ n ≤ N, ∀ η ∈ K, |iteratedDeriv n (R.normalizedInitial C) η| ≤ B) (n : ℕ) : n ≤ N → ∀ η ∈ K, |iteratedDeriv n (R.endpointLog T κ w₁ w₂ C) η| ≤ B + 1 + 2 / 5 * Real.log (11 / 10) + |Real.log 220 / 2|

theorem NavierStokes.TransitionRamp.StockReference.SmallLogControl.mono_tolerance {J : Set ℝ} (R : StockReference J) {K : Set ℝ} {N : ℕ} {ε ε' T κ w₁ w₂ : ℝ} (hc : R.SmallLogControl K N ε T κ w₁ w₂) (hε : ε ≤ ε') : R.SmallLogControl K N ε' T κ w₁ w₂

theorem NavierStokes.TransitionRamp.StockReference.axialVelocity_jets_of_control {J : Set ℝ} (R : StockReference J) (hJ : IsOpen J) {K : Set ℝ} (hKJ : K ⊆ J) {N : ℕ} {T κ w₁ w₂ B : ℝ} (hb : 0 ≤ R.bigTime) (hw₁ : 0 < w₁) (hw₂ : 0 < w₂) (hc : R.SmallLogControl K N 1 T κ w₁ w₂) (hi : ∀ n ≤ N, ∀ η ∈ K, |iteratedDeriv n R.initialU η| ≤ B) (y : ℝ) : 0 ≤ y → ∀ η ∈ K, ∀ n ≤ N, |iteratedDeriv n (fun (ξ : ℝ) => R.axialVelocity T κ w₁ (y, ξ)) η| ≤ B + 1

theorem NavierStokes.TransitionRamp.StockReference.physicalF_postaxis_jet_bound {J : Set ℝ} (R : StockReference J) (hJ : IsOpen J) {K : Set ℝ} (hKJ : K ⊆ J) {N : ℕ} {T κ w₁ w₂ C B X η : ℝ} (hb : 0 ≤ R.bigTime) (hw₁ : 0 < w₁) (hw₂ : 0 < w₂) (hC : 0 < C) (hB : 1 ≤ B) (hX : R.radius0 < X) (hη : η ∈ K) (hc : R.SmallLogControl K N 1 T κ w₁ w₂) (hi : ∀ n ≤ N, ∀ η ∈ K, |iteratedDeriv n (R.normalizedInitial C) η| ≤ B) {n : ℕ} (hn : n ≤ N) : |iteratedDeriv n (fun (ξ : ℝ) => R.physicalF T κ w₁ w₂ (X, ξ)) η| ≤ ↑n.factorial * Real.exp (B + 1) * (B + 1) ^ n / C

theorem NavierStokes.TransitionRamp.StockReference.physicalU_postaxis_jet_bound {J : Set ℝ} (R : StockReference J) (hJ : IsOpen J) {K : Set ℝ} (hKJ : K ⊆ J) {N : ℕ} {T κ w₁ w₂ B X η : ℝ} (hb : 0 ≤ R.bigTime) (hw₁ : 0 < w₁) (hw₂ : 0 < w₂) (hX : R.radius0 < X) (hη : η ∈ K) (hc : R.SmallLogControl K N 1 T κ w₁ w₂) (hi : ∀ n ≤ N, ∀ η ∈ K, |iteratedDeriv n R.initialU η| ≤ B) {n : ℕ} (hn : n ≤ N) : |iteratedDeriv n (fun (ξ : ℝ) => R.physicalU T κ w₁ (X, ξ)) η| ≤ B + 1

theorem NavierStokes.TransitionRamp.naturalU_slice_smooth {h j σ Λ : ℝ} {P0 : ℝ → ℝ} (d : NaturalAxisCoefficients.AnalyticInputs h j σ P0) {C : ℝ} (E : NaturalEntrance.CoefficientProfile d Λ C) {X : ℝ} (hY : Λ * X ∈ Set.Ioo (-20) 20) : ContDiffOn ℝ (↑⊤) (fun (η : ℝ) => E.family.U (X, η)) ReferencePath.parameterInterval

theorem NavierStokes.TransitionRamp.naturalU_error_jet {h j σ Λ : ℝ} {P0 : ℝ → ℝ} (d : NaturalAxisCoefficients.AnalyticInputs h j σ P0) {C : ℝ} (E : NaturalEntrance.CoefficientProfile d Λ C) {X η : ℝ} (hY : Λ * X ∈ Set.Ioo (-20) 20) (hη : η ∈ ReferencePath.parameterInterval) (n : ℕ) : iteratedDeriv n (fun (ξ : ℝ) => E.family.U (X, ξ) - NaturalAxisData.U j ξ) η = 1 / Λ * AxisEvaluation.mixedSeries NaturalAxisCoefficients.window d.coefficients.epsilon E.coefficients.2 0 n (Λ * X, η)

theorem NavierStokes.TransitionRamp.exists_naturalU_jets {h j σ Λ : ℝ} {P0 : ℝ → ℝ} (d : NaturalAxisCoefficients.AnalyticInputs h j σ P0) (hΛ : 0 < Λ) (N : ℕ) : ∃ (B : ℝ), 1 ≤ B ∧ ∀ (C : ℝ) (E : NaturalEntrance.CoefficientProfile d Λ C) (X : ℝ), Λ * X ∈ Set.Icc 0 (41 / 10) → ∀ n ≤ N, ∀ η ∈ Set.Icc (-1) 1, |iteratedDeriv n (fun (ξ : ℝ) => E.family.U (X, ξ)) η| ≤ B

theorem NavierStokes.TransitionRamp.naturalF_jet_bound {h j σ Λ : ℝ} {P0 : ℝ → ℝ} (d : NaturalAxisCoefficients.AnalyticInputs h j σ P0) (hσ : 0 < σ) (hscale : AxisReference.stabilityScale d.coefficients.epsilon (NaturalProfile.profileErrorConstant d) ≤ Λ) {C : ℝ} (E : NaturalEntrance.CoefficientProfile d Λ C) (hC : 0 < C) {X η B : ℝ} (hY : Λ * X ∈ Set.Icc 0 (41 / 10)) (hη : η ∈ Set.Icc (-1) 1) {N n : ℕ} (hn : n ≤ N) (hB : 1 ≤ B) (hb : ∀ i ≤ N, ∀ ξ ∈ Set.Icc (-1) 1, |iteratedDeriv i (normalizedNaturalLog d E (Λ * X)) ξ| ≤ B) : |iteratedDeriv n (fun (ξ : ℝ) => E.family.f (X, ξ)) η| ≤ ↑n.factorial * Real.exp (B + 1) * (B + 1) ^ n / C

theorem NavierStokes.TransitionRamp.normalizedInitial_jets {h j σ Λ : ℝ} {P0 : ℝ → ℝ} (d : NaturalAxisCoefficients.AnalyticInputs h j σ P0) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) (hscale : AxisReference.stabilityScale d.coefficients.epsilon (NaturalProfile.profileErrorConstant d) ≤ Λ) (hP0 : ContDiff ℝ (↑⊤) P0) {C : ℝ} (E : NaturalEntrance.CoefficientProfile d Λ C) (hC : 0 < C) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) {N : ℕ} {B : ℝ} (hb : ∀ n ≤ N, ∀ η ∈ Set.Icc (-1) 1, |iteratedDeriv n (normalizedNaturalLog d E 4) η| ≤ B) (n : ℕ) : n ≤ N → ∀ η ∈ Set.Icc (-1) 1, |iteratedDeriv n ((ofNatural E.family hΛ hsmall hδ hδT hP0).normalizedInitial C) η| ≤ B

theorem NavierStokes.TransitionRamp.endpointU_error_jet_bound {h j σ Λ : ℝ} {P0 : ℝ → ℝ} (d : NaturalAxisCoefficients.AnalyticInputs h j σ P0) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) (hP0 : ContDiff ℝ (↑⊤) P0) {C : ℝ} (E : NaturalEntrance.CoefficientProfile d Λ C) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) {N : ℕ} {ε T κ w₁ w₂ : ℝ} (hb : 0 ≤ (ofNatural E.family hΛ hsmall hδ hδT hP0).bigTime) (hc : (ofNatural E.family hΛ hsmall hδ hδT hP0).SmallLogControl (Set.Icc (-1) 1) N ε T κ w₁ w₂) {n : ℕ} (hn : n ≤ N) {η : ℝ} (hη : η ∈ Set.Icc (-1) 1) : |iteratedDeriv n (fun (ξ : ℝ) => (ofNatural E.family hΛ hsmall hδ hδT hP0).endpointU T κ w₁ ξ - NaturalAxisData.U j ξ) η| ≤ ReferenceJetBounds.jetConstant d.coefficients 0 n / Λ + ε

The actual held axial endpoint remains within the coefficient error and the chosen continuation error of the prescribed axial datum, in every fixed parameter derivative.

theorem NavierStokes.TransitionRamp.endpointU_four_eta_jet_bound {h j σ Λ : ℝ} {P0 : ℝ → ℝ} (d : NaturalAxisCoefficients.AnalyticInputs h j σ P0) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) (hP0 : ContDiff ℝ (↑⊤) P0) {C : ℝ} (E : NaturalEntrance.CoefficientProfile d Λ C) {δ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) {N : ℕ} {ε T κ w₁ w₂ : ℝ} (hb : 0 ≤ (ofNatural E.family hΛ hsmall hδ hδT hP0).bigTime) (hc : (ofNatural E.family hΛ hsmall hδ hδT hP0).SmallLogControl (Set.Icc (-1) 1) N ε T κ w₁ w₂) {n : ℕ} (hn : n ≤ N) {η : ℝ} (hη : η ∈ Set.Icc (-1) 1) : |iteratedDeriv n (fun (ξ : ℝ) => (ofNatural E.family hΛ hsmall hδ hδT hP0).endpointU T κ w₁ ξ - 4 * ξ) η| ≤ ReferenceJetBounds.jetConstant d.coefficients 0 n / Λ + ε + |j|

theorem NavierStokes.TransitionRamp.ordered_seed_bounds {h j σ Λ : ℝ} {P0 : ℝ → ℝ} (d : NaturalAxisCoefficients.AnalyticInputs h j σ P0) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) (hscale : AxisReference.stabilityScale d.coefficients.epsilon (NaturalProfile.profileErrorConstant d) ≤ Λ) (hP0 : ContDiff ℝ (↑⊤) P0) (N : ℕ) : ∃ (B : ℝ), 1 ≤ B ∧ ∃ (K : ℝ), 1 ≤ K ∧ ∃ (BJ : ℝ), 1 ≤ BJ ∧ ∀ (C : ℝ), 0 < C → ∀ (E : NaturalEntrance.CoefficientProfile d Λ C) (δ : ℝ) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit), have R := ofNatural E.family hΛ hsmall hδ hδT hP0; ∀ (T κ w₁ w₂ : ℝ), δ ≤ R.bigTime → 0 < w₁ → 0 < w₂ → R.SmallLogControl (Set.Icc (-1) 1) N 1 T κ w₁ w₂ → (∀ (X : ℝ), 0 ≤ X → ∀ η ∈ Set.Icc (-1) 1, ∀ n ≤ N, |iteratedDeriv n (fun (ξ : ℝ) => R.physicalF T κ w₁ w₂ (X, ξ)) η| ≤ K / C ∧ |iteratedDeriv n (fun (ξ : ℝ) => R.physicalU T κ w₁ (X, ξ)) η| ≤ B) ∧ ∀ η ∈ Set.Icc (-1) 1, ∀ n ≤ N, |iteratedDeriv n (R.endpointLog T κ w₁ w₂ C) η| ≤ BJ ∧ |iteratedDeriv n (R.endpointU T κ w₁) η| ≤ B

Uniform bounds for the full, actually constructed, seed. The constants are chosen after the scale and before C; the short ramp controls are chosen after the concrete coefficient-space solution. The bound is valid at every nonnegative radius, so it also covers any later finite shape interval.