Uniform future-pressure bounds for the actual outgoing schedule

The estimates concern OutgoingTail.finalAngular, rather than a profile with an assumed envelope. Its clock decay is obtained directly from the prescribed slopes, including the first unit ramp. Angular derivatives are derivatives of the actual improper integral.

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

The logarithm of the clock factor, omitting its positive constant prefactor.

Equations

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

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

Clock slope, constructed using slope.

Equations

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

theorem NavierStokes.FuturePressureBounds.logClock_hasDerivAt (d : OutgoingTail.TailData) (y : ℝ) : HasDerivAt (logClock d) (clockSlope d y) y

theorem NavierStokes.FuturePressureBounds.logClock_differentiable (d : OutgoingTail.TailData) : Differentiable ℝ (logClock d)

theorem NavierStokes.FuturePressureBounds.clockSlope_le (d : OutgoingTail.TailData) (y : ℝ) : clockSlope d y ≤ 1 / 5

theorem NavierStokes.FuturePressureBounds.clockSlope_le_after_one (d : OutgoingTail.TailData) {y : ℝ} (hy : 1 ≤ y) : clockSlope d y ≤ -(2 / 5)

theorem NavierStokes.FuturePressureBounds.logClock_increment (d : OutgoingTail.TailData) {y t : ℝ} (hyt : y ≤ t) : logClock d t - logClock d y ≤ 1 / 5 * (t - y)

theorem NavierStokes.FuturePressureBounds.logClock_increment_after_one (d : OutgoingTail.TailData) {y t : ℝ} (hy : 1 ≤ y) (hyt : y ≤ t) : logClock d t - logClock d y ≤ -(2 / 5) * (t - y)

theorem NavierStokes.FuturePressureBounds.logClock_future (d : OutgoingTail.TailData) {y t : ℝ} (hy : 0 ≤ y) (hyt : y ≤ t) : logClock d t - logClock d y ≤ 3 / 5 - 2 / 5 * (t - y)

The first unit ramp costs at most 3/5 in the logarithmic envelope.

theorem NavierStokes.FuturePressureBounds.finalAngular_clock_eq (d : OutgoingTail.TailData) (y : ℝ) : OutgoingTail.finalAngular d (y, 0) = d.core.P / (1 - d.rho) * Real.exp (logClock d y)

theorem NavierStokes.FuturePressureBounds.finalAngular_clock_ratio (d : OutgoingTail.TailData) (y t : ℝ) : OutgoingTail.finalAngular d (t, 0) = OutgoingTail.finalAngular d (y, 0) * Real.exp (logClock d t - logClock d y)

theorem NavierStokes.FuturePressureBounds.clock_future_bound (d : OutgoingTail.TailData) {y t : ℝ} (hy : 0 ≤ y) (hyt : y ≤ t) : SchedulePressure.clockWeight d t ≤ SchedulePressure.clockWeight d y * Real.exp (6 / 5) * Real.exp (-(4 / 5) * (t - y))

theorem NavierStokes.FuturePressureBounds.future_clock_integral_le (d : OutgoingTail.TailData) {y : ℝ} (hy : 0 ≤ y) : ∫ (t : ℝ) in Set.Ioi y, SchedulePressure.clockWeight d t ≤ 5 / 4 * Real.exp (6 / 5) * SchedulePressure.clockWeight d y

theorem NavierStokes.FuturePressureBounds.angular_square_le_clock (d : OutgoingTail.TailData) (t eta : ℝ) : OutgoingTail.finalAngular d (t, eta) ^ 2 ≤ SchedulePressure.clockWeight d t

theorem NavierStokes.FuturePressureBounds.clock_le_four_angular_square (d : OutgoingTail.TailData) (y : ℝ) {eta : ℝ} (heta : |eta| ≤ 1) : SchedulePressure.clockWeight d y ≤ 4 * OutgoingTail.finalAngular d (y, eta) ^ 2

noncomputable def NavierStokes.FuturePressureBounds.envelopeConstant : ℝ

A single numerical constant, independent of every schedule parameter.

Equations

• NavierStokes.FuturePressureBounds.envelopeConstant = 5 * Real.exp (6 / 5)

