The actual terminal heat edit and its integral debts

The switch uses logarithmic time: it starts at tail time 1/5 and is complete at tail time 1/2. Quantitative estimates below are proved for the actual improper integrals, then applied to the constructed outgoing tail. No debt bound is an input to the final outgoing-tail theorems.

noncomputable def NavierStokes.HeatTailEdit.exponent (h : ℝ) : ℝ

Exponent, given by 1 / 2 + h.

Equations

• NavierStokes.HeatTailEdit.exponent h = 1 / 2 + h

noncomputable def NavierStokes.HeatTailEdit.heatConstant (h ν : ℝ) : ℝ

Heat constant, given by 2 * ν * h * (1 + h).

Equations

• NavierStokes.HeatTailEdit.heatConstant h ν = 2 * ν * h * (1 + h)

noncomputable def NavierStokes.HeatTailEdit.switch (K X : ℝ) : ℝ

Switch, given by OutgoingSchedule.sigma (Real.log (X / K) / (3 / 10)).

Equations

• NavierStokes.HeatTailEdit.switch K X = NavierStokes.OutgoingSchedule.sigma (Real.log (X / K) / (3 / 10))

noncomputable def NavierStokes.HeatTailEdit.multiplier (h ν K X : ℝ) : ℝ

Multiplier, given by 1 + switch K X * (RadialHeatProfile.profile (1 + h) (2 * ν / X) - 1).

Equations

• NavierStokes.HeatTailEdit.multiplier h ν K X = 1 + NavierStokes.HeatTailEdit.switch K X * (NavierStokes.RadialHeatProfile.profile (1 + h) (2 * ν / X) - 1)

noncomputable def NavierStokes.HeatTailEdit.edit (E : ℝ → ℝ) (h ν K X : ℝ) : ℝ

Edit, given by E X * multiplier h ν K X.

Equations

• NavierStokes.HeatTailEdit.edit E h ν K X = E X * NavierStokes.HeatTailEdit.multiplier h ν K X

noncomputable def NavierStokes.HeatTailEdit.change (E : ℝ → ℝ) (h ν K X : ℝ) : ℝ

Change, given by edit E h ν K X - E X.

Equations

• NavierStokes.HeatTailEdit.change E h ν K X = NavierStokes.HeatTailEdit.edit E h ν K X - E X

noncomputable def NavierStokes.HeatTailEdit.squareChange (E : ℝ → ℝ) (h ν K X : ℝ) : ℝ

Square change, given by edit E h ν K X ^ 2 - E X ^ 2.

Equations

• NavierStokes.HeatTailEdit.squareChange E h ν K X = NavierStokes.HeatTailEdit.edit E h ν K X ^ 2 - E X ^ 2

theorem NavierStokes.HeatTailEdit.switch_bounds (K X : ℝ) : 0 ≤ switch K X ∧ switch K X ≤ 1

theorem NavierStokes.HeatTailEdit.switch_zero {K X : ℝ} (hK : 0 < K) (hX : 0 < X) (hXK : X ≤ K) : switch K X = 0

theorem NavierStokes.HeatTailEdit.switch_one {K X : ℝ} (h : 3 / 10 ≤ Real.log (X / K)) : switch K X = 1

theorem NavierStokes.HeatTailEdit.edit_before (E : ℝ → ℝ) (h ν : ℝ) {K X : ℝ} (hK : 0 < K) (hX : 0 < X) (hXK : X ≤ K) : edit E h ν K X = E X

theorem NavierStokes.HeatTailEdit.edit_after (E : ℝ → ℝ) (h ν : ℝ) {K X : ℝ} (hfull : 3 / 10 ≤ Real.log (X / K)) : edit E h ν K X = E X * RadialHeatProfile.profile (1 + h) (2 * ν / X)

theorem NavierStokes.HeatTailEdit.multiplier_bounds {h ν K X : ℝ} (hh : 0 < h) (hν : 0 ≤ ν) (hX : 0 < X) : 0 < multiplier h ν K X ∧ multiplier h ν K X ≤ 1

theorem NavierStokes.HeatTailEdit.edit_pos {E : ℝ → ℝ} {h ν K X : ℝ} (hh : 0 < h) (hν : 0 ≤ ν) (hX : 0 < X) (hE : 0 < E X) : 0 < edit E h ν K X

