Constructed flattening, release, and terminal power tail

This file extends the actual outgoing core. The angular/pressure-neutral moment edit is deliberately a separate operation: its required release datum is used to initialize an explicitly solved scalar ODE, but is not asserted to be the unedited angular history.

A proved, fixed bound on the actual step derivative

theorem NavierStokes.OutgoingTail.edge_derivative_nonneg (x : ℝ) : 0 ≤ 2 * FlatCutoff.edge 1 x / x ^ 3

theorem NavierStokes.OutgoingTail.sigma_derivative_nonneg (x : ℝ) : 0 ≤ deriv OutgoingSchedule.sigma x

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

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

theorem NavierStokes.OutgoingTail.exists_sigma_derivative_bound : ∃ (S : ℝ), 1 ≤ S ∧ ∀ (x : ℝ), deriv OutgoingSchedule.sigma x ≤ S

noncomputable def NavierStokes.OutgoingTail.stepBound : ℝ

Step bound, given by Classical.choose exists_sigma_derivative_bound.

Equations

• NavierStokes.OutgoingTail.stepBound = Classical.choose NavierStokes.OutgoingTail.exists_sigma_derivative_bound

theorem NavierStokes.OutgoingTail.stepBound_ge_one : 1 ≤ stepBound

theorem NavierStokes.OutgoingTail.sigma_derivative_le (x : ℝ) : deriv OutgoingSchedule.sigma x ≤ stepBound

noncomputable def NavierStokes.OutgoingTail.flattenLength : ℝ

Flatten length, given by 10 * (stepBound + 1) * Real.log 2 + 1.

Equations

• NavierStokes.OutgoingTail.flattenLength = 10 * (NavierStokes.OutgoingTail.stepBound + 1) * Real.log 2 + 1

theorem NavierStokes.OutgoingTail.flattenLength_pos : 0 < flattenLength

noncomputable def NavierStokes.OutgoingTail.tailCoefficient : ℝ

Tail coefficient, given by Real.exp (-5) / (16 * (stepBound + 1)).

Equations

• NavierStokes.OutgoingTail.tailCoefficient = Real.exp (-5) / (16 * (NavierStokes.OutgoingTail.stepBound + 1))

theorem NavierStokes.OutgoingTail.tailCoefficient_pos : 0 < tailCoefficient

theorem NavierStokes.OutgoingTail.tailCoefficient_le : tailCoefficient ≤ Real.exp (-5) / 16

theorem NavierStokes.OutgoingTail.tailCoefficient_lt_one : tailCoefficient < 1

structure NavierStokes.OutgoingTail.TailData : Type

Tail data, collecting core, h, h_pos, h_small.

• core : OutgoingSchedule.Parameters

  Core of TailData, of type OutgoingSchedule.Parameters.

• h : ℝ

  Step-size parameter of TailData, of type ℝ.

• h_pos : 0 < self.h
• h_small : 2 * self.h < self.core.lam

theorem NavierStokes.OutgoingTail.TailData.h_lt_half (d : TailData) : d.h < 1 / 2

theorem NavierStokes.OutgoingTail.TailData.h_lt_lam (d : TailData) : d.h < d.core.lam

theorem NavierStokes.OutgoingTail.TailData.one_sub_h_pos (d : TailData) : 0 < 1 - d.h

noncomputable def NavierStokes.OutgoingTail.TailData.flattenEnd (d : TailData) : ℝ

Flatten end, given by d.core.endpoint + flattenLength.

Equations

• d.flattenEnd = d.core.endpoint + NavierStokes.OutgoingTail.flattenLength

noncomputable def NavierStokes.OutgoingTail.TailData.uniformWait (d : TailData) : ℝ

Uniform wait, given by 30 * Real.log (1 / d.core.lam).

Equations

• d.uniformWait = 30 * Real.log (1 / d.core.lam)

noncomputable def NavierStokes.OutgoingTail.TailData.releaseStart (d : TailData) : ℝ

Release start, given by d.flattenEnd + d.uniformWait.

Equations

• d.releaseStart = d.flattenEnd + d.uniformWait

theorem NavierStokes.OutgoingTail.TailData.uniformWait_pos (d : TailData) : 0 < d.uniformWait

noncomputable def NavierStokes.OutgoingTail.TailData.longHold (d : TailData) : ℝ

Long hold, given by 4 * Real.log (1 / d.h).

Equations

• d.longHold = 4 * Real.log (1 / d.h)

noncomputable def NavierStokes.OutgoingTail.TailData.secondRampStart (d : TailData) : ℝ

Second ramp start, given by 1 + d.longHold.

Equations

• d.secondRampStart = 1 + d.longHold

noncomputable def NavierStokes.OutgoingTail.TailData.rampEnd (d : TailData) : ℝ

Ramp end, given by d.secondRampStart + 1.

Equations

• d.rampEnd = d.secondRampStart + 1

theorem NavierStokes.OutgoingTail.TailData.longHold_pos (d : TailData) : 0 < d.longHold

theorem NavierStokes.OutgoingTail.TailData.rampEnd_pos (d : TailData) : 0 < d.rampEnd

noncomputable def NavierStokes.OutgoingTail.TailData.rho (d : TailData) : ℝ

Rho, given by tailCoefficient * d.h.

Equations

• d.rho = NavierStokes.OutgoingTail.tailCoefficient * d.h

theorem NavierStokes.OutgoingTail.TailData.rho_pos (d : TailData) : 0 < d.rho

theorem NavierStokes.OutgoingTail.TailData.rho_lt_half (d : TailData) : d.rho < 1 / 2

The fixed terminal taper and its positive weighted debt

noncomputable def NavierStokes.OutgoingTail.tailShape (d : TailData) (t : ℝ) : ℝ

Tail shape, given by 1 - d.rho + d.rho * sigma ((t - 1) / 2).

Equations

• NavierStokes.OutgoingTail.tailShape d t = 1 - d.rho + d.rho * NavierStokes.OutgoingSchedule.sigma ((t - 1) / 2)

noncomputable def NavierStokes.OutgoingTail.tailShapeDeriv (d : TailData) (t : ℝ) : ℝ

Tail shape derivative, given by (d.rho / 2) * deriv sigma ((t - 1) / 2).

Equations

• NavierStokes.OutgoingTail.tailShapeDeriv d t = d.rho / 2 * deriv NavierStokes.OutgoingSchedule.sigma ((t - 1) / 2)

theorem NavierStokes.OutgoingTail.tailShape_contDiff (d : TailData) : ContDiff ℝ (↑⊤) (tailShape d)

theorem NavierStokes.OutgoingTail.tailShapeDeriv_contDiff (d : TailData) : ContDiff ℝ (↑⊤) (tailShapeDeriv d)

theorem NavierStokes.OutgoingTail.tailShape_hasDerivAt (d : TailData) (t : ℝ) : HasDerivAt (tailShape d) (tailShapeDeriv d t) t

theorem NavierStokes.OutgoingTail.tailShape_early (d : TailData) {t : ℝ} (ht : t ≤ 1) : tailShape d t = 1 - d.rho

theorem NavierStokes.OutgoingTail.tailShape_late (d : TailData) {t : ℝ} (ht : 3 ≤ t) : tailShape d t = 1

theorem NavierStokes.OutgoingTail.tailShape_bounds (d : TailData) (t : ℝ) : 1 - d.rho ≤ tailShape d t ∧ tailShape d t ≤ 1

theorem NavierStokes.OutgoingTail.tailShape_pos (d : TailData) (t : ℝ) : 0 < tailShape d t

theorem NavierStokes.OutgoingTail.tailShapeDeriv_nonneg (d : TailData) (t : ℝ) : 0 ≤ tailShapeDeriv d t

theorem NavierStokes.OutgoingTail.tailShapeDeriv_integral (d : TailData) : ∫ (t : ℝ) in 0..3, tailShapeDeriv d t = d.rho

noncomputable def NavierStokes.OutgoingTail.tailLogSlope (d : TailData) (t : ℝ) : ℝ

Tail log slope, given by -d.h + tailShapeDeriv d t / tailShape d t.

Equations

• NavierStokes.OutgoingTail.tailLogSlope d t = -d.h + NavierStokes.OutgoingTail.tailShapeDeriv d t / NavierStokes.OutgoingTail.tailShape d t

noncomputable def NavierStokes.OutgoingTail.tailDebt (d : TailData) : ℝ

Tail debt, given by `(∫ t in (0 : ℝ)..3, Real.exp ((1 - d.h) * t) * tailShapeDeriv d t) / (1

• d.rho)`.

Equations

• NavierStokes.OutgoingTail.tailDebt d = (∫ (t : ℝ) in 0..3, Real.exp ((1 - d.h) * t) * NavierStokes.OutgoingTail.tailShapeDeriv d t) / (1 - d.rho)

theorem NavierStokes.OutgoingTail.tailDebt_bounds (d : TailData) : d.rho / (1 - d.rho) ≤ tailDebt d ∧ tailDebt d ≤ Real.exp 3 * d.rho / (1 - d.rho)

theorem NavierStokes.OutgoingTail.tailDebt_pos (d : TailData) : 0 < tailDebt d

theorem NavierStokes.OutgoingTail.tailDebt_small (d : TailData) : tailDebt d < Real.exp (-2) * d.h

theorem NavierStokes.OutgoingTail.tail_taper_log_derivative (d : TailData) (t : ℝ) : 0 ≤ tailShapeDeriv d t / tailShape d t ∧ tailShapeDeriv d t / tailShape d t < d.h / 4

Actual release coefficient and the integrating-factor solution

noncomputable def NavierStokes.OutgoingTail.releaseSlope (d : TailData) (t : ℝ) : ℝ

Release slope, given by -d.core.lam - (1 - d.core.lam) * sigma t + (1 - d.h) * sigma (t - d.secondRampStart).

Equations

• NavierStokes.OutgoingTail.releaseSlope d t = -d.core.lam - (1 - d.core.lam) * NavierStokes.OutgoingSchedule.sigma t + (1 - d.h) * NavierStokes.OutgoingSchedule.sigma (t - d.secondRampStart)

theorem NavierStokes.OutgoingTail.releaseSlope_contDiff (d : TailData) : ContDiff ℝ (↑⊤) (releaseSlope d)

theorem NavierStokes.OutgoingTail.releaseSlope_early (d : TailData) {t : ℝ} (ht : t ≤ 0) : releaseSlope d t = -d.core.lam

theorem NavierStokes.OutgoingTail.releaseSlope_plateau (d : TailData) {t : ℝ} (ht : 1 ≤ t) (ht' : t ≤ d.secondRampStart) : releaseSlope d t = -1

theorem NavierStokes.OutgoingTail.releaseSlope_late (d : TailData) {t : ℝ} (ht : d.rampEnd ≤ t) : releaseSlope d t = -d.h

theorem NavierStokes.OutgoingTail.releaseSlope_bounds (d : TailData) (t : ℝ) : -1 ≤ releaseSlope d t ∧ releaseSlope d t ≤ -d.h

noncomputable def NavierStokes.OutgoingTail.releaseRate (d : TailData) (t : ℝ) : ℝ

Release rate, given by 1 + releaseSlope d t.

Equations

• NavierStokes.OutgoingTail.releaseRate d t = 1 + NavierStokes.OutgoingTail.releaseSlope d t

noncomputable def NavierStokes.OutgoingTail.releaseSource (d : TailData) (t : ℝ) : ℝ

Release source, given by -releaseSlope d t - d.h.

Equations

• NavierStokes.OutgoingTail.releaseSource d t = -NavierStokes.OutgoingTail.releaseSlope d t - d.h

noncomputable def NavierStokes.OutgoingTail.initialLag (d : TailData) : ℝ

Initial lag, given by (d.core.lam - d.h) / (1 - d.core.lam).

Equations

• NavierStokes.OutgoingTail.initialLag d = (d.core.lam - d.h) / (1 - d.core.lam)

theorem NavierStokes.OutgoingTail.initialLag_gt_h (d : TailData) : d.h < initialLag d

theorem NavierStokes.OutgoingTail.releaseRate_contDiff (d : TailData) : ContDiff ℝ (↑⊤) (releaseRate d)

theorem NavierStokes.OutgoingTail.releaseSource_contDiff (d : TailData) : ContDiff ℝ (↑⊤) (releaseSource d)

noncomputable def NavierStokes.OutgoingTail.linearLag (a b : ℝ → ℝ) (q t : ℝ) : ℝ

Linear lag, given by Real.exp (-primitive a t) * (q + primitive (fun v => Real.exp (primitive a v) * b v) t).

Equations

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

theorem NavierStokes.OutgoingTail.linearLag_contDiff {a b : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) a) (hb : ContDiff ℝ (↑⊤) b) (q : ℝ) : ContDiff ℝ (↑⊤) (linearLag a b q)

theorem NavierStokes.OutgoingTail.linearLag_initial (a b : ℝ → ℝ) (q : ℝ) : linearLag a b q 0 = q

theorem NavierStokes.OutgoingTail.linearLag_hasDerivAt {a b : ℝ → ℝ} (ha : Continuous a) (hb : Continuous b) (q t : ℝ) : HasDerivAt (linearLag a b q) (b t - a t * linearLag a b q t) t

noncomputable def NavierStokes.OutgoingTail.releaseLag (d : TailData) : ℝ → ℝ

Release lag, given by linearLag (releaseRate d) (releaseSource d) (initialLag d).

Equations

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

theorem NavierStokes.OutgoingTail.releaseLag_contDiff (d : TailData) : ContDiff ℝ (↑⊤) (releaseLag d)

theorem NavierStokes.OutgoingTail.releaseLag_initial (d : TailData) : releaseLag d 0 = initialLag d

theorem NavierStokes.OutgoingTail.releaseLag_equation (d : TailData) (t : ℝ) : deriv (releaseLag d) t + (1 + releaseSlope d t) * releaseLag d t = -releaseSlope d t - d.h

theorem NavierStokes.OutgoingTail.release_source_nonneg (d : TailData) (t : ℝ) : 0 ≤ releaseSource d t

theorem NavierStokes.OutgoingTail.release_rate_bounds (d : TailData) (t : ℝ) : 0 ≤ releaseRate d t ∧ releaseRate d t ≤ 1

theorem NavierStokes.OutgoingTail.release_rate_integral_bound (d : TailData) : OutgoingSchedule.primitive (releaseRate d) d.rampEnd ≤ 2

theorem NavierStokes.OutgoingTail.releaseLag_lower (d : TailData) : Real.exp (-2) * initialLag d ≤ releaseLag d d.rampEnd

theorem NavierStokes.OutgoingTail.releaseLag_gt_tailDebt (d : TailData) : tailDebt d < releaseLag d d.rampEnd

noncomputable def NavierStokes.OutgoingTail.decayHold (d : TailData) : ℝ

Decay hold, given by Real.log (releaseLag d d.rampEnd / tailDebt d) / (1 - d.h).

Equations

• NavierStokes.OutgoingTail.decayHold d = Real.log (NavierStokes.OutgoingTail.releaseLag d d.rampEnd / NavierStokes.OutgoingTail.tailDebt d) / (1 - d.h)

theorem NavierStokes.OutgoingTail.decayHold_pos (d : TailData) : 0 < decayHold d

theorem NavierStokes.OutgoingTail.decayHold_hits_target (d : TailData) : releaseLag d d.rampEnd * Real.exp (-(1 - d.h) * decayHold d) = tailDebt d

One globally smooth positive angular profile

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

Log shape, given by Real.log (1 + eta ^ 2).

Equations

• NavierStokes.OutgoingTail.logShape eta = Real.log (1 + eta ^ 2)

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

noncomputable def NavierStokes.OutgoingTail.flattenFactor (d : TailData) (p : ℝ × ℝ) : ℝ

Flatten factor, given by Real.exp (sigma ((p.1 - d.core.endpoint) / flattenLength) * (logShape p.2 - Real.log 2)).

Equations

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

noncomputable def NavierStokes.OutgoingTail.flattened (d : TailData) (p : ℝ × ℝ) : ℝ

Flattened, given by angular d.core.P d.core.dropLength d.core.lam p * flattenFactor d p.

Equations

• NavierStokes.OutgoingTail.flattened d p = NavierStokes.OutgoingSchedule.angular d.core.P d.core.dropLength d.core.lam p * NavierStokes.OutgoingTail.flattenFactor d p

theorem NavierStokes.OutgoingTail.flattenFactor_contDiff (d : TailData) : ContDiff ℝ (↑⊤) (flattenFactor d)

theorem NavierStokes.OutgoingTail.flattened_contDiff (d : TailData) : ContDiff ℝ (↑⊤) (flattened d)

theorem NavierStokes.OutgoingTail.flattened_pos (d : TailData) (p : ℝ × ℝ) : 0 < flattened d p

theorem NavierStokes.OutgoingTail.flattenFactor_before (d : TailData) (eta : ℝ) {y : ℝ} (hy : y ≤ d.core.endpoint) : flattenFactor d (y, eta) = 1

theorem NavierStokes.OutgoingTail.flattened_before (d : TailData) (eta : ℝ) {y : ℝ} (hy : y ≤ d.core.endpoint) : flattened d (y, eta) = OutgoingSchedule.angular d.core.P d.core.dropLength d.core.lam (y, eta)

theorem NavierStokes.OutgoingTail.flattened_uniform (d : TailData) (eta : ℝ) {y : ℝ} (hy : d.flattenEnd ≤ y) : flattened d (y, eta) = OutgoingSchedule.radialAmplitude d.core.P d.core.dropLength d.core.lam y / 2

noncomputable def NavierStokes.OutgoingTail.releaseAdjustment (d : TailData) : ℝ → ℝ

Release adjustment, given by primitive (fun t => releaseSlope d t + d.core.lam).

Equations

• NavierStokes.OutgoingTail.releaseAdjustment d = NavierStokes.OutgoingSchedule.primitive fun (t : ℝ) => NavierStokes.OutgoingTail.releaseSlope d t + d.core.lam

theorem NavierStokes.OutgoingTail.releaseAdjustment_contDiff (d : TailData) : ContDiff ℝ (↑⊤) (releaseAdjustment d)

theorem NavierStokes.OutgoingTail.releaseAdjustment_early (d : TailData) {t : ℝ} (ht : t ≤ 0) : releaseAdjustment d t = 0

theorem NavierStokes.OutgoingTail.releaseAdjustment_late (d : TailData) {a t : ℝ} (ha : d.rampEnd ≤ a) (hat : a ≤ t) : releaseAdjustment d t = releaseAdjustment d a + (d.core.lam - d.h) * (t - a)

noncomputable def NavierStokes.OutgoingTail.tailStart (d : TailData) : ℝ

Tail start, given by d.releaseStart + d.rampEnd + decayHold d.

Equations

• NavierStokes.OutgoingTail.tailStart d = d.releaseStart + d.rampEnd + NavierStokes.OutgoingTail.decayHold d

noncomputable def NavierStokes.OutgoingTail.tailEnd (d : TailData) : ℝ

Tail end, given by tailStart d + 3.

Equations

• NavierStokes.OutgoingTail.tailEnd d = NavierStokes.OutgoingTail.tailStart d + 3

theorem NavierStokes.OutgoingTail.releaseStart_gt_flattenEnd (d : TailData) : d.flattenEnd < d.releaseStart

theorem NavierStokes.OutgoingTail.flattenEnd_gt_core (d : TailData) : d.core.endpoint < d.flattenEnd

theorem NavierStokes.OutgoingTail.tailStart_gt_release (d : TailData) : d.releaseStart < tailStart d

noncomputable def NavierStokes.OutgoingTail.finalAngular (d : TailData) (p : ℝ × ℝ) : ℝ

Final angular, given by flattened d p * Real.exp (releaseAdjustment d (p.1 - d.releaseStart)) * (tailShape d (p.1 - tailStart d) / (1 - d.rho)).

Equations

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

theorem NavierStokes.OutgoingTail.finalAngular_contDiff (d : TailData) : ContDiff ℝ (↑⊤) (finalAngular d)

theorem NavierStokes.OutgoingTail.finalAngular_pos (d : TailData) (p : ℝ × ℝ) : 0 < finalAngular d p

theorem NavierStokes.OutgoingTail.finalAngular_before (d : TailData) (eta : ℝ) {y : ℝ} (hy : y ≤ d.core.endpoint) : finalAngular d (y, eta) = OutgoingSchedule.angular d.core.P d.core.dropLength d.core.lam (y, eta)

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

Carrier, given by (radialAmplitude d.core.P d.core.dropLength d.core.lam y / 2) * Real.exp (releaseAdjustment d (y - d.releaseStart)).

Equations

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

theorem NavierStokes.OutgoingTail.carrier_pos (d : TailData) (y : ℝ) : 0 < carrier d y

theorem NavierStokes.OutgoingTail.finalAngular_uniform (d : TailData) (eta : ℝ) {y : ℝ} (hy : d.flattenEnd ≤ y) : finalAngular d (y, eta) = carrier d y * (tailShape d (y - tailStart d) / (1 - d.rho))

theorem NavierStokes.OutgoingTail.finalAngular_eta_independent (d : TailData) (eta eta' : ℝ) {y : ℝ} (hy : d.flattenEnd ≤ y) : finalAngular d (y, eta) = finalAngular d (y, eta')

theorem NavierStokes.OutgoingTail.finalAngular_uniform_wait (d : TailData) (eta : ℝ) {y : ℝ} (hy : d.flattenEnd ≤ y) (hy' : y ≤ d.releaseStart) : finalAngular d (y, eta) = OutgoingSchedule.radialAmplitude d.core.P d.core.dropLength d.core.lam y / 2

theorem NavierStokes.OutgoingTail.coreEndpoint_ge_hold (d : TailData) : d.core.holdStart ≤ d.core.endpoint

theorem NavierStokes.OutgoingTail.carrier_late_scaling (d : TailData) {a y : ℝ} (ha : d.releaseStart + d.rampEnd ≤ a) (hay : a ≤ y) : carrier d y = carrier d a * Real.exp (-(1 / 2 + d.h) * (y - a))

noncomputable def NavierStokes.OutgoingTail.powerConstant (d : TailData) : ℝ

Power constant, given by carrier d (tailStart d) * Real.exp ((1 / 2 + d.h) * tailStart d) / (1 - d.rho).

Equations

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

theorem NavierStokes.OutgoingTail.powerConstant_pos (d : TailData) : 0 < powerConstant d

theorem NavierStokes.OutgoingTail.finalAngular_tail (d : TailData) (eta : ℝ) {y : ℝ} (hy : tailStart d ≤ y) : finalAngular d (y, eta) = powerConstant d * Real.exp (-(1 / 2 + d.h) * y) * tailShape d (y - tailStart d)

theorem NavierStokes.OutgoingTail.finalAngular_eventual_power (d : TailData) (eta : ℝ) {y : ℝ} (hy : tailEnd d ≤ y) : finalAngular d (y, eta) = powerConstant d * Real.exp (-(1 / 2 + d.h) * y)

theorem NavierStokes.OutgoingTail.finalAngular_radial_power (d : TailData) (eta : ℝ) {X : ℝ} (hX : 0 < X) (hfar : tailEnd d ≤ Real.log X) : finalAngular d (Real.log X, eta) = powerConstant d * X ^ (-(1 / 2 + d.h))

theorem NavierStokes.OutgoingTail.axial_product_unchanged (d : TailData) (amp : ℝ → ℝ) (eta y : ℝ) : finalAngular d (y, eta) * OutgoingSchedule.axial d.core amp (y, eta) = OutgoingSchedule.angular d.core.P d.core.dropLength d.core.lam (y, eta) * OutgoingSchedule.axial d.core amp (y, eta)

The prescribed taper is an actual backward lag solution

noncomputable def NavierStokes.OutgoingTail.tailRate (d : TailData) (t : ℝ) : ℝ

Tail rate, given by 1 + tailLogSlope d t.

Equations

• NavierStokes.OutgoingTail.tailRate d t = 1 + NavierStokes.OutgoingTail.tailLogSlope d t

theorem NavierStokes.OutgoingTail.tailRate_contDiff (d : TailData) : ContDiff ℝ (↑⊤) (tailRate d)

noncomputable def NavierStokes.OutgoingTail.weightedTailDerivative (d : TailData) (t : ℝ) : ℝ

Weighted tail derivative, given by Real.exp ((1 - d.h) * t) * tailShapeDeriv d t.

Equations

• NavierStokes.OutgoingTail.weightedTailDerivative d t = Real.exp ((1 - d.h) * t) * NavierStokes.OutgoingTail.tailShapeDeriv d t

theorem NavierStokes.OutgoingTail.weightedTailDerivative_contDiff (d : TailData) : ContDiff ℝ (↑⊤) (weightedTailDerivative d)

theorem NavierStokes.OutgoingTail.tailRate_primitive (d : TailData) (t : ℝ) : OutgoingSchedule.primitive (tailRate d) t = (1 - d.h) * t + Real.log (tailShape d t) - Real.log (1 - d.rho)

theorem NavierStokes.OutgoingTail.tail_integrating_factor (d : TailData) (t : ℝ) : Real.exp (OutgoingSchedule.primitive (tailRate d) t) = Real.exp ((1 - d.h) * t) * tailShape d t / (1 - d.rho)

theorem NavierStokes.OutgoingTail.tailDebt_source_formula (d : TailData) : tailDebt d = ∫ (v : ℝ) in 0..3, Real.exp (OutgoingSchedule.primitive (tailRate d) v) * (tailShapeDeriv d v / tailShape d v)

This is exactly the weighted integral prescribed for Qp in stage 5.

noncomputable def NavierStokes.OutgoingTail.tailNumerator (d : TailData) (t : ℝ) : ℝ

Tail numerator, given by Real.exp (-(1 - d.h) * t) * (primitive (weightedTailDerivative d) 3 - primitive (weightedTailDerivative d) t).

Equations

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

noncomputable def NavierStokes.OutgoingTail.tailLag (d : TailData) (t : ℝ) : ℝ

Tail lag, given by tailNumerator d t / tailShape d t.

Equations

• NavierStokes.OutgoingTail.tailLag d t = NavierStokes.OutgoingTail.tailNumerator d t / NavierStokes.OutgoingTail.tailShape d t

theorem NavierStokes.OutgoingTail.tailNumerator_contDiff (d : TailData) : ContDiff ℝ (↑⊤) (tailNumerator d)

theorem NavierStokes.OutgoingTail.tailLag_contDiff (d : TailData) : ContDiff ℝ (↑⊤) (tailLag d)

theorem NavierStokes.OutgoingTail.tailNumerator_hasDerivAt (d : TailData) (t : ℝ) : HasDerivAt (tailNumerator d) (-(1 - d.h) * tailNumerator d t - tailShapeDeriv d t) t

theorem NavierStokes.OutgoingTail.tailLag_hasDerivAt (d : TailData) (t : ℝ) : HasDerivAt (tailLag d) (-tailRate d t * tailLag d t - tailShapeDeriv d t / tailShape d t) t

theorem NavierStokes.OutgoingTail.tailLag_equation (d : TailData) (t : ℝ) : deriv (tailLag d) t + (1 + tailLogSlope d t) * tailLag d t = -tailLogSlope d t - d.h

theorem NavierStokes.OutgoingTail.tailLag_initial (d : TailData) : tailLag d 0 = tailDebt d

theorem NavierStokes.OutgoingTail.tailLag_terminal (d : TailData) : tailLag d 3 = 0

theorem NavierStokes.OutgoingTail.tailLag_nonneg (d : TailData) {t : ℝ} (ht : t ≤ 3) : 0 ≤ tailLag d t

noncomputable def NavierStokes.OutgoingTail.holdLag (d : TailData) (t : ℝ) : ℝ

Hold lag, given by releaseLag d d.rampEnd * Real.exp (-(1 - d.h) * t).

Equations

• NavierStokes.OutgoingTail.holdLag d t = NavierStokes.OutgoingTail.releaseLag d d.rampEnd * Real.exp (-(1 - d.h) * t)

theorem NavierStokes.OutgoingTail.holdLag_hasDerivAt (d : TailData) (t : ℝ) : HasDerivAt (holdLag d) (-(1 - d.h) * holdLag d t) t

theorem NavierStokes.OutgoingTail.holdLag_equation (d : TailData) (t : ℝ) : deriv (holdLag d) t + (1 - d.h) * holdLag d t = 0

theorem NavierStokes.OutgoingTail.holdLag_matches (d : TailData) : holdLag d 0 = releaseLag d d.rampEnd ∧ holdLag d (decayHold d) = tailLag d 0

noncomputable def NavierStokes.OutgoingTail.tailDataOfCore (c : OutgoingSchedule.Parameters) : TailData

Every existing core has the scalar parameters used in this tail construction.

Equations

• NavierStokes.OutgoingTail.tailDataOfCore c = { core := c, h := c.lam / 4, h_pos := ⋯, h_small := ⋯ }

theorem NavierStokes.OutgoingTail.constructed_tail (d : TailData) : ContDiff ℝ (↑⊤) (finalAngular d) ∧ (∀ (p : ℝ × ℝ), 0 < finalAngular d p) ∧ 0 < decayHold d ∧ holdLag d (decayHold d) = tailLag d 0 ∧ tailLag d 3 = 0 ∧ (∀ (eta y : ℝ), y ≤ d.core.endpoint → finalAngular d (y, eta) = OutgoingSchedule.angular d.core.P d.core.dropLength d.core.lam (y, eta)) ∧ ∀ (eta y : ℝ), tailEnd d ≤ y → finalAngular d (y, eta) = powerConstant d * Real.exp (-(1 / 2 + d.h) * y)

The exact flattening slope and the unchanged axial histories

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

Flattening slope, given by -d.core.lam + (deriv sigma ((y - d.core.endpoint) / flattenLength) / flattenLength) * (logShape eta - Real.log 2).

Equations

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

theorem NavierStokes.OutgoingTail.flatteningSlope_bounds (d : TailData) (y eta : ℝ) (heta : eta ^ 2 ≤ 1) : -d.core.lam - 1 / 10 ≤ flatteningSlope d y eta ∧ flatteningSlope d y eta ≤ -d.core.lam

theorem NavierStokes.OutgoingTail.flattened_hasDerivAt (d : TailData) (eta : ℝ) {y : ℝ} (hy : d.core.endpoint ≤ y) : HasDerivAt (fun (t : ℝ) => flattened d (t, eta)) (flattened d (y, eta) * (flatteningSlope d y eta - 1 / 2)) y

theorem NavierStokes.OutgoingTail.flattened_log_hasDerivAt (d : TailData) (eta : ℝ) {y : ℝ} (hy : d.core.endpoint ≤ y) : HasDerivAt (fun (t : ℝ) => Real.log (flattened d (t, eta))) (flatteningSlope d y eta - 1 / 2) y

noncomputable def NavierStokes.OutgoingTail.extendedAngularMoment (d : TailData) (amp : ℝ → ℝ) (eta y : ℝ) : ℝ

Extended angular moment as an element of ℝ.

Equations

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

theorem NavierStokes.OutgoingTail.extendedAngularMoment_eq (d : TailData) (amp : ℝ → ℝ) (eta y : ℝ) : extendedAngularMoment d amp eta y = OutgoingSchedule.angularMoment d.core amp eta y

theorem NavierStokes.OutgoingTail.extended_moments_zero (d : TailData) (amp : ℝ → ℝ) (eta : ℝ) {y : ℝ} (hy : d.core.endpoint ≤ y) : OutgoingSchedule.massMoment d.core amp eta y = 0 ∧ extendedAngularMoment d amp eta y = 0

theorem NavierStokes.OutgoingTail.carrier_hasDerivAt (d : TailData) {y : ℝ} (hy : d.releaseStart ≤ y) : HasDerivAt (carrier d) (carrier d y * (releaseSlope d (y - d.releaseStart) - 1 / 2)) y

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

Profile slope, given by releaseSlope d (y - d.releaseStart) + tailShapeDeriv d (y - tailStart d) / tailShape d (y - tailStart d).

Equations

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

theorem NavierStokes.OutgoingTail.finalAngular_hasDerivAt_on_release (d : TailData) (eta : ℝ) {y : ℝ} (hy : d.releaseStart ≤ y) : HasDerivAt (fun (t : ℝ) => finalAngular d (t, eta)) (finalAngular d (y, eta) * (profileSlope d y - 1 / 2)) y

theorem NavierStokes.OutgoingTail.finalAngular_log_hasDerivAt_on_release (d : TailData) (eta : ℝ) {y : ℝ} (hy : d.releaseStart ≤ y) : HasDerivAt (fun (t : ℝ) => Real.log (finalAngular d (t, eta))) (profileSlope d y - 1 / 2) y

theorem NavierStokes.OutgoingTail.profileSlope_tail (d : TailData) {y : ℝ} (hy : tailStart d ≤ y) : profileSlope d y = tailLogSlope d (y - tailStart d)

theorem NavierStokes.OutgoingTail.uniformWait_gt_twentyseven (d : TailData) : 27 < d.uniformWait

The last four log units are available for the separate angular reset.

theorem NavierStokes.OutgoingTail.finalAngular_last_four (d : TailData) (eta : ℝ) {y : ℝ} (hy : d.releaseStart - 4 ≤ y) (hy' : y ≤ d.releaseStart) : finalAngular d (y, eta) = OutgoingSchedule.radialAmplitude d.core.P d.core.dropLength d.core.lam y / 2