Energy of the constructed outgoing tail

The integrands in this file are the actual OutgoingTail.finalAngular. The long release plateau is retained in the estimates; bounding the release only by its terminal slope would give an incorrect uniformity claim in h.

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

Energy density, given by Real.exp y * finalAngular d (y, eta) ^ 2.

Equations

• NavierStokes.TailEnergyBounds.energyDensity d eta y = Real.exp y * NavierStokes.OutgoingTail.finalAngular d (y, eta) ^ 2

theorem NavierStokes.TailEnergyBounds.energyDensity_pos (d : OutgoingTail.TailData) (eta y : ℝ) : 0 < energyDensity d eta y

theorem NavierStokes.TailEnergyBounds.energyDensity_continuous (d : OutgoingTail.TailData) (eta : ℝ) : Continuous (energyDensity d eta)

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

Release primitive, given by primitive (releaseSlope d).

Equations

• NavierStokes.TailEnergyBounds.releasePrimitive d = NavierStokes.OutgoingSchedule.primitive (NavierStokes.OutgoingTail.releaseSlope d)

theorem NavierStokes.TailEnergyBounds.releaseAdjustment_eq (d : OutgoingTail.TailData) (t : ℝ) : OutgoingTail.releaseAdjustment d t = releasePrimitive d t + d.core.lam * t

theorem NavierStokes.TailEnergyBounds.primitive_increment_le {g : ℝ → ℝ} (hg : Continuous g) {a b c : ℝ} (hab : a ≤ b) (hc : ∀ t ∈ Set.Icc a b, g t ≤ c) : OutgoingSchedule.primitive g b ≤ OutgoingSchedule.primitive g a + (b - a) * c

theorem NavierStokes.TailEnergyBounds.releasePrimitive_increment_le (d : OutgoingTail.TailData) {a b : ℝ} (hab : a ≤ b) : releasePrimitive d b ≤ releasePrimitive d a - d.h * (b - a)

@[simp]

theorem NavierStokes.TailEnergyBounds.releasePrimitive_zero (d : OutgoingTail.TailData) : releasePrimitive d 0 = 0

theorem NavierStokes.TailEnergyBounds.releasePrimitive_nonpos (d : OutgoingTail.TailData) {t : ℝ} (ht : 0 ≤ t) : releasePrimitive d t ≤ 0

