The physical heat continuation with exact terminal compensation

One normalized outgoing profile supplies the angular reset and axial amplitude. Its radial dilation is heated with diffusion 1 - eta^2, and three additive bumps on its actual second reserved patch restore the three changed moments.

Actual radial dilation of the constructed outgoing profile

The entrance radius rescales the radial variable. All moment laws below are proved by change of variables in the actual integrals. The final section locates the clean terminal switch and the second reserved compensation patch. No heat edit is applied in this module.

theorem NavierStokes.OutgoingDilation.image_mul_Ioc (R X : ℝ) (hR : 0 < R) : (fun (x : ℝ) => R * x) '' Set.Ioc 0 (X / R) = Set.Ioc 0 X

theorem NavierStokes.OutgoingDilation.integral_dilate_Ioc (f : ℝ → ℝ) (R X : ℝ) (hR : 0 < R) : ∫ (x : ℝ) in Set.Ioc 0 X, f (x / R) = R * ∫ (x : ℝ) in Set.Ioc 0 (X / R), f x

theorem NavierStokes.OutgoingDilation.integrable_dilate_Ioc (f : ℝ → ℝ) (R X : ℝ) (hR : 0 < R) (hf : MeasureTheory.IntegrableOn f (Set.Ioc 0 (X / R)) MeasureTheory.volume) : MeasureTheory.IntegrableOn (fun (x : ℝ) => f (x / R)) (Set.Ioc 0 X) MeasureTheory.volume

theorem NavierStokes.OutgoingDilation.integral_dilate_Ioi (f : ℝ → ℝ) (R X : ℝ) (hR : 0 < R) : ∫ (x : ℝ) in Set.Ioi X, f (x / R) = R * ∫ (x : ℝ) in Set.Ioi (X / R), f x

theorem NavierStokes.OutgoingDilation.integrable_dilate_Ioi_iff (f : ℝ → ℝ) (R X : ℝ) (hR : 0 < R) : MeasureTheory.IntegrableOn (fun (x : ℝ) => f (x / R)) (Set.Ioi X) MeasureTheory.volume ↔ MeasureTheory.IntegrableOn f (Set.Ioi (X / R)) MeasureTheory.volume

noncomputable def NavierStokes.OutgoingDilation.E (F : OutgoingProfile.Profile) (XR : ℝ) (p : ℝ × ℝ) : ℝ

E, given by F.E (p.1 / XR, p.2).

Equations

• NavierStokes.OutgoingDilation.E F XR p = F.E (p.1 / XR, p.2)

noncomputable def NavierStokes.OutgoingDilation.U (F : OutgoingProfile.Profile) (XR : ℝ) (p : ℝ × ℝ) : ℝ

U, given by F.U (p.1 / XR, p.2).

Equations

• NavierStokes.OutgoingDilation.U F XR p = F.U (p.1 / XR, p.2)

noncomputable def NavierStokes.OutgoingDilation.H (F : OutgoingProfile.Profile) (XR : ℝ) (p : ℝ × ℝ) : ℝ

H, given by Real.sqrt (2 * p.1) * E F XR p.

Equations

• NavierStokes.OutgoingDilation.H F XR p = √(2 * p.1) * NavierStokes.OutgoingDilation.E F XR p

noncomputable def NavierStokes.OutgoingDilation.Pi (F : OutgoingProfile.Profile) (XR : ℝ) (p : ℝ × ℝ) : ℝ

Pi, given by F.Pi (p.1 / XR, p.2).

Equations

• NavierStokes.OutgoingDilation.Pi F XR p = F.Pi (p.1 / XR, p.2)

noncomputable def NavierStokes.OutgoingDilation.powerE (F : OutgoingProfile.Profile) (XR X : ℝ) : ℝ

Power E, given by F.powerE (X / XR).

Equations

• NavierStokes.OutgoingDilation.powerE F XR X = F.powerE (X / XR)

noncomputable def NavierStokes.OutgoingDilation.powerH (F : OutgoingProfile.Profile) (XR X : ℝ) : ℝ

Power H, given by Real.sqrt (2 * X) * powerE F XR X.

Equations

• NavierStokes.OutgoingDilation.powerH F XR X = √(2 * X) * NavierStokes.OutgoingDilation.powerE F XR X

noncomputable def NavierStokes.OutgoingDilation.energyDensity (F : OutgoingProfile.Profile) (XR eta X : ℝ) : ℝ

Energy density, given by U F XR (X, eta) ^ 2 - E F XR (X, eta) ^ 2 / 2.

Equations

• NavierStokes.OutgoingDilation.energyDensity F XR eta X = NavierStokes.OutgoingDilation.U F XR (X, eta) ^ 2 - NavierStokes.OutgoingDilation.E F XR (X, eta) ^ 2 / 2

noncomputable def NavierStokes.OutgoingDilation.canonicalKernel (F : OutgoingProfile.Profile) (XR eta X : ℝ) : ℝ

Canonical kernel, given by E F XR (X, eta) ^ 2 / X.

Equations

• NavierStokes.OutgoingDilation.canonicalKernel F XR eta X = NavierStokes.OutgoingDilation.E F XR (X, eta) ^ 2 / X

noncomputable def NavierStokes.OutgoingDilation.M (F : OutgoingProfile.Profile) (XR eta X : ℝ) : ℝ

M, given by ∫ u in Ioc 0 X, U F XR (u, eta).

Equations

• NavierStokes.OutgoingDilation.M F XR eta X = ∫ (u : ℝ) in Set.Ioc 0 X, NavierStokes.OutgoingDilation.U F XR (u, eta)

noncomputable def NavierStokes.OutgoingDilation.I (F : OutgoingProfile.Profile) (XR eta X : ℝ) : ℝ

I, given by ∫ u in Ioc 0 X, H F XR (u, eta).

Equations

• NavierStokes.OutgoingDilation.I F XR eta X = ∫ (u : ℝ) in Set.Ioc 0 X, NavierStokes.OutgoingDilation.H F XR (u, eta)

noncomputable def NavierStokes.OutgoingDilation.J (F : OutgoingProfile.Profile) (XR eta X : ℝ) : ℝ

J, given by ∫ u in Ioc 0 X, H F XR (u, eta) * U F XR (u, eta).

Equations

• NavierStokes.OutgoingDilation.J F XR eta X = ∫ (u : ℝ) in Set.Ioc 0 X, NavierStokes.OutgoingDilation.H F XR (u, eta) * NavierStokes.OutgoingDilation.U F XR (u, eta)

noncomputable def NavierStokes.OutgoingDilation.S (F : OutgoingProfile.Profile) (XR eta X : ℝ) : ℝ

S, given by ∫ u in Ioc 0 X, energyDensity F XR eta u.

Equations

• NavierStokes.OutgoingDilation.S F XR eta X = ∫ (u : ℝ) in Set.Ioc 0 X, NavierStokes.OutgoingDilation.energyDensity F XR eta u

noncomputable def NavierStokes.OutgoingDilation.totalS (F : OutgoingProfile.Profile) (XR eta : ℝ) : ℝ

Total S, given by ∫ u in Ioi 0, energyDensity F XR eta u.

Equations

• NavierStokes.OutgoingDilation.totalS F XR eta = ∫ (u : ℝ) in Set.Ioi 0, NavierStokes.OutgoingDilation.energyDensity F XR eta u

noncomputable def NavierStokes.OutgoingDilation.renormalizedI (F : OutgoingProfile.Profile) (XR eta : ℝ) : ℝ

Renormalized I, given by ∫ u in Ioi 0, H F XR (u, eta) - powerH F XR u.

Equations

• NavierStokes.OutgoingDilation.renormalizedI F XR eta = ∫ (u : ℝ) in Set.Ioi 0, NavierStokes.OutgoingDilation.H F XR (u, eta) - NavierStokes.OutgoingDilation.powerH F XR u

noncomputable def NavierStokes.OutgoingDilation.axisDatum (F : OutgoingProfile.Profile) (XR eta : ℝ) : ℝ

Axis datum, given by -(1 / 2 : ℝ) * ∫ u in Ioi 0, canonicalKernel F XR eta u.

Equations

• NavierStokes.OutgoingDilation.axisDatum F XR eta = -(1 / 2) * ∫ (u : ℝ) in Set.Ioi 0, NavierStokes.OutgoingDilation.canonicalKernel F XR eta u

theorem NavierStokes.OutgoingDilation.H_scaling (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) (p : ℝ × ℝ) : H F XR p = √XR * F.H (p.1 / XR, p.2)

theorem NavierStokes.OutgoingDilation.powerH_scaling (F : OutgoingProfile.Profile) (XR X : ℝ) (hXR : 0 < XR) : powerH F XR X = √XR * F.powerH (X / XR)

theorem NavierStokes.OutgoingDilation.energyDensity_scaling (F : OutgoingProfile.Profile) (XR eta X : ℝ) : energyDensity F XR eta X = F.energyDensity eta (X / XR)

theorem NavierStokes.OutgoingDilation.canonicalKernel_scaling (F : OutgoingProfile.Profile) (XR eta X : ℝ) (hXR : 0 < XR) : canonicalKernel F XR eta X = XR⁻¹ * F.canonicalKernel eta (X / XR)

theorem NavierStokes.OutgoingDilation.M_scaling (F : OutgoingProfile.Profile) (XR eta X : ℝ) (hXR : 0 < XR) : M F XR eta X = XR * F.M eta (X / XR)

theorem NavierStokes.OutgoingDilation.I_scaling (F : OutgoingProfile.Profile) (XR eta X : ℝ) (hXR : 0 < XR) : I F XR eta X = XR * √XR * ∫ (u : ℝ) in Set.Ioc 0 (X / XR), F.H (u, eta)

theorem NavierStokes.OutgoingDilation.J_scaling (F : OutgoingProfile.Profile) (XR eta X : ℝ) (hXR : 0 < XR) : J F XR eta X = XR * √XR * F.J eta (X / XR)

theorem NavierStokes.OutgoingDilation.S_scaling (F : OutgoingProfile.Profile) (XR eta X : ℝ) (hXR : 0 < XR) : S F XR eta X = XR * ∫ (u : ℝ) in Set.Ioc 0 (X / XR), F.energyDensity eta u

theorem NavierStokes.OutgoingDilation.totalS_scaling (F : OutgoingProfile.Profile) (XR eta : ℝ) (hXR : 0 < XR) : totalS F XR eta = XR * F.totalS eta

theorem NavierStokes.OutgoingDilation.renormalizedI_scaling (F : OutgoingProfile.Profile) (XR eta : ℝ) (hXR : 0 < XR) : renormalizedI F XR eta = XR * √XR * ∫ (u : ℝ) in Set.Ioi 0, F.H (u, eta) - F.powerH u

theorem NavierStokes.OutgoingDilation.positive (F : OutgoingProfile.Profile) (XR : ℝ) (p : ℝ × ℝ) : 0 < E F XR p

theorem NavierStokes.OutgoingDilation.dilation_contDiffOn (XR : ℝ) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × ℝ) => (p.1 / XR, p.2)) OutgoingProfile.domain

theorem NavierStokes.OutgoingDilation.dilation_mapsTo (XR : ℝ) (hXR : 0 < XR) : Set.MapsTo (fun (p : ℝ × ℝ) => (p.1 / XR, p.2)) OutgoingProfile.domain OutgoingProfile.domain

theorem NavierStokes.OutgoingDilation.E_contDiffOn (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) : ContDiffOn ℝ (↑⊤) (E F XR) OutgoingProfile.domain

theorem NavierStokes.OutgoingDilation.U_contDiffOn (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) : ContDiffOn ℝ (↑⊤) (U F XR) OutgoingProfile.domain

theorem NavierStokes.OutgoingDilation.H_contDiffOn (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) : ContDiffOn ℝ (↑⊤) (H F XR) OutgoingProfile.domain

theorem NavierStokes.OutgoingDilation.Pi_contDiffOn (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) : ContDiffOn ℝ (↑⊤) (Pi F XR) OutgoingProfile.domain

def NavierStokes.OutgoingDilation.familyDomain : Set (ℝ × ℝ × ℝ)

Family domain, given by Ioi 0 ×ˢ domain.

Equations

• NavierStokes.OutgoingDilation.familyDomain = Set.Ioi 0 ×ˢ NavierStokes.OutgoingProfile.domain

theorem NavierStokes.OutgoingDilation.dilation_family_contDiffOn : ContDiffOn ℝ (↑⊤) (fun (z : ℝ × ℝ × ℝ) => (z.2.1 / z.1, z.2.2)) familyDomain

theorem NavierStokes.OutgoingDilation.dilation_family_mapsTo : Set.MapsTo (fun (z : ℝ × ℝ × ℝ) => (z.2.1 / z.1, z.2.2)) familyDomain OutgoingProfile.domain

theorem NavierStokes.OutgoingDilation.E_family_contDiffOn (F : OutgoingProfile.Profile) : ContDiffOn ℝ (↑⊤) (fun (z : ℝ × ℝ × ℝ) => E F z.1 z.2) familyDomain

theorem NavierStokes.OutgoingDilation.U_family_contDiffOn (F : OutgoingProfile.Profile) : ContDiffOn ℝ (↑⊤) (fun (z : ℝ × ℝ × ℝ) => U F z.1 z.2) familyDomain

theorem NavierStokes.OutgoingDilation.H_family_contDiffOn (F : OutgoingProfile.Profile) : ContDiffOn ℝ (↑⊤) (fun (z : ℝ × ℝ × ℝ) => H F z.1 z.2) familyDomain

theorem NavierStokes.OutgoingDilation.Pi_family_contDiffOn (F : OutgoingProfile.Profile) : ContDiffOn ℝ (↑⊤) (fun (z : ℝ × ℝ × ℝ) => Pi F z.1 z.2) familyDomain

theorem NavierStokes.OutgoingDilation.mass_integrable (F : OutgoingProfile.Profile) (XR eta : ℝ) (hXR : 0 < XR) : MeasureTheory.IntegrableOn (fun (X : ℝ) => U F XR (X, eta)) (Set.Ioi 0) MeasureTheory.volume

theorem NavierStokes.OutgoingDilation.angular_integrable (F : OutgoingProfile.Profile) (XR eta : ℝ) (hXR : 0 < XR) : MeasureTheory.IntegrableOn (fun (X : ℝ) => H F XR (X, eta) * U F XR (X, eta)) (Set.Ioi 0) MeasureTheory.volume

theorem NavierStokes.OutgoingDilation.energy_integrable (F : OutgoingProfile.Profile) (XR eta : ℝ) (hXR : 0 < XR) : MeasureTheory.IntegrableOn (energyDensity F XR eta) (Set.Ioi 0) MeasureTheory.volume

theorem NavierStokes.OutgoingDilation.renormalized_integrable (F : OutgoingProfile.Profile) (XR eta : ℝ) (hXR : 0 < XR) : MeasureTheory.IntegrableOn (fun (X : ℝ) => H F XR (X, eta) - powerH F XR X) (Set.Ioi 0) MeasureTheory.volume

theorem NavierStokes.OutgoingDilation.normalized_I_integrable (F : OutgoingProfile.Profile) (eta X : ℝ) (hX : 0 < X) : MeasureTheory.IntegrableOn (fun (u : ℝ) => F.H (u, eta)) (Set.Ioc 0 X) MeasureTheory.volume

theorem NavierStokes.OutgoingDilation.I_integrable (F : OutgoingProfile.Profile) (XR eta X : ℝ) (hXR : 0 < XR) (hX : 0 < X) : MeasureTheory.IntegrableOn (fun (u : ℝ) => H F XR (u, eta)) (Set.Ioc 0 X) MeasureTheory.volume

theorem NavierStokes.OutgoingDilation.mass_total_zero (F : OutgoingProfile.Profile) (XR eta : ℝ) (hXR : 0 < XR) : ∫ (X : ℝ) in Set.Ioi 0, U F XR (X, eta) = 0

theorem NavierStokes.OutgoingDilation.angular_total_zero (F : OutgoingProfile.Profile) (XR eta : ℝ) (hXR : 0 < XR) : ∫ (X : ℝ) in Set.Ioi 0, H F XR (X, eta) * U F XR (X, eta) = 0

theorem NavierStokes.OutgoingDilation.renormalized_zero (F : OutgoingProfile.Profile) (XR eta : ℝ) (hXR : 0 < XR) : renormalizedI F XR eta = 0

theorem NavierStokes.OutgoingDilation.energy_zero {F : OutgoingProfile.Profile} {C : ℝ} (hF : OutgoingProfile.Specification F C) (XR eta : ℝ) (hXR : 0 < XR) (heta : eta ^ 2 ≤ 1) : totalS F XR eta = 0

theorem NavierStokes.OutgoingDilation.canonicalKernel_integral (F : OutgoingProfile.Profile) (XR eta X : ℝ) (hXR : 0 < XR) : ∫ (u : ℝ) in Set.Ioi X, canonicalKernel F XR eta u = ∫ (u : ℝ) in Set.Ioi (X / XR), F.canonicalKernel eta u

theorem NavierStokes.OutgoingDilation.canonicalKernel_integrable (F : OutgoingProfile.Profile) (XR eta : ℝ) (hXR : 0 < XR) : MeasureTheory.IntegrableOn (canonicalKernel F XR eta) (Set.Ioi 0) MeasureTheory.volume

theorem NavierStokes.OutgoingDilation.Pi_canonical (F : OutgoingProfile.Profile) (XR eta X : ℝ) (hXR : 0 < XR) (hX : 0 < X) : Pi F XR (X, eta) = -(1 / 2) * ∫ (u : ℝ) in Set.Ioi X, E F XR (u, eta) ^ 2 / u

theorem NavierStokes.OutgoingDilation.normalized_axisDatum_integral (F : OutgoingProfile.Profile) (eta : ℝ) : F.axisDatum eta = -(1 / 2) * ∫ (u : ℝ) in Set.Ioi 0, F.canonicalKernel eta u

theorem NavierStokes.OutgoingDilation.axisDatum_unchanged (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) : axisDatum F XR = F.axisDatum

theorem NavierStokes.OutgoingDilation.Pi_tendsto_axis (F : OutgoingProfile.Profile) (XR eta : ℝ) (hXR : 0 < XR) : Filter.Tendsto (fun (X : ℝ) => Pi F XR (X, eta)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (axisDatum F XR eta))

noncomputable def NavierStokes.OutgoingDilation.clock (XR X : ℝ) : ℝ

Clock, given by Real.log (X / XR).

Equations

• NavierStokes.OutgoingDilation.clock XR X = Real.log (X / XR)

noncomputable def NavierStokes.OutgoingDilation.radius (XR y : ℝ) : ℝ

Radius, given by XR * Real.exp y.

Equations

• NavierStokes.OutgoingDilation.radius XR y = XR * Real.exp y

theorem NavierStokes.OutgoingDilation.radius_pos (XR y : ℝ) (hXR : 0 < XR) : 0 < radius XR y

theorem NavierStokes.OutgoingDilation.clock_radius (XR y : ℝ) (hXR : 0 < XR) : clock XR (radius XR y) = y

theorem NavierStokes.OutgoingDilation.clock_center (XR X y : ℝ) (hXR : 0 < XR) (hX : 0 < X) : y + Real.log (X / radius XR y) = clock XR X

theorem NavierStokes.OutgoingDilation.clock_radius_mul (XR y x : ℝ) (hXR : 0 < XR) (hx : 0 < x) : clock XR (radius XR y * x) = y + Real.log x

theorem NavierStokes.OutgoingDilation.radius_le_iff (XR X y : ℝ) (hXR : 0 < XR) (hX : 0 < X) : radius XR y ≤ X ↔ y ≤ clock XR X

theorem NavierStokes.OutgoingDilation.radius_lt_iff (XR X y : ℝ) (hXR : 0 < XR) (hX : 0 < X) : radius XR y < X ↔ y < clock XR X

noncomputable def NavierStokes.OutgoingDilation.pulseEndRadius (F : OutgoingProfile.Profile) (XR : ℝ) : ℝ

Pulse end radius, given by radius XR F.data.core.endpoint.

Equations

• NavierStokes.OutgoingDilation.pulseEndRadius F XR = NavierStokes.OutgoingDilation.radius XR F.data.core.endpoint

noncomputable def NavierStokes.OutgoingDilation.tailRadius (F : OutgoingProfile.Profile) (XR : ℝ) : ℝ

Tail radius, given by radius XR (tailEnd F.data).

Equations

• NavierStokes.OutgoingDilation.tailRadius F XR = NavierStokes.OutgoingDilation.radius XR (NavierStokes.OutgoingTail.tailEnd F.data)

noncomputable def NavierStokes.OutgoingDilation.switchRadius (F : OutgoingProfile.Profile) (XR : ℝ) : ℝ

Switch radius, given by radius XR (HeatTailEdit.switchStart F.data).

Equations

• NavierStokes.OutgoingDilation.switchRadius F XR = NavierStokes.OutgoingDilation.radius XR (NavierStokes.HeatTailEdit.switchStart F.data)

noncomputable def NavierStokes.OutgoingDilation.carrierAmplitude (F : OutgoingProfile.Profile) : ℝ

Carrier amplitude, given by HeatTailEdit.outgoingAmplitude F.data.

Equations

• NavierStokes.OutgoingDilation.carrierAmplitude F = NavierStokes.HeatTailEdit.outgoingAmplitude F.data

theorem NavierStokes.OutgoingDilation.switchRadius_eq (F : OutgoingProfile.Profile) (XR : ℝ) : switchRadius F XR = XR * Real.exp (OutgoingTail.tailStart F.data + 1 / 5)

theorem NavierStokes.OutgoingDilation.switchRadius_pos (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) : 0 < switchRadius F XR

theorem NavierStokes.OutgoingDilation.carrierAmplitude_pos (F : OutgoingProfile.Profile) : 0 < carrierAmplitude F

theorem NavierStokes.OutgoingDilation.ideal_prefix (F : OutgoingProfile.Profile) (XR eta X : ℝ) (hXR : 0 < XR) (hX : 0 < X) (hX' : X ≤ XR) : E F XR (X, eta) = F.data.core.P * OutgoingSchedule.shape eta * (X / XR) ^ (1 / 10) ∧ U F XR (X, eta) = 4 * eta ∧ Pi F XR (X, eta) = axisDatum F XR eta + 5 / 2 * F.data.core.P ^ 2 * OutgoingSchedule.shape eta ^ 2 * (X / XR) ^ (1 / 5)

theorem NavierStokes.OutgoingDilation.after_pulse (F : OutgoingProfile.Profile) (XR eta X : ℝ) (hXR : 0 < XR) (hX : 0 < X) (hfar : pulseEndRadius F XR ≤ X) : U F XR (X, eta) = 0 ∧ M F XR eta X = 0 ∧ J F XR eta X = 0

theorem NavierStokes.OutgoingDilation.powerE_coefficient (F : OutgoingProfile.Profile) (XR X : ℝ) (hXR : 0 < XR) (hX : 0 < X) : powerE F XR X = OutgoingTail.powerConstant F.data * XR ^ (1 / 2 + F.data.h) * X ^ (-(1 / 2 + F.data.h))

theorem NavierStokes.OutgoingDilation.eventual_power (F : OutgoingProfile.Profile) (XR eta X : ℝ) (hXR : 0 < XR) (hX : 0 < X) (hfar : tailRadius F XR ≤ X) : U F XR (X, eta) = 0 ∧ E F XR (X, eta) = powerE F XR X ∧ I F XR eta X = X * H F XR (X, eta) / (1 - F.data.h)

theorem NavierStokes.OutgoingDilation.E_eq_clean_switch_profile (F : OutgoingProfile.Profile) (XR eta X : ℝ) (hXR : 0 < XR) (hX : switchRadius F XR ≤ X) : E F XR (X, eta) = HeatTailEdit.outgoingProfile F.data (switchRadius F XR) eta X

theorem NavierStokes.OutgoingDilation.E_tail_factorization (F : OutgoingProfile.Profile) (XR eta X : ℝ) (hXR : 0 < XR) (hX : switchRadius F XR ≤ X) : E F XR (X, eta) = HeatTailEdit.powerTail F.data.h (carrierAmplitude F) (switchRadius F XR) (HeatTailEdit.outgoingShape F.data) X

theorem NavierStokes.OutgoingDilation.E_at_switch (F : OutgoingProfile.Profile) (XR eta : ℝ) (hXR : 0 < XR) : E F XR (switchRadius F XR, eta) = carrierAmplitude F * (1 - F.data.rho)

theorem NavierStokes.OutgoingDilation.switchRadius_tendsto (F : OutgoingProfile.Profile) : Filter.Tendsto (switchRadius F) Filter.atTop Filter.atTop

The actual second reserved shaped-wait patch

noncomputable def NavierStokes.OutgoingDilation.patchClock (F : OutgoingProfile.Profile) : ℝ

Patch clock, given by F.data.core.pulseStart - 20.

Equations

• NavierStokes.OutgoingDilation.patchClock F = F.data.core.pulseStart - 20

noncomputable def NavierStokes.OutgoingDilation.patchRadius (F : OutgoingProfile.Profile) (XR : ℝ) : ℝ

Patch radius, given by radius XR (patchClock F).

Equations

• NavierStokes.OutgoingDilation.patchRadius F XR = NavierStokes.OutgoingDilation.radius XR (NavierStokes.OutgoingDilation.patchClock F)

noncomputable def NavierStokes.OutgoingDilation.patchRatio (F : OutgoingProfile.Profile) : ℝ

Patch ratio, given by Real.exp (patchClock F - HeatTailEdit.switchStart F.data).

Equations

• NavierStokes.OutgoingDilation.patchRatio F = Real.exp (NavierStokes.OutgoingDilation.patchClock F - NavierStokes.HeatTailEdit.switchStart F.data)

noncomputable def NavierStokes.OutgoingDilation.patchAmplitude (F : OutgoingProfile.Profile) : ℝ

Patch amplitude, given by OutgoingSchedule.radialAmplitude F.data.core.P F.data.core.dropLength F.data.core.lam (patchClock F).

Equations

• NavierStokes.OutgoingDilation.patchAmplitude F = NavierStokes.OutgoingSchedule.radialAmplitude F.data.core.P F.data.core.dropLength F.data.core.lam (NavierStokes.OutgoingDilation.patchClock F)

noncomputable def NavierStokes.OutgoingDilation.shapedPatchAmplitude (F : OutgoingProfile.Profile) (eta : ℝ) : ℝ

Shaped patch amplitude, given by patchAmplitude F * OutgoingSchedule.shape eta.

Equations

• NavierStokes.OutgoingDilation.shapedPatchAmplitude F eta = NavierStokes.OutgoingDilation.patchAmplitude F * NavierStokes.OutgoingSchedule.shape eta

noncomputable def NavierStokes.OutgoingDilation.compensationPatch : TerminalCompensation.Patch

In the coordinate x = X / patchRadius, the second reserved patch is the fixed interval (1, exp 5).

Equations

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

theorem NavierStokes.OutgoingDilation.patchClock_after_hold (F : OutgoingProfile.Profile) : F.data.core.holdStart < patchClock F

theorem NavierStokes.OutgoingDilation.patchClock_end_before_pulse (F : OutgoingProfile.Profile) : patchClock F + 5 < F.data.core.pulseStart

theorem NavierStokes.OutgoingDilation.patchClock_end_before_switch (F : OutgoingProfile.Profile) : patchClock F + 5 < HeatTailEdit.switchStart F.data

theorem NavierStokes.OutgoingDilation.patchRadius_pos (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) : 0 < patchRadius F XR

theorem NavierStokes.OutgoingDilation.patchAmplitude_pos (F : OutgoingProfile.Profile) : 0 < patchAmplitude F

theorem NavierStokes.OutgoingDilation.shapedPatchAmplitude_pos (F : OutgoingProfile.Profile) (eta : ℝ) : 0 < shapedPatchAmplitude F eta

theorem NavierStokes.OutgoingDilation.shapedPatchAmplitude_contDiff (F : OutgoingProfile.Profile) : ContDiff ℝ (↑⊤) (shapedPatchAmplitude F)

theorem NavierStokes.OutgoingDilation.patchRatio_pos (F : OutgoingProfile.Profile) : 0 < patchRatio F

theorem NavierStokes.OutgoingDilation.patchRadius_eq_ratio (F : OutgoingProfile.Profile) (XR : ℝ) : patchRadius F XR = patchRatio F * switchRadius F XR

theorem NavierStokes.OutgoingDilation.patchRatio_right_lt_one (F : OutgoingProfile.Profile) : patchRatio F * compensationPatch.right < 1

theorem NavierStokes.OutgoingDilation.patch_before_switch (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) : patchRadius F XR * compensationPatch.right < switchRadius F XR

theorem NavierStokes.OutgoingDilation.patch_switch_disjoint (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) : Disjoint (Set.Icc (patchRadius F XR) (patchRadius F XR * compensationPatch.right)) (Set.Ici (switchRadius F XR))

theorem NavierStokes.OutgoingDilation.patch_log_bounds {x : ℝ} (hx : x ∈ Set.Icc compensationPatch.left compensationPatch.right) : 0 < x ∧ 0 ≤ Real.log x ∧ Real.log x ≤ 5

theorem NavierStokes.OutgoingDilation.U_on_patch (F : OutgoingProfile.Profile) (XR eta x : ℝ) (hXR : 0 < XR) (hx : x ∈ Set.Icc compensationPatch.left compensationPatch.right) : U F XR (patchRadius F XR * x, eta) = 0

theorem NavierStokes.OutgoingDilation.E_on_patch (F : OutgoingProfile.Profile) (XR eta x : ℝ) (hXR : 0 < XR) (hx : x ∈ Set.Icc compensationPatch.left compensationPatch.right) : E F XR (patchRadius F XR * x, eta) = shapedPatchAmplitude F eta * x ^ (-(1 / 2 + F.data.core.lam))

theorem NavierStokes.OutgoingDilation.patch_fields (F : OutgoingProfile.Profile) (XR eta x : ℝ) (hXR : 0 < XR) (hx : x ∈ Set.Icc compensationPatch.left compensationPatch.right) : U F XR (patchRadius F XR * x, eta) = 0 ∧ E F XR (patchRadius F XR * x, eta) = shapedPatchAmplitude F eta * x ^ (-(1 / 2 + F.data.core.lam))

The actual second reserved patch has the exact shaped power used by the terminal compensation solver, and the axial field is zero there.

theorem NavierStokes.OutgoingDilation.patch_model (F : OutgoingProfile.Profile) (XR eta X : ℝ) (hXR : 0 < XR) (hX : X / patchRadius F XR ∈ Set.Icc compensationPatch.left compensationPatch.right) : E F XR (X, eta) = TerminalCompensation.cleanProfile F.data.core.lam (patchRadius F XR) (shapedPatchAmplitude F eta) X

theorem NavierStokes.OutgoingDilation.correction_zero_after_switch (F : OutgoingProfile.Profile) (XR X : ℝ) (hXR : 0 < XR) (c : TerminalCompensation.Coeff) (hX : switchRadius F XR ≤ X) : TerminalCompensation.correction compensationPatch c (X / patchRadius F XR) = 0

theorem NavierStokes.OutgoingDilation.correction_times_U_zero (F : OutgoingProfile.Profile) (XR eta X : ℝ) (hXR : 0 < XR) (c : TerminalCompensation.Coeff) : TerminalCompensation.correction compensationPatch c (X / patchRadius F XR) * U F XR (X, eta) = 0

Any additive correction on this actual patch leaves E*U pointwise unchanged, before solving its three compensation moments.

structure NavierStokes.OutgoingDilation.DilatedSpecification (F : OutgoingProfile.Profile) (XR : ℝ) : Prop

A specification for actual fields in the unnormalized radial variable.

• angular_smooth : ContDiffOn ℝ (↑⊤) (E F XR) OutgoingProfile.domain
• axial_smooth : ContDiffOn ℝ (↑⊤) (U F XR) OutgoingProfile.domain
• momentum_smooth : ContDiffOn ℝ (↑⊤) (H F XR) OutgoingProfile.domain
• pressure_smooth : ContDiffOn ℝ (↑⊤) (Pi F XR) OutgoingProfile.domain
• angular_positive (p : ℝ × ℝ) : p ∈ OutgoingProfile.domain → 0 < E F XR p
• mass_integrable (eta : ℝ) : MeasureTheory.IntegrableOn (fun (X : ℝ) => U F XR (X, eta)) (Set.Ioi 0) MeasureTheory.volume
• angular_integrable (eta : ℝ) : MeasureTheory.IntegrableOn (fun (X : ℝ) => H F XR (X, eta) * U F XR (X, eta)) (Set.Ioi 0) MeasureTheory.volume
• mass_zero (eta : ℝ) : ∫ (X : ℝ) in Set.Ioi 0, U F XR (X, eta) = 0
• angular_zero (eta : ℝ) : ∫ (X : ℝ) in Set.Ioi 0, H F XR (X, eta) * U F XR (X, eta) = 0
• after_pulse (eta X : ℝ) : 0 < X → pulseEndRadius F XR ≤ X → U F XR (X, eta) = 0 ∧ M F XR eta X = 0 ∧ J F XR eta X = 0
• energy_integrable (eta : ℝ) : MeasureTheory.IntegrableOn (energyDensity F XR eta) (Set.Ioi 0) MeasureTheory.volume
• energy_zero (eta : ℝ) : eta ^ 2 ≤ 1 → totalS F XR eta = 0
• renormalized_integrable (eta : ℝ) : MeasureTheory.IntegrableOn (fun (X : ℝ) => H F XR (X, eta) - powerH F XR X) (Set.Ioi 0) MeasureTheory.volume
• renormalized_zero (eta : ℝ) : renormalizedI F XR eta = 0
• eventual_power (eta X : ℝ) : 0 < X → tailRadius F XR ≤ X → U F XR (X, eta) = 0 ∧ E F XR (X, eta) = powerE F XR X ∧ I F XR eta X = X * H F XR (X, eta) / (1 - F.data.h)
• ideal_prefix (eta X : ℝ) : 0 < X → X ≤ XR → E F XR (X, eta) = F.data.core.P * OutgoingSchedule.shape eta * (X / XR) ^ (1 / 10) ∧ U F XR (X, eta) = 4 * eta ∧ Pi F XR (X, eta) = axisDatum F XR eta + 5 / 2 * F.data.core.P ^ 2 * OutgoingSchedule.shape eta ^ 2 * (X / XR) ^ (1 / 5)
• pressure_integrable (eta : ℝ) : MeasureTheory.IntegrableOn (canonicalKernel F XR eta) (Set.Ioi 0) MeasureTheory.volume
• pressure_canonical (eta X : ℝ) : 0 < X → Pi F XR (X, eta) = -(1 / 2) * ∫ (u : ℝ) in Set.Ioi X, E F XR (u, eta) ^ 2 / u
• axis_unchanged : axisDatum F XR = F.axisDatum
• axis_limit (eta : ℝ) : Filter.Tendsto (fun (X : ℝ) => Pi F XR (X, eta)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (axisDatum F XR eta))
• fixed_switch_amplitude (eta : ℝ) : E F XR (switchRadius F XR, eta) = carrierAmplitude F * (1 - F.data.rho)
• shaped_patch (eta x : ℝ) : x ∈ Set.Icc compensationPatch.left compensationPatch.right → U F XR (patchRadius F XR * x, eta) = 0 ∧ E F XR (patchRadius F XR * x, eta) = shapedPatchAmplitude F eta * x ^ (-(1 / 2 + F.data.core.lam))
• patch_disjoint : Disjoint (Set.Icc (patchRadius F XR) (patchRadius F XR * compensationPatch.right)) (Set.Ici (switchRadius F XR))

theorem NavierStokes.OutgoingDilation.preserves_specification {F : OutgoingProfile.Profile} {C : ℝ} (hF : OutgoingProfile.Specification F C) (XR : ℝ) (hXR : 0 < XR) : DilatedSpecification F XR

theorem NavierStokes.OutgoingDilation.exists_dilated_outgoing_profiles (P m : ℝ) (hP : 0 < P) (hm : 0 < m) : ∃ (lam₀ : ℝ) (C : ℝ), 0 < lam₀ ∧ 0 < C ∧ ∀ (lam : ℝ), 0 < lam → lam < lam₀ → ∀ (h : ℝ), 0 < h → 2 * h < lam → ∃ (F : OutgoingProfile.Profile), F.data.core.P = P ∧ F.data.core.m = m ∧ F.data.core.lam = lam ∧ F.data.h = h ∧ OutgoingProfile.Specification F C ∧ ∀ (XR : ℝ), 0 < XR → DilatedSpecification F XR

The same reset and amplitude work simultaneously for every entrance radius. The schedule is chosen once, before the radius is selected.

theorem NavierStokes.OutgoingDilation.exists_fixed_schedule (P m : ℝ) (hP : 0 < P) (hm : 0 < m) : ∃ (lam : ℝ) (C : ℝ), 0 < lam ∧ 0 < C ∧ ∀ (h : ℝ), 0 < h → 2 * h < lam → ∃ (F : OutgoingProfile.Profile), F.data.core.P = P ∧ F.data.core.m = m ∧ F.data.core.lam = lam ∧ F.data.h = h ∧ OutgoingProfile.Specification F C ∧ ∀ (XR : ℝ), 0 < XR → DilatedSpecification F XR

@[reducible, inline]

abbrev NavierStokes.HeatedOutgoing.Coeff : Type

Coefficient: an abbreviation for TerminalCompensation.Coeff.

Equations

• NavierStokes.HeatedOutgoing.Coeff = NavierStokes.TerminalCompensation.Coeff

def NavierStokes.HeatedOutgoing.parameterDomain : Set ℝ

Parameter domain, given by Icc (-1) 1.

Equations

• NavierStokes.HeatedOutgoing.parameterDomain = Set.Icc (-1) 1

def NavierStokes.HeatedOutgoing.domain : Set (ℝ × ℝ)

Domain, given by Ioi 0 ×ˢ parameterDomain.

Equations

• NavierStokes.HeatedOutgoing.domain = Set.Ioi 0 ×ˢ NavierStokes.HeatedOutgoing.parameterDomain

noncomputable def NavierStokes.HeatedOutgoing.heatE (F : OutgoingProfile.Profile) (XR : ℝ) (p : ℝ × ℝ) : ℝ

Heat E, given by OutgoingDilation.E F XR p * HeatTailEdit.multiplier F.data.h (ParametricHeatTail.diffusion p.2) (switchRadius F XR) p.1.

Equations

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

noncomputable def NavierStokes.HeatedOutgoing.patchIncrement (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (p : ℝ × ℝ) : ℝ

Patch increment, given by shapedPatchAmplitude F p.2 * TerminalCompensation.correction compensationPatch (c p.2) (p.1 / patchRadius F XR).

Equations

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

noncomputable def NavierStokes.HeatedOutgoing.E (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (p : ℝ × ℝ) : ℝ

E, given by heatE F XR p + patchIncrement F XR c p.

Equations

• NavierStokes.HeatedOutgoing.E F XR c p = NavierStokes.HeatedOutgoing.heatE F XR p + NavierStokes.HeatedOutgoing.patchIncrement F XR c p

noncomputable def NavierStokes.HeatedOutgoing.U (F : OutgoingProfile.Profile) (XR : ℝ) : ℝ × ℝ → ℝ

U, given by OutgoingDilation.U F XR.

Equations

• NavierStokes.HeatedOutgoing.U F XR = NavierStokes.OutgoingDilation.U F XR

noncomputable def NavierStokes.HeatedOutgoing.H (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (p : ℝ × ℝ) : ℝ

H, given by Real.sqrt (2 * p.1) * E F XR c p.

Equations

• NavierStokes.HeatedOutgoing.H F XR c p = √(2 * p.1) * NavierStokes.HeatedOutgoing.E F XR c p

noncomputable def NavierStokes.HeatedOutgoing.canonicalKernel (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (eta X : ℝ) : ℝ

Canonical kernel, given by E F XR c (X, eta) ^ 2 / X.

Equations

• NavierStokes.HeatedOutgoing.canonicalKernel F XR c eta X = NavierStokes.HeatedOutgoing.E F XR c (X, eta) ^ 2 / X

noncomputable def NavierStokes.HeatedOutgoing.Pi (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (p : ℝ × ℝ) : ℝ

Pi, given by -(1 / 2 : ℝ) * ∫ X in Ioi p.1, canonicalKernel F XR c p.2 X.

Equations

• NavierStokes.HeatedOutgoing.Pi F XR c p = -(1 / 2) * ∫ (X : ℝ) in Set.Ioi p.1, NavierStokes.HeatedOutgoing.canonicalKernel F XR c p.2 X

noncomputable def NavierStokes.HeatedOutgoing.axisDatum (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (eta : ℝ) : ℝ

Axis datum, given by -(1 / 2 : ℝ) * ∫ X in Ioi 0, canonicalKernel F XR c eta X.

Equations

• NavierStokes.HeatedOutgoing.axisDatum F XR c eta = -(1 / 2) * ∫ (X : ℝ) in Set.Ioi 0, NavierStokes.HeatedOutgoing.canonicalKernel F XR c eta X

noncomputable def NavierStokes.HeatedOutgoing.energyDensity (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (eta X : ℝ) : ℝ

Energy density, given by U F XR (X, eta) ^ 2 - E F XR c (X, eta) ^ 2 / 2.

Equations

• NavierStokes.HeatedOutgoing.energyDensity F XR c eta X = NavierStokes.HeatedOutgoing.U F XR (X, eta) ^ 2 - NavierStokes.HeatedOutgoing.E F XR c (X, eta) ^ 2 / 2

noncomputable def NavierStokes.HeatedOutgoing.totalS (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (eta : ℝ) : ℝ

Total S, given by ∫ X in Ioi 0, energyDensity F XR c eta X.

Equations

• NavierStokes.HeatedOutgoing.totalS F XR c eta = ∫ (X : ℝ) in Set.Ioi 0, NavierStokes.HeatedOutgoing.energyDensity F XR c eta X

noncomputable def NavierStokes.HeatedOutgoing.M (F : OutgoingProfile.Profile) (XR eta X : ℝ) : ℝ

M, given by ∫ u in Ioc 0 X, U F XR (u, eta).

Equations

• NavierStokes.HeatedOutgoing.M F XR eta X = ∫ (u : ℝ) in Set.Ioc 0 X, NavierStokes.HeatedOutgoing.U F XR (u, eta)

noncomputable def NavierStokes.HeatedOutgoing.J (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (eta X : ℝ) : ℝ

J, given by ∫ u in Ioc 0 X, H F XR c (u, eta) * U F XR (u, eta).

Equations

• NavierStokes.HeatedOutgoing.J F XR c eta X = ∫ (u : ℝ) in Set.Ioc 0 X, NavierStokes.HeatedOutgoing.H F XR c (u, eta) * NavierStokes.HeatedOutgoing.U F XR (u, eta)

noncomputable def NavierStokes.HeatedOutgoing.extendedHeatE (F : OutgoingProfile.Profile) (XR : ℝ) (p : ℝ × ℝ) : ℝ

Only the already proved smooth extension is used off the physical band.

Equations

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

theorem NavierStokes.HeatedOutgoing.heatE_eq_extended (F : OutgoingProfile.Profile) (XR : ℝ) {p : ℝ × ℝ} (hp : p ∈ domain) : heatE F XR p = extendedHeatE F XR p

theorem NavierStokes.HeatedOutgoing.extendedHeatE_contDiffOn (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) : ContDiffOn ℝ (↑⊤) (extendedHeatE F XR) OutgoingProfile.domain

theorem NavierStokes.HeatedOutgoing.heatE_contDiffOn (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) : ContDiffOn ℝ (↑⊤) (heatE F XR) domain

theorem NavierStokes.HeatedOutgoing.patchIncrement_contDiffOn (F : OutgoingProfile.Profile) (XR : ℝ) {c : ℝ → Coeff} (hc : ContDiffOn ℝ (↑⊤) c parameterDomain) : ContDiffOn ℝ (↑⊤) (patchIncrement F XR c) domain

theorem NavierStokes.HeatedOutgoing.E_contDiffOn (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) {c : ℝ → Coeff} (hc : ContDiffOn ℝ (↑⊤) c parameterDomain) : ContDiffOn ℝ (↑⊤) (E F XR c) domain

theorem NavierStokes.HeatedOutgoing.U_contDiffOn (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) : ContDiffOn ℝ (↑⊤) (U F XR) domain

theorem NavierStokes.HeatedOutgoing.H_contDiffOn (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) {c : ℝ → Coeff} (hc : ContDiffOn ℝ (↑⊤) c parameterDomain) : ContDiffOn ℝ (↑⊤) (H F XR c) domain

theorem NavierStokes.HeatedOutgoing.heatE_before (F : OutgoingProfile.Profile) (XR eta X : ℝ) (hXR : 0 < XR) (hX : 0 < X) (hXK : X ≤ OutgoingDilation.switchRadius F XR) : heatE F XR (X, eta) = OutgoingDilation.E F XR (X, eta)

theorem NavierStokes.HeatedOutgoing.heatE_after (F : OutgoingProfile.Profile) (XR eta X : ℝ) (hXR : 0 < XR) (hXK : OutgoingDilation.switchRadius F XR ≤ X) : heatE F XR (X, eta) = ParametricHeatTail.physicalEdit F.data (OutgoingDilation.switchRadius F XR) eta X

theorem NavierStokes.HeatedOutgoing.E_after_switch (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (eta X : ℝ) (hXR : 0 < XR) (hXK : OutgoingDilation.switchRadius F XR ≤ X) : E F XR c (X, eta) = ParametricHeatTail.physicalEdit F.data (OutgoingDilation.switchRadius F XR) eta X

theorem NavierStokes.HeatedOutgoing.patch_below_switch (F : OutgoingProfile.Profile) (XR X : ℝ) (hXR : 0 < XR) (hpatch : X / OutgoingDilation.patchRadius F XR ∈ Set.Icc OutgoingDilation.compensationPatch.left OutgoingDilation.compensationPatch.right) : X < OutgoingDilation.switchRadius F XR

theorem NavierStokes.HeatedOutgoing.E_on_patch (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (eta X : ℝ) (hXR : 0 < XR) (hX : 0 < X) (hpatch : X / OutgoingDilation.patchRadius F XR ∈ Set.Icc OutgoingDilation.compensationPatch.left OutgoingDilation.compensationPatch.right) : E F XR c (X, eta) = TerminalCompensation.physicalProfile OutgoingDilation.compensationPatch F.data.core.lam (OutgoingDilation.patchRadius F XR) (OutgoingDilation.shapedPatchAmplitude F eta) (c eta) X

theorem NavierStokes.HeatedOutgoing.patchIncrement_eq_difference (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (eta X : ℝ) : patchIncrement F XR c (X, eta) = TerminalCompensation.physicalProfile OutgoingDilation.compensationPatch F.data.core.lam (OutgoingDilation.patchRadius F XR) (OutgoingDilation.shapedPatchAmplitude F eta) (c eta) X - TerminalCompensation.cleanProfile F.data.core.lam (OutgoingDilation.patchRadius F XR) (OutgoingDilation.shapedPatchAmplitude F eta) X

theorem NavierStokes.HeatedOutgoing.correction_zero_outside (c : Coeff) {x : ℝ} (hx : x ∉ Set.Icc OutgoingDilation.compensationPatch.left OutgoingDilation.compensationPatch.right) : TerminalCompensation.correction OutgoingDilation.compensationPatch c x = 0

theorem NavierStokes.HeatedOutgoing.E_before_patch (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (eta X : ℝ) (hXR : 0 < XR) (hX : 0 < X) (hpatch : X ≤ OutgoingDilation.patchRadius F XR) : E F XR c (X, eta) = OutgoingDilation.E F XR (X, eta)

theorem NavierStokes.HeatedOutgoing.heatE_pos (F : OutgoingProfile.Profile) (XR eta X : ℝ) (hX : 0 < X) (heta : eta ∈ parameterDomain) : 0 < heatE F XR (X, eta)

noncomputable def NavierStokes.HeatedOutgoing.heatRow (F : OutgoingProfile.Profile) (XR eta : ℝ) (i : Fin 3) (X : ℝ) : ℝ

Heat row as an element of ℝ.

Equations

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

noncomputable def NavierStokes.HeatedOutgoing.patchRow (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (eta : ℝ) (i : Fin 3) (X : ℝ) : ℝ

Patch row as an element of ℝ.

Equations

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

noncomputable def NavierStokes.HeatedOutgoing.changeRow (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (eta : ℝ) (i : Fin 3) (X : ℝ) : ℝ

Change row as an element of ℝ.

Equations

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

theorem NavierStokes.HeatedOutgoing.heat_differences (F : OutgoingProfile.Profile) (XR eta X : ℝ) (hXR : 0 < XR) (hX : 0 < X) : heatE F XR (X, eta) - OutgoingDilation.E F XR (X, eta) = HeatTailEdit.change (HeatTailEdit.outgoingProfile F.data (OutgoingDilation.switchRadius F XR) eta) F.data.h (ParametricHeatTail.diffusion eta) (OutgoingDilation.switchRadius F XR) X ∧ heatE F XR (X, eta) ^ 2 - OutgoingDilation.E F XR (X, eta) ^ 2 = HeatTailEdit.squareChange (HeatTailEdit.outgoingProfile F.data (OutgoingDilation.switchRadius F XR) eta) F.data.h (ParametricHeatTail.diffusion eta) (OutgoingDilation.switchRadius F XR) X

theorem NavierStokes.HeatedOutgoing.patch_square_difference (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (eta X : ℝ) (hXR : 0 < XR) (hX : 0 < X) : E F XR c (X, eta) ^ 2 - heatE F XR (X, eta) ^ 2 = patchRow F XR c eta 1 X

theorem NavierStokes.HeatedOutgoing.changeRow_decomposition (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (eta : ℝ) (i : Fin 3) (X : ℝ) (hXR : 0 < XR) (hX : 0 < X) : changeRow F XR c eta i X = heatRow F XR eta i X + patchRow F XR c eta i X

theorem NavierStokes.HeatedOutgoing.positive_tail_indicator (f : ℝ → ℝ) (K : ℝ) (hK : 0 < K) (hz : ∀ (X : ℝ), 0 < X → X ≤ K → f X = 0) : (Set.Ioi 0).indicator f = (Set.Ioi K).indicator f

theorem NavierStokes.HeatedOutgoing.integrable_positive_tail (f : ℝ → ℝ) (K : ℝ) (hK : 0 < K) (hz : ∀ (X : ℝ), 0 < X → X ≤ K → f X = 0) (hi : MeasureTheory.IntegrableOn f (Set.Ioi K) MeasureTheory.volume) : MeasureTheory.IntegrableOn f (Set.Ioi 0) MeasureTheory.volume

theorem NavierStokes.HeatedOutgoing.integral_positive_tail (f : ℝ → ℝ) (K : ℝ) (hK : 0 < K) (hz : ∀ (X : ℝ), 0 < X → X ≤ K → f X = 0) : ∫ (X : ℝ) in Set.Ioi 0, f X = ∫ (X : ℝ) in Set.Ioi K, f X

theorem NavierStokes.HeatedOutgoing.heatRow_zero_before (F : OutgoingProfile.Profile) (XR eta : ℝ) (i : Fin 3) (X : ℝ) (hXR : 0 < XR) (hX : 0 < X) (hXK : X ≤ OutgoingDilation.switchRadius F XR) : heatRow F XR eta i X = 0

theorem NavierStokes.HeatedOutgoing.heatRow_integrable (F : OutgoingProfile.Profile) (XR eta : ℝ) (i : Fin 3) (hXR : 0 < XR) (heta : eta ∈ parameterDomain) : MeasureTheory.IntegrableOn (heatRow F XR eta i) (Set.Ioi 0) MeasureTheory.volume

theorem NavierStokes.HeatedOutgoing.heatRow_integral (F : OutgoingProfile.Profile) (XR eta : ℝ) (i : Fin 3) (hXR : 0 < XR) : ∫ (X : ℝ) in Set.Ioi 0, heatRow F XR eta i X = ParametricTerminalCompensation.physicalDebt F.data (OutgoingDilation.switchRadius F XR) eta i

theorem NavierStokes.HeatedOutgoing.patchRow_integrable (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (eta : ℝ) (i : Fin 3) (hXR : 0 < XR) : MeasureTheory.IntegrableOn (patchRow F XR c eta i) (Set.Ioi 0) MeasureTheory.volume

theorem NavierStokes.HeatedOutgoing.patchRow_integral (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (eta : ℝ) (i : Fin 3) (hXR : 0 < XR) : ∫ (X : ℝ) in Set.Ioi 0, patchRow F XR c eta i X = TerminalCompensation.physicalMoments OutgoingDilation.compensationPatch F.data.core.lam (OutgoingDilation.patchRadius F XR) (OutgoingDilation.shapedPatchAmplitude F eta) (c eta) i

structure NavierStokes.HeatedOutgoing.CompensationWitness (F : OutgoingProfile.Profile) (XR C : ℝ) : Type

The coefficients are obtained below from the actual physical heat debts. The base profile, hence its original reset and amplitude, is retained.

• radius_pos : 0 < XR
• switch_large : 1 ≤ OutgoingDilation.switchRadius F XR
• coefficients : ℝ → Coeff

  Coefficients of CompensationWitness, of type ℝ → Coeff.

• smooth : ContDiffOn ℝ (↑⊤) self.coefficients parameterDomain
• moments (eta : ℝ) : eta ∈ parameterDomain → TerminalCompensation.physicalMoments OutgoingDilation.compensationPatch F.data.core.lam (OutgoingDilation.patchRadius F XR) (OutgoingDilation.shapedPatchAmplitude F eta) (self.coefficients eta) + ParametricTerminalCompensation.physicalDebt F.data (OutgoingDilation.switchRadius F XR) eta = 0
• coefficient_bound (eta : ℝ) : eta ∈ parameterDomain → ‖self.coefficients eta‖ ≤ C / OutgoingDilation.switchRadius F XR
• derivative_bound (eta : ℝ) : eta ∈ parameterDomain → ‖derivWithin self.coefficients parameterDomain eta‖ ≤ C / OutgoingDilation.switchRadius F XR
• first_jet (eta : ℝ) : eta ∈ parameterDomain → ParametricTerminalCompensation.FirstJetWithinBound OutgoingDilation.compensationPatch (OutgoingDilation.shapedPatchAmplitude F) self.coefficients parameterDomain eta (C / OutgoingDilation.switchRadius F XR)
• patch_positive (eta : ℝ) : eta ∈ parameterDomain → ∀ (X : ℝ), 0 < X → 0 < TerminalCompensation.physicalProfile OutgoingDilation.compensationPatch F.data.core.lam (OutgoingDilation.patchRadius F XR) (OutgoingDilation.shapedPatchAmplitude F eta) (self.coefficients eta) X

theorem NavierStokes.HeatedOutgoing.exists_compensation (F : OutgoingProfile.Profile) : ∃ (XR₀ : ℝ) (C : ℝ), 0 < XR₀ ∧ 0 < C ∧ ∀ (XR : ℝ), XR₀ ≤ XR → Nonempty (CompensationWitness F XR C)

theorem NavierStokes.HeatedOutgoing.CompensationWitness.positive {F : OutgoingProfile.Profile} {XR C : ℝ} (w : CompensationWitness F XR C) (eta X : ℝ) (heta : eta ∈ parameterDomain) (hX : 0 < X) : 0 < E F XR w.coefficients (X, eta)

theorem NavierStokes.HeatedOutgoing.CompensationWitness.changeRow_integrable {F : OutgoingProfile.Profile} {XR C : ℝ} (w : CompensationWitness F XR C) (eta : ℝ) (i : Fin 3) (heta : eta ∈ parameterDomain) : MeasureTheory.IntegrableOn (changeRow F XR w.coefficients eta i) (Set.Ioi 0) MeasureTheory.volume

theorem NavierStokes.HeatedOutgoing.CompensationWitness.changeRow_integral_zero {F : OutgoingProfile.Profile} {XR C : ℝ} (w : CompensationWitness F XR C) (eta : ℝ) (i : Fin 3) (heta : eta ∈ parameterDomain) : ∫ (X : ℝ) in Set.Ioi 0, changeRow F XR w.coefficients eta i X = 0

theorem NavierStokes.HeatedOutgoing.kernel_decomposition (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (eta X : ℝ) : canonicalKernel F XR c eta X = OutgoingDilation.canonicalKernel F XR eta X + changeRow F XR c eta 0 X

theorem NavierStokes.HeatedOutgoing.energy_decomposition (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (eta X : ℝ) : energyDensity F XR c eta X = OutgoingDilation.energyDensity F XR eta X - changeRow F XR c eta 1 X / 2

theorem NavierStokes.HeatedOutgoing.renormalized_decomposition (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (eta X : ℝ) : H F XR c (X, eta) - OutgoingDilation.powerH F XR X = OutgoingDilation.H F XR (X, eta) - OutgoingDilation.powerH F XR X + changeRow F XR c eta 2 X

theorem NavierStokes.HeatedOutgoing.parameter_sq_le_one {eta : ℝ} (heta : eta ∈ parameterDomain) : eta ^ 2 ≤ 1

theorem NavierStokes.HeatedOutgoing.pulseEnd_le_switch (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) : OutgoingDilation.pulseEndRadius F XR ≤ OutgoingDilation.switchRadius F XR

theorem NavierStokes.HeatedOutgoing.U_after_switch (F : OutgoingProfile.Profile) (XR eta X : ℝ) (hXR : 0 < XR) (hK : OutgoingDilation.switchRadius F XR ≤ X) : U F XR (X, eta) = 0

theorem NavierStokes.HeatedOutgoing.heatE_times_U (F : OutgoingProfile.Profile) (XR eta X : ℝ) (hXR : 0 < XR) (hX : 0 < X) : heatE F XR (X, eta) * U F XR (X, eta) = OutgoingDilation.E F XR (X, eta) * U F XR (X, eta)

theorem NavierStokes.HeatedOutgoing.E_times_U (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (eta X : ℝ) (hXR : 0 < XR) (hX : 0 < X) : E F XR c (X, eta) * U F XR (X, eta) = OutgoingDilation.E F XR (X, eta) * U F XR (X, eta)

theorem NavierStokes.HeatedOutgoing.J_integrand_eq (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (eta X : ℝ) (hXR : 0 < XR) (hX : 0 < X) : H F XR c (X, eta) * U F XR (X, eta) = OutgoingDilation.H F XR (X, eta) * OutgoingDilation.U F XR (X, eta)

theorem NavierStokes.HeatedOutgoing.M_unchanged (F : OutgoingProfile.Profile) (XR eta X : ℝ) : M F XR eta X = OutgoingDilation.M F XR eta X

theorem NavierStokes.HeatedOutgoing.J_unchanged (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (eta X : ℝ) (hXR : 0 < XR) : J F XR c eta X = OutgoingDilation.J F XR eta X

theorem NavierStokes.HeatedOutgoing.entrance_before_patch (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) : XR < OutgoingDilation.patchRadius F XR

theorem NavierStokes.HeatedOutgoing.CompensationWitness.canonicalKernel_integrable {F : OutgoingProfile.Profile} {XR C : ℝ} (w : CompensationWitness F XR C) (eta : ℝ) (heta : eta ∈ parameterDomain) : MeasureTheory.IntegrableOn (canonicalKernel F XR w.coefficients eta) (Set.Ioi 0) MeasureTheory.volume

theorem NavierStokes.HeatedOutgoing.CompensationWitness.pressure_integral_unchanged {F : OutgoingProfile.Profile} {XR C : ℝ} (w : CompensationWitness F XR C) (eta : ℝ) (heta : eta ∈ parameterDomain) : ∫ (X : ℝ) in Set.Ioi 0, canonicalKernel F XR w.coefficients eta X = ∫ (X : ℝ) in Set.Ioi 0, OutgoingDilation.canonicalKernel F XR eta X

theorem NavierStokes.HeatedOutgoing.CompensationWitness.axisDatum_eq {F : OutgoingProfile.Profile} {XR C : ℝ} (w : CompensationWitness F XR C) (eta : ℝ) (heta : eta ∈ parameterDomain) : axisDatum F XR w.coefficients eta = F.axisDatum eta

theorem NavierStokes.HeatedOutgoing.CompensationWitness.energy_integrable {F : OutgoingProfile.Profile} {XR C : ℝ} (w : CompensationWitness F XR C) (eta : ℝ) (heta : eta ∈ parameterDomain) : MeasureTheory.IntegrableOn (energyDensity F XR w.coefficients eta) (Set.Ioi 0) MeasureTheory.volume

theorem NavierStokes.HeatedOutgoing.CompensationWitness.energy_zero {F : OutgoingProfile.Profile} {XR C : ℝ} (w : CompensationWitness F XR C) {B : ℝ} (hF : OutgoingProfile.Specification F B) (eta : ℝ) (heta : eta ∈ parameterDomain) : totalS F XR w.coefficients eta = 0

theorem NavierStokes.HeatedOutgoing.CompensationWitness.renormalized_integrable {F : OutgoingProfile.Profile} {XR C : ℝ} (w : CompensationWitness F XR C) (eta : ℝ) (heta : eta ∈ parameterDomain) : MeasureTheory.IntegrableOn (fun (X : ℝ) => H F XR w.coefficients (X, eta) - OutgoingDilation.powerH F XR X) (Set.Ioi 0) MeasureTheory.volume

theorem NavierStokes.HeatedOutgoing.CompensationWitness.renormalized_zero {F : OutgoingProfile.Profile} {XR C : ℝ} (w : CompensationWitness F XR C) (eta : ℝ) (heta : eta ∈ parameterDomain) : ∫ (X : ℝ) in Set.Ioi 0, H F XR w.coefficients (X, eta) - OutgoingDilation.powerH F XR X = 0

theorem NavierStokes.HeatedOutgoing.CompensationWitness.mass_integrable {F : OutgoingProfile.Profile} {XR C : ℝ} (w : CompensationWitness F XR C) (eta : ℝ) : MeasureTheory.IntegrableOn (fun (X : ℝ) => U F XR (X, eta)) (Set.Ioi 0) MeasureTheory.volume

theorem NavierStokes.HeatedOutgoing.CompensationWitness.angular_integrable {F : OutgoingProfile.Profile} {XR C : ℝ} (w : CompensationWitness F XR C) (eta : ℝ) : MeasureTheory.IntegrableOn (fun (X : ℝ) => H F XR w.coefficients (X, eta) * U F XR (X, eta)) (Set.Ioi 0) MeasureTheory.volume

theorem NavierStokes.HeatedOutgoing.CompensationWitness.mass_zero {F : OutgoingProfile.Profile} {XR C : ℝ} (w : CompensationWitness F XR C) (eta : ℝ) : ∫ (X : ℝ) in Set.Ioi 0, U F XR (X, eta) = 0

theorem NavierStokes.HeatedOutgoing.CompensationWitness.angular_zero {F : OutgoingProfile.Profile} {XR C : ℝ} (w : CompensationWitness F XR C) (eta : ℝ) : ∫ (X : ℝ) in Set.Ioi 0, H F XR w.coefficients (X, eta) * U F XR (X, eta) = 0

theorem NavierStokes.HeatedOutgoing.CompensationWitness.after_pulse {F : OutgoingProfile.Profile} {XR C : ℝ} (w : CompensationWitness F XR C) (eta X : ℝ) (hX : 0 < X) (hfar : OutgoingDilation.pulseEndRadius F XR ≤ X) : U F XR (X, eta) = 0 ∧ M F XR eta X = 0 ∧ J F XR w.coefficients eta X = 0

theorem NavierStokes.HeatedOutgoing.CompensationWitness.Pi_before_patch {F : OutgoingProfile.Profile} {XR C : ℝ} (w : CompensationWitness F XR C) (eta X : ℝ) (heta : eta ∈ parameterDomain) (hX : 0 < X) (hpatch : X ≤ OutgoingDilation.patchRadius F XR) : Pi F XR w.coefficients (X, eta) = OutgoingDilation.Pi F XR (X, eta)

theorem NavierStokes.HeatedOutgoing.CompensationWitness.ideal_prefix {F : OutgoingProfile.Profile} {XR C : ℝ} (w : CompensationWitness F XR C) (eta X : ℝ) (heta : eta ∈ parameterDomain) (hX : 0 < X) (hX' : X ≤ XR) : E F XR w.coefficients (X, eta) = F.data.core.P * OutgoingSchedule.shape eta * (X / XR) ^ (1 / 10) ∧ U F XR (X, eta) = 4 * eta ∧ Pi F XR w.coefficients (X, eta) = F.axisDatum eta + 5 / 2 * F.data.core.P ^ 2 * OutgoingSchedule.shape eta ^ 2 * (X / XR) ^ (1 / 5)

Pressure regularity is proved using finite integrals with free bump coefficients, then composing with the constructed relative smooth branch.

noncomputable def NavierStokes.HeatedOutgoing.freeLogE (F : OutgoingProfile.Profile) (XR : ℝ) (z : (Coeff × ℝ) × ℝ) : ℝ

Free log E, constructed using extendedHeatE.

Equations

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

theorem NavierStokes.HeatedOutgoing.freeLogE_contDiff (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) : ContDiff ℝ (↑⊤) (freeLogE F XR)

theorem NavierStokes.HeatedOutgoing.freeLogE_eq (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (eta y : ℝ) (heta : eta ∈ parameterDomain) : freeLogE F XR ((c eta, eta), y) = E F XR c (Real.exp y, eta)

theorem NavierStokes.HeatedOutgoing.primitive_contDiff {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] (f : P × ℝ → ℝ) (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ ↑⊤ fun (z : P × ℝ) => ∫ (t : ℝ) in 0..z.2, f (z.1, t)

theorem NavierStokes.HeatedOutgoing.anchoredPrimitive_contDiff {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] (f : P × ℝ → ℝ) (hf : ContDiff ℝ (↑⊤) f) (a : ℝ) : ContDiff ℝ ↑⊤ fun (z : P × ℝ) => ∫ (t : ℝ) in a..z.2, f (z.1, t)

theorem NavierStokes.HeatedOutgoing.canonicalKernel_comp_exp (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (eta y : ℝ) : |Real.exp y| • canonicalKernel F XR c eta (Real.exp y) = E F XR c (Real.exp y, eta) ^ 2

theorem NavierStokes.HeatedOutgoing.Pi_exp (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (eta y : ℝ) : Pi F XR c (Real.exp y, eta) = -(1 / 2) * ∫ (t : ℝ) in Set.Ioi y, E F XR c (Real.exp t, eta) ^ 2

theorem NavierStokes.HeatedOutgoing.CompensationWitness.logE_square_integrable {F : OutgoingProfile.Profile} {XR C : ℝ} (w : CompensationWitness F XR C) (eta : ℝ) (heta : eta ∈ parameterDomain) : MeasureTheory.Integrable (fun (y : ℝ) => E F XR w.coefficients (Real.exp y, eta) ^ 2) MeasureTheory.volume

theorem NavierStokes.HeatedOutgoing.CompensationWitness.Pi_exp_primitive {F : OutgoingProfile.Profile} {XR C : ℝ} (w : CompensationWitness F XR C) (eta y : ℝ) (heta : eta ∈ parameterDomain) : Pi F XR w.coefficients (Real.exp y, eta) = OutgoingDilation.Pi F XR (OutgoingDilation.patchRadius F XR, eta) + 1 / 2 * ∫ (t : ℝ) in Real.log (OutgoingDilation.patchRadius F XR)..y, freeLogE F XR ((w.coefficients eta, eta), t) ^ 2

theorem NavierStokes.HeatedOutgoing.CompensationWitness.Pi_log_contDiffOn {F : OutgoingProfile.Profile} {XR C : ℝ} (w : CompensationWitness F XR C) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × ℝ) => Pi F XR w.coefficients (Real.exp p.1, p.2)) (Set.univ ×ˢ parameterDomain)

theorem NavierStokes.HeatedOutgoing.CompensationWitness.Pi_contDiffOn {F : OutgoingProfile.Profile} {XR C : ℝ} (w : CompensationWitness F XR C) : ContDiffOn ℝ (↑⊤) (Pi F XR w.coefficients) domain

theorem NavierStokes.HeatedOutgoing.E_between_patch_and_switch (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (eta X : ℝ) (hXR : 0 < XR) (hX : 0 < X) (hpatch : OutgoingDilation.patchRadius F XR * OutgoingDilation.compensationPatch.right ≤ X) (hswitch : X ≤ OutgoingDilation.switchRadius F XR) : E F XR c (X, eta) = OutgoingDilation.E F XR (X, eta)

theorem NavierStokes.HeatedOutgoing.full_switch_above_radius {K X : ℝ} (hK : 0 < K) (hX : 0 < X) (hfull : 1 / 2 ≤ Real.log (X / K) + 1 / 5) : K ≤ X

theorem NavierStokes.HeatedOutgoing.E_full_switch (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (eta X : ℝ) (hXR : 0 < XR) (hX : 0 < X) (hfull : 1 / 2 ≤ Real.log (X / OutgoingDilation.switchRadius F XR) + 1 / 5) : E F XR c (X, eta) = OutgoingDilation.carrierAmplitude F * OutgoingDilation.switchRadius F XR ^ HeatTailEdit.exponent F.data.h * RadialHeatProfile.spatialProfile (1 + F.data.h) (ParametricHeatTail.diffusion eta) X * OutgoingTail.tailShape F.data (Real.log (X / OutgoingDilation.switchRadius F XR) + 1 / 5)

theorem NavierStokes.HeatedOutgoing.E_eventual_heat (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (eta X : ℝ) (hXR : 0 < XR) (hX : 0 < X) (hlate : 3 ≤ Real.log (X / OutgoingDilation.switchRadius F XR) + 1 / 5) : E F XR c (X, eta) = OutgoingDilation.carrierAmplitude F * OutgoingDilation.switchRadius F XR ^ HeatTailEdit.exponent F.data.h * RadialHeatProfile.spatialProfile (1 + F.data.h) (ParametricHeatTail.diffusion eta) X

theorem NavierStokes.HeatedOutgoing.E_eventual_heat_carrier (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) {q s τ eta : ℝ} (hXR : 0 < XR) (hq : 0 < q) (hs : 0 < s) (hν : ParametricHeatTail.diffusion eta = τ / q) (hlate : 3 ≤ Real.log (s / q / OutgoingDilation.switchRadius F XR) + 1 / 5) : q ^ (-HeatTailEdit.exponent F.data.h) * E F XR c (s / q, eta) = OutgoingDilation.carrierAmplitude F * OutgoingDilation.switchRadius F XR ^ HeatTailEdit.exponent F.data.h * RadialHeatProfile.spatialProfile (1 + F.data.h) τ s

theorem NavierStokes.HeatedOutgoing.Pi_after_switch (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (eta X : ℝ) (hXR : 0 < XR) (hX : OutgoingDilation.switchRadius F XR ≤ X) : Pi F XR c (X, eta) = -(1 / 2) * ∫ (u : ℝ) in Set.Ioi X, ParametricHeatTail.physicalEdit F.data (OutgoingDilation.switchRadius F XR) eta u ^ 2 / u

theorem NavierStokes.HeatedOutgoing.CompensationWitness.Pi_tendsto_axis {F : OutgoingProfile.Profile} {XR C : ℝ} (w : CompensationWitness F XR C) (eta : ℝ) (heta : eta ∈ parameterDomain) : Filter.Tendsto (fun (X : ℝ) => Pi F XR w.coefficients (X, eta)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (F.axisDatum eta))

theorem NavierStokes.HeatedOutgoing.CompensationWitness.axisDatum_analytic_extension {F : OutgoingProfile.Profile} {XR C : ℝ} (w : CompensationWitness F XR C) : AnalyticOnNhd ℂ (SchedulePressure.complexAxisPressure F.data) PressureDatum.strip ∧ ∀ eta ∈ parameterDomain, SchedulePressure.complexAxisPressure F.data ↑eta = ↑(axisDatum F XR w.coefficients eta)

All properties below refer to the same actual fields and the same outgoing profile. The coefficient witness also retains its quantitative relative first-jet bounds.

structure NavierStokes.HeatedOutgoing.Specification (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) : Prop

Specification data, collecting angular_smooth, axial_smooth, momentum_smooth, pressure_smooth, angular_positive, axial_unchanged and their compatibility conditions.

• angular_smooth : ContDiffOn ℝ (↑⊤) (E F XR c) domain
• axial_smooth : ContDiffOn ℝ (↑⊤) (U F XR) domain
• momentum_smooth : ContDiffOn ℝ (↑⊤) (H F XR c) domain
• pressure_smooth : ContDiffOn ℝ (↑⊤) (Pi F XR c) domain
• angular_positive (eta : ℝ) : eta ∈ parameterDomain → ∀ (X : ℝ), 0 < X → 0 < E F XR c (X, eta)
• axial_unchanged : U F XR = OutgoingDilation.U F XR
• mass_unchanged (eta X : ℝ) : M F XR eta X = OutgoingDilation.M F XR eta X
• angular_unchanged (eta X : ℝ) : J F XR c eta X = OutgoingDilation.J F XR eta X
• mass_integrable (eta : ℝ) : MeasureTheory.IntegrableOn (fun (X : ℝ) => U F XR (X, eta)) (Set.Ioi 0) MeasureTheory.volume
• angular_integrable (eta : ℝ) : MeasureTheory.IntegrableOn (fun (X : ℝ) => H F XR c (X, eta) * U F XR (X, eta)) (Set.Ioi 0) MeasureTheory.volume
• mass_zero (eta : ℝ) : ∫ (X : ℝ) in Set.Ioi 0, U F XR (X, eta) = 0
• angular_zero (eta : ℝ) : ∫ (X : ℝ) in Set.Ioi 0, H F XR c (X, eta) * U F XR (X, eta) = 0
• after_pulse (eta X : ℝ) : 0 < X → OutgoingDilation.pulseEndRadius F XR ≤ X → U F XR (X, eta) = 0 ∧ M F XR eta X = 0 ∧ J F XR c eta X = 0
• energy_integrable (eta : ℝ) : eta ∈ parameterDomain → MeasureTheory.IntegrableOn (energyDensity F XR c eta) (Set.Ioi 0) MeasureTheory.volume
• energy_zero (eta : ℝ) : eta ∈ parameterDomain → totalS F XR c eta = 0
• renormalized_integrable (eta : ℝ) : eta ∈ parameterDomain → MeasureTheory.IntegrableOn (fun (X : ℝ) => H F XR c (X, eta) - OutgoingDilation.powerH F XR X) (Set.Ioi 0) MeasureTheory.volume
• renormalized_zero (eta : ℝ) : eta ∈ parameterDomain → ∫ (X : ℝ) in Set.Ioi 0, H F XR c (X, eta) - OutgoingDilation.powerH F XR X = 0
• pressure_integrable (eta : ℝ) : eta ∈ parameterDomain → MeasureTheory.IntegrableOn (canonicalKernel F XR c eta) (Set.Ioi 0) MeasureTheory.volume
• pressure_canonical (eta X : ℝ) : Pi F XR c (X, eta) = -(1 / 2) * ∫ (u : ℝ) in Set.Ioi X, E F XR c (u, eta) ^ 2 / u
• axis_unchanged (eta : ℝ) : eta ∈ parameterDomain → axisDatum F XR c eta = F.axisDatum eta
• axis_limit (eta : ℝ) : eta ∈ parameterDomain → Filter.Tendsto (fun (X : ℝ) => Pi F XR c (X, eta)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (F.axisDatum eta))
• analytic_axis_datum : AnalyticOnNhd ℂ (SchedulePressure.complexAxisPressure F.data) PressureDatum.strip ∧ ∀ eta ∈ parameterDomain, SchedulePressure.complexAxisPressure F.data ↑eta = ↑(axisDatum F XR c eta)
• before_patch (eta : ℝ) : eta ∈ parameterDomain → ∀ (X : ℝ), 0 < X → X ≤ OutgoingDilation.patchRadius F XR → E F XR c (X, eta) = OutgoingDilation.E F XR (X, eta) ∧ Pi F XR c (X, eta) = OutgoingDilation.Pi F XR (X, eta)
• ideal_prefix (eta : ℝ) : eta ∈ parameterDomain → ∀ (X : ℝ), 0 < X → X ≤ XR → E F XR c (X, eta) = F.data.core.P * OutgoingSchedule.shape eta * (X / XR) ^ (1 / 10) ∧ U F XR (X, eta) = 4 * eta ∧ Pi F XR c (X, eta) = F.axisDatum eta + 5 / 2 * F.data.core.P ^ 2 * OutgoingSchedule.shape eta ^ 2 * (X / XR) ^ (1 / 5)
• switch_overlap (eta X : ℝ) : OutgoingDilation.switchRadius F XR ≤ X → E F XR c (X, eta) = ParametricHeatTail.physicalEdit F.data (OutgoingDilation.switchRadius F XR) eta X
• terminal_heat (eta X : ℝ) : 0 < X → 3 ≤ Real.log (X / OutgoingDilation.switchRadius F XR) + 1 / 5 → E F XR c (X, eta) = OutgoingDilation.carrierAmplitude F * OutgoingDilation.switchRadius F XR ^ HeatTailEdit.exponent F.data.h * RadialHeatProfile.spatialProfile (1 + F.data.h) (ParametricHeatTail.diffusion eta) X
• patch_disjoint : Disjoint (Set.Icc (OutgoingDilation.patchRadius F XR) (OutgoingDilation.patchRadius F XR * OutgoingDilation.compensationPatch.right)) (Set.Ici (OutgoingDilation.switchRadius F XR))

theorem NavierStokes.HeatedOutgoing.CompensationWitness.specification {F : OutgoingProfile.Profile} {XR B C : ℝ} (w : CompensationWitness F XR C) (hF : OutgoingProfile.Specification F B) : Specification F XR w.coefficients

theorem NavierStokes.HeatedOutgoing.exists_heated_profile {F : OutgoingProfile.Profile} {B : ℝ} (hF : OutgoingProfile.Specification F B) : ∃ (XR₀ : ℝ) (C : ℝ), 0 < XR₀ ∧ 0 < C ∧ ∀ (XR : ℝ), XR₀ ≤ XR → ∃ (w : CompensationWitness F XR C), Specification F XR w.coefficients

For a single fixed outgoing profile, every sufficiently large entrance radius allows the actual physical heat continuation and its exact repair.

theorem NavierStokes.HeatedOutgoing.exists_fixed_schedule (P m : ℝ) (hP : 0 < P) (hm : 0 < m) : ∃ (lam : ℝ) (B : ℝ), 0 < lam ∧ 0 < B ∧ ∀ (h : ℝ), 0 < h → 2 * h < lam → ∃ (F : OutgoingProfile.Profile), F.data.core.P = P ∧ F.data.core.m = m ∧ F.data.core.lam = lam ∧ F.data.h = h ∧ OutgoingProfile.Specification F B ∧ ∃ (XR₀ : ℝ) (C : ℝ), 0 < XR₀ ∧ 0 < C ∧ ∀ (XR : ℝ), XR₀ ≤ XR → ∃ (w : CompensationWitness F XR C), Specification F XR w.coefficients

The order of choices is P,m, one positive lam, permitted h, one reset/amplitude profile, and then large X_R and its terminal coefficients.