theorem NavierStokes.HeatTailEdit.switch_contDiffOn {K : ℝ} (hK : 0 < K) : ContDiffOn ℝ (↑⊤) (switch K) (Set.Ioi 0)

theorem NavierStokes.HeatTailEdit.multiplier_contDiffOn {h ν K : ℝ} (hh : 0 < h) (hν : 0 < ν) (hK : 0 < K) : ContDiffOn ℝ (↑⊤) (multiplier h ν K) (Set.Ioi 0)

theorem NavierStokes.HeatTailEdit.edit_contDiffOn {E : ℝ → ℝ} {h ν K : ℝ} (hh : 0 < h) (hν : 0 < ν) (hK : 0 < K) (hE : ContDiffOn ℝ (↑⊤) E (Set.Ioi 0)) : ContDiffOn ℝ (↑⊤) (edit E h ν K) (Set.Ioi 0)

theorem NavierStokes.HeatTailEdit.heatConstant_pos {h ν : ℝ} (hh : 0 < h) (hν : 0 < ν) : 0 < heatConstant h ν

theorem NavierStokes.HeatTailEdit.multiplier_sub_one_bound {h ν K X : ℝ} (hh : 0 < h) (hν : 0 ≤ ν) (hX : 0 < X) : |multiplier h ν K X - 1| ≤ heatConstant h ν / X

theorem NavierStokes.HeatTailEdit.change_bound {E : ℝ → ℝ} {h ν K X : ℝ} (hh : 0 < h) (hν : 0 ≤ ν) (hX : 0 < X) : |change E h ν K X| ≤ heatConstant h ν * |E X| / X

theorem NavierStokes.HeatTailEdit.squareChange_bound {E : ℝ → ℝ} {h ν K X : ℝ} (hh : 0 < h) (hν : 0 ≤ ν) (hX : 0 < X) : |squareChange E h ν K X| ≤ 2 * heatConstant h ν * E X ^ 2 / X

One exact weighted power integral

noncomputable def NavierStokes.HeatTailEdit.weightedKernel (K p q X : ℝ) : ℝ

Weighted kernel, given by X ^ q * (X / K) ^ p / X.

Equations

• NavierStokes.HeatTailEdit.weightedKernel K p q X = X ^ q * (X / K) ^ p / X

theorem NavierStokes.HeatTailEdit.weightedKernel_eq {K X : ℝ} (hK : 0 < K) (hX : 0 < X) (p q : ℝ) : weightedKernel K p q X = X ^ (p + q - 1) / K ^ p

theorem NavierStokes.HeatTailEdit.weightedKernel_integrable {K p q : ℝ} (hK : 0 < K) (hpq : p + q < 0) : MeasureTheory.IntegrableOn (weightedKernel K p q) (Set.Ioi K) MeasureTheory.volume

theorem NavierStokes.HeatTailEdit.integral_weightedKernel {K p q : ℝ} (hK : 0 < K) (hpq : p + q < 0) : ∫ (X : ℝ) in Set.Ioi K, weightedKernel K p q X = K ^ q / (-p - q)

theorem NavierStokes.HeatTailEdit.weighted_integral_bound {K p q B : ℝ} {g : ℝ → ℝ} (hK : 0 < K) (hpq : p + q < 0) (hg : ContinuousOn g (Set.Ioi K)) (hb : ∀ X ∈ Set.Ioi K, |g X| ≤ B * (X / K) ^ p / X) : MeasureTheory.IntegrableOn (fun (X : ℝ) => X ^ q * g X) (Set.Ioi K) MeasureTheory.volume ∧ |∫ (X : ℝ) in Set.Ioi K, X ^ q * g X| ≤ B * K ^ q / (-p - q)

Quantitative debts for a prescribed bounded terminal shape

noncomputable def NavierStokes.HeatTailEdit.powerTail (h e K : ℝ) (f : ℝ → ℝ) (X : ℝ) : ℝ

Power tail, given by e * (X / K) ^ (-exponent h) * f (Real.log (X / K)).

Equations

• NavierStokes.HeatTailEdit.powerTail h e K f X = e * (X / K) ^ (-NavierStokes.HeatTailEdit.exponent h) * f (Real.log (X / K))

theorem NavierStokes.HeatTailEdit.powerTail_contDiffOn {K : ℝ} (hK : 0 < K) (h e : ℝ) {f : ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) : ContDiffOn ℝ (↑⊤) (powerTail h e K f) (Set.Ioi 0)

theorem NavierStokes.HeatTailEdit.powerTail_bound {K e M X : ℝ} (hK : 0 < K) (he : 0 ≤ e) (hX : K ≤ X) (h : ℝ) {f : ℝ → ℝ} (hf : ∀ (t : ℝ), 0 ≤ t → |f t| ≤ M) : |powerTail h e K f X| ≤ e * M * (X / K) ^ (-exponent h)

theorem NavierStokes.HeatTailEdit.powerTail_square_bound {K e M X : ℝ} (hK : 0 < K) (he : 0 ≤ e) (hM : 0 ≤ M) (hX : K ≤ X) (h : ℝ) {f : ℝ → ℝ} (hf : ∀ (t : ℝ), 0 ≤ t → |f t| ≤ M) : powerTail h e K f X ^ 2 ≤ e ^ 2 * M ^ 2 * (X / K) ^ (-2 * exponent h)

theorem NavierStokes.HeatTailEdit.powerTail_weighted_change {h ν K e M q : ℝ} (hh : 0 < h) (hν : 0 < ν) (hK : 0 < K) (he : 0 ≤ e) {f : ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hbound : ∀ (t : ℝ), 0 ≤ t → |f t| ≤ M) (hq : q < exponent h) : MeasureTheory.IntegrableOn (fun (X : ℝ) => X ^ q * change (powerTail h e K f) h ν K X) (Set.Ioi K) MeasureTheory.volume ∧ |∫ (X : ℝ) in Set.Ioi K, X ^ q * change (powerTail h e K f) h ν K X| ≤ heatConstant h ν * e * M * K ^ q / (exponent h - q)

theorem NavierStokes.HeatTailEdit.powerTail_weighted_squareChange {h ν K e M q : ℝ} (hh : 0 < h) (hν : 0 < ν) (hK : 0 < K) (he : 0 ≤ e) (hM : 0 ≤ M) {f : ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hbound : ∀ (t : ℝ), 0 ≤ t → |f t| ≤ M) (hq : q < 2 * exponent h) : MeasureTheory.IntegrableOn (fun (X : ℝ) => X ^ q * squareChange (powerTail h e K f) h ν K X) (Set.Ioi K) MeasureTheory.volume ∧ |∫ (X : ℝ) in Set.Ioi K, X ^ q * squareChange (powerTail h e K f) h ν K X| ≤ 2 * heatConstant h ν * e ^ 2 * M ^ 2 * K ^ q / (2 * exponent h - q)

noncomputable def NavierStokes.HeatTailEdit.pressureDebt (E : ℝ → ℝ) (h ν K : ℝ) : ℝ

Pressure debt, given by ∫ X in Ioi K, squareChange E h ν K X / X.

Equations

• NavierStokes.HeatTailEdit.pressureDebt E h ν K = ∫ (X : ℝ) in Set.Ioi K, NavierStokes.HeatTailEdit.squareChange E h ν K X / X

noncomputable def NavierStokes.HeatTailEdit.energyDebt (E : ℝ → ℝ) (h ν K : ℝ) : ℝ

Energy debt, given by ∫ X in Ioi K, squareChange E h ν K X.

Equations

• NavierStokes.HeatTailEdit.energyDebt E h ν K = ∫ (X : ℝ) in Set.Ioi K, NavierStokes.HeatTailEdit.squareChange E h ν K X

noncomputable def NavierStokes.HeatTailEdit.angularDebt (E : ℝ → ℝ) (h ν K : ℝ) : ℝ

Angular debt, given by ∫ X in Ioi K, Real.sqrt (2 * X) * change E h ν K X.

Equations

• NavierStokes.HeatTailEdit.angularDebt E h ν K = ∫ (X : ℝ) in Set.Ioi K, √(2 * X) * NavierStokes.HeatTailEdit.change E h ν K X

theorem NavierStokes.HeatTailEdit.pressureDebt_eq (E : ℝ → ℝ) (h ν K : ℝ) : pressureDebt E h ν K = ∫ (X : ℝ) in Set.Ioi K, X ^ (-1) * squareChange E h ν K X

theorem NavierStokes.HeatTailEdit.angularDebt_eq (E : ℝ → ℝ) (h ν K : ℝ) : angularDebt E h ν K = √2 * ∫ (X : ℝ) in Set.Ioi K, X ^ (1 / 2) * change E h ν K X

theorem NavierStokes.HeatTailEdit.powerTail_pressure {h ν K e M : ℝ} (hh : 0 < h) (hν : 0 < ν) (hK : 0 < K) (he : 0 ≤ e) (hM : 0 ≤ M) {f : ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hbound : ∀ (t : ℝ), 0 ≤ t → |f t| ≤ M) : MeasureTheory.IntegrableOn (fun (X : ℝ) => squareChange (powerTail h e K f) h ν K X / X) (Set.Ioi K) MeasureTheory.volume ∧ |pressureDebt (powerTail h e K f) h ν K| ≤ 2 * heatConstant h ν * e ^ 2 * M ^ 2 / (K * (2 * exponent h + 1))

theorem NavierStokes.HeatTailEdit.powerTail_energy {h ν K e M : ℝ} (hh : 0 < h) (hν : 0 < ν) (hK : 0 < K) (he : 0 ≤ e) (hM : 0 ≤ M) {f : ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hbound : ∀ (t : ℝ), 0 ≤ t → |f t| ≤ M) : MeasureTheory.IntegrableOn (squareChange (powerTail h e K f) h ν K) (Set.Ioi K) MeasureTheory.volume ∧ |energyDebt (powerTail h e K f) h ν K| ≤ 2 * heatConstant h ν * e ^ 2 * M ^ 2 / (2 * exponent h)

theorem NavierStokes.HeatTailEdit.powerTail_angular {h ν K e M : ℝ} (hh : 0 < h) (hν : 0 < ν) (hK : 0 < K) (he : 0 ≤ e) {f : ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hbound : ∀ (t : ℝ), 0 ≤ t → |f t| ≤ M) : MeasureTheory.IntegrableOn (fun (X : ℝ) => √(2 * X) * change (powerTail h e K f) h ν K X) (Set.Ioi K) MeasureTheory.volume ∧ |angularDebt (powerTail h e K f) h ν K| ≤ √2 * heatConstant h ν * e * M * √K / h

The actual outgoing schedule

noncomputable def NavierStokes.HeatTailEdit.switchStart (d : OutgoingTail.TailData) : ℝ

Switch start, given by tailStart d + 1 / 5.

Equations

• NavierStokes.HeatTailEdit.switchStart d = NavierStokes.OutgoingTail.tailStart d + 1 / 5

noncomputable def NavierStokes.HeatTailEdit.outgoingAmplitude (d : OutgoingTail.TailData) : ℝ

This carrier amplitude is fixed by the schedule, independently of K.

Equations

• NavierStokes.HeatTailEdit.outgoingAmplitude d = NavierStokes.OutgoingTail.powerConstant d * Real.exp (-NavierStokes.HeatTailEdit.exponent d.h * NavierStokes.HeatTailEdit.switchStart d)

noncomputable def NavierStokes.HeatTailEdit.outgoingShape (d : OutgoingTail.TailData) (t : ℝ) : ℝ

Outgoing shape, given by tailShape d (t + 1 / 5).

Equations

• NavierStokes.HeatTailEdit.outgoingShape d t = NavierStokes.OutgoingTail.tailShape d (t + 1 / 5)

noncomputable def NavierStokes.HeatTailEdit.outgoingProfile (d : OutgoingTail.TailData) (K eta X : ℝ) : ℝ

Outgoing profile, given by finalAngular d (switchStart d + Real.log (X / K), eta).

Equations

• NavierStokes.HeatTailEdit.outgoingProfile d K eta X = NavierStokes.OutgoingTail.finalAngular d (NavierStokes.HeatTailEdit.switchStart d + Real.log (X / K), eta)

noncomputable def NavierStokes.HeatTailEdit.outgoingEdit (d : OutgoingTail.TailData) (ν K eta X : ℝ) : ℝ

Outgoing edit, given by edit (outgoingProfile d K eta) d.h ν K X.

Equations

• NavierStokes.HeatTailEdit.outgoingEdit d ν K eta X = NavierStokes.HeatTailEdit.edit (NavierStokes.HeatTailEdit.outgoingProfile d K eta) d.h ν K X

theorem NavierStokes.HeatTailEdit.outgoingAmplitude_pos (d : OutgoingTail.TailData) : 0 < outgoingAmplitude d

theorem NavierStokes.HeatTailEdit.outgoingShape_contDiff (d : OutgoingTail.TailData) : ContDiff ℝ (↑⊤) (outgoingShape d)

theorem NavierStokes.HeatTailEdit.outgoingShape_bound (d : OutgoingTail.TailData) (t : ℝ) : |outgoingShape d t| ≤ 1

theorem NavierStokes.HeatTailEdit.outgoingProfile_pos (d : OutgoingTail.TailData) (K eta X : ℝ) : 0 < outgoingProfile d K eta X

theorem NavierStokes.HeatTailEdit.outgoingProfile_eq_powerTail_of_log (d : OutgoingTail.TailData) {K X : ℝ} (hK : 0 < K) (hX : 0 < X) (hlog : 0 ≤ Real.log (X / K)) (eta : ℝ) : outgoingProfile d K eta X = powerTail d.h (outgoingAmplitude d) K (outgoingShape d) X

theorem NavierStokes.HeatTailEdit.outgoingProfile_eq_powerTail (d : OutgoingTail.TailData) {K X : ℝ} (hK : 0 < K) (hX : K ≤ X) (eta : ℝ) : outgoingProfile d K eta X = powerTail d.h (outgoingAmplitude d) K (outgoingShape d) X

theorem NavierStokes.HeatTailEdit.outgoingProfile_joint_contDiffOn (d : OutgoingTail.TailData) {K : ℝ} (hK : 0 < K) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × ℝ) => outgoingProfile d K p.2 p.1) (Set.Ioi 0 ×ˢ Set.univ)

theorem NavierStokes.HeatTailEdit.outgoingEdit_joint_contDiffOn (d : OutgoingTail.TailData) {ν K : ℝ} (hν : 0 < ν) (hK : 0 < K) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × ℝ) => outgoingEdit d ν K p.2 p.1) (Set.Ioi 0 ×ˢ Set.univ)

theorem NavierStokes.HeatTailEdit.outgoingEdit_pos (d : OutgoingTail.TailData) {ν K X : ℝ} (hν : 0 ≤ ν) (hX : 0 < X) (eta : ℝ) : 0 < outgoingEdit d ν K eta X

theorem NavierStokes.HeatTailEdit.outgoingEdit_before (d : OutgoingTail.TailData) (ν eta : ℝ) {K X : ℝ} (hK : 0 < K) (hX : 0 < X) (hXK : X ≤ K) : outgoingEdit d ν K eta X = outgoingProfile d K eta X

Exact matching before tail logarithmic time 0.2.

theorem NavierStokes.HeatTailEdit.outgoingEdit_full (d : OutgoingTail.TailData) (ν eta : ℝ) {K X : ℝ} (hK : 0 < K) (hX : 0 < X) (hfull : 1 / 2 ≤ Real.log (X / K) + 1 / 5) : outgoingEdit d ν K eta X = outgoingAmplitude d * (X / K) ^ (-exponent d.h) * OutgoingTail.tailShape d (Real.log (X / K) + 1 / 5) * RadialHeatProfile.profile (1 + d.h) (2 * ν / X)

At tail logarithmic time 0.5, the full heat factor is present.

theorem NavierStokes.HeatTailEdit.outgoing_change_eq (d : OutgoingTail.TailData) (ν eta : ℝ) {K X : ℝ} (hK : 0 < K) (hX : K ≤ X) : change (outgoingProfile d K eta) d.h ν K X = change (powerTail d.h (outgoingAmplitude d) K (outgoingShape d)) d.h ν K X

theorem NavierStokes.HeatTailEdit.outgoing_squareChange_eq (d : OutgoingTail.TailData) (ν eta : ℝ) {K X : ℝ} (hK : 0 < K) (hX : K ≤ X) : squareChange (outgoingProfile d K eta) d.h ν K X = squareChange (powerTail d.h (outgoingAmplitude d) K (outgoingShape d)) d.h ν K X

theorem NavierStokes.HeatTailEdit.outgoing_pressureDebt_eq (d : OutgoingTail.TailData) (ν eta : ℝ) {K : ℝ} (hK : 0 < K) : pressureDebt (outgoingProfile d K eta) d.h ν K = pressureDebt (powerTail d.h (outgoingAmplitude d) K (outgoingShape d)) d.h ν K

theorem NavierStokes.HeatTailEdit.outgoing_energyDebt_eq (d : OutgoingTail.TailData) (ν eta : ℝ) {K : ℝ} (hK : 0 < K) : energyDebt (outgoingProfile d K eta) d.h ν K = energyDebt (powerTail d.h (outgoingAmplitude d) K (outgoingShape d)) d.h ν K

theorem NavierStokes.HeatTailEdit.outgoing_angularDebt_eq (d : OutgoingTail.TailData) (ν eta : ℝ) {K : ℝ} (hK : 0 < K) : angularDebt (outgoingProfile d K eta) d.h ν K = angularDebt (powerTail d.h (outgoingAmplitude d) K (outgoingShape d)) d.h ν K

theorem NavierStokes.HeatTailEdit.outgoing_pressure (d : OutgoingTail.TailData) {ν K : ℝ} (hν : 0 < ν) (hK : 0 < K) (eta : ℝ) : MeasureTheory.IntegrableOn (fun (X : ℝ) => squareChange (outgoingProfile d K eta) d.h ν K X / X) (Set.Ioi K) MeasureTheory.volume ∧ |pressureDebt (outgoingProfile d K eta) d.h ν K| ≤ 2 * heatConstant d.h ν * outgoingAmplitude d ^ 2 / (K * (2 * exponent d.h + 1))

theorem NavierStokes.HeatTailEdit.outgoing_energy (d : OutgoingTail.TailData) {ν K : ℝ} (hν : 0 < ν) (hK : 0 < K) (eta : ℝ) : MeasureTheory.IntegrableOn (squareChange (outgoingProfile d K eta) d.h ν K) (Set.Ioi K) MeasureTheory.volume ∧ |energyDebt (outgoingProfile d K eta) d.h ν K| ≤ 2 * heatConstant d.h ν * outgoingAmplitude d ^ 2 / (2 * exponent d.h)

theorem NavierStokes.HeatTailEdit.outgoing_angular (d : OutgoingTail.TailData) {ν K : ℝ} (hν : 0 < ν) (hK : 0 < K) (eta : ℝ) : MeasureTheory.IntegrableOn (fun (X : ℝ) => √(2 * X) * change (outgoingProfile d K eta) d.h ν K X) (Set.Ioi K) MeasureTheory.volume ∧ |angularDebt (outgoingProfile d K eta) d.h ν K| ≤ √2 * heatConstant d.h ν * outgoingAmplitude d * √K / d.h

theorem NavierStokes.HeatTailEdit.outgoingEdit_heat_factorization (d : OutgoingTail.TailData) (ν eta : ℝ) {K X : ℝ} (hK : 0 < K) (hX : 0 < X) (hfull : 1 / 2 ≤ Real.log (X / K) + 1 / 5) : outgoingEdit d ν K eta X = outgoingAmplitude d * K ^ exponent d.h * RadialHeatProfile.spatialProfile (1 + d.h) ν X * OutgoingTail.tailShape d (Real.log (X / K) + 1 / 5)

The fully switched profile is exactly the radial heat profile times the prescribed flat terminal shape, with its normalization made explicit.

theorem NavierStokes.HeatTailEdit.outgoingEdit_eventual_heat (d : OutgoingTail.TailData) (ν eta : ℝ) {K X : ℝ} (hK : 0 < K) (hX : 0 < X) (htail : 3 ≤ Real.log (X / K) + 1 / 5) : outgoingEdit d ν K eta X = outgoingAmplitude d * K ^ exponent d.h * RadialHeatProfile.spatialProfile (1 + d.h) ν X

Beyond the terminal taper, the profile is the unmodified exact radial heat solution with a positive constant normalization.

theorem NavierStokes.HeatTailEdit.outgoingProfile_at_switch (d : OutgoingTail.TailData) {K : ℝ} (hK : 0 < K) (eta : ℝ) : outgoingProfile d K eta K = outgoingAmplitude d * (1 - d.rho)

The actual switch amplitude is fixed by the schedule and comparable to the carrier amplitude used in the estimates.

theorem NavierStokes.HeatTailEdit.outgoing_pressure_eta_contDiff (d : OutgoingTail.TailData) (ν : ℝ) {K : ℝ} (hK : 0 < K) : ContDiff ℝ ↑⊤ fun (eta : ℝ) => pressureDebt (outgoingProfile d K eta) d.h ν K

theorem NavierStokes.HeatTailEdit.outgoing_energy_eta_contDiff (d : OutgoingTail.TailData) (ν : ℝ) {K : ℝ} (hK : 0 < K) : ContDiff ℝ ↑⊤ fun (eta : ℝ) => energyDebt (outgoingProfile d K eta) d.h ν K

theorem NavierStokes.HeatTailEdit.outgoing_angular_eta_contDiff (d : OutgoingTail.TailData) (ν : ℝ) {K : ℝ} (hK : 0 < K) : ContDiff ℝ ↑⊤ fun (eta : ℝ) => angularDebt (outgoingProfile d K eta) d.h ν K

theorem NavierStokes.HeatTailEdit.outgoing_pressure_eta_jet_zero (d : OutgoingTail.TailData) (ν : ℝ) {K : ℝ} (hK : 0 < K) (n : ℕ) (eta : ℝ) : iteratedDeriv (n + 1) (fun (eta : ℝ) => pressureDebt (outgoingProfile d K eta) d.h ν K) eta = 0

theorem NavierStokes.HeatTailEdit.outgoing_energy_eta_jet_zero (d : OutgoingTail.TailData) (ν : ℝ) {K : ℝ} (hK : 0 < K) (n : ℕ) (eta : ℝ) : iteratedDeriv (n + 1) (fun (eta : ℝ) => energyDebt (outgoingProfile d K eta) d.h ν K) eta = 0

theorem NavierStokes.HeatTailEdit.outgoing_angular_eta_jet_zero (d : OutgoingTail.TailData) (ν : ℝ) {K : ℝ} (hK : 0 < K) (n : ℕ) (eta : ℝ) : iteratedDeriv (n + 1) (fun (eta : ℝ) => angularDebt (outgoingProfile d K eta) d.h ν K) eta = 0

theorem NavierStokes.HeatTailEdit.outgoing_pressure_jet_bound (d : OutgoingTail.TailData) {ν K : ℝ} (hν : 0 < ν) (hK : 0 < K) (n : ℕ) (eta : ℝ) : |iteratedDeriv n (fun (eta : ℝ) => pressureDebt (outgoingProfile d K eta) d.h ν K) eta| ≤ 2 * heatConstant d.h ν * outgoingAmplitude d ^ 2 / (K * (2 * exponent d.h + 1))

The pressure estimate holds with every fixed slow-variable jet.

theorem NavierStokes.HeatTailEdit.outgoing_energy_jet_bound (d : OutgoingTail.TailData) {ν K : ℝ} (hν : 0 < ν) (hK : 0 < K) (n : ℕ) (eta : ℝ) : |iteratedDeriv n (fun (eta : ℝ) => energyDebt (outgoingProfile d K eta) d.h ν K) eta| ≤ 2 * heatConstant d.h ν * outgoingAmplitude d ^ 2 / (2 * exponent d.h)

The energy estimate holds with every fixed slow-variable jet.

theorem NavierStokes.HeatTailEdit.outgoing_angular_jet_bound (d : OutgoingTail.TailData) {ν K : ℝ} (hν : 0 < ν) (hK : 0 < K) (n : ℕ) (eta : ℝ) : |iteratedDeriv n (fun (eta : ℝ) => angularDebt (outgoingProfile d K eta) d.h ν K) eta| ≤ √2 * heatConstant d.h ν * outgoingAmplitude d * √K / d.h

The renormalized angular estimate holds with every fixed slow-variable jet.