theorem NavierStokes.TailEnergyBounds.releasePrimitive_plateau_le (d : OutgoingTail.TailData) {t : ℝ} (ht : 0 ≤ t) (ht' : t ≤ d.secondRampStart) : releasePrimitive d t ≤ 1 - t

theorem NavierStokes.TailEnergyBounds.releasePrimitive_late_le (d : OutgoingTail.TailData) {t : ℝ} (ht : d.secondRampStart ≤ t) : releasePrimitive d t ≤ -d.longHold - d.h * (t - d.secondRampStart)

theorem NavierStokes.TailEnergyBounds.plateau_suppression (d : OutgoingTail.TailData) : Real.exp (-2 * d.longHold) = d.h ^ 8

theorem NavierStokes.TailEnergyBounds.h_secondRampStart_le (d : OutgoingTail.TailData) : d.h * d.secondRampStart ≤ 4

theorem NavierStokes.TailEnergyBounds.release_exp_bound (d : OutgoingTail.TailData) {t : ℝ} (ht : 0 ≤ t) : Real.exp (2 * releasePrimitive d t) ≤ Real.exp 2 * Real.exp (-2 * t) + d.h ^ 8 * Real.exp 8 * Real.exp (-(2 * d.h) * t)

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

theorem NavierStokes.TailEnergyBounds.tailShape_ratio_sq_le (d : OutgoingTail.TailData) (t : ℝ) : (OutgoingTail.tailShape d t / (1 - d.rho)) ^ 2 ≤ 4

theorem NavierStokes.TailEnergyBounds.energyDensity_release_bound (d : OutgoingTail.TailData) (eta : ℝ) {y : ℝ} (hy : d.releaseStart ≤ y) : energyDensity d eta y ≤ 4 * energyDensity d eta d.releaseStart * (Real.exp 2 * Real.exp (-2 * (y - d.releaseStart)) + d.h ^ 8 * Real.exp 8 * Real.exp (-(2 * d.h) * (y - d.releaseStart)))

The improper release integral

theorem NavierStokes.TailEnergyBounds.integrableOn_shift_exp {a : ℝ} (ha : 0 < a) (R : ℝ) : MeasureTheory.IntegrableOn (fun (y : ℝ) => Real.exp (-a * (y - R))) (Set.Ioi R) MeasureTheory.volume

theorem NavierStokes.TailEnergyBounds.integral_shift_exp {a : ℝ} (ha : 0 < a) (R : ℝ) : ∫ (y : ℝ) in Set.Ioi R, Real.exp (-a * (y - R)) = 1 / a

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

Release envelope, given by Real.exp 2 * Real.exp (-2 * (y - d.releaseStart)) + d.h ^ 8 * Real.exp 8 * Real.exp (-(2 * d.h) * (y - d.releaseStart)).

Equations

• NavierStokes.TailEnergyBounds.releaseEnvelope d y = Real.exp 2 * Real.exp (-2 * (y - d.releaseStart)) + d.h ^ 8 * Real.exp 8 * Real.exp (-(2 * d.h) * (y - d.releaseStart))

theorem NavierStokes.TailEnergyBounds.releaseEnvelope_integrable (d : OutgoingTail.TailData) : MeasureTheory.IntegrableOn (releaseEnvelope d) (Set.Ioi d.releaseStart) MeasureTheory.volume

theorem NavierStokes.TailEnergyBounds.integral_releaseEnvelope (d : OutgoingTail.TailData) : ∫ (y : ℝ) in Set.Ioi d.releaseStart, releaseEnvelope d y = Real.exp 2 / 2 + d.h ^ 7 * Real.exp 8 / 2

noncomputable def NavierStokes.TailEnergyBounds.releaseConstant : ℝ

Release constant, given by 2 * (Real.exp 2 + Real.exp 8).

Equations

• NavierStokes.TailEnergyBounds.releaseConstant = 2 * (Real.exp 2 + Real.exp 8)

theorem NavierStokes.TailEnergyBounds.releaseConstant_pos : 0 < releaseConstant

theorem NavierStokes.TailEnergyBounds.energyDensity_integrable_release (d : OutgoingTail.TailData) (eta : ℝ) : MeasureTheory.IntegrableOn (energyDensity d eta) (Set.Ioi d.releaseStart) MeasureTheory.volume

theorem NavierStokes.TailEnergyBounds.integral_energyDensity_release_le (d : OutgoingTail.TailData) (eta : ℝ) : ∫ (y : ℝ) in Set.Ioi d.releaseStart, energyDensity d eta y ≤ releaseConstant * energyDensity d eta d.releaseStart

The release cost is independent of both h and lam.

Flattening and the uniform wait

theorem NavierStokes.TailEnergyBounds.finalAngular_before_release (d : OutgoingTail.TailData) (eta : ℝ) {y : ℝ} (hy : y ≤ d.releaseStart) : OutgoingTail.finalAngular d (y, eta) = OutgoingTail.flattened d (y, eta)

theorem NavierStokes.TailEnergyBounds.flattenFactor_le_one (d : OutgoingTail.TailData) (eta y : ℝ) (heta : eta ^ 2 ≤ 1) : OutgoingTail.flattenFactor d (y, eta) ≤ 1

theorem NavierStokes.TailEnergyBounds.core_energy_hold (d : OutgoingTail.TailData) (eta : ℝ) {y : ℝ} (hy : d.core.endpoint ≤ y) : Real.exp y * OutgoingSchedule.angular d.core.P d.core.dropLength d.core.lam (y, eta) ^ 2 = energyDensity d eta d.core.endpoint * Real.exp (-2 * d.core.lam * (y - d.core.endpoint))

theorem NavierStokes.TailEnergyBounds.energyDensity_prefix_le (d : OutgoingTail.TailData) (eta : ℝ) (heta : eta ^ 2 ≤ 1) {y : ℝ} (hy : d.core.endpoint ≤ y) (hy' : y ≤ d.releaseStart) : energyDensity d eta y ≤ energyDensity d eta d.core.endpoint

theorem NavierStokes.TailEnergyBounds.endpoint_le_releaseStart (d : OutgoingTail.TailData) : d.core.endpoint ≤ d.releaseStart

theorem NavierStokes.TailEnergyBounds.energyDensity_integrable_postPulse (d : OutgoingTail.TailData) (eta : ℝ) : MeasureTheory.IntegrableOn (energyDensity d eta) (Set.Ioi d.core.endpoint) MeasureTheory.volume

noncomputable def NavierStokes.TailEnergyBounds.postPulseEnergy (d : OutgoingTail.TailData) (eta : ℝ) : ℝ

Post pulse energy, given by ∫ y in Ioi d.core.endpoint, energyDensity d eta y.

Equations

• NavierStokes.TailEnergyBounds.postPulseEnergy d eta = ∫ (y : ℝ) in Set.Ioi d.core.endpoint, NavierStokes.TailEnergyBounds.energyDensity d eta y

theorem NavierStokes.TailEnergyBounds.postPulseEnergy_nonneg (d : OutgoingTail.TailData) (eta : ℝ) : 0 ≤ postPulseEnergy d eta

theorem NavierStokes.TailEnergyBounds.postPulseEnergy_split (d : OutgoingTail.TailData) (eta : ℝ) {a : ℝ} (ha : d.core.endpoint ≤ a) : postPulseEnergy d eta = (∫ (y : ℝ) in d.core.endpoint..a, energyDensity d eta y) + ∫ (y : ℝ) in Set.Ioi a, energyDensity d eta y

theorem NavierStokes.TailEnergyBounds.postPulseEnergy_le_length (d : OutgoingTail.TailData) (eta : ℝ) (heta : eta ^ 2 ≤ 1) : postPulseEnergy d eta ≤ (d.releaseStart - d.core.endpoint + releaseConstant) * energyDensity d eta d.core.endpoint

noncomputable def NavierStokes.TailEnergyBounds.tailConstant : ℝ

Tail constant, given by flattenLength + 30 + releaseConstant.

Equations

• NavierStokes.TailEnergyBounds.tailConstant = NavierStokes.OutgoingTail.flattenLength + 30 + NavierStokes.TailEnergyBounds.releaseConstant

theorem NavierStokes.TailEnergyBounds.tailConstant_pos : 0 < tailConstant

theorem NavierStokes.TailEnergyBounds.postPulseEnergy_le (d : OutgoingTail.TailData) (eta : ℝ) (heta : eta ^ 2 ≤ 1) : postPulseEnergy d eta ≤ tailConstant * (1 + Real.log (1 / d.core.lam)) * energyDensity d eta d.core.endpoint

Actual outgoing energy, with a constant independent of every parameter.

Genuine parameter regularity and derivative bounds

theorem NavierStokes.TailEnergyBounds.energyDensity_contDiff (d : OutgoingTail.TailData) : ContDiff ℝ ↑⊤ fun (p : ℝ × ℝ) => energyDensity d p.1 p.2

theorem NavierStokes.TailEnergyBounds.postPulseEnergy_split_flattenEnd (d : OutgoingTail.TailData) (eta : ℝ) : postPulseEnergy d eta = (∫ (y : ℝ) in d.core.endpoint..d.flattenEnd, energyDensity d eta y) + ∫ (y : ℝ) in Set.Ioi d.flattenEnd, energyDensity d 0 y

theorem NavierStokes.TailEnergyBounds.postPulseEnergy_contDiff (d : OutgoingTail.TailData) : ContDiff ℝ (↑⊤) (postPulseEnergy d)

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

Eta coefficient, given by -(4 * (1 - sigma ((y - d.core.endpoint) / flattenLength)) * eta / (1 + eta ^ 2)).

Equations

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

theorem NavierStokes.TailEnergyBounds.etaCoefficient_continuous (d : OutgoingTail.TailData) (eta : ℝ) : Continuous (etaCoefficient d eta)

theorem NavierStokes.TailEnergyBounds.finalAngular_hasDerivAt_eta (d : OutgoingTail.TailData) (eta y : ℝ) : HasDerivAt (fun (q : ℝ) => OutgoingTail.finalAngular d (y, q)) (-(2 * (1 - OutgoingSchedule.sigma ((y - d.core.endpoint) / OutgoingTail.flattenLength)) * eta / (1 + eta ^ 2)) * OutgoingTail.finalAngular d (y, eta)) eta

theorem NavierStokes.TailEnergyBounds.energyDensity_hasDerivAt_eta (d : OutgoingTail.TailData) (eta y : ℝ) : HasDerivAt (fun (q : ℝ) => energyDensity d q y) (etaCoefficient d eta y * energyDensity d eta y) eta

theorem NavierStokes.TailEnergyBounds.etaCoefficient_abs_le (d : OutgoingTail.TailData) (eta y : ℝ) : |etaCoefficient d eta y| ≤ 2

theorem NavierStokes.TailEnergyBounds.energyDensity_eta_bound (d : OutgoingTail.TailData) (eta y : ℝ) : |etaCoefficient d eta y * energyDensity d eta y| ≤ 2 * energyDensity d eta y

theorem NavierStokes.TailEnergyBounds.integral_energyDensity_hasDerivAt (d : OutgoingTail.TailData) (eta a b : ℝ) : HasDerivAt (fun (q : ℝ) => ∫ (y : ℝ) in a..b, energyDensity d q y) (∫ (y : ℝ) in a..b, etaCoefficient d eta y * energyDensity d eta y) eta

theorem NavierStokes.TailEnergyBounds.postPulseEnergy_hasDerivAt (d : OutgoingTail.TailData) (eta : ℝ) : HasDerivAt (postPulseEnergy d) (∫ (y : ℝ) in d.core.endpoint..d.flattenEnd, etaCoefficient d eta y * energyDensity d eta y) eta

theorem NavierStokes.TailEnergyBounds.abs_deriv_postPulseEnergy_le (d : OutgoingTail.TailData) (eta : ℝ) (heta : eta ^ 2 ≤ 1) : |deriv (postPulseEnergy d) eta| ≤ 2 * OutgoingTail.flattenLength * energyDensity d eta d.core.endpoint

Parameter variation occurs only on the fixed flattening interval.

Relation to the pulse normalization

theorem NavierStokes.TailEnergyBounds.energyDensity_endpoint_eq (d : OutgoingTail.TailData) (eta : ℝ) : energyDensity d eta d.core.endpoint = Real.exp d.core.pulseStart * OutgoingSchedule.pulseAmplitude d.core ^ 2 * OutgoingSchedule.shape eta ^ 2 * Real.exp (-26)

theorem NavierStokes.TailEnergyBounds.energyDensity_endpoint_le (d : OutgoingTail.TailData) (eta : ℝ) : energyDensity d eta d.core.endpoint ≤ Real.exp d.core.pulseStart * OutgoingSchedule.pulseAmplitude d.core ^ 2 * OutgoingSchedule.shape eta ^ 2

theorem NavierStokes.TailEnergyBounds.normalized_postPulseEnergy_le (d : OutgoingTail.TailData) (eta : ℝ) (heta : eta ^ 2 ≤ 1) : d.core.lam * postPulseEnergy d eta / (Real.exp d.core.pulseStart * OutgoingSchedule.pulseAmplitude d.core ^ 2 * OutgoingSchedule.shape eta ^ 2) ≤ tailConstant * d.core.lam * (1 + Real.log (1 / d.core.lam))

theorem NavierStokes.TailEnergyBounds.normalized_deriv_postPulseEnergy_le (d : OutgoingTail.TailData) (eta : ℝ) (heta : eta ^ 2 ≤ 1) : d.core.lam * |deriv (postPulseEnergy d) eta| / (Real.exp d.core.pulseStart * OutgoingSchedule.pulseAmplitude d.core ^ 2 * OutgoingSchedule.shape eta ^ 2) ≤ 2 * OutgoingTail.flattenLength * d.core.lam

Normalization of the derivative of the energy. The derivative of the normalized quotient also has the elementary derivative of shape eta ^ 2.

Differentiating the fully normalized quotient

noncomputable def NavierStokes.TailEnergyBounds.normalizedPostPulseEnergy (d : OutgoingTail.TailData) (eta : ℝ) : ℝ

Normalized post pulse energy, given by d.core.lam * postPulseEnergy d eta / (Real.exp d.core.pulseStart * pulseAmplitude d.core ^ 2 * shape eta ^ 2).

Equations

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

theorem NavierStokes.TailEnergyBounds.normalizedPostPulseEnergy_eq (d : OutgoingTail.TailData) (eta : ℝ) : normalizedPostPulseEnergy d eta = d.core.lam / (Real.exp d.core.pulseStart * OutgoingSchedule.pulseAmplitude d.core ^ 2) * postPulseEnergy d eta * (1 + eta ^ 2) ^ 2

theorem NavierStokes.TailEnergyBounds.normalizedPostPulseEnergy_nonneg (d : OutgoingTail.TailData) (eta : ℝ) : 0 ≤ normalizedPostPulseEnergy d eta

theorem NavierStokes.TailEnergyBounds.normalizedPostPulseEnergy_contDiff (d : OutgoingTail.TailData) : ContDiff ℝ (↑⊤) (normalizedPostPulseEnergy d)

theorem NavierStokes.TailEnergyBounds.normalizedPostPulseEnergy_hasDerivAt (d : OutgoingTail.TailData) (eta : ℝ) : HasDerivAt (normalizedPostPulseEnergy d) (d.core.lam * deriv (postPulseEnergy d) eta / (Real.exp d.core.pulseStart * OutgoingSchedule.pulseAmplitude d.core ^ 2 * OutgoingSchedule.shape eta ^ 2) + 4 * eta / (1 + eta ^ 2) * normalizedPostPulseEnergy d eta) eta

theorem NavierStokes.TailEnergyBounds.abs_deriv_normalizedPostPulseEnergy_le (d : OutgoingTail.TailData) (eta : ℝ) (heta : eta ^ 2 ≤ 1) : |deriv (normalizedPostPulseEnergy d) eta| ≤ (2 * OutgoingTail.flattenLength + 4 * tailConstant) * d.core.lam * (1 + Real.log (1 / d.core.lam))

This is the derivative of the full quotient, including its shape factor.

theorem NavierStokes.TailEnergyBounds.abs_deriv_normalized_postPulseEnergy_le (d : OutgoingTail.TailData) (eta : ℝ) (heta : eta ^ 2 ≤ 1) : |deriv (fun (q : ℝ) => d.core.lam * postPulseEnergy d q / (Real.exp d.core.pulseStart * OutgoingSchedule.pulseAmplitude d.core ^ 2 * OutgoingSchedule.shape q ^ 2)) eta| ≤ (2 * OutgoingTail.flattenLength + 4 * tailConstant) * d.core.lam * (1 + Real.log (1 / d.core.lam))