Actual pulse energy and its scalar amplitude

The pulse constant is the integral of the constructed smooth pulse from OutgoingSchedule, rather than an abstract coefficient satisfying assumed bounds. All energy coefficients below refer to the actual outgoing profiles.

Quantitative bounds for the constructed outgoing pulse

All profiles and moments in this file are those of OutgoingSchedule and LocalizedMomentRepair. In particular the correction bumps are not an additional choice. Their log-coordinate translates are identified below.

theorem NavierStokes.OutgoingPulseBounds.slope_bounds (c : OutgoingSchedule.Parameters) (y : ℝ) : -c.lam ≤ OutgoingSchedule.slope c.dropLength c.lam y ∧ OutgoingSchedule.slope c.dropLength c.lam y ≤ 3 / 5

theorem NavierStokes.OutgoingPulseBounds.logAmplitude_bounds (c : OutgoingSchedule.Parameters) {y : ℝ} (hy : 0 ≤ y) : -y ≤ OutgoingSchedule.logAmplitude c.dropLength c.lam y ∧ OutgoingSchedule.logAmplitude c.dropLength c.lam y ≤ y

theorem NavierStokes.OutgoingPulseBounds.radialAmplitude_bounds (c : OutgoingSchedule.Parameters) {y : ℝ} (hy : 0 ≤ y) : c.P * Real.exp (-y) ≤ OutgoingSchedule.radialAmplitude c.P c.dropLength c.lam y ∧ OutgoingSchedule.radialAmplitude c.P c.dropLength c.lam y ≤ c.P * Real.exp y

theorem NavierStokes.OutgoingPulseBounds.integral_stops {g : ℝ → ℝ} (hg : Continuous g) {a b : ℝ} (hab : a ≤ b) (hz : ∀ (t : ℝ), a ≤ t → g t = 0) : ∫ (t : ℝ) in 0..b, g t = ∫ (t : ℝ) in 0..a, g t

theorem NavierStokes.OutgoingPulseBounds.dropEnd_le_pulseStart (c : OutgoingSchedule.Parameters) : Real.exp c.m ≤ c.pulseStart

theorem NavierStokes.OutgoingPulseBounds.prefixM_fixed_interval (c : OutgoingSchedule.Parameters) : OutgoingSchedule.prefixM c = 4 + ∫ (y : ℝ) in 0..Real.exp c.m, Real.exp y * OutgoingSchedule.dropCoefficient c.m y

theorem NavierStokes.OutgoingPulseBounds.prefixJ_fixed_interval (c : OutgoingSchedule.Parameters) : OutgoingSchedule.prefixJ c = 5 / 2 * √2 * c.P + ∫ (y : ℝ) in 0..Real.exp c.m, √2 * Real.exp (3 * y / 2) * OutgoingSchedule.radialAmplitude c.P c.dropLength c.lam y * OutgoingSchedule.dropCoefficient c.m y

theorem NavierStokes.OutgoingPulseBounds.prefixM_bounds (c : OutgoingSchedule.Parameters) : 0 ≤ OutgoingSchedule.prefixM c ∧ OutgoingSchedule.prefixM c ≤ 4 + 4 * Real.exp c.m * Real.exp (Real.exp c.m)

theorem NavierStokes.OutgoingPulseBounds.prefixJ_bounds (c : OutgoingSchedule.Parameters) : 0 ≤ OutgoingSchedule.prefixJ c ∧ OutgoingSchedule.prefixJ c ≤ 5 / 2 * √2 * c.P + 4 * √2 * c.P * Real.exp c.m * Real.exp (3 * Real.exp c.m)

Decay along the explicitly timed shaped wait

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

Beta, given by c.exponents i + 1.

Equations

• NavierStokes.OutgoingPulseBounds.beta c i = c.exponents i + 1

theorem NavierStokes.OutgoingPulseBounds.beta_bounds (c : OutgoingSchedule.Parameters) (i : Fin 2) : 0 < beta c i ∧ beta c i ≤ 1 / 2

theorem NavierStokes.OutgoingPulseBounds.beta_small_bounds (c : OutgoingSchedule.Parameters) (hc : c.lam ≤ 1 / 120) (i : Fin 2) : 2 / 5 ≤ beta c i ∧ 29 ≤ 60 * beta c i

noncomputable def NavierStokes.OutgoingPulseBounds.holdAmplitude (c : OutgoingSchedule.Parameters) : ℝ

Hold amplitude, given by radialAmplitude c.P c.dropLength c.lam c.holdStart.

Equations

• NavierStokes.OutgoingPulseBounds.holdAmplitude c = NavierStokes.OutgoingSchedule.radialAmplitude c.P c.dropLength c.lam c.holdStart

theorem NavierStokes.OutgoingPulseBounds.holdAmplitude_pos (c : OutgoingSchedule.Parameters) : 0 < holdAmplitude c

theorem NavierStokes.OutgoingPulseBounds.pulseAmplitude_split (c : OutgoingSchedule.Parameters) : OutgoingSchedule.pulseAmplitude c = holdAmplitude c * Real.exp (-(1 / 2 + c.lam) * c.wait)

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

Hold scale, with branches according to i = 0.

Equations

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

noncomputable def NavierStokes.OutgoingPulseBounds.scaleFloor (P m : ℝ) (i : Fin 2) : ℝ

Scale floor, with branches according to i = 0.

Equations

• NavierStokes.OutgoingPulseBounds.scaleFloor P m i = if i = 0 then P else √2 * P ^ 2 * Real.exp (-(Real.exp m + 12) / 2)

theorem NavierStokes.OutgoingPulseBounds.scaleFloor_pos {P : ℝ} (hP : 0 < P) (m : ℝ) (i : Fin 2) : 0 < scaleFloor P m i

theorem NavierStokes.OutgoingPulseBounds.holdScale_lower (c : OutgoingSchedule.Parameters) (i : Fin 2) : scaleFloor c.P c.m i ≤ holdScale c i

theorem NavierStokes.OutgoingPulseBounds.momentScale_split (c : OutgoingSchedule.Parameters) (i : Fin 2) : OutgoingSchedule.momentScale c i = holdScale c i * Real.exp (beta c i * c.wait)

theorem NavierStokes.OutgoingPulseBounds.exp_log_inverse_nat {lam : ℝ} (hlam : 0 < lam) (n : ℕ) : Real.exp (-↑n * Real.log (1 / lam)) = lam ^ n

theorem NavierStokes.OutgoingPulseBounds.wait_decay (c : OutgoingSchedule.Parameters) (hwait : c.wait = 60 * Real.log (1 / c.lam)) (hsmall : c.lam ≤ 1 / 120) (i : Fin 2) : Real.exp (-(beta c i * c.wait)) ≤ c.lam ^ 29

theorem NavierStokes.OutgoingPulseBounds.pulseAmplitude_small (c : OutgoingSchedule.Parameters) (hwait : c.wait = 60 * Real.log (1 / c.lam)) : OutgoingSchedule.pulseAmplitude c ≤ c.P * Real.exp (Real.exp c.m + 12) * c.lam ^ 30

noncomputable def NavierStokes.OutgoingPulseBounds.prefixNumeratorBound (P m : ℝ) (i : Fin 2) : ℝ

Prefix numerator bound, with branches according to i = 0.

Equations

• NavierStokes.OutgoingPulseBounds.prefixNumeratorBound P m i = if i = 0 then 4 + 4 * Real.exp m * Real.exp (Real.exp m) else 5 / 2 * √2 * P + 4 * √2 * P * Real.exp m * Real.exp (3 * Real.exp m)

noncomputable def NavierStokes.OutgoingPulseBounds.prefixBound (P m : ℝ) (i : Fin 2) : ℝ

Prefix bound, given by prefixNumeratorBound P m i / scaleFloor P m i.

Equations

• NavierStokes.OutgoingPulseBounds.prefixBound P m i = NavierStokes.OutgoingPulseBounds.prefixNumeratorBound P m i / NavierStokes.OutgoingPulseBounds.scaleFloor P m i

theorem NavierStokes.OutgoingPulseBounds.prefixNumeratorBound_pos {P : ℝ} (hP : 0 < P) (m : ℝ) (i : Fin 2) : 0 < prefixNumeratorBound P m i

theorem NavierStokes.OutgoingPulseBounds.prefixBound_pos {P : ℝ} (hP : 0 < P) (m : ℝ) (i : Fin 2) : 0 < prefixBound P m i

theorem NavierStokes.OutgoingPulseBounds.prefixCoefficient_nonneg (c : OutgoingSchedule.Parameters) (i : Fin 2) : 0 ≤ OutgoingSchedule.prefixCoefficient c i

theorem NavierStokes.OutgoingPulseBounds.prefixCoefficient_decay (c : OutgoingSchedule.Parameters) (i : Fin 2) : OutgoingSchedule.prefixCoefficient c i ≤ prefixBound c.P c.m i * Real.exp (-(beta c i * c.wait))

theorem NavierStokes.OutgoingPulseBounds.prefixCoefficient_small (c : OutgoingSchedule.Parameters) (hwait : c.wait = 60 * Real.log (1 / c.lam)) (hsmall : c.lam ≤ 1 / 120) (i : Fin 2) : |OutgoingSchedule.prefixCoefficient c i| ≤ prefixBound c.P c.m i * c.lam ^ 29

The mass average is divided by the actual angular profile, including its parameter shape. These bounds therefore include the shape's first derivative.

noncomputable def NavierStokes.OutgoingPulseBounds.parameterPolynomial (eta : ℝ) : ℝ

Parameter polynomial, given by eta * (1 + eta ^ 2).

Equations

• NavierStokes.OutgoingPulseBounds.parameterPolynomial eta = eta * (1 + eta ^ 2)

theorem NavierStokes.OutgoingPulseBounds.parameterPolynomial_bound {eta : ℝ} (heta : |eta| ≤ 1) : |parameterPolynomial eta| ≤ 2

theorem NavierStokes.OutgoingPulseBounds.parameterPolynomial_hasDerivAt (eta : ℝ) : HasDerivAt parameterPolynomial (1 + 3 * eta ^ 2) eta

theorem NavierStokes.OutgoingPulseBounds.parameterPolynomial_derivative_bound {eta : ℝ} (heta : |eta| ≤ 1) : |deriv parameterPolynomial eta| ≤ 4

theorem NavierStokes.OutgoingPulseBounds.normalized_mass_prefix (c : OutgoingSchedule.Parameters) (amp : ℝ → ℝ) (eta : ℝ) : OutgoingSchedule.massMoment c amp eta c.pulseStart / (Real.exp c.pulseStart * OutgoingSchedule.angular c.P c.dropLength c.lam (c.pulseStart, eta)) = OutgoingSchedule.prefixCoefficient c 0 * parameterPolynomial eta

theorem NavierStokes.OutgoingPulseBounds.normalized_mass_prefix_small (c : OutgoingSchedule.Parameters) (hwait : c.wait = 60 * Real.log (1 / c.lam)) (hsmall : c.lam ≤ 1 / 120) (amp : ℝ → ℝ) {eta : ℝ} (heta : |eta| ≤ 1) : |OutgoingSchedule.massMoment c amp eta c.pulseStart / (Real.exp c.pulseStart * OutgoingSchedule.angular c.P c.dropLength c.lam (c.pulseStart, eta))| ≤ 2 * prefixBound c.P c.m 0 * c.lam ^ 29

The actual bump is one fixed template in log coordinates

noncomputable def NavierStokes.OutgoingPulseBounds.templateLower : ℝ

Template lower, given by Real.exp (-(3 / 20 : ℝ)).

Equations

• NavierStokes.OutgoingPulseBounds.templateLower = Real.exp (-(3 / 20))

noncomputable def NavierStokes.OutgoingPulseBounds.templateUpper : ℝ

Template upper, given by Real.exp (3 / 20 : ℝ).

Equations

• NavierStokes.OutgoingPulseBounds.templateUpper = Real.exp (3 / 20)

noncomputable def NavierStokes.OutgoingPulseBounds.radialTemplate : ℝ → ℝ

Radial template, given by LocalizedMomentRepair.bump templateLower templateUpper.

Equations

• NavierStokes.OutgoingPulseBounds.radialTemplate = NavierStokes.LocalizedMomentRepair.bump NavierStokes.OutgoingPulseBounds.templateLower NavierStokes.OutgoingPulseBounds.templateUpper

noncomputable def NavierStokes.OutgoingPulseBounds.logTemplate (z : ℝ) : ℝ

Log template, given by radialTemplate (Real.exp z).

Equations

• NavierStokes.OutgoingPulseBounds.logTemplate z = NavierStokes.OutgoingPulseBounds.radialTemplate (Real.exp z)

theorem NavierStokes.OutgoingPulseBounds.templateLower_pos : 0 < templateLower

theorem NavierStokes.OutgoingPulseBounds.templateLower_lt_upper : templateLower < templateUpper

theorem NavierStokes.OutgoingPulseBounds.radialTemplate_contDiff : ContDiff ℝ (↑⊤) radialTemplate

theorem NavierStokes.OutgoingPulseBounds.radialTemplate_hasCompactSupport : HasCompactSupport radialTemplate

theorem NavierStokes.OutgoingPulseBounds.radialTemplate_nonneg (x : ℝ) : 0 ≤ radialTemplate x

theorem NavierStokes.OutgoingPulseBounds.radialTemplate_support (x : ℝ) (hx : radialTemplate x ≠ 0) : templateLower < x ∧ x < templateUpper

theorem NavierStokes.OutgoingPulseBounds.logTemplate_contDiff : ContDiff ℝ (↑⊤) logTemplate

theorem NavierStokes.OutgoingPulseBounds.logTemplate_support : Function.support logTemplate ⊆ Set.Icc (-1) 1

theorem NavierStokes.OutgoingPulseBounds.logTemplate_hasCompactSupport : HasCompactSupport logTemplate

theorem NavierStokes.OutgoingPulseBounds.logTemplate_jet_bound (k : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (y : ℝ), |iteratedDeriv k logTemplate y| ≤ C

theorem NavierStokes.OutgoingPulseBounds.bump_scale {k : ℝ} (hk : k ≠ 0) (l u x : ℝ) : LocalizedMomentRepair.bump (k * l) (k * u) (k * x) = LocalizedMomentRepair.bump l u x

noncomputable def NavierStokes.OutgoingPulseBounds.center (c : OutgoingSchedule.Parameters) (j : Fin 2) : ℝ

Center, given by c.pulseLength - if j = 0 then 3 else 1.

Equations

• NavierStokes.OutgoingPulseBounds.center c j = c.pulseLength - if j = 0 then 3 else 1

theorem NavierStokes.OutgoingPulseBounds.lower_scale (c : OutgoingSchedule.Parameters) (j : Fin 2) : c.lower j = Real.exp (center c j) * templateLower

theorem NavierStokes.OutgoingPulseBounds.upper_scale (c : OutgoingSchedule.Parameters) (j : Fin 2) : c.upper j = Real.exp (center c j) * templateUpper

theorem NavierStokes.OutgoingPulseBounds.bump_log_translate (c : OutgoingSchedule.Parameters) (j : Fin 2) (y : ℝ) : LocalizedMomentRepair.bump (c.lower j) (c.upper j) (Real.exp y) = logTemplate (y - center c j)

noncomputable def NavierStokes.OutgoingPulseBounds.templateMass : ℝ

Template mass, given by ∫ x, radialTemplate x.

Equations

• NavierStokes.OutgoingPulseBounds.templateMass = ∫ (x : ℝ), NavierStokes.OutgoingPulseBounds.radialTemplate x

noncomputable def NavierStokes.OutgoingPulseBounds.rowMoment (a : ℝ) : ℝ

Row moment, given by ∫ x, x ^ a * radialTemplate x.

Equations

• NavierStokes.OutgoingPulseBounds.rowMoment a = ∫ (x : ℝ), x ^ a * NavierStokes.OutgoingPulseBounds.radialTemplate x

noncomputable def NavierStokes.OutgoingPulseBounds.rowFloor : ℝ

Row floor, given by Real.exp (-1) * templateMass.

Equations

• NavierStokes.OutgoingPulseBounds.rowFloor = Real.exp (-1) * NavierStokes.OutgoingPulseBounds.templateMass

theorem NavierStokes.OutgoingPulseBounds.templateMass_pos : 0 < templateMass

theorem NavierStokes.OutgoingPulseBounds.rowFloor_pos : 0 < rowFloor

theorem NavierStokes.OutgoingPulseBounds.rowMoment_integrable (a : ℝ) : MeasureTheory.Integrable (fun (x : ℝ) => x ^ a * radialTemplate x) MeasureTheory.volume

theorem NavierStokes.OutgoingPulseBounds.rowMoment_bounds {a : ℝ} (ha : -1 ≤ a) (ha' : a ≤ 0) : rowFloor ≤ rowMoment a ∧ rowMoment a ≤ Real.exp 1 * templateMass

theorem NavierStokes.OutgoingPulseBounds.power_bump_integral_scale (a : ℝ) {k l u : ℝ} (hk : 0 < k) (hl : 0 < l) (hlu : l < u) : ∫ (t : ℝ), t ^ a * LocalizedMomentRepair.bump (k * l) (k * u) t = k * k ^ a * ∫ (t : ℝ), t ^ a * LocalizedMomentRepair.bump l u t

theorem NavierStokes.OutgoingPulseBounds.actual_matrix_entry (c : OutgoingSchedule.Parameters) (i j : Fin 2) : LocalizedMomentRepair.matrix c.exponents c.lower c.upper i j = rowMoment (c.exponents i) * Real.exp (beta c i * center c j)

noncomputable def NavierStokes.OutgoingPulseBounds.normalizedMatrix (c : OutgoingSchedule.Parameters) : Matrix (Fin 2) (Fin 2) ℝ

The actual moment matrix, with each row normalized at the first center.

Equations

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

theorem NavierStokes.OutgoingPulseBounds.normalizedMatrix_entry (c : OutgoingSchedule.Parameters) (i j : Fin 2) : normalizedMatrix c i j = rowMoment (c.exponents i) * if j = 0 then 1 else Real.exp (2 * beta c i)

theorem NavierStokes.OutgoingPulseBounds.rowMoment_lower (c : OutgoingSchedule.Parameters) (i : Fin 2) : rowFloor ≤ rowMoment (c.exponents i)

theorem NavierStokes.OutgoingPulseBounds.rowMoment_pos (c : OutgoingSchedule.Parameters) (i : Fin 2) : 0 < rowMoment (c.exponents i)

theorem NavierStokes.OutgoingPulseBounds.separation_exponential_bounds (c : OutgoingSchedule.Parameters) (i : Fin 2) : 1 ≤ Real.exp (2 * beta c i) ∧ Real.exp (2 * beta c i) ≤ Real.exp 1

theorem NavierStokes.OutgoingPulseBounds.separation_exponential_gap (c : OutgoingSchedule.Parameters) : 2 * c.lam ≤ Real.exp (2 * beta c 0) - Real.exp (2 * beta c 1)

theorem NavierStokes.OutgoingPulseBounds.normalizedMatrix_det_ne_zero (c : OutgoingSchedule.Parameters) : (normalizedMatrix c).det ≠ 0

noncomputable def NavierStokes.OutgoingPulseBounds.inverseBound : ℝ

A uniform inverse estimate from the actual exponential column separation.

Equations

• NavierStokes.OutgoingPulseBounds.inverseBound = (1 + Real.exp 1) / NavierStokes.OutgoingPulseBounds.rowFloor

theorem NavierStokes.OutgoingPulseBounds.inverseBound_pos : 0 < inverseBound

theorem NavierStokes.OutgoingPulseBounds.two_row_solution_bound {k lam A0 A1 r0 r1 x0 x1 d0 d1 : ℝ} (hk : 0 < k) (hlam : 0 < lam) (hlam' : lam ≤ 1) (hA0 : k ≤ A0) (hA1 : k ≤ A1) (hr0 : 0 ≤ r0) (hr0' : r0 ≤ Real.exp 1) (hgap : lam ≤ r0 - r1) (h0 : A0 * (x0 + r0 * x1) = d0) (h1 : A1 * (x0 + r1 * x1) = d1) : lam * |x0| ≤ (1 + Real.exp 1) / k * (|d0| + |d1|) ∧ lam * |x1| ≤ (1 + Real.exp 1) / k * (|d0| + |d1|)

theorem NavierStokes.OutgoingPulseBounds.normalized_solution_bound (c : OutgoingSchedule.Parameters) (x d : Fin 2 → ℝ) (h : (normalizedMatrix c).mulVec x = d) (j : Fin 2) : c.lam * |x j| ≤ inverseBound * (|d 0| + |d 1|)

theorem NavierStokes.OutgoingPulseBounds.normalized_inverse_entry_bound (c : OutgoingSchedule.Parameters) (i j : Fin 2) : c.lam * |(normalizedMatrix c)⁻¹ i j| ≤ inverseBound

theorem NavierStokes.OutgoingPulseBounds.normalized_inverse_norm_bound (c : OutgoingSchedule.Parameters) : c.lam * ‖fun (i j : Fin 2) => (normalizedMatrix c)⁻¹ i j‖ ≤ inverseBound

noncomputable def NavierStokes.OutgoingPulseBounds.normalizedDebt (c : OutgoingSchedule.Parameters) (d : Fin 2 → ℝ) (i : Fin 2) : ℝ

Normalized debt, given by Real.exp (-(beta c i * center c 0)) * d i.

Equations

• NavierStokes.OutgoingPulseBounds.normalizedDebt c d i = Real.exp (-(NavierStokes.OutgoingPulseBounds.beta c i * NavierStokes.OutgoingPulseBounds.center c 0)) * d i

theorem NavierStokes.OutgoingPulseBounds.actual_coefficients_normalized_system (c : OutgoingSchedule.Parameters) (d : Fin 2 → ℝ) : (normalizedMatrix c).mulVec (LocalizedMomentRepair.coefficients c.exponents c.lower c.upper d) = normalizedDebt c d

theorem NavierStokes.OutgoingPulseBounds.actual_coefficients_bound (c : OutgoingSchedule.Parameters) (d : Fin 2 → ℝ) (j : Fin 2) : c.lam * |LocalizedMomentRepair.coefficients c.exponents c.lower c.upper d j| ≤ inverseBound * (|normalizedDebt c d 0| + |normalizedDebt c d 1|)

Actual normalized debts

theorem NavierStokes.OutgoingPulseBounds.mainPulse_hasCompactSupport : HasCompactSupport OutgoingSchedule.mainPulse

theorem NavierStokes.OutgoingPulseBounds.exists_mainPulse_bound : ∃ (C : ℝ), 0 < C ∧ ∀ (z : ℝ), |OutgoingSchedule.mainPulse z| ≤ C

noncomputable def NavierStokes.OutgoingPulseBounds.mainBound : ℝ

Main bound, given by Classical.choose exists_mainPulse_bound.

Equations

• NavierStokes.OutgoingPulseBounds.mainBound = Classical.choose NavierStokes.OutgoingPulseBounds.exists_mainPulse_bound

theorem NavierStokes.OutgoingPulseBounds.mainBound_pos : 0 < mainBound

theorem NavierStokes.OutgoingPulseBounds.mainPulse_abs_le (z : ℝ) : |OutgoingSchedule.mainPulse z| ≤ mainBound

theorem NavierStokes.OutgoingPulseBounds.mainMoment_log (c : OutgoingSchedule.Parameters) (i : Fin 2) : OutgoingSchedule.mainMoment c i = ∫ (y : ℝ) in 0..c.pulseLength, Real.exp (beta c i * y) * OutgoingSchedule.mainPulse (c.lam * y)

theorem NavierStokes.OutgoingPulseBounds.mainMoment_log_short (c : OutgoingSchedule.Parameters) (i : Fin 2) : OutgoingSchedule.mainMoment c i = ∫ (y : ℝ) in 0..11 / c.lam, Real.exp (beta c i * y) * OutgoingSchedule.mainPulse (c.lam * y)

theorem NavierStokes.OutgoingPulseBounds.center_gap_bound (c : OutgoingSchedule.Parameters) (hsmall : c.lam ≤ 1 / 120) (i : Fin 2) : 1 / (2 * c.lam) ≤ beta c i * (center c 0 - 11 / c.lam)

theorem NavierStokes.OutgoingPulseBounds.normalized_mainMoment_bound (c : OutgoingSchedule.Parameters) (hsmall : c.lam ≤ 1 / 120) (i : Fin 2) : |Real.exp (-(beta c i * center c 0)) * OutgoingSchedule.mainMoment c i| ≤ 11 * mainBound / c.lam * Real.exp (-(1 / (2 * c.lam)))

theorem NavierStokes.OutgoingPulseBounds.prefixCoefficient_le_bound (c : OutgoingSchedule.Parameters) (i : Fin 2) : |OutgoingSchedule.prefixCoefficient c i| ≤ prefixBound c.P c.m i

theorem NavierStokes.OutgoingPulseBounds.normalized_prefixCoefficient_bound (c : OutgoingSchedule.Parameters) (hsmall : c.lam ≤ 1 / 120) (i : Fin 2) : |Real.exp (-(beta c i * center c 0)) * OutgoingSchedule.prefixCoefficient c i| ≤ prefixBound c.P c.m i * Real.exp (-(1 / (2 * c.lam)))

noncomputable def NavierStokes.OutgoingPulseBounds.affineDebt (c : OutgoingSchedule.Parameters) (q A : ℝ) (i : Fin 2) : ℝ

Affine debt, given by -(q * prefixCoefficient c i + A * mainMoment c i).

Equations

• NavierStokes.OutgoingPulseBounds.affineDebt c q A i = -(q * NavierStokes.OutgoingSchedule.prefixCoefficient c i + A * NavierStokes.OutgoingSchedule.mainMoment c i)

noncomputable def NavierStokes.OutgoingPulseBounds.affineCoefficients (c : OutgoingSchedule.Parameters) (q A : ℝ) : Fin 2 → ℝ

Affine coefficients, given by LocalizedMomentRepair.coefficients c.exponents c.lower c.upper (affineDebt c q A).

Equations

• NavierStokes.OutgoingPulseBounds.affineCoefficients c q A = NavierStokes.LocalizedMomentRepair.coefficients c.exponents c.lower c.upper (NavierStokes.OutgoingPulseBounds.affineDebt c q A)

noncomputable def NavierStokes.OutgoingPulseBounds.debtBound (P m : ℝ) (i : Fin 2) : ℝ

Debt bound, given by prefixBound P m i + 11 * mainBound.

Equations

• NavierStokes.OutgoingPulseBounds.debtBound P m i = NavierStokes.OutgoingPulseBounds.prefixBound P m i + 11 * NavierStokes.OutgoingPulseBounds.mainBound

theorem NavierStokes.OutgoingPulseBounds.debtBound_pos {P : ℝ} (hP : 0 < P) (m : ℝ) (i : Fin 2) : 0 < debtBound P m i

theorem NavierStokes.OutgoingPulseBounds.affineDebt_normalized_bound (c : OutgoingSchedule.Parameters) (hsmall : c.lam ≤ 1 / 120) (q A : ℝ) (i : Fin 2) : |normalizedDebt c (affineDebt c q A) i| ≤ debtBound c.P c.m i / c.lam * Real.exp (-(1 / (2 * c.lam))) * (|q| + |A|)

theorem NavierStokes.OutgoingPulseBounds.inverse_square_exp_absorption {lam : ℝ} (hlam : 0 < lam) : Real.exp (-(1 / (2 * lam))) / lam ^ 2 ≤ 64 * Real.exp (-(1 / (4 * lam)))

noncomputable def NavierStokes.OutgoingPulseBounds.coefficientBound (P m : ℝ) : ℝ

Coefficient bound, given by 64 * inverseBound * (debtBound P m 0 + debtBound P m 1).

Equations

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

theorem NavierStokes.OutgoingPulseBounds.coefficientBound_pos {P : ℝ} (hP : 0 < P) (m : ℝ) : 0 < coefficientBound P m

theorem NavierStokes.OutgoingPulseBounds.affineCoefficients_exp_bound (c : OutgoingSchedule.Parameters) (hsmall : c.lam ≤ 1 / 120) (q A : ℝ) (j : Fin 2) : |affineCoefficients c q A j| ≤ coefficientBound c.P c.m * Real.exp (-(1 / (4 * c.lam))) * (|q| + |A|)

theorem NavierStokes.OutgoingPulseBounds.pulse_coefficients_exp_bound (c : OutgoingSchedule.Parameters) (hsmall : c.lam ≤ 1 / 120) (amp : ℝ → ℝ) {eta : ℝ} (heta : |eta| ≤ 1) (j : Fin 2) : |LocalizedMomentRepair.coefficients c.exponents c.lower c.upper (OutgoingSchedule.debt c amp eta) j| ≤ 2 * coefficientBound c.P c.m * Real.exp (-(1 / (4 * c.lam))) * (1 + |amp eta|)

Fixed radial jets and first parameter derivatives

theorem NavierStokes.OutgoingPulseBounds.affineCoefficients_decomposition (c : OutgoingSchedule.Parameters) (q A : ℝ) (j : Fin 2) : affineCoefficients c q A j = q * affineCoefficients c 1 0 j + A * affineCoefficients c 0 1 j

theorem NavierStokes.OutgoingPulseBounds.debt_eq_affine (c : OutgoingSchedule.Parameters) (amp : ℝ → ℝ) (eta : ℝ) : OutgoingSchedule.debt c amp eta = affineDebt c (parameterPolynomial eta) (amp eta)

theorem NavierStokes.OutgoingPulseBounds.pulse_coefficients_hasDerivAt (c : OutgoingSchedule.Parameters) {amp : ℝ → ℝ} {eta amp' : ℝ} (ha : HasDerivAt amp amp' eta) (j : Fin 2) : HasDerivAt (fun (t : ℝ) => LocalizedMomentRepair.coefficients c.exponents c.lower c.upper (OutgoingSchedule.debt c amp t) j) (affineCoefficients c (1 + 3 * eta ^ 2) amp' j) eta

noncomputable def NavierStokes.OutgoingPulseBounds.affineProfile (c : OutgoingSchedule.Parameters) (q A y : ℝ) : ℝ

Affine profile, given by ∑ j : Fin 2, affineCoefficients c q A j * logTemplate (y - center c j).

Equations

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

theorem NavierStokes.OutgoingPulseBounds.affineProfile_contDiff (c : OutgoingSchedule.Parameters) (q A : ℝ) : ContDiff ℝ (↑⊤) (affineProfile c q A)

theorem NavierStokes.OutgoingPulseBounds.correction_log_eq_affineProfile (c : OutgoingSchedule.Parameters) (amp : ℝ → ℝ) (eta y : ℝ) : OutgoingSchedule.correction c amp eta (Real.exp y) = affineProfile c (parameterPolynomial eta) (amp eta) y

theorem NavierStokes.OutgoingPulseBounds.affineProfile_jet_formula (c : OutgoingSchedule.Parameters) (q A : ℝ) (k : ℕ) (y : ℝ) : iteratedDeriv k (affineProfile c q A) y = ∑ j : Fin 2, affineCoefficients c q A j * iteratedDeriv k logTemplate (y - center c j)

noncomputable def NavierStokes.OutgoingPulseBounds.templateJetBound (k : ℕ) : ℝ

Template jet bound, given by 1 + Classical.choose (logTemplate_jet_bound k).

Equations

• NavierStokes.OutgoingPulseBounds.templateJetBound k = 1 + Classical.choose ⋯

theorem NavierStokes.OutgoingPulseBounds.templateJetBound_pos (k : ℕ) : 0 < templateJetBound k

theorem NavierStokes.OutgoingPulseBounds.logTemplate_jet_le (k : ℕ) (y : ℝ) : |iteratedDeriv k logTemplate y| ≤ templateJetBound k

noncomputable def NavierStokes.OutgoingPulseBounds.correctionJetBound (P m : ℝ) (k : ℕ) : ℝ

Correction jet bound, given by 2 * coefficientBound P m * templateJetBound k.

Equations

• NavierStokes.OutgoingPulseBounds.correctionJetBound P m k = 2 * NavierStokes.OutgoingPulseBounds.coefficientBound P m * NavierStokes.OutgoingPulseBounds.templateJetBound k

theorem NavierStokes.OutgoingPulseBounds.correctionJetBound_pos {P : ℝ} (hP : 0 < P) (m : ℝ) (k : ℕ) : 0 < correctionJetBound P m k

theorem NavierStokes.OutgoingPulseBounds.affineProfile_jet_bound (c : OutgoingSchedule.Parameters) (hsmall : c.lam ≤ 1 / 120) (q A : ℝ) (k : ℕ) (y : ℝ) : |iteratedDeriv k (affineProfile c q A) y| ≤ correctionJetBound c.P c.m k * Real.exp (-(1 / (4 * c.lam))) * (|q| + |A|)

theorem NavierStokes.OutgoingPulseBounds.affineProfile_jet_decomposition (c : OutgoingSchedule.Parameters) (q A : ℝ) (k : ℕ) (y : ℝ) : iteratedDeriv k (affineProfile c q A) y = q * iteratedDeriv k (affineProfile c 1 0) y + A * iteratedDeriv k (affineProfile c 0 1) y

noncomputable def NavierStokes.OutgoingPulseBounds.correctionJet (c : OutgoingSchedule.Parameters) (amp : ℝ → ℝ) (k : ℕ) (eta y : ℝ) : ℝ

Correction jet, given by iteratedDeriv k (fun t => correction c amp eta (Real.exp t)) y.

Equations

• NavierStokes.OutgoingPulseBounds.correctionJet c amp k eta y = iteratedDeriv k (fun (t : ℝ) => NavierStokes.OutgoingSchedule.correction c amp eta (Real.exp t)) y

theorem NavierStokes.OutgoingPulseBounds.correctionJet_eq (c : OutgoingSchedule.Parameters) (amp : ℝ → ℝ) (k : ℕ) (eta y : ℝ) : correctionJet c amp k eta y = iteratedDeriv k (affineProfile c (parameterPolynomial eta) (amp eta)) y

theorem NavierStokes.OutgoingPulseBounds.correctionJet_bound (c : OutgoingSchedule.Parameters) (hsmall : c.lam ≤ 1 / 120) (amp : ℝ → ℝ) (k : ℕ) {eta : ℝ} (heta : |eta| ≤ 1) (y : ℝ) : |correctionJet c amp k eta y| ≤ 2 * correctionJetBound c.P c.m k * Real.exp (-(1 / (4 * c.lam))) * (1 + |amp eta|)

theorem NavierStokes.OutgoingPulseBounds.correctionJet_eta_hasDerivAt (c : OutgoingSchedule.Parameters) {amp : ℝ → ℝ} {eta amp' : ℝ} (ha : HasDerivAt amp amp' eta) (k : ℕ) (y : ℝ) : HasDerivAt (fun (t : ℝ) => correctionJet c amp k t y) (iteratedDeriv k (affineProfile c (1 + 3 * eta ^ 2) amp') y) eta

theorem NavierStokes.OutgoingPulseBounds.correctionJet_eta_bound (c : OutgoingSchedule.Parameters) (hsmall : c.lam ≤ 1 / 120) {amp : ℝ → ℝ} {eta amp' : ℝ} (ha : HasDerivAt amp amp' eta) (heta : |eta| ≤ 1) (k : ℕ) (y : ℝ) : |deriv (fun (t : ℝ) => correctionJet c amp k t y) eta| ≤ 4 * correctionJetBound c.P c.m k * Real.exp (-(1 / (4 * c.lam))) * (1 + |amp'|)

theorem NavierStokes.OutgoingPulseBounds.normalized_mass_prefix_hasDerivAt (c : OutgoingSchedule.Parameters) (amp : ℝ → ℝ) (eta : ℝ) : HasDerivAt (fun (t : ℝ) => OutgoingSchedule.massMoment c amp t c.pulseStart / (Real.exp c.pulseStart * OutgoingSchedule.angular c.P c.dropLength c.lam (c.pulseStart, t))) (OutgoingSchedule.prefixCoefficient c 0 * (1 + 3 * eta ^ 2)) eta

theorem NavierStokes.OutgoingPulseBounds.normalized_mass_prefix_derivative_small (c : OutgoingSchedule.Parameters) (hwait : c.wait = 60 * Real.log (1 / c.lam)) (hsmall : c.lam ≤ 1 / 120) (amp : ℝ → ℝ) {eta : ℝ} (heta : |eta| ≤ 1) : |deriv (fun (t : ℝ) => OutgoingSchedule.massMoment c amp t c.pulseStart / (Real.exp c.pulseStart * OutgoingSchedule.angular c.P c.dropLength c.lam (c.pulseStart, t))) eta| ≤ 4 * prefixBound c.P c.m 0 * c.lam ^ 29

theorem NavierStokes.OutgoingPulseBounds.individual_correction_jet_formula (c : OutgoingSchedule.Parameters) (amp : ℝ → ℝ) (eta : ℝ) (j : Fin 2) (k : ℕ) (y : ℝ) : iteratedDeriv k (fun (t : ℝ) => LocalizedMomentRepair.coefficients c.exponents c.lower c.upper (OutgoingSchedule.debt c amp eta) j * LocalizedMomentRepair.bump (c.lower j) (c.upper j) (Real.exp t)) y = affineCoefficients c (parameterPolynomial eta) (amp eta) j * iteratedDeriv k logTemplate (y - center c j)

theorem NavierStokes.OutgoingPulseBounds.individual_correction_jet_bound (c : OutgoingSchedule.Parameters) (hsmall : c.lam ≤ 1 / 120) (amp : ℝ → ℝ) {eta : ℝ} (heta : |eta| ≤ 1) (j : Fin 2) (k : ℕ) (y : ℝ) : |iteratedDeriv k (fun (t : ℝ) => LocalizedMomentRepair.coefficients c.exponents c.lower c.upper (OutgoingSchedule.debt c amp eta) j * LocalizedMomentRepair.bump (c.lower j) (c.upper j) (Real.exp t)) y| ≤ correctionJetBound c.P c.m k * Real.exp (-(1 / (4 * c.lam))) * (1 + |amp eta|)

theorem NavierStokes.OutgoingPulseBounds.individual_correction_jet_eta_bound (c : OutgoingSchedule.Parameters) (hsmall : c.lam ≤ 1 / 120) {amp : ℝ → ℝ} {eta amp' : ℝ} (ha : HasDerivAt amp amp' eta) (heta : |eta| ≤ 1) (j : Fin 2) (k : ℕ) (y : ℝ) : |deriv (fun (s : ℝ) => iteratedDeriv k (fun (t : ℝ) => LocalizedMomentRepair.coefficients c.exponents c.lower c.upper (OutgoingSchedule.debt c amp s) j * LocalizedMomentRepair.bump (c.lower j) (c.upper j) (Real.exp t)) y) eta| ≤ 2 * correctionJetBound c.P c.m k * Real.exp (-(1 / (4 * c.lam))) * (1 + |amp'|)

theorem NavierStokes.OutgoingPulseBounds.paper_prefix_bounds (P m : ℝ) (hP : 0 < P) (hm : 0 < m) : ∃ (C : ℝ), 0 < C ∧ ∀ (lam : ℝ) (hlam : 0 < lam) (hsmall : lam ≤ 1 / 120), have c := OutgoingSchedule.paperParameters P m lam hP hm hlam ⋯; OutgoingSchedule.pulseAmplitude c ≤ C * lam ^ 30 ∧ ∀ (amp : ℝ → ℝ) (eta : ℝ), |eta| ≤ 1 → |OutgoingSchedule.massMoment c amp eta c.pulseStart / (Real.exp c.pulseStart * OutgoingSchedule.angular c.P c.dropLength c.lam (c.pulseStart, eta))| ≤ C * lam ^ 29 ∧ |deriv (fun (t : ℝ) => OutgoingSchedule.massMoment c amp t c.pulseStart / (Real.exp c.pulseStart * OutgoingSchedule.angular c.P c.dropLength c.lam (c.pulseStart, t))) eta| ≤ C * lam ^ 29

One constant controls the two prefix estimates and the first parameter derivative for the exact family specified in the manuscript.

theorem NavierStokes.OutgoingPulseBounds.paper_correction_bounds (P m : ℝ) (hP : 0 < P) (hm : 0 < m) (k : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (lam : ℝ) (hlam : 0 < lam) (hsmall : lam ≤ 1 / 120), have c := OutgoingSchedule.paperParameters P m lam hP hm hlam ⋯; ∀ (amp : ℝ → ℝ) (eta y : ℝ), |eta| ≤ 1 → |correctionJet c amp k eta y| ≤ C * Real.exp (-(1 / (4 * lam))) * (1 + |amp eta|) ∧ ∀ (amp' : ℝ), HasDerivAt amp amp' eta → |deriv (fun (t : ℝ) => correctionJet c amp k t y) eta| ≤ C * Real.exp (-(1 / (4 * lam))) * (1 + |amp'|)

For every fixed radial derivative order there is a single constant independent of lam, the amplitude function, the parameter, and the radial coordinate.

Scalar identities for the outgoing radial schedule

This file verifies the ideal-prefix source and its lower bound, the exponential weights of the axial moment rows, their two-column algebraic reset, the negative energy term in equation (13), and the constant-coefficient lag equation.

These finite-dimensional calculations do not establish existence of the full smooth schedule, estimates on the correction bumps, or the stress-cone bounds.

noncomputable def NavierStokes.RadialSchedule.axialExponent (h : ℝ) : ℝ

Axial exponent, given by 1 / 2 - h.

Equations

• NavierStokes.RadialSchedule.axialExponent h = 1 / 2 - h

def NavierStokes.RadialSchedule.axialShape (η : ℝ) : ℝ

Axial shape, given by 1 - η ^ 2.

Equations

• NavierStokes.RadialSchedule.axialShape η = 1 - η ^ 2

def NavierStokes.RadialSchedule.coordinateFactor (h η : ℝ) : ℝ

Coordinate factor, given by 1 - 2 * h * η ^ 2.

Equations

• NavierStokes.RadialSchedule.coordinateFactor h η = 1 - 2 * h * η ^ 2

def NavierStokes.RadialSchedule.idealAxialVelocity (η : ℝ) : ℝ

Ideal axial velocity, given by 4 * η.

Equations

• NavierStokes.RadialSchedule.idealAxialVelocity η = 4 * η

noncomputable def NavierStokes.RadialSchedule.idealTransport (h η : ℝ) : ℝ

Ideal transport, given by `1 - 2 * axialExponent h * η * idealAxialVelocity η - axialShape η

• 4`.

Equations

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

noncomputable def NavierStokes.RadialSchedule.logShapeDerivative (η : ℝ) : ℝ

The logarithmic shape derivative of (1 + η²)⁻¹.

Equations

• NavierStokes.RadialSchedule.logShapeDerivative η = -(2 * η / (1 + η ^ 2))

theorem NavierStokes.RadialSchedule.log_shape_hasDerivAt (η : ℝ) : HasDerivAt (fun (x : ℝ) => -Real.log (1 + x ^ 2)) (logShapeDerivative η) η

noncomputable def NavierStokes.RadialSchedule.idealSource (h η : ℝ) : ℝ

Ideal source as an element of ℝ.

Equations

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

noncomputable def NavierStokes.RadialSchedule.idealLag (h η : ℝ) : ℝ

The constant particular solution with l = 3/5.

Equations

• NavierStokes.RadialSchedule.idealLag h η = NavierStokes.RadialSchedule.idealSource h η / (8 / 5)

theorem NavierStokes.RadialSchedule.ideal_transport_eq (h η : ℝ) : idealTransport h η = 1 - 4 * coordinateFactor h η

theorem NavierStokes.RadialSchedule.ideal_source_displayed (h η : ℝ) : idealSource h η = 3 / 5 * (4 * coordinateFactor h η - 1) - h * (1 - 8 * η ^ 2) + (axialExponent h + 4 * axialShape η) * η * (2 * η / (1 + η ^ 2))

theorem NavierStokes.RadialSchedule.ideal_source_positive_decomposition (h η : ℝ) : idealSource h η = 9 / 5 - h + 16 / 5 * h * η ^ 2 + 2 * (axialExponent h + 4 * axialShape η) * η ^ 2 / (1 + η ^ 2)

theorem NavierStokes.RadialSchedule.ideal_lag_ge_one {h η : ℝ} (hh : 0 ≤ h) (hsmall : h ≤ 1 / 5) (hη : η ^ 2 ≤ 1) : 1 ≤ idealLag h η

A quantitative version of the ideal-prefix positivity in Section 4.4.

theorem NavierStokes.RadialSchedule.ideal_lag_equation (h η : ℝ) : (1 + 3 / 5) * idealLag h η = idealSource h η

The profile equation is satisfied by the constant particular solution.

noncomputable def NavierStokes.RadialSchedule.radiusProfile (X₀ y : ℝ) : ℝ

Radius profile, given by X₀ * Real.exp y.

Equations

• NavierStokes.RadialSchedule.radiusProfile X₀ y = X₀ * Real.exp y

noncomputable def NavierStokes.RadialSchedule.angularVelocityProfile (e₀ lam y : ℝ) : ℝ

Angular velocity profile, given by e₀ * Real.exp (-(1 / 2 + lam) * y).

Equations

• NavierStokes.RadialSchedule.angularVelocityProfile e₀ lam y = e₀ * Real.exp (-(1 / 2 + lam) * y)

noncomputable def NavierStokes.RadialSchedule.angularMomentumProfile (H₀ lam y : ℝ) : ℝ

Angular momentum profile, given by H₀ * Real.exp (-lam * y).

Equations

• NavierStokes.RadialSchedule.angularMomentumProfile H₀ lam y = H₀ * Real.exp (-lam * y)

theorem NavierStokes.RadialSchedule.first_axial_moment_weight (X₀ e₀ lam y : ℝ) : radiusProfile X₀ y * angularVelocityProfile e₀ lam y = X₀ * e₀ * Real.exp ((1 / 2 - lam) * y)

Weight of R in dM/dy = X E R.

theorem NavierStokes.RadialSchedule.second_axial_moment_weight (X₀ e₀ H₀ lam y : ℝ) : radiusProfile X₀ y * angularVelocityProfile e₀ lam y * angularMomentumProfile H₀ lam y = X₀ * e₀ * H₀ * Real.exp ((1 / 2 - 2 * lam) * y)

Weight of R in dJ/dy = X E H R.

theorem NavierStokes.RadialSchedule.energy_moment_weight (X₀ e₀ lam y : ℝ) : radiusProfile X₀ y * angularVelocityProfile e₀ lam y ^ 2 = X₀ * e₀ ^ 2 * Real.exp (-2 * lam * y)

The common energy weight used to rescale the pulse in equation (13).

theorem NavierStokes.RadialSchedule.axial_weight_gap_neg {lam δ : ℝ} (hlam : 0 < lam) (hδ : 0 < δ) : Real.exp ((1 / 2 - 2 * lam) * δ) - Real.exp ((1 / 2 - lam) * δ) < 0

The two axial slopes differ whenever lam > 0, as do their translated weights.

theorem NavierStokes.RadialSchedule.axial_moment_determinant_neg {lam δ c₁ c₂ : ℝ} (hlam : 0 < lam) (hδ : 0 < δ) (hc₁ : 0 < c₁) (hc₂ : 0 < c₂) : c₁ * (c₂ * Real.exp ((1 / 2 - 2 * lam) * δ)) - c₁ * Real.exp ((1 / 2 - lam) * δ) * c₂ < 0

Determinant of the moment matrix for two equal bumps separated by δ.

theorem NavierStokes.RadialSchedule.two_moment_reset {r₁ r₂ : ℝ} (hgap : r₂ ≠ r₁) (debt₁ debt₂ : ℝ) : have b := (debt₁ - debt₂) / (r₂ - r₁); have a := -debt₁ - r₁ * b; debt₁ + a + r₁ * b = 0 ∧ debt₂ + a + r₂ * b = 0

Explicit algebraic reset for arbitrary debts in the two normalized moment rows. The theorem does not assert bounds on these coefficients or construct smooth bumps.

theorem NavierStokes.RadialSchedule.pulse_negative_energy_integral : ∫ (z : ℝ) in 0..13, 1 / 2 * Real.exp (-2 * z) = (1 - Real.exp (-26)) / 4

The exact negative part of the scaled pulse energy in equation (13).

noncomputable def NavierStokes.RadialSchedule.pulseEnergyDebt : ℝ

Pulse energy debt, given by (1 - Real.exp (-26)) / 4.

Equations

• NavierStokes.RadialSchedule.pulseEnergyDebt = (1 - Real.exp (-26)) / 4

theorem NavierStokes.RadialSchedule.pulse_energy_debt_bounds : 6 / 25 ≤ pulseEnergyDebt ∧ pulseEnergyDebt ≤ 1 / 4

theorem NavierStokes.RadialSchedule.pulse_amplitude_endpoint_signs {K error₀ error₁ : ℝ} (hKlo : 1 / 5 ≤ K) (hKhi : K ≤ 1 / 4) (herror₀ : |error₀| ≤ 1 / 100) (herror₁ : |error₁| ≤ 1 / 100) : K * (9 / 10) ^ 2 - pulseEnergyDebt + error₀ < 0 ∧ 0 < K * (6 / 5) ^ 2 - pulseEnergyDebt + error₁

Equation (13) has opposite endpoint signs if its error is at most 1/100. The asymptotic estimate needed to establish that bound is not formalized here.

theorem NavierStokes.RadialSchedule.pulse_amplitude_root {K : ℝ} (error : ℝ → ℝ) (hKlo : 1 / 5 ≤ K) (hKhi : K ≤ 1 / 4) (hcontinuous : ContinuousOn error (Set.Icc (9 / 10) (6 / 5))) (herror : ∀ A ∈ Set.Icc (9 / 10) (6 / 5), |error A| ≤ 1 / 100) : ∃ A ∈ Set.Icc (9 / 10) (6 / 5), K * A ^ 2 - pulseEnergyDebt + error A = 0

A continuous error bounded by 1/100 gives an amplitude in the manuscript's bracket. No monotonicity, uniqueness, smooth dependence, or asymptotic error estimate is inferred from this theorem.

noncomputable def NavierStokes.RadialSchedule.lagSolution (a c q₀ y : ℝ) : ℝ

Constant-source lag solution, written in a form that also specifies its initial value.

Equations

• NavierStokes.RadialSchedule.lagSolution a c q₀ y = c / a + (q₀ - c / a) * Real.exp (-a * y)

theorem NavierStokes.RadialSchedule.lag_solution_initial (a c q₀ : ℝ) : lagSolution a c q₀ 0 = q₀

theorem NavierStokes.RadialSchedule.lag_solution_hasDerivAt (a c q₀ y : ℝ) : HasDerivAt (lagSolution a c q₀) (-(a * (q₀ - c / a) * Real.exp (-a * y))) y

theorem NavierStokes.RadialSchedule.lag_solution_equation {a : ℝ} (ha : a ≠ 0) (c q₀ y : ℝ) : deriv (lagSolution a c q₀) y + a * lagSolution a c q₀ y = c

theorem NavierStokes.RadialSchedule.release_initial_lag {lam : ℝ} (hlam : lam ≠ 1) (h : ℝ) : -1 + (1 - h) / (1 - lam) = (lam - h) / (1 - lam)

The release initial lag follows algebraically from the angular moment reset.

theorem NavierStokes.RadialSchedule.release_initial_lag_positive {lam h : ℝ} (hhlam : h < lam) (hlam : lam < 1) : 0 < (lam - h) / (1 - lam)

theorem NavierStokes.PulseAmplitude.pulseRamp_nonneg {z : ℝ} (hz : 0 ≤ z) : 0 ≤ OutgoingSchedule.pulseRamp z

theorem NavierStokes.PulseAmplitude.pulseRamp_le {z : ℝ} (hz : 0 ≤ z) : OutgoingSchedule.pulseRamp z ≤ z

theorem NavierStokes.PulseAmplitude.pulseRamp_lower {z : ℝ} (hz : 1 / 50 ≤ z) : z - 1 / 50 ≤ OutgoingSchedule.pulseRamp z

theorem NavierStokes.PulseAmplitude.mainPulse_nonneg {z : ℝ} (hz : 0 ≤ z) : 0 ≤ OutgoingSchedule.mainPulse z

theorem NavierStokes.PulseAmplitude.mainPulse_le {z : ℝ} (hz : 0 ≤ z) : OutgoingSchedule.mainPulse z ≤ z

theorem NavierStokes.PulseAmplitude.mainPulse_lower {z : ℝ} (hz : 1 / 50 ≤ z) (hz' : z ≤ 10) : z - 1 / 50 ≤ OutgoingSchedule.mainPulse z

noncomputable def NavierStokes.PulseAmplitude.pulseConstant : ℝ

Pulse constant, given by ∫ z in (0 : ℝ)..13, Real.exp (-2 * z) * mainPulse z ^ 2.

Equations

• NavierStokes.PulseAmplitude.pulseConstant = ∫ (z : ℝ) in 0..13, Real.exp (-2 * z) * NavierStokes.OutgoingSchedule.mainPulse z ^ 2

theorem NavierStokes.PulseAmplitude.energyWeight_continuous : Continuous fun (z : ℝ) => Real.exp (-2 * z)

noncomputable def NavierStokes.PulseAmplitude.weightedSquarePrimitive (a z : ℝ) : ℝ

Weighted square primitive, given by -Real.exp (-2 * z) * ((z - a) ^ 2 / 2 + (z - a) / 2 + 1 / 4).

Equations

• NavierStokes.PulseAmplitude.weightedSquarePrimitive a z = -Real.exp (-2 * z) * ((z - a) ^ 2 / 2 + (z - a) / 2 + 1 / 4)

theorem NavierStokes.PulseAmplitude.weightedSquarePrimitive_hasDerivAt (a z : ℝ) : HasDerivAt (weightedSquarePrimitive a) (Real.exp (-2 * z) * (z - a) ^ 2) z

theorem NavierStokes.PulseAmplitude.weightedSquare_integral (a l u : ℝ) : ∫ (z : ℝ) in l..u, Real.exp (-2 * z) * (z - a) ^ 2 = weightedSquarePrimitive a u - weightedSquarePrimitive a l

theorem NavierStokes.PulseAmplitude.pulseConstant_upper : pulseConstant ≤ 1 / 4

theorem NavierStokes.PulseAmplitude.pulseConstant_lower : 1 / 5 < pulseConstant

theorem NavierStokes.PulseAmplitude.pulseConstant_bounds : 1 / 5 < pulseConstant ∧ pulseConstant ≤ 1 / 4

The actual affine correction and the actual pulse quadratic

def NavierStokes.PulseAmplitude.etaPolynomial (eta : ℝ) : ℝ

Eta polynomial, given by eta * (1 + eta ^ 2).

Equations

• NavierStokes.PulseAmplitude.etaPolynomial eta = eta * (1 + eta ^ 2)

noncomputable def NavierStokes.PulseAmplitude.prefixRepair (c : OutgoingSchedule.Parameters) (y : ℝ) : ℝ

Prefix repair, given by LocalizedMomentRepair.repair c.exponents c.lower c.upper (fun i => -prefixCoefficient c i) (Real.exp y).

Equations

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

noncomputable def NavierStokes.PulseAmplitude.amplitudeRepair (c : OutgoingSchedule.Parameters) (y : ℝ) : ℝ

Amplitude repair, given by LocalizedMomentRepair.repair c.exponents c.lower c.upper (fun i => -mainMoment c i) (Real.exp y).

Equations

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

noncomputable def NavierStokes.PulseAmplitude.amplitudeShape (c : OutgoingSchedule.Parameters) (y : ℝ) : ℝ

Amplitude shape, given by mainPulse (c.lam * y) + amplitudeRepair c y.

Equations

• NavierStokes.PulseAmplitude.amplitudeShape c y = NavierStokes.OutgoingSchedule.mainPulse (c.lam * y) + NavierStokes.PulseAmplitude.amplitudeRepair c y

theorem NavierStokes.PulseAmplitude.prefixRepair_contDiff (c : OutgoingSchedule.Parameters) : ContDiff ℝ (↑⊤) (prefixRepair c)

theorem NavierStokes.PulseAmplitude.amplitudeRepair_contDiff (c : OutgoingSchedule.Parameters) : ContDiff ℝ (↑⊤) (amplitudeRepair c)

theorem NavierStokes.PulseAmplitude.amplitudeShape_contDiff (c : OutgoingSchedule.Parameters) : ContDiff ℝ (↑⊤) (amplitudeShape c)

theorem NavierStokes.PulseAmplitude.correction_eq_affine (c : OutgoingSchedule.Parameters) (amp : ℝ → ℝ) (eta y : ℝ) : OutgoingSchedule.correction c amp eta (Real.exp y) = etaPolynomial eta * prefixRepair c y + amp eta * amplitudeRepair c y

theorem NavierStokes.PulseAmplitude.pulseRatio_eq_affine (c : OutgoingSchedule.Parameters) (amp : ℝ → ℝ) (eta y : ℝ) : OutgoingSchedule.pulseRatio c amp (y, eta) = amp eta * amplitudeShape c y + etaPolynomial eta * prefixRepair c y

theorem NavierStokes.PulseAmplitude.prefixRepair_eq_correction (c : OutgoingSchedule.Parameters) (y : ℝ) : 2 * prefixRepair c y = OutgoingSchedule.correction c (fun (x : ℝ) => 0) 1 (Real.exp y)

theorem NavierStokes.PulseAmplitude.amplitudeRepair_eq_correction (c : OutgoingSchedule.Parameters) (y : ℝ) : amplitudeRepair c y = OutgoingSchedule.correction c (fun (x : ℝ) => 1) 0 (Real.exp y)

theorem NavierStokes.PulseAmplitude.mainPulse_mul_correction (c : OutgoingSchedule.Parameters) (amp : ℝ → ℝ) (eta y : ℝ) : OutgoingSchedule.mainPulse (c.lam * y) * OutgoingSchedule.correction c amp eta (Real.exp y) = 0

theorem NavierStokes.PulseAmplitude.mainPulse_mul_amplitudeRepair (c : OutgoingSchedule.Parameters) (y : ℝ) : OutgoingSchedule.mainPulse (c.lam * y) * amplitudeRepair c y = 0

theorem NavierStokes.PulseAmplitude.mainPulse_mul_prefixRepair (c : OutgoingSchedule.Parameters) (y : ℝ) : OutgoingSchedule.mainPulse (c.lam * y) * prefixRepair c y = 0

noncomputable def NavierStokes.PulseAmplitude.pulseWeight (c : OutgoingSchedule.Parameters) (y : ℝ) : ℝ

Pulse weight, given by Real.exp (-2 * c.lam * y).

Equations

• NavierStokes.PulseAmplitude.pulseWeight c y = Real.exp (-2 * c.lam * y)

theorem NavierStokes.PulseAmplitude.pulseWeight_continuous (c : OutgoingSchedule.Parameters) : Continuous (pulseWeight c)

theorem NavierStokes.PulseAmplitude.pulse_rescale_integral (c : OutgoingSchedule.Parameters) (f : ℝ → ℝ) : c.lam * ∫ (y : ℝ) in 0..c.pulseLength, f (c.lam * y) = ∫ (z : ℝ) in 0..13, f z

noncomputable def NavierStokes.PulseAmplitude.quadraticCoefficient (c : OutgoingSchedule.Parameters) : ℝ

Quadratic coefficient, given by c.lam * ∫ y in (0 : ℝ)..c.pulseLength, pulseWeight c y * amplitudeShape c y ^ 2.

Equations

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

noncomputable def NavierStokes.PulseAmplitude.linearCoefficient (c : OutgoingSchedule.Parameters) : ℝ

Linear coefficient, given by 2 * c.lam * ∫ y in (0 : ℝ)..c.pulseLength, pulseWeight c y * amplitudeShape c y * prefixRepair c y.

Equations

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

noncomputable def NavierStokes.PulseAmplitude.constantCorrection (c : OutgoingSchedule.Parameters) : ℝ

Constant correction, given by c.lam * ∫ y in (0 : ℝ)..c.pulseLength, pulseWeight c y * prefixRepair c y ^ 2.

Equations

• NavierStokes.PulseAmplitude.constantCorrection c = c.lam * ∫ (y : ℝ) in 0..c.pulseLength, NavierStokes.PulseAmplitude.pulseWeight c y * NavierStokes.PulseAmplitude.prefixRepair c y ^ 2

noncomputable def NavierStokes.PulseAmplitude.scaledPulseEnergy (c : OutgoingSchedule.Parameters) (A eta : ℝ) : ℝ

Scaled pulse energy, given by c.lam * ∫ y in (0 : ℝ)..c.pulseLength, pulseWeight c y * (pulseRatio c (fun _ => A) (y, eta) ^ 2 - 1 / 2).

Equations

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

theorem NavierStokes.PulseAmplitude.normalized_main_energy (c : OutgoingSchedule.Parameters) : c.lam * ∫ (y : ℝ) in 0..c.pulseLength, pulseWeight c y * OutgoingSchedule.mainPulse (c.lam * y) ^ 2 = pulseConstant

theorem NavierStokes.PulseAmplitude.normalized_negative_energy (c : OutgoingSchedule.Parameters) : c.lam * ∫ (y : ℝ) in 0..c.pulseLength, 1 / 2 * pulseWeight c y = RadialSchedule.pulseEnergyDebt

theorem NavierStokes.PulseAmplitude.quadraticCoefficient_eq (c : OutgoingSchedule.Parameters) : quadraticCoefficient c = pulseConstant + c.lam * ∫ (y : ℝ) in 0..c.pulseLength, pulseWeight c y * amplitudeRepair c y ^ 2

theorem NavierStokes.PulseAmplitude.quadraticCoefficient_ge (c : OutgoingSchedule.Parameters) : pulseConstant ≤ quadraticCoefficient c

theorem NavierStokes.PulseAmplitude.scaledPulseEnergy_eq (c : OutgoingSchedule.Parameters) (A eta : ℝ) : scaledPulseEnergy c A eta = quadraticCoefficient c * A ^ 2 + linearCoefficient c * etaPolynomial eta * A + constantCorrection c * etaPolynomial eta ^ 2 - RadialSchedule.pulseEnergyDebt

Exact prefix coefficients and uniform bounds

noncomputable def NavierStokes.PulseAmplitude.coreEnergyWeight (c : OutgoingSchedule.Parameters) (y : ℝ) : ℝ

Core energy weight, given by Real.exp y * radialAmplitude c.P c.dropLength c.lam y ^ 2.

Equations

• NavierStokes.PulseAmplitude.coreEnergyWeight c y = Real.exp y * NavierStokes.OutgoingSchedule.radialAmplitude c.P c.dropLength c.lam y ^ 2

noncomputable def NavierStokes.PulseAmplitude.normalization (c : OutgoingSchedule.Parameters) : ℝ

Normalization, given by Real.exp c.pulseStart * pulseAmplitude c ^ 2.

Equations

• NavierStokes.PulseAmplitude.normalization c = Real.exp c.pulseStart * NavierStokes.OutgoingSchedule.pulseAmplitude c ^ 2

theorem NavierStokes.PulseAmplitude.normalization_pos (c : OutgoingSchedule.Parameters) : 0 < normalization c

theorem NavierStokes.PulseAmplitude.coreEnergyWeight_nonneg (c : OutgoingSchedule.Parameters) (y : ℝ) : 0 ≤ coreEnergyWeight c y

theorem NavierStokes.PulseAmplitude.coreEnergyWeight_contDiff (c : OutgoingSchedule.Parameters) : ContDiff ℝ (↑⊤) (coreEnergyWeight c)

theorem NavierStokes.PulseAmplitude.coreEnergyWeight_hasDerivAt (c : OutgoingSchedule.Parameters) (y : ℝ) : HasDerivAt (coreEnergyWeight c) (2 * OutgoingSchedule.slope c.dropLength c.lam y * coreEnergyWeight c y) y

theorem NavierStokes.PulseAmplitude.slope_ge_neg_lambda (c : OutgoingSchedule.Parameters) (y : ℝ) : -c.lam ≤ OutgoingSchedule.slope c.dropLength c.lam y

theorem NavierStokes.PulseAmplitude.weightedCore_monotone (c : OutgoingSchedule.Parameters) : Monotone fun (y : ℝ) => coreEnergyWeight c y * Real.exp (2 * c.lam * y)

theorem NavierStokes.PulseAmplitude.prefix_weight_bound (c : OutgoingSchedule.Parameters) {y : ℝ} (hy : 0 ≤ y) (hy' : y ≤ c.pulseStart) : coreEnergyWeight c y ≤ normalization c * Real.exp (2 * c.lam * c.pulseStart)

theorem NavierStokes.PulseAmplitude.initial_weight_bound (c : OutgoingSchedule.Parameters) : c.P ^ 2 ≤ normalization c * Real.exp (2 * c.lam * c.pulseStart)

noncomputable def NavierStokes.PulseAmplitude.prefixAxialEnergy (c : OutgoingSchedule.Parameters) : ℝ

Prefix axial energy, given by 16 + ∫ y in (0 : ℝ)..c.pulseStart, Real.exp y * dropCoefficient c.m y ^ 2.

Equations

• NavierStokes.PulseAmplitude.prefixAxialEnergy c = 16 + ∫ (y : ℝ) in 0..c.pulseStart, Real.exp y * NavierStokes.OutgoingSchedule.dropCoefficient c.m y ^ 2

noncomputable def NavierStokes.PulseAmplitude.prefixAngularEnergy (c : OutgoingSchedule.Parameters) : ℝ

Prefix angular energy, given by (5 / 12) * c.P ^ 2 + ∫ y in (0 : ℝ)..c.pulseStart, coreEnergyWeight c y / 2.

Equations

• NavierStokes.PulseAmplitude.prefixAngularEnergy c = 5 / 12 * c.P ^ 2 + ∫ (y : ℝ) in 0..c.pulseStart, NavierStokes.PulseAmplitude.coreEnergyWeight c y / 2

noncomputable def NavierStokes.PulseAmplitude.prefixEnergy (c : OutgoingSchedule.Parameters) (eta : ℝ) : ℝ

Prefix energy, given by prefixAxialEnergy c * eta ^ 2 - prefixAngularEnergy c * shape eta ^ 2.

Equations

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

theorem NavierStokes.PulseAmplitude.prefixAngularEnergy_bound (c : OutgoingSchedule.Parameters) : prefixAngularEnergy c ≤ (5 / 12 + c.pulseStart / 2) * (normalization c * Real.exp (2 * c.lam * c.pulseStart))

theorem NavierStokes.PulseAmplitude.prefixAxialEnergy_bound (c : OutgoingSchedule.Parameters) : prefixAxialEnergy c ≤ 16 * Real.exp (Real.exp c.m)

The complete outgoing energy is an actual improper integral

noncomputable def NavierStokes.PulseAmplitude.energyIntegrand (d : OutgoingTail.TailData) (A eta y : ℝ) : ℝ

Energy integrand, given by Real.exp y * (axial d.core (fun _ => A) (y, eta) ^ 2 - OutgoingTail.finalAngular d (y, eta) ^ 2 / 2).

Equations

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

noncomputable def NavierStokes.PulseAmplitude.totalEnergy (d : OutgoingTail.TailData) (A eta : ℝ) : ℝ

Total energy, given by ∫ y, energyIntegrand d A eta y.

Equations

• NavierStokes.PulseAmplitude.totalEnergy d A eta = ∫ (y : ℝ), NavierStokes.PulseAmplitude.energyIntegrand d A eta y

noncomputable def NavierStokes.PulseAmplitude.tailEnergy (d : OutgoingTail.TailData) (eta : ℝ) : ℝ

Tail energy, given by ∫ y in Ioi d.core.endpoint, Real.exp y * OutgoingTail.finalAngular d (y, eta) ^ 2.

Equations

• NavierStokes.PulseAmplitude.tailEnergy d eta = ∫ (y : ℝ) in Set.Ioi d.core.endpoint, Real.exp y * NavierStokes.OutgoingTail.finalAngular d (y, eta) ^ 2

theorem NavierStokes.PulseAmplitude.energyIntegrand_continuous (d : OutgoingTail.TailData) (A eta : ℝ) : Continuous (energyIntegrand d A eta)

theorem NavierStokes.PulseAmplitude.coreEndpoint_pos (c : OutgoingSchedule.Parameters) : 0 < c.endpoint

theorem NavierStokes.PulseAmplitude.pulseStart_le_endpoint (c : OutgoingSchedule.Parameters) : c.pulseStart ≤ c.endpoint

theorem NavierStokes.PulseAmplitude.energyIntegrand_ideal (d : OutgoingTail.TailData) (A eta : ℝ) {y : ℝ} (hy : y ≤ 0) : energyIntegrand d A eta y = 16 * eta ^ 2 * Real.exp y - d.core.P ^ 2 * OutgoingSchedule.shape eta ^ 2 / 2 * Real.exp (6 / 5 * y)

theorem NavierStokes.PulseAmplitude.energyIntegrand_integrable_ideal (d : OutgoingTail.TailData) (A eta : ℝ) : MeasureTheory.IntegrableOn (energyIntegrand d A eta) (Set.Iic 0) MeasureTheory.volume

theorem NavierStokes.PulseAmplitude.energyIntegrand_integral_ideal (d : OutgoingTail.TailData) (A eta : ℝ) : ∫ (y : ℝ) in Set.Iic 0, energyIntegrand d A eta y = 16 * eta ^ 2 - 5 / 12 * d.core.P ^ 2 * OutgoingSchedule.shape eta ^ 2

theorem NavierStokes.PulseAmplitude.energyIntegrand_prefix (d : OutgoingTail.TailData) (A eta : ℝ) {y : ℝ} (hy : y ≤ d.core.pulseStart) : energyIntegrand d A eta y = eta ^ 2 * (Real.exp y * OutgoingSchedule.dropCoefficient d.core.m y ^ 2) - OutgoingSchedule.shape eta ^ 2 * (coreEnergyWeight d.core y / 2)

theorem NavierStokes.PulseAmplitude.energyIntegrand_integrable_Iic (d : OutgoingTail.TailData) (A eta : ℝ) {b : ℝ} (hb : 0 ≤ b) : MeasureTheory.IntegrableOn (energyIntegrand d A eta) (Set.Iic b) MeasureTheory.volume

theorem NavierStokes.PulseAmplitude.energyIntegrand_integral_prefix (d : OutgoingTail.TailData) (A eta : ℝ) : ∫ (y : ℝ) in Set.Iic d.core.pulseStart, energyIntegrand d A eta y = prefixEnergy d.core eta

theorem NavierStokes.PulseAmplitude.energyIntegrand_pulse (d : OutgoingTail.TailData) (A eta : ℝ) {y : ℝ} (hy : d.core.pulseStart ≤ y) (hy' : y ≤ d.core.endpoint) : energyIntegrand d A eta y = normalization d.core * OutgoingSchedule.shape eta ^ 2 * (pulseWeight d.core (y - d.core.pulseStart) * (OutgoingSchedule.pulseRatio d.core (fun (x : ℝ) => A) (y - d.core.pulseStart, eta) ^ 2 - 1 / 2))

theorem NavierStokes.PulseAmplitude.energyIntegrand_integral_pulse (d : OutgoingTail.TailData) (A eta : ℝ) : ∫ (y : ℝ) in d.core.pulseStart..d.core.endpoint, energyIntegrand d A eta y = normalization d.core * OutgoingSchedule.shape eta ^ 2 / d.core.lam * scaledPulseEnergy d.core A eta

theorem NavierStokes.PulseAmplitude.energyIntegrand_late (d : OutgoingTail.TailData) (A eta : ℝ) {y : ℝ} (hy : d.core.endpoint ≤ y) : energyIntegrand d A eta y = -(Real.exp y * OutgoingTail.finalAngular d (y, eta) ^ 2) / 2

theorem NavierStokes.PulseAmplitude.totalEnergy_eq_of_integrable (d : OutgoingTail.TailData) (A eta : ℝ) (htail : MeasureTheory.IntegrableOn (fun (y : ℝ) => Real.exp y * OutgoingTail.finalAngular d (y, eta) ^ 2) (Set.Ioi d.core.endpoint) MeasureTheory.volume) : totalEnergy d A eta = prefixEnergy d.core eta + normalization d.core * OutgoingSchedule.shape eta ^ 2 / d.core.lam * scaledPulseEnergy d.core A eta - tailEnergy d eta / 2

theorem NavierStokes.PulseAmplitude.tailEnergy_eq (d : OutgoingTail.TailData) (eta : ℝ) : tailEnergy d eta = TailEnergyBounds.postPulseEnergy d eta

theorem NavierStokes.PulseAmplitude.tailEnergy_contDiff (d : OutgoingTail.TailData) : ContDiff ℝ (↑⊤) (tailEnergy d)

theorem NavierStokes.PulseAmplitude.totalEnergy_eq (d : OutgoingTail.TailData) (A eta : ℝ) : totalEnergy d A eta = prefixEnergy d.core eta + normalization d.core * OutgoingSchedule.shape eta ^ 2 / d.core.lam * scaledPulseEnergy d.core A eta - tailEnergy d eta / 2

noncomputable def NavierStokes.PulseAmplitude.normalizedPrefixAxial (c : OutgoingSchedule.Parameters) : ℝ

Normalized prefix axial, given by c.lam * prefixAxialEnergy c / normalization c.

Equations

• NavierStokes.PulseAmplitude.normalizedPrefixAxial c = c.lam * NavierStokes.PulseAmplitude.prefixAxialEnergy c / NavierStokes.PulseAmplitude.normalization c

noncomputable def NavierStokes.PulseAmplitude.normalizedPrefixAngular (c : OutgoingSchedule.Parameters) : ℝ

Normalized prefix angular, given by c.lam * prefixAngularEnergy c / normalization c.

Equations

• NavierStokes.PulseAmplitude.normalizedPrefixAngular c = c.lam * NavierStokes.PulseAmplitude.prefixAngularEnergy c / NavierStokes.PulseAmplitude.normalization c

noncomputable def NavierStokes.PulseAmplitude.normalizedTail (d : OutgoingTail.TailData) (eta : ℝ) : ℝ

Normalized tail, given by d.core.lam * tailEnergy d eta / (2 * normalization d.core * shape eta ^ 2).

Equations

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

noncomputable def NavierStokes.PulseAmplitude.linearTerm (c : OutgoingSchedule.Parameters) (eta : ℝ) : ℝ

Linear term, given by linearCoefficient c * etaPolynomial eta.

Equations

• NavierStokes.PulseAmplitude.linearTerm c eta = NavierStokes.PulseAmplitude.linearCoefficient c * NavierStokes.PulseAmplitude.etaPolynomial eta

noncomputable def NavierStokes.PulseAmplitude.constantTerm (d : OutgoingTail.TailData) (eta : ℝ) : ℝ

Constant term as an element of ℝ.

Equations

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

noncomputable def NavierStokes.PulseAmplitude.energyPolynomial (d : OutgoingTail.TailData) (A eta : ℝ) : ℝ

Energy polynomial, given by `quadraticCoefficient d.core * A ^ 2 + linearTerm d.core eta * A

• constantTerm d eta`.

Equations

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

theorem NavierStokes.PulseAmplitude.totalEnergy_normalized (d : OutgoingTail.TailData) (A eta : ℝ) : d.core.lam * totalEnergy d A eta / (normalization d.core * OutgoingSchedule.shape eta ^ 2) = energyPolynomial d A eta

theorem NavierStokes.PulseAmplitude.etaPolynomial_contDiff : ContDiff ℝ (↑⊤) etaPolynomial

theorem NavierStokes.PulseAmplitude.normalizedTail_contDiff (d : OutgoingTail.TailData) : ContDiff ℝ (↑⊤) (normalizedTail d)

theorem NavierStokes.PulseAmplitude.linearTerm_contDiff (c : OutgoingSchedule.Parameters) : ContDiff ℝ (↑⊤) (linearTerm c)

theorem NavierStokes.PulseAmplitude.constantTerm_contDiff (d : OutgoingTail.TailData) : ContDiff ℝ (↑⊤) (constantTerm d)

noncomputable def NavierStokes.PulseAmplitude.negativeClamp (x : ℝ) : ℝ

A globally smooth extension of a negative constant coefficient. It agrees with the original coefficient below -1/5; the physical parameter band will be proved to lie strictly in that region.

Equations

• NavierStokes.PulseAmplitude.negativeClamp x = (1 - NavierStokes.OutgoingSchedule.sigma (10 * (x + 1 / 5))) * x - NavierStokes.OutgoingSchedule.sigma (10 * (x + 1 / 5)) / 10

theorem NavierStokes.PulseAmplitude.negativeClamp_contDiff : ContDiff ℝ (↑⊤) negativeClamp

theorem NavierStokes.PulseAmplitude.negativeClamp_eq {x : ℝ} (hx : x ≤ -(1 / 5)) : negativeClamp x = x

theorem NavierStokes.PulseAmplitude.negativeClamp_le (x : ℝ) : negativeClamp x ≤ -(1 / 10)

theorem NavierStokes.PulseAmplitude.negativeClamp_neg (x : ℝ) : negativeClamp x < 0

noncomputable def NavierStokes.PulseAmplitude.discriminant (d : OutgoingTail.TailData) (eta : ℝ) : ℝ

Discriminant, given by linearTerm d.core eta ^ 2 - 4 * quadraticCoefficient d.core * negativeClamp (constantTerm d eta).

Equations

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

theorem NavierStokes.PulseAmplitude.quadraticCoefficient_pos (c : OutgoingSchedule.Parameters) : 0 < quadraticCoefficient c

theorem NavierStokes.PulseAmplitude.discriminant_pos (d : OutgoingTail.TailData) (eta : ℝ) : 0 < discriminant d eta

noncomputable def NavierStokes.PulseAmplitude.amplitude (d : OutgoingTail.TailData) (eta : ℝ) : ℝ

A globally C∞ amplitude. The negative clamp only extends the formula outside the physical parameter band; the theorem below proves its exact agreement with the actual energy equation where the coefficient is small.

Equations

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

theorem NavierStokes.PulseAmplitude.amplitude_contDiff (d : OutgoingTail.TailData) : ContDiff ℝ (↑⊤) (amplitude d)

theorem NavierStokes.PulseAmplitude.amplitude_pos (d : OutgoingTail.TailData) (eta : ℝ) : 0 < amplitude d eta

theorem NavierStokes.PulseAmplitude.amplitude_clamped_equation (d : OutgoingTail.TailData) (eta : ℝ) : quadraticCoefficient d.core * amplitude d eta ^ 2 + linearTerm d.core eta * amplitude d eta + negativeClamp (constantTerm d eta) = 0

theorem NavierStokes.PulseAmplitude.amplitude_energy_equation (d : OutgoingTail.TailData) (eta : ℝ) (hc : constantTerm d eta ≤ -(1 / 5)) : energyPolynomial d (amplitude d eta) eta = 0

theorem NavierStokes.PulseAmplitude.amplitude_totalEnergy_zero (d : OutgoingTail.TailData) (eta : ℝ) (hc : constantTerm d eta ≤ -(1 / 5)) : totalEnergy d (amplitude d eta) eta = 0

Actual coefficient estimates for the paper's wait duration

noncomputable def NavierStokes.PulseAmplitude.logarithmicRate (lam : ℝ) : ℝ

Logarithmic rate, given by lam * (1 + Real.log (1 / lam)).

Equations

• NavierStokes.PulseAmplitude.logarithmicRate lam = lam * (1 + Real.log (1 / lam))

theorem NavierStokes.PulseAmplitude.log_inverse_nonneg (c : OutgoingSchedule.Parameters) : 0 ≤ Real.log (1 / c.lam)

theorem NavierStokes.PulseAmplitude.logarithmicRate_pos (c : OutgoingSchedule.Parameters) : 0 < logarithmicRate c.lam

theorem NavierStokes.PulseAmplitude.lambda_le_logarithmicRate (c : OutgoingSchedule.Parameters) : c.lam ≤ logarithmicRate c.lam

theorem NavierStokes.PulseAmplitude.prefixAxialEnergy_nonneg (c : OutgoingSchedule.Parameters) : 0 ≤ prefixAxialEnergy c

theorem NavierStokes.PulseAmplitude.prefixAngularEnergy_nonneg (c : OutgoingSchedule.Parameters) : 0 ≤ prefixAngularEnergy c

theorem NavierStokes.PulseAmplitude.normalizedPrefix_nonneg (c : OutgoingSchedule.Parameters) : 0 ≤ normalizedPrefixAxial c ∧ 0 ≤ normalizedPrefixAngular c

theorem NavierStokes.PulseAmplitude.normalizedPrefix_bound_raw (c : OutgoingSchedule.Parameters) : normalizedPrefixAxial c + normalizedPrefixAngular c ≤ c.lam * Real.exp (2 * c.lam * c.pulseStart) * (16 * Real.exp (Real.exp c.m) / c.P ^ 2 + 5 / 12 + c.pulseStart / 2)

noncomputable def NavierStokes.PulseAmplitude.prefixBoundConstant (P m : ℝ) : ℝ

Prefix bound constant, given by Real.exp ((Real.exp m + 12) / 5 + 120) * (16 * Real.exp (Real.exp m) / P ^ 2 + 5 / 12 + (Real.exp m + 12) / 2 + 30).

Equations

• NavierStokes.PulseAmplitude.prefixBoundConstant P m = Real.exp ((Real.exp m + 12) / 5 + 120) * (16 * Real.exp (Real.exp m) / P ^ 2 + 5 / 12 + (Real.exp m + 12) / 2 + 30)

theorem NavierStokes.PulseAmplitude.prefixBoundConstant_pos (P m : ℝ) : 0 < prefixBoundConstant P m

theorem NavierStokes.PulseAmplitude.wait_exponential_bound (c : OutgoingSchedule.Parameters) (hwait : c.wait = 60 * Real.log (1 / c.lam)) : Real.exp (2 * c.lam * c.pulseStart) ≤ Real.exp ((Real.exp c.m + 12) / 5 + 120)

theorem NavierStokes.PulseAmplitude.normalizedPrefix_bound (c : OutgoingSchedule.Parameters) (hwait : c.wait = 60 * Real.log (1 / c.lam)) : normalizedPrefixAxial c + normalizedPrefixAngular c ≤ prefixBoundConstant c.P c.m * logarithmicRate c.lam

theorem NavierStokes.PulseAmplitude.normalizedTail_nonneg (d : OutgoingTail.TailData) (eta : ℝ) : 0 ≤ normalizedTail d eta

theorem NavierStokes.PulseAmplitude.normalizedTail_bound (d : OutgoingTail.TailData) (eta : ℝ) (heta : eta ^ 2 ≤ 1) : normalizedTail d eta ≤ TailEnergyBounds.tailConstant / 2 * logarithmicRate d.core.lam

theorem NavierStokes.PulseAmplitude.pulseWeight_le_one (c : OutgoingSchedule.Parameters) {y : ℝ} (hy : 0 ≤ y) : pulseWeight c y ≤ 1

theorem NavierStokes.PulseAmplitude.weighted_square_bound (c : OutgoingSchedule.Parameters) (f : ℝ → ℝ) (hf : Continuous f) (M : ℝ) (hM : 0 ≤ M) (hbound : ∀ (y : ℝ), |f y| ≤ M) : 0 ≤ c.lam * ∫ (y : ℝ) in 0..c.pulseLength, pulseWeight c y * f y ^ 2 ∧ c.lam * ∫ (y : ℝ) in 0..c.pulseLength, pulseWeight c y * f y ^ 2 ≤ 13 * M ^ 2

theorem NavierStokes.PulseAmplitude.weighted_product_bound (c : OutgoingSchedule.Parameters) (f g : ℝ → ℝ) (M : ℝ) (hM : 0 ≤ M) (hf : ∀ (y : ℝ), |f y| ≤ M) (hg : ∀ (y : ℝ), |g y| ≤ M) : |c.lam * ∫ (y : ℝ) in 0..c.pulseLength, pulseWeight c y * f y * g y| ≤ 13 * M ^ 2

theorem NavierStokes.PulseAmplitude.etaPolynomial_hasDerivAt (eta : ℝ) : HasDerivAt etaPolynomial (1 + 3 * eta ^ 2) eta

theorem NavierStokes.PulseAmplitude.etaPolynomial_bounds {eta : ℝ} (heta : eta ^ 2 ≤ 1) : |etaPolynomial eta| ≤ 2 ∧ |deriv etaPolynomial eta| ≤ 4

theorem NavierStokes.PulseAmplitude.quadratic_root_bracket {a b c r : ℝ} (ha : 1 / 5 ≤ a) (ha' : a ≤ 13 / 50) (hb : |b| ≤ 1 / 100) (hc : -(13 / 50) ≤ c) (hc' : c ≤ -(23 / 100)) (hr : 0 < r) (heq : a * r ^ 2 + b * r + c = 0) : 9 / 10 < r ∧ r < 6 / 5

theorem NavierStokes.PulseAmplitude.amplitude_derivative_identity (d : OutgoingTail.TailData) (eta : ℝ) (hc : constantTerm d eta < -(1 / 5)) : (2 * quadraticCoefficient d.core * amplitude d eta + linearTerm d.core eta) * deriv (amplitude d) eta + deriv (linearTerm d.core) eta * amplitude d eta + deriv (constantTerm d) eta = 0

theorem NavierStokes.PulseAmplitude.prefixRepair_eq_affineProfile (c : OutgoingSchedule.Parameters) (y : ℝ) : prefixRepair c y = OutgoingPulseBounds.affineProfile c 1 0 y

theorem NavierStokes.PulseAmplitude.amplitudeRepair_eq_affineProfile (c : OutgoingSchedule.Parameters) (y : ℝ) : amplitudeRepair c y = OutgoingPulseBounds.affineProfile c 0 1 y

theorem NavierStokes.PulseAmplitude.repairBasis_bound (c : OutgoingSchedule.Parameters) (hsmall : c.lam ≤ 1 / 120) (y : ℝ) : |prefixRepair c y| ≤ OutgoingPulseBounds.correctionJetBound c.P c.m 0 * Real.exp (-(1 / (4 * c.lam))) ∧ |amplitudeRepair c y| ≤ OutgoingPulseBounds.correctionJetBound c.P c.m 0 * Real.exp (-(1 / (4 * c.lam)))

theorem NavierStokes.PulseAmplitude.exp_inverse_bound {lam : ℝ} (hlam : 0 < lam) : Real.exp (-(1 / (4 * lam))) ^ 2 ≤ 4 * lam

noncomputable def NavierStokes.PulseAmplitude.correctionEnergyConstant (P m : ℝ) : ℝ

Correction energy constant, given by 104 * OutgoingPulseBounds.correctionJetBound P m 0 ^ 2.

Equations

• NavierStokes.PulseAmplitude.correctionEnergyConstant P m = 104 * NavierStokes.OutgoingPulseBounds.correctionJetBound P m 0 ^ 2

theorem NavierStokes.PulseAmplitude.correctionEnergyConstant_pos {P : ℝ} (hP : 0 < P) (m : ℝ) : 0 < correctionEnergyConstant P m

theorem NavierStokes.PulseAmplitude.correctionEnergy_bounds (c : OutgoingSchedule.Parameters) (hsmall : c.lam ≤ 1 / 120) : 0 ≤ quadraticCoefficient c - pulseConstant ∧ quadraticCoefficient c - pulseConstant ≤ correctionEnergyConstant c.P c.m * c.lam ∧ |linearCoefficient c| ≤ correctionEnergyConstant c.P c.m * c.lam ∧ 0 ≤ constantCorrection c ∧ constantCorrection c ≤ correctionEnergyConstant c.P c.m * c.lam

noncomputable def NavierStokes.PulseAmplitude.errorConstant (P m : ℝ) : ℝ

Error constant, given by 1 + prefixBoundConstant P m + correctionEnergyConstant P m + 2 * OutgoingTail.flattenLength + 4 * TailEnergyBounds.tailConstant.

Equations

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

theorem NavierStokes.PulseAmplitude.errorConstant_pos {P : ℝ} (hP : 0 < P) (m : ℝ) : 0 < errorConstant P m

theorem NavierStokes.PulseAmplitude.errorConstant_ge {P : ℝ} (hP : 0 < P) (m : ℝ) : prefixBoundConstant P m ≤ errorConstant P m ∧ correctionEnergyConstant P m ≤ errorConstant P m ∧ TailEnergyBounds.tailConstant / 2 ≤ errorConstant P m ∧ OutgoingTail.flattenLength + 2 * TailEnergyBounds.tailConstant ≤ errorConstant P m

noncomputable def NavierStokes.PulseAmplitude.errorScale (c : OutgoingSchedule.Parameters) : ℝ

Error scale, given by errorConstant c.P c.m * logarithmicRate c.lam.

Equations

• NavierStokes.PulseAmplitude.errorScale c = NavierStokes.PulseAmplitude.errorConstant c.P c.m * NavierStokes.PulseAmplitude.logarithmicRate c.lam

theorem NavierStokes.PulseAmplitude.errorScale_pos (c : OutgoingSchedule.Parameters) : 0 < errorScale c

structure NavierStokes.PulseAmplitude.EnergyErrorBounds (d : OutgoingTail.TailData) (eta e : ℝ) : Prop

Bounds on the actual integral coefficients. This proposition is proved from the explicit schedule in actual_energy_error_bounds below.

• scale_nonneg : 0 ≤ e
• quadratic_error : quadraticCoefficient d.core - pulseConstant ≤ e
• linear_error : |linearCoefficient d.core| ≤ e
• correction_nonneg : 0 ≤ constantCorrection d.core
• correction_error : constantCorrection d.core ≤ e
• prefix_axial_nonneg : 0 ≤ normalizedPrefixAxial d.core
• prefix_axial_error : normalizedPrefixAxial d.core ≤ e
• prefix_angular_nonneg : 0 ≤ normalizedPrefixAngular d.core
• prefix_angular_error : normalizedPrefixAngular d.core ≤ e
• tail_nonneg : 0 ≤ normalizedTail d eta
• tail_error : normalizedTail d eta ≤ e

theorem NavierStokes.PulseAmplitude.actual_energy_error_bounds (d : OutgoingTail.TailData) (hsmall : d.core.lam ≤ 1 / 120) (hwait : d.core.wait = 60 * Real.log (1 / d.core.lam)) (eta : ℝ) (heta : eta ^ 2 ≤ 1) : EnergyErrorBounds d eta (errorScale d.core)

theorem NavierStokes.PulseAmplitude.numerical_coefficient_bounds (d : OutgoingTail.TailData) (eta e : ℝ) (heta : eta ^ 2 ≤ 1) (h : EnergyErrorBounds d eta e) (he : e ≤ 1 / 1000) : 1 / 5 ≤ quadraticCoefficient d.core ∧ quadraticCoefficient d.core ≤ 13 / 50 ∧ |linearTerm d.core eta| ≤ 1 / 100 ∧ -(13 / 50) ≤ constantTerm d eta ∧ constantTerm d eta ≤ -(23 / 100)

theorem NavierStokes.PulseAmplitude.amplitude_spec_of_error_bound (d : OutgoingTail.TailData) (eta e : ℝ) (heta : eta ^ 2 ≤ 1) (h : EnergyErrorBounds d eta e) (he : e ≤ 1 / 1000) : 9 / 10 < amplitude d eta ∧ amplitude d eta < 6 / 5 ∧ totalEnergy d (amplitude d eta) eta = 0

theorem NavierStokes.PulseAmplitude.normalizedTail_derivative_bound (d : OutgoingTail.TailData) (eta : ℝ) (heta : eta ^ 2 ≤ 1) : |deriv (normalizedTail d) eta| ≤ errorScale d.core

theorem NavierStokes.PulseAmplitude.linearTerm_hasDerivAt (c : OutgoingSchedule.Parameters) (eta : ℝ) : HasDerivAt (linearTerm c) (linearCoefficient c * (1 + 3 * eta ^ 2)) eta

theorem NavierStokes.PulseAmplitude.constantTerm_hasDerivAt (d : OutgoingTail.TailData) (eta : ℝ) : HasDerivAt (constantTerm d) (2 * (constantCorrection d.core + normalizedPrefixAxial d.core) * etaPolynomial eta * (1 + 3 * eta ^ 2) - deriv (normalizedTail d) eta) eta

theorem NavierStokes.PulseAmplitude.coefficient_derivative_bounds (d : OutgoingTail.TailData) (eta e : ℝ) (heta : eta ^ 2 ≤ 1) (h : EnergyErrorBounds d eta e) (hT : |deriv (normalizedTail d) eta| ≤ e) : |deriv (linearTerm d.core) eta| ≤ 4 * e ∧ |deriv (constantTerm d) eta| ≤ 33 * e

theorem NavierStokes.PulseAmplitude.amplitude_derivative_bound_of_error (d : OutgoingTail.TailData) (eta e : ℝ) (heta : eta ^ 2 ≤ 1) (h : EnergyErrorBounds d eta e) (he : e ≤ 1 / 1000) (hT : |deriv (normalizedTail d) eta| ≤ e) : |deriv (amplitude d) eta| ≤ 128 * e

theorem NavierStokes.PulseAmplitude.logarithmicRate_tendsto_zero : Filter.Tendsto logarithmicRate (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

theorem NavierStokes.PulseAmplitude.exists_rate_threshold (C : ℝ) : ∃ (delta : ℝ), 0 < delta ∧ ∀ (lam : ℝ), 0 < lam → lam < delta → C * logarithmicRate lam ≤ 1 / 1000

theorem NavierStokes.PulseAmplitude.energyPolynomial_strictMonoOn (d : OutgoingTail.TailData) (eta e : ℝ) (heta : eta ^ 2 ≤ 1) (h : EnergyErrorBounds d eta e) (he : e ≤ 1 / 1000) : StrictMonoOn (fun (A : ℝ) => energyPolynomial d A eta) (Set.Ici (9 / 10))

theorem NavierStokes.PulseAmplitude.amplitude_unique (d : OutgoingTail.TailData) (eta e : ℝ) (heta : eta ^ 2 ≤ 1) (h : EnergyErrorBounds d eta e) (he : e ≤ 1 / 1000) (A : ℝ) (hA : A ∈ Set.Icc (9 / 10) (6 / 5)) (hzero : totalEnergy d A eta = 0) : A = amplitude d eta

theorem NavierStokes.PulseAmplitude.axial_eq_of_amplitude_eq (c : OutgoingSchedule.Parameters) (amp₁ amp₂ : ℝ → ℝ) (eta y : ℝ) (hamp : amp₁ eta = amp₂ eta) : OutgoingSchedule.axial c amp₁ (y, eta) = OutgoingSchedule.axial c amp₂ (y, eta)

theorem NavierStokes.PulseAmplitude.realized_energy_eq (d : OutgoingTail.TailData) (eta : ℝ) : ∫ (y : ℝ), Real.exp y * (OutgoingSchedule.axial d.core (amplitude d) (y, eta) ^ 2 - OutgoingTail.finalAngular d (y, eta) ^ 2 / 2) = totalEnergy d (amplitude d eta) eta

theorem NavierStokes.PulseAmplitude.amplitude_spec (d : OutgoingTail.TailData) (hsmall : d.core.lam ≤ 1 / 120) (hwait : d.core.wait = 60 * Real.log (1 / d.core.lam)) (hscale : errorScale d.core ≤ 1 / 1000) : ContDiff ℝ (↑⊤) (amplitude d) ∧ ∀ (eta : ℝ), eta ^ 2 ≤ 1 → 9 / 10 < amplitude d eta ∧ amplitude d eta < 6 / 5 ∧ ∫ (y : ℝ), Real.exp y * (OutgoingSchedule.axial d.core (amplitude d) (y, eta) ^ 2 - OutgoingTail.finalAngular d (y, eta) ^ 2 / 2) = 0 ∧ |deriv (amplitude d) eta| ≤ 128 * errorScale d.core ∧ ∀ A ∈ Set.Icc (9 / 10) (6 / 5), totalEnergy d A eta = 0 → A = amplitude d eta

All smallness conditions refer to proved explicit constants and the actual schedule parameter. The amplitude is a concrete globally C∞ function.

theorem NavierStokes.PulseAmplitude.exists_uniform_amplitude_threshold (P m : ℝ) (hP : 0 < P) : ∃ (lam₀ : ℝ) (C : ℝ), 0 < lam₀ ∧ 0 < C ∧ ∀ (d : OutgoingTail.TailData), d.core.P = P → d.core.m = m → d.core.wait = 60 * Real.log (1 / d.core.lam) → d.core.lam < lam₀ → ContDiff ℝ (↑⊤) (amplitude d) ∧ ∀ (eta : ℝ), eta ^ 2 ≤ 1 → 9 / 10 < amplitude d eta ∧ amplitude d eta < 6 / 5 ∧ ∫ (y : ℝ), Real.exp y * (OutgoingSchedule.axial d.core (amplitude d) (y, eta) ^ 2 - OutgoingTail.finalAngular d (y, eta) ^ 2 / 2) = 0 ∧ |deriv (amplitude d) eta| ≤ C * d.core.lam * (1 + Real.log (1 / d.core.lam)) ∧ ∀ A ∈ Set.Icc (9 / 10) (6 / 5), totalEnergy d A eta = 0 → A = amplitude d eta

One threshold works for all terminal parameters 0 < h < lam/2. The constructed core with OutgoingTail.finalAngular has zero total energy, with an actual smooth amplitude in the manuscript's bracket and the claimed derivative rate. The separate angular-moment reset is not included here.

The same equality in the actual radial variable

theorem NavierStokes.PulseAmplitude.energyIntegrand_integrable (d : OutgoingTail.TailData) (A eta : ℝ) : MeasureTheory.Integrable (energyIntegrand d A eta) MeasureTheory.volume

noncomputable def NavierStokes.PulseAmplitude.radialEnergyIntegrand (d : OutgoingTail.TailData) (amp : ℝ → ℝ) (eta XR X : ℝ) : ℝ

Radial energy integrand, given by axial d.core amp (Real.log (X / XR), eta) ^ 2 - OutgoingTail.finalAngular d (Real.log (X / XR), eta) ^ 2 / 2.

Equations

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

theorem NavierStokes.PulseAmplitude.radialEnergy_integrable (d : OutgoingTail.TailData) (amp : ℝ → ℝ) (eta XR : ℝ) (hXR : 0 < XR) : MeasureTheory.IntegrableOn (radialEnergyIntegrand d amp eta XR) (Set.Ioi 0) MeasureTheory.volume

theorem NavierStokes.PulseAmplitude.radialEnergy_integral (d : OutgoingTail.TailData) (amp : ℝ → ℝ) (eta XR : ℝ) (hXR : 0 < XR) : ∫ (X : ℝ) in Set.Ioi 0, radialEnergyIntegrand d amp eta XR X = XR * totalEnergy d (amp eta) eta

theorem NavierStokes.PulseAmplitude.radialEnergy_zero (d : OutgoingTail.TailData) (hsmall : d.core.lam ≤ 1 / 120) (hwait : d.core.wait = 60 * Real.log (1 / d.core.lam)) (hscale : errorScale d.core ≤ 1 / 1000) (eta : ℝ) (heta : eta ^ 2 ≤ 1) (XR : ℝ) (hXR : 0 < XR) : ∫ (X : ℝ) in Set.Ioi 0, radialEnergyIntegrand d (amplitude d) eta XR X = 0