A single outgoing profile before the heat-tail edit #

The profile stores one actual scheduled angular-reset witness. Its axial amplitude is the corrected energy root associated with that same witness. All histories and pressures below are integrals of these fields.

source

structure NavierStokes.OutgoingProfile.Profile :

Type

One reset, used by both the angular profile and the energy root.

data : OutgoingTail.TailData
Data of Profile, of type TailData.
coefficientBound : ℝ
Coefficient bound of Profile, of type ℝ.
reset : UniformAngularReset.ResetWitness self.data self.coefficientBound
Reset of Profile, of type ResetWitness data coefficientBound.

Instances For

source

noncomputable def NavierStokes.OutgoingProfile.Profile.amp (F : Profile) :

ℝ → ℝ

Amp, given by CorrectedPulseAmplitude.amplitude F.data F.reset.coefficients.

Equations

F.amp = NavierStokes.CorrectedPulseAmplitude.amplitude F.data F.reset.coefficients

Instances For

source

noncomputable def NavierStokes.OutgoingProfile.Profile.logE (F : Profile) :

ℝ × ℝ → ℝ

Log E, given by correctedAngular F.data F.reset.coefficients.

Equations

F.logE = NavierStokes.UniformAngularReset.correctedAngular F.data F.reset.coefficients

Instances For

source

noncomputable def NavierStokes.OutgoingProfile.Profile.logU (F : Profile) :

ℝ × ℝ → ℝ

Log U, given by axial F.data.core F.amp.

Equations

F.logU = NavierStokes.OutgoingSchedule.axial F.data.core F.amp

Instances For

source

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

ℝ

E, given by F.logE (Real.log p.1, p.2).

Equations

F.E p = F.logE (Real.log p.1, p.2)

Instances For

source

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

ℝ

U, given by F.logU (Real.log p.1, p.2).

Equations

F.U p = F.logU (Real.log p.1, p.2)

Instances For

source

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

ℝ

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

Equations

F.H p = √(2 * p.1) * F.E p

Instances For

source

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

ℝ

Power E, given by powerConstant F.data * X ^ (-(1 / 2 + F.data.h)).

Equations

F.powerE X = NavierStokes.OutgoingTail.powerConstant F.data * X ^ (-(1 / 2 + F.data.h))

Instances For

source

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

ℝ

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

Equations

F.powerH X = √(2 * X) * F.powerE X

Instances For

source

noncomputable def NavierStokes.OutgoingProfile.Profile.massWeight (F : Profile) (eta y : ℝ) :

ℝ

Mass weight, given by Real.exp y * F.logU (y, eta).

Equations

F.massWeight eta y = Real.exp y * F.logU (y, eta)

Instances For

source

noncomputable def NavierStokes.OutgoingProfile.Profile.angularWeight (F : Profile) (eta y : ℝ) :

ℝ

Angular weight, given by Real.sqrt 2 * Real.exp (3 * y / 2) * F.logE (y, eta) * F.logU (y, eta).

Equations

F.angularWeight eta y = √2 * Real.exp (3 * y / 2) * F.logE (y, eta) * F.logU (y, eta)

Instances For

source

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

ℝ

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

Equations

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

Instances For

source

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

ℝ

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

Equations

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

Instances For

source

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

ℝ

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

Equations

F.energyDensity eta X = F.U (X, eta) ^ 2 - F.E (X, eta) ^ 2 / 2

Instances For

source

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

ℝ

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

Equations

F.totalS eta = ∫ (X : ℝ) in Set.Ioi 0, F.energyDensity eta X

Instances For

source

noncomputable def NavierStokes.OutgoingProfile.Profile.pressureWeight (F : Profile) (eta y : ℝ) :

ℝ

Pressure weight, given by F.logE (y, eta) ^ 2.

Equations

F.pressureWeight eta y = F.logE (y, eta) ^ 2

Instances For

source

noncomputable def NavierStokes.OutgoingProfile.Profile.logPi (F : Profile) (p : ℝ × ℝ) :

ℝ

Log pi, given by -(1 / 2 : ℝ) * ∫ y in Ioi p.1, F.pressureWeight p.2 y.

Equations

F.logPi p = -(1 / 2) * ∫ (y : ℝ) in Set.Ioi p.1, F.pressureWeight p.2 y

Instances For

source

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

ℝ

Pi, given by F.logPi (Real.log p.1, p.2).

Equations

F.Pi p = F.logPi (Real.log p.1, p.2)

Instances For

source

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

ℝ

Axis datum, given by -(1 / 2 : ℝ) * ∫ y, F.pressureWeight eta y.

Equations

F.axisDatum eta = -(1 / 2) * ∫ (y : ℝ), F.pressureWeight eta y

Instances For

source

noncomputable def NavierStokes.OutgoingProfile.Profile.pressureChange (F : Profile) (eta y : ℝ) :

ℝ

Pressure change, given by F.pressureWeight eta y - finalAngular F.data (y, eta) ^ 2.

Equations

F.pressureChange eta y = F.pressureWeight eta y - NavierStokes.OutgoingTail.finalAngular F.data (y, eta) ^ 2

Instances For

source

theorem NavierStokes.OutgoingProfile.Profile.amp_contDiff (F : Profile) :

ContDiff ℝ (↑⊤) F.amp

source

theorem NavierStokes.OutgoingProfile.Profile.logE_contDiff (F : Profile) :

ContDiff ℝ (↑⊤) F.logE

source

theorem NavierStokes.OutgoingProfile.Profile.logU_contDiff (F : Profile) :

ContDiff ℝ (↑⊤) F.logU

source

theorem NavierStokes.OutgoingProfile.Profile.E_pos (F : Profile) (p : ℝ × ℝ) :

0 < F.E p

source

theorem NavierStokes.OutgoingProfile.Profile.logE_before (F : Profile) (eta : ℝ) {y : ℝ} (hy : y ≤ F.data.core.endpoint) :

F.logE (y, eta) = OutgoingSchedule.angular F.data.core.P F.data.core.dropLength F.data.core.lam (y, eta)

source

theorem NavierStokes.OutgoingProfile.Profile.logE_ideal (F : Profile) (eta : ℝ) {y : ℝ} (hy : y ≤ 0) :

F.logE (y, eta) = F.data.core.P * OutgoingSchedule.shape eta * Real.exp (y / 10)

source

theorem NavierStokes.OutgoingProfile.Profile.logU_ideal (F : Profile) (eta : ℝ) {y : ℝ} (hy : y ≤ 0) :

F.logU (y, eta) = 4 * eta

source

theorem NavierStokes.OutgoingProfile.Profile.logU_after (F : Profile) (eta : ℝ) {y : ℝ} (hy : F.data.core.endpoint ≤ y) :

F.logU (y, eta) = 0

source

theorem NavierStokes.OutgoingProfile.Profile.angular_product_unchanged (F : Profile) (eta y : ℝ) :

F.logE (y, eta) * F.logU (y, eta) = OutgoingSchedule.angular F.data.core.P F.data.core.dropLength F.data.core.lam (y, eta) * F.logU (y, eta)

source

theorem NavierStokes.OutgoingProfile.Profile.logE_eventual (F : Profile) (eta : ℝ) {y : ℝ} (hy : OutgoingTail.tailEnd F.data ≤ y) :

F.logE (y, eta) = OutgoingTail.powerConstant F.data * Real.exp (-(1 / 2 + F.data.h) * y)

source

theorem NavierStokes.OutgoingProfile.Profile.E_ideal (F : Profile) (eta : ℝ) {X : ℝ} (hX : 0 < X) (hX' : X ≤ 1) :

F.E (X, eta) = F.data.core.P * OutgoingSchedule.shape eta * X ^ (1 / 10)

source

theorem NavierStokes.OutgoingProfile.Profile.U_ideal (F : Profile) (eta : ℝ) {X : ℝ} (hX : 0 < X) (hX' : X ≤ 1) :

F.U (X, eta) = 4 * eta

source

theorem NavierStokes.OutgoingProfile.Profile.E_eventual (F : Profile) (eta : ℝ) {X : ℝ} (hX : 0 < X) (hfar : OutgoingTail.tailEnd F.data ≤ Real.log X) :

F.E (X, eta) = F.powerE X

source

theorem NavierStokes.OutgoingProfile.Profile.U_after (F : Profile) (eta : ℝ) {X : ℝ} (hfar : F.data.core.endpoint ≤ Real.log X) :

F.U (X, eta) = 0

source

def NavierStokes.OutgoingProfile.domain :

Set (ℝ × ℝ)

Domain, given by Ioi 0 ×ˢ univ.

Equations

NavierStokes.OutgoingProfile.domain = Set.Ioi 0 ×ˢ Set.univ

Instances For

source

theorem NavierStokes.OutgoingProfile.logarithmic_coordinates_contDiffOn :

ContDiffOn ℝ (↑⊤) (fun (p : ℝ × ℝ) => (Real.log p.1, p.2)) domain

source

theorem NavierStokes.OutgoingProfile.Profile.E_contDiffOn (F : Profile) :

ContDiffOn ℝ (↑⊤) F.E domain

source

theorem NavierStokes.OutgoingProfile.Profile.U_contDiffOn (F : Profile) :

ContDiffOn ℝ (↑⊤) F.U domain

source

theorem NavierStokes.OutgoingProfile.Profile.H_contDiffOn (F : Profile) :

ContDiffOn ℝ (↑⊤) F.H domain

source

theorem NavierStokes.OutgoingProfile.Profile.pressureChange_zero (F : Profile) (eta : ℝ) {y : ℝ} (hy : y ∉ Set.Ioo (F.data.releaseStart - 4) F.data.releaseStart) :

F.pressureChange eta y = 0

source

theorem NavierStokes.OutgoingProfile.Profile.pressureChange_integrable (F : Profile) (eta : ℝ) :

MeasureTheory.Integrable (F.pressureChange eta) MeasureTheory.volume

source

theorem NavierStokes.OutgoingProfile.Profile.pressureWeight_integrable (F : Profile) (eta : ℝ) :

MeasureTheory.Integrable (F.pressureWeight eta) MeasureTheory.volume

source

theorem NavierStokes.OutgoingProfile.Profile.pressureWeight_integral (F : Profile) (eta : ℝ) :

∫ (y : ℝ), F.pressureWeight eta y = ∫ (y : ℝ), OutgoingTail.finalAngular F.data (y, eta) ^ 2

source

theorem NavierStokes.OutgoingProfile.Profile.axisDatum_eq (F : Profile) :

F.axisDatum = SchedulePressure.axisPressure F.data

source

theorem NavierStokes.OutgoingProfile.Profile.axisDatum_contDiff (F : Profile) :

ContDiff ℝ (↑⊤) F.axisDatum

source

theorem NavierStokes.OutgoingProfile.Profile.axisDatum_analytic_extension (F : Profile) :

AnalyticOnNhd ℂ (SchedulePressure.complexAxisPressure F.data) PressureDatum.strip ∧ ∀ (eta : ℝ), SchedulePressure.complexAxisPressure F.data ↑eta = ↑(F.axisDatum eta)

source

theorem NavierStokes.OutgoingProfile.Profile.natural_axis_pressureData (F : Profile) (hP : 2 ≤ F.data.core.P) :

NaturalAxisData.PressureData F.axisDatum

source

theorem NavierStokes.OutgoingProfile.exponential_prefix_integral (f : ℝ → ℝ) (hf : Continuous f) (a b : ℝ) (hb : 0 < b) (he : ∀ y ≤ 0, f y = a * Real.exp (b * y)) {y : ℝ} (hy : 0 ≤ y) :

MeasureTheory.IntegrableOn f (Set.Iic y) MeasureTheory.volume ∧ ∫ (t : ℝ) in Set.Iic y, f t = a / b + ∫ (t : ℝ) in 0..y, f t

Actual incoming exponential tails, integrated through any nonnegative clock time. No finite-prefix constant is an additional assumption.

source

theorem NavierStokes.OutgoingProfile.primitive_joint_contDiff (f : ℝ × ℝ → ℝ) (hf : ContDiff ℝ (↑⊤) f) :

ContDiff ℝ ↑⊤ fun (p : ℝ × ℝ) => ∫ (t : ℝ) in 0..p.1, f (t, p.2)

Compact parameter integration supplies joint smoothness of the actual variable-endpoint primitive.

source

theorem NavierStokes.OutgoingProfile.Profile.massWeight_continuous (F : Profile) (eta : ℝ) :

Continuous (F.massWeight eta)

source

theorem NavierStokes.OutgoingProfile.Profile.angularWeight_continuous (F : Profile) (eta : ℝ) :

Continuous (F.angularWeight eta)

source

theorem NavierStokes.OutgoingProfile.Profile.massWeight_ideal (F : Profile) (eta : ℝ) {y : ℝ} (hy : y ≤ 0) :

F.massWeight eta y = 4 * eta * Real.exp (1 * y)

source

theorem NavierStokes.OutgoingProfile.Profile.angularWeight_ideal (F : Profile) (eta : ℝ) {y : ℝ} (hy : y ≤ 0) :

F.angularWeight eta y = 4 * √2 * F.data.core.P * eta * OutgoingSchedule.shape eta * Real.exp (8 / 5 * y)

source

theorem NavierStokes.OutgoingProfile.Profile.massWeight_integral_Iic (F : Profile) (eta : ℝ) {y : ℝ} (hy : 0 ≤ y) :

MeasureTheory.IntegrableOn (F.massWeight eta) (Set.Iic y) MeasureTheory.volume ∧ ∫ (t : ℝ) in Set.Iic y, F.massWeight eta t = OutgoingSchedule.massMoment F.data.core F.amp eta y

source

theorem NavierStokes.OutgoingProfile.Profile.angularWeight_integral_Iic (F : Profile) (eta : ℝ) {y : ℝ} (hy : 0 ≤ y) :

MeasureTheory.IntegrableOn (F.angularWeight eta) (Set.Iic y) MeasureTheory.volume ∧ ∫ (t : ℝ) in Set.Iic y, F.angularWeight eta t = OutgoingSchedule.angularMoment F.data.core F.amp eta y

source

theorem NavierStokes.OutgoingProfile.Profile.massWeight_integrable (F : Profile) (eta : ℝ) :

MeasureTheory.Integrable (F.massWeight eta) MeasureTheory.volume

source

theorem NavierStokes.OutgoingProfile.Profile.angularWeight_integrable (F : Profile) (eta : ℝ) :

MeasureTheory.Integrable (F.angularWeight eta) MeasureTheory.volume

source

theorem NavierStokes.OutgoingProfile.Profile.massWeight_integral_zero (F : Profile) (eta : ℝ) :

∫ (y : ℝ), F.massWeight eta y = 0

source

theorem NavierStokes.OutgoingProfile.Profile.angularWeight_integral_zero (F : Profile) (eta : ℝ) :

∫ (y : ℝ), F.angularWeight eta y = 0

source

theorem NavierStokes.OutgoingProfile.Profile.pressureWeight_ideal (F : Profile) (eta : ℝ) {y : ℝ} (hy : y ≤ 0) :

F.pressureWeight eta y = F.data.core.P ^ 2 * OutgoingSchedule.shape eta ^ 2 * Real.exp (1 / 5 * y)

source

theorem NavierStokes.OutgoingProfile.Profile.pressureWeight_integral_ideal (F : Profile) (eta : ℝ) {y : ℝ} (hy : y ≤ 0) :

∫ (t : ℝ) in Set.Iic y, F.pressureWeight eta t = 5 * F.data.core.P ^ 2 * OutgoingSchedule.shape eta ^ 2 * Real.exp (y / 5)

source

theorem NavierStokes.OutgoingProfile.Profile.logPi_eq_primitive (F : Profile) (y eta : ℝ) :

F.logPi (y, eta) = F.axisDatum eta + 5 / 2 * F.data.core.P ^ 2 * OutgoingSchedule.shape eta ^ 2 + 1 / 2 * ∫ (t : ℝ) in 0..y, F.pressureWeight eta t

source

theorem NavierStokes.OutgoingProfile.Profile.logPi_contDiff (F : Profile) :

ContDiff ℝ (↑⊤) F.logPi

source

theorem NavierStokes.OutgoingProfile.Profile.Pi_contDiffOn (F : Profile) :

ContDiffOn ℝ (↑⊤) F.Pi domain

source

theorem NavierStokes.OutgoingProfile.Profile.logPi_ideal (F : Profile) (eta : ℝ) {y : ℝ} (hy : y ≤ 0) :

F.logPi (y, eta) = F.axisDatum eta + 5 / 2 * F.data.core.P ^ 2 * OutgoingSchedule.shape eta ^ 2 * Real.exp (y / 5)

source

theorem NavierStokes.OutgoingProfile.Profile.Pi_ideal (F : Profile) (eta : ℝ) {X : ℝ} (hX : 0 < X) (hX' : X ≤ 1) :

F.Pi (X, eta) = F.axisDatum eta + 5 / 2 * F.data.core.P ^ 2 * OutgoingSchedule.shape eta ^ 2 * X ^ (1 / 5)

source

theorem NavierStokes.OutgoingProfile.Profile.mass_comp_exp (F : Profile) (eta y : ℝ) :

|Real.exp y| • F.U (Real.exp y, eta) = F.massWeight eta y

source

theorem NavierStokes.OutgoingProfile.Profile.angular_comp_exp (F : Profile) (eta y : ℝ) :

|Real.exp y| • (F.H (Real.exp y, eta) * F.U (Real.exp y, eta)) = F.angularWeight eta y

source

theorem NavierStokes.OutgoingProfile.Profile.mass_integrable (F : Profile) (eta : ℝ) :

MeasureTheory.IntegrableOn (fun (X : ℝ) => F.U (X, eta)) (Set.Ioi 0) MeasureTheory.volume

source

theorem NavierStokes.OutgoingProfile.Profile.angular_integrable (F : Profile) (eta : ℝ) :

MeasureTheory.IntegrableOn (fun (X : ℝ) => F.H (X, eta) * F.U (X, eta)) (Set.Ioi 0) MeasureTheory.volume

source

theorem NavierStokes.OutgoingProfile.Profile.mass_integral_zero (F : Profile) (eta : ℝ) :

∫ (X : ℝ) in Set.Ioi 0, F.U (X, eta) = 0

source

theorem NavierStokes.OutgoingProfile.Profile.angular_integral_zero (F : Profile) (eta : ℝ) :

∫ (X : ℝ) in Set.Ioi 0, F.H (X, eta) * F.U (X, eta) = 0

source

theorem NavierStokes.OutgoingProfile.Profile.M_at_exp (F : Profile) (eta : ℝ) {y : ℝ} (hy : 0 ≤ y) :

F.M eta (Real.exp y) = OutgoingSchedule.massMoment F.data.core F.amp eta y

source

theorem NavierStokes.OutgoingProfile.Profile.J_at_exp (F : Profile) (eta : ℝ) {y : ℝ} (hy : 0 ≤ y) :

F.J eta (Real.exp y) = OutgoingSchedule.angularMoment F.data.core F.amp eta y

source

theorem NavierStokes.OutgoingProfile.Profile.moments_after (F : Profile) (eta : ℝ) {X : ℝ} (hX : 0 < X) (hfar : F.data.core.endpoint ≤ Real.log X) :

F.M eta X = 0 ∧ F.J eta X = 0

source

theorem NavierStokes.OutgoingProfile.Profile.energyDensity_eq (F : Profile) (eta : ℝ) :

F.energyDensity eta = CorrectedPulseAmplitude.radialEnergyIntegrand F.data F.reset.coefficients F.amp eta 1

source

theorem NavierStokes.OutgoingProfile.Profile.energy_integrable (F : Profile) (eta : ℝ) :

MeasureTheory.IntegrableOn (F.energyDensity eta) (Set.Ioi 0) MeasureTheory.volume

source

theorem NavierStokes.OutgoingProfile.Profile.totalS_eq (F : Profile) (eta : ℝ) :

F.totalS eta = CorrectedPulseAmplitude.totalEnergy F.data F.reset.coefficients (F.amp eta) eta

source

theorem NavierStokes.OutgoingProfile.Profile.renormalized_integrable (F : Profile) (eta : ℝ) :

MeasureTheory.IntegrableOn (fun (X : ℝ) => F.H (X, eta) - F.powerH X) (Set.Ioi 0) MeasureTheory.volume

source

theorem NavierStokes.OutgoingProfile.Profile.renormalized_angular_moment (F : Profile) (eta : ℝ) :

∫ (X : ℝ) in Set.Ioi 0, F.H (X, eta) - F.powerH X = 0

source

theorem NavierStokes.OutgoingProfile.Profile.angular_history_eventual (F : Profile) (eta : ℝ) {X : ℝ} (hX : 0 < X) (hfar : OutgoingTail.tailEnd F.data ≤ Real.log X) :

∫ (u : ℝ) in Set.Ioc 0 X, F.H (u, eta) = X * F.H (X, eta) / (1 - F.data.h)

source

theorem NavierStokes.OutgoingProfile.Profile.Pi_tendsto_axis (F : Profile) (eta : ℝ) :

Filter.Tendsto (fun (X : ℝ) => F.Pi (X, eta)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (F.axisDatum eta))

source

theorem NavierStokes.OutgoingProfile.image_exp_Ioi (y : ℝ) :

Real.exp '' Set.Ioi y = Set.Ioi (Real.exp y)

source

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

ℝ

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

Equations

F.canonicalKernel eta X = F.E (X, eta) ^ 2 / X

Instances For

source

theorem NavierStokes.OutgoingProfile.Profile.canonicalKernel_comp_exp (F : Profile) (eta y : ℝ) :

|Real.exp y| • F.canonicalKernel eta (Real.exp y) = F.pressureWeight eta y

source

theorem NavierStokes.OutgoingProfile.Profile.canonicalKernel_integrable (F : Profile) (eta : ℝ) :

MeasureTheory.IntegrableOn (F.canonicalKernel eta) (Set.Ioi 0) MeasureTheory.volume

source

theorem NavierStokes.OutgoingProfile.Profile.Pi_canonical (F : Profile) (eta : ℝ) {X : ℝ} (hX : 0 < X) :

F.Pi (X, eta) = -(1 / 2) * ∫ (u : ℝ) in Set.Ioi X, F.E (u, eta) ^ 2 / u

source

theorem NavierStokes.OutgoingProfile.Profile.tailEnd_after_endpoint (F : Profile) :

F.data.core.endpoint ≤ OutgoingTail.tailEnd F.data

source

structure NavierStokes.OutgoingProfile.Specification (F : Profile) (C : ℝ) :

Prop

All fields in this specification refer to one Profile, hence one reset and its associated corrected energy root.

amplitude_smooth : ContDiff ℝ (↑⊤) F.amp
angular_smooth : ContDiffOn ℝ (↑⊤) F.E domain
axial_smooth : ContDiffOn ℝ (↑⊤) F.U domain
momentum_smooth : ContDiffOn ℝ (↑⊤) F.H domain
pressure_smooth : ContDiffOn ℝ (↑⊤) F.Pi domain
angular_positive (p : ℝ × ℝ) : p ∈ domain → 0 < F.E p
amplitude_bounds (eta : ℝ) : eta ^ 2 ≤ 1 → 9 / 10 < F.amp eta ∧ F.amp eta < 6 / 5 ∧ |deriv F.amp eta| ≤ C * F.data.core.lam * (1 + Real.log (1 / F.data.core.lam))
mass_integrable (eta : ℝ) : MeasureTheory.IntegrableOn (fun (X : ℝ) => F.U (X, eta)) (Set.Ioi 0) MeasureTheory.volume
angular_integrable (eta : ℝ) : MeasureTheory.IntegrableOn (fun (X : ℝ) => F.H (X, eta) * F.U (X, eta)) (Set.Ioi 0) MeasureTheory.volume
mass_total_zero (eta : ℝ) : ∫ (X : ℝ) in Set.Ioi 0, F.U (X, eta) = 0
angular_total_zero (eta : ℝ) : ∫ (X : ℝ) in Set.Ioi 0, F.H (X, eta) * F.U (X, eta) = 0
after_pulse (eta X : ℝ) : 0 < X → F.data.core.endpoint ≤ Real.log X → F.U (X, eta) = 0 ∧ F.M eta X = 0 ∧ F.J eta X = 0
energy_integrable (eta : ℝ) : MeasureTheory.IntegrableOn (F.energyDensity eta) (Set.Ioi 0) MeasureTheory.volume
energy_zero (eta : ℝ) : eta ^ 2 ≤ 1 → F.totalS eta = 0
renormalized_integrable (eta : ℝ) : MeasureTheory.IntegrableOn (fun (X : ℝ) => F.H (X, eta) - F.powerH X) (Set.Ioi 0) MeasureTheory.volume
renormalized_zero (eta : ℝ) : ∫ (X : ℝ) in Set.Ioi 0, F.H (X, eta) - F.powerH X = 0
eventual_power (eta X : ℝ) : 0 < X → OutgoingTail.tailEnd F.data ≤ Real.log X → F.U (X, eta) = 0 ∧ F.E (X, eta) = F.powerE X ∧ ∫ (u : ℝ) in Set.Ioc 0 X, F.H (u, eta) = X * F.H (X, eta) / (1 - F.data.h)
ideal_prefix (eta X : ℝ) : 0 < X → X ≤ 1 → F.E (X, eta) = F.data.core.P * OutgoingSchedule.shape eta * X ^ (1 / 10) ∧ F.U (X, eta) = 4 * eta ∧ F.Pi (X, eta) = F.axisDatum eta + 5 / 2 * F.data.core.P ^ 2 * OutgoingSchedule.shape eta ^ 2 * X ^ (1 / 5)
pressure_integrable (eta : ℝ) : MeasureTheory.IntegrableOn (F.canonicalKernel eta) (Set.Ioi 0) MeasureTheory.volume
pressure_canonical (eta X : ℝ) : 0 < X → F.Pi (X, eta) = -(1 / 2) * ∫ (u : ℝ) in Set.Ioi X, F.E (u, eta) ^ 2 / u
same_axis_datum : F.axisDatum = SchedulePressure.axisPressure F.data
axis_limit (eta : ℝ) : Filter.Tendsto (fun (X : ℝ) => F.Pi (X, eta)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (F.axisDatum eta))
analytic_axis_datum : AnalyticOnNhd ℂ (SchedulePressure.complexAxisPressure F.data) PressureDatum.strip ∧ ∀ (eta : ℝ), SchedulePressure.complexAxisPressure F.data ↑eta = ↑(F.axisDatum eta)

Instances For

source

theorem NavierStokes.OutgoingProfile.exists_profile_for_data (P m : ℝ) (hP : 0 < P) :

∃ (lam₀ : ℝ) (C : ℝ), 0 < lam₀ ∧ 0 < C ∧ ∀ (d : OutgoingTail.TailData), d.core.P = P → d.core.m = m → d.core.wait = 60 * Real.log (1 / d.core.lam) → d.core.lam < lam₀ → ∃ (F : Profile), F.data = d ∧ Specification F C

Assemble the actual fields from the same witness returned by the corrected amplitude construction. The smallness threshold is uniform in the tail h.

source

theorem NavierStokes.OutgoingProfile.exists_outgoing_profile (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 : Profile), F.data.core.P = P ∧ F.data.core.m = m ∧ F.data.core.lam = lam ∧ F.data.h = h ∧ F.data.core.wait = 60 * Real.log (1 / lam) ∧ Specification F C

Choose lam after the fixed prefix parameters, and then any permitted h. The actual outgoing profile has every exact pre-heat moment constraint.

source

theorem NavierStokes.OutgoingProfile.exists_fixed_lambda (P m : ℝ) (hP : 0 < P) (hm : 0 < m) :

∃ (lam : ℝ) (C : ℝ), 0 < lam ∧ 0 < C ∧ ∀ (h : ℝ), 0 < h → 2 * h < lam → ∃ (F : Profile), F.data.core.P = P ∧ F.data.core.m = m ∧ F.data.core.lam = lam ∧ F.data.h = h ∧ Specification F C

A single positive schedule parameter works before the terminal parameter is selected.

Documentation

LeanPool.NavierStokesAndEuler.NavierStokes.OutgoingProfile

A single outgoing profile before the heat-tail edit #