The physical heat edit: diffusion is 1 - eta^2

The diffusion variable is allowed to reach zero. All endpoint derivatives below are derivatives within the closed parameter domain; no extension to negative diffusion is assumed.

Differentiation of dominated derivative chains on the closed half-line

def NavierStokes.ParametricHeatTail.ChainDominated {α : Type u_1} [MeasurableSpace α] (J : ℕ → ℝ → α → ℝ) (μ : MeasureTheory.Measure α) : Prop

The domination is uniform in the parameter on each bounded interval.

Equations

• NavierStokes.ParametricHeatTail.ChainDominated J μ = ∀ (n : ℕ) (L : ℝ), 0 < L → ∃ (b : α → ℝ), MeasureTheory.Integrable b μ ∧ ∀ᵐ (t : α) ∂μ, ∀ ν ∈ Set.Icc 0 L, ‖J n ν t‖ ≤ b t

theorem NavierStokes.ParametricHeatTail.chain_integrable {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {J : ℕ → ℝ → α → ℝ} (hm : ∀ (n : ℕ) (ν : ℝ), 0 ≤ ν → MeasureTheory.AEStronglyMeasurable (J n ν) μ) (hb : ChainDominated J μ) (n : ℕ) {ν : ℝ} (hν : 0 ≤ ν) : MeasureTheory.Integrable (J n ν) μ

theorem NavierStokes.ParametricHeatTail.integral_chain_continuousOn {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {J : ℕ → ℝ → α → ℝ} (hJ : ∀ᵐ (t : α) ∂μ, ∀ (n : ℕ) (ν : ℝ), 0 ≤ ν → HasDerivWithinAt (fun (u : ℝ) => J n u t) (J (n + 1) ν t) (Set.Ici 0) ν) (hm : ∀ (n : ℕ) (ν : ℝ), 0 ≤ ν → MeasureTheory.AEStronglyMeasurable (J n ν) μ) (hb : ChainDominated J μ) (n : ℕ) : ContinuousOn (fun (ν : ℝ) => ∫ (t : α), J n ν t ∂μ) (Set.Ici 0)

theorem NavierStokes.ParametricHeatTail.integral_chain_hasDerivAt {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {J : ℕ → ℝ → α → ℝ} (hJ : ∀ᵐ (t : α) ∂μ, ∀ (n : ℕ) (ν : ℝ), 0 ≤ ν → HasDerivWithinAt (fun (u : ℝ) => J n u t) (J (n + 1) ν t) (Set.Ici 0) ν) (hm : ∀ (n : ℕ) (ν : ℝ), 0 ≤ ν → MeasureTheory.AEStronglyMeasurable (J n ν) μ) (hb : ChainDominated J μ) (n : ℕ) {ν : ℝ} (hν : 0 < ν) : HasDerivAt (fun (u : ℝ) => ∫ (t : α), J n u t ∂μ) (∫ (t : α), J (n + 1) ν t ∂μ) ν

theorem NavierStokes.ParametricHeatTail.integral_chain_hasDerivWithinAt {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {J : ℕ → ℝ → α → ℝ} (hJ : ∀ᵐ (t : α) ∂μ, ∀ (n : ℕ) (ν : ℝ), 0 ≤ ν → HasDerivWithinAt (fun (u : ℝ) => J n u t) (J (n + 1) ν t) (Set.Ici 0) ν) (hm : ∀ (n : ℕ) (ν : ℝ), 0 ≤ ν → MeasureTheory.AEStronglyMeasurable (J n ν) μ) (hb : ChainDominated J μ) (n : ℕ) {ν : ℝ} (hν : 0 ≤ ν) : HasDerivWithinAt (fun (u : ℝ) => ∫ (t : α), J n u t ∂μ) (∫ (t : α), J (n + 1) ν t ∂μ) (Set.Ici 0) ν

theorem NavierStokes.ParametricHeatTail.iteratedDerivWithin_integral_chain {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {J : ℕ → ℝ → α → ℝ} (hJ : ∀ᵐ (t : α) ∂μ, ∀ (n : ℕ) (ν : ℝ), 0 ≤ ν → HasDerivWithinAt (fun (u : ℝ) => J n u t) (J (n + 1) ν t) (Set.Ici 0) ν) (hm : ∀ (n : ℕ) (ν : ℝ), 0 ≤ ν → MeasureTheory.AEStronglyMeasurable (J n ν) μ) (hb : ChainDominated J μ) (n : ℕ) {ν : ℝ} (hν : 0 ≤ ν) : iteratedDerivWithin n (fun (u : ℝ) => ∫ (t : α), J 0 u t ∂μ) (Set.Ici 0) ν = ∫ (t : α), J n ν t ∂μ

theorem NavierStokes.ParametricHeatTail.contDiffOn_integral_chain {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {J : ℕ → ℝ → α → ℝ} (hJ : ∀ᵐ (t : α) ∂μ, ∀ (n : ℕ) (ν : ℝ), 0 ≤ ν → HasDerivWithinAt (fun (u : ℝ) => J n u t) (J (n + 1) ν t) (Set.Ici 0) ν) (hm : ∀ (n : ℕ) (ν : ℝ), 0 ≤ ν → MeasureTheory.AEStronglyMeasurable (J n ν) μ) (hb : ChainDominated J μ) : ContDiffOn ℝ (↑⊤) (fun (ν : ℝ) => ∫ (t : α), J 0 ν t ∂μ) (Set.Ici 0)

Explicit algebra of genuine derivative chains

noncomputable def NavierStokes.ParametricHeatTail.jetProduct (a b : ℕ → ℝ) : ℕ → ℝ

Recursive Leibniz product. Its derivative identity is proved below.

Equations

• One or more equations did not get rendered due to their size.
• NavierStokes.ParametricHeatTail.jetProduct a b 0 = a 0 * b 0

theorem NavierStokes.ParametricHeatTail.jetProduct_nonneg {a b : ℕ → ℝ} (ha : ∀ (i : ℕ), 0 ≤ a i) (hb : ∀ (i : ℕ), 0 ≤ b i) (n : ℕ) : 0 ≤ jetProduct a b n

theorem NavierStokes.ParametricHeatTail.jetProduct_hasDerivWithinAt {a b : ℕ → ℝ → ℝ} {s : Set ℝ} {ν : ℝ} (ha : ∀ (i : ℕ), HasDerivWithinAt (a i) (a (i + 1) ν) s ν) (hb : ∀ (i : ℕ), HasDerivWithinAt (b i) (b (i + 1) ν) s ν) (n : ℕ) : HasDerivWithinAt (fun (u : ℝ) => jetProduct (fun (i : ℕ) => a i u) (fun (i : ℕ) => b i u) n) (jetProduct (fun (i : ℕ) => a i ν) (fun (i : ℕ) => b i ν) (n + 1)) s ν

theorem NavierStokes.ParametricHeatTail.jetProduct_continuousOn {a b : ℕ → ℝ → ℝ} {s : Set ℝ} (ha : ∀ (i : ℕ), ContinuousOn (a i) s) (hb : ∀ (i : ℕ), ContinuousOn (b i) s) (n : ℕ) : ContinuousOn (fun (x : ℝ) => jetProduct (fun (i : ℕ) => a i x) (fun (i : ℕ) => b i x) n) s

theorem NavierStokes.ParametricHeatTail.jetProduct_bound {a b A B : ℕ → ℝ} {X : ℝ} (hX : 1 ≤ X) (hA : ∀ (i : ℕ), 0 ≤ A i) (hB : ∀ (i : ℕ), 0 ≤ B i) (ha : ∀ (i : ℕ), |a i| ≤ A i / X) (hb : ∀ (i : ℕ), |b i| ≤ B i / X) (n : ℕ) : |jetProduct a b n| ≤ jetProduct A B n / X

The actual diffusion jets of the switched multiplier

noncomputable def NavierStokes.ParametricHeatTail.heatJetBound (h : ℝ) (n : ℕ) : ℝ

Heat jet bound, given by |(Real.Gamma (1 + h))⁻¹ * RadialHeatProfile.derivativeCoeff (1 + h) n| * Real.Gamma (1 + h + (n : ℝ)).

Equations

• NavierStokes.ParametricHeatTail.heatJetBound h n = |(Real.Gamma (1 + h))⁻¹ * NavierStokes.RadialHeatProfile.derivativeCoeff (1 + h) n| * Real.Gamma (1 + h + ↑n)

noncomputable def NavierStokes.ParametricHeatTail.correctionJet (h K : ℝ) : ℕ → ℝ → ℝ → ℝ

Correction jet used in parametric heat tail.

Equations

• One or more equations did not get rendered due to their size.
• NavierStokes.ParametricHeatTail.correctionJet h K 0 x✝¹ x✝ = NavierStokes.HeatTailEdit.switch K x✝ * (NavierStokes.RadialHeatProfile.profile (1 + h) (2 * x✝¹ / x✝) - 1)

noncomputable def NavierStokes.ParametricHeatTail.correctionBound (h L : ℝ) : ℕ → ℝ

Correction bound as an element of ℕ → ℝ | 0 => heatConstant h L | n + 1 => 2 ^ (n + 1) * heatJetBound h (n + 1).

Equations

• NavierStokes.ParametricHeatTail.correctionBound h L 0 = NavierStokes.HeatTailEdit.heatConstant h L
• NavierStokes.ParametricHeatTail.correctionBound h L n.succ = 2 ^ (n + 1) * NavierStokes.ParametricHeatTail.heatJetBound h (n + 1)

theorem NavierStokes.ParametricHeatTail.correctionJet_zero (h K ν X : ℝ) : correctionJet h K 0 ν X = HeatTailEdit.multiplier h ν K X - 1

theorem NavierStokes.ParametricHeatTail.heatJetBound_nonneg {h : ℝ} (hh : 0 < h) (n : ℕ) : 0 ≤ heatJetBound h n

theorem NavierStokes.ParametricHeatTail.correctionBound_nonneg {h L : ℝ} (hh : 0 < h) (hL : 0 ≤ L) (n : ℕ) : 0 ≤ correctionBound h L n

theorem NavierStokes.ParametricHeatTail.correctionJet_hasDerivWithinAt {h K ν X : ℝ} (hh : 0 < h) (hX : 0 < X) (hν : 0 ≤ ν) (n : ℕ) : HasDerivWithinAt (fun (u : ℝ) => correctionJet h K n u X) (correctionJet h K (n + 1) ν X) (Set.Ici 0) ν

theorem NavierStokes.ParametricHeatTail.correctionJet_continuousOn_X {h K ν : ℝ} (hh : 0 < h) (hK : 0 < K) (hν : 0 ≤ ν) (n : ℕ) : ContinuousOn (fun (X : ℝ) => correctionJet h K n ν X) (Set.Ioi 0)

theorem NavierStokes.ParametricHeatTail.correctionJet_bound {h K L ν X : ℝ} (hh : 0 < h) (hX : 1 ≤ X) (hν : ν ∈ Set.Icc 0 L) (n : ℕ) : |correctionJet h K n ν X| ≤ correctionBound h L n / X

noncomputable def NavierStokes.ParametricHeatTail.squareCorrectionJet (h K : ℝ) (n : ℕ) (ν X : ℝ) : ℝ

All diffusion derivatives of M^2-1, with M the actual switched multiplier.

Equations

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

noncomputable def NavierStokes.ParametricHeatTail.squareCorrectionBound (h L : ℝ) (n : ℕ) : ℝ

Square correction bound, given by 2 * correctionBound h L n + jetProduct (correctionBound h L) (correctionBound h L) n.

Equations

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

theorem NavierStokes.ParametricHeatTail.squareCorrectionJet_zero (h K ν X : ℝ) : squareCorrectionJet h K 0 ν X = HeatTailEdit.multiplier h ν K X ^ 2 - 1

theorem NavierStokes.ParametricHeatTail.squareCorrectionJet_hasDerivWithinAt {h K ν X : ℝ} (hh : 0 < h) (hX : 0 < X) (hν : 0 ≤ ν) (n : ℕ) : HasDerivWithinAt (fun (u : ℝ) => squareCorrectionJet h K n u X) (squareCorrectionJet h K (n + 1) ν X) (Set.Ici 0) ν

theorem NavierStokes.ParametricHeatTail.squareCorrectionJet_continuousOn_X {h K ν : ℝ} (hh : 0 < h) (hK : 0 < K) (hν : 0 ≤ ν) (n : ℕ) : ContinuousOn (fun (X : ℝ) => squareCorrectionJet h K n ν X) (Set.Ioi 0)

theorem NavierStokes.ParametricHeatTail.squareCorrectionBound_nonneg {h L : ℝ} (hh : 0 < h) (hL : 0 ≤ L) (n : ℕ) : 0 ≤ squareCorrectionBound h L n

theorem NavierStokes.ParametricHeatTail.squareCorrectionJet_bound {h K L ν X : ℝ} (hh : 0 < h) (hX : 1 ≤ X) (hν : ν ∈ Set.Icc 0 L) (n : ℕ) : |squareCorrectionJet h K n ν X| ≤ squareCorrectionBound h L n / X

Actual improper integrals of the diffusion jets

noncomputable def NavierStokes.ParametricHeatTail.editJet (square : Bool) (h K : ℝ) (n : ℕ) (ν X : ℝ) : ℝ

false selects the linear edit, true the square edit.

Equations

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

noncomputable def NavierStokes.ParametricHeatTail.editBound (square : Bool) (h L : ℝ) (n : ℕ) : ℝ

Edit bound, with branches according to square.

Equations

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

theorem NavierStokes.ParametricHeatTail.editJet_hasDerivWithinAt {h K ν X : ℝ} (hh : 0 < h) (hX : 0 < X) (hν : 0 ≤ ν) (square : Bool) (n : ℕ) : HasDerivWithinAt (fun (u : ℝ) => editJet square h K n u X) (editJet square h K (n + 1) ν X) (Set.Ici 0) ν

theorem NavierStokes.ParametricHeatTail.editJet_continuousOn_X {h K ν : ℝ} (hh : 0 < h) (hK : 0 < K) (hν : 0 ≤ ν) (square : Bool) (n : ℕ) : ContinuousOn (fun (X : ℝ) => editJet square h K n ν X) (Set.Ioi 0)

theorem NavierStokes.ParametricHeatTail.editBound_nonneg {h L : ℝ} (hh : 0 < h) (hL : 0 ≤ L) (square : Bool) (n : ℕ) : 0 ≤ editBound square h L n

theorem NavierStokes.ParametricHeatTail.editJet_bound {h K L ν X : ℝ} (hh : 0 < h) (hX : 1 ≤ X) (hν : ν ∈ Set.Icc 0 L) (square : Bool) (n : ℕ) : |editJet square h K n ν X| ≤ editBound square h L n / X

noncomputable def NavierStokes.ParametricHeatTail.weightedJet (W : ℝ → ℝ) (square : Bool) (h K q : ℝ) (n : ℕ) (ν X : ℝ) : ℝ

Weighted jet, given by X ^ q * W X * editJet square h K n ν X.

Equations

• NavierStokes.ParametricHeatTail.weightedJet W square h K q n ν X = X ^ q * W X * NavierStokes.ParametricHeatTail.editJet square h K n ν X

noncomputable def NavierStokes.ParametricHeatTail.weightedDebtJet (W : ℝ → ℝ) (square : Bool) (h K q : ℝ) (n : ℕ) (ν : ℝ) : ℝ

Weighted debt jet, given by ∫ X in Ioi K, weightedJet W square h K q n ν X.

Equations

• NavierStokes.ParametricHeatTail.weightedDebtJet W square h K q n ν = ∫ (X : ℝ) in Set.Ioi K, NavierStokes.ParametricHeatTail.weightedJet W square h K q n ν X

theorem NavierStokes.ParametricHeatTail.weightedJet_derivative {W : ℝ → ℝ} {h K q : ℝ} (hh : 0 < h) (hK : 1 ≤ K) (square : Bool) : ∀ᵐ (X : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioi K), ∀ (n : ℕ) (ν : ℝ), 0 ≤ ν → HasDerivWithinAt (fun (u : ℝ) => weightedJet W square h K q n u X) (weightedJet W square h K q (n + 1) ν X) (Set.Ici 0) ν

theorem NavierStokes.ParametricHeatTail.weightedJet_continuousOn {W : ℝ → ℝ} {h K q : ℝ} (hh : 0 < h) (hK : 1 ≤ K) (hW : ContinuousOn W (Set.Ioi K)) (square : Bool) (n : ℕ) {ν : ℝ} (hν : 0 ≤ ν) : ContinuousOn (weightedJet W square h K q n ν) (Set.Ioi K)

theorem NavierStokes.ParametricHeatTail.weightedJet_measurable {W : ℝ → ℝ} {h K q : ℝ} (hh : 0 < h) (hK : 1 ≤ K) (hW : ContinuousOn W (Set.Ioi K)) (square : Bool) (n : ℕ) (ν : ℝ) (hν : 0 ≤ ν) : MeasureTheory.AEStronglyMeasurable (weightedJet W square h K q n ν) (MeasureTheory.volume.restrict (Set.Ioi K))

theorem NavierStokes.ParametricHeatTail.weightedJet_bound {W : ℝ → ℝ} {h K p q B : ℝ} (hh : 0 < h) (hK : 1 ≤ K) (hB : 0 ≤ B) (hweight : ∀ X ∈ Set.Ioi K, |W X| ≤ B * (X / K) ^ p) (square : Bool) (n : ℕ) {L ν X : ℝ} (hν : ν ∈ Set.Icc 0 L) (hX : X ∈ Set.Ioi K) : ‖weightedJet W square h K q n ν X‖ ≤ B * editBound square h L n * HeatTailEdit.weightedKernel K p q X

theorem NavierStokes.ParametricHeatTail.weightedJet_dominated {W : ℝ → ℝ} {h K p q B : ℝ} (hh : 0 < h) (hK : 1 ≤ K) (hB : 0 ≤ B) (hweight : ∀ X ∈ Set.Ioi K, |W X| ≤ B * (X / K) ^ p) (hpq : p + q < 0) (square : Bool) : ChainDominated (weightedJet W square h K q) (MeasureTheory.volume.restrict (Set.Ioi K))

theorem NavierStokes.ParametricHeatTail.weightedDebtJet_bound {W : ℝ → ℝ} {h K p q B : ℝ} (hh : 0 < h) (hK : 1 ≤ K) (hB : 0 ≤ B) (hweight : ∀ X ∈ Set.Ioi K, |W X| ≤ B * (X / K) ^ p) (hpq : p + q < 0) (square : Bool) (n : ℕ) {L ν : ℝ} : 0 < L → ∀ (hν : ν ∈ Set.Icc 0 L), |weightedDebtJet W square h K q n ν| ≤ B * editBound square h L n * K ^ q / (-p - q)

theorem NavierStokes.ParametricHeatTail.weightedJet_integrable {W : ℝ → ℝ} {h K p q B : ℝ} (hh : 0 < h) (hK : 1 ≤ K) (hW : ContinuousOn W (Set.Ioi K)) (hB : 0 ≤ B) (hweight : ∀ X ∈ Set.Ioi K, |W X| ≤ B * (X / K) ^ p) (hpq : p + q < 0) (square : Bool) (n : ℕ) {ν : ℝ} (hν : 0 ≤ ν) : MeasureTheory.IntegrableOn (weightedJet W square h K q n ν) (Set.Ioi K) MeasureTheory.volume

theorem NavierStokes.ParametricHeatTail.weightedDebtJet_derivative {W : ℝ → ℝ} {h K p q B : ℝ} (hh : 0 < h) (hK : 1 ≤ K) (hW : ContinuousOn W (Set.Ioi K)) (hB : 0 ≤ B) (hweight : ∀ X ∈ Set.Ioi K, |W X| ≤ B * (X / K) ^ p) (hpq : p + q < 0) (square : Bool) (n : ℕ) {ν : ℝ} (hν : 0 ≤ ν) : HasDerivWithinAt (weightedDebtJet W square h K q n) (weightedDebtJet W square h K q (n + 1) ν) (Set.Ici 0) ν

theorem NavierStokes.ParametricHeatTail.weightedDebtJet_eq_iteratedDerivWithin {W : ℝ → ℝ} {h K p q B : ℝ} (hh : 0 < h) (hK : 1 ≤ K) (hW : ContinuousOn W (Set.Ioi K)) (hB : 0 ≤ B) (hweight : ∀ X ∈ Set.Ioi K, |W X| ≤ B * (X / K) ^ p) (hpq : p + q < 0) (square : Bool) (n : ℕ) {ν : ℝ} (hν : 0 ≤ ν) : iteratedDerivWithin n (weightedDebtJet W square h K q 0) (Set.Ici 0) ν = weightedDebtJet W square h K q n ν

theorem NavierStokes.ParametricHeatTail.weightedDebt_contDiffOn {W : ℝ → ℝ} {h K p q B : ℝ} (hh : 0 < h) (hK : 1 ≤ K) (hW : ContinuousOn W (Set.Ioi K)) (hB : 0 ≤ B) (hweight : ∀ X ∈ Set.Ioi K, |W X| ≤ B * (X / K) ^ p) (hpq : p + q < 0) (square : Bool) : ContDiffOn ℝ (↑⊤) (weightedDebtJet W square h K q 0) (Set.Ici 0)

The actual outgoing shape and the three physical debts

noncomputable def NavierStokes.ParametricHeatTail.tailWeight (d : OutgoingTail.TailData) (K : ℝ) (square : Bool) (X : ℝ) : ℝ

Tail weight, with branches according to square.

Equations

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

noncomputable def NavierStokes.ParametricHeatTail.tailDecay (d : OutgoingTail.TailData) (square : Bool) : ℝ

Tail decay, with branches according to square.

Equations

• NavierStokes.ParametricHeatTail.tailDecay d square = if square = true then -2 * NavierStokes.HeatTailEdit.exponent d.h else -NavierStokes.HeatTailEdit.exponent d.h

noncomputable def NavierStokes.ParametricHeatTail.tailSize (d : OutgoingTail.TailData) (square : Bool) : ℝ

Tail size, with branches according to square.

Equations

• NavierStokes.ParametricHeatTail.tailSize d square = if square = true then NavierStokes.HeatTailEdit.outgoingAmplitude d ^ 2 else NavierStokes.HeatTailEdit.outgoingAmplitude d

noncomputable def NavierStokes.ParametricHeatTail.nuDebtJet (d : OutgoingTail.TailData) (K : ℝ) (square : Bool) (q : ℝ) (n : ℕ) (ν : ℝ) : ℝ

Nu debt jet, given by weightedDebtJet (tailWeight d K square) square d.h K q n ν.

Equations

• NavierStokes.ParametricHeatTail.nuDebtJet d K square q n ν = NavierStokes.ParametricHeatTail.weightedDebtJet (NavierStokes.ParametricHeatTail.tailWeight d K square) square d.h K q n ν

noncomputable def NavierStokes.ParametricHeatTail.nuConstant (d : OutgoingTail.TailData) (square : Bool) (q : ℝ) (n : ℕ) : ℝ

Nu constant, given by tailSize d square * editBound square d.h 1 n / (-tailDecay d square - q).

Equations

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

theorem NavierStokes.ParametricHeatTail.tailSize_nonneg (d : OutgoingTail.TailData) (square : Bool) : 0 ≤ tailSize d square

theorem NavierStokes.ParametricHeatTail.tailWeight_continuousOn (d : OutgoingTail.TailData) {K : ℝ} (hK : 0 < K) (square : Bool) : ContinuousOn (tailWeight d K square) (Set.Ioi K)

theorem NavierStokes.ParametricHeatTail.tailWeight_bound (d : OutgoingTail.TailData) {K : ℝ} (hK : 0 < K) (square : Bool) (X : ℝ) (hX : X ∈ Set.Ioi K) : |tailWeight d K square X| ≤ tailSize d square * (X / K) ^ tailDecay d square

theorem NavierStokes.ParametricHeatTail.nuConstant_nonneg (d : OutgoingTail.TailData) (square : Bool) {q : ℝ} (hq : tailDecay d square + q < 0) (n : ℕ) : 0 ≤ nuConstant d square q n

theorem NavierStokes.ParametricHeatTail.nuDebtJet_derivative (d : OutgoingTail.TailData) {K : ℝ} (hK : 1 ≤ K) (square : Bool) {q : ℝ} (hq : tailDecay d square + q < 0) (n : ℕ) {ν : ℝ} (hν : 0 ≤ ν) : HasDerivWithinAt (nuDebtJet d K square q n) (nuDebtJet d K square q (n + 1) ν) (Set.Ici 0) ν

theorem NavierStokes.ParametricHeatTail.nuDebt_contDiffOn (d : OutgoingTail.TailData) {K : ℝ} (hK : 1 ≤ K) (square : Bool) {q : ℝ} (hq : tailDecay d square + q < 0) : ContDiffOn ℝ (↑⊤) (nuDebtJet d K square q 0) (Set.Ici 0)

theorem NavierStokes.ParametricHeatTail.nuDebtJet_eq_iteratedDerivWithin (d : OutgoingTail.TailData) {K : ℝ} (hK : 1 ≤ K) (square : Bool) {q : ℝ} (hq : tailDecay d square + q < 0) (n : ℕ) {ν : ℝ} (hν : 0 ≤ ν) : iteratedDerivWithin n (nuDebtJet d K square q 0) (Set.Ici 0) ν = nuDebtJet d K square q n ν

theorem NavierStokes.ParametricHeatTail.nuDebtJet_bound (d : OutgoingTail.TailData) {K : ℝ} (hK : 1 ≤ K) (square : Bool) {q : ℝ} (hq : tailDecay d square + q < 0) (n : ℕ) {ν : ℝ} (hν : ν ∈ Set.Icc 0 1) : |nuDebtJet d K square q n ν| ≤ nuConstant d square q n * K ^ q

noncomputable def NavierStokes.ParametricHeatTail.diffusion (eta : ℝ) : ℝ

Diffusion, given by 1 - eta ^ 2.

Equations

• NavierStokes.ParametricHeatTail.diffusion eta = 1 - eta ^ 2

noncomputable def NavierStokes.ParametricHeatTail.physicalPressure (d : OutgoingTail.TailData) (K eta : ℝ) : ℝ

Physical pressure, given by pressureDebt (outgoingProfile d K eta) d.h (diffusion eta) K.

Equations

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

noncomputable def NavierStokes.ParametricHeatTail.physicalEnergy (d : OutgoingTail.TailData) (K eta : ℝ) : ℝ

Physical energy, given by energyDebt (outgoingProfile d K eta) d.h (diffusion eta) K.

Equations

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

noncomputable def NavierStokes.ParametricHeatTail.physicalAngular (d : OutgoingTail.TailData) (K eta : ℝ) : ℝ

Physical angular, given by angularDebt (outgoingProfile d K eta) d.h (diffusion eta) K.

Equations

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

theorem NavierStokes.ParametricHeatTail.physicalPressure_eq (d : OutgoingTail.TailData) {K : ℝ} (hK : 0 < K) (eta : ℝ) : physicalPressure d K eta = nuDebtJet d K true (-1) 0 (diffusion eta)

theorem NavierStokes.ParametricHeatTail.physicalEnergy_eq (d : OutgoingTail.TailData) {K : ℝ} (hK : 0 < K) (eta : ℝ) : physicalEnergy d K eta = nuDebtJet d K true 0 0 (diffusion eta)

theorem NavierStokes.ParametricHeatTail.physicalAngular_eq (d : OutgoingTail.TailData) {K : ℝ} (hK : 0 < K) (eta : ℝ) : physicalAngular d K eta = √2 * nuDebtJet d K false (1 / 2) 0 (diffusion eta)

Composition with the physical diffusion 1 - eta^2

theorem NavierStokes.ParametricHeatTail.diffusion_contDiff : ContDiff ℝ (↑⊤) diffusion

theorem NavierStokes.ParametricHeatTail.diffusion_mem {eta : ℝ} (hη : eta ∈ Set.Icc (-1) 1) : diffusion eta ∈ Set.Icc 0 1

theorem NavierStokes.ParametricHeatTail.diffusion_hasDerivAt (eta : ℝ) : HasDerivAt diffusion (-2 * eta) eta

theorem NavierStokes.ParametricHeatTail.diffusion_deriv : deriv diffusion = fun (eta : ℝ) => -2 * eta

theorem NavierStokes.ParametricHeatTail.diffusion_second : iteratedDeriv 2 diffusion = fun (x : ℝ) => -2

theorem NavierStokes.ParametricHeatTail.diffusion_higher (n : ℕ) : iteratedDeriv (n + 3) diffusion = fun (x : ℝ) => 0

theorem NavierStokes.ParametricHeatTail.diffusion_jet_bound {eta : ℝ} (hη : eta ∈ Set.Icc (-1) 1) (n : ℕ) (hn : 1 ≤ n) : ‖iteratedFDerivWithin ℝ n diffusion (Set.Icc (-1) 1) eta‖ ≤ 2 ^ n

noncomputable def NavierStokes.ParametricHeatTail.etaDebt (d : OutgoingTail.TailData) (K : ℝ) (square : Bool) (q eta : ℝ) : ℝ

Eta debt, given by nuDebtJet d K square q 0 (diffusion eta).

Equations

• NavierStokes.ParametricHeatTail.etaDebt d K square q eta = NavierStokes.ParametricHeatTail.nuDebtJet d K square q 0 (NavierStokes.ParametricHeatTail.diffusion eta)

noncomputable def NavierStokes.ParametricHeatTail.etaConstant (d : OutgoingTail.TailData) (square : Bool) (q : ℝ) (n : ℕ) : ℝ

Eta constant, given by (n.factorial : ℝ) * (∑ i ∈ Finset.range (n + 1), nuConstant d square q i) * 2 ^ n.

Equations

• NavierStokes.ParametricHeatTail.etaConstant d square q n = (↑n.factorial * ∑ i ∈ Finset.range (n + 1), NavierStokes.ParametricHeatTail.nuConstant d square q i) * 2 ^ n

theorem NavierStokes.ParametricHeatTail.etaConstant_nonneg (d : OutgoingTail.TailData) (square : Bool) {q : ℝ} (hq : tailDecay d square + q < 0) (n : ℕ) : 0 ≤ etaConstant d square q n

theorem NavierStokes.ParametricHeatTail.etaDebt_contDiffOn (d : OutgoingTail.TailData) {K : ℝ} (hK : 1 ≤ K) (square : Bool) {q : ℝ} (hq : tailDecay d square + q < 0) : ContDiffOn ℝ (↑⊤) (etaDebt d K square q) (Set.Icc (-1) 1)

theorem NavierStokes.ParametricHeatTail.etaDebt_hasDerivWithinAt (d : OutgoingTail.TailData) {K : ℝ} (hK : 1 ≤ K) (square : Bool) {q : ℝ} (hq : tailDecay d square + q < 0) {eta : ℝ} (hη : eta ∈ Set.Icc (-1) 1) : HasDerivWithinAt (etaDebt d K square q) (nuDebtJet d K square q 1 (diffusion eta) * (-2 * eta)) (Set.Icc (-1) 1) eta

theorem NavierStokes.ParametricHeatTail.etaDebt_jet_bound (d : OutgoingTail.TailData) {K : ℝ} (hK : 1 ≤ K) (square : Bool) {q : ℝ} (hq : tailDecay d square + q < 0) (n : ℕ) {eta : ℝ} (hη : eta ∈ Set.Icc (-1) 1) : |iteratedDerivWithin n (etaDebt d K square q) (Set.Icc (-1) 1) eta| ≤ etaConstant d square q n * K ^ q

theorem NavierStokes.ParametricHeatTail.pressure_decay (d : OutgoingTail.TailData) : tailDecay d true + -1 < 0

theorem NavierStokes.ParametricHeatTail.energy_decay (d : OutgoingTail.TailData) : tailDecay d true + 0 < 0

theorem NavierStokes.ParametricHeatTail.angular_decay (d : OutgoingTail.TailData) : tailDecay d false + 1 / 2 < 0

theorem NavierStokes.ParametricHeatTail.physicalPressure_contDiffOn (d : OutgoingTail.TailData) {K : ℝ} (hK : 1 ≤ K) : ContDiffOn ℝ (↑⊤) (physicalPressure d K) (Set.Icc (-1) 1)

theorem NavierStokes.ParametricHeatTail.physicalEnergy_contDiffOn (d : OutgoingTail.TailData) {K : ℝ} (hK : 1 ≤ K) : ContDiffOn ℝ (↑⊤) (physicalEnergy d K) (Set.Icc (-1) 1)

theorem NavierStokes.ParametricHeatTail.physicalAngular_contDiffOn (d : OutgoingTail.TailData) {K : ℝ} (hK : 1 ≤ K) : ContDiffOn ℝ (↑⊤) (physicalAngular d K) (Set.Icc (-1) 1)

theorem NavierStokes.ParametricHeatTail.physicalPressure_hasDerivWithinAt (d : OutgoingTail.TailData) {K : ℝ} (hK : 1 ≤ K) {eta : ℝ} (hη : eta ∈ Set.Icc (-1) 1) : HasDerivWithinAt (physicalPressure d K) (nuDebtJet d K true (-1) 1 (diffusion eta) * (-2 * eta)) (Set.Icc (-1) 1) eta

theorem NavierStokes.ParametricHeatTail.physicalEnergy_hasDerivWithinAt (d : OutgoingTail.TailData) {K : ℝ} (hK : 1 ≤ K) {eta : ℝ} (hη : eta ∈ Set.Icc (-1) 1) : HasDerivWithinAt (physicalEnergy d K) (nuDebtJet d K true 0 1 (diffusion eta) * (-2 * eta)) (Set.Icc (-1) 1) eta

theorem NavierStokes.ParametricHeatTail.physicalAngular_hasDerivWithinAt (d : OutgoingTail.TailData) {K : ℝ} (hK : 1 ≤ K) {eta : ℝ} (hη : eta ∈ Set.Icc (-1) 1) : HasDerivWithinAt (physicalAngular d K) (√2 * (nuDebtJet d K false (1 / 2) 1 (diffusion eta) * (-2 * eta))) (Set.Icc (-1) 1) eta

theorem NavierStokes.ParametricHeatTail.physicalPressure_jet_bound (d : OutgoingTail.TailData) {K : ℝ} (hK : 1 ≤ K) (n : ℕ) {eta : ℝ} (hη : eta ∈ Set.Icc (-1) 1) : |iteratedDerivWithin n (physicalPressure d K) (Set.Icc (-1) 1) eta| ≤ etaConstant d true (-1) n / K

theorem NavierStokes.ParametricHeatTail.physicalEnergy_jet_bound (d : OutgoingTail.TailData) {K : ℝ} (hK : 1 ≤ K) (n : ℕ) {eta : ℝ} (hη : eta ∈ Set.Icc (-1) 1) : |iteratedDerivWithin n (physicalEnergy d K) (Set.Icc (-1) 1) eta| ≤ etaConstant d true 0 n

theorem NavierStokes.ParametricHeatTail.physicalAngular_jet_bound (d : OutgoingTail.TailData) {K : ℝ} (hK : 1 ≤ K) (n : ℕ) {eta : ℝ} (hη : eta ∈ Set.Icc (-1) 1) : |iteratedDerivWithin n (physicalAngular d K) (Set.Icc (-1) 1) eta| ≤ √2 * etaConstant d false (1 / 2) n * √K

theorem NavierStokes.ParametricHeatTail.exists_physical_debt_jet_bounds (d : OutgoingTail.TailData) (n : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (K : ℝ), 1 ≤ K → ∀ eta ∈ Set.Icc (-1) 1, |iteratedDerivWithin n (physicalPressure d K) (Set.Icc (-1) 1) eta| ≤ C / K ∧ |iteratedDerivWithin n (physicalEnergy d K) (Set.Icc (-1) 1) eta| ≤ C ∧ |iteratedDerivWithin n (physicalAngular d K) (Set.Icc (-1) 1) eta| ≤ C * √K

Every fixed genuine eta jet has the manuscript's three unnormalized scales.

theorem NavierStokes.ParametricHeatTail.exists_physical_debt_C1_bounds (d : OutgoingTail.TailData) : ∃ (C : ℝ), 0 < C ∧ ∀ (K : ℝ), 1 ≤ K → ∀ eta ∈ Set.Icc (-1) 1, |physicalPressure d K eta| ≤ C / K ∧ |derivWithin (physicalPressure d K) (Set.Icc (-1) 1) eta| ≤ C / K ∧ |physicalEnergy d K eta| ≤ C ∧ |derivWithin (physicalEnergy d K) (Set.Icc (-1) 1) eta| ≤ C ∧ |physicalAngular d K eta| ≤ C * √K ∧ |derivWithin (physicalAngular d K) (Set.Icc (-1) 1) eta| ≤ C * √K

A single constant controls values and actual first within derivatives. This is the scalar input to the variable-debt nonlinear compensation theorem.

Endpoint jets and the velocity in physical units

theorem NavierStokes.ParametricHeatTail.correctionJet_eq_iteratedDerivWithin {h K X ν : ℝ} (hh : 0 < h) (hX : 0 < X) (hν : 0 ≤ ν) (n : ℕ) : iteratedDerivWithin n (fun (u : ℝ) => HeatTailEdit.multiplier h u K X - 1) (Set.Ici 0) ν = correctionJet h K n ν X

theorem NavierStokes.ParametricHeatTail.multiplier_nu_contDiffOn {h K X : ℝ} (hh : 0 < h) (hX : 0 < X) : ContDiffOn ℝ (↑⊤) (fun (ν : ℝ) => HeatTailEdit.multiplier h ν K X) (Set.Ici 0)

theorem NavierStokes.ParametricHeatTail.multiplier_nu_jet {h K X ν : ℝ} (hh : 0 < h) (hX : 0 < X) (hν : 0 ≤ ν) (n : ℕ) : iteratedDerivWithin (n + 1) (fun (u : ℝ) => HeatTailEdit.multiplier h u K X) (Set.Ici 0) ν = correctionJet h K (n + 1) ν X

theorem NavierStokes.ParametricHeatTail.multiplier_nu_jet_bound {h K X ν : ℝ} (hh : 0 < h) (hX : 1 ≤ X) (hν : ν ∈ Set.Icc 0 1) (n : ℕ) : |iteratedDerivWithin (n + 1) (fun (u : ℝ) => HeatTailEdit.multiplier h u K X) (Set.Ici 0) ν| ≤ correctionBound h 1 (n + 1) / X

theorem NavierStokes.ParametricHeatTail.multiplier_zero {h : ℝ} (hh : 0 < h) (K X : ℝ) : HeatTailEdit.multiplier h 0 K X = 1

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

theorem NavierStokes.ParametricHeatTail.physical_debts_integrable (d : OutgoingTail.TailData) {K eta : ℝ} (hK : 0 < K) (hη : eta ∈ Set.Icc (-1) 1) : MeasureTheory.IntegrableOn (fun (X : ℝ) => HeatTailEdit.squareChange (HeatTailEdit.outgoingProfile d K eta) d.h (diffusion eta) K X / X) (Set.Ioi K) MeasureTheory.volume ∧ MeasureTheory.IntegrableOn (HeatTailEdit.squareChange (HeatTailEdit.outgoingProfile d K eta) d.h (diffusion eta) K) (Set.Ioi K) MeasureTheory.volume ∧ MeasureTheory.IntegrableOn (fun (X : ℝ) => √(2 * X) * HeatTailEdit.change (HeatTailEdit.outgoingProfile d K eta) d.h (diffusion eta) K X) (Set.Ioi K) MeasureTheory.volume

theorem NavierStokes.ParametricHeatTail.physical_debts_zero (d : OutgoingTail.TailData) (K : ℝ) {eta : ℝ} (hη : diffusion eta = 0) : physicalPressure d K eta = 0 ∧ physicalEnergy d K eta = 0 ∧ physicalAngular d K eta = 0

noncomputable def NavierStokes.ParametricHeatTail.physicalEdit (d : OutgoingTail.TailData) (K eta X : ℝ) : ℝ

Physical edit, given by outgoingEdit d (diffusion eta) K eta X.

Equations

• NavierStokes.ParametricHeatTail.physicalEdit d K eta X = NavierStokes.HeatTailEdit.outgoingEdit d (NavierStokes.ParametricHeatTail.diffusion eta) K eta X

theorem NavierStokes.ParametricHeatTail.physicalEdit_pos (d : OutgoingTail.TailData) (K : ℝ) {eta X : ℝ} (hη : eta ∈ Set.Icc (-1) 1) (hX : 0 < X) : 0 < physicalEdit d K eta X

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

theorem NavierStokes.ParametricHeatTail.physicalEdit_joint_contDiffOn (d : OutgoingTail.TailData) {K : ℝ} (hK : 0 < K) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × ℝ) => physicalEdit d K p.2 p.1) (Set.Ioi 0 ×ˢ Set.Icc (-1) 1)

theorem NavierStokes.ParametricHeatTail.diffusion_of_physical_coordinates {q τ z : ℝ} (hq : 0 < q) (hrel : q = τ + z ^ 2) : diffusion (z / √q) = τ / q

theorem NavierStokes.ParametricHeatTail.heat_ratio_physical {q s τ : ℝ} (hq : 0 < q) (hs : 0 < s) : 2 * (τ / q) / (s / q) = 2 * τ / s

theorem NavierStokes.ParametricHeatTail.physicalEdit_heat_carrier (d : OutgoingTail.TailData) {K q s τ eta : ℝ} (hK : 0 < K) (hq : 0 < q) (hs : 0 < s) (hν : diffusion eta = τ / q) (hfull : 1 / 2 ≤ Real.log (s / q / K) + 1 / 5) : q ^ (-HeatTailEdit.exponent d.h) * physicalEdit d K eta (s / q) = HeatTailEdit.outgoingAmplitude d * K ^ HeatTailEdit.exponent d.h * RadialHeatProfile.spatialProfile (1 + d.h) τ s * OutgoingTail.tailShape d (Real.log (s / q / K) + 1 / 5)

The similarity prefactor cancels all powers of q. The carrier is exactly a constant times s^(-A) H(2 tau / s).

theorem NavierStokes.ParametricHeatTail.physicalEdit_eventual_heat_carrier (d : OutgoingTail.TailData) {K q s τ eta : ℝ} (hK : 0 < K) (hq : 0 < q) (hs : 0 < s) (hν : diffusion eta = τ / q) (hlate : 3 ≤ Real.log (s / q / K) + 1 / 5) : q ^ (-HeatTailEdit.exponent d.h) * physicalEdit d K eta (s / q) = HeatTailEdit.outgoingAmplitude d * K ^ HeatTailEdit.exponent d.h * RadialHeatProfile.spatialProfile (1 + d.h) τ s

The eta derivatives are not identically zero. In particular, the actual one-sided angular derivative at the physical endpoint eta = 1 is positive.

theorem NavierStokes.ParametricHeatTail.switch_pos {K X : ℝ} (hK : 0 < K) (hX : K < X) : 0 < HeatTailEdit.switch K X

theorem NavierStokes.ParametricHeatTail.profile_first_jet_neg {h z : ℝ} (hh : 0 < h) (hz : 0 ≤ z) : RadialHeatProfile.profileJet (1 + h) 1 z < 0

theorem NavierStokes.ParametricHeatTail.nuDebt_linear_first_neg (d : OutgoingTail.TailData) {K : ℝ} (hK : 1 ≤ K) {q : ℝ} (hq : tailDecay d false + q < 0) {ν : ℝ} (hν : 0 ≤ ν) : nuDebtJet d K false q 1 ν < 0

theorem NavierStokes.ParametricHeatTail.physicalAngular_endpoint_derivative_pos (d : OutgoingTail.TailData) {K : ℝ} (hK : 1 ≤ K) : 0 < derivWithin (physicalAngular d K) (Set.Icc (-1) 1) 1