Actual history limits on the pure heat tail

All tail integrals below are actual improper integrals. Their differentiated kernels have explicit integrable power majorants. The physical histories use the same outgoing profile and the same compensation witness throughout.

Differentiated heat corrections and their actual tail integrals

noncomputable def NavierStokes.HeatTailHistoryLimits.tailKernel (square : Bool) (h k : ℝ) (n : ℕ) (ν u : ℝ) : ℝ

Tail kernel, given by u ^ (-k) * ExtendedHeatDebts.editJet square h 1 n ν u.

Equations

• NavierStokes.HeatTailHistoryLimits.tailKernel square h k n ν u = u ^ (-k) * NavierStokes.ExtendedHeatDebts.editJet square h 1 n ν u

noncomputable def NavierStokes.HeatTailHistoryLimits.tailJet (square : Bool) (h k : ℝ) (n : ℕ) (X ν : ℝ) : ℝ

Tail jet, given by ∫ u in Ioi X, tailKernel square h k n ν u.

Equations

• NavierStokes.HeatTailHistoryLimits.tailJet square h k n X ν = ∫ (u : ℝ) in Set.Ioi X, NavierStokes.HeatTailHistoryLimits.tailKernel square h k n ν u

theorem NavierStokes.HeatTailHistoryLimits.integral_decay_power {k X : ℝ} (hk : 0 < k) (hX : 0 < X) : ∫ (u : ℝ) in Set.Ioi X, u ^ (-k - 1) = X ^ (-k) / k

theorem NavierStokes.HeatTailHistoryLimits.tailKernel_bound {h k L ν u : ℝ} (hh : 0 < h) (hu : 1 ≤ u) (hν : |ν| ≤ L) (square : Bool) (n : ℕ) : ‖tailKernel square h k n ν u‖ ≤ ExtendedHeatDebts.editBound square h L n * u ^ (-k - 1)

theorem NavierStokes.HeatTailHistoryLimits.tailKernel_continuousOn {h : ℝ} (hh : 0 < h) (square : Bool) (k : ℝ) (n : ℕ) (ν : ℝ) : ContinuousOn (tailKernel square h k n ν) (Set.Ioi 0)

theorem NavierStokes.HeatTailHistoryLimits.tailKernel_measurable {h X : ℝ} (hh : 0 < h) (hX : 1 ≤ X) (square : Bool) (k : ℝ) (n : ℕ) (ν : ℝ) : MeasureTheory.AEStronglyMeasurable (tailKernel square h k n ν) (MeasureTheory.volume.restrict (Set.Ioi X))

theorem NavierStokes.HeatTailHistoryLimits.tailKernel_dominated {h k X : ℝ} (hh : 0 < h) (hk : 0 < k) (hX : 1 ≤ X) (square : Bool) : ExtendedHeatDebts.ChainDominated (fun (n : ℕ) (ν u : ℝ) => tailKernel square h k n ν u) (MeasureTheory.volume.restrict (Set.Ioi X))

theorem NavierStokes.HeatTailHistoryLimits.tailKernel_integrable {h k X : ℝ} (hh : 0 < h) (hk : 0 < k) (hX : 1 ≤ X) (square : Bool) (n : ℕ) (ν : ℝ) : MeasureTheory.IntegrableOn (tailKernel square h k n ν) (Set.Ioi X) MeasureTheory.volume

theorem NavierStokes.HeatTailHistoryLimits.tailJet_bound {h k X L ν : ℝ} (hh : 0 < h) (hk : 0 < k) (hX : 1 ≤ X) (hν : |ν| ≤ L) (square : Bool) (n : ℕ) : |tailJet square h k n X ν| ≤ ExtendedHeatDebts.editBound square h L n / k * X ^ (-k)

theorem NavierStokes.HeatTailHistoryLimits.tailKernel_hasDerivAt {h : ℝ} (hh : 0 < h) (square : Bool) (k : ℝ) (n : ℕ) (u ν : ℝ) : HasDerivAt (fun (v : ℝ) => tailKernel square h k n v u) (tailKernel square h k (n + 1) ν u) ν

theorem NavierStokes.HeatTailHistoryLimits.tailJet_hasDerivAt {h k X : ℝ} (hh : 0 < h) (hk : 0 < k) (hX : 1 ≤ X) (square : Bool) (n : ℕ) (ν : ℝ) : HasDerivAt (tailJet square h k n X) (tailJet square h k (n + 1) X ν) ν

theorem NavierStokes.HeatTailHistoryLimits.tailJet_contDiff {h k X : ℝ} (hh : 0 < h) (hk : 0 < k) (hX : 1 ≤ X) (square : Bool) : ContDiff ℝ (↑⊤) (tailJet square h k 0 X)

theorem NavierStokes.HeatTailHistoryLimits.tailJet_eq_iteratedDeriv {h k X : ℝ} (hh : 0 < h) (hk : 0 < k) (hX : 1 ≤ X) (square : Bool) (n : ℕ) (ν : ℝ) : iteratedDeriv n (tailJet square h k 0 X) ν = tailJet square h k n X ν

theorem NavierStokes.HeatTailHistoryLimits.tailJet_tendsto_zero {h k : ℝ} (hh : 0 < h) (hk : 0 < k) (square : Bool) (n : ℕ) (ν : ℝ) : Filter.Tendsto (fun (X : ℝ) => tailJet square h k n X ν) Filter.atTop (nhds 0)

theorem NavierStokes.HeatTailHistoryLimits.mul_decay_power {k X : ℝ} (hX : 0 < X) : X * X ^ (-k) = X ^ (-(k - 1))

theorem NavierStokes.HeatTailHistoryLimits.mul_tailJet_tendsto_zero {h k : ℝ} (hh : 0 < h) (hk : 1 < k) (square : Bool) (n : ℕ) (ν : ℝ) : Filter.Tendsto (fun (X : ℝ) => X * tailJet square h k n X ν) Filter.atTop (nhds 0)

noncomputable def NavierStokes.HeatTailHistoryLimits.etaTail (square : Bool) (h k X η : ℝ) : ℝ

Eta tail, given by tailJet square h k 0 X (ParametricHeatTail.diffusion η).

Equations

• NavierStokes.HeatTailHistoryLimits.etaTail square h k X η = NavierStokes.HeatTailHistoryLimits.tailJet square h k 0 X (NavierStokes.ParametricHeatTail.diffusion η)

theorem NavierStokes.HeatTailHistoryLimits.etaTail_contDiff {h k X : ℝ} (hh : 0 < h) (hk : 0 < k) (hX : 1 ≤ X) (square : Bool) : ContDiff ℝ (↑⊤) (etaTail square h k X)

theorem NavierStokes.HeatTailHistoryLimits.etaTail_hasDerivAt {h k X : ℝ} (hh : 0 < h) (hk : 0 < k) (hX : 1 ≤ X) (square : Bool) (η : ℝ) : HasDerivAt (etaTail square h k X) (tailJet square h k 1 X (ParametricHeatTail.diffusion η) * (-2 * η)) η

theorem NavierStokes.HeatTailHistoryLimits.etaTail_bound {h k X η : ℝ} (hh : 0 < h) (hk : 0 < k) (hX : 1 ≤ X) (hη : η ∈ Set.Icc (-1) 1) (square : Bool) : |etaTail square h k X η| ≤ ExtendedHeatDebts.editBound square h 1 0 / k * X ^ (-k)

theorem NavierStokes.HeatTailHistoryLimits.etaTail_derivative_bound {h k X η : ℝ} (hh : 0 < h) (hk : 0 < k) (hX : 1 ≤ X) (hη : η ∈ Set.Icc (-1) 1) (square : Bool) : |deriv (etaTail square h k X) η| ≤ 2 * (ExtendedHeatDebts.editBound square h 1 1 / k) * X ^ (-k)

theorem NavierStokes.HeatTailHistoryLimits.etaTail_tendsto_zero {h k : ℝ} (hh : 0 < h) (hk : 0 < k) (square : Bool) (η : ℝ) : Filter.Tendsto (fun (X : ℝ) => etaTail square h k X η) Filter.atTop (nhds 0)

theorem NavierStokes.HeatTailHistoryLimits.etaTail_derivative_tendsto_zero {h k : ℝ} (hh : 0 < h) (hk : 0 < k) (square : Bool) (η : ℝ) : Filter.Tendsto (fun (X : ℝ) => deriv (etaTail square h k X) η) Filter.atTop (nhds 0)

theorem NavierStokes.HeatTailHistoryLimits.mul_etaTail_tendsto_zero {h k : ℝ} (hh : 0 < h) (hk : 1 < k) (square : Bool) (η : ℝ) : Filter.Tendsto (fun (X : ℝ) => X * etaTail square h k X η) Filter.atTop (nhds 0)

theorem NavierStokes.HeatTailHistoryLimits.mul_etaTail_derivative_tendsto_zero {h k : ℝ} (hh : 0 < h) (hk : 1 < k) (square : Bool) (η : ℝ) : Filter.Tendsto (fun (X : ℝ) => X * deriv (etaTail square h k X) η) Filter.atTop (nhds 0)

Exact exterior formulas for the supplied outgoing profile

noncomputable def NavierStokes.HeatTailHistoryLimits.amplitude (F : OutgoingProfile.Profile) (XR : ℝ) : ℝ

Amplitude, given by RenormalizedHeatMoment.outgoingPowerAmplitude F XR.

Equations

• NavierStokes.HeatTailHistoryLimits.amplitude F XR = NavierStokes.RenormalizedHeatMoment.outgoingPowerAmplitude F XR

noncomputable def NavierStokes.HeatTailHistoryLimits.angularAmplitude (F : OutgoingProfile.Profile) (XR : ℝ) : ℝ

Angular amplitude, given by Real.sqrt 2 * amplitude F XR.

Equations

• NavierStokes.HeatTailHistoryLimits.angularAmplitude F XR = √2 * NavierStokes.HeatTailHistoryLimits.amplitude F XR

noncomputable def NavierStokes.HeatTailHistoryLimits.tailStart (F : OutgoingProfile.Profile) (XR : ℝ) : ℝ

Tail start, given by max (RenormalizedHeatMoment.heatThreshold F XR) (Real.exp 1).

Equations

• NavierStokes.HeatTailHistoryLimits.tailStart F XR = max (NavierStokes.RenormalizedHeatMoment.heatThreshold F XR) (Real.exp 1)

theorem NavierStokes.HeatTailHistoryLimits.tailStart_ge_one (F : OutgoingProfile.Profile) (XR : ℝ) : 1 ≤ tailStart F XR

theorem NavierStokes.HeatTailHistoryLimits.tailStart_ge_switch (F : OutgoingProfile.Profile) {XR : ℝ} (hXR : 0 < XR) : OutgoingDilation.switchRadius F XR ≤ tailStart F XR

theorem NavierStokes.HeatTailHistoryLimits.helper_switch_one {X : ℝ} (hX : Real.exp 1 ≤ X) : HeatTailEdit.switch 1 X = 1

noncomputable def NavierStokes.HeatTailHistoryLimits.heatFactor (h η X : ℝ) : ℝ

Heat factor, given by HeatProfileExtension.physicalProfile (1 + h) X η.

Equations

• NavierStokes.HeatTailHistoryLimits.heatFactor h η X = NavierStokes.HeatProfileExtension.physicalProfile (1 + h) X η

theorem NavierStokes.HeatTailHistoryLimits.heatFactor_eq_profile (h : ℝ) {η X : ℝ} (hη : η ∈ Set.Icc (-1) 1) (hX : 0 < X) : heatFactor h η X = RadialHeatProfile.profile (1 + h) (2 * (1 - η ^ 2) / X)

theorem NavierStokes.HeatTailHistoryLimits.correction_eq_factor (h η : ℝ) {X : ℝ} (hX : Real.exp 1 ≤ X) : ExtendedHeatDebts.editJet false h 1 0 (ParametricHeatTail.diffusion η) X = heatFactor h η X - 1

theorem NavierStokes.HeatTailHistoryLimits.squareCorrection_eq_factor (h η : ℝ) {X : ℝ} (hX : Real.exp 1 ≤ X) : ExtendedHeatDebts.editJet true h 1 0 (ParametricHeatTail.diffusion η) X = heatFactor h η X ^ 2 - 1

theorem NavierStokes.HeatTailHistoryLimits.sqrt_power_identity (h D : ℝ) {X : ℝ} (hX : 0 < X) : √(2 * X) * (D * X ^ (-(1 / 2 + h))) = √2 * D * X ^ (-h)

theorem NavierStokes.HeatTailHistoryLimits.powerH_eq (F : OutgoingProfile.Profile) {XR X : ℝ} (hXR : 0 < XR) (hX : 0 < X) : OutgoingDilation.powerH F XR X = angularAmplitude F XR * X ^ (-F.data.h)

theorem NavierStokes.HeatTailHistoryLimits.heated_H_eq (F : OutgoingProfile.Profile) {XR : ℝ} (hXR : 0 < XR) (c : ℝ → HeatedOutgoing.Coeff) {η X : ℝ} (hη : η ∈ Set.Icc (-1) 1) (hX : tailStart F XR ≤ X) : HeatedOutgoing.H F XR c (X, η) = angularAmplitude F XR * X ^ (-F.data.h) * heatFactor F.data.h η X

theorem NavierStokes.HeatTailHistoryLimits.heated_square_eq (F : OutgoingProfile.Profile) {XR : ℝ} (hXR : 0 < XR) (c : ℝ → HeatedOutgoing.Coeff) {η X : ℝ} (hη : η ∈ Set.Icc (-1) 1) (hX : tailStart F XR ≤ X) : HeatedOutgoing.E F XR c (X, η) ^ 2 = amplitude F XR ^ 2 * X ^ (-(1 + 2 * F.data.h)) * heatFactor F.data.h η X ^ 2

theorem NavierStokes.HeatTailHistoryLimits.heated_difference_eq_kernel (F : OutgoingProfile.Profile) {XR : ℝ} (hXR : 0 < XR) (c : ℝ → HeatedOutgoing.Coeff) {η X : ℝ} (hη : η ∈ Set.Icc (-1) 1) (hX : tailStart F XR ≤ X) : HeatedOutgoing.H F XR c (X, η) - OutgoingDilation.powerH F XR X = angularAmplitude F XR * tailKernel false F.data.h F.data.h 0 (ParametricHeatTail.diffusion η) X

theorem NavierStokes.HeatTailHistoryLimits.heated_square_eq_kernel (F : OutgoingProfile.Profile) {XR : ℝ} (hXR : 0 < XR) (c : ℝ → HeatedOutgoing.Coeff) {η X : ℝ} (hη : η ∈ Set.Icc (-1) 1) (hX : tailStart F XR ≤ X) : HeatedOutgoing.E F XR c (X, η) ^ 2 = amplitude F XR ^ 2 * (X ^ (-(1 + 2 * F.data.h)) + tailKernel true F.data.h (1 + 2 * F.data.h) 0 (ParametricHeatTail.diffusion η) X)

theorem NavierStokes.HeatTailHistoryLimits.canonicalKernel_eq_kernel (F : OutgoingProfile.Profile) {XR : ℝ} (hXR : 0 < XR) (c : ℝ → HeatedOutgoing.Coeff) {η X : ℝ} (hη : η ∈ Set.Icc (-1) 1) (hX : tailStart F XR ≤ X) : HeatedOutgoing.canonicalKernel F XR c η X = amplitude F XR ^ 2 * (X ^ (-(2 + 2 * F.data.h)) + tailKernel true F.data.h (2 + 2 * F.data.h) 0 (ParametricHeatTail.diffusion η) X)

The constants are fixed by the same compensation witness

noncomputable def NavierStokes.HeatTailHistoryLimits.angularHistory (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → HeatedOutgoing.Coeff) (η X : ℝ) : ℝ

Angular history, given by ∫ u in Ioc 0 X, HeatedOutgoing.H F XR c (u,η).

Equations

• NavierStokes.HeatTailHistoryLimits.angularHistory F XR c η X = ∫ (u : ℝ) in Set.Ioc 0 X, NavierStokes.HeatedOutgoing.H F XR c (u, η)

noncomputable def NavierStokes.HeatTailHistoryLimits.energyHistory (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → HeatedOutgoing.Coeff) (η X : ℝ) : ℝ

Energy history, given by ∫ u in Ioc 0 X, HeatedOutgoing.energyDensity F XR c η u.

Equations

• NavierStokes.HeatTailHistoryLimits.energyHistory F XR c η X = ∫ (u : ℝ) in Set.Ioc 0 X, NavierStokes.HeatedOutgoing.energyDensity F XR c η u

noncomputable def NavierStokes.HeatTailHistoryLimits.powerHistory (F : OutgoingProfile.Profile) (XR X : ℝ) : ℝ

Power history, given by ∫ u in Ioc 0 X, OutgoingDilation.powerH F XR u.

Equations

• NavierStokes.HeatTailHistoryLimits.powerHistory F XR X = ∫ (u : ℝ) in Set.Ioc 0 X, NavierStokes.OutgoingDilation.powerH F XR u

theorem NavierStokes.HeatTailHistoryLimits.split_positive_integral {f : ℝ → ℝ} (hf : MeasureTheory.IntegrableOn f (Set.Ioi 0) MeasureTheory.volume) {X : ℝ} (hX : 0 ≤ X) : (∫ (u : ℝ) in Set.Ioc 0 X, f u) + ∫ (u : ℝ) in Set.Ioi X, f u = ∫ (u : ℝ) in Set.Ioi 0, f u

theorem NavierStokes.HeatTailHistoryLimits.angularHistory_integrable {F : OutgoingProfile.Profile} {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) {η X : ℝ} (hη : η ∈ HeatedOutgoing.parameterDomain) (hX : 0 < X) : MeasureTheory.IntegrableOn (fun (u : ℝ) => HeatedOutgoing.H F XR w.coefficients (u, η)) (Set.Ioc 0 X) MeasureTheory.volume

theorem NavierStokes.HeatTailHistoryLimits.angularHistory_eq_power_sub_future {F : OutgoingProfile.Profile} {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) {η X : ℝ} (hη : η ∈ HeatedOutgoing.parameterDomain) (hX : 0 < X) : angularHistory F XR w.coefficients η X = powerHistory F XR X - ∫ (u : ℝ) in Set.Ioi X, HeatedOutgoing.H F XR w.coefficients (u, η) - OutgoingDilation.powerH F XR u

theorem NavierStokes.HeatTailHistoryLimits.energyHistory_eq_square_future {F : OutgoingProfile.Profile} {XR C B : ℝ} (hF : OutgoingProfile.Specification F B) (w : HeatedOutgoing.CompensationWitness F XR C) {η X : ℝ} (hη : η ∈ HeatedOutgoing.parameterDomain) (hX : OutgoingDilation.switchRadius F XR ≤ X) : energyHistory F XR w.coefficients η X = 1 / 2 * ∫ (u : ℝ) in Set.Ioi X, HeatedOutgoing.E F XR w.coefficients (u, η) ^ 2

noncomputable def NavierStokes.HeatTailHistoryLimits.powerTail (k X : ℝ) : ℝ

Power tail, given by X ^ (-(k - 1)) / (k - 1).

Equations

• NavierStokes.HeatTailHistoryLimits.powerTail k X = X ^ (-(k - 1)) / (k - 1)

theorem NavierStokes.HeatTailHistoryLimits.powerTail_eq_integral {k X : ℝ} (hk : 1 < k) (hX : 0 < X) : powerTail k X = ∫ (u : ℝ) in Set.Ioi X, u ^ (-k)

theorem NavierStokes.HeatTailHistoryLimits.angularHistory_formula {F : OutgoingProfile.Profile} {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) {η X : ℝ} (hη : η ∈ HeatedOutgoing.parameterDomain) (hX : tailStart F XR ≤ X) : angularHistory F XR w.coefficients η X = powerHistory F XR X - angularAmplitude F XR * etaTail false F.data.h F.data.h X η

theorem NavierStokes.HeatTailHistoryLimits.square_future_formula (F : OutgoingProfile.Profile) {XR : ℝ} (hXR : 0 < XR) (c : ℝ → HeatedOutgoing.Coeff) {η X : ℝ} (hη : η ∈ HeatedOutgoing.parameterDomain) (hX : tailStart F XR ≤ X) : ∫ (u : ℝ) in Set.Ioi X, HeatedOutgoing.E F XR c (u, η) ^ 2 = amplitude F XR ^ 2 * (powerTail (1 + 2 * F.data.h) X + etaTail true F.data.h (1 + 2 * F.data.h) X η)

theorem NavierStokes.HeatTailHistoryLimits.energyHistory_formula {F : OutgoingProfile.Profile} {XR C B : ℝ} (hF : OutgoingProfile.Specification F B) (w : HeatedOutgoing.CompensationWitness F XR C) {η X : ℝ} (hη : η ∈ HeatedOutgoing.parameterDomain) (hX : tailStart F XR ≤ X) : energyHistory F XR w.coefficients η X = amplitude F XR ^ 2 / 2 * (powerTail (1 + 2 * F.data.h) X + etaTail true F.data.h (1 + 2 * F.data.h) X η)

theorem NavierStokes.HeatTailHistoryLimits.pressure_formula (F : OutgoingProfile.Profile) {XR : ℝ} (hXR : 0 < XR) (c : ℝ → HeatedOutgoing.Coeff) {η X : ℝ} (hη : η ∈ HeatedOutgoing.parameterDomain) (hX : tailStart F XR ≤ X) : HeatedOutgoing.Pi F XR c (X, η) = -(amplitude F XR ^ 2 / 2) * (powerTail (2 + 2 * F.data.h) X + etaTail true F.data.h (2 + 2 * F.data.h) X η)

Genuine parameter derivatives and the history limits

theorem NavierStokes.HeatTailHistoryLimits.parameter_germ {f g : ℝ → ℝ} {η : ℝ} (hη : η ∈ Set.Ioo (-1) 1) (he : ∀ t ∈ Set.Icc (-1) 1, f t = g t) : f =ᶠ[nhds η] g

theorem NavierStokes.HeatTailHistoryLimits.angularHistory_hasDerivAt {F : OutgoingProfile.Profile} {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) {η X : ℝ} (hη : η ∈ Set.Ioo (-1) 1) (hX : tailStart F XR ≤ X) : HasDerivAt (fun (t : ℝ) => angularHistory F XR w.coefficients t X) (-angularAmplitude F XR * deriv (etaTail false F.data.h F.data.h X) η) η

theorem NavierStokes.HeatTailHistoryLimits.energyHistory_hasDerivAt {F : OutgoingProfile.Profile} {XR C B : ℝ} (hF : OutgoingProfile.Specification F B) (w : HeatedOutgoing.CompensationWitness F XR C) {η X : ℝ} (hη : η ∈ Set.Ioo (-1) 1) (hX : tailStart F XR ≤ X) : HasDerivAt (fun (t : ℝ) => energyHistory F XR w.coefficients t X) (amplitude F XR ^ 2 / 2 * deriv (etaTail true F.data.h (1 + 2 * F.data.h) X) η) η

theorem NavierStokes.HeatTailHistoryLimits.pressure_hasDerivAt (F : OutgoingProfile.Profile) {XR : ℝ} (hXR : 0 < XR) (c : ℝ → HeatedOutgoing.Coeff) {η X : ℝ} (hη : η ∈ Set.Ioo (-1) 1) (hX : tailStart F XR ≤ X) : HasDerivAt (fun (t : ℝ) => HeatedOutgoing.Pi F XR c (X, t)) (-(amplitude F XR ^ 2 / 2) * deriv (etaTail true F.data.h (2 + 2 * F.data.h) X) η) η

theorem NavierStokes.HeatTailHistoryLimits.powerTail_tendsto_zero {k : ℝ} (hk : 1 < k) : Filter.Tendsto (powerTail k) Filter.atTop (nhds 0)

theorem NavierStokes.HeatTailHistoryLimits.mul_powerTail_tendsto_zero {k : ℝ} (hk : 2 < k) : Filter.Tendsto (fun (X : ℝ) => X * powerTail k X) Filter.atTop (nhds 0)

theorem NavierStokes.HeatTailHistoryLimits.angularHistory_sub_power_tendsto_zero {F : OutgoingProfile.Profile} {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) {η : ℝ} (hη : η ∈ HeatedOutgoing.parameterDomain) : Filter.Tendsto (fun (X : ℝ) => angularHistory F XR w.coefficients η X - powerHistory F XR X) Filter.atTop (nhds 0)

theorem NavierStokes.HeatTailHistoryLimits.angularHistory_eta_tendsto_zero {F : OutgoingProfile.Profile} {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) {η : ℝ} (hη : η ∈ Set.Ioo (-1) 1) : Filter.Tendsto (fun (X : ℝ) => deriv (fun (t : ℝ) => angularHistory F XR w.coefficients t X) η) Filter.atTop (nhds 0)

theorem NavierStokes.HeatTailHistoryLimits.energyHistory_tendsto_zero {F : OutgoingProfile.Profile} {XR C B : ℝ} (hF : OutgoingProfile.Specification F B) (w : HeatedOutgoing.CompensationWitness F XR C) {η : ℝ} (hη : η ∈ HeatedOutgoing.parameterDomain) : Filter.Tendsto (fun (X : ℝ) => energyHistory F XR w.coefficients η X) Filter.atTop (nhds 0)

theorem NavierStokes.HeatTailHistoryLimits.energyHistory_eta_tendsto_zero {F : OutgoingProfile.Profile} {XR C B : ℝ} (hF : OutgoingProfile.Specification F B) (w : HeatedOutgoing.CompensationWitness F XR C) {η : ℝ} (hη : η ∈ Set.Ioo (-1) 1) : Filter.Tendsto (fun (X : ℝ) => deriv (fun (t : ℝ) => energyHistory F XR w.coefficients t X) η) Filter.atTop (nhds 0)

theorem NavierStokes.HeatTailHistoryLimits.mul_pressure_tendsto_zero (F : OutgoingProfile.Profile) {XR : ℝ} (hXR : 0 < XR) (c : ℝ → HeatedOutgoing.Coeff) {η : ℝ} (hη : η ∈ HeatedOutgoing.parameterDomain) : Filter.Tendsto (fun (X : ℝ) => X * HeatedOutgoing.Pi F XR c (X, η)) Filter.atTop (nhds 0)

theorem NavierStokes.HeatTailHistoryLimits.mul_pressure_eta_tendsto_zero (F : OutgoingProfile.Profile) {XR : ℝ} (hXR : 0 < XR) (c : ℝ → HeatedOutgoing.Coeff) {η : ℝ} (hη : η ∈ Set.Ioo (-1) 1) : Filter.Tendsto (fun (X : ℝ) => X * deriv (fun (t : ℝ) => HeatedOutgoing.Pi F XR c (X, t)) η) Filter.atTop (nhds 0)

The actual angular field and its radial derivative at infinity

noncomputable def NavierStokes.HeatTailHistoryLimits.heatH (h D η X : ℝ) : ℝ

Heat H, given by D * X ^ (-h) * heatFactor h η X.

Equations

• NavierStokes.HeatTailHistoryLimits.heatH h D η X = D * X ^ (-h) * NavierStokes.HeatTailHistoryLimits.heatFactor h η X

noncomputable def NavierStokes.HeatTailHistoryLimits.factorSlope (h η X : ℝ) : ℝ

Factor slope, given by -h * heatFactor h η X - (2 * (1 - η ^ 2) / X) * deriv (HeatProfileExtension.extension (1 + h)) (2 * (1 - η ^ 2) / X).

Equations

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

theorem NavierStokes.HeatTailHistoryLimits.heatFactor_tendsto_one {h : ℝ} (hh : 0 < h) (η : ℝ) : Filter.Tendsto (heatFactor h η) Filter.atTop (nhds 1)

theorem NavierStokes.HeatTailHistoryLimits.factorSlope_tendsto {h : ℝ} (hh : 0 < h) (η : ℝ) : Filter.Tendsto (factorSlope h η) Filter.atTop (nhds (-h))

theorem NavierStokes.HeatTailHistoryLimits.heatH_tendsto_zero {h : ℝ} (hh : 0 < h) (D η : ℝ) : Filter.Tendsto (heatH h D η) Filter.atTop (nhds 0)

theorem NavierStokes.HeatTailHistoryLimits.heatH_hasDerivAt {h X : ℝ} (hh : 0 < h) (D η : ℝ) (hX : 0 < X) : HasDerivAt (heatH h D η) (D * X ^ (-h - 1) * factorSlope h η X) X

theorem NavierStokes.HeatTailHistoryLimits.heatH_weighted_deriv {h X : ℝ} (hh : 0 < h) (D η : ℝ) (hX : 0 < X) : X * deriv (heatH h D η) X = D * X ^ (-h) * factorSlope h η X

theorem NavierStokes.HeatTailHistoryLimits.heatH_weighted_deriv_tendsto_zero {h : ℝ} (hh : 0 < h) (D η : ℝ) : Filter.Tendsto (fun (X : ℝ) => X * deriv (heatH h D η) X) Filter.atTop (nhds 0)

theorem NavierStokes.HeatTailHistoryLimits.H_tendsto_zero (F : OutgoingProfile.Profile) {XR : ℝ} (hXR : 0 < XR) (c : ℝ → HeatedOutgoing.Coeff) {η : ℝ} (hη : η ∈ HeatedOutgoing.parameterDomain) : Filter.Tendsto (fun (X : ℝ) => HeatedOutgoing.H F XR c (X, η)) Filter.atTop (nhds 0)

theorem NavierStokes.HeatTailHistoryLimits.H_hasDerivAt (F : OutgoingProfile.Profile) {XR : ℝ} (hXR : 0 < XR) (c : ℝ → HeatedOutgoing.Coeff) {η X : ℝ} (hη : η ∈ HeatedOutgoing.parameterDomain) (hX : tailStart F XR < X) : HasDerivAt (fun (u : ℝ) => HeatedOutgoing.H F XR c (u, η)) (angularAmplitude F XR * X ^ (-F.data.h - 1) * factorSlope F.data.h η X) X

theorem NavierStokes.HeatTailHistoryLimits.mul_H_deriv_tendsto_zero (F : OutgoingProfile.Profile) {XR : ℝ} (hXR : 0 < XR) (c : ℝ → HeatedOutgoing.Coeff) {η : ℝ} (hη : η ∈ HeatedOutgoing.parameterDomain) : Filter.Tendsto (fun (X : ℝ) => X * deriv (fun (u : ℝ) => HeatedOutgoing.H F XR c (u, η)) X) Filter.atTop (nhds 0)

theorem NavierStokes.HeatTailHistoryLimits.mul_tailKernel_tendsto_zero {h k : ℝ} (hh : 0 < h) (hk : 0 < k) (square : Bool) (n : ℕ) (ν : ℝ) : Filter.Tendsto (fun (X : ℝ) => X * tailKernel square h k n ν X) Filter.atTop (nhds 0)

theorem NavierStokes.HeatTailHistoryLimits.mul_H_sub_powerH_tendsto_zero (F : OutgoingProfile.Profile) {XR : ℝ} (hXR : 0 < XR) (c : ℝ → HeatedOutgoing.Coeff) {η : ℝ} (hη : η ∈ HeatedOutgoing.parameterDomain) : Filter.Tendsto (fun (X : ℝ) => X * (HeatedOutgoing.H F XR c (X, η) - OutgoingDilation.powerH F XR X)) Filter.atTop (nhds 0)

theorem NavierStokes.HeatTailHistoryLimits.actual_history_limits {F : OutgoingProfile.Profile} {XR C B : ℝ} (hF : OutgoingProfile.Specification F B) (w : HeatedOutgoing.CompensationWitness F XR C) {η : ℝ} (hη : η ∈ Set.Ioo (-1) 1) : Filter.Tendsto (fun (X : ℝ) => angularHistory F XR w.coefficients η X - powerHistory F XR X) Filter.atTop (nhds 0) ∧ Filter.Tendsto (fun (X : ℝ) => deriv (fun (t : ℝ) => angularHistory F XR w.coefficients t X) η) Filter.atTop (nhds 0) ∧ Filter.Tendsto (fun (X : ℝ) => HeatedOutgoing.H F XR w.coefficients (X, η)) Filter.atTop (nhds 0) ∧ Filter.Tendsto (fun (X : ℝ) => X * deriv (fun (u : ℝ) => HeatedOutgoing.H F XR w.coefficients (u, η)) X) Filter.atTop (nhds 0) ∧ Filter.Tendsto (fun (X : ℝ) => energyHistory F XR w.coefficients η X) Filter.atTop (nhds 0) ∧ Filter.Tendsto (fun (X : ℝ) => deriv (fun (t : ℝ) => energyHistory F XR w.coefficients t X) η) Filter.atTop (nhds 0) ∧ Filter.Tendsto (fun (X : ℝ) => X * HeatedOutgoing.Pi F XR w.coefficients (X, η)) Filter.atTop (nhds 0) ∧ Filter.Tendsto (fun (X : ℝ) => X * deriv (fun (t : ℝ) => HeatedOutgoing.Pi F XR w.coefficients (X, t)) η) Filter.atTop (nhds 0) ∧ Filter.Tendsto (fun (X : ℝ) => X * (HeatedOutgoing.H F XR w.coefficients (X, η) - OutgoingDilation.powerH F XR X)) Filter.atTop (nhds 0)

All required history limits for one and the same actual heat completion.