Pulse amplitude after the actual angular-moment reset

The scalar energy equation here uses UniformAngularReset.correctedAngular. Its signed reset energy is retained in the constant coefficient, and the reset witness and amplitude are constructed together for small lam.

Actual energy cost of the scheduled angular reset

Pressure neutrality has no extra factor exp y. This file instead integrates the actual energy difference, proves its parameter regularity, and uses the constructed reset's small coefficients to bound that difference.

theorem NavierStokes.ResetEnergyBounds.relative_abs_le_two_norm (c : AngularMomentReset.Coeff) (y : ℝ) : |AngularMomentReset.relative c y| ≤ 2 * ‖c‖

theorem NavierStokes.ResetEnergyBounds.relative_coeff_hasDerivAt {c : ℝ → AngularMomentReset.Coeff} {c' : AngularMomentReset.Coeff} {eta : ℝ} (hc : HasDerivAt c c' eta) (u : ℝ) : HasDerivAt (fun (q : ℝ) => AngularMomentReset.relative (c q) u) (AngularMomentReset.relative c' u) eta

noncomputable def NavierStokes.ResetEnergyBounds.resetDensity (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (eta y : ℝ) : ℝ

Reset density, given by Real.exp y * ((correctedAngular d c (y, eta)) ^ 2 - (finalAngular d (y, eta)) ^ 2).

Equations

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

theorem NavierStokes.ResetEnergyBounds.resetDensity_eq (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (eta y : ℝ) : resetDensity d c eta y = TailEnergyBounds.energyDensity d eta y * ((1 + AngularMomentReset.relative (c eta) (y - UniformAngularReset.correctionCenter d)) ^ 2 - 1)

theorem NavierStokes.ResetEnergyBounds.resetDensity_reference (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (eta y : ℝ) : resetDensity d c eta y = Real.exp y * AngularMomentReset.baseE d.core.lam (UniformAngularReset.referenceAmplitude d) y ^ 2 * ((1 + AngularMomentReset.relative (c eta) (y - UniformAngularReset.correctionCenter d)) ^ 2 - 1)

theorem NavierStokes.ResetEnergyBounds.resetDensity_zero (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (eta : ℝ) {y : ℝ} (hy : y ∉ Set.Ioo (d.releaseStart - 4) d.releaseStart) : resetDensity d c eta y = 0

theorem NavierStokes.ResetEnergyBounds.resetDensity_support (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (eta : ℝ) : Function.support (resetDensity d c eta) ⊆ Set.Icc (d.releaseStart - 4) d.releaseStart

theorem NavierStokes.ResetEnergyBounds.resetDensity_contDiff (d : OutgoingTail.TailData) {c : ℝ → AngularMomentReset.Coeff} (hc : ContDiff ℝ (↑⊤) c) : ContDiff ℝ (↑⊤) (Function.uncurry (resetDensity d c))

theorem NavierStokes.ResetEnergyBounds.resetDensity_continuous (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (eta : ℝ) : Continuous (resetDensity d c eta)

theorem NavierStokes.ResetEnergyBounds.resetDensity_integrable (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (eta : ℝ) : MeasureTheory.Integrable (resetDensity d c eta) MeasureTheory.volume

noncomputable def NavierStokes.ResetEnergyBounds.resetEnergy (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (eta : ℝ) : ℝ

Reset energy, given by ∫ y, resetDensity d c eta y.

Equations

• NavierStokes.ResetEnergyBounds.resetEnergy d c eta = ∫ (y : ℝ), NavierStokes.ResetEnergyBounds.resetDensity d c eta y

theorem NavierStokes.ResetEnergyBounds.resetEnergy_eq_interval (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (eta : ℝ) : resetEnergy d c eta = ∫ (y : ℝ) in d.releaseStart - 4..d.releaseStart, resetDensity d c eta y

theorem NavierStokes.ResetEnergyBounds.resetEnergy_contDiff (d : OutgoingTail.TailData) {c : ℝ → AngularMomentReset.Coeff} (hc : ContDiff ℝ (↑⊤) c) : ContDiff ℝ (↑⊤) (resetEnergy d c)

noncomputable def NavierStokes.ResetEnergyBounds.resetDensityEta (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (eta y : ℝ) : ℝ

Reset density eta, constructed using Real.exp.

Equations

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

theorem NavierStokes.ResetEnergyBounds.resetDensity_hasDerivAt (d : OutgoingTail.TailData) {c : ℝ → AngularMomentReset.Coeff} (hc : ContDiff ℝ (↑⊤) c) (eta y : ℝ) : HasDerivAt (fun (q : ℝ) => resetDensity d c q y) (resetDensityEta d c eta y) eta

theorem NavierStokes.ResetEnergyBounds.resetDensityEta_joint_continuous (d : OutgoingTail.TailData) {c : ℝ → AngularMomentReset.Coeff} (hc : ContDiff ℝ (↑⊤) c) : Continuous (Function.uncurry (resetDensityEta d c))

theorem NavierStokes.ResetEnergyBounds.resetEnergy_hasDerivAt (d : OutgoingTail.TailData) {c : ℝ → AngularMomentReset.Coeff} (hc : ContDiff ℝ (↑⊤) c) (eta : ℝ) : HasDerivAt (resetEnergy d c) (∫ (y : ℝ) in d.releaseStart - 4..d.releaseStart, resetDensityEta d c eta y) eta

theorem NavierStokes.ResetEnergyBounds.coefficient_scale_nonneg {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) : 0 ≤ K * d.core.lam ^ 28

theorem NavierStokes.ResetEnergyBounds.relative_bound {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta y : ℝ) : |AngularMomentReset.relative (w.coefficients eta) y| ≤ 2 * (K * d.core.lam ^ 28)

theorem NavierStokes.ResetEnergyBounds.relative_eta_bound {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta y : ℝ) : |AngularMomentReset.relative (deriv w.coefficients eta) y| ≤ 2 * (K * d.core.lam ^ 28)

theorem NavierStokes.ResetEnergyBounds.resetDensity_abs_le {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) (heta : eta ^ 2 ≤ 1) {y : ℝ} (hy : y ∈ Set.Icc (d.releaseStart - 4) d.releaseStart) : |resetDensity d w.coefficients eta y| ≤ 6 * (K * d.core.lam ^ 28) * TailEnergyBounds.energyDensity d eta d.core.endpoint

theorem NavierStokes.ResetEnergyBounds.resetDensityEta_abs_le {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) (heta : eta ^ 2 ≤ 1) {y : ℝ} (hy : y ∈ Set.Icc (d.releaseStart - 4) d.releaseStart) : |resetDensityEta d w.coefficients eta y| ≤ 6 * (K * d.core.lam ^ 28) * TailEnergyBounds.energyDensity d eta d.core.endpoint

theorem NavierStokes.ResetEnergyBounds.resetEnergy_abs_le {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) (heta : eta ^ 2 ≤ 1) : |resetEnergy d w.coefficients eta| ≤ 24 * (K * d.core.lam ^ 28) * TailEnergyBounds.energyDensity d eta d.core.endpoint

theorem NavierStokes.ResetEnergyBounds.resetEnergy_deriv_abs_le {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) (heta : eta ^ 2 ≤ 1) : |deriv (resetEnergy d w.coefficients) eta| ≤ 24 * (K * d.core.lam ^ 28) * TailEnergyBounds.energyDensity d eta d.core.endpoint

Relation to the actual corrected post-pulse energy

theorem NavierStokes.ResetEnergyBounds.corrected_energy_eq (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (eta y : ℝ) : Real.exp y * UniformAngularReset.correctedAngular d c (y, eta) ^ 2 = TailEnergyBounds.energyDensity d eta y + resetDensity d c eta y

theorem NavierStokes.ResetEnergyBounds.corrected_energy_integrable_postPulse (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (eta : ℝ) : MeasureTheory.IntegrableOn (fun (y : ℝ) => Real.exp y * UniformAngularReset.correctedAngular d c (y, eta) ^ 2) (Set.Ioi d.core.endpoint) MeasureTheory.volume

theorem NavierStokes.ResetEnergyBounds.integral_corrected_energy (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (eta : ℝ) : ∫ (y : ℝ) in Set.Ioi d.core.endpoint, Real.exp y * UniformAngularReset.correctedAngular d c (y, eta) ^ 2 = TailEnergyBounds.postPulseEnergy d eta + resetEnergy d c eta

theorem NavierStokes.ResetEnergyBounds.corrected_energy_contDiff (d : OutgoingTail.TailData) {c : ℝ → AngularMomentReset.Coeff} (hc : ContDiff ℝ (↑⊤) c) : ContDiff ℝ ↑⊤ fun (eta : ℝ) => ∫ (y : ℝ) in Set.Ioi d.core.endpoint, Real.exp y * UniformAngularReset.correctedAngular d c (y, eta) ^ 2

Full normalization, including its parameter derivative

noncomputable def NavierStokes.ResetEnergyBounds.pulseNormalization (d : OutgoingTail.TailData) : ℝ

Pulse normalization, given by Real.exp d.core.pulseStart * pulseAmplitude d.core ^ 2.

Equations

• NavierStokes.ResetEnergyBounds.pulseNormalization d = Real.exp d.core.pulseStart * NavierStokes.OutgoingSchedule.pulseAmplitude d.core ^ 2

theorem NavierStokes.ResetEnergyBounds.pulseNormalization_pos (d : OutgoingTail.TailData) : 0 < pulseNormalization d

noncomputable def NavierStokes.ResetEnergyBounds.normalizedResetEnergy (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (eta : ℝ) : ℝ

Normalized reset energy, given by `d.core.lam * resetEnergy d c eta / (pulseNormalization d

• shape eta ^ 2)`.

Equations

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

theorem NavierStokes.ResetEnergyBounds.normalizedResetEnergy_eq (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (eta : ℝ) : normalizedResetEnergy d c eta = d.core.lam / pulseNormalization d * resetEnergy d c eta * (1 + eta ^ 2) ^ 2

theorem NavierStokes.ResetEnergyBounds.normalizedResetEnergy_contDiff (d : OutgoingTail.TailData) {c : ℝ → AngularMomentReset.Coeff} (hc : ContDiff ℝ (↑⊤) c) : ContDiff ℝ (↑⊤) (normalizedResetEnergy d c)

theorem NavierStokes.ResetEnergyBounds.normalizedResetEnergy_hasDerivAt (d : OutgoingTail.TailData) {c : ℝ → AngularMomentReset.Coeff} (hc : ContDiff ℝ (↑⊤) c) (eta : ℝ) : HasDerivAt (normalizedResetEnergy d c) (d.core.lam * deriv (resetEnergy d c) eta / (pulseNormalization d * OutgoingSchedule.shape eta ^ 2) + 4 * eta / (1 + eta ^ 2) * normalizedResetEnergy d c eta) eta

theorem NavierStokes.ResetEnergyBounds.normalizedResetEnergy_abs_le {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) (heta : eta ^ 2 ≤ 1) : |normalizedResetEnergy d w.coefficients eta| ≤ 24 * K * d.core.lam ^ 29

theorem NavierStokes.ResetEnergyBounds.normalized_resetEnergy_deriv_abs_le {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) (heta : eta ^ 2 ≤ 1) : d.core.lam * |deriv (resetEnergy d w.coefficients) eta| / (pulseNormalization d * OutgoingSchedule.shape eta ^ 2) ≤ 24 * K * d.core.lam ^ 29

theorem NavierStokes.ResetEnergyBounds.normalizedResetEnergy_deriv_abs_le {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) (heta : eta ^ 2 ≤ 1) : |deriv (normalizedResetEnergy d w.coefficients) eta| ≤ 72 * K * d.core.lam ^ 29

theorem NavierStokes.ResetEnergyBounds.exists_scheduled_reset_energy_bounds : ∃ (lam0 : ℝ) (K : ℝ) (C : ℝ), 0 < lam0 ∧ 0 < K ∧ 0 < C ∧ ∀ (d : OutgoingTail.TailData), d.core.lam < lam0 → ∃ (w : UniformAngularReset.ResetWitness d K), ContDiff ℝ (↑⊤) (normalizedResetEnergy d w.coefficients) ∧ ∀ (eta : ℝ), eta ^ 2 ≤ 1 → |normalizedResetEnergy d w.coefficients eta| ≤ C * d.core.lam ^ 29 ∧ |deriv (normalizedResetEnergy d w.coefficients) eta| ≤ C * d.core.lam ^ 29

The outgoing schedule supplies the actual correction and all bounds. There is no separate smallness assumption on a chosen correction.

theorem NavierStokes.ResetEnergyBounds.exists_scheduled_reset_small_energy (epsilon : ℝ) (hepsilon : 0 < epsilon) : ∃ (lam0 : ℝ) (K : ℝ), 0 < lam0 ∧ 0 < K ∧ ∀ (d : OutgoingTail.TailData), d.core.lam < lam0 → ∃ (w : UniformAngularReset.ResetWitness d K), ContDiff ℝ (↑⊤) (normalizedResetEnergy d w.coefficients) ∧ ∀ (eta : ℝ), eta ^ 2 ≤ 1 → |normalizedResetEnergy d w.coefficients eta| < epsilon ∧ |deriv (normalizedResetEnergy d w.coefficients) eta| < epsilon

The constructed reset has arbitrarily small normalized energy and first parameter derivative when the common parameter lam is sufficiently small.

noncomputable def NavierStokes.CorrectedPulseAmplitude.energyIntegrand (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (A eta y : ℝ) : ℝ

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

Equations

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

noncomputable def NavierStokes.CorrectedPulseAmplitude.totalEnergy (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (A eta : ℝ) : ℝ

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

Equations

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

theorem NavierStokes.CorrectedPulseAmplitude.energyIntegrand_eq (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (A eta y : ℝ) : energyIntegrand d c A eta y = PulseAmplitude.energyIntegrand d A eta y - ResetEnergyBounds.resetDensity d c eta y / 2

theorem NavierStokes.CorrectedPulseAmplitude.energyIntegrand_integrable (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (A eta : ℝ) : MeasureTheory.Integrable (energyIntegrand d c A eta) MeasureTheory.volume

theorem NavierStokes.CorrectedPulseAmplitude.totalEnergy_eq (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (A eta : ℝ) : totalEnergy d c A eta = PulseAmplitude.totalEnergy d A eta - ResetEnergyBounds.resetEnergy d c eta / 2

noncomputable def NavierStokes.CorrectedPulseAmplitude.energyShift (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (eta : ℝ) : ℝ

Energy shift, given by ResetEnergyBounds.normalizedResetEnergy d c eta / 2.

Equations

• NavierStokes.CorrectedPulseAmplitude.energyShift d c eta = NavierStokes.ResetEnergyBounds.normalizedResetEnergy d c eta / 2

noncomputable def NavierStokes.CorrectedPulseAmplitude.constantTerm (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (eta : ℝ) : ℝ

Constant term, given by PulseAmplitude.constantTerm d eta - energyShift d c eta.

Equations

• NavierStokes.CorrectedPulseAmplitude.constantTerm d c eta = NavierStokes.PulseAmplitude.constantTerm d eta - NavierStokes.CorrectedPulseAmplitude.energyShift d c eta

noncomputable def NavierStokes.CorrectedPulseAmplitude.energyPolynomial (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (A eta : ℝ) : ℝ

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

Equations

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

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

theorem NavierStokes.CorrectedPulseAmplitude.energyShift_contDiff (d : OutgoingTail.TailData) {c : ℝ → AngularMomentReset.Coeff} (hc : ContDiff ℝ (↑⊤) c) : ContDiff ℝ (↑⊤) (energyShift d c)

theorem NavierStokes.CorrectedPulseAmplitude.constantTerm_contDiff (d : OutgoingTail.TailData) {c : ℝ → AngularMomentReset.Coeff} (hc : ContDiff ℝ (↑⊤) c) : ContDiff ℝ (↑⊤) (constantTerm d c)

noncomputable def NavierStokes.CorrectedPulseAmplitude.discriminant (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (eta : ℝ) : ℝ

Discriminant, constructed using PulseAmplitude.linearTerm.

Equations

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

theorem NavierStokes.CorrectedPulseAmplitude.discriminant_pos (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (eta : ℝ) : 0 < discriminant d c eta

noncomputable def NavierStokes.CorrectedPulseAmplitude.amplitude (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (eta : ℝ) : ℝ

Amplitude, given by (-PulseAmplitude.linearTerm d.core eta + Real.sqrt (discriminant d c eta)) / (2 * PulseAmplitude.quadraticCoefficient d.core).

Equations

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

theorem NavierStokes.CorrectedPulseAmplitude.amplitude_contDiff (d : OutgoingTail.TailData) {c : ℝ → AngularMomentReset.Coeff} (hc : ContDiff ℝ (↑⊤) c) : ContDiff ℝ (↑⊤) (amplitude d c)

theorem NavierStokes.CorrectedPulseAmplitude.amplitude_pos (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (eta : ℝ) : 0 < amplitude d c eta

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

theorem NavierStokes.CorrectedPulseAmplitude.amplitude_energy_equation (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (eta : ℝ) (hc : constantTerm d c eta ≤ -(1 / 5)) : energyPolynomial d c (amplitude d c eta) eta = 0

theorem NavierStokes.CorrectedPulseAmplitude.amplitude_totalEnergy_zero (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (eta : ℝ) (hc : constantTerm d c eta ≤ -(1 / 5)) : totalEnergy d c (amplitude d c eta) eta = 0

noncomputable def NavierStokes.CorrectedPulseAmplitude.combinedConstant (P m K : ℝ) : ℝ

Combined constant, given by PulseAmplitude.errorConstant P m + 36 * K + 1.

Equations

• NavierStokes.CorrectedPulseAmplitude.combinedConstant P m K = NavierStokes.PulseAmplitude.errorConstant P m + 36 * K + 1

noncomputable def NavierStokes.CorrectedPulseAmplitude.combinedScale (d : OutgoingTail.TailData) (K : ℝ) : ℝ

Combined scale, given by combinedConstant d.core.P d.core.m K * PulseAmplitude.logarithmicRate d.core.lam.

Equations

• NavierStokes.CorrectedPulseAmplitude.combinedScale d K = NavierStokes.CorrectedPulseAmplitude.combinedConstant d.core.P d.core.m K * NavierStokes.PulseAmplitude.logarithmicRate d.core.lam

theorem NavierStokes.CorrectedPulseAmplitude.combinedConstant_pos {P : ℝ} (hP : 0 < P) (m K : ℝ) (hK : 0 < K) : 0 < combinedConstant P m K

theorem NavierStokes.CorrectedPulseAmplitude.oldScale_le (d : OutgoingTail.TailData) (K : ℝ) (hK : 0 < K) : PulseAmplitude.errorScale d.core ≤ combinedScale d K

theorem NavierStokes.CorrectedPulseAmplitude.power29_le_lambda (d : OutgoingTail.TailData) : d.core.lam ^ 29 ≤ d.core.lam

theorem NavierStokes.CorrectedPulseAmplitude.energyShift_bounds {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (hK : 0 < K) (eta : ℝ) (heta : eta ^ 2 ≤ 1) : |energyShift d w.coefficients eta| ≤ combinedScale d K ∧ |deriv (energyShift d w.coefficients) eta| ≤ combinedScale d K

theorem NavierStokes.CorrectedPulseAmplitude.old_error_bounds (d : OutgoingTail.TailData) (K : ℝ) (hK : 0 < K) (hsmall : d.core.lam ≤ 1 / 120) (hwait : d.core.wait = 60 * Real.log (1 / d.core.lam)) (eta : ℝ) (heta : eta ^ 2 ≤ 1) : PulseAmplitude.EnergyErrorBounds d eta (combinedScale d K)

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

theorem NavierStokes.CorrectedPulseAmplitude.amplitude_spec_of_bounds (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (eta e : ℝ) (heta : eta ^ 2 ≤ 1) (h : PulseAmplitude.EnergyErrorBounds d eta e) (hshift : |energyShift d c eta| ≤ e) (he : e ≤ 1 / 1000) : 9 / 10 < amplitude d c eta ∧ amplitude d c eta < 6 / 5 ∧ totalEnergy d c (amplitude d c eta) eta = 0

theorem NavierStokes.CorrectedPulseAmplitude.amplitude_derivative_identity (d : OutgoingTail.TailData) {c : ℝ → AngularMomentReset.Coeff} (hc : ContDiff ℝ (↑⊤) c) (eta : ℝ) (hneg : constantTerm d c eta < -(1 / 5)) : (2 * PulseAmplitude.quadraticCoefficient d.core * amplitude d c eta + PulseAmplitude.linearTerm d.core eta) * deriv (amplitude d c) eta + deriv (PulseAmplitude.linearTerm d.core) eta * amplitude d c eta + deriv (constantTerm d c) eta = 0

theorem NavierStokes.CorrectedPulseAmplitude.coefficient_derivative_bounds (d : OutgoingTail.TailData) {c : ℝ → AngularMomentReset.Coeff} (hc : ContDiff ℝ (↑⊤) c) (eta e : ℝ) (heta : eta ^ 2 ≤ 1) (h : PulseAmplitude.EnergyErrorBounds d eta e) (hT : |deriv (PulseAmplitude.normalizedTail d) eta| ≤ e) (hs : |deriv (energyShift d c) eta| ≤ e) : |deriv (PulseAmplitude.linearTerm d.core) eta| ≤ 4 * e ∧ |deriv (constantTerm d c) eta| ≤ 34 * e

theorem NavierStokes.CorrectedPulseAmplitude.amplitude_derivative_bound (d : OutgoingTail.TailData) {c : ℝ → AngularMomentReset.Coeff} (hc : ContDiff ℝ (↑⊤) c) (eta e : ℝ) (heta : eta ^ 2 ≤ 1) (h : PulseAmplitude.EnergyErrorBounds d eta e) (hshift : |energyShift d c eta| ≤ e) (he : e ≤ 1 / 1000) (hT : |deriv (PulseAmplitude.normalizedTail d) eta| ≤ e) (hs : |deriv (energyShift d c) eta| ≤ e) : |deriv (amplitude d c) eta| ≤ 128 * e

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

theorem NavierStokes.CorrectedPulseAmplitude.amplitude_unique (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (eta e : ℝ) (heta : eta ^ 2 ≤ 1) (h : PulseAmplitude.EnergyErrorBounds d eta e) (hshift : |energyShift d c eta| ≤ e) (he : e ≤ 1 / 1000) (A : ℝ) (hA : A ∈ Set.Icc (9 / 10) (6 / 5)) (hz : totalEnergy d c A eta = 0) : A = amplitude d c eta

theorem NavierStokes.CorrectedPulseAmplitude.realized_energy_eq (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (eta : ℝ) : ∫ (y : ℝ), Real.exp y * (OutgoingSchedule.axial d.core (amplitude d c) (y, eta) ^ 2 - UniformAngularReset.correctedAngular d c (y, eta) ^ 2 / 2) = totalEnergy d c (amplitude d c eta) eta

noncomputable def NavierStokes.CorrectedPulseAmplitude.radialEnergyIntegrand (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (amp : ℝ → ℝ) (eta XR X : ℝ) : ℝ

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

Equations

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

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

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

theorem NavierStokes.CorrectedPulseAmplitude.amplitude_spec {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (hK : 0 < K) (hsmall : d.core.lam ≤ 1 / 120) (hwait : d.core.wait = 60 * Real.log (1 / d.core.lam)) (hscale : combinedScale d K ≤ 1 / 1000) : ContDiff ℝ (↑⊤) (amplitude d w.coefficients) ∧ ∀ (eta : ℝ), eta ^ 2 ≤ 1 → 9 / 10 < amplitude d w.coefficients eta ∧ amplitude d w.coefficients eta < 6 / 5 ∧ totalEnergy d w.coefficients (amplitude d w.coefficients eta) eta = 0 ∧ |deriv (amplitude d w.coefficients) eta| ≤ 128 * combinedScale d K ∧ ∀ A ∈ Set.Icc (9 / 10) (6 / 5), totalEnergy d w.coefficients A eta = 0 → A = amplitude d w.coefficients eta

The actual reset coefficients and the actual energy estimates suffice; the scalar amplitude has no assumed root or sign-change hypothesis.

theorem NavierStokes.CorrectedPulseAmplitude.exists_corrected_amplitude (P m : ℝ) (hP : 0 < P) : ∃ (lam₀ : ℝ) (K : ℝ) (C : ℝ), 0 < lam₀ ∧ 0 < K ∧ 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₀ → ∃ (w : UniformAngularReset.ResetWitness d K), ContDiff ℝ (↑⊤) (amplitude d w.coefficients) ∧ ∀ (eta : ℝ), eta ^ 2 ≤ 1 → 9 / 10 < amplitude d w.coefficients eta ∧ amplitude d w.coefficients eta < 6 / 5 ∧ totalEnergy d w.coefficients (amplitude d w.coefficients eta) eta = 0 ∧ |deriv (amplitude d w.coefficients) eta| ≤ C * d.core.lam * (1 + Real.log (1 / d.core.lam)) ∧ (∀ (XR : ℝ), 0 < XR → MeasureTheory.IntegrableOn (radialEnergyIntegrand d w.coefficients (amplitude d w.coefficients) eta XR) (Set.Ioi 0) MeasureTheory.volume ∧ ∫ (X : ℝ) in Set.Ioi 0, radialEnergyIntegrand d w.coefficients (amplitude d w.coefficients) eta XR X = 0) ∧ ∀ A ∈ Set.Icc (9 / 10) (6 / 5), totalEnergy d w.coefficients A eta = 0 → A = amplitude d w.coefficients eta

The scheduled angular reset and pulse amplitude are constructed together. The exact radial energy uses the corrected angular profile. The common threshold is uniform over every terminal parameter 0 < h < lam/2.