An actual compensated outgoing profile on an open parameter neighborhood

The coefficients are solved once for the literal extended heat debts. Their restriction supplies the physical-band witness; no comparison of unrelated existential choices is used.

@[reducible, inline]

abbrev NavierStokes.ExtendedHeatedOutgoing.Coeff : Type

Coefficient: an abbreviation for TerminalCompensation.Coeff.

Equations

• NavierStokes.ExtendedHeatedOutgoing.Coeff = NavierStokes.TerminalCompensation.Coeff

def NavierStokes.ExtendedHeatedOutgoing.parameterDomain : Set ℝ

Parameter domain, given by Ioo (-(3 / 2 : ℝ)) (3 / 2).

Equations

• NavierStokes.ExtendedHeatedOutgoing.parameterDomain = Set.Ioo (-(3 / 2)) (3 / 2)

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

Domain, given by Ioi 0 ×ˢ parameterDomain.

Equations

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

theorem NavierStokes.ExtendedHeatedOutgoing.parameterDomain_open : IsOpen parameterDomain

theorem NavierStokes.ExtendedHeatedOutgoing.parameterDomain_subset : parameterDomain ⊆ ExtendedHeatDebts.enlargedBand

theorem NavierStokes.ExtendedHeatedOutgoing.physicalBand_subset : HeatedOutgoing.parameterDomain ⊆ parameterDomain

theorem NavierStokes.ExtendedHeatedOutgoing.enlargedBand_mem_nhds {eta : ℝ} (heta : eta ∈ parameterDomain) : ExtendedHeatDebts.enlargedBand ∈ nhds eta

noncomputable def NavierStokes.ExtendedHeatedOutgoing.heatE (F : OutgoingProfile.Profile) (XR : ℝ) : ℝ × ℝ → ℝ

Heat E, given by HeatedOutgoing.extendedHeatE F XR.

Equations

• NavierStokes.ExtendedHeatedOutgoing.heatE F XR = NavierStokes.HeatedOutgoing.extendedHeatE F XR

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

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

Equations

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

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

U, given by HeatedOutgoing.U F XR.

Equations

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

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

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

Equations

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

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

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

Equations

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

noncomputable def NavierStokes.ExtendedHeatedOutgoing.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.ExtendedHeatedOutgoing.Pi F XR c p = -(1 / 2) * ∫ (X : ℝ) in Set.Ioi p.1, NavierStokes.ExtendedHeatedOutgoing.canonicalKernel F XR c p.2 X

noncomputable def NavierStokes.ExtendedHeatedOutgoing.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.ExtendedHeatedOutgoing.axisDatum F XR c eta = -(1 / 2) * ∫ (X : ℝ) in Set.Ioi 0, NavierStokes.ExtendedHeatedOutgoing.canonicalKernel F XR c eta X

noncomputable def NavierStokes.ExtendedHeatedOutgoing.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.ExtendedHeatedOutgoing.energyDensity F XR c eta X = NavierStokes.ExtendedHeatedOutgoing.U F XR (X, eta) ^ 2 - NavierStokes.ExtendedHeatedOutgoing.E F XR c (X, eta) ^ 2 / 2

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

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

Equations

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

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

M, given by HeatedOutgoing.M F XR eta X.

Equations

• NavierStokes.ExtendedHeatedOutgoing.M F XR eta X = NavierStokes.HeatedOutgoing.M F XR eta X

noncomputable def NavierStokes.ExtendedHeatedOutgoing.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.ExtendedHeatedOutgoing.J F XR c eta X = ∫ (u : ℝ) in Set.Ioc 0 X, NavierStokes.ExtendedHeatedOutgoing.H F XR c (u, eta) * NavierStokes.ExtendedHeatedOutgoing.U F XR (u, eta)

structure NavierStokes.ExtendedHeatedOutgoing.Witness (F : OutgoingProfile.Profile) (XR C : ℝ) : Type

Quantitative data from one solve on the enlarged compact parameter set.

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

  Coefficients of Witness, of type ℝ → Coeff.

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

theorem NavierStokes.ExtendedHeatedOutgoing.exists_witness (F : OutgoingProfile.Profile) : ∃ (XR₀ : ℝ) (C : ℝ), 0 < XR₀ ∧ 0 < C ∧ ∀ (XR : ℝ), XR₀ ≤ XR → Nonempty (Witness F XR C)

theorem NavierStokes.ExtendedHeatedOutgoing.Witness.coefficients_contDiffOn {F : OutgoingProfile.Profile} {XR C : ℝ} (w : Witness F XR C) : ContDiffOn ℝ (↑⊤) w.coefficients parameterDomain

theorem NavierStokes.ExtendedHeatedOutgoing.Witness.coefficients_contDiffAt {F : OutgoingProfile.Profile} {XR C : ℝ} (w : Witness F XR C) {eta : ℝ} (heta : eta ∈ parameterDomain) : ContDiffAt ℝ (↑⊤) w.coefficients eta

theorem NavierStokes.ExtendedHeatedOutgoing.Witness.derivative_bound_open {F : OutgoingProfile.Profile} {XR C : ℝ} (w : Witness F XR C) {eta : ℝ} (heta : eta ∈ parameterDomain) : ‖deriv w.coefficients eta‖ ≤ C / OutgoingDilation.switchRadius F XR

theorem NavierStokes.ExtendedHeatedOutgoing.Witness.parameter_correction_contDiffOn {F : OutgoingProfile.Profile} {XR C : ℝ} (w : Witness F XR C) (x : ℝ) : ContDiffOn ℝ (↑⊤) (fun (eta : ℝ) => OutgoingDilation.shapedPatchAmplitude F eta * TerminalCompensation.correction OutgoingDilation.compensationPatch (w.coefficients eta) x) ExtendedHeatDebts.enlargedBand

noncomputable def NavierStokes.ExtendedHeatedOutgoing.Witness.physical {F : OutgoingProfile.Profile} {XR C : ℝ} (w : Witness F XR C) : HeatedOutgoing.CompensationWitness F XR C

Restriction of the constructed branch, rather than a new existential solve.

Equations

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

@[simp]

theorem NavierStokes.ExtendedHeatedOutgoing.Witness.physical_coefficients {F : OutgoingProfile.Profile} {XR C : ℝ} (w : Witness F XR C) : w.physical.coefficients = w.coefficients

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

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

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

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

theorem NavierStokes.ExtendedHeatedOutgoing.E_eq_physical (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (eta X : ℝ) (heta : eta ∈ HeatedOutgoing.parameterDomain) (hX : 0 < X) : E F XR c (X, eta) = HeatedOutgoing.E F XR c (X, eta)

theorem NavierStokes.ExtendedHeatedOutgoing.H_eq_physical (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (eta X : ℝ) (heta : eta ∈ HeatedOutgoing.parameterDomain) (hX : 0 < X) : H F XR c (X, eta) = HeatedOutgoing.H F XR c (X, eta)

theorem NavierStokes.ExtendedHeatedOutgoing.Pi_eq_physical (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (eta X : ℝ) (heta : eta ∈ HeatedOutgoing.parameterDomain) (hX : 0 ≤ X) : Pi F XR c (X, eta) = HeatedOutgoing.Pi F XR c (X, eta)

theorem NavierStokes.ExtendedHeatedOutgoing.heatE_eq_edit (F : OutgoingProfile.Profile) (XR eta X : ℝ) : heatE F XR (X, eta) = ExtendedHeatDebts.edit (fun (u : ℝ) => OutgoingDilation.E F XR (u, eta)) F.data.h (ParametricHeatTail.diffusion eta) (OutgoingDilation.switchRadius F XR) X

theorem NavierStokes.ExtendedHeatedOutgoing.edit_before (f : ℝ → ℝ) (h nu : ℝ) {K X : ℝ} (hK : 0 < K) (hX : 0 < X) (hle : X ≤ K) : ExtendedHeatDebts.edit f h nu K X = f X

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

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

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

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

theorem NavierStokes.ExtendedHeatedOutgoing.E_on_patch (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (eta X : ℝ) (hXR : 0 < XR) (hX : 0 < X) (hp : 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

noncomputable def NavierStokes.ExtendedHeatedOutgoing.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.ExtendedHeatedOutgoing.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.ExtendedHeatedOutgoing.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) = ExtendedHeatDebts.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 = ExtendedHeatDebts.squareChange (HeatTailEdit.outgoingProfile F.data (OutgoingDilation.switchRadius F XR) eta) F.data.h (ParametricHeatTail.diffusion eta) (OutgoingDilation.switchRadius F XR) X

theorem NavierStokes.ExtendedHeatedOutgoing.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 = HeatedOutgoing.patchRow F XR c eta 1 X

theorem NavierStokes.ExtendedHeatedOutgoing.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 + HeatedOutgoing.patchRow F XR c eta i X

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

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

theorem NavierStokes.ExtendedHeatedOutgoing.Witness.heatRow_integrable {F : OutgoingProfile.Profile} {XR C : ℝ} (w : Witness F XR C) (eta : ℝ) (i : Fin 3) : MeasureTheory.IntegrableOn (heatRow F XR eta i) (Set.Ioi 0) MeasureTheory.volume

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

theorem NavierStokes.ExtendedHeatedOutgoing.Witness.changeRow_integral_zero {F : OutgoingProfile.Profile} {XR C : ℝ} (w : Witness 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.ExtendedHeatedOutgoing.Witness.positive {F : OutgoingProfile.Profile} {XR C : ℝ} (w : Witness F XR C) (eta X : ℝ) (heta : eta ∈ parameterDomain) (hX : 0 < X) : 0 < E F XR w.coefficients (X, eta)

theorem NavierStokes.ExtendedHeatedOutgoing.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.ExtendedHeatedOutgoing.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.ExtendedHeatedOutgoing.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.ExtendedHeatedOutgoing.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.ExtendedHeatedOutgoing.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.ExtendedHeatedOutgoing.M_unchanged (F : OutgoingProfile.Profile) (XR eta X : ℝ) : M F XR eta X = OutgoingDilation.M F XR eta X

theorem NavierStokes.ExtendedHeatedOutgoing.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.ExtendedHeatedOutgoing.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.ExtendedHeatedOutgoing.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.ExtendedHeatedOutgoing.freeLogE_eq (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (eta y : ℝ) : HeatedOutgoing.freeLogE F XR ((c eta, eta), y) = E F XR c (Real.exp y, eta)

theorem NavierStokes.ExtendedHeatedOutgoing.Witness.canonicalKernel_integrable {F : OutgoingProfile.Profile} {XR C : ℝ} (w : Witness F XR C) (eta : ℝ) : MeasureTheory.IntegrableOn (canonicalKernel F XR w.coefficients eta) (Set.Ioi 0) MeasureTheory.volume

theorem NavierStokes.ExtendedHeatedOutgoing.Witness.pressure_integral_unchanged {F : OutgoingProfile.Profile} {XR C : ℝ} (w : Witness 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.ExtendedHeatedOutgoing.Witness.axisDatum_eq {F : OutgoingProfile.Profile} {XR C : ℝ} (w : Witness F XR C) (eta : ℝ) (heta : eta ∈ parameterDomain) : axisDatum F XR w.coefficients eta = F.axisDatum eta

theorem NavierStokes.ExtendedHeatedOutgoing.Witness.energy_integrable {F : OutgoingProfile.Profile} {XR C : ℝ} (w : Witness F XR C) (eta : ℝ) : MeasureTheory.IntegrableOn (energyDensity F XR w.coefficients eta) (Set.Ioi 0) MeasureTheory.volume

theorem NavierStokes.ExtendedHeatedOutgoing.Witness.totalS_eq {F : OutgoingProfile.Profile} {XR C : ℝ} (w : Witness F XR C) (eta : ℝ) (heta : eta ∈ parameterDomain) : totalS F XR w.coefficients eta = OutgoingDilation.totalS F XR eta

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

theorem NavierStokes.ExtendedHeatedOutgoing.Witness.renormalized_zero {F : OutgoingProfile.Profile} {XR C : ℝ} (w : Witness 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.ExtendedHeatedOutgoing.Witness.mass_integrable {F : OutgoingProfile.Profile} {XR C : ℝ} (w : Witness F XR C) (eta : ℝ) : MeasureTheory.IntegrableOn (fun (X : ℝ) => U F XR (X, eta)) (Set.Ioi 0) MeasureTheory.volume

theorem NavierStokes.ExtendedHeatedOutgoing.Witness.angular_integrable {F : OutgoingProfile.Profile} {XR C : ℝ} (w : Witness 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.ExtendedHeatedOutgoing.Witness.mass_zero {F : OutgoingProfile.Profile} {XR C : ℝ} (w : Witness F XR C) (eta : ℝ) : ∫ (X : ℝ) in Set.Ioi 0, U F XR (X, eta) = 0

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

theorem NavierStokes.ExtendedHeatedOutgoing.Witness.after_pulse {F : OutgoingProfile.Profile} {XR C : ℝ} (w : Witness 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.ExtendedHeatedOutgoing.Witness.Pi_before_patch {F : OutgoingProfile.Profile} {XR C : ℝ} (w : Witness 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.ExtendedHeatedOutgoing.Witness.ideal_prefix {F : OutgoingProfile.Profile} {XR C : ℝ} (w : Witness 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)

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

theorem NavierStokes.ExtendedHeatedOutgoing.Witness.Pi_exp_primitive {F : OutgoingProfile.Profile} {XR C : ℝ} (w : Witness 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, HeatedOutgoing.freeLogE F XR ((w.coefficients eta, eta), t) ^ 2

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

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

theorem NavierStokes.ExtendedHeatedOutgoing.Witness.fields_contDiffAt {F : OutgoingProfile.Profile} {XR C : ℝ} (w : Witness F XR C) {p : ℝ × ℝ} (hp : p ∈ domain) : ContDiffAt ℝ (↑⊤) (E F XR w.coefficients) p ∧ ContDiffAt ℝ (↑⊤) (U F XR) p ∧ ContDiffAt ℝ (↑⊤) (H F XR w.coefficients) p ∧ ContDiffAt ℝ (↑⊤) (Pi F XR w.coefficients) p

theorem NavierStokes.ExtendedHeatedOutgoing.Witness.Pi_tendsto_axis {F : OutgoingProfile.Profile} {XR C : ℝ} (w : Witness 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))

The original amplitude is a globally smooth clamped formula. Its actual energy equation holds on this explicit open set. The schedule bounds below place the entire physical band strictly inside that set.

noncomputable def NavierStokes.ExtendedHeatedOutgoing.energyDomain (F : OutgoingProfile.Profile) : Set ℝ

Energy domain, given by parameterDomain ∩ {eta | CorrectedPulseAmplitude.constantTerm F.data F.reset.coefficients eta < -(1 / 5)}.

Equations

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

theorem NavierStokes.ExtendedHeatedOutgoing.energyDomain_open (F : OutgoingProfile.Profile) : IsOpen (energyDomain F)

structure NavierStokes.ExtendedHeatedOutgoing.ScheduleBounds (F : OutgoingProfile.Profile) : Prop

Schedule bounds data, collecting coefficient_pos, lambda_small, wait_eq, scale_small.

• coefficient_pos : 0 < F.coefficientBound
• lambda_small : F.data.core.lam ≤ 1 / 120
• wait_eq : F.data.core.wait = 60 * Real.log (1 / F.data.core.lam)
• scale_small : CorrectedPulseAmplitude.combinedScale F.data F.coefficientBound ≤ 1 / 1000

theorem NavierStokes.ExtendedHeatedOutgoing.ScheduleBounds.constantTerm_bound {F : OutgoingProfile.Profile} (b : ScheduleBounds F) {eta : ℝ} (heta : eta ∈ HeatedOutgoing.parameterDomain) : CorrectedPulseAmplitude.constantTerm F.data F.reset.coefficients eta ≤ -(23 / 100)

theorem NavierStokes.ExtendedHeatedOutgoing.ScheduleBounds.physicalBand_subset {F : OutgoingProfile.Profile} (b : ScheduleBounds F) : HeatedOutgoing.parameterDomain ⊆ energyDomain F

noncomputable def NavierStokes.ExtendedHeatedOutgoing.amplitudeBound (F : OutgoingProfile.Profile) : ℝ

Amplitude bound, given by 128 * CorrectedPulseAmplitude.combinedConstant F.data.core.P F.data.core.m F.coefficientBound.

Equations

• NavierStokes.ExtendedHeatedOutgoing.amplitudeBound F = 128 * NavierStokes.CorrectedPulseAmplitude.combinedConstant F.data.core.P F.data.core.m F.coefficientBound

theorem NavierStokes.ExtendedHeatedOutgoing.ScheduleBounds.amplitudeBound_pos {F : OutgoingProfile.Profile} (b : ScheduleBounds F) : 0 < amplitudeBound F

theorem NavierStokes.ExtendedHeatedOutgoing.ScheduleBounds.specification {F : OutgoingProfile.Profile} (b : ScheduleBounds F) : OutgoingProfile.Specification F (amplitudeBound F)

The same reset and amplitude provide the original full specification, with the stronger quantitative data retained for the open extension.

theorem NavierStokes.ExtendedHeatedOutgoing.base_energy_zero (F : OutgoingProfile.Profile) (XR eta : ℝ) (hXR : 0 < XR) (heta : eta ∈ energyDomain F) : OutgoingDilation.totalS F XR eta = 0

theorem NavierStokes.ExtendedHeatedOutgoing.Witness.energy_zero {F : OutgoingProfile.Profile} {XR C : ℝ} (w : Witness F XR C) (eta : ℝ) (heta : eta ∈ energyDomain F) : totalS F XR w.coefficients eta = 0

theorem NavierStokes.ExtendedHeatedOutgoing.exists_scheduled_profile (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 ∧ ScheduleBounds F ∧ OutgoingProfile.Specification F B

The quantitative schedule is chosen directly with one actual reset. The amplitude attached to the resulting Profile is unchanged thereafter.

theorem NavierStokes.ExtendedHeatedOutgoing.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 * X ^ (-HeatTailEdit.exponent F.data.h) * HeatProfileExtension.physicalProfile (1 + F.data.h) X eta * OutgoingTail.tailShape F.data (Real.log (X / OutgoingDilation.switchRadius F XR) + 1 / 5)

theorem NavierStokes.ExtendedHeatedOutgoing.E_eventual_extended_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 * X ^ (-HeatTailEdit.exponent F.data.h) * HeatProfileExtension.physicalProfile (1 + F.data.h) X eta

theorem NavierStokes.ExtendedHeatedOutgoing.E_eventual_heat (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (eta X : ℝ) (hXR : 0 < XR) (hX : 0 < X) (heta : eta ∈ HeatedOutgoing.parameterDomain) (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.ExtendedHeatedOutgoing.E_between_patch_and_switch (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (eta X : ℝ) (hXR : 0 < XR) (hX : 0 < X) (hp : OutgoingDilation.patchRadius F XR * OutgoingDilation.compensationPatch.right ≤ X) (hK : X ≤ OutgoingDilation.switchRadius F XR) : E F XR c (X, eta) = OutgoingDilation.E F XR (X, eta)

theorem NavierStokes.ExtendedHeatedOutgoing.exists_symmetric_neighborhood {V : Set ℝ} (hV : IsOpen V) (hband : HeatedOutgoing.parameterDomain ⊆ V) : ∃ (a : ℝ), 1 < a ∧ a < 3 / 2 ∧ Set.Ioo (-a) a ⊆ V

theorem NavierStokes.ExtendedHeatedOutgoing.ScheduleBounds.exists_parameter_interval {F : OutgoingProfile.Profile} (b : ScheduleBounds F) : ∃ (a : ℝ), 1 < a ∧ a < 3 / 2 ∧ Set.Ioo (-a) a ⊆ energyDomain F

theorem NavierStokes.ExtendedHeatedOutgoing.Witness.first_jet_open {F : OutgoingProfile.Profile} {XR C : ℝ} (w : Witness F XR C) {eta : ℝ} (heta : eta ∈ parameterDomain) : TerminalCompensation.FirstJetBound OutgoingDilation.compensationPatch (OutgoingDilation.shapedPatchAmplitude F) w.coefficients eta (C / OutgoingDilation.switchRadius F XR)

theorem NavierStokes.ExtendedHeatedOutgoing.Witness.physical_specification {F : OutgoingProfile.Profile} {XR C : ℝ} (w : Witness F XR C) (b : ScheduleBounds F) : HeatedOutgoing.Specification F XR w.physical.coefficients

theorem NavierStokes.ExtendedHeatedOutgoing.Witness.fields_eq_physical {F : OutgoingProfile.Profile} {XR C : ℝ} (w : Witness F XR C) (eta X : ℝ) (heta : eta ∈ HeatedOutgoing.parameterDomain) (hX : 0 < X) : E F XR w.coefficients (X, eta) = HeatedOutgoing.E F XR w.physical.coefficients (X, eta) ∧ U F XR (X, eta) = HeatedOutgoing.U F XR (X, eta) ∧ H F XR w.coefficients (X, eta) = HeatedOutgoing.H F XR w.physical.coefficients (X, eta) ∧ Pi F XR w.coefficients (X, eta) = HeatedOutgoing.Pi F XR w.physical.coefficients (X, eta)

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

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

The complete open-neighborhood specification. All functions are the literal extended fields of the same chosen outgoing profile.

• neighborhood_open : IsOpen (energyDomain F)
• neighborhood_contains : HeatedOutgoing.parameterDomain ⊆ energyDomain F
• fields_smooth (p : ℝ × ℝ) : p ∈ Set.Ioi 0 ×ˢ energyDomain F → ContDiffAt ℝ (↑⊤) (E F XR c) p ∧ ContDiffAt ℝ (↑⊤) (U F XR) p ∧ ContDiffAt ℝ (↑⊤) (H F XR c) p ∧ ContDiffAt ℝ (↑⊤) (Pi F XR c) p
• angular_positive (eta : ℝ) : eta ∈ energyDomain F → ∀ (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
• energy_integrable (eta : ℝ) : MeasureTheory.IntegrableOn (energyDensity F XR c eta) (Set.Ioi 0) MeasureTheory.volume
• pressure_integrable (eta : ℝ) : MeasureTheory.IntegrableOn (canonicalKernel F XR c eta) (Set.Ioi 0) MeasureTheory.volume
• renormalized_integrable (eta : ℝ) : MeasureTheory.IntegrableOn (fun (X : ℝ) => H F XR c (X, eta) - OutgoingDilation.powerH F XR X) (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
• energy_zero (eta : ℝ) : eta ∈ energyDomain F → totalS F XR c eta = 0
• renormalized_zero (eta : ℝ) : eta ∈ energyDomain F → ∫ (X : ℝ) in Set.Ioi 0, H F XR c (X, eta) - OutgoingDilation.powerH F XR X = 0
• 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 ∈ energyDomain F → axisDatum F XR c eta = F.axisDatum eta
• axis_limit (eta : ℝ) : eta ∈ energyDomain F → 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 ∈ energyDomain F, SchedulePressure.complexAxisPressure F.data ↑eta = ↑(axisDatum F XR c eta)
• 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
• before_patch (eta : ℝ) : eta ∈ energyDomain F → ∀ (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 ∈ energyDomain F → ∀ (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)
• terminal_extended_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 * X ^ (-HeatTailEdit.exponent F.data.h) * HeatProfileExtension.physicalProfile (1 + F.data.h) X eta
• physical_specification : HeatedOutgoing.Specification F XR c

theorem NavierStokes.ExtendedHeatedOutgoing.Witness.specification {F : OutgoingProfile.Profile} {XR C : ℝ} (w : Witness F XR C) (b : ScheduleBounds F) : Specification F XR w.coefficients

theorem NavierStokes.ExtendedHeatedOutgoing.exists_open_profile {F : OutgoingProfile.Profile} (b : ScheduleBounds F) : ∃ (XR₀ : ℝ) (C : ℝ), 0 < XR₀ ∧ 0 < C ∧ ∀ (XR : ℝ), XR₀ ≤ XR → ∃ (w : Witness F XR C), Specification F XR w.coefficients

theorem NavierStokes.ExtendedHeatedOutgoing.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 ∧ ScheduleBounds F ∧ OutgoingProfile.Specification F B ∧ ∃ (a : ℝ), 1 < a ∧ a < 3 / 2 ∧ Set.Ioo (-a) a ⊆ energyDomain F ∧ ∃ (XR₀ : ℝ) (C : ℝ), 0 < XR₀ ∧ 0 < C ∧ ∀ (XR : ℝ), XR₀ ≤ XR → ∃ (w : Witness F XR C), Specification F XR w.coefficients

One schedule and one reset/amplitude pair yield an open parameter interval and the actual compensated profile at every sufficiently large entrance radius. The physical witness is the constructed restriction.