Actual shaped-hold errors with constants uniform in the small slope

The angular lag is solved exactly from its incoming value at holdStart. The two decaying modes are kept separate, so no inverse small-slope constant appears in the error estimate.

theorem NavierStokes.ShapedWaitBounds.affine_envelope_bound {initial source initialScale sourceScale energy time : ℝ} (hInitial : initial ≤ initialScale * energy) (hSource : source ≤ sourceScale * energy) (hInitialScale : 0 ≤ initialScale) (hSourceScale : 0 ≤ sourceScale) (hEnergy : 0 ≤ energy) (hTime : 0 ≤ time) : initial + time * source ≤ (initialScale + sourceScale) * (1 + time) * energy

Combine initial and source bounds under one nonnegative affine envelope.

theorem NavierStokes.ShapedWaitBounds.linearLag_neg (r b : ℝ → ℝ) (q₀ y : ℝ) : OutgoingTail.linearLag r (fun (t : ℝ) => -b t) (-q₀) y = -OutgoingTail.linearLag r b q₀ y

theorem NavierStokes.ShapedWaitBounds.linearLag_le_constant {r b : ℝ → ℝ} (hr : Continuous r) (hb : Continuous b) {q₀ B y : ℝ} (hy : 0 ≤ y) (hq : q₀ ≤ B) (hs : ∀ t ∈ Set.Icc 0 y, b t ≤ r t * B) : OutgoingTail.linearLag r b q₀ y ≤ B

theorem NavierStokes.ShapedWaitBounds.linearLag_abs_le {r b : ℝ → ℝ} (hr : Continuous r) (hb : Continuous b) {q₀ B y : ℝ} (hy : 0 ≤ y) (hq : |q₀| ≤ B) (hs : ∀ t ∈ Set.Icc 0 y, |b t| ≤ r t * B) : |OutgoingTail.linearLag r b q₀ y| ≤ B

theorem NavierStokes.ShapedWaitBounds.angularSource_abs_bound (c : OutgoingSchedule.Parameters) {h y η : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1 / 100) (hy : 0 ≤ y) (hη : |η| ≤ 1) : |OutgoingEntranceCone.angularSource c h η y| ≤ 8

theorem NavierStokes.ShapedWaitBounds.angularLag_abs_bound (c : OutgoingSchedule.Parameters) {h y η : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1 / 100) (hy : 0 ≤ y) (hη : |η| ≤ 1) : |OutgoingEntranceCone.angularLag c h η y| ≤ 10

noncomputable def NavierStokes.ShapedWaitBounds.equilibrium (c : OutgoingSchedule.Parameters) (h η : ℝ) : ℝ

Equilibrium, given by (c.lam - h + D h * η * shapeGradient η) / (1 - c.lam).

Equations

• NavierStokes.ShapedWaitBounds.equilibrium c h η = (c.lam - h + NavierStokes.NaturalAxisData.D h * η * NavierStokes.OutgoingEntranceCone.shapeGradient η) / (1 - c.lam)

noncomputable def NavierStokes.ShapedWaitBounds.holdCoefficient (c : OutgoingSchedule.Parameters) (h η : ℝ) : ℝ

Hold coefficient, given by L h η * averagedDrop c c.holdStart.

Equations

• NavierStokes.ShapedWaitBounds.holdCoefficient c h η = NavierStokes.NaturalAxisData.L h η * NavierStokes.OutgoingEntranceCone.averagedDrop c c.holdStart

noncomputable def NavierStokes.ShapedWaitBounds.holdSource (c : OutgoingSchedule.Parameters) (h η t : ℝ) : ℝ

Hold source, given by `c.lam - h + D h * η * shapeGradient η - c.lam * holdCoefficient c h η

• Real.exp (-t)`.

Equations

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

noncomputable def NavierStokes.ShapedWaitBounds.holdFormula (c : OutgoingSchedule.Parameters) (h η t : ℝ) : ℝ

Hold formula, constructed using equilibrium.

Equations

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

theorem NavierStokes.ShapedWaitBounds.hold_rate_pos (c : OutgoingSchedule.Parameters) : 0 < 1 - c.lam

theorem NavierStokes.ShapedWaitBounds.dropCoefficient_hold (c : OutgoingSchedule.Parameters) {t : ℝ} (ht : 0 ≤ t) : OutgoingSchedule.dropCoefficient c.m (c.holdStart + t) = 0

theorem NavierStokes.ShapedWaitBounds.averagedDrop_hold (c : OutgoingSchedule.Parameters) {t : ℝ} (ht : 0 ≤ t) : OutgoingEntranceCone.averagedDrop c (c.holdStart + t) = Real.exp (-t) * OutgoingEntranceCone.averagedDrop c c.holdStart

theorem NavierStokes.ShapedWaitBounds.angularRate_hold (c : OutgoingSchedule.Parameters) {t : ℝ} (ht : 0 ≤ t) : OutgoingEntranceCone.angularRate c (c.holdStart + t) = 1 - c.lam

theorem NavierStokes.ShapedWaitBounds.angularSource_hold (c : OutgoingSchedule.Parameters) (h η : ℝ) {t : ℝ} (ht : 0 ≤ t) : OutgoingEntranceCone.angularSource c h η (c.holdStart + t) = holdSource c h η t

theorem NavierStokes.ShapedWaitBounds.decay_hasDerivAt (r t : ℝ) : HasDerivAt (fun (t : ℝ) => Real.exp (-r * t)) (-r * Real.exp (-r * t)) t

theorem NavierStokes.ShapedWaitBounds.holdFormula_hasDerivAt (c : OutgoingSchedule.Parameters) (h η t : ℝ) : HasDerivAt (holdFormula c h η) (holdSource c h η t - (1 - c.lam) * holdFormula c h η t) t

theorem NavierStokes.ShapedWaitBounds.angularLag_hold_formula (c : OutgoingSchedule.Parameters) (h η : ℝ) {t : ℝ} (ht : 0 ≤ t) : OutgoingEntranceCone.angularLag c h η (c.holdStart + t) = holdFormula c h η t

Exact integration of the shaped-hold equation, with no division by λ.

theorem NavierStokes.ShapedWaitBounds.equilibrium_bounds (v : OutgoingTail.TailData) {η : ℝ} (hh1 : v.h ≤ 1 / 100) (hη : |η| ≤ 1) : 0 ≤ equilibrium v.core v.h η ∧ equilibrium v.core v.h η ≤ 1

theorem NavierStokes.ShapedWaitBounds.holdCoefficient_bounds (c : OutgoingSchedule.Parameters) {h η : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1 / 100) (hη : |η| ≤ 1) : 0 ≤ holdCoefficient c h η ∧ holdCoefficient c h η ≤ 4

theorem NavierStokes.ShapedWaitBounds.angularLag_hold_error (v : OutgoingTail.TailData) {η t : ℝ} (hh1 : v.h ≤ 1 / 100) (hη : |η| ≤ 1) (ht : 0 ≤ t) : |OutgoingEntranceCone.angularLag v.core v.h η (v.core.holdStart + t) - equilibrium v.core v.h η| ≤ 19 * Real.exp (-(1 - v.core.lam) * t)

theorem NavierStokes.ShapedWaitBounds.canonical_Qs_pulseStart_error {v : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness v K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (hh1 : v.h ≤ 1 / 100) {η : ℝ} (hη : |η| ≤ 1) : |OutgoingHistories.Qs w Amp (v.core.pulseStart, η) - equilibrium v.core v.h η| ≤ 19 * Real.exp (-(1 - v.core.lam) * v.core.wait)

noncomputable def NavierStokes.ShapedWaitBounds.waitForPower (c : OutgoingSchedule.Parameters) (n : ℕ) : ℝ

Wait for power, given by -(n : ℝ) * Real.log c.lam / (1 - c.lam).

Equations

• NavierStokes.ShapedWaitBounds.waitForPower c n = -↑n * Real.log c.lam / (1 - c.lam)

theorem NavierStokes.ShapedWaitBounds.decay_le_power (c : OutgoingSchedule.Parameters) (n : ℕ) (ht : waitForPower c n ≤ c.wait) : Real.exp (-(1 - c.lam) * c.wait) ≤ c.lam ^ n

theorem NavierStokes.ShapedWaitBounds.canonical_Qs_pulseStart_power_error {v : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness v K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (hh1 : v.h ≤ 1 / 100) {η : ℝ} (hη : |η| ≤ 1) (n : ℕ) (hwait : waitForPower v.core n ≤ v.core.wait) : |OutgoingHistories.Qs w Amp (v.core.pulseStart, η) - equilibrium v.core v.h η| ≤ 19 * v.core.lam ^ n

The positive shaped-hold floor

noncomputable def NavierStokes.ShapedWaitBounds.holdFloor (m : ℝ) : ℝ

Hold floor, given by min (coneFloor * Real.exp (-entranceTime m) / 4) (1 / 16).

Equations

• NavierStokes.ShapedWaitBounds.holdFloor m = min (NavierStokes.OutgoingEntranceCone.coneFloor * Real.exp (-NavierStokes.OutgoingEntranceCone.entranceTime m) / 4) (1 / 16)

theorem NavierStokes.ShapedWaitBounds.holdFloor_pos (m : ℝ) : 0 < holdFloor m

theorem NavierStokes.ShapedWaitBounds.holdFloor_bounds (m : ℝ) : holdFloor m ≤ OutgoingEntranceCone.coneFloor ∧ holdFloor m ≤ 1 / 16 ∧ 4 * holdFloor m ≤ OutgoingEntranceCone.coneFloor * Real.exp (-OutgoingEntranceCone.entranceTime m)

theorem NavierStokes.ShapedWaitBounds.holdSource_lower (v : OutgoingTail.TailData) {η t : ℝ} (hh1 : v.h ≤ 1 / 100) (hhlam : v.h ≤ v.core.lam / 4) (hη : |η| ≤ 1) (ht : 0 ≤ t) : v.core.lam / 4 + 49 / 100 * η ^ 2 ≤ holdSource v.core v.h η t

theorem NavierStokes.ShapedWaitBounds.holdFormula_eq_linearLag (c : OutgoingSchedule.Parameters) (h η t : ℝ) : holdFormula c h η t = OutgoingTail.linearLag (fun (x : ℝ) => 1 - c.lam) (holdSource c h η) (OutgoingEntranceCone.angularLag c h η c.holdStart) t

theorem NavierStokes.ShapedWaitBounds.angularLag_hold_lower (v : OutgoingTail.TailData) {η t : ℝ} (hh1 : v.h ≤ 1 / 100) (hhlam : v.h ≤ v.core.lam / 4) (hhT : v.h ≤ Real.exp (-(v.core.holdStart + 3 / 5)) / 8) (hη : |η| ≤ 1) (ht : 0 ≤ t) : holdFloor v.core.m * (η ^ 2 + v.core.lam + Real.exp (-(1 - v.core.lam) * t)) ≤ OutgoingEntranceCone.angularLag v.core v.h η (v.core.holdStart + t)

The axial source and its actual convolution on the hold

theorem NavierStokes.ShapedWaitBounds.pressureClock_contDiff (c : OutgoingSchedule.Parameters) : ContDiff ℝ (↑⊤) (OutgoingEntranceCone.pressureClock c)

theorem NavierStokes.ShapedWaitBounds.entrancePressure_contDiff (v : OutgoingTail.TailData) : ContDiff ℝ ↑⊤ fun (p : ℝ × ℝ) => OutgoingEntranceCone.entrancePressure v p.1 p.2

theorem NavierStokes.ShapedWaitBounds.pressureGradient_contDiff (v : OutgoingTail.TailData) : ContDiff ℝ ↑⊤ fun (p : ℝ × ℝ) => OutgoingEntranceCone.pressureGradient v p.1 p.2

theorem NavierStokes.ShapedWaitBounds.pressureAxialSource_contDiff (v : OutgoingTail.TailData) : ContDiff ℝ ↑⊤ fun (p : ℝ × ℝ) => OutgoingEntranceCone.pressureAxialSource v p.1 p.2

theorem NavierStokes.ShapedWaitBounds.geometricAxialSource_hold (c : OutgoingSchedule.Parameters) (h η : ℝ) {t : ℝ} (ht : 0 ≤ t) : OutgoingEntranceCone.geometricAxialSource c h (c.holdStart + t) η = 0

theorem NavierStokes.ShapedWaitBounds.axialLag_hold_history (v : OutgoingTail.TailData) (η : ℝ) {t : ℝ} (ht : 0 ≤ t) : OutgoingEntranceCone.axialLag v (v.core.holdStart + t) η = OutgoingEntranceCone.historyAverage (fun (u : ℝ) => OutgoingEntranceCone.pressureAxialSource v (v.core.holdStart + u) η) (OutgoingEntranceCone.axialLag v v.core.holdStart η) t

theorem NavierStokes.ShapedWaitBounds.historyAverage_abs_bound {b : ℝ → ℝ} {b₀ A B t : ℝ} (ht : 0 ≤ t) (hb₀ : |b₀| ≤ A) (hb : ∀ u ∈ Set.Icc 0 t, |Real.exp u * b u| ≤ B) : |OutgoingEntranceCone.historyAverage b b₀ t| ≤ Real.exp (-t) * (A + t * B)

theorem NavierStokes.ShapedWaitBounds.angular_hold (c : OutgoingSchedule.Parameters) (η : ℝ) {t : ℝ} (ht : 0 ≤ t) : OutgoingSchedule.angular c.P c.dropLength c.lam (c.holdStart + t, η) = OutgoingSchedule.angular c.P c.dropLength c.lam (c.holdStart, η) * Real.exp (-(1 / 2 + c.lam) * t)

theorem NavierStokes.ShapedWaitBounds.weighted_angular_square_hold (c : OutgoingSchedule.Parameters) (η : ℝ) {t : ℝ} (ht : 0 ≤ t) : Real.exp t * OutgoingSchedule.angular c.P c.dropLength c.lam (c.holdStart + t, η) ^ 2 = OutgoingSchedule.angular c.P c.dropLength c.lam (c.holdStart, η) ^ 2 * Real.exp (-2 * c.lam * t)

noncomputable def NavierStokes.ShapedWaitBounds.initialEnergyLower (P m : ℝ) : ℝ

Initial energy lower, given by P * Real.exp (-entranceTime m) / 2.

Equations

• NavierStokes.ShapedWaitBounds.initialEnergyLower P m = P * Real.exp (-NavierStokes.OutgoingEntranceCone.entranceTime m) / 2

noncomputable def NavierStokes.ShapedWaitBounds.initialEnergyUpper (P m : ℝ) : ℝ

Initial energy upper, given by P * Real.exp (entranceTime m).

Equations

• NavierStokes.ShapedWaitBounds.initialEnergyUpper P m = P * Real.exp (NavierStokes.OutgoingEntranceCone.entranceTime m)

noncomputable def NavierStokes.ShapedWaitBounds.initialAxialBound (P m : ℝ) : ℝ

Initial axial bound, given by 64 + (3 + 4 * pressureBound) * energyEnvelope P (entranceTime m).

Equations

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

noncomputable def NavierStokes.ShapedWaitBounds.axialWaitConstant (P m : ℝ) : ℝ

Axial wait constant, given by initialAxialBound P m / initialEnergyLower P m + pressureSourceBound * initialEnergyUpper P m.

Equations

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

theorem NavierStokes.ShapedWaitBounds.initialEnergyLower_pos {P : ℝ} (hP : 0 < P) (m : ℝ) : 0 < initialEnergyLower P m

theorem NavierStokes.ShapedWaitBounds.initialEnergyUpper_pos {P : ℝ} (hP : 0 < P) (m : ℝ) : 0 < initialEnergyUpper P m

theorem NavierStokes.ShapedWaitBounds.initialAxialBound_pos (P m : ℝ) : 0 < initialAxialBound P m

theorem NavierStokes.ShapedWaitBounds.axialWaitConstant_pos {P : ℝ} (hP : 0 < P) (m : ℝ) : 0 < axialWaitConstant P m

theorem NavierStokes.ShapedWaitBounds.angular_hold_start_bounds (c : OutgoingSchedule.Parameters) {η : ℝ} (hη : |η| ≤ 1) : initialEnergyLower c.P c.m ≤ OutgoingSchedule.angular c.P c.dropLength c.lam (c.holdStart, η) ∧ OutgoingSchedule.angular c.P c.dropLength c.lam (c.holdStart, η) ≤ initialEnergyUpper c.P c.m

theorem NavierStokes.ShapedWaitBounds.axialLag_hold_start_bound (v : OutgoingTail.TailData) {η : ℝ} (hh1 : v.h ≤ 1 / 100) (hη : |η| ≤ 1) : |OutgoingEntranceCone.axialLag v v.core.holdStart η| ≤ initialAxialBound v.core.P v.core.m * |η|

theorem NavierStokes.ShapedWaitBounds.weighted_pressure_source_bound (v : OutgoingTail.TailData) {η t : ℝ} (hh1 : v.h ≤ 1 / 100) (hη : |η| ≤ 1) (ht : 0 ≤ t) (htw : t ≤ v.core.wait) : |Real.exp t * OutgoingEntranceCone.pressureAxialSource v (v.core.holdStart + t) η| ≤ OutgoingEntranceCone.pressureSourceBound * |η| * OutgoingSchedule.angular v.core.P v.core.dropLength v.core.lam (v.core.holdStart, η) ^ 2

theorem NavierStokes.ShapedWaitBounds.axialLag_hold_bound (v : OutgoingTail.TailData) {η t : ℝ} (hh1 : v.h ≤ 1 / 100) (hη : |η| ≤ 1) (ht : 0 ≤ t) (htw : t ≤ v.core.wait) : |OutgoingEntranceCone.axialLag v (v.core.holdStart + t) η| ≤ Real.exp (-t) * (initialAxialBound v.core.P v.core.m * |η| + t * (OutgoingEntranceCone.pressureSourceBound * |η| * OutgoingSchedule.angular v.core.P v.core.dropLength v.core.lam (v.core.holdStart, η) ^ 2))

theorem NavierStokes.ShapedWaitBounds.axialLag_hold_ratio_bound (v : OutgoingTail.TailData) {η t : ℝ} (hh1 : v.h ≤ 1 / 100) (hη : |η| ≤ 1) (ht : 0 ≤ t) (htw : t ≤ v.core.wait) : |OutgoingEntranceCone.axialLag v (v.core.holdStart + t) η / OutgoingSchedule.angular v.core.P v.core.dropLength v.core.lam (v.core.holdStart + t, η)| ≤ axialWaitConstant v.core.P v.core.m * |η| * (1 + t) * Real.exp (-(1 / 2 - v.core.lam) * t)

theorem NavierStokes.ShapedWaitBounds.canonical_Ns_hold_ratio_bound {v : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness v K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) {η t : ℝ} (hh1 : v.h ≤ 1 / 100) (hη : |η| ≤ 1) (ht : 0 ≤ t) (htw : t ≤ v.core.wait) : |OutgoingHistories.Ns w Amp (v.core.holdStart + t, η) / OutgoingHistories.E w (v.core.holdStart + t, η)| ≤ axialWaitConstant v.core.P v.core.m * |η| * (1 + t) * Real.exp (-(1 / 2 - v.core.lam) * t)

Differentiating the genuine parameter-dependent histories

theorem NavierStokes.ShapedWaitBounds.linearLag_hasDerivAt_parameter {r : ℝ → ℝ} {b : ℝ × ℝ → ℝ} (hr : ContDiff ℝ (↑⊤) r) (hb : ContDiff ℝ (↑⊤) b) {q₀ : ℝ → ℝ} {q₀' η : ℝ} (hq : HasDerivAt q₀ q₀' η) (y : ℝ) : HasDerivAt (fun (θ : ℝ) => OutgoingTail.linearLag r (fun (t : ℝ) => b (t, θ)) (q₀ θ) y) (OutgoingTail.linearLag r (fun (t : ℝ) => OutgoingHistories.dEta b (t, η)) q₀' y) η

theorem NavierStokes.ShapedWaitBounds.shapeGradient_hasDerivAt (η : ℝ) : HasDerivAt OutgoingEntranceCone.shapeGradient (2 * (1 - η ^ 2) / (1 + η ^ 2) ^ 2) η

theorem NavierStokes.ShapedWaitBounds.shapeGradient_deriv_bound {η : ℝ} (hη : |η| ≤ 1) : |deriv OutgoingEntranceCone.shapeGradient η| ≤ 2

noncomputable def NavierStokes.ShapedWaitBounds.angularSourceEta (c : OutgoingSchedule.Parameters) (h η y : ℝ) : ℝ

Angular source eta as an element of ℝ.

Equations

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

theorem NavierStokes.ShapedWaitBounds.angularSource_hasDerivAt_eta (c : OutgoingSchedule.Parameters) (h y η : ℝ) : HasDerivAt (fun (θ : ℝ) => OutgoingEntranceCone.angularSource c h θ y) (angularSourceEta c h η y) η

theorem NavierStokes.ShapedWaitBounds.angularSource_joint_contDiff (c : OutgoingSchedule.Parameters) (h : ℝ) : ContDiff ℝ ↑⊤ fun (p : ℝ × ℝ) => OutgoingEntranceCone.angularSource c h p.2 p.1

theorem NavierStokes.ShapedWaitBounds.angularSourceEta_eq_dEta (c : OutgoingSchedule.Parameters) (h y η : ℝ) : OutgoingHistories.dEta (fun (p : ProfileHistories.Point) => OutgoingEntranceCone.angularSource c h p.2 p.1) (y, η) = angularSourceEta c h η y

theorem NavierStokes.ShapedWaitBounds.angularSourceEta_abs_bound (c : OutgoingSchedule.Parameters) {h y η : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1 / 100) (hy : 0 ≤ y) (hη : |η| ≤ 1) : |angularSourceEta c h η y| ≤ 100

theorem NavierStokes.ShapedWaitBounds.idealAngularLag_hasDerivAt (c : OutgoingSchedule.Parameters) (h η : ℝ) : HasDerivAt (OutgoingEntranceCone.idealAngularLag h) (angularSourceEta c h η 0 / (8 / 5)) η

theorem NavierStokes.ShapedWaitBounds.angularLag_hasDerivAt_eta (c : OutgoingSchedule.Parameters) (h η y : ℝ) : HasDerivAt (fun (θ : ℝ) => OutgoingEntranceCone.angularLag c h θ y) (OutgoingTail.linearLag (OutgoingEntranceCone.angularRate c) (angularSourceEta c h η) (angularSourceEta c h η 0 / (8 / 5)) y) η

theorem NavierStokes.ShapedWaitBounds.angularLag_deriv_eta_bound (c : OutgoingSchedule.Parameters) {h y η : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1 / 100) (hy : 0 ≤ y) (hη : |η| ≤ 1) : |deriv (fun (θ : ℝ) => OutgoingEntranceCone.angularLag c h θ y) η| ≤ 200

theorem NavierStokes.ShapedWaitBounds.equilibrium_hasDerivAt (c : OutgoingSchedule.Parameters) (h η : ℝ) : HasDerivAt (equilibrium c h) (NaturalAxisData.D h * (OutgoingEntranceCone.shapeGradient η + η * deriv OutgoingEntranceCone.shapeGradient η) / (1 - c.lam)) η

theorem NavierStokes.ShapedWaitBounds.equilibrium_deriv_bound (v : OutgoingTail.TailData) {η : ℝ} (hh1 : v.h ≤ 1 / 100) (hη : |η| ≤ 1) : |deriv (equilibrium v.core v.h) η| ≤ 4

theorem NavierStokes.ShapedWaitBounds.holdCoefficient_hasDerivAt (c : OutgoingSchedule.Parameters) (h η : ℝ) : HasDerivAt (holdCoefficient c h) (-4 * h * η * OutgoingEntranceCone.averagedDrop c c.holdStart) η

theorem NavierStokes.ShapedWaitBounds.holdCoefficient_deriv_bound (c : OutgoingSchedule.Parameters) {h η : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1 / 100) (hη : |η| ≤ 1) : |deriv (holdCoefficient c h) η| ≤ 1

theorem NavierStokes.ShapedWaitBounds.angularLag_hold_deriv_error (v : OutgoingTail.TailData) {η t : ℝ} (hh1 : v.h ≤ 1 / 100) (hη : |η| ≤ 1) (ht : 0 ≤ t) : |deriv (fun (θ : ℝ) => OutgoingEntranceCone.angularLag v.core v.h θ (v.core.holdStart + t) - equilibrium v.core v.h θ) η| ≤ 206 * Real.exp (-(1 - v.core.lam) * t)

The axial parameter derivative at the beginning of the hold

noncomputable def NavierStokes.ShapedWaitBounds.initialAxialDerivative (v : OutgoingTail.TailData) (η : ℝ) : ℝ

Initial axial derivative as an element of ℝ.

Equations

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

noncomputable def NavierStokes.ShapedWaitBounds.initialAxialDerivativeBound (P m : ℝ) : ℝ

Initial axial derivative bound, given by 256 + (32 + 16 * pressureBound) * energyEnvelope P (entranceTime m).

Equations

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

theorem NavierStokes.ShapedWaitBounds.initialAxialDerivativeBound_pos (P m : ℝ) : 0 < initialAxialDerivativeBound P m

theorem NavierStokes.ShapedWaitBounds.initialAxial_hasDerivAt (v : OutgoingTail.TailData) (η : ℝ) : HasDerivAt (fun (θ : ℝ) => OutgoingEntranceCone.axialLag v v.core.holdStart θ) (initialAxialDerivative v η) η

theorem NavierStokes.ShapedWaitBounds.initialAxialDerivative_bound (v : OutgoingTail.TailData) {η : ℝ} (hh1 : v.h ≤ 1 / 100) (hη : |η| ≤ 1) : |initialAxialDerivative v η| ≤ initialAxialDerivativeBound v.core.P v.core.m

theorem NavierStokes.ShapedWaitBounds.weighted_bound_of_angular_square (c : OutgoingSchedule.Parameters) (η : ℝ) {t B z : ℝ} (ht : 0 ≤ t) (hB : 0 ≤ B) (hz : |z| ≤ B * OutgoingSchedule.angular c.P c.dropLength c.lam (c.holdStart + t, η) ^ 2) : |Real.exp t * z| ≤ B * OutgoingSchedule.angular c.P c.dropLength c.lam (c.holdStart, η) ^ 2

theorem NavierStokes.ShapedWaitBounds.axialLag_hold_hasDerivAt_eta (v : OutgoingTail.TailData) (η : ℝ) {t : ℝ} (ht : 0 ≤ t) : HasDerivAt (fun (θ : ℝ) => OutgoingEntranceCone.axialLag v (v.core.holdStart + t) θ) (OutgoingEntranceCone.historyAverage (fun (u : ℝ) => deriv (OutgoingEntranceCone.pressureAxialSource v (v.core.holdStart + u)) η) (initialAxialDerivative v η) t) η

theorem NavierStokes.ShapedWaitBounds.axialLag_hold_deriv_bound (v : OutgoingTail.TailData) {η t : ℝ} (hh1 : v.h ≤ 1 / 100) (hη : |η| ≤ 1) (ht : 0 ≤ t) (htw : t ≤ v.core.wait) : |deriv (fun (θ : ℝ) => OutgoingEntranceCone.axialLag v (v.core.holdStart + t) θ) η| ≤ Real.exp (-t) * (initialAxialDerivativeBound v.core.P v.core.m + t * (OutgoingEntranceCone.pressureSourceBound * OutgoingSchedule.angular v.core.P v.core.dropLength v.core.lam (v.core.holdStart, η) ^ 2))

theorem NavierStokes.ShapedWaitBounds.normalize_hold_bound (c : OutgoingSchedule.Parameters) {η t A z : ℝ} (hη : |η| ≤ 1) (ht : 0 ≤ t) (hA : 0 ≤ A) (hz : |z| ≤ Real.exp (-t) * (A + t * (OutgoingEntranceCone.pressureSourceBound * OutgoingSchedule.angular c.P c.dropLength c.lam (c.holdStart, η) ^ 2))) : |z / OutgoingSchedule.angular c.P c.dropLength c.lam (c.holdStart + t, η)| ≤ (A / initialEnergyLower c.P c.m + OutgoingEntranceCone.pressureSourceBound * initialEnergyUpper c.P c.m) * (1 + t) * Real.exp (-(1 / 2 - c.lam) * t)

noncomputable def NavierStokes.ShapedWaitBounds.axialDerivativeWaitConstant (P m : ℝ) : ℝ

Axial derivative wait constant, given by initialAxialDerivativeBound P m / initialEnergyLower P m + pressureSourceBound * initialEnergyUpper P m.

Equations

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

noncomputable def NavierStokes.ShapedWaitBounds.axialRatioDerivativeWaitConstant (P m : ℝ) : ℝ

Axial ratio derivative wait constant, given by axialDerivativeWaitConstant P m + 2 * axialWaitConstant P m.

Equations

• NavierStokes.ShapedWaitBounds.axialRatioDerivativeWaitConstant P m = NavierStokes.ShapedWaitBounds.axialDerivativeWaitConstant P m + 2 * NavierStokes.ShapedWaitBounds.axialWaitConstant P m

theorem NavierStokes.ShapedWaitBounds.axialDerivativeWaitConstant_pos {P : ℝ} (hP : 0 < P) (m : ℝ) : 0 < axialDerivativeWaitConstant P m

theorem NavierStokes.ShapedWaitBounds.axialRatioDerivativeWaitConstant_pos {P : ℝ} (hP : 0 < P) (m : ℝ) : 0 < axialRatioDerivativeWaitConstant P m

theorem NavierStokes.ShapedWaitBounds.axialLag_hold_deriv_ratio_bound (v : OutgoingTail.TailData) {η t : ℝ} (hh1 : v.h ≤ 1 / 100) (hη : |η| ≤ 1) (ht : 0 ≤ t) (htw : t ≤ v.core.wait) : |deriv (fun (θ : ℝ) => OutgoingEntranceCone.axialLag v (v.core.holdStart + t) θ) η / OutgoingSchedule.angular v.core.P v.core.dropLength v.core.lam (v.core.holdStart + t, η)| ≤ axialDerivativeWaitConstant v.core.P v.core.m * (1 + t) * Real.exp (-(1 / 2 - v.core.lam) * t)

theorem NavierStokes.ShapedWaitBounds.normalizedAxial_hasDerivAt (v : OutgoingTail.TailData) (η : ℝ) {t : ℝ} (ht : 0 ≤ t) : HasDerivAt (fun (θ : ℝ) => OutgoingEntranceCone.axialLag v (v.core.holdStart + t) θ / OutgoingSchedule.angular v.core.P v.core.dropLength v.core.lam (v.core.holdStart + t, θ)) (deriv (fun (θ : ℝ) => OutgoingEntranceCone.axialLag v (v.core.holdStart + t) θ) η / OutgoingSchedule.angular v.core.P v.core.dropLength v.core.lam (v.core.holdStart + t, η) + OutgoingEntranceCone.shapeGradient η * (OutgoingEntranceCone.axialLag v (v.core.holdStart + t) η / OutgoingSchedule.angular v.core.P v.core.dropLength v.core.lam (v.core.holdStart + t, η))) η

theorem NavierStokes.ShapedWaitBounds.axialLag_hold_ratio_deriv_bound (v : OutgoingTail.TailData) {η t : ℝ} (hh1 : v.h ≤ 1 / 100) (hη : |η| ≤ 1) (ht : 0 ≤ t) (htw : t ≤ v.core.wait) : |deriv (fun (θ : ℝ) => OutgoingEntranceCone.axialLag v (v.core.holdStart + t) θ / OutgoingSchedule.angular v.core.P v.core.dropLength v.core.lam (v.core.holdStart + t, θ)) η| ≤ axialRatioDerivativeWaitConstant v.core.P v.core.m * (1 + t) * Real.exp (-(1 / 2 - v.core.lam) * t)

theorem NavierStokes.ShapedWaitBounds.canonical_Ns_hold_ratio_deriv_bound {v : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness v K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) {η t : ℝ} (hh1 : v.h ≤ 1 / 100) (hη : |η| ≤ 1) (ht : 0 ≤ t) (htw : t ≤ v.core.wait) : |deriv (fun (θ : ℝ) => OutgoingHistories.Ns w Amp (v.core.holdStart + t, θ) / OutgoingHistories.E w (v.core.holdStart + t, θ)) η| ≤ axialRatioDerivativeWaitConstant v.core.P v.core.m * (1 + t) * Real.exp (-(1 / 2 - v.core.lam) * t)

Canonical combined statements and pulse-entry powers

theorem NavierStokes.ShapedWaitBounds.canonical_Qs_hold_lower {v : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness v K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) {η t : ℝ} (hh1 : v.h ≤ 1 / 100) (hhlam : v.h ≤ v.core.lam / 4) (hhT : v.h ≤ Real.exp (-(v.core.holdStart + 3 / 5)) / 8) (hη : |η| ≤ 1) (ht : 0 ≤ t) (htw : t ≤ v.core.wait) : holdFloor v.core.m * (η ^ 2 + v.core.lam + Real.exp (-(1 - v.core.lam) * t)) ≤ OutgoingHistories.Qs w Amp (v.core.holdStart + t, η)

theorem NavierStokes.ShapedWaitBounds.canonical_Qs_hold_error {v : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness v K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) {η t : ℝ} (hh1 : v.h ≤ 1 / 100) (hη : |η| ≤ 1) (ht : 0 ≤ t) (htw : t ≤ v.core.wait) : |OutgoingHistories.Qs w Amp (v.core.holdStart + t, η) - equilibrium v.core v.h η| ≤ 19 * Real.exp (-(1 - v.core.lam) * t)

theorem NavierStokes.ShapedWaitBounds.canonical_Qs_hold_deriv_error {v : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness v K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) {η t : ℝ} (hh1 : v.h ≤ 1 / 100) (hη : |η| ≤ 1) (ht : 0 ≤ t) (htw : t ≤ v.core.wait) : |deriv (fun (θ : ℝ) => OutgoingHistories.Qs w Amp (v.core.holdStart + t, θ) - equilibrium v.core v.h θ) η| ≤ 206 * Real.exp (-(1 - v.core.lam) * t)

noncomputable def NavierStokes.ShapedWaitBounds.holdConstant (P m : ℝ) : ℝ

Hold constant, given by 206 + axialWaitConstant P m + axialRatioDerivativeWaitConstant P m.

Equations

• NavierStokes.ShapedWaitBounds.holdConstant P m = 206 + NavierStokes.ShapedWaitBounds.axialWaitConstant P m + NavierStokes.ShapedWaitBounds.axialRatioDerivativeWaitConstant P m

theorem NavierStokes.ShapedWaitBounds.holdConstant_bounds {P : ℝ} (hP : 0 < P) (m : ℝ) : 0 < holdConstant P m ∧ 206 ≤ holdConstant P m ∧ axialWaitConstant P m ≤ holdConstant P m ∧ axialRatioDerivativeWaitConstant P m ≤ holdConstant P m

theorem NavierStokes.ShapedWaitBounds.canonical_hold_estimates {v : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness v K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) {η t : ℝ} (hh1 : v.h ≤ 1 / 100) (hhlam : v.h ≤ v.core.lam / 4) (hhT : v.h ≤ Real.exp (-(v.core.holdStart + 3 / 5)) / 8) (hη : |η| ≤ 1) (ht : 0 ≤ t) (htw : t ≤ v.core.wait) : holdFloor v.core.m * (η ^ 2 + v.core.lam + Real.exp (-(1 - v.core.lam) * t)) ≤ OutgoingHistories.Qs w Amp (v.core.holdStart + t, η) ∧ |OutgoingHistories.Qs w Amp (v.core.holdStart + t, η) - equilibrium v.core v.h η| ≤ holdConstant v.core.P v.core.m * (1 + t) * Real.exp (-(1 - v.core.lam) * t) ∧ |deriv (fun (θ : ℝ) => OutgoingHistories.Qs w Amp (v.core.holdStart + t, θ) - equilibrium v.core v.h θ) η| ≤ holdConstant v.core.P v.core.m * (1 + t) * Real.exp (-(1 - v.core.lam) * t) ∧ |OutgoingHistories.Ns w Amp (v.core.holdStart + t, η) / OutgoingHistories.E w (v.core.holdStart + t, η)| ≤ holdConstant v.core.P v.core.m * |η| * (1 + t) * Real.exp (-(1 / 2 - v.core.lam) * t) ∧ |deriv (fun (θ : ℝ) => OutgoingHistories.Ns w Amp (v.core.holdStart + t, θ) / OutgoingHistories.E w (v.core.holdStart + t, θ)) η| ≤ holdConstant v.core.P v.core.m * (1 + t) * Real.exp (-(1 / 2 - v.core.lam) * t)

The complete estimates (16), including the actual first parameter derivatives, with one displayed constant depending only on the earlier P,m.

theorem NavierStokes.ShapedWaitBounds.canonical_Qs_pulseStart_deriv_power_error {v : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness v K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (hh1 : v.h ≤ 1 / 100) {η : ℝ} (hη : |η| ≤ 1) (n : ℕ) (hwait : waitForPower v.core n ≤ v.core.wait) : |deriv (fun (θ : ℝ) => OutgoingHistories.Qs w Amp (v.core.pulseStart, θ) - equilibrium v.core v.h θ) η| ≤ 206 * v.core.lam ^ n

theorem NavierStokes.ShapedWaitBounds.polynomial_decay_le_power (c : OutgoingSchedule.Parameters) (hlam : c.lam ≤ 1 / 120) (hwait : -60 * Real.log c.lam ≤ c.wait) : (1 + c.wait) * Real.exp (-(1 / 2 - c.lam) * c.wait) ≤ 120 * c.lam ^ 29

A logarithmic wait gives the claimed polynomial smallness of the axial history, including its harmless linear factor, with no hidden λ constant.

theorem NavierStokes.ShapedWaitBounds.canonical_Ns_pulseStart_power_bounds {v : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness v K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (hh1 : v.h ≤ 1 / 100) (hlam : v.core.lam ≤ 1 / 120) (hwait : -60 * Real.log v.core.lam ≤ v.core.wait) {η : ℝ} (hη : |η| ≤ 1) : |OutgoingHistories.Ns w Amp (v.core.pulseStart, η) / OutgoingHistories.E w (v.core.pulseStart, η)| ≤ 120 * axialWaitConstant v.core.P v.core.m * |η| * v.core.lam ^ 29 ∧ |deriv (fun (θ : ℝ) => OutgoingHistories.Ns w Amp (v.core.pulseStart, θ) / OutgoingHistories.E w (v.core.pulseStart, θ)) η| ≤ 120 * axialRatioDerivativeWaitConstant v.core.P v.core.m * v.core.lam ^ 29