Actual angular history through the release and terminal tail

The corrected angular field has the exact initial moment required by the release controller. Matching derivatives and initial values identifies its actual integral with each constructed lag solution. The terminal identity then gives the vanishing renormalized angular moment.

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

Corrected weight, given by Real.exp (3 * y / 2) * correctedAngular d c (y, eta).

Equations

• NavierStokes.ReleaseMoments.correctedWeight d c eta y = Real.exp (3 * y / 2) * NavierStokes.UniformAngularReset.correctedAngular d c (y, eta)

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

History, given by (5 / 8) * d.core.P * shape eta + primitive (correctedWeight d c eta) y.

Equations

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

noncomputable def NavierStokes.ReleaseMoments.releaseWeight (d : OutgoingTail.TailData) (y : ℝ) : ℝ

Release weight, given by Real.exp (3 * y / 2) * finalAngular d (y, 0).

Equations

• NavierStokes.ReleaseMoments.releaseWeight d y = Real.exp (3 * y / 2) * NavierStokes.OutgoingTail.finalAngular d (y, 0)

theorem NavierStokes.ReleaseMoments.releaseWeight_contDiff (d : OutgoingTail.TailData) : ContDiff ℝ (↑⊤) (releaseWeight d)

theorem NavierStokes.ReleaseMoments.releaseWeight_pos (d : OutgoingTail.TailData) (y : ℝ) : 0 < releaseWeight d y