theorem NavierStokes.FuturePressureBounds.envelopeConstant_pos : 0 < envelopeConstant

theorem NavierStokes.FuturePressureBounds.future_square_integral_le (d : OutgoingTail.TailData) {y eta : ℝ} (hy : 0 ≤ y) (heta : |eta| ≤ 1) : ∫ (t : ℝ) in Set.Ioi y, OutgoingTail.finalAngular d (t, eta) ^ 2 ≤ envelopeConstant * OutgoingTail.finalAngular d (y, eta) ^ 2

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

The canonical pressure from the actual future of the clean outgoing field.

Equations

• NavierStokes.FuturePressureBounds.Pi d y eta = -(1 / 2) * ∫ (t : ℝ) in Set.Ioi y, NavierStokes.OutgoingTail.finalAngular d (t, eta) ^ 2

noncomputable def NavierStokes.FuturePressureBounds.futureMass (d : OutgoingTail.TailData) (y : ℝ) (n : ℕ) (eta : ℝ) : ℝ

The moment indexed by the nonnegative shape exponent.

Equations

• NavierStokes.FuturePressureBounds.futureMass d y n eta = ∫ (t : ℝ) in Set.Ioi y, NavierStokes.SchedulePressure.shapeExponent d t ^ n * NavierStokes.OutgoingTail.finalAngular d (t, eta) ^ 2

noncomputable def NavierStokes.FuturePressureBounds.futureWeight (d : OutgoingTail.TailData) (y : ℝ) (n : ℕ) (t : ℝ) : ℝ

Future weight, given by (Ioi y).indicator (clockWeight d) t * shapeExponent d t ^ n.

Equations

• NavierStokes.FuturePressureBounds.futureWeight d y n t = (Set.Ioi y).indicator (NavierStokes.SchedulePressure.clockWeight d) t * NavierStokes.SchedulePressure.shapeExponent d t ^ n

theorem NavierStokes.FuturePressureBounds.futureWeight_admissible (d : OutgoingTail.TailData) (y : ℝ) (n : ℕ) : PressureDatum.Admissible (futureWeight d y n) (SchedulePressure.shapeExponent d) 1

theorem NavierStokes.FuturePressureBounds.futureMass_eq (d : OutgoingTail.TailData) (y : ℝ) (n : ℕ) (eta : ℝ) : futureMass d y n eta = ∫ (t : ℝ), futureWeight d y n t * PressureDatum.kernel (SchedulePressure.shapeExponent d t) eta

theorem NavierStokes.FuturePressureBounds.futureMass_pressure (d : OutgoingTail.TailData) (y : ℝ) (n : ℕ) : futureMass d y n = fun (eta : ℝ) => -2 * PressureDatum.pressure (futureWeight d y n) (SchedulePressure.shapeExponent d) eta

theorem NavierStokes.FuturePressureBounds.Pi_eq_pressure (d : OutgoingTail.TailData) (y : ℝ) : Pi d y = PressureDatum.pressure (futureWeight d y 0) (SchedulePressure.shapeExponent d)

theorem NavierStokes.FuturePressureBounds.Pi_contDiff_eta (d : OutgoingTail.TailData) (y : ℝ) : ContDiff ℝ (↑⊤) (Pi d y)

theorem NavierStokes.FuturePressureBounds.futureMass_nonneg (d : OutgoingTail.TailData) (y : ℝ) (n : ℕ) (eta : ℝ) : 0 ≤ futureMass d y n eta

theorem NavierStokes.FuturePressureBounds.futureMass_le_zero (d : OutgoingTail.TailData) (y : ℝ) (n : ℕ) (eta : ℝ) : futureMass d y n eta ≤ futureMass d y 0 eta

theorem NavierStokes.FuturePressureBounds.Pi_nonpos (d : OutgoingTail.TailData) (y eta : ℝ) : Pi d y eta ≤ 0

theorem NavierStokes.FuturePressureBounds.Pi_abs_eq (d : OutgoingTail.TailData) (y eta : ℝ) : |Pi d y eta| = 1 / 2 * futureMass d y 0 eta

theorem NavierStokes.FuturePressureBounds.Pi_abs_le (d : OutgoingTail.TailData) {y eta : ℝ} (hy : 0 ≤ y) (heta : |eta| ≤ 1) : |Pi d y eta| ≤ envelopeConstant / 2 * OutgoingTail.finalAngular d (y, eta) ^ 2

theorem NavierStokes.FuturePressureBounds.futureMass_hasDerivAt (d : OutgoingTail.TailData) (y : ℝ) (n : ℕ) (eta : ℝ) : HasDerivAt (futureMass d y n) (-4 * eta / (1 + eta ^ 2) * futureMass d y (n + 1) eta) eta

theorem NavierStokes.FuturePressureBounds.Pi_hasDerivAt_eta (d : OutgoingTail.TailData) (y eta : ℝ) : HasDerivAt (Pi d y) (2 * eta / (1 + eta ^ 2) * futureMass d y 1 eta) eta

theorem NavierStokes.FuturePressureBounds.Pi_deriv_eta (d : OutgoingTail.TailData) (y eta : ℝ) : deriv (Pi d y) eta = 2 * eta / (1 + eta ^ 2) * futureMass d y 1 eta

theorem NavierStokes.FuturePressureBounds.Pi_second_hasDerivAt_eta (d : OutgoingTail.TailData) (y eta : ℝ) : HasDerivAt (deriv (Pi d y)) (2 * (1 - eta ^ 2) / (1 + eta ^ 2) ^ 2 * futureMass d y 1 eta - 8 * eta ^ 2 / (1 + eta ^ 2) ^ 2 * futureMass d y 2 eta) eta

theorem NavierStokes.FuturePressureBounds.Pi_second_deriv_eta (d : OutgoingTail.TailData) (y eta : ℝ) : deriv (deriv (Pi d y)) eta = 2 * (1 - eta ^ 2) / (1 + eta ^ 2) ^ 2 * futureMass d y 1 eta - 8 * eta ^ 2 / (1 + eta ^ 2) ^ 2 * futureMass d y 2 eta

theorem NavierStokes.FuturePressureBounds.Pi_deriv_abs_le_pressure (d : OutgoingTail.TailData) (y eta : ℝ) : |deriv (Pi d y) eta| ≤ 4 * |eta| * |Pi d y eta|

The angular derivative retains its factor |eta| on the entire real axis.

theorem NavierStokes.FuturePressureBounds.Pi_deriv_abs_le (d : OutgoingTail.TailData) {y eta : ℝ} (hy : 0 ≤ y) (heta : |eta| ≤ 1) : |deriv (Pi d y) eta| ≤ 2 * envelopeConstant * |eta| * OutgoingTail.finalAngular d (y, eta) ^ 2

theorem NavierStokes.FuturePressureBounds.Pi_second_deriv_abs_le_pressure (d : OutgoingTail.TailData) (y : ℝ) {eta : ℝ} (heta : |eta| ≤ 1) : |deriv (deriv (Pi d y)) eta| ≤ 20 * |Pi d y eta|

theorem NavierStokes.FuturePressureBounds.Pi_second_deriv_abs_le (d : OutgoingTail.TailData) {y eta : ℝ} (hy : 0 ≤ y) (heta : |eta| ≤ 1) : |deriv (deriv (Pi d y)) eta| ≤ 10 * envelopeConstant * OutgoingTail.finalAngular d (y, eta) ^ 2

theorem NavierStokes.FuturePressureBounds.Pi_increment (d : OutgoingTail.TailData) (a y eta : ℝ) : Pi d y eta = Pi d a eta + 1 / 2 * ∫ (t : ℝ) in a..y, OutgoingTail.finalAngular d (t, eta) ^ 2

An exact finite-history expression, valid even when the endpoint is negative.

theorem NavierStokes.FuturePressureBounds.Pi_hasDerivAt_y (d : OutgoingTail.TailData) (y eta : ℝ) : HasDerivAt (fun (t : ℝ) => Pi d t eta) (1 / 2 * OutgoingTail.finalAngular d (y, eta) ^ 2) y

theorem NavierStokes.FuturePressureBounds.Pi_deriv_y (d : OutgoingTail.TailData) (y eta : ℝ) : deriv (fun (t : ℝ) => Pi d t eta) y = 1 / 2 * OutgoingTail.finalAngular d (y, eta) ^ 2

theorem NavierStokes.FuturePressureBounds.Pi_eq_axisPressure_add (d : OutgoingTail.TailData) (y eta : ℝ) : Pi d y eta = SchedulePressure.axisPressure d eta + 1 / 2 * ∫ (t : ℝ) in Set.Iic y, OutgoingTail.finalAngular d (t, eta) ^ 2

theorem NavierStokes.FuturePressureBounds.ideal_left_integral (d : OutgoingTail.TailData) (eta : ℝ) : ∫ (t : ℝ) in Set.Iic 0, OutgoingTail.finalAngular d (t, eta) ^ 2 = 5 * d.core.P ^ 2 * OutgoingSchedule.shape eta ^ 2

theorem NavierStokes.FuturePressureBounds.Pi_zero (d : OutgoingTail.TailData) (eta : ℝ) : Pi d 0 eta = SchedulePressure.axisPressure d eta + 5 / 2 * d.core.P ^ 2 * OutgoingSchedule.shape eta ^ 2

theorem NavierStokes.FuturePressureBounds.Pi_eq_radial_history (d : OutgoingTail.TailData) {y : ℝ} (hy : 0 ≤ y) (hyend : y ≤ d.core.endpoint) (eta : ℝ) : Pi d y eta = SchedulePressure.axisPressure d eta + OutgoingSchedule.shape eta ^ 2 * (5 / 2 * d.core.P ^ 2 + 1 / 2 * ∫ (t : ℝ) in 0..y, OutgoingSchedule.radialAmplitude d.core.P d.core.dropLength d.core.lam t ^ 2)

The exact bridge to the initial ramp/drop pressure history.

theorem NavierStokes.FuturePressureBounds.future_integral_unchanged {f g : ℝ → ℝ} {y : ℝ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hzero : ∫ (t : ℝ), f t - g t = 0) (hbefore : ∀ t ≤ y, f t = g t) : ∫ (t : ℝ) in Set.Ioi y, f t = ∫ (t : ℝ) in Set.Ioi y, g t

A future-supported edit with zero total integral has zero future integral.

theorem NavierStokes.FuturePressureBounds.corrected_square_integrable {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) : MeasureTheory.Integrable (fun (t : ℝ) => UniformAngularReset.correctedAngular d w.coefficients (t, eta) ^ 2) MeasureTheory.volume

theorem NavierStokes.FuturePressureBounds.corrected_future_integral_eq {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {y : ℝ} (hy : y ≤ d.releaseStart - 4) (eta : ℝ) : ∫ (t : ℝ) in Set.Ioi y, UniformAngularReset.correctedAngular d w.coefficients (t, eta) ^ 2 = ∫ (t : ℝ) in Set.Ioi y, OutgoingTail.finalAngular d (t, eta) ^ 2

The actual pressure-neutral angular reset may be omitted before its support.

theorem NavierStokes.FuturePressureBounds.corrected_future_pressure_eq {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {y : ℝ} (hy : y ≤ d.releaseStart - 4) (eta : ℝ) : -(1 / 2) * ∫ (t : ℝ) in Set.Ioi y, UniformAngularReset.correctedAngular d w.coefficients (t, eta) ^ 2 = Pi d y eta

theorem NavierStokes.FuturePressureBounds.uniform_pressure_bounds (d : OutgoingTail.TailData) {y eta : ℝ} (hy : 0 ≤ y) (heta : |eta| ≤ 1) : |Pi d y eta| ≤ envelopeConstant / 2 * OutgoingTail.finalAngular d (y, eta) ^ 2 ∧ |deriv (Pi d y) eta| ≤ 2 * envelopeConstant * |eta| * OutgoingTail.finalAngular d (y, eta) ^ 2 ∧ |deriv (deriv (Pi d y)) eta| ≤ 10 * envelopeConstant * OutgoingTail.finalAngular d (y, eta) ^ 2

All three estimates use numerical constants uniform in lambda, h, and the other choices in the constructed schedule.