Constructed outgoing profiles through the axial pulse

The clock is the global logarithmic radius, with the first ramp starting at zero. All functions below are actual formulas. Stage inequalities are hypotheses on real parameters, not assumptions that suitable profiles or corrections exist.

The manuscript's smooth step

noncomputable def NavierStokes.OutgoingSchedule.sigma (x : ℝ) : ℝ

Sigma, given by FlatCutoff.edge 1 x / (FlatCutoff.edge 1 x + FlatCutoff.edge 1 (1 - x)).

Equations

• NavierStokes.OutgoingSchedule.sigma x = NavierStokes.FlatCutoff.edge 1 x / (NavierStokes.FlatCutoff.edge 1 x + NavierStokes.FlatCutoff.edge 1 (1 - x))

theorem NavierStokes.OutgoingSchedule.sigma_denom_pos (x : ℝ) : 0 < FlatCutoff.edge 1 x + FlatCutoff.edge 1 (1 - x)

theorem NavierStokes.OutgoingSchedule.sigma_contDiff : ContDiff ℝ (↑⊤) sigma

theorem NavierStokes.OutgoingSchedule.sigma_zero {x : ℝ} (hx : x ≤ 0) : sigma x = 0

theorem NavierStokes.OutgoingSchedule.sigma_one {x : ℝ} (hx : 1 ≤ x) : sigma x = 1

theorem NavierStokes.OutgoingSchedule.sigma_nonneg (x : ℝ) : 0 ≤ sigma x

theorem NavierStokes.OutgoingSchedule.sigma_le_one (x : ℝ) : sigma x ≤ 1

theorem NavierStokes.OutgoingSchedule.edge_monotone : Monotone (FlatCutoff.edge 1)

theorem NavierStokes.OutgoingSchedule.sigma_monotone : Monotone sigma

Smooth primitives and the single global slope

noncomputable def NavierStokes.OutgoingSchedule.primitive (g : ℝ → ℝ) (y : ℝ) : ℝ

Primitive, given by ∫ t in (0 : ℝ)..y, g t.

Equations

• NavierStokes.OutgoingSchedule.primitive g y = ∫ (t : ℝ) in 0..y, g t

theorem NavierStokes.OutgoingSchedule.primitive_hasDerivAt {g : ℝ → ℝ} (hg : Continuous g) (y : ℝ) : HasDerivAt (primitive g) (g y) y

theorem NavierStokes.OutgoingSchedule.primitive_contDiff {g : ℝ → ℝ} (hg : ContDiff ℝ (↑⊤) g) : ContDiff ℝ (↑⊤) (primitive g)

theorem NavierStokes.OutgoingSchedule.primitive_increment {g : ℝ → ℝ} (hg : Continuous g) (a b c : ℝ) (hc : ∀ t ∈ Set.uIcc a b, g t = c) : primitive g b = primitive g a + (b - a) * c

noncomputable def NavierStokes.OutgoingSchedule.slope (dropLength lam y : ℝ) : ℝ

Slope, given by (3 / 5) * (1 - sigma y) - lam * sigma (y - (dropLength + 1)).

Equations

• NavierStokes.OutgoingSchedule.slope dropLength lam y = 3 / 5 * (1 - NavierStokes.OutgoingSchedule.sigma y) - lam * NavierStokes.OutgoingSchedule.sigma (y - (dropLength + 1))

theorem NavierStokes.OutgoingSchedule.slope_contDiff (dropLength lam : ℝ) : ContDiff ℝ (↑⊤) (slope dropLength lam)

theorem NavierStokes.OutgoingSchedule.slope_ideal {dropLength lam y : ℝ} (hd : 0 ≤ dropLength) (hy : y ≤ 0) : slope dropLength lam y = 3 / 5

theorem NavierStokes.OutgoingSchedule.slope_drop {dropLength lam y : ℝ} (hy : 1 ≤ y) (hy' : y ≤ dropLength + 1) : slope dropLength lam y = 0

theorem NavierStokes.OutgoingSchedule.slope_hold {dropLength lam y : ℝ} (hd : 0 ≤ dropLength) (hy : dropLength + 2 ≤ y) : slope dropLength lam y = -lam

noncomputable def NavierStokes.OutgoingSchedule.logAmplitude (dropLength lam : ℝ) : ℝ → ℝ

Log amplitude, given by primitive (fun y => slope dropLength lam y - 1 / 2).

Equations

• NavierStokes.OutgoingSchedule.logAmplitude dropLength lam = NavierStokes.OutgoingSchedule.primitive fun (y : ℝ) => NavierStokes.OutgoingSchedule.slope dropLength lam y - 1 / 2

noncomputable def NavierStokes.OutgoingSchedule.radialAmplitude (P dropLength lam y : ℝ) : ℝ

Radial amplitude, given by P * Real.exp (logAmplitude dropLength lam y).

Equations

• NavierStokes.OutgoingSchedule.radialAmplitude P dropLength lam y = P * Real.exp (NavierStokes.OutgoingSchedule.logAmplitude dropLength lam y)

noncomputable def NavierStokes.OutgoingSchedule.shape (eta : ℝ) : ℝ

Shape, given by (1 + eta ^ 2)⁻¹.

Equations

• NavierStokes.OutgoingSchedule.shape eta = (1 + eta ^ 2)⁻¹

noncomputable def NavierStokes.OutgoingSchedule.angular (P dropLength lam : ℝ) (p : ℝ × ℝ) : ℝ

Angular, given by radialAmplitude P dropLength lam p.1 * shape p.2.

Equations

• NavierStokes.OutgoingSchedule.angular P dropLength lam p = NavierStokes.OutgoingSchedule.radialAmplitude P dropLength lam p.1 * NavierStokes.OutgoingSchedule.shape p.2

theorem NavierStokes.OutgoingSchedule.logAmplitude_contDiff (dropLength lam : ℝ) : ContDiff ℝ (↑⊤) (logAmplitude dropLength lam)

theorem NavierStokes.OutgoingSchedule.radialAmplitude_contDiff (P dropLength lam : ℝ) : ContDiff ℝ (↑⊤) (radialAmplitude P dropLength lam)

theorem NavierStokes.OutgoingSchedule.shape_pos (eta : ℝ) : 0 < shape eta

theorem NavierStokes.OutgoingSchedule.shape_contDiff : ContDiff ℝ (↑⊤) shape

theorem NavierStokes.OutgoingSchedule.angular_contDiff (P dropLength lam : ℝ) : ContDiff ℝ (↑⊤) (angular P dropLength lam)

theorem NavierStokes.OutgoingSchedule.angular_pos {P : ℝ} (hP : 0 < P) (dropLength lam : ℝ) (p : ℝ × ℝ) : 0 < angular P dropLength lam p

theorem NavierStokes.OutgoingSchedule.radialAmplitude_hasDerivAt (P dropLength lam y : ℝ) : HasDerivAt (radialAmplitude P dropLength lam) (radialAmplitude P dropLength lam y * (slope dropLength lam y - 1 / 2)) y

theorem NavierStokes.OutgoingSchedule.logAmplitude_ideal {dropLength lam y : ℝ} (hd : 0 ≤ dropLength) (hy : y ≤ 0) : logAmplitude dropLength lam y = y / 10

theorem NavierStokes.OutgoingSchedule.angular_ideal {dropLength lam y eta P : ℝ} (hd : 0 ≤ dropLength) (hy : y ≤ 0) : angular P dropLength lam (y, eta) = P * shape eta * Real.exp (y / 10)

theorem NavierStokes.OutgoingSchedule.radialAmplitude_hold {dropLength lam a y P : ℝ} (hd : 0 ≤ dropLength) (ha : dropLength + 2 ≤ a) (hay : a ≤ y) : radialAmplitude P dropLength lam y = radialAmplitude P dropLength lam a * Real.exp (-(1 / 2 + lam) * (y - a))

The logarithmically slow axial drop

noncomputable def NavierStokes.OutgoingSchedule.dropCoefficient (m y : ℝ) : ℝ

Drop coefficient, with branches according to y ≤ 1.

Equations

• NavierStokes.OutgoingSchedule.dropCoefficient m y = if y ≤ 1 then 4 else 4 * (1 - NavierStokes.OutgoingSchedule.sigma (Real.log y / m))

theorem NavierStokes.OutgoingSchedule.dropCoefficient_early (m : ℝ) {y : ℝ} (hy : y ≤ 1) : dropCoefficient m y = 4

theorem NavierStokes.OutgoingSchedule.dropCoefficient_eq {m y : ℝ} (hm : 0 < m) (hy : 0 < y) : dropCoefficient m y = 4 * (1 - sigma (Real.log y / m))

theorem NavierStokes.OutgoingSchedule.dropCoefficient_contDiff {m : ℝ} (hm : 0 < m) : ContDiff ℝ (↑⊤) (dropCoefficient m)

theorem NavierStokes.OutgoingSchedule.dropCoefficient_late {m y : ℝ} (hm : 0 < m) (hy : Real.exp m ≤ y) : dropCoefficient m y = 0

theorem NavierStokes.OutgoingSchedule.dropCoefficient_bounds (m y : ℝ) : 0 ≤ dropCoefficient m y ∧ dropCoefficient m y ≤ 4

noncomputable def NavierStokes.OutgoingSchedule.initialAxial (m : ℝ) (p : ℝ × ℝ) : ℝ

Initial axial, given by dropCoefficient m p.1 * p.2.

Equations

• NavierStokes.OutgoingSchedule.initialAxial m p = NavierStokes.OutgoingSchedule.dropCoefficient m p.1 * p.2

theorem NavierStokes.OutgoingSchedule.initialAxial_contDiff {m : ℝ} (hm : 0 < m) : ContDiff ℝ (↑⊤) (initialAxial m)

The main pulse and fixed, separated repair intervals

noncomputable def NavierStokes.OutgoingSchedule.pulseRamp : ℝ → ℝ

Pulse ramp, given by primitive (fun z => sigma (50 * z)).

Equations

• NavierStokes.OutgoingSchedule.pulseRamp = NavierStokes.OutgoingSchedule.primitive fun (z : ℝ) => NavierStokes.OutgoingSchedule.sigma (50 * z)

noncomputable def NavierStokes.OutgoingSchedule.mainPulse (z : ℝ) : ℝ

Main pulse, given by pulseRamp z * (1 - sigma (z - 10)).

Equations

• NavierStokes.OutgoingSchedule.mainPulse z = NavierStokes.OutgoingSchedule.pulseRamp z * (1 - NavierStokes.OutgoingSchedule.sigma (z - 10))

theorem NavierStokes.OutgoingSchedule.pulseRamp_contDiff : ContDiff ℝ (↑⊤) pulseRamp

theorem NavierStokes.OutgoingSchedule.mainPulse_contDiff : ContDiff ℝ (↑⊤) mainPulse

theorem NavierStokes.OutgoingSchedule.pulseRamp_zero {z : ℝ} (hz : z ≤ 0) : pulseRamp z = 0

theorem NavierStokes.OutgoingSchedule.mainPulse_zero_left {z : ℝ} (hz : z ≤ 0) : mainPulse z = 0

theorem NavierStokes.OutgoingSchedule.mainPulse_zero_right {z : ℝ} (hz : 11 ≤ z) : mainPulse z = 0

structure NavierStokes.OutgoingSchedule.Parameters : Type

Only finite real parameters and their elementary inequalities are input.

• P : ℝ

  P of Parameters, of type ℝ.

• m : ℝ

  M of Parameters, of type ℝ.

• lam : ℝ

  Lam of Parameters, of type ℝ.

• wait : ℝ

  Wait of Parameters, of type ℝ.

• P_pos : 0 < self.P
• m_pos : 0 < self.m
• lam_pos : 0 < self.lam
• lam_lt : self.lam < 1 / 10
• wait_gt : 25 < self.wait

noncomputable def NavierStokes.OutgoingSchedule.Parameters.dropLength (c : Parameters) : ℝ

Drop length, given by Real.exp c.m + 10.

Equations

• c.dropLength = Real.exp c.m + 10

noncomputable def NavierStokes.OutgoingSchedule.Parameters.holdStart (c : Parameters) : ℝ

Hold start, given by c.dropLength + 2.

Equations

• c.holdStart = c.dropLength + 2

noncomputable def NavierStokes.OutgoingSchedule.Parameters.pulseStart (c : Parameters) : ℝ

Pulse start, given by c.holdStart + c.wait.

Equations

• c.pulseStart = c.holdStart + c.wait

noncomputable def NavierStokes.OutgoingSchedule.Parameters.pulseLength (c : Parameters) : ℝ

Pulse length, given by 13 / c.lam.

Equations

• c.pulseLength = 13 / c.lam

noncomputable def NavierStokes.OutgoingSchedule.Parameters.endpoint (c : Parameters) : ℝ

Endpoint, given by c.pulseStart + c.pulseLength.

Equations

• c.endpoint = c.pulseStart + c.pulseLength

theorem NavierStokes.OutgoingSchedule.Parameters.dropLength_pos (c : Parameters) : 0 < c.dropLength

theorem NavierStokes.OutgoingSchedule.Parameters.holdStart_pos (c : Parameters) : 0 < c.holdStart

theorem NavierStokes.OutgoingSchedule.Parameters.pulseStart_ge_hold (c : Parameters) : c.holdStart ≤ c.pulseStart

theorem NavierStokes.OutgoingSchedule.Parameters.pulseStart_pos (c : Parameters) : 0 < c.pulseStart

theorem NavierStokes.OutgoingSchedule.Parameters.pulseLength_pos (c : Parameters) : 0 < c.pulseLength

noncomputable def NavierStokes.OutgoingSchedule.Parameters.exponents (c : Parameters) (i : Fin 2) : ℝ

Exponents, with branches according to i = 0.

Equations

• c.exponents i = if i = 0 then -(1 / 2 + c.lam) else -(1 / 2 + 2 * c.lam)

noncomputable def NavierStokes.OutgoingSchedule.Parameters.lower (c : Parameters) (i : Fin 2) : ℝ

The log supports lie inside (L-3.15,L-2.85) and (L-1.15,L-.85).

Equations

• c.lower i = Real.exp (c.pulseLength - if i = 0 then 63 / 20 else 23 / 20)

noncomputable def NavierStokes.OutgoingSchedule.Parameters.upper (c : Parameters) (i : Fin 2) : ℝ

Upper, given by Real.exp (c.pulseLength - if i = 0 then 57 / 20 else 17 / 20).

Equations

• c.upper i = Real.exp (c.pulseLength - if i = 0 then 57 / 20 else 17 / 20)

theorem NavierStokes.OutgoingSchedule.Parameters.exponents_injective (c : Parameters) : Function.Injective c.exponents

theorem NavierStokes.OutgoingSchedule.Parameters.lower_pos (c : Parameters) (i : Fin 2) : 0 < c.lower i

theorem NavierStokes.OutgoingSchedule.Parameters.lower_lt_upper (c : Parameters) (i : Fin 2) : c.lower i < c.upper i

theorem NavierStokes.OutgoingSchedule.Parameters.intervals_separated (c : Parameters) (i j : Fin 2) (hij : i < j) : c.upper i ≤ c.lower j

theorem NavierStokes.OutgoingSchedule.Parameters.one_lt_lower (c : Parameters) (i : Fin 2) : 1 < c.lower i

theorem NavierStokes.OutgoingSchedule.Parameters.upper_lt_end (c : Parameters) (i : Fin 2) : c.upper i < Real.exp c.pulseLength

theorem NavierStokes.OutgoingSchedule.Parameters.main_end_lt_lower (c : Parameters) (i : Fin 2) : Real.exp (11 / c.lam) < c.lower i

Explicit smooth debts and constructed corrections

noncomputable def NavierStokes.OutgoingSchedule.prefixM (c : Parameters) : ℝ

Prefix M, given by 4 + ∫ y in (0 : ℝ)..c.pulseStart, Real.exp y * dropCoefficient c.m y.

Equations

• NavierStokes.OutgoingSchedule.prefixM c = 4 + ∫ (y : ℝ) in 0..c.pulseStart, Real.exp y * NavierStokes.OutgoingSchedule.dropCoefficient c.m y

noncomputable def NavierStokes.OutgoingSchedule.prefixJ (c : Parameters) : ℝ

Prefix J as an element of ℝ.

Equations

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

noncomputable def NavierStokes.OutgoingSchedule.pulseAmplitude (c : Parameters) : ℝ

Pulse amplitude, given by radialAmplitude c.P c.dropLength c.lam c.pulseStart.

Equations

• NavierStokes.OutgoingSchedule.pulseAmplitude c = NavierStokes.OutgoingSchedule.radialAmplitude c.P c.dropLength c.lam c.pulseStart

noncomputable def NavierStokes.OutgoingSchedule.momentScale (c : Parameters) (i : Fin 2) : ℝ

Moment scale, with branches according to i = 0.

Equations

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

theorem NavierStokes.OutgoingSchedule.pulseAmplitude_pos (c : Parameters) : 0 < pulseAmplitude c

theorem NavierStokes.OutgoingSchedule.momentScale_pos (c : Parameters) (i : Fin 2) : 0 < momentScale c i

noncomputable def NavierStokes.OutgoingSchedule.prefixCoefficient (c : Parameters) (i : Fin 2) : ℝ

Prefix coefficient, given by (if i = 0 then prefixM c else prefixJ c) / momentScale c i.

Equations

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

noncomputable def NavierStokes.OutgoingSchedule.mainMoment (c : Parameters) (i : Fin 2) : ℝ

Main moment, given by ∫ x in (1 : ℝ)..Real.exp c.pulseLength, x ^ c.exponents i * mainPulse (c.lam * Real.log x).

Equations

• NavierStokes.OutgoingSchedule.mainMoment c i = ∫ (x : ℝ) in 1..Real.exp c.pulseLength, x ^ c.exponents i * NavierStokes.OutgoingSchedule.mainPulse (c.lam * Real.log x)

noncomputable def NavierStokes.OutgoingSchedule.debt (c : Parameters) (amp : ℝ → ℝ) (eta : ℝ) (i : Fin 2) : ℝ

Debt, given by -(prefixCoefficient c i * eta * (1 + eta ^ 2) + amp eta * mainMoment c i).

Equations

• NavierStokes.OutgoingSchedule.debt c amp eta i = -(NavierStokes.OutgoingSchedule.prefixCoefficient c i * eta * (1 + eta ^ 2) + amp eta * NavierStokes.OutgoingSchedule.mainMoment c i)

theorem NavierStokes.OutgoingSchedule.debt_contDiff (c : Parameters) {amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) amp) (i : Fin 2) : ContDiff ℝ ↑⊤ fun (eta : ℝ) => debt c amp eta i

noncomputable def NavierStokes.OutgoingSchedule.correction (c : Parameters) (amp : ℝ → ℝ) (eta x : ℝ) : ℝ

Correction, given by LocalizedMomentRepair.repair c.exponents c.lower c.upper (debt c amp eta) x.

Equations

• NavierStokes.OutgoingSchedule.correction c amp eta x = NavierStokes.LocalizedMomentRepair.repair c.exponents c.lower c.upper (NavierStokes.OutgoingSchedule.debt c amp eta) x

theorem NavierStokes.OutgoingSchedule.correction_exact (c : Parameters) (amp : ℝ → ℝ) (eta : ℝ) (i : Fin 2) : ∫ (x : ℝ), x ^ c.exponents i * correction c amp eta x = debt c amp eta i

theorem NavierStokes.OutgoingSchedule.correction_contDiff_joint (c : Parameters) {amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) amp) : ContDiff ℝ ↑⊤ fun (p : ℝ × ℝ) => correction c amp p.2 (Real.exp p.1)

theorem NavierStokes.OutgoingSchedule.correction_zero_of_outside (c : Parameters) (amp : ℝ → ℝ) (eta x : ℝ) (hx : ∀ (i : Fin 2), x ∉ Set.Ioo (c.lower i) (c.upper i)) : correction c amp eta x = 0

theorem NavierStokes.OutgoingSchedule.correction_zero_early (c : Parameters) (amp : ℝ → ℝ) (eta : ℝ) {y : ℝ} (hy : y ≤ 0) : correction c amp eta (Real.exp y) = 0

theorem NavierStokes.OutgoingSchedule.correction_zero_late (c : Parameters) (amp : ℝ → ℝ) (eta : ℝ) {y : ℝ} (hy : c.pulseLength ≤ y) : correction c amp eta (Real.exp y) = 0

noncomputable def NavierStokes.OutgoingSchedule.pulseRatio (c : Parameters) (amp : ℝ → ℝ) (p : ℝ × ℝ) : ℝ

Pulse ratio, given by amp p.2 * mainPulse (c.lam * p.1) + correction c amp p.2 (Real.exp p.1).

Equations

• NavierStokes.OutgoingSchedule.pulseRatio c amp p = amp p.2 * NavierStokes.OutgoingSchedule.mainPulse (c.lam * p.1) + NavierStokes.OutgoingSchedule.correction c amp p.2 (Real.exp p.1)

theorem NavierStokes.OutgoingSchedule.pulseRatio_contDiff (c : Parameters) {amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) amp) : ContDiff ℝ (↑⊤) (pulseRatio c amp)

theorem NavierStokes.OutgoingSchedule.pulseRatio_zero_early (c : Parameters) (amp : ℝ → ℝ) (eta : ℝ) {y : ℝ} (hy : y ≤ 0) : pulseRatio c amp (y, eta) = 0

theorem NavierStokes.OutgoingSchedule.pulseRatio_zero_late (c : Parameters) (amp : ℝ → ℝ) (eta : ℝ) {y : ℝ} (hy : c.pulseLength ≤ y) : pulseRatio c amp (y, eta) = 0

noncomputable def NavierStokes.OutgoingSchedule.axial (c : Parameters) (amp : ℝ → ℝ) (p : ℝ × ℝ) : ℝ

Axial, given by initialAxial c.m p + angular c.P c.dropLength c.lam p * pulseRatio c amp (p.1 - c.pulseStart, p.2).

Equations

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

theorem NavierStokes.OutgoingSchedule.axial_contDiff (c : Parameters) {amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) amp) : ContDiff ℝ (↑⊤) (axial c amp)

theorem NavierStokes.OutgoingSchedule.axial_before_pulse (c : Parameters) (amp : ℝ → ℝ) (eta : ℝ) {y : ℝ} (hy : y ≤ c.pulseStart) : axial c amp (y, eta) = dropCoefficient c.m y * eta

theorem NavierStokes.OutgoingSchedule.axial_shaped_wait (c : Parameters) (amp : ℝ → ℝ) (eta : ℝ) {y : ℝ} (hy : c.holdStart ≤ y) (hy' : y ≤ c.pulseStart) : axial c amp (y, eta) = 0

theorem NavierStokes.OutgoingSchedule.axial_after_pulse (c : Parameters) (amp : ℝ → ℝ) (eta : ℝ) {y : ℝ} (hy : c.endpoint ≤ y) : axial c amp (y, eta) = 0

theorem NavierStokes.OutgoingSchedule.angular_shaped_wait (c : Parameters) (eta : ℝ) {y : ℝ} (hy : c.holdStart ≤ y) : angular c.P c.dropLength c.lam (y, eta) = radialAmplitude c.P c.dropLength c.lam c.holdStart * shape eta * Real.exp (-(1 / 2 + c.lam) * (y - c.holdStart))

Exact finite radial moments of the pulse

noncomputable def NavierStokes.OutgoingSchedule.radialPulse (c : Parameters) (amp : ℝ → ℝ) (eta x : ℝ) : ℝ

Radial pulse, given by amp eta * mainPulse (c.lam * Real.log x) + correction c amp eta x.

Equations

• NavierStokes.OutgoingSchedule.radialPulse c amp eta x = amp eta * NavierStokes.OutgoingSchedule.mainPulse (c.lam * Real.log x) + NavierStokes.OutgoingSchedule.correction c amp eta x

theorem NavierStokes.OutgoingSchedule.radialPulse_exp (c : Parameters) (amp : ℝ → ℝ) (eta y : ℝ) : radialPulse c amp eta (Real.exp y) = pulseRatio c amp (y, eta)

theorem NavierStokes.OutgoingSchedule.radialPulse_continuousOn (c : Parameters) (amp : ℝ → ℝ) (eta : ℝ) : ContinuousOn (radialPulse c amp eta) (Set.Ioi 0)

theorem NavierStokes.OutgoingSchedule.correction_interval_exact (c : Parameters) (amp : ℝ → ℝ) (eta : ℝ) (i : Fin 2) : ∫ (x : ℝ) in 1..Real.exp c.pulseLength, x ^ c.exponents i * correction c amp eta x = debt c amp eta i

theorem NavierStokes.OutgoingSchedule.pulse_moment_exact (c : Parameters) (amp : ℝ → ℝ) (eta : ℝ) (i : Fin 2) : ∫ (x : ℝ) in 1..Real.exp c.pulseLength, x ^ c.exponents i * radialPulse c amp eta x = -(prefixCoefficient c i * eta * (1 + eta ^ 2))

theorem NavierStokes.OutgoingSchedule.pulse_closes_prefix (c : Parameters) (amp : ℝ → ℝ) (eta : ℝ) : prefixM c * eta + momentScale c 0 * shape eta * ∫ (x : ℝ) in 1..Real.exp c.pulseLength, x ^ c.exponents 0 * radialPulse c amp eta x = 0 ∧ prefixJ c * eta * shape eta + momentScale c 1 * shape eta ^ 2 * ∫ (x : ℝ) in 1..Real.exp c.pulseLength, x ^ c.exponents 1 * radialPulse c amp eta x = 0

Reattaching the actual prefix gives zero total mass and angular moments. The two components have physical factors shape η and (shape η)^2.

The moments of the combined log-radius profile

theorem NavierStokes.OutgoingSchedule.exp_weight_substitution {R : ℝ → ℝ} (hR : ContinuousOn R (Set.Ioi 0)) (a B L : ℝ) : ∫ (y : ℝ) in B..B + L, Real.exp ((a + 1) * (y - B)) * R (Real.exp (y - B)) = ∫ (x : ℝ) in 1..Real.exp L, x ^ a * R x

theorem NavierStokes.OutgoingSchedule.axial_radial_contDiff (c : Parameters) (amp : ℝ → ℝ) (eta : ℝ) : ContDiff ℝ ↑⊤ fun (y : ℝ) => axial c amp (y, eta)

theorem NavierStokes.OutgoingSchedule.angular_pulse (c : Parameters) (eta : ℝ) {y : ℝ} (hy : c.pulseStart ≤ y) : angular c.P c.dropLength c.lam (y, eta) = pulseAmplitude c * shape eta * Real.exp (-(1 / 2 + c.lam) * (y - c.pulseStart))

theorem NavierStokes.OutgoingSchedule.axial_pulse (c : Parameters) (amp : ℝ → ℝ) (eta : ℝ) {y : ℝ} (hy : c.pulseStart ≤ y) : axial c amp (y, eta) = angular c.P c.dropLength c.lam (y, eta) * radialPulse c amp eta (Real.exp (y - c.pulseStart))

theorem NavierStokes.OutgoingSchedule.mass_integrand_pulse (c : Parameters) (amp : ℝ → ℝ) (eta : ℝ) {y : ℝ} (hy : c.pulseStart ≤ y) : Real.exp y * axial c amp (y, eta) = momentScale c 0 * shape eta * (Real.exp ((c.exponents 0 + 1) * (y - c.pulseStart)) * radialPulse c amp eta (Real.exp (y - c.pulseStart)))

theorem NavierStokes.OutgoingSchedule.angular_integrand_pulse (c : Parameters) (amp : ℝ → ℝ) (eta : ℝ) {y : ℝ} (hy : c.pulseStart ≤ y) : √2 * Real.exp (3 * y / 2) * angular c.P c.dropLength c.lam (y, eta) * axial c amp (y, eta) = momentScale c 1 * shape eta ^ 2 * (Real.exp ((c.exponents 1 + 1) * (y - c.pulseStart)) * radialPulse c amp eta (Real.exp (y - c.pulseStart)))

noncomputable def NavierStokes.OutgoingSchedule.massMoment (c : Parameters) (amp : ℝ → ℝ) (eta y : ℝ) : ℝ

X=e^y; the first term is the exact mass of the ideal prefix 0<X≤1.

Equations

• NavierStokes.OutgoingSchedule.massMoment c amp eta y = 4 * eta + ∫ (t : ℝ) in 0..y, Real.exp t * NavierStokes.OutgoingSchedule.axial c amp (t, eta)

noncomputable def NavierStokes.OutgoingSchedule.angularMoment (c : Parameters) (amp : ℝ → ℝ) (eta y : ℝ) : ℝ

The first term integrates U H over the ideal prefix 0<X≤1.

Equations

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

theorem NavierStokes.OutgoingSchedule.massMoment_at_pulseStart (c : Parameters) (amp : ℝ → ℝ) (eta : ℝ) : massMoment c amp eta c.pulseStart = prefixM c * eta

theorem NavierStokes.OutgoingSchedule.angularMoment_at_pulseStart (c : Parameters) (amp : ℝ → ℝ) (eta : ℝ) : angularMoment c amp eta c.pulseStart = prefixJ c * eta * shape eta

theorem NavierStokes.OutgoingSchedule.axial_reserved_band (c : Parameters) (amp : ℝ → ℝ) (eta y : ℝ) (hy : c.pulseStart - 25 ≤ y) (hy' : y ≤ c.pulseStart - 3) : axial c amp (y, eta) = 0

theorem NavierStokes.OutgoingSchedule.correction_zero_on_main_pulse (c : Parameters) (amp : ℝ → ℝ) (eta : ℝ) {y : ℝ} (hy : y ≤ 11 / c.lam) : correction c amp eta (Real.exp y) = 0

theorem NavierStokes.OutgoingSchedule.pulseRatio_on_main_pulse (c : Parameters) (amp : ℝ → ℝ) (eta : ℝ) {y : ℝ} (hy : y ≤ 11 / c.lam) : pulseRatio c amp (y, eta) = amp eta * mainPulse (c.lam * y)

theorem NavierStokes.OutgoingSchedule.axial_ideal (c : Parameters) (amp : ℝ → ℝ) (eta : ℝ) {y : ℝ} (hy : y ≤ 0) : axial c amp (y, eta) = 4 * eta

theorem NavierStokes.OutgoingSchedule.axial_drop (c : Parameters) (amp : ℝ → ℝ) (eta : ℝ) {t : ℝ} (ht : 0 ≤ t) (ht' : t ≤ c.dropLength) : axial c amp (1 + t, eta) = 4 * (1 - sigma (Real.log (1 + t) / c.m)) * eta

theorem NavierStokes.OutgoingSchedule.radialAmplitude_drop {dropLength lam y P : ℝ} (hy : 1 ≤ y) (hy' : y ≤ dropLength + 1) : radialAmplitude P dropLength lam y = radialAmplitude P dropLength lam 1 * Real.exp (-(y - 1) / 2)

theorem NavierStokes.OutgoingSchedule.ideal_mass_prefix_integral (eta : ℝ) : ∫ (_x : ℝ) in 0..1, 4 * eta = 4 * eta

theorem NavierStokes.OutgoingSchedule.ideal_angular_prefix_integral (P eta : ℝ) : ∫ (x : ℝ) in 0..1, 4 * eta * √2 * P * shape eta * x ^ (3 / 5) = 5 / 2 * √2 * P * eta * shape eta

theorem NavierStokes.OutgoingSchedule.massMoment_endpoint (c : Parameters) (amp : ℝ → ℝ) (eta : ℝ) : massMoment c amp eta c.endpoint = 0

Both moments are the actual log-coordinate integrals of the combined fields.

theorem NavierStokes.OutgoingSchedule.angularMoment_endpoint (c : Parameters) (amp : ℝ → ℝ) (eta : ℝ) : angularMoment c amp eta c.endpoint = 0

theorem NavierStokes.OutgoingSchedule.exact_axial_moments (c : Parameters) (amp : ℝ → ℝ) (eta : ℝ) : massMoment c amp eta c.endpoint = 0 ∧ angularMoment c amp eta c.endpoint = 0

The constructed profiles satisfy both endpoint equations for every parameter value.

theorem NavierStokes.OutgoingSchedule.massMoment_after_pulse (c : Parameters) (amp : ℝ → ℝ) (eta : ℝ) {y : ℝ} (hy : c.endpoint ≤ y) : massMoment c amp eta y = 0

theorem NavierStokes.OutgoingSchedule.angularMoment_after_pulse (c : Parameters) (amp : ℝ → ℝ) (eta : ℝ) {y : ℝ} (hy : c.endpoint ≤ y) : angularMoment c amp eta y = 0

noncomputable def NavierStokes.OutgoingSchedule.paperParameters (P m lam : ℝ) (hP : 0 < P) (hm : 0 < m) (hlam : 0 < lam) (hlam' : lam < 1 / 10) : Parameters

The manuscript's precise shaped-wait duration is a valid instance.

Equations

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

theorem NavierStokes.OutgoingSchedule.constructed_core (c : Parameters) {amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) amp) : ContDiff ℝ (↑⊤) (angular c.P c.dropLength c.lam) ∧ ContDiff ℝ (↑⊤) (axial c amp) ∧ (∀ (p : ℝ × ℝ), 0 < angular c.P c.dropLength c.lam p) ∧ (∀ (eta y : ℝ), c.endpoint ≤ y → axial c amp (y, eta) = 0 ∧ massMoment c amp eta y = 0 ∧ angularMoment c amp eta y = 0) ∧ ∀ (eta y : ℝ), c.holdStart ≤ y → y ≤ c.pulseStart → axial c amp (y, eta) = 0 ∧ angular c.P c.dropLength c.lam (y, eta) = radialAmplitude c.P c.dropLength c.lam c.holdStart * shape eta * Real.exp (-(1 / 2 + c.lam) * (y - c.holdStart))

A compact interface for using the constructed profiles in later stages.