theorem NavierStokes.ReleaseMoments.correctedWeight_contDiff (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (hc : ContDiff ℝ (↑⊤) c) (eta : ℝ) : ContDiff ℝ (↑⊤) (correctedWeight d c eta)

theorem NavierStokes.ReleaseMoments.corrected_eq_release (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (eta : ℝ) {y : ℝ} (hy : d.releaseStart ≤ y) : UniformAngularReset.correctedAngular d c (y, eta) = OutgoingTail.finalAngular d (y, 0)

theorem NavierStokes.ReleaseMoments.correctedWeight_eq_release (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (eta : ℝ) {y : ℝ} (hy : d.releaseStart ≤ y) : correctedWeight d c eta y = releaseWeight d y

theorem NavierStokes.ReleaseMoments.correctedWeight_ideal (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (eta : ℝ) {y : ℝ} (hy : y ≤ 0) : correctedWeight d c eta y = d.core.P * OutgoingSchedule.shape eta * Real.exp (8 / 5 * y)

theorem NavierStokes.ReleaseMoments.ResetWitness.history_contDiff_y {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) : ContDiff ℝ (↑⊤) (history d w.coefficients eta)

theorem NavierStokes.ReleaseMoments.ResetWitness.history_hasDerivAt {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta y : ℝ) : HasDerivAt (history d w.coefficients eta) (correctedWeight d w.coefficients eta y) y

theorem NavierStokes.ReleaseMoments.ResetWitness.history_integrable {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {y : ℝ} (hy : 0 ≤ y) : MeasureTheory.IntegrableOn (correctedWeight d w.coefficients eta) (Set.Iic y) MeasureTheory.volume

theorem NavierStokes.ReleaseMoments.ResetWitness.history_eq_integral {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {y : ℝ} (hy : 0 ≤ y) : history d w.coefficients eta y = ∫ (t : ℝ) in Set.Iic y, correctedWeight d w.coefficients eta t

theorem NavierStokes.ReleaseMoments.ResetWitness.history_at_release {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) : history d w.coefficients eta d.releaseStart = releaseWeight d d.releaseStart / (1 - d.core.lam)

theorem NavierStokes.ReleaseMoments.ResetWitness.history_hasDerivAt_release {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {y : ℝ} (hy : d.releaseStart ≤ y) : HasDerivAt (history d w.coefficients eta) (releaseWeight d y) y

theorem NavierStokes.ReleaseMoments.ResetWitness.history_eta_independent {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta eta' : ℝ) {y : ℝ} (hy : d.releaseStart ≤ y) : history d w.coefficients eta y = history d w.coefficients eta' y

theorem NavierStokes.ReleaseMoments.ResetWitness.history_contDiff_eta {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {y : ℝ} (hy : d.releaseStart ≤ y) : ContDiff ℝ ↑⊤ fun (eta : ℝ) => history d w.coefficients eta y

theorem NavierStokes.ReleaseMoments.ResetWitness.history_deriv_eta_zero {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {y : ℝ} (hy : d.releaseStart ≤ y) (eta : ℝ) : deriv (fun (p : ℝ) => history d w.coefficients p y) eta = 0

theorem NavierStokes.ReleaseMoments.releaseWeight_hasDerivAt (d : OutgoingTail.TailData) {y : ℝ} (hy : d.releaseStart ≤ y) : HasDerivAt (releaseWeight d) (releaseWeight d y * (1 + OutgoingTail.profileSlope d y)) y

noncomputable def NavierStokes.ReleaseMoments.momentCandidate (d : OutgoingTail.TailData) (q : ℝ → ℝ) (y : ℝ) : ℝ

Moment candidate, given by (1 + q y) * releaseWeight d y / (1 - d.h).

Equations

• NavierStokes.ReleaseMoments.momentCandidate d q y = (1 + q y) * NavierStokes.ReleaseMoments.releaseWeight d y / (1 - d.h)

theorem NavierStokes.ReleaseMoments.momentCandidate_hasDerivAt (d : OutgoingTail.TailData) (q : ℝ → ℝ) {y : ℝ} (hy : d.releaseStart ≤ y) (hq : HasDerivAt q (-OutgoingTail.profileSlope d y - d.h - (1 + OutgoingTail.profileSlope d y) * q y) y) : HasDerivAt (momentCandidate d q) (releaseWeight d y) y

The lag equation turns the candidate into a primitive of the actual release weight. This is the uniqueness mechanism used below.

theorem NavierStokes.ReleaseMoments.ResetWitness.history_eq_candidate {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) (q : ℝ → ℝ) {a y : ℝ} (ha : d.releaseStart ≤ a) (hay : a ≤ y) (hq : ∀ t ∈ Set.Icc a y, HasDerivAt q (-OutgoingTail.profileSlope d t - d.h - (1 + OutgoingTail.profileSlope d t) * q t) t) (hinit : history d w.coefficients eta a = momentCandidate d q a) : history d w.coefficients eta y = momentCandidate d q y

theorem NavierStokes.ReleaseMoments.tailShapeDeriv_zero_early (d : OutgoingTail.TailData) {t : ℝ} (ht : t ≤ 0) : OutgoingTail.tailShapeDeriv d t = 0

theorem NavierStokes.ReleaseMoments.tailShapeDeriv_zero_late (d : OutgoingTail.TailData) {t : ℝ} (ht : 3 ≤ t) : OutgoingTail.tailShapeDeriv d t = 0

theorem NavierStokes.ReleaseMoments.profileSlope_before_tail (d : OutgoingTail.TailData) {y : ℝ} (hy : y ≤ OutgoingTail.tailStart d) : OutgoingTail.profileSlope d y = OutgoingTail.releaseSlope d (y - d.releaseStart)

theorem NavierStokes.ReleaseMoments.releaseLag_hasDerivAt (d : OutgoingTail.TailData) (t : ℝ) : HasDerivAt (OutgoingTail.releaseLag d) (-OutgoingTail.releaseSlope d t - d.h - (1 + OutgoingTail.releaseSlope d t) * OutgoingTail.releaseLag d t) t

theorem NavierStokes.ReleaseMoments.shifted_releaseLag_hasDerivAt (d : OutgoingTail.TailData) {y : ℝ} (hy : y ≤ OutgoingTail.tailStart d) : HasDerivAt (fun (t : ℝ) => OutgoingTail.releaseLag d (t - d.releaseStart)) (-OutgoingTail.profileSlope d y - d.h - (1 + OutgoingTail.profileSlope d y) * OutgoingTail.releaseLag d (y - d.releaseStart)) y

theorem NavierStokes.ReleaseMoments.ResetWitness.history_release {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {y : ℝ} (hy : d.releaseStart ≤ y) (hy' : y ≤ d.releaseStart + d.rampEnd) : history d w.coefficients eta y = momentCandidate d (fun (t : ℝ) => OutgoingTail.releaseLag d (t - d.releaseStart)) y

theorem NavierStokes.ReleaseMoments.ResetWitness.history_hold {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {y : ℝ} (hy : d.releaseStart + d.rampEnd ≤ y) (hy' : y ≤ OutgoingTail.tailStart d) : history d w.coefficients eta y = momentCandidate d (fun (t : ℝ) => OutgoingTail.holdLag d (t - (d.releaseStart + d.rampEnd))) y

theorem NavierStokes.ReleaseMoments.ResetWitness.history_tail {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {y : ℝ} (hy : OutgoingTail.tailStart d ≤ y) : history d w.coefficients eta y = momentCandidate d (fun (t : ℝ) => OutgoingTail.tailLag d (t - OutgoingTail.tailStart d)) y

theorem NavierStokes.ReleaseMoments.tailLag_zero_late (d : OutgoingTail.TailData) {t : ℝ} (ht : 3 ≤ t) : OutgoingTail.tailLag d t = 0

theorem NavierStokes.ReleaseMoments.ResetWitness.history_eventual_power {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {y : ℝ} (hy : OutgoingTail.tailEnd d ≤ y) : history d w.coefficients eta y = releaseWeight d y / (1 - d.h)

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

Normalized lag, given by (1 - d.h) * history d c eta y / releaseWeight d y - 1.

Equations

• NavierStokes.ReleaseMoments.normalizedLag d c eta y = (1 - d.h) * NavierStokes.ReleaseMoments.history d c eta y / NavierStokes.ReleaseMoments.releaseWeight d y - 1

theorem NavierStokes.ReleaseMoments.ResetWitness.normalizedLag_hasDerivAt {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {y : ℝ} (hy : d.releaseStart ≤ y) : HasDerivAt (normalizedLag d w.coefficients eta) (-OutgoingTail.profileSlope d y - d.h - (1 + OutgoingTail.profileSlope d y) * normalizedLag d w.coefficients eta y) y

theorem NavierStokes.ReleaseMoments.ResetWitness.normalizedLag_eq_of_history {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) (q : ℝ → ℝ) (y : ℝ) (heq : history d w.coefficients eta y = momentCandidate d q y) : normalizedLag d w.coefficients eta y = q y

theorem NavierStokes.ReleaseMoments.ResetWitness.normalizedLag_release {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {y : ℝ} (hy : d.releaseStart ≤ y) (hy' : y ≤ d.releaseStart + d.rampEnd) : normalizedLag d w.coefficients eta y = OutgoingTail.releaseLag d (y - d.releaseStart)

theorem NavierStokes.ReleaseMoments.ResetWitness.normalizedLag_hold {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {y : ℝ} (hy : d.releaseStart + d.rampEnd ≤ y) (hy' : y ≤ OutgoingTail.tailStart d) : normalizedLag d w.coefficients eta y = OutgoingTail.holdLag d (y - (d.releaseStart + d.rampEnd))

theorem NavierStokes.ReleaseMoments.ResetWitness.normalizedLag_tail {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {y : ℝ} (hy : OutgoingTail.tailStart d ≤ y) : normalizedLag d w.coefficients eta y = OutgoingTail.tailLag d (y - OutgoingTail.tailStart d)

theorem NavierStokes.ReleaseMoments.ResetWitness.normalizedLag_initial {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) : normalizedLag d w.coefficients eta d.releaseStart = OutgoingTail.initialLag d

theorem NavierStokes.ReleaseMoments.ResetWitness.normalizedLag_eventual_zero {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {y : ℝ} (hy : OutgoingTail.tailEnd d ≤ y) : normalizedLag d w.coefficients eta y = 0

noncomputable def NavierStokes.ReleaseMoments.powerWeight (d : OutgoingTail.TailData) (y : ℝ) : ℝ

Power weight, given by powerConstant d * Real.exp ((1 - d.h) * y).

Equations

• NavierStokes.ReleaseMoments.powerWeight d y = NavierStokes.OutgoingTail.powerConstant d * Real.exp ((1 - d.h) * y)

theorem NavierStokes.ReleaseMoments.weighted_power (d : OutgoingTail.TailData) (y : ℝ) : Real.exp (3 * y / 2) * (OutgoingTail.powerConstant d * Real.exp (-(1 / 2 + d.h) * y)) = powerWeight d y

theorem NavierStokes.ReleaseMoments.correctedWeight_eq_power (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (eta : ℝ) {y : ℝ} (hy : OutgoingTail.tailEnd d ≤ y) : correctedWeight d c eta y = powerWeight d y

theorem NavierStokes.ReleaseMoments.releaseWeight_eq_power (d : OutgoingTail.TailData) {y : ℝ} (hy : OutgoingTail.tailEnd d ≤ y) : releaseWeight d y = powerWeight d y

theorem NavierStokes.ReleaseMoments.tailEnd_pos (d : OutgoingTail.TailData) : 0 < OutgoingTail.tailEnd d

theorem NavierStokes.ReleaseMoments.powerWeight_integrable (d : OutgoingTail.TailData) (y : ℝ) : MeasureTheory.IntegrableOn (powerWeight d) (Set.Iic y) MeasureTheory.volume

theorem NavierStokes.ReleaseMoments.powerWeight_integral (d : OutgoingTail.TailData) (y : ℝ) : ∫ (t : ℝ) in Set.Iic y, powerWeight d t = powerWeight d y / (1 - d.h)

theorem NavierStokes.ReleaseMoments.ResetWitness.renormalized_log_integrable {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) : MeasureTheory.Integrable (fun (y : ℝ) => correctedWeight d w.coefficients eta y - powerWeight d y) MeasureTheory.volume

theorem NavierStokes.ReleaseMoments.ResetWitness.renormalized_log_integral {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) : ∫ (y : ℝ), correctedWeight d w.coefficients eta y - powerWeight d y = 0

noncomputable def NavierStokes.ReleaseMoments.radialH (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (eta X : ℝ) : ℝ

Radial H, given by Real.sqrt (2 * X) * correctedAngular d c (Real.log X, eta).

Equations

• NavierStokes.ReleaseMoments.radialH d c eta X = √(2 * X) * NavierStokes.UniformAngularReset.correctedAngular d c (Real.log X, eta)

noncomputable def NavierStokes.ReleaseMoments.radialPowerH (d : OutgoingTail.TailData) (X : ℝ) : ℝ

Radial power H, given by Real.sqrt (2 * X) * (powerConstant d * X ^ (-(1 / 2 + d.h))).

Equations

• NavierStokes.ReleaseMoments.radialPowerH d X = √(2 * X) * (NavierStokes.OutgoingTail.powerConstant d * X ^ (-(1 / 2 + d.h)))

theorem NavierStokes.ReleaseMoments.exponential_radial_weight (y : ℝ) : Real.exp y * √(2 * Real.exp y) = √2 * Real.exp (3 * y / 2)

theorem NavierStokes.ReleaseMoments.radialH_comp_exp (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (eta y : ℝ) : |Real.exp y| • radialH d c eta (Real.exp y) = √2 * correctedWeight d c eta y

theorem NavierStokes.ReleaseMoments.radialPowerH_comp_exp (d : OutgoingTail.TailData) (y : ℝ) : |Real.exp y| • radialPowerH d (Real.exp y) = √2 * powerWeight d y

theorem NavierStokes.ReleaseMoments.radial_difference_comp_exp (d : OutgoingTail.TailData) (c : ℝ → AngularMomentReset.Coeff) (eta y : ℝ) : |Real.exp y| • (radialH d c eta (Real.exp y) - radialPowerH d (Real.exp y)) = √2 * (correctedWeight d c eta y - powerWeight d y)

theorem NavierStokes.ReleaseMoments.image_exp_Iic (y : ℝ) : Real.exp '' Set.Iic y = Set.Ioc 0 (Real.exp y)

theorem NavierStokes.ReleaseMoments.ResetWitness.radial_history_integrable {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {y : ℝ} (hy : 0 ≤ y) : MeasureTheory.IntegrableOn (radialH d w.coefficients eta) (Set.Ioc 0 (Real.exp y)) MeasureTheory.volume

theorem NavierStokes.ReleaseMoments.ResetWitness.radial_history_eq {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {y : ℝ} (hy : 0 ≤ y) : ∫ (X : ℝ) in Set.Ioc 0 (Real.exp y), radialH d w.coefficients eta X = √2 * history d w.coefficients eta y

theorem NavierStokes.ReleaseMoments.ResetWitness.radial_history_eta_independent {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta eta' : ℝ) {X : ℝ} (hX : 0 < X) (hrel : d.releaseStart ≤ Real.log X) : ∫ (u : ℝ) in Set.Ioc 0 X, radialH d w.coefficients eta u = ∫ (u : ℝ) in Set.Ioc 0 X, radialH d w.coefficients eta' u

theorem NavierStokes.ReleaseMoments.ResetWitness.radial_history_contDiff_eta {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {X : ℝ} (hX : 0 < X) (hrel : d.releaseStart ≤ Real.log X) : ContDiff ℝ ↑⊤ fun (eta : ℝ) => ∫ (u : ℝ) in Set.Ioc 0 X, radialH d w.coefficients eta u

theorem NavierStokes.ReleaseMoments.ResetWitness.radial_history_eventual {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {X : ℝ} (hX : 0 < X) (hfar : OutgoingTail.tailEnd d ≤ Real.log X) : ∫ (u : ℝ) in Set.Ioc 0 X, radialH d w.coefficients eta u = X * radialH d w.coefficients eta X / (1 - d.h)

The eventual physical history, in the manuscript's X coordinate.

theorem NavierStokes.ReleaseMoments.ResetWitness.renormalized_radial_integrable {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) : MeasureTheory.IntegrableOn (fun (X : ℝ) => radialH d w.coefficients eta X - radialPowerH d X) (Set.Ioi 0) MeasureTheory.volume

theorem NavierStokes.ReleaseMoments.ResetWitness.renormalized_angular_moment {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) : ∫ (X : ℝ) in Set.Ioi 0, radialH d w.coefficients eta X - radialPowerH d X = 0

The exact renormalized angular moment (12), for the actual corrected field and the actual eventual power coefficient.

theorem NavierStokes.ReleaseMoments.complete_release_moments : ∃ (lam0 : ℝ), 0 < lam0 ∧ ∀ (d : OutgoingTail.TailData), d.core.lam < lam0 → ∃ (c : ℝ → AngularMomentReset.Coeff), ContDiff ℝ (↑⊤) (UniformAngularReset.correctedAngular d c) ∧ ∀ (eta : ℝ), MeasureTheory.IntegrableOn (fun (X : ℝ) => radialH d c eta X - radialPowerH d X) (Set.Ioi 0) MeasureTheory.volume ∧ ∫ (X : ℝ) in Set.Ioi 0, radialH d c eta X - radialPowerH d X = 0 ∧ ∀ (X : ℝ), 0 < X → OutgoingTail.tailEnd d ≤ Real.log X → ∫ (u : ℝ) in Set.Ioc 0 X, radialH d c eta u = X * radialH d c eta X / (1 - d.h)

The actual scheduled correction has the exact renormalized angular moment and eventual physical history for a common small-lam threshold.