The actual outgoing tail and its cone estimates

The controller below is identified with an actual corrected angular history by ReleaseMoments. Bounds never assume an amplitude small relative to h: the prescribed long release plateau supplies that suppression.

Pressure through the actual angular reset

The corrected pressure is the improper integral of the actual corrected field. The difference from the clean pressure is an explicit finite partial-reset integral. Bounds use the first angular coefficient jet supplied by the proved reset witness; no parity or second-jet estimate is assumed.

noncomputable def NavierStokes.CorrectedPressureBounds.correctedPi {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (y eta : ℝ) : ℝ

Corrected pi, given by -(1 / 2 : ℝ) * ∫ t in Ioi y, correctedAngular d w.coefficients (t, eta) ^ 2.

Equations

• NavierStokes.CorrectedPressureBounds.correctedPi w y eta = -(1 / 2) * ∫ (t : ℝ) in Set.Ioi y, NavierStokes.UniformAngularReset.correctedAngular d w.coefficients (t, eta) ^ 2

noncomputable def NavierStokes.CorrectedPressureBounds.editDensity {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (p : ℝ × ℝ) : ℝ

Edit density, given by correctedAngular d w.coefficients p ^ 2 - finalAngular d p ^ 2.

Equations

• NavierStokes.CorrectedPressureBounds.editDensity w p = NavierStokes.UniformAngularReset.correctedAngular d w.coefficients p ^ 2 - NavierStokes.OutgoingTail.finalAngular d p ^ 2

noncomputable def NavierStokes.CorrectedPressureBounds.releaseSquare (d : OutgoingTail.TailData) : ℝ

Release square, given by finalAngular d (d.releaseStart, 0) ^ 2.

Equations

• NavierStokes.CorrectedPressureBounds.releaseSquare d = NavierStokes.OutgoingTail.finalAngular d (d.releaseStart, 0) ^ 2

noncomputable def NavierStokes.CorrectedPressureBounds.editSize (d : OutgoingTail.TailData) (K : ℝ) : ℝ

Edit size, given by K * d.core.lam ^ (28 : ℕ).

Equations

• NavierStokes.CorrectedPressureBounds.editSize d K = K * d.core.lam ^ 28

theorem NavierStokes.CorrectedPressureBounds.releaseSquare_pos (d : OutgoingTail.TailData) : 0 < releaseSquare d

theorem NavierStokes.CorrectedPressureBounds.editSize_nonneg {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) : 0 ≤ editSize d K

theorem NavierStokes.CorrectedPressureBounds.witness_K_nonneg {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) : 0 ≤ K

theorem NavierStokes.CorrectedPressureBounds.relative_abs_le_two_norm (c : AngularMomentReset.Coeff) (t : ℝ) : |AngularMomentReset.relative c t| ≤ 2 * ‖c‖

theorem NavierStokes.CorrectedPressureBounds.relative_coefficient_bound {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta t : ℝ) : |AngularMomentReset.relative (w.coefficients eta) t| ≤ 2 * editSize d K

theorem NavierStokes.CorrectedPressureBounds.relative_eta_hasDerivAt {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta t : ℝ) : HasDerivAt (fun (q : ℝ) => AngularMomentReset.relative (w.coefficients q) t) (AngularMomentReset.relative (deriv w.coefficients eta) t) eta

theorem NavierStokes.CorrectedPressureBounds.relative_eta_bound {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta t : ℝ) : |AngularMomentReset.relative (deriv w.coefficients eta) t| ≤ 2 * editSize d K

theorem NavierStokes.CorrectedPressureBounds.corrected_square_comparison {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (p : ℝ × ℝ) : 1 / 4 * OutgoingTail.finalAngular d p ^ 2 ≤ UniformAngularReset.correctedAngular d w.coefficients p ^ 2 ∧ UniformAngularReset.correctedAngular d w.coefficients p ^ 2 ≤ 9 / 4 * OutgoingTail.finalAngular d p ^ 2

theorem NavierStokes.CorrectedPressureBounds.baseE_square_ratio (lam amp t r : ℝ) : AngularMomentReset.baseE lam amp t ^ 2 = AngularMomentReset.baseE lam amp r ^ 2 * Real.exp ((1 + 2 * lam) * (r - t))

theorem NavierStokes.CorrectedPressureBounds.window_square_bounds (d : OutgoingTail.TailData) {t : ℝ} (ht : t ∈ Set.Icc (d.releaseStart - 4) d.releaseStart) (eta : ℝ) : releaseSquare d ≤ OutgoingTail.finalAngular d (t, eta) ^ 2 ∧ OutgoingTail.finalAngular d (t, eta) ^ 2 ≤ Real.exp 5 * releaseSquare d

theorem NavierStokes.CorrectedPressureBounds.editDensity_contDiff {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) : ContDiff ℝ (↑⊤) (editDensity w)

theorem NavierStokes.CorrectedPressureBounds.editDensity_eq {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (t eta : ℝ) : editDensity w (t, eta) = AngularMomentReset.baseE d.core.lam (UniformAngularReset.referenceAmplitude d) t ^ 2 * ((1 + AngularMomentReset.relative (w.coefficients eta) (t - UniformAngularReset.correctionCenter d)) ^ 2 - 1)

theorem NavierStokes.CorrectedPressureBounds.editDensity_zero_outside {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {t : ℝ} (ht : t ∉ Set.Ioo (d.releaseStart - 4) d.releaseStart) : editDensity w (t, eta) = 0

noncomputable def NavierStokes.CorrectedPressureBounds.editDensityEta {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (p : ℝ × ℝ) : ℝ

Edit density eta, constructed using 2.

Equations

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

theorem NavierStokes.CorrectedPressureBounds.editDensity_hasDerivAt_eta {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (t eta : ℝ) : HasDerivAt (fun (q : ℝ) => editDensity w (t, q)) (editDensityEta w (t, eta)) eta

theorem NavierStokes.CorrectedPressureBounds.editDensityEta_zero_outside {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {t : ℝ} (ht : t ∉ Set.Ioo (d.releaseStart - 4) d.releaseStart) : editDensityEta w (t, eta) = 0

theorem NavierStokes.CorrectedPressureBounds.editDensityEta_continuous_t {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) : Continuous fun (t : ℝ) => editDensityEta w (t, eta)

theorem NavierStokes.CorrectedPressureBounds.editDensity_abs_le {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (t eta : ℝ) : |editDensity w (t, eta)| ≤ 5 * editSize d K * Real.exp 5 * releaseSquare d

theorem NavierStokes.CorrectedPressureBounds.editDensityEta_abs_le {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (t eta : ℝ) : |editDensityEta w (t, eta)| ≤ 6 * editSize d K * Real.exp 5 * releaseSquare d

theorem NavierStokes.CorrectedPressureBounds.integral_Ioi_increment {f : ℝ → ℝ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (a y : ℝ) : ∫ (t : ℝ) in Set.Ioi y, f t = (∫ (t : ℝ) in Set.Ioi a, f t) - ∫ (t : ℝ) in a..y, f t

theorem NavierStokes.CorrectedPressureBounds.correctedPi_increment {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (a y eta : ℝ) : correctedPi w y eta = correctedPi w a eta + 1 / 2 * ∫ (t : ℝ) in a..y, UniformAngularReset.correctedAngular d w.coefficients (t, eta) ^ 2

theorem NavierStokes.CorrectedPressureBounds.correctedPi_eq_before {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {y : ℝ} (hy : y ≤ d.releaseStart - 4) (eta : ℝ) : correctedPi w y eta = FuturePressureBounds.Pi d y eta

theorem NavierStokes.CorrectedPressureBounds.correctedPi_eq_after {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {y : ℝ} (hy : d.releaseStart ≤ y) (eta : ℝ) : correctedPi w y eta = FuturePressureBounds.Pi d y eta

theorem NavierStokes.CorrectedPressureBounds.correctedPi_eq_partial {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (y eta : ℝ) : correctedPi w y eta = FuturePressureBounds.Pi d y eta + 1 / 2 * ∫ (t : ℝ) in d.releaseStart - 4..y, editDensity w (t, eta)

noncomputable def NavierStokes.CorrectedPressureBounds.pressureChange {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (y eta : ℝ) : ℝ

Pressure change, given by correctedPi w y eta - Pi d y eta.

Equations

• NavierStokes.CorrectedPressureBounds.pressureChange w y eta = NavierStokes.CorrectedPressureBounds.correctedPi w y eta - NavierStokes.FuturePressureBounds.Pi d y eta

theorem NavierStokes.CorrectedPressureBounds.pressureChange_eq_partial {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (y eta : ℝ) : pressureChange w y eta = 1 / 2 * ∫ (t : ℝ) in d.releaseStart - 4..y, editDensity w (t, eta)

theorem NavierStokes.CorrectedPressureBounds.pressureChange_zero_before {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {y : ℝ} (hy : y ≤ d.releaseStart - 4) (eta : ℝ) : pressureChange w y eta = 0

theorem NavierStokes.CorrectedPressureBounds.pressureChange_zero_after {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {y : ℝ} (hy : d.releaseStart ≤ y) (eta : ℝ) : pressureChange w y eta = 0

theorem NavierStokes.CorrectedPressureBounds.intervalPrimitive_contDiff {f : ℝ × ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (a : ℝ) : ContDiff ℝ ↑⊤ fun (p : ℝ × ℝ) => ∫ (t : ℝ) in a..p.1, f (t, p.2)

Joint smoothness of a finite integral with a variable upper limit.

theorem NavierStokes.CorrectedPressureBounds.cleanPi_joint_contDiff (d : OutgoingTail.TailData) : ContDiff ℝ ↑⊤ fun (p : ℝ × ℝ) => FuturePressureBounds.Pi d p.1 p.2

theorem NavierStokes.CorrectedPressureBounds.pressureChange_joint_contDiff {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) : ContDiff ℝ ↑⊤ fun (p : ℝ × ℝ) => pressureChange w p.1 p.2

theorem NavierStokes.CorrectedPressureBounds.correctedPi_joint_contDiff {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) : ContDiff ℝ ↑⊤ fun (p : ℝ × ℝ) => correctedPi w p.1 p.2

theorem NavierStokes.CorrectedPressureBounds.correctedPi_hasDerivAt_y {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (y eta : ℝ) : HasDerivAt (fun (t : ℝ) => correctedPi w t eta) (1 / 2 * UniformAngularReset.correctedAngular d w.coefficients (y, eta) ^ 2) y

theorem NavierStokes.CorrectedPressureBounds.pressureChange_hasDerivAt_eta {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (y eta : ℝ) : HasDerivAt (pressureChange w y) (1 / 2 * ∫ (t : ℝ) in d.releaseStart - 4..y, editDensityEta w (t, eta)) eta

theorem NavierStokes.CorrectedPressureBounds.correctedPi_hasDerivAt_eta {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (y eta : ℝ) : HasDerivAt (correctedPi w y) (deriv (FuturePressureBounds.Pi d y) eta + 1 / 2 * ∫ (t : ℝ) in d.releaseStart - 4..y, editDensityEta w (t, eta)) eta

theorem NavierStokes.CorrectedPressureBounds.correctedPi_deriv_eta {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (y eta : ℝ) : deriv (correctedPi w y) eta = deriv (FuturePressureBounds.Pi d y) eta + deriv (pressureChange w y) eta

theorem NavierStokes.CorrectedPressureBounds.pressureChange_deriv_zero_before {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {y : ℝ} (hy : y ≤ d.releaseStart - 4) (eta : ℝ) : deriv (pressureChange w y) eta = 0

theorem NavierStokes.CorrectedPressureBounds.pressureChange_deriv_zero_after {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {y : ℝ} (hy : d.releaseStart ≤ y) (eta : ℝ) : deriv (pressureChange w y) eta = 0

theorem NavierStokes.CorrectedPressureBounds.cleanPi_eta_independent_after_flatten (d : OutgoingTail.TailData) {y : ℝ} (hy : d.flattenEnd ≤ y) (eta eta' : ℝ) : FuturePressureBounds.Pi d y eta = FuturePressureBounds.Pi d y eta'

theorem NavierStokes.CorrectedPressureBounds.correctedPi_eta_independent_after {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {y : ℝ} (hy : d.releaseStart ≤ y) (eta eta' : ℝ) : correctedPi w y eta = correctedPi w y eta'

theorem NavierStokes.CorrectedPressureBounds.correctedPi_deriv_eta_zero_after {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {y : ℝ} (hy : d.releaseStart ≤ y) (eta : ℝ) : deriv (correctedPi w y) eta = 0

theorem NavierStokes.CorrectedPressureBounds.half_partial_integral_abs_le {f : ℝ → ℝ} {B r y : ℝ} (hB : 0 ≤ B) (hy : y ∈ Set.Icc (r - 4) r) (hbound : ∀ (t : ℝ), |f t| ≤ B) : |1 / 2 * ∫ (t : ℝ) in r - 4..y, f t| ≤ 2 * B

theorem NavierStokes.CorrectedPressureBounds.pressureChange_abs_le {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (y eta : ℝ) : |pressureChange w y eta| ≤ 10 * editSize d K * Real.exp 5 * releaseSquare d

theorem NavierStokes.CorrectedPressureBounds.pressureChange_deriv_abs_le {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (y eta : ℝ) : |deriv (pressureChange w y) eta| ≤ 12 * editSize d K * Real.exp 5 * releaseSquare d

theorem NavierStokes.CorrectedPressureBounds.clean_square_le_corrected {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (p : ℝ × ℝ) : OutgoingTail.finalAngular d p ^ 2 ≤ 4 * UniformAngularReset.correctedAngular d w.coefficients p ^ 2

theorem NavierStokes.CorrectedPressureBounds.pressureChange_deriv_abs_le_corrected {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (y eta : ℝ) : |deriv (pressureChange w y) eta| ≤ 48 * Real.exp 5 * editSize d K * UniformAngularReset.correctedAngular d w.coefficients (y, eta) ^ 2

The edit derivative is controlled by the actual local corrected field.

theorem NavierStokes.CorrectedPressureBounds.correctedPi_nonpos {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (y eta : ℝ) : correctedPi w y eta ≤ 0

theorem NavierStokes.CorrectedPressureBounds.correctedPi_abs_eq {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (y eta : ℝ) : |correctedPi w y eta| = 1 / 2 * ∫ (t : ℝ) in Set.Ioi y, UniformAngularReset.correctedAngular d w.coefficients (t, eta) ^ 2

theorem NavierStokes.CorrectedPressureBounds.correctedPi_abs_le {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {y eta : ℝ} (hy : 0 ≤ y) (heta : |eta| ≤ 1) : |correctedPi w y eta| ≤ 9 / 2 * FuturePressureBounds.envelopeConstant * UniformAngularReset.correctedAngular d w.coefficients (y, eta) ^ 2

theorem NavierStokes.CorrectedPressureBounds.correctedPi_deriv_abs_le {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {y eta : ℝ} (hy : 0 ≤ y) (heta : |eta| ≤ 1) : |deriv (correctedPi w y) eta| ≤ (8 * FuturePressureBounds.envelopeConstant * |eta| + 48 * Real.exp 5 * editSize d K) * UniformAngularReset.correctedAngular d w.coefficients (y, eta) ^ 2

noncomputable def NavierStokes.CorrectedPressureBounds.correctedConstant : ℝ

Corrected constant, given by 13 * envelopeConstant + 48 * Real.exp 5.

Equations

• NavierStokes.CorrectedPressureBounds.correctedConstant = 13 * NavierStokes.FuturePressureBounds.envelopeConstant + 48 * Real.exp 5

theorem NavierStokes.CorrectedPressureBounds.correctedConstant_pos : 0 < correctedConstant

theorem NavierStokes.CorrectedPressureBounds.corrected_bounds {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {y eta : ℝ} (hy : 0 ≤ y) (heta : |eta| ≤ 1) : |correctedPi w y eta| ≤ correctedConstant * (1 + editSize d K) * UniformAngularReset.correctedAngular d w.coefficients (y, eta) ^ 2 ∧ |deriv (correctedPi w y) eta| ≤ correctedConstant * (1 + editSize d K) * UniformAngularReset.correctedAngular d w.coefficients (y, eta) ^ 2

theorem NavierStokes.CorrectedPressureBounds.corrected_bounds_of_small {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (hsmall : editSize d K ≤ 1) {y eta : ℝ} (hy : 0 ≤ y) (heta : |eta| ≤ 1) : |correctedPi w y eta| ≤ correctedConstant * UniformAngularReset.correctedAngular d w.coefficients (y, eta) ^ 2 ∧ |deriv (correctedPi w y) eta| ≤ correctedConstant * UniformAngularReset.correctedAngular d w.coefficients (y, eta) ^ 2

theorem NavierStokes.CorrectedPressureBounds.exists_editSize_small_threshold (K : ℝ) (hK : 0 ≤ K) : ∃ (lam0 : ℝ), 0 < lam0 ∧ ∀ (d : OutgoingTail.TailData), d.core.lam < lam0 → editSize d K ≤ 1

The smallness condition follows from an explicit threshold depending only on K.

theorem NavierStokes.CorrectedPressureBounds.releaseSquare_le_core_endpoint (d : OutgoingTail.TailData) {eta : ℝ} (heta : |eta| ≤ 1) : releaseSquare d ≤ 4 * Real.exp (6 / 5) * OutgoingTail.finalAngular d (d.core.endpoint, eta) ^ 2

theorem NavierStokes.CorrectedPressureBounds.pressureChange_core_endpoint_bounds {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (y : ℝ) {eta : ℝ} (heta : |eta| ≤ 1) : |pressureChange w y eta| ≤ 40 * Real.exp 5 * Real.exp (6 / 5) * editSize d K * OutgoingTail.finalAngular d (d.core.endpoint, eta) ^ 2 ∧ |deriv (pressureChange w y) eta| ≤ 48 * Real.exp 5 * Real.exp (6 / 5) * editSize d K * OutgoingTail.finalAngular d (d.core.endpoint, eta) ^ 2

theorem NavierStokes.CorrectedPressureBounds.correctedPi_eq_axisPressure_add {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (y eta : ℝ) : correctedPi w y eta = SchedulePressure.axisPressure d eta + 1 / 2 * ∫ (t : ℝ) in Set.Iic y, UniformAngularReset.correctedAngular d w.coefficients (t, eta) ^ 2

Canonical forward pressure with the unchanged whole-axis pressure datum.

theorem NavierStokes.CorrectedPressureBounds.pressureChange_hasDerivAt_y {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (y eta : ℝ) : HasDerivAt (fun (t : ℝ) => pressureChange w t eta) (1 / 2 * editDensity w (y, eta)) y

theorem NavierStokes.TailCone.initialLag_ge_half_lambda (d : OutgoingTail.TailData) : d.core.lam / 2 ≤ OutgoingTail.initialLag d

theorem NavierStokes.TailCone.release_rate_integral_bound_all (d : OutgoingTail.TailData) {t : ℝ} (_ht : 0 ≤ t) (ht' : t ≤ d.rampEnd) : OutgoingSchedule.primitive (OutgoingTail.releaseRate d) t ≤ 2

theorem NavierStokes.TailCone.releaseLag_lower_all (d : OutgoingTail.TailData) {t : ℝ} (ht : 0 ≤ t) (ht' : t ≤ d.rampEnd) : Real.exp (-2) * (d.core.lam / 2) ≤ OutgoingTail.releaseLag d t

theorem NavierStokes.TailCone.tailDebt_ge_coefficient (d : OutgoingTail.TailData) : OutgoingTail.tailCoefficient * d.h ≤ OutgoingTail.tailDebt d

theorem NavierStokes.TailCone.holdLag_lower (d : OutgoingTail.TailData) {t : ℝ} (ht : t ≤ OutgoingTail.decayHold d) : OutgoingTail.tailCoefficient * d.h ≤ OutgoingTail.holdLag d t

theorem NavierStokes.TailCone.tailLag_first_half (d : OutgoingTail.TailData) {t : ℝ} (ht : 0 ≤ t) (ht' : t ≤ 1 / 2) : OutgoingTail.tailLag d t = OutgoingTail.tailDebt d * Real.exp (-(1 - d.h) * t)

theorem NavierStokes.TailCone.tailLag_first_half_lower (d : OutgoingTail.TailData) {t : ℝ} (ht : 0 ≤ t) (ht' : t ≤ 1 / 2) : Real.exp (-1) * OutgoingTail.tailCoefficient * d.h ≤ OutgoingTail.tailLag d t

noncomputable def NavierStokes.TailCone.releaseLowerConstant : ℝ

Release lower constant, given by min (Real.exp (-2)) (Real.exp (-1) * tailCoefficient).

Equations

• NavierStokes.TailCone.releaseLowerConstant = min (Real.exp (-2)) (Real.exp (-1) * NavierStokes.OutgoingTail.tailCoefficient)

theorem NavierStokes.TailCone.releaseLowerConstant_pos : 0 < releaseLowerConstant

theorem NavierStokes.TailCone.normalizedLag_release_lower {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {y : ℝ} (hy : d.releaseStart ≤ y) (hy' : y ≤ d.releaseStart + d.rampEnd) : Real.exp (-2) * (d.core.lam / 2) ≤ ReleaseMoments.normalizedLag d w.coefficients eta y

theorem NavierStokes.TailCone.normalizedLag_lower {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {y : ℝ} (hy : d.releaseStart ≤ y) (hy' : y ≤ OutgoingTail.tailStart d + 1 / 2) : releaseLowerConstant * d.h ≤ ReleaseMoments.normalizedLag d w.coefficients eta y

Positivity of the actual angular-history lag through the first half tail unit.

theorem NavierStokes.TailCone.normalizedLag_pos {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {y : ℝ} (hy : d.releaseStart ≤ y) (hy' : y ≤ OutgoingTail.tailStart d + 1 / 2) : 0 < ReleaseMoments.normalizedLag d w.coefficients eta y

The designed suppression of the actual field

theorem NavierStokes.TailCone.finalAngular_release_formula (d : OutgoingTail.TailData) (eta : ℝ) {y : ℝ} (hy : d.releaseStart ≤ y) : OutgoingTail.finalAngular d (y, eta) = OutgoingTail.finalAngular d (d.releaseStart, eta) * Real.exp (TailEnergyBounds.releasePrimitive d (y - d.releaseStart) - (y - d.releaseStart) / 2) * (OutgoingTail.tailShape d (y - OutgoingTail.tailStart d) / (1 - d.rho))

theorem NavierStokes.TailCone.tailShape_ratio_le_two (d : OutgoingTail.TailData) (t : ℝ) : OutgoingTail.tailShape d t / (1 - d.rho) ≤ 2

theorem NavierStokes.TailCone.plateau_amplitude_suppression (d : OutgoingTail.TailData) : Real.exp (-d.longHold) = d.h ^ 4

theorem NavierStokes.TailCone.finalAngular_suppressed (d : OutgoingTail.TailData) (eta : ℝ) {y : ℝ} (hy : d.releaseStart + d.secondRampStart ≤ y) : OutgoingTail.finalAngular d (y, eta) ≤ 2 * OutgoingTail.finalAngular d (d.releaseStart, eta) * d.h ^ 4

theorem NavierStokes.TailCone.finalAngular_div_h_suppressed (d : OutgoingTail.TailData) (eta : ℝ) {y : ℝ} (hy : d.releaseStart + d.secondRampStart ≤ y) : OutgoingTail.finalAngular d (y, eta) / d.h ≤ 2 * OutgoingTail.finalAngular d (d.releaseStart, eta) * d.h ^ 3

theorem NavierStokes.TailCone.profileSlope_bounds (d : OutgoingTail.TailData) (y : ℝ) : -1 ≤ OutgoingTail.profileSlope d y ∧ OutgoingTail.profileSlope d y ≤ -(3 * d.h / 4)

noncomputable def NavierStokes.TailCone.releaseA (d : OutgoingTail.TailData) (y : ℝ) : ℝ

Release A, given by 2 - 2 * profileSlope d y.

Equations

• NavierStokes.TailCone.releaseA d y = 2 - 2 * NavierStokes.OutgoingTail.profileSlope d y

theorem NavierStokes.TailCone.releaseA_bounds (d : OutgoingTail.TailData) (y : ℝ) : 2 < releaseA d y ∧ releaseA d y ≤ 4

theorem NavierStokes.TailCone.releaseA_eq_derivative (d : OutgoingTail.TailData) (eta : ℝ) {y : ℝ} (hy : d.releaseStart ≤ y) : releaseA d y = 1 - 2 * deriv (fun (t : ℝ) => Real.log (OutgoingTail.finalAngular d (t, eta))) y

Future integrals on the uniform release

theorem NavierStokes.TailCone.finalAngular_release_decay (d : OutgoingTail.TailData) (eta : ℝ) {y t : ℝ} (hy : d.releaseStart ≤ y) (hyt : y ≤ t) : OutgoingTail.finalAngular d (t, eta) ≤ OutgoingTail.finalAngular d (y, eta) * Real.exp (-(1 / 2 + 3 * d.h / 4) * (t - y))

theorem NavierStokes.TailCone.weighted_square_release_decay (d : OutgoingTail.TailData) (eta : ℝ) {y t : ℝ} (hy : d.releaseStart ≤ y) (hyt : y ≤ t) : Real.exp (t - y) * OutgoingTail.finalAngular d (t, eta) ^ 2 ≤ OutgoingTail.finalAngular d (y, eta) ^ 2 * Real.exp (-(3 * d.h / 2) * (t - y))

theorem NavierStokes.TailCone.weighted_square_release_integrable (d : OutgoingTail.TailData) (eta : ℝ) {y : ℝ} (hy : d.releaseStart ≤ y) : MeasureTheory.IntegrableOn (fun (t : ℝ) => Real.exp (t - y) * OutgoingTail.finalAngular d (t, eta) ^ 2) (Set.Ioi y) MeasureTheory.volume

theorem NavierStokes.TailCone.weighted_square_release_integral_le (d : OutgoingTail.TailData) (eta : ℝ) {y : ℝ} (hy : d.releaseStart ≤ y) : d.h * ∫ (t : ℝ) in Set.Ioi y, Real.exp (t - y) * OutgoingTail.finalAngular d (t, eta) ^ 2 ≤ OutgoingTail.finalAngular d (y, eta) ^ 2

noncomputable def NavierStokes.TailCone.releaseFutureEnergy (d : OutgoingTail.TailData) (y : ℝ) : ℝ

Release future energy, given by ∫ t in Ioi y, Real.exp (t - y) * finalAngular d (t, 0) ^ 2.

Equations

• NavierStokes.TailCone.releaseFutureEnergy d y = ∫ (t : ℝ) in Set.Ioi y, Real.exp (t - y) * NavierStokes.OutgoingTail.finalAngular d (t, 0) ^ 2

noncomputable def NavierStokes.TailCone.releaseFutureMass (d : OutgoingTail.TailData) (y : ℝ) : ℝ

Release future mass, given by ∫ t in Ioi y, finalAngular d (t, 0) ^ 2.

Equations

• NavierStokes.TailCone.releaseFutureMass d y = ∫ (t : ℝ) in Set.Ioi y, NavierStokes.OutgoingTail.finalAngular d (t, 0) ^ 2

noncomputable def NavierStokes.TailCone.releaseNumerator (d : OutgoingTail.TailData) (eta y : ℝ) : ℝ

The backward-energy numerator in the uniform region. Its identification with the source primitive uses the actual zero total energy.

Equations

• NavierStokes.TailCone.releaseNumerator d eta y = 2 * eta * (d.h * NavierStokes.TailCone.releaseFutureEnergy d y - (1 / 2 + d.h) * NavierStokes.TailCone.releaseFutureMass d y)

noncomputable def NavierStokes.TailCone.numeratorConstant : ℝ

Numerator constant, given by 2 * (1 + FuturePressureBounds.envelopeConstant).

Equations

• NavierStokes.TailCone.numeratorConstant = 2 * (1 + NavierStokes.FuturePressureBounds.envelopeConstant)

theorem NavierStokes.TailCone.numeratorConstant_pos : 0 < numeratorConstant

theorem NavierStokes.TailCone.releaseNumerator_abs_le (d : OutgoingTail.TailData) {eta y : ℝ} (heta : |eta| ≤ 1) (hy : d.releaseStart ≤ y) : |releaseNumerator d eta y| ≤ numeratorConstant * OutgoingTail.finalAngular d (y, 0) ^ 2

Uniform smallness after dividing by the actual controller

theorem NavierStokes.TailCone.releaseAmplitude_le_pulse (d : OutgoingTail.TailData) (eta : ℝ) : OutgoingTail.finalAngular d (d.releaseStart, eta) ≤ OutgoingSchedule.pulseAmplitude d.core

theorem NavierStokes.TailCone.releaseAmplitude_small (d : OutgoingTail.TailData) (hwait : d.core.wait = 60 * Real.log (1 / d.core.lam)) (eta : ℝ) : OutgoingTail.finalAngular d (d.releaseStart, eta) ≤ d.core.P * Real.exp (Real.exp d.core.m + 12) * d.core.lam ^ 30

theorem NavierStokes.TailCone.finalAngular_le_releaseAmplitude (d : OutgoingTail.TailData) (eta : ℝ) {y : ℝ} (hy : d.releaseStart ≤ y) : OutgoingTail.finalAngular d (y, eta) ≤ OutgoingTail.finalAngular d (d.releaseStart, eta)

noncomputable def NavierStokes.TailCone.releaseVelocityRatio (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (eta y : ℝ) : ℝ

Release velocity ratio, given by releaseNumerator d eta y / (finalAngular d (y, 0) * ReleaseMoments.normalizedLag d c eta y).

Equations

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

theorem NavierStokes.TailCone.releaseVelocityRatio_abs_le {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {eta y : ℝ} (heta : |eta| ≤ 1) (hy : d.releaseStart ≤ y) (hy' : y ≤ OutgoingTail.tailStart d + 1 / 2) : |releaseVelocityRatio d w.coefficients eta y| ≤ numeratorConstant * OutgoingTail.finalAngular d (y, 0) / ReleaseMoments.normalizedLag d w.coefficients eta y

noncomputable def NavierStokes.TailCone.earlyRatioConstant : ℝ

Early ratio constant, given by 2 * numeratorConstant / Real.exp (-2).

Equations

• NavierStokes.TailCone.earlyRatioConstant = 2 * NavierStokes.TailCone.numeratorConstant / Real.exp (-2)

noncomputable def NavierStokes.TailCone.lateRatioConstant : ℝ

Late ratio constant, given by 2 * numeratorConstant / releaseLowerConstant.

Equations

• NavierStokes.TailCone.lateRatioConstant = 2 * NavierStokes.TailCone.numeratorConstant / NavierStokes.TailCone.releaseLowerConstant

theorem NavierStokes.TailCone.earlyRatioConstant_pos : 0 < earlyRatioConstant

theorem NavierStokes.TailCone.lateRatioConstant_pos : 0 < lateRatioConstant

theorem NavierStokes.TailCone.releaseVelocityRatio_early {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (hwait : d.core.wait = 60 * Real.log (1 / d.core.lam)) {eta y : ℝ} (heta : |eta| ≤ 1) (hy : d.releaseStart ≤ y) (hy' : y ≤ d.releaseStart + d.rampEnd) : |releaseVelocityRatio d w.coefficients eta y| ≤ earlyRatioConstant * (d.core.P * Real.exp (Real.exp d.core.m + 12)) * d.core.lam ^ 29

theorem NavierStokes.TailCone.releaseVelocityRatio_late {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (hwait : d.core.wait = 60 * Real.log (1 / d.core.lam)) {eta y : ℝ} (heta : |eta| ≤ 1) (hy : d.releaseStart + d.secondRampStart ≤ y) (hy' : y ≤ OutgoingTail.tailStart d + 1 / 2) : |releaseVelocityRatio d w.coefficients eta y| ≤ lateRatioConstant * (d.core.P * Real.exp (Real.exp d.core.m + 12)) * d.core.lam ^ 29

noncomputable def NavierStokes.TailCone.releaseConeConstant (P m : ℝ) : ℝ

Release cone constant, given by (earlyRatioConstant + lateRatioConstant) * (P * Real.exp (Real.exp m + 12)).

Equations

• NavierStokes.TailCone.releaseConeConstant P m = (NavierStokes.TailCone.earlyRatioConstant + NavierStokes.TailCone.lateRatioConstant) * (P * Real.exp (Real.exp m + 12))

theorem NavierStokes.TailCone.releaseConeConstant_pos {P m : ℝ} (hP : 0 < P) : 0 < releaseConeConstant P m

theorem NavierStokes.TailCone.releaseVelocityRatio_uniform {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (hwait : d.core.wait = 60 * Real.log (1 / d.core.lam)) {eta y : ℝ} (heta : |eta| ≤ 1) (hy : d.releaseStart ≤ y) (hy' : y ≤ OutgoingTail.tailStart d + 1 / 2) : |releaseVelocityRatio d w.coefficients eta y| ≤ releaseConeConstant d.core.P d.core.m * d.core.lam ^ 29

Actual slopes and the finite stress cone

theorem NavierStokes.TailCone.corrected_release_eventuallyEq (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (eta : ℝ) {y : ℝ} (hy : d.releaseStart ≤ y) : (fun (t : ℝ) => UniformAngularReset.correctedAngular d c (t, eta)) =ᶠ[nhds y] fun (t : ℝ) => OutgoingTail.finalAngular d (t, eta)

theorem NavierStokes.TailCone.corrected_releaseA (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (eta : ℝ) {y : ℝ} (hy : d.releaseStart ≤ y) : 1 - 2 * deriv (fun (t : ℝ) => Real.log (UniformAngularReset.correctedAngular d c (t, eta))) y = releaseA d y

theorem NavierStokes.TailCone.corrected_bs_zero (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (Amp : ℝ → ℝ) (eta : ℝ) {y : ℝ} (hy : d.core.endpoint < y) : 2 * deriv (fun (t : ℝ) => OutgoingSchedule.axial d.core Amp (t, eta)) y / UniformAngularReset.correctedAngular d c (y, eta) = 0

theorem NavierStokes.TailCone.cone_of_zero_bs {a r p : ℝ} (ha : 2 < a) (ha' : a ≤ 4) (hr : |r| ≤ 1 / 2) (hp : 16 < p) : 2 < p ∧ 2 < a ∧ a < ConeAlgebra.coneBound p (p * r)

noncomputable def NavierStokes.TailCone.releaseP1 (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (XR eta y : ℝ) : ℝ

Release P1, given by XR * Real.exp y * ReleaseMoments.normalizedLag d c eta y / CoordinateAlgebra.L d.h eta.

Equations

• NavierStokes.TailCone.releaseP1 d c XR eta y = XR * Real.exp y * NavierStokes.ReleaseMoments.normalizedLag d c eta y / NavierStokes.CoordinateAlgebra.L d.h eta

noncomputable def NavierStokes.TailCone.releaseRadiusThreshold (d : OutgoingTail.TailData) : ℝ

Release radius threshold, given by 16 / (Real.exp d.releaseStart * (releaseLowerConstant * d.h)).

Equations

• NavierStokes.TailCone.releaseRadiusThreshold d = 16 / (Real.exp d.releaseStart * (NavierStokes.TailCone.releaseLowerConstant * d.h))

theorem NavierStokes.TailCone.releaseRadiusThreshold_pos (d : OutgoingTail.TailData) : 0 < releaseRadiusThreshold d

theorem NavierStokes.TailCone.releaseP1_large {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {XR eta y : ℝ} (hXR : releaseRadiusThreshold d < XR) (heta : eta ^ 2 ≤ 1) (hy : d.releaseStart ≤ y) (hy' : y ≤ OutgoingTail.tailStart d + 1 / 2) : 16 < releaseP1 d w.coefficients XR eta y

theorem NavierStokes.TailCone.release_true_cone {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (hwait : d.core.wait = 60 * Real.log (1 / d.core.lam)) (hsmall : releaseConeConstant d.core.P d.core.m * d.core.lam ^ 29 ≤ 1 / 2) {XR eta y : ℝ} (hXR : releaseRadiusThreshold d < XR) (heta : |eta| ≤ 1) (hy : d.releaseStart ≤ y) (hy' : y ≤ OutgoingTail.tailStart d + 1 / 2) : 2 < releaseP1 d w.coefficients XR eta y ∧ 2 < releaseA d y ∧ releaseA d y < ConeAlgebra.coneBound (releaseP1 d w.coefficients XR eta y) (releaseP1 d w.coefficients XR eta y * releaseVelocityRatio d w.coefficients eta y)

theorem NavierStokes.TailCone.exists_release_cone_threshold (P m : ℝ) (hP : 0 < P) : ∃ (lam0 : ℝ), 0 < lam0 ∧ ∀ (d : OutgoingTail.TailData), d.core.P = P → d.core.m = m → d.core.lam < lam0 → releaseConeConstant d.core.P d.core.m * d.core.lam ^ 29 < 1 / 2

Identification with the actual global histories

theorem NavierStokes.TailCone.actualI_eq_releaseHistory {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {y : ℝ} (hy : 0 ≤ y) : OutgoingHistories.I w (y, eta) = ReleaseMoments.history d w.coefficients eta y

theorem NavierStokes.TailCone.actualI_eta_zero {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {y : ℝ} (hy : d.releaseStart ≤ y) : OutgoingHistories.dEta (OutgoingHistories.I w) (y, eta) = 0

theorem NavierStokes.TailCone.actualQs_eq_normalizedLag {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (eta : ℝ) {y : ℝ} (hy : d.releaseStart ≤ y) : OutgoingHistories.Qs w Amp (y, eta) = ReleaseMoments.normalizedLag d w.coefficients eta y

theorem NavierStokes.TailCone.actual_energyWeight_eq {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (eta t : ℝ) : Real.exp t * (OutgoingHistories.U d Amp (t, eta) ^ 2 - OutgoingHistories.E w (t, eta) ^ 2 / 2) = CorrectedPulseAmplitude.energyIntegrand d w.coefficients (Amp eta) eta t

theorem NavierStokes.TailCone.actualS_backward {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (eta : ℝ) {y : ℝ} (hy : d.core.endpoint ≤ y) (hz : CorrectedPulseAmplitude.totalEnergy d w.coefficients (Amp eta) eta = 0) : OutgoingHistories.S w Amp (y, eta) = 1 / 2 * ∫ (t : ℝ) in Set.Ioi y, Real.exp t * UniformAngularReset.correctedAngular d w.coefficients (t, eta) ^ 2

Zero actual total energy fixes the future energy term, including the reset.

theorem NavierStokes.TailCone.actualS_uniform {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (eta : ℝ) {y : ℝ} (hy : d.releaseStart ≤ y) (hz : CorrectedPulseAmplitude.totalEnergy d w.coefficients (Amp eta) eta = 0) : OutgoingHistories.S w Amp (y, eta) = Real.exp y / 2 * releaseFutureEnergy d y

theorem NavierStokes.TailCone.actualS_eta_zero {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (eta : ℝ) {y : ℝ} (hy : d.releaseStart ≤ y) (hz : ∀ᶠ (q : ℝ) in nhds eta, CorrectedPulseAmplitude.totalEnergy d w.coefficients (Amp q) q = 0) : OutgoingHistories.dEta (OutgoingHistories.S w Amp) (y, eta) = 0

theorem NavierStokes.TailCone.actualPi_eq_correctedPi {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (y eta : ℝ) : OutgoingHistories.Pi w (y, eta) = CorrectedPressureBounds.correctedPi w y eta

theorem NavierStokes.TailCone.actualPi_uniform {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {y : ℝ} (hy : d.releaseStart ≤ y) : OutgoingHistories.Pi w (y, eta) = -(1 / 2) * releaseFutureMass d y

theorem NavierStokes.TailCone.actualPi_eta_zero {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {y : ℝ} (hy : d.releaseStart ≤ y) : OutgoingHistories.dEta (OutgoingHistories.Pi w) (y, eta) = 0

theorem NavierStokes.TailCone.actualNs_eq_releaseNumerator {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (eta : ℝ) {y : ℝ} (hy : d.releaseStart ≤ y) (hz : ∀ᶠ (q : ℝ) in nhds eta, CorrectedPulseAmplitude.totalEnergy d w.coefficients (Amp q) q = 0) : OutgoingHistories.Ns w Amp (y, eta) = releaseNumerator d eta y

theorem NavierStokes.TailCone.amplitude_energy_zero_germ {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) (hneg : CorrectedPulseAmplitude.constantTerm d w.coefficients eta < -(1 / 5)) : ∀ᶠ (q : ℝ) in nhds eta, CorrectedPulseAmplitude.totalEnergy d w.coefficients (CorrectedPulseAmplitude.amplitude d w.coefficients q) q = 0

theorem NavierStokes.TailCone.actualRatio_eq_releaseVelocityRatio {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (eta : ℝ) {y : ℝ} (hy : d.releaseStart ≤ y) (hz : ∀ᶠ (q : ℝ) in nhds eta, CorrectedPulseAmplitude.totalEnergy d w.coefficients (Amp q) q = 0) : OutgoingHistories.Ns w Amp (y, eta) / (OutgoingHistories.E w (y, eta) * OutgoingHistories.Qs w Amp (y, eta)) = releaseVelocityRatio d w.coefficients eta y

theorem NavierStokes.TailCone.actual_release_cone {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (hwait : d.core.wait = 60 * Real.log (1 / d.core.lam)) (hsmall : releaseConeConstant d.core.P d.core.m * d.core.lam ^ 29 ≤ 1 / 2) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) {XR eta y : ℝ} (hXR : releaseRadiusThreshold d < XR) (heta : |eta| ≤ 1) (hy : d.releaseStart ≤ y) (hy' : y ≤ OutgoingTail.tailStart d + 1 / 2) (hz : ∀ᶠ (q : ℝ) in nhds eta, CorrectedPulseAmplitude.totalEnergy d w.coefficients (Amp q) q = 0) : 0 < OutgoingHistories.Qs w Amp (y, eta) ∧ 2 < releaseA d y ∧ 2 < XR * Real.exp y * OutgoingHistories.Qs w Amp (y, eta) / CoordinateAlgebra.L d.h eta ∧ releaseA d y < ConeAlgebra.coneBound (XR * Real.exp y * OutgoingHistories.Qs w Amp (y, eta) / CoordinateAlgebra.L d.h eta) (XR * Real.exp y * OutgoingHistories.Qs w Amp (y, eta) / CoordinateAlgebra.L d.h eta * (OutgoingHistories.Ns w Amp (y, eta) / (OutgoingHistories.E w (y, eta) * OutgoingHistories.Qs w Amp (y, eta))))

Actual logarithmic derivatives through flattening and reset

noncomputable def NavierStokes.TailCone.resetRelative {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta y : ℝ) : ℝ

Reset relative, given by relative (w.coefficients eta) (y - correctionCenter d).

Equations

• NavierStokes.TailCone.resetRelative w eta y = NavierStokes.AngularMomentReset.relative (w.coefficients eta) (y - NavierStokes.UniformAngularReset.correctionCenter d)

noncomputable def NavierStokes.TailCone.resetRadialDerivative {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta y : ℝ) : ℝ

Reset radial derivative, given by deriv (relative (w.coefficients eta)) (y - correctionCenter d).

Equations

• NavierStokes.TailCone.resetRadialDerivative w eta y = deriv (NavierStokes.AngularMomentReset.relative (w.coefficients eta)) (y - NavierStokes.UniformAngularReset.correctionCenter d)

noncomputable def NavierStokes.TailCone.resetEtaDerivative {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta y : ℝ) : ℝ

Reset eta derivative, given by relative (deriv w.coefficients eta) (y - correctionCenter d).

Equations

• NavierStokes.TailCone.resetEtaDerivative w eta y = NavierStokes.AngularMomentReset.relative (deriv w.coefficients eta) (y - NavierStokes.UniformAngularReset.correctionCenter d)

noncomputable def NavierStokes.TailCone.correctedFlatSlope {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta y : ℝ) : ℝ

Corrected flat slope, given by `flatteningSlope d y eta + resetRadialDerivative w eta y / (1

• resetRelative w eta y)`.

Equations

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

noncomputable def NavierStokes.TailCone.correctedEtaSlope {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta y : ℝ) : ℝ

Corrected eta slope, given by etaRate d eta y + resetEtaDerivative w eta y / (1 + resetRelative w eta y).

Equations

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

theorem NavierStokes.TailCone.resetFactor_ge_half {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta y : ℝ) : 1 / 2 ≤ 1 + resetRelative w eta y

theorem NavierStokes.TailCone.correctedFlat_hasDerivAt {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {y : ℝ} (hy : d.core.endpoint ≤ y) (hy' : y < d.releaseStart) : HasDerivAt (fun (t : ℝ) => OutgoingHistories.E w (t, eta)) (OutgoingHistories.E w (y, eta) * (correctedFlatSlope w eta y - 1 / 2)) y

theorem NavierStokes.TailCone.correctedEta_hasDerivAt {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta y : ℝ) : HasDerivAt (fun (q : ℝ) => OutgoingHistories.E w (y, q)) (OutgoingHistories.E w (y, eta) * correctedEtaSlope w eta y) eta

theorem NavierStokes.TailCone.correctedFlat_dY_H {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {y : ℝ} (hy : d.core.endpoint ≤ y) (hy' : y < d.releaseStart) : OutgoingHistories.dY (OutgoingHistories.H w) (y, eta) = OutgoingHistories.H w (y, eta) * correctedFlatSlope w eta y

theorem NavierStokes.TailCone.corrected_dEta_H {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta y : ℝ) : OutgoingHistories.dEta (OutgoingHistories.H w) (y, eta) = OutgoingHistories.H w (y, eta) * correctedEtaSlope w eta y

theorem NavierStokes.TailCone.correctedFlat_Sq {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (eta : ℝ) {y : ℝ} (hy : d.core.endpoint ≤ y) (hy' : y < d.releaseStart) : OutgoingHistories.Sq w Amp (y, eta) = -correctedFlatSlope w eta y - d.h - StressAlgebra.axialExponent d.h * eta * correctedEtaSlope w eta y

noncomputable def NavierStokes.TailCone.resetJetConstant : ℝ

Reset jet constant, given by Classical.choose relative_first_jet_bound.

Equations

• NavierStokes.TailCone.resetJetConstant = Classical.choose NavierStokes.AngularMomentReset.relative_first_jet_bound

theorem NavierStokes.TailCone.resetJetConstant_pos : 0 < resetJetConstant

theorem NavierStokes.TailCone.relative_radial_bound (c : AngularMomentReset.Coeff) (y : ℝ) : |deriv (AngularMomentReset.relative c) y| ≤ resetJetConstant * ‖c‖

noncomputable def NavierStokes.TailCone.resetSourceError (d : OutgoingTail.TailData) (K : ℝ) : ℝ

Reset source error, given by (2 * resetJetConstant + 2) * (K * d.core.lam ^ (28 : ℕ)).

Equations

• NavierStokes.TailCone.resetSourceError d K = (2 * NavierStokes.TailCone.resetJetConstant + 2) * (K * d.core.lam ^ 28)

theorem NavierStokes.TailCone.reset_radial_ratio_bound {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta y : ℝ) : |resetRadialDerivative w eta y / (1 + resetRelative w eta y)| ≤ 2 * resetJetConstant * (K * d.core.lam ^ 28)

theorem NavierStokes.TailCone.reset_eta_ratio_bound {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta y : ℝ) : |resetEtaDerivative w eta y / (1 + resetRelative w eta y)| ≤ 4 * (K * d.core.lam ^ 28)

theorem NavierStokes.TailCone.eta_times_etaRate_nonpos (d : OutgoingTail.TailData) (eta y : ℝ) : eta * UniformAngularReset.etaRate d eta y ≤ 0

theorem NavierStokes.TailCone.correctedFlatSlope_bounds {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta y : ℝ) (heta : eta ^ 2 ≤ 1) : -d.core.lam - 1 / 10 - resetSourceError d K ≤ correctedFlatSlope w eta y ∧ correctedFlatSlope w eta y ≤ -d.core.lam + resetSourceError d K

theorem NavierStokes.TailCone.correctedFlat_source_lower {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (eta : ℝ) (heta : |eta| ≤ 1) {y : ℝ} (hy : d.core.endpoint ≤ y) (hy' : y < d.releaseStart) : d.core.lam / 2 - resetSourceError d K ≤ OutgoingHistories.Sq w Amp (y, eta)

theorem NavierStokes.TailCone.correctedFlat_geometry {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (hsmall : resetSourceError d K ≤ d.core.lam / 4) (eta y : ℝ) (heta : eta ^ 2 ≤ 1) : 2 < 2 - 2 * correctedFlatSlope w eta y ∧ 2 - 2 * correctedFlatSlope w eta y ≤ 4 ∧ 1 + correctedFlatSlope w eta y ≤ 1

theorem NavierStokes.TailCone.ode_constant_barrier {q a b : ℝ → ℝ} (hq : Continuous q) (ha : Continuous a) {lo hi B : ℝ} (hlh : lo ≤ hi) (hinit : B ≤ q lo) (hODE : ∀ t ∈ Set.Ioo lo hi, HasDerivAt q (b t - a t * q t) t) (hsource : ∀ t ∈ Set.Ioo lo hi, a t * B ≤ b t) : B ≤ q hi

theorem NavierStokes.TailCone.flatten_Qs_lower_of_endpoint {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (hsmall : resetSourceError d K ≤ d.core.lam / 4) (eta : ℝ) (heta : |eta| ≤ 1) (hinit : d.core.lam / 4 ≤ OutgoingHistories.Qs w Amp (d.core.endpoint, eta)) {y : ℝ} (hy : d.core.endpoint ≤ y) (hy' : y ≤ d.releaseStart) : d.core.lam / 4 ≤ OutgoingHistories.Qs w Amp (y, eta)

theorem NavierStokes.TailCone.corrected_flatten_Qs_lower {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (hK : 0 < K) (hwait : d.core.wait = 60 * Real.log (1 / d.core.lam)) (hsmall : d.core.lam ≤ 1 / 120) (hscale : CorrectedPulseAmplitude.combinedScale d K ≤ 1 / 1000) (hpulse : PulseCone.sourceConstant d.core.P d.core.m * d.core.lam ^ 29 ≤ 1 / 8) (hh1 : d.h ≤ 1 / 100) (hhT : d.h ≤ Real.exp (-(d.core.holdStart + 3 / 5)) / 8) (hreset : resetSourceError d K ≤ d.core.lam / 4) (eta : ℝ) (heta : |eta| ≤ 1) {y : ℝ} (hy : d.core.endpoint ≤ y) (hy' : y ≤ d.releaseStart) : d.core.lam / 4 ≤ OutgoingHistories.Qs w (CorrectedPulseAmplitude.amplitude d w.coefficients) (y, eta)

Energy and its parameter derivative on the finite post-pulse interval

theorem NavierStokes.TailCone.corrected_density_prefix_le {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) (heta : eta ^ 2 ≤ 1) {y : ℝ} (hy : d.core.endpoint ≤ y) (hy' : y ≤ d.releaseStart) : Real.exp y * OutgoingHistories.E w (y, eta) ^ 2 ≤ 9 / 4 * TailEnergyBounds.energyDensity d eta d.core.endpoint

theorem NavierStokes.TailCone.corrected_square_prefix_le {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) (heta : eta ^ 2 ≤ 1) {y : ℝ} (hy : d.core.endpoint ≤ y) (hy' : y ≤ d.releaseStart) : OutgoingHistories.E w (y, eta) ^ 2 ≤ 9 / 4 * OutgoingTail.finalAngular d (d.core.endpoint, eta) ^ 2

theorem NavierStokes.TailCone.correctedEtaSlope_abs_le {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (hsmall : K * d.core.lam ^ 28 ≤ 1) (eta y : ℝ) : |correctedEtaSlope w eta y| ≤ 5

theorem NavierStokes.TailCone.actualS_endpoint {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (eta : ℝ) (hz : CorrectedPulseAmplitude.totalEnergy d w.coefficients (Amp eta) eta = 0) : OutgoingHistories.S w Amp (d.core.endpoint, eta) = 1 / 2 * (TailEnergyBounds.postPulseEnergy d eta + ResetEnergyBounds.resetEnergy d w.coefficients eta)

theorem NavierStokes.TailCone.actualS_eta_endpoint {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (eta : ℝ) (hz : ∀ᶠ (q : ℝ) in nhds eta, CorrectedPulseAmplitude.totalEnergy d w.coefficients (Amp q) q = 0) : OutgoingHistories.dEta (OutgoingHistories.S w Amp) (d.core.endpoint, eta) = 1 / 2 * (deriv (TailEnergyBounds.postPulseEnergy d) eta + deriv (ResetEnergyBounds.resetEnergy d w.coefficients) eta)

theorem NavierStokes.TailCone.actualS_after_hasDerivAt {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (eta : ℝ) {y : ℝ} (hy : d.core.endpoint ≤ y) : HasDerivAt (fun (t : ℝ) => OutgoingHistories.S w Amp (t, eta)) (-(Real.exp y * OutgoingHistories.E w (y, eta) ^ 2) / 2) y

theorem NavierStokes.TailCone.actualS_eta_after_hasDerivAt {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (eta : ℝ) {y : ℝ} (hy : d.core.endpoint ≤ y) : HasDerivAt (fun (t : ℝ) => OutgoingHistories.dEta (OutgoingHistories.S w Amp) (t, eta)) (-(Real.exp y * OutgoingHistories.E w (y, eta) ^ 2) * correctedEtaSlope w eta y) y

theorem NavierStokes.TailCone.abs_increment_le {f f' : ℝ → ℝ} {a b C : ℝ} (hab : a ≤ b) (hf : ∀ t ∈ Set.Icc a b, HasDerivAt f (f' t) t) (hb : ∀ t ∈ Set.Icc a b, |f' t| ≤ C) : |f b - f a| ≤ C * (b - a)

noncomputable def NavierStokes.TailCone.finiteEnergyBudget (d : OutgoingTail.TailData) : ℝ

Finite energy budget, given by `flattenLength + releaseConstant + 40 + 20 * (d.releaseStart

• d.core.endpoint)`.

Equations

• NavierStokes.TailCone.finiteEnergyBudget d = NavierStokes.OutgoingTail.flattenLength + NavierStokes.TailEnergyBounds.releaseConstant + 40 + 20 * (d.releaseStart - d.core.endpoint)

theorem NavierStokes.TailCone.finiteEnergyBudget_pos (d : OutgoingTail.TailData) : 0 < finiteEnergyBudget d

theorem NavierStokes.TailCone.actualS_finite_bounds {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (hsmall : K * d.core.lam ^ 28 ≤ 1) (eta : ℝ) (heta : eta ^ 2 ≤ 1) (hz : ∀ᶠ (q : ℝ) in nhds eta, CorrectedPulseAmplitude.totalEnergy d w.coefficients (Amp q) q = 0) {y : ℝ} (hy : d.core.endpoint ≤ y) (hy' : y ≤ d.releaseStart) : |OutgoingHistories.S w Amp (y, eta)| ≤ finiteEnergyBudget d * TailEnergyBounds.energyDensity d eta d.core.endpoint ∧ |OutgoingHistories.dEta (OutgoingHistories.S w Amp) (y, eta)| ≤ finiteEnergyBudget d * TailEnergyBounds.energyDensity d eta d.core.endpoint

noncomputable def NavierStokes.TailCone.finiteNumeratorBudget (d : OutgoingTail.TailData) : ℝ

Finite numerator budget, given by 5 * finiteEnergyBudget d + 12 * CorrectedPressureBounds.correctedConstant.

Equations

• NavierStokes.TailCone.finiteNumeratorBudget d = 5 * NavierStokes.TailCone.finiteEnergyBudget d + 12 * NavierStokes.CorrectedPressureBounds.correctedConstant

theorem NavierStokes.TailCone.finiteNumeratorBudget_pos (d : OutgoingTail.TailData) : 0 < finiteNumeratorBudget d

theorem NavierStokes.TailCone.actualNs_finite_bound {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (hsmall : K * d.core.lam ^ 28 ≤ 1) (eta : ℝ) (heta : |eta| ≤ 1) (hz : ∀ᶠ (q : ℝ) in nhds eta, CorrectedPulseAmplitude.totalEnergy d w.coefficients (Amp q) q = 0) {y : ℝ} (hy : d.core.endpoint ≤ y) (hy' : y ≤ d.releaseStart) : |OutgoingHistories.Ns w Amp (y, eta)| ≤ finiteNumeratorBudget d * OutgoingTail.finalAngular d (d.core.endpoint, eta) ^ 2

theorem NavierStokes.TailCone.lambda_log_bound (d : OutgoingTail.TailData) : d.core.lam * Real.log (1 / d.core.lam) ≤ 1

theorem NavierStokes.TailCone.lambda_finite_length_bound (d : OutgoingTail.TailData) : d.core.lam * (d.releaseStart - d.core.endpoint) ≤ OutgoingTail.flattenLength + 30

noncomputable def NavierStokes.TailCone.finiteNumeratorConstant : ℝ

Finite numerator constant, given by 5 * (flattenLength + releaseConstant + 40 + 20 * (flattenLength + 30)) + 12 * CorrectedPressureBounds.correctedConstant.

Equations

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

theorem NavierStokes.TailCone.finiteNumeratorConstant_pos : 0 < finiteNumeratorConstant

theorem NavierStokes.TailCone.finiteNumeratorBudget_bound (d : OutgoingTail.TailData) : d.core.lam * finiteNumeratorBudget d ≤ finiteNumeratorConstant

A lower amplitude bound up to release

The finite waiting interval loses only eighteen powers of lam, whereas the earlier scheduled wait has already supplied thirty powers.

theorem NavierStokes.TailCone.flattenFactor_ge_half (d : OutgoingTail.TailData) (eta y : ℝ) : 1 / 2 ≤ OutgoingTail.flattenFactor d (y, eta)

noncomputable def NavierStokes.TailCone.finiteAmplitudeConstant : ℝ

Finite amplitude constant, given by Real.exp (-(3 / 5 : ℝ) * flattenLength) / 4.

Equations

• NavierStokes.TailCone.finiteAmplitudeConstant = Real.exp (-(3 / 5) * NavierStokes.OutgoingTail.flattenLength) / 4

theorem NavierStokes.TailCone.finiteAmplitudeConstant_pos : 0 < finiteAmplitudeConstant

theorem NavierStokes.TailCone.corrected_amplitude_finite_lower {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {y : ℝ} (hy : d.core.endpoint ≤ y) (hy' : y ≤ d.releaseStart) : finiteAmplitudeConstant * OutgoingTail.finalAngular d (d.core.endpoint, eta) * d.core.lam ^ 18 ≤ OutgoingHistories.E w (y, eta)

theorem NavierStokes.TailCone.endpointAmplitude_le_pulse (d : OutgoingTail.TailData) (eta : ℝ) : OutgoingTail.finalAngular d (d.core.endpoint, eta) ≤ OutgoingSchedule.pulseAmplitude d.core

noncomputable def NavierStokes.TailCone.finiteConeConstant (P m : ℝ) : ℝ

Finite cone constant, given by `(4 * finiteNumeratorConstant / finiteAmplitudeConstant) * (P

• Real.exp (Real.exp m + 12))`.

Equations

• NavierStokes.TailCone.finiteConeConstant P m = 4 * NavierStokes.TailCone.finiteNumeratorConstant / NavierStokes.TailCone.finiteAmplitudeConstant * (P * Real.exp (Real.exp m + 12))

theorem NavierStokes.TailCone.finiteConeConstant_pos {P : ℝ} (hP : 0 < P) (m : ℝ) : 0 < finiteConeConstant P m

theorem NavierStokes.TailCone.actual_finite_ratio_bound {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (hwait : d.core.wait = 60 * Real.log (1 / d.core.lam)) (hsmall : K * d.core.lam ^ 28 ≤ 1) (eta : ℝ) (heta : |eta| ≤ 1) (hz : ∀ᶠ (q : ℝ) in nhds eta, CorrectedPulseAmplitude.totalEnergy d w.coefficients (Amp q) q = 0) {y : ℝ} (hy : d.core.endpoint ≤ y) (hy' : y ≤ d.releaseStart) (hQ : d.core.lam / 4 ≤ OutgoingHistories.Qs w Amp (y, eta)) : |OutgoingHistories.Ns w Amp (y, eta) / (OutgoingHistories.E w (y, eta) * OutgoingHistories.Qs w Amp (y, eta))| ≤ finiteConeConstant d.core.P d.core.m * d.core.lam ^ 10

Cone quantities of the actual corrected profile

noncomputable def NavierStokes.TailCone.actualA {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (y eta : ℝ) : ℝ

Actual A, given by 1 - 2 * deriv (fun t => Real.log (OutgoingHistories.E w (t, eta))) y.

Equations

• NavierStokes.TailCone.actualA w y eta = 1 - 2 * deriv (fun (t : ℝ) => Real.log (NavierStokes.OutgoingHistories.E w (t, eta))) y

noncomputable def NavierStokes.TailCone.actualBs {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (y eta : ℝ) : ℝ

Actual bs, given by 2 * deriv (fun t => OutgoingHistories.U d Amp (t, eta)) y / OutgoingHistories.E w (y, eta).

Equations

• NavierStokes.TailCone.actualBs w Amp y eta = 2 * deriv (fun (t : ℝ) => NavierStokes.OutgoingHistories.U d Amp (t, eta)) y / NavierStokes.OutgoingHistories.E w (y, eta)

theorem NavierStokes.TailCone.actualA_finite {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {y : ℝ} (hy : d.core.endpoint ≤ y) (hy' : y < d.releaseStart) : actualA w y eta = 2 - 2 * correctedFlatSlope w eta y

theorem NavierStokes.TailCone.actualA_release {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {y : ℝ} (hy : d.releaseStart ≤ y) : actualA w y eta = releaseA d y

theorem NavierStokes.TailCone.actualBs_zero {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (eta : ℝ) {y : ℝ} (hy : d.core.endpoint ≤ y) : actualBs w Amp y eta = 0

theorem NavierStokes.TailCone.actualP2_eq {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (XR eta y : ℝ) (heta : eta ^ 2 ≤ 1) (hQ : 0 < OutgoingHistories.Qs w Amp (y, eta)) : OutgoingHistories.p2 XR w Amp (y, eta) = OutgoingHistories.p1 XR w Amp (y, eta) * (OutgoingHistories.Ns w Amp (y, eta) / (OutgoingHistories.E w (y, eta) * OutgoingHistories.Qs w Amp (y, eta)))

noncomputable def NavierStokes.TailCone.finiteRadiusThreshold (d : OutgoingTail.TailData) : ℝ

Finite radius threshold, given by 16 / (Real.exp d.core.endpoint * (d.core.lam / 4)).

Equations

• NavierStokes.TailCone.finiteRadiusThreshold d = 16 / (Real.exp d.core.endpoint * (d.core.lam / 4))

theorem NavierStokes.TailCone.finiteRadiusThreshold_pos (d : OutgoingTail.TailData) : 0 < finiteRadiusThreshold d

theorem NavierStokes.TailCone.actualP1_finite_large {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) {XR eta y : ℝ} (hXR : finiteRadiusThreshold d < XR) (heta : eta ^ 2 ≤ 1) (hy : d.core.endpoint ≤ y) (hQ : d.core.lam / 4 ≤ OutgoingHistories.Qs w Amp (y, eta)) : 16 < OutgoingHistories.p1 XR w Amp (y, eta)

theorem NavierStokes.TailCone.corrected_amplitude_energy_zero_germ {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (hK : 0 < K) (hwait : d.core.wait = 60 * Real.log (1 / d.core.lam)) (hsmall : d.core.lam ≤ 1 / 120) (hscale : CorrectedPulseAmplitude.combinedScale d K ≤ 1 / 1000) (eta : ℝ) (heta : eta ^ 2 ≤ 1) : ∀ᶠ (q : ℝ) in nhds eta, CorrectedPulseAmplitude.totalEnergy d w.coefficients (CorrectedPulseAmplitude.amplitude d w.coefficients q) q = 0

theorem NavierStokes.TailCone.reset_scale_le_one {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (hreset : resetSourceError d K ≤ d.core.lam / 4) : K * d.core.lam ^ 28 ≤ 1

noncomputable def NavierStokes.TailCone.tailRadiusThreshold (d : OutgoingTail.TailData) : ℝ

Tail radius threshold, given by max (finiteRadiusThreshold d) (releaseRadiusThreshold d).

Equations

• NavierStokes.TailCone.tailRadiusThreshold d = max (NavierStokes.TailCone.finiteRadiusThreshold d) (NavierStokes.TailCone.releaseRadiusThreshold d)

theorem NavierStokes.TailCone.tailRadiusThreshold_pos (d : OutgoingTail.TailData) : 0 < tailRadiusThreshold d

theorem NavierStokes.TailCone.corrected_tail_cone {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (hK : 0 < K) (hwait : d.core.wait = 60 * Real.log (1 / d.core.lam)) (hsmall : d.core.lam ≤ 1 / 120) (hscale : CorrectedPulseAmplitude.combinedScale d K ≤ 1 / 1000) (hpulse : PulseCone.sourceConstant d.core.P d.core.m * d.core.lam ^ 29 ≤ 1 / 8) (hh1 : d.h ≤ 1 / 100) (hhT : d.h ≤ Real.exp (-(d.core.holdStart + 3 / 5)) / 8) (hreset : resetSourceError d K ≤ d.core.lam / 4) (hfinite : finiteConeConstant d.core.P d.core.m * d.core.lam ^ 10 ≤ 1 / 2) (hrelease : releaseConeConstant d.core.P d.core.m * d.core.lam ^ 29 ≤ 1 / 2) {XR eta y : ℝ} (hXR : tailRadiusThreshold d < XR) (heta : |eta| ≤ 1) (hy : d.core.endpoint ≤ y) (hy' : y ≤ OutgoingTail.tailStart d + 1 / 2) : 0 < OutgoingHistories.Qs w (CorrectedPulseAmplitude.amplitude d w.coefficients) (y, eta) ∧ actualBs w (CorrectedPulseAmplitude.amplitude d w.coefficients) y eta = 0 ∧ 2 < actualA w y eta ∧ actualA w y eta ≤ 4 ∧ 2 < OutgoingHistories.p1 XR w (CorrectedPulseAmplitude.amplitude d w.coefficients) (y, eta) ∧ actualA w y eta < ConeAlgebra.coneBound (OutgoingHistories.p1 XR w (CorrectedPulseAmplitude.amplitude d w.coefficients) (y, eta)) (OutgoingHistories.p2 XR w (CorrectedPulseAmplitude.amplitude d w.coefficients) (y, eta))

All quantities are those of the corrected profile and its actual integral histories. The scalar smallness conditions are arranged by the thresholds below.

Simultaneous parameter choice, uniform in the terminal parameter

theorem NavierStokes.TailCone.lambda_power_le_self (d : OutgoingTail.TailData) (n : ℕ) : d.core.lam ^ (n + 1) ≤ d.core.lam

theorem NavierStokes.TailCone.exists_finite_cone_threshold (P m : ℝ) (hP : 0 < P) : ∃ (lam0 : ℝ), 0 < lam0 ∧ ∀ (d : OutgoingTail.TailData), d.core.P = P → d.core.m = m → d.core.lam < lam0 → finiteConeConstant d.core.P d.core.m * d.core.lam ^ 10 < 1 / 2

theorem NavierStokes.TailCone.exists_reset_source_threshold (K : ℝ) (hK : 0 < K) : ∃ (lam0 : ℝ), 0 < lam0 ∧ ∀ (d : OutgoingTail.TailData), d.core.lam < lam0 → resetSourceError d K ≤ d.core.lam / 4

theorem NavierStokes.TailCone.exists_tail_smallness_threshold (P m K : ℝ) (hP : 0 < P) (hK : 0 < K) : ∃ (lam0 : ℝ), 0 < lam0 ∧ ∀ (d : OutgoingTail.TailData), d.core.P = P → d.core.m = m → d.core.lam < lam0 → d.core.lam ≤ 1 / 120 ∧ CorrectedPulseAmplitude.combinedScale d K ≤ 1 / 1000 ∧ PulseCone.sourceConstant d.core.P d.core.m * d.core.lam ^ 29 ≤ 1 / 8 ∧ d.h ≤ 1 / 100 ∧ d.h ≤ Real.exp (-(d.core.holdStart + 3 / 5)) / 8 ∧ resetSourceError d K ≤ d.core.lam / 4 ∧ finiteConeConstant d.core.P d.core.m * d.core.lam ^ 10 ≤ 1 / 2 ∧ releaseConeConstant d.core.P d.core.m * d.core.lam ^ 29 ≤ 1 / 2

noncomputable def NavierStokes.TailCone.PostPulseCone {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (XR : ℝ) : Prop

The post-pulse pointwise cone for the exact corrected schedule.

Equations

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

theorem NavierStokes.TailCone.exists_scheduled_tail_cone (P m : ℝ) (hP : 0 < P) : ∃ (lam0 : ℝ) (K : ℝ), 0 < lam0 ∧ 0 < K ∧ ∀ (d : OutgoingTail.TailData), d.core.P = P → d.core.m = m → d.core.wait = 60 * Real.log (1 / d.core.lam) → d.core.lam < lam0 → ∃ (w : UniformAngularReset.ResetWitness d K), ContDiff ℝ (↑⊤) (CorrectedPulseAmplitude.amplitude d w.coefficients) ∧ (∀ (eta : ℝ), eta ^ 2 ≤ 1 → CorrectedPulseAmplitude.totalEnergy d w.coefficients (CorrectedPulseAmplitude.amplitude d w.coefficients eta) eta = 0) ∧ ∃ (R0 : ℝ), 0 < R0 ∧ ∀ (XR : ℝ), R0 < XR → PostPulseCone w XR

A common positive lam threshold works for every 0 < 2*h < lam. The entrance radius is chosen only after the full schedule, including h. No energy, pressure, angular-lag, or cone inequality is assumed as input.