Literal heat debts on an open physical parameter domain

Negative diffusion uses the constructed smooth heat-profile extension. The three debts remain the actual improper integrals of the edited outgoing profile. All differentiated kernels and their integrable majorants are derived from that extension.

Dominated derivative chains on the entire real parameter line

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

Chain dominated, given by ∀ n L, 0 < L → ∃ b : α → ℝ, Integrable b μ ∧ ∀ᵐ t ∂μ, ∀ ν : ℝ, |ν| ≤ L → ‖J n ν t‖ ≤ b t.

Equations

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

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

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

theorem NavierStokes.ExtendedHeatDebts.iteratedDeriv_integral_chain {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {J : ℕ → ℝ → α → ℝ} (hJ : ∀ᵐ (t : α) ∂μ, ∀ (n : ℕ) (ν : ℝ), HasDerivAt (fun (u : ℝ) => J n u t) (J (n + 1) ν t) ν) (hm : ∀ (n : ℕ) (ν : ℝ), MeasureTheory.AEStronglyMeasurable (J n ν) μ) (hb : ChainDominated J μ) (n : ℕ) (ν : ℝ) : iteratedDeriv n (fun (u : ℝ) => ∫ (t : α), J 0 u t ∂μ) ν = ∫ (t : α), J n ν t ∂μ

theorem NavierStokes.ExtendedHeatDebts.contDiff_integral_chain {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {J : ℕ → ℝ → α → ℝ} (hJ : ∀ᵐ (t : α) ∂μ, ∀ (n : ℕ) (ν : ℝ), HasDerivAt (fun (u : ℝ) => J n u t) (J (n + 1) ν t) ν) (hm : ∀ (n : ℕ) (ν : ℝ), MeasureTheory.AEStronglyMeasurable (J n ν) μ) (hb : ChainDominated J μ) : ContDiff ℝ ↑⊤ fun (u : ℝ) => ∫ (t : α), J 0 u t ∂μ

The actual extended edit and all its diffusion derivatives

noncomputable def NavierStokes.ExtendedHeatDebts.correction (h K ν X : ℝ) : ℝ

Correction, given by switch K X * (HeatProfileExtension.scaledProfile (1 + h) X ν - 1).

Equations

• NavierStokes.ExtendedHeatDebts.correction h K ν X = NavierStokes.HeatTailEdit.switch K X * (NavierStokes.HeatProfileExtension.scaledProfile (1 + h) X ν - 1)

noncomputable def NavierStokes.ExtendedHeatDebts.multiplier (h ν K X : ℝ) : ℝ

Multiplier, given by 1 + correction h K ν X.

Equations

• NavierStokes.ExtendedHeatDebts.multiplier h ν K X = 1 + NavierStokes.ExtendedHeatDebts.correction h K ν X

noncomputable def NavierStokes.ExtendedHeatDebts.edit (E : ℝ → ℝ) (h ν K X : ℝ) : ℝ

Edit, given by E X * multiplier h ν K X.

Equations

• NavierStokes.ExtendedHeatDebts.edit E h ν K X = E X * NavierStokes.ExtendedHeatDebts.multiplier h ν K X

noncomputable def NavierStokes.ExtendedHeatDebts.change (E : ℝ → ℝ) (h ν K X : ℝ) : ℝ

Change, given by edit E h ν K X - E X.

Equations

• NavierStokes.ExtendedHeatDebts.change E h ν K X = NavierStokes.ExtendedHeatDebts.edit E h ν K X - E X

noncomputable def NavierStokes.ExtendedHeatDebts.squareChange (E : ℝ → ℝ) (h ν K X : ℝ) : ℝ

Square change, given by edit E h ν K X ^ 2 - E X ^ 2.

Equations

• NavierStokes.ExtendedHeatDebts.squareChange E h ν K X = NavierStokes.ExtendedHeatDebts.edit E h ν K X ^ 2 - E X ^ 2

noncomputable def NavierStokes.ExtendedHeatDebts.correctionJet (h K : ℝ) (n : ℕ) (ν X : ℝ) : ℝ

Correction jet, given by iteratedDeriv n (fun u => correction h K u X) ν.

Equations

• NavierStokes.ExtendedHeatDebts.correctionJet h K n ν X = iteratedDeriv n (fun (u : ℝ) => NavierStokes.ExtendedHeatDebts.correction h K u X) ν

noncomputable def NavierStokes.ExtendedHeatDebts.correctionBound (h L : ℝ) (n : ℕ) : ℝ

Correction bound, with branches according to n = 0.

Equations

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

theorem NavierStokes.ExtendedHeatDebts.correctionBound_zero (h L : ℝ) : correctionBound h L 0 = 2 * HeatProfileExtension.derivativeBound (1 + h) 1 * L

theorem NavierStokes.ExtendedHeatDebts.correctionBound_succ (h L : ℝ) (n : ℕ) : correctionBound h L (n + 1) = 2 ^ (n + 1) * HeatProfileExtension.derivativeBound (1 + h) (n + 1)

theorem NavierStokes.ExtendedHeatDebts.correction_contDiff {h : ℝ} (hh : 0 < h) (K X : ℝ) : ContDiff ℝ ↑⊤ fun (ν : ℝ) => correction h K ν X

theorem NavierStokes.ExtendedHeatDebts.correctionJet_hasDerivAt {h : ℝ} (hh : 0 < h) (K X : ℝ) (n : ℕ) (ν : ℝ) : HasDerivAt (fun (u : ℝ) => correctionJet h K n u X) (correctionJet h K (n + 1) ν X) ν

theorem NavierStokes.ExtendedHeatDebts.correctionJet_zero (h K ν X : ℝ) : correctionJet h K 0 ν X = correction h K ν X

theorem NavierStokes.ExtendedHeatDebts.correctionJet_succ {h : ℝ} (hh : 0 < h) (K X ν : ℝ) (n : ℕ) : correctionJet h K (n + 1) ν X = HeatTailEdit.switch K X * (2 / X) ^ (n + 1) * iteratedDeriv (n + 1) (HeatProfileExtension.extension (1 + h)) (2 * ν / X)

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

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

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

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

Square correction jet, given by 2 * correctionJet h K n ν X + jetProduct (fun i => correctionJet h K i ν X) (fun i => correctionJet h K i ν X) n.

Equations

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

noncomputable def NavierStokes.ExtendedHeatDebts.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.ExtendedHeatDebts.squareCorrectionJet_zero (h K ν X : ℝ) : squareCorrectionJet h K 0 ν X = multiplier h ν K X ^ 2 - 1

theorem NavierStokes.ExtendedHeatDebts.squareCorrectionJet_hasDerivAt {h : ℝ} (hh : 0 < h) (K X : ℝ) (n : ℕ) (ν : ℝ) : HasDerivAt (fun (u : ℝ) => squareCorrectionJet h K n u X) (squareCorrectionJet h K (n + 1) ν X) ν

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

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

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

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

Edit jet, with branches according to square.

Equations

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

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

Edit bound, with branches according to square.

Equations

• NavierStokes.ExtendedHeatDebts.editBound square h L n = if square = true then NavierStokes.ExtendedHeatDebts.squareCorrectionBound h L n else NavierStokes.ExtendedHeatDebts.correctionBound h L n

theorem NavierStokes.ExtendedHeatDebts.editJet_hasDerivAt {h : ℝ} (hh : 0 < h) (K X : ℝ) (square : Bool) (n : ℕ) (ν : ℝ) : HasDerivAt (fun (u : ℝ) => editJet square h K n u X) (editJet square h K (n + 1) ν X) ν

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

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

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

Literal weighted improper integrals

noncomputable def NavierStokes.ExtendedHeatDebts.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.ExtendedHeatDebts.weightedJet W square h K q n ν X = X ^ q * W X * NavierStokes.ExtendedHeatDebts.editJet square h K n ν X

noncomputable def NavierStokes.ExtendedHeatDebts.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.ExtendedHeatDebts.weightedDebtJet W square h K q n ν = ∫ (X : ℝ) in Set.Ioi K, NavierStokes.ExtendedHeatDebts.weightedJet W square h K q n ν X

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

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

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

theorem NavierStokes.ExtendedHeatDebts.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ν : |ν| ≤ 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.ExtendedHeatDebts.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.ExtendedHeatDebts.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 ν : ℝ} (hν : |ν| ≤ L) : |weightedDebtJet W square h K q n ν| ≤ B * editBound square h L n * K ^ q / (-p - q)

theorem NavierStokes.ExtendedHeatDebts.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 : ℕ) (ν : ℝ) : MeasureTheory.IntegrableOn (weightedJet W square h K q n ν) (Set.Ioi K) MeasureTheory.volume

theorem NavierStokes.ExtendedHeatDebts.weightedDebtJet_hasDerivAt {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 : ℕ) (ν : ℝ) : HasDerivAt (weightedDebtJet W square h K q n) (weightedDebtJet W square h K q (n + 1) ν) ν

theorem NavierStokes.ExtendedHeatDebts.weightedDebtJet_eq_iteratedDeriv {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 : ℕ) (ν : ℝ) : iteratedDeriv n (weightedDebtJet W square h K q 0) ν = weightedDebtJet W square h K q n ν

theorem NavierStokes.ExtendedHeatDebts.weightedDebt_contDiff {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) : ContDiff ℝ (↑⊤) (weightedDebtJet W square h K q 0)

Specialization to the actual outgoing profile

noncomputable def NavierStokes.ExtendedHeatDebts.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.ExtendedHeatDebts.nuDebtJet d K square q n ν = NavierStokes.ExtendedHeatDebts.weightedDebtJet (NavierStokes.ParametricHeatTail.tailWeight d K square) square d.h K q n ν

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

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

Equations

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

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

theorem NavierStokes.ExtendedHeatDebts.nuDebtJet_hasDerivAt (d : OutgoingTail.TailData) {K : ℝ} (hK : 1 ≤ K) (square : Bool) {q : ℝ} (hq : ParametricHeatTail.tailDecay d square + q < 0) (n : ℕ) (ν : ℝ) : HasDerivAt (nuDebtJet d K square q n) (nuDebtJet d K square q (n + 1) ν) ν

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

theorem NavierStokes.ExtendedHeatDebts.nuDebtJet_eq_iteratedDeriv (d : OutgoingTail.TailData) {K : ℝ} (hK : 1 ≤ K) (square : Bool) {q : ℝ} (hq : ParametricHeatTail.tailDecay d square + q < 0) (n : ℕ) (ν : ℝ) : iteratedDeriv n (nuDebtJet d K square q 0) ν = nuDebtJet d K square q n ν

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

noncomputable def NavierStokes.ExtendedHeatDebts.physicalEdit (d : OutgoingTail.TailData) (K η X : ℝ) : ℝ

The literal extended outgoing edit.

Equations

• NavierStokes.ExtendedHeatDebts.physicalEdit d K η X = NavierStokes.ExtendedHeatDebts.edit (NavierStokes.HeatTailEdit.outgoingProfile d K η) d.h (NavierStokes.ParametricHeatTail.diffusion η) K X

noncomputable def NavierStokes.ExtendedHeatDebts.physicalPressure (d : OutgoingTail.TailData) (K η : ℝ) : ℝ

Physical pressure, given by ∫ X in Ioi K, squareChange (outgoingProfile d K η) d.h (diffusion η) K X / X.

Equations

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

noncomputable def NavierStokes.ExtendedHeatDebts.physicalEnergy (d : OutgoingTail.TailData) (K η : ℝ) : ℝ

Physical energy, given by ∫ X in Ioi K, squareChange (outgoingProfile d K η) d.h (diffusion η) K X.

Equations

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

noncomputable def NavierStokes.ExtendedHeatDebts.physicalAngular (d : OutgoingTail.TailData) (K η : ℝ) : ℝ

Physical angular, given by ∫ X in Ioi K, Real.sqrt (2 * X) * change (outgoingProfile d K η) d.h (diffusion η) K X.

Equations

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

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

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

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

theorem NavierStokes.ExtendedHeatDebts.multiplier_eq_original (h : ℝ) {ν K X : ℝ} (hν : 0 ≤ ν) (hX : 0 < X) : multiplier h ν K X = HeatTailEdit.multiplier h ν K X

theorem NavierStokes.ExtendedHeatDebts.edit_eq_original (E : ℝ → ℝ) (h : ℝ) {ν K X : ℝ} (hν : 0 ≤ ν) (hX : 0 < X) : edit E h ν K X = HeatTailEdit.edit E h ν K X

theorem NavierStokes.ExtendedHeatDebts.physicalPressure_eq_original (d : OutgoingTail.TailData) {K η : ℝ} (hK : 0 < K) (hη : η ∈ Set.Icc (-1) 1) : physicalPressure d K η = ParametricHeatTail.physicalPressure d K η

theorem NavierStokes.ExtendedHeatDebts.physicalEnergy_eq_original (d : OutgoingTail.TailData) {K η : ℝ} (hK : 0 < K) (hη : η ∈ Set.Icc (-1) 1) : physicalEnergy d K η = ParametricHeatTail.physicalEnergy d K η

theorem NavierStokes.ExtendedHeatDebts.physicalAngular_eq_original (d : OutgoingTail.TailData) {K η : ℝ} (hK : 0 < K) (hη : η ∈ Set.Icc (-1) 1) : physicalAngular d K η = ParametricHeatTail.physicalAngular d K η

Exact radius rescaling and joint smoothness

theorem NavierStokes.ExtendedHeatDebts.correction_scale (h ν : ℝ) {K : ℝ} (hK : K ≠ 0) (X : ℝ) : correction h K ν (K * X) = correction h 1 (ν / K) X

theorem NavierStokes.ExtendedHeatDebts.tailWeight_scale (d : OutgoingTail.TailData) {K : ℝ} (hK : K ≠ 0) (square : Bool) (X : ℝ) : ParametricHeatTail.tailWeight d K square (K * X) = ParametricHeatTail.tailWeight d 1 square X

theorem NavierStokes.ExtendedHeatDebts.editJet_scale_zero (h ν : ℝ) {K : ℝ} (hK : K ≠ 0) (square : Bool) (X : ℝ) : editJet square h K 0 ν (K * X) = editJet square h 1 0 (ν / K) X

theorem NavierStokes.ExtendedHeatDebts.weightedJet_scale_zero (d : OutgoingTail.TailData) {K : ℝ} (hK : 0 < K) (square : Bool) (q ν : ℝ) {X : ℝ} (hX : 0 ≤ X) : weightedJet (ParametricHeatTail.tailWeight d K square) square d.h K q 0 ν (K * X) = K ^ q * weightedJet (ParametricHeatTail.tailWeight d 1 square) square d.h 1 q 0 (ν / K) X

theorem NavierStokes.ExtendedHeatDebts.nuDebt_scale (d : OutgoingTail.TailData) {K : ℝ} (hK : 0 < K) (square : Bool) (q ν : ℝ) : nuDebtJet d K square q 0 ν = K ^ (q + 1) * nuDebtJet d 1 square q 0 (ν / K)

A genuine change of variables in the improper integral gives all radius dependence through an explicit power and the rescaled diffusion.

theorem NavierStokes.ExtendedHeatDebts.nuDebt_joint_contDiffOn (d : OutgoingTail.TailData) (square : Bool) {q : ℝ} (hq : ParametricHeatTail.tailDecay d square + q < 0) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × ℝ) => nuDebtJet d p.1 square q 0 p.2) (Set.Ioi 0 ×ˢ Set.univ)

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

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

Equations

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

theorem NavierStokes.ExtendedHeatDebts.etaDebt_contDiff (d : OutgoingTail.TailData) {K : ℝ} (hK : 1 ≤ K) (square : Bool) {q : ℝ} (hq : ParametricHeatTail.tailDecay d square + q < 0) : ContDiff ℝ (↑⊤) (etaDebt d K square q)

theorem NavierStokes.ExtendedHeatDebts.etaDebt_hasDerivAt (d : OutgoingTail.TailData) {K : ℝ} (hK : 1 ≤ K) (square : Bool) {q : ℝ} (hq : ParametricHeatTail.tailDecay d square + q < 0) (η : ℝ) : HasDerivAt (etaDebt d K square q) (nuDebtJet d K square q 1 (ParametricHeatTail.diffusion η) * (-2 * η)) η

theorem NavierStokes.ExtendedHeatDebts.etaDebt_joint_contDiffOn (d : OutgoingTail.TailData) (square : Bool) {q : ℝ} (hq : ParametricHeatTail.tailDecay d square + q < 0) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × ℝ) => etaDebt d p.1 square q p.2) (Set.Ioi 0 ×ˢ Set.univ)

theorem NavierStokes.ExtendedHeatDebts.physicalPressure_joint_contDiffOn (d : OutgoingTail.TailData) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × ℝ) => physicalPressure d p.1 p.2) (Set.Ioi 0 ×ˢ Set.univ)

theorem NavierStokes.ExtendedHeatDebts.physicalEnergy_joint_contDiffOn (d : OutgoingTail.TailData) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × ℝ) => physicalEnergy d p.1 p.2) (Set.Ioi 0 ×ˢ Set.univ)

theorem NavierStokes.ExtendedHeatDebts.physicalAngular_joint_contDiffOn (d : OutgoingTail.TailData) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × ℝ) => physicalAngular d p.1 p.2) (Set.Ioi 0 ×ˢ Set.univ)

Uniform estimates on a fixed enlarged physical band

noncomputable def NavierStokes.ExtendedHeatDebts.enlargedBand : Set ℝ

Enlarged band, given by Icc (-(3 / 2 : ℝ)) (3 / 2).

Equations

• NavierStokes.ExtendedHeatDebts.enlargedBand = Set.Icc (-(3 / 2)) (3 / 2)

theorem NavierStokes.ExtendedHeatDebts.physicalBand_subset_enlargedBand : Set.Icc (-1) 1 ⊆ enlargedBand

theorem NavierStokes.ExtendedHeatDebts.enlargedBand_diffusion_bound {η : ℝ} (hη : η ∈ enlargedBand) : |ParametricHeatTail.diffusion η| ≤ 3

theorem NavierStokes.ExtendedHeatDebts.enlargedBand_diffusion_derivative_bound {η : ℝ} (hη : η ∈ enlargedBand) (n : ℕ) (hn : 1 ≤ n) : ‖iteratedFDeriv ℝ n ParametricHeatTail.diffusion η‖ ≤ 3 ^ n

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

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

Equations

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

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

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

theorem NavierStokes.ExtendedHeatDebts.physicalPressure_contDiff (d : OutgoingTail.TailData) {K : ℝ} (hK : 1 ≤ K) : ContDiff ℝ (↑⊤) (physicalPressure d K)

theorem NavierStokes.ExtendedHeatDebts.physicalEnergy_contDiff (d : OutgoingTail.TailData) {K : ℝ} (hK : 1 ≤ K) : ContDiff ℝ (↑⊤) (physicalEnergy d K)

theorem NavierStokes.ExtendedHeatDebts.physicalAngular_contDiff (d : OutgoingTail.TailData) {K : ℝ} (hK : 1 ≤ K) : ContDiff ℝ (↑⊤) (physicalAngular d K)

theorem NavierStokes.ExtendedHeatDebts.physicalPressure_jet_bound (d : OutgoingTail.TailData) {K : ℝ} (hK : 1 ≤ K) (n : ℕ) {η : ℝ} (hη : η ∈ enlargedBand) : |iteratedDeriv n (physicalPressure d K) η| ≤ etaConstant d true (-1) n / K

theorem NavierStokes.ExtendedHeatDebts.physicalEnergy_jet_bound (d : OutgoingTail.TailData) {K : ℝ} (hK : 1 ≤ K) (n : ℕ) {η : ℝ} (hη : η ∈ enlargedBand) : |iteratedDeriv n (physicalEnergy d K) η| ≤ etaConstant d true 0 n

theorem NavierStokes.ExtendedHeatDebts.physicalAngular_jet_bound (d : OutgoingTail.TailData) {K : ℝ} (hK : 1 ≤ K) (n : ℕ) {η : ℝ} (hη : η ∈ enlargedBand) : |iteratedDeriv n (physicalAngular d K) η| ≤ √2 * etaConstant d false (1 / 2) n * √K

theorem NavierStokes.ExtendedHeatDebts.exists_physical_debt_jet_bounds (d : OutgoingTail.TailData) (n : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (K : ℝ), 1 ≤ K → ∀ η ∈ enlargedBand, |iteratedDeriv n (physicalPressure d K) η| ≤ C / K ∧ |iteratedDeriv n (physicalEnergy d K) η| ≤ C ∧ |iteratedDeriv n (physicalAngular d K) η| ≤ C * √K

theorem NavierStokes.ExtendedHeatDebts.exists_physical_debt_C1_bounds (d : OutgoingTail.TailData) : ∃ (C : ℝ), 0 < C ∧ ∀ (K : ℝ), 1 ≤ K → ∀ η ∈ enlargedBand, |physicalPressure d K η| ≤ C / K ∧ |deriv (physicalPressure d K) η| ≤ C / K ∧ |physicalEnergy d K η| ≤ C ∧ |deriv (physicalEnergy d K) η| ≤ C ∧ |physicalAngular d K η| ≤ C * √K ∧ |deriv (physicalAngular d K) η| ≤ C * √K

noncomputable def NavierStokes.ExtendedHeatDebts.physicalDebt (d : OutgoingTail.TailData) (K η : ℝ) : TerminalCompensation.Coeff

Physical debt, given by ![physicalPressure d K η, physicalEnergy d K η, physicalAngular d K η].

Equations

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

noncomputable def NavierStokes.ExtendedHeatDebts.normalizedDebt (d : OutgoingTail.TailData) (K η : ℝ) : TerminalCompensation.Coeff

Normalized debt, given by TerminalCompensation.scaledDebt K (physicalDebt d K η).

Equations

• NavierStokes.ExtendedHeatDebts.normalizedDebt d K η = NavierStokes.TerminalCompensation.scaledDebt K (NavierStokes.ExtendedHeatDebts.physicalDebt d K η)

theorem NavierStokes.ExtendedHeatDebts.normalizedDebt_contDiff (d : OutgoingTail.TailData) {K : ℝ} (hK : 1 ≤ K) : ContDiff ℝ (↑⊤) (normalizedDebt d K)

theorem NavierStokes.ExtendedHeatDebts.normalizedDebt_deriv (d : OutgoingTail.TailData) {K : ℝ} (hK : 1 ≤ K) (η : ℝ) : deriv (normalizedDebt d K) η = TerminalCompensation.scaledDebt K ![deriv (physicalPressure d K) η, deriv (physicalEnergy d K) η, deriv (physicalAngular d K) η]

theorem NavierStokes.ExtendedHeatDebts.exists_normalized_C1_bounds (d : OutgoingTail.TailData) : ∃ (C : ℝ), 0 < C ∧ ∀ (K : ℝ), 1 ≤ K → ∀ η ∈ enlargedBand, ‖normalizedDebt d K η‖ ≤ C / K ∧ ‖deriv (normalizedDebt d K) η‖ ≤ C / K

The exact normalized vector has the same uniform C1 inverse-radius cost on the enlarged compact band, using ordinary derivatives everywhere.

theorem NavierStokes.ExtendedHeatDebts.eventually_physicalEdit_pos (d : OutgoingTail.TailData) : ∃ (K₀ : ℝ), 0 < K₀ ∧ ∀ (K : ℝ), K₀ ≤ K → ∀ η ∈ enlargedBand, ∀ (X : ℝ), 0 < X → 0 < physicalEdit d K η X

The extended physical edit remains strictly positive throughout the enlarged band once the switch radius is sufficiently large.

Every actual physical-parameter derivative passes under the integral

theorem NavierStokes.ExtendedHeatDebts.partial_iteratedDeriv_contDiffOn {F : ℝ × ℝ → ℝ} {K : ℝ} (hF : ContDiffOn ℝ (↑⊤) F (Set.univ ×ˢ Set.Ioi K)) (n : ℕ) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × ℝ) => iteratedDeriv n (fun (η : ℝ) => F (η, p.2)) p.1) (Set.univ ×ˢ Set.Ioi K)

theorem NavierStokes.ExtendedHeatDebts.editJet_zero_contDiff {h : ℝ} (hh : 0 < h) (K X : ℝ) (square : Bool) : ContDiff ℝ ↑⊤ fun (ν : ℝ) => editJet square h K 0 ν X

theorem NavierStokes.ExtendedHeatDebts.iteratedDeriv_weightedJet {h : ℝ} (hh : 0 < h) (W : ℝ → ℝ) (K q X : ℝ) (square : Bool) (n : ℕ) (ν : ℝ) : iteratedDeriv n (fun (u : ℝ) => weightedJet W square h K q 0 u X) ν = weightedJet W square h K q n ν X

theorem NavierStokes.ExtendedHeatDebts.weightedJet_zero_contDiff {h : ℝ} (hh : 0 < h) (W : ℝ → ℝ) (K q X : ℝ) (square : Bool) : ContDiff ℝ ↑⊤ fun (ν : ℝ) => weightedJet W square h K q 0 ν X

theorem NavierStokes.ExtendedHeatDebts.actualIntegrand_joint_contDiffOn (d : OutgoingTail.TailData) {K : ℝ} (hK : 1 ≤ K) (square : Bool) (q : ℝ) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × ℝ) => weightedJet (ParametricHeatTail.tailWeight d K square) square d.h K q 0 (ParametricHeatTail.diffusion p.1) p.2) (Set.univ ×ˢ Set.Ioi K)

noncomputable def NavierStokes.ExtendedHeatDebts.etaIntegrandJet (d : OutgoingTail.TailData) (K : ℝ) (square : Bool) (q : ℝ) (n : ℕ) (η X : ℝ) : ℝ

Eta integrand jet, given by iteratedDeriv n (fun θ => weightedJet (tailWeight d K square) square d.h K q 0 (diffusion θ) X) η.

Equations

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

theorem NavierStokes.ExtendedHeatDebts.etaIntegrandJet_measurable (d : OutgoingTail.TailData) {K : ℝ} (hK : 1 ≤ K) (square : Bool) (q : ℝ) (n : ℕ) (η : ℝ) : MeasureTheory.AEStronglyMeasurable (etaIntegrandJet d K square q n η) (MeasureTheory.volume.restrict (Set.Ioi K))

theorem NavierStokes.ExtendedHeatDebts.diffusion_abs_bound {L η : ℝ} (hη : |η| ≤ L) : |ParametricHeatTail.diffusion η| ≤ 1 + L ^ 2

theorem NavierStokes.ExtendedHeatDebts.diffusion_iterated_bound {L η : ℝ} (hL : 0 ≤ L) (hη : |η| ≤ L) (n : ℕ) (hn : 1 ≤ n) : ‖iteratedFDeriv ℝ n ParametricHeatTail.diffusion η‖ ≤ (2 * (L + 1)) ^ n

theorem NavierStokes.ExtendedHeatDebts.etaIntegrandJet_dominated (d : OutgoingTail.TailData) {K : ℝ} (hK : 1 ≤ K) (square : Bool) {q : ℝ} (hq : ParametricHeatTail.tailDecay d square + q < 0) : ChainDominated (etaIntegrandJet d K square q) (MeasureTheory.volume.restrict (Set.Ioi K))

theorem NavierStokes.ExtendedHeatDebts.etaIntegrandJet_derivative (d : OutgoingTail.TailData) (K : ℝ) (square : Bool) (q : ℝ) : ∀ᵐ (X : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioi K), ∀ (n : ℕ) (η : ℝ), HasDerivAt (fun (θ : ℝ) => etaIntegrandJet d K square q n θ X) (etaIntegrandJet d K square q (n + 1) η X) η

theorem NavierStokes.ExtendedHeatDebts.etaIntegrandJet_integrable (d : OutgoingTail.TailData) {K : ℝ} (hK : 1 ≤ K) (square : Bool) {q : ℝ} (hq : ParametricHeatTail.tailDecay d square + q < 0) (n : ℕ) (η : ℝ) : MeasureTheory.IntegrableOn (etaIntegrandJet d K square q n η) (Set.Ioi K) MeasureTheory.volume

theorem NavierStokes.ExtendedHeatDebts.etaDebt_derivative_integral (d : OutgoingTail.TailData) {K : ℝ} (hK : 1 ≤ K) (square : Bool) {q : ℝ} (hq : ParametricHeatTail.tailDecay d square + q < 0) (n : ℕ) (η : ℝ) : iteratedDeriv n (etaDebt d K square q) η = ∫ (X : ℝ) in Set.Ioi K, etaIntegrandJet d K square q n η X

Every genuine eta derivative of the improper debt is the integral of the same genuine derivative of its integrand.

theorem NavierStokes.ExtendedHeatDebts.pressure_integrand_eq (d : OutgoingTail.TailData) {K X : ℝ} (hK : 0 < K) (hX : K < X) (η : ℝ) : squareChange (HeatTailEdit.outgoingProfile d K η) d.h (ParametricHeatTail.diffusion η) K X / X = weightedJet (ParametricHeatTail.tailWeight d K true) true d.h K (-1) 0 (ParametricHeatTail.diffusion η) X

theorem NavierStokes.ExtendedHeatDebts.energy_integrand_eq (d : OutgoingTail.TailData) {K X : ℝ} (hK : 0 < K) (hX : K < X) (η : ℝ) : squareChange (HeatTailEdit.outgoingProfile d K η) d.h (ParametricHeatTail.diffusion η) K X = weightedJet (ParametricHeatTail.tailWeight d K true) true d.h K 0 0 (ParametricHeatTail.diffusion η) X

theorem NavierStokes.ExtendedHeatDebts.angular_integrand_eq (d : OutgoingTail.TailData) {K X : ℝ} (hK : 0 < K) (hX : K < X) (η : ℝ) : √(2 * X) * change (HeatTailEdit.outgoingProfile d K η) d.h (ParametricHeatTail.diffusion η) K X = √2 * weightedJet (ParametricHeatTail.tailWeight d K false) false d.h K (1 / 2) 0 (ParametricHeatTail.diffusion η) X

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

theorem NavierStokes.ExtendedHeatDebts.physicalPressure_derivative_integral (d : OutgoingTail.TailData) {K : ℝ} (hK : 1 ≤ K) (n : ℕ) (η : ℝ) : iteratedDeriv n (physicalPressure d K) η = ∫ (X : ℝ) in Set.Ioi K, iteratedDeriv n (fun (θ : ℝ) => squareChange (HeatTailEdit.outgoingProfile d K θ) d.h (ParametricHeatTail.diffusion θ) K X / X) η

Differentiation under the literal pressure-debt improper integral.

theorem NavierStokes.ExtendedHeatDebts.physicalEnergy_derivative_integral (d : OutgoingTail.TailData) {K : ℝ} (hK : 1 ≤ K) (n : ℕ) (η : ℝ) : iteratedDeriv n (physicalEnergy d K) η = ∫ (X : ℝ) in Set.Ioi K, iteratedDeriv n (fun (θ : ℝ) => squareChange (HeatTailEdit.outgoingProfile d K θ) d.h (ParametricHeatTail.diffusion θ) K X) η

Differentiation under the literal energy-debt improper integral.

theorem NavierStokes.ExtendedHeatDebts.physicalAngular_derivative_integral (d : OutgoingTail.TailData) {K : ℝ} (hK : 1 ≤ K) (n : ℕ) (η : ℝ) : iteratedDeriv n (physicalAngular d K) η = ∫ (X : ℝ) in Set.Ioi K, iteratedDeriv n (fun (θ : ℝ) => √(2 * X) * change (HeatTailEdit.outgoingProfile d K θ) d.h (ParametricHeatTail.diffusion θ) K X) η

Differentiation under the literal angular-debt improper integral.

theorem NavierStokes.ExtendedHeatDebts.physicalDebt_eq_original (d : OutgoingTail.TailData) {K η : ℝ} (hK : 0 < K) (hη : η ∈ Set.Icc (-1) 1) : physicalDebt d K η = ParametricTerminalCompensation.physicalDebt d K η

theorem NavierStokes.ExtendedHeatDebts.normalizedDebt_eq_original (d : OutgoingTail.TailData) {K η : ℝ} (hK : 0 < K) (hη : η ∈ Set.Icc (-1) 1) : normalizedDebt d K η = TerminalCompensation.scaledDebt K (ParametricTerminalCompensation.physicalDebt d K η)

theorem NavierStokes.ExtendedHeatDebts.enlargedBand_isCompact : IsCompact enlargedBand

theorem NavierStokes.ExtendedHeatDebts.enlargedBand_uniqueDiffOn : UniqueDiffOn ℝ enlargedBand

theorem NavierStokes.ExtendedHeatDebts.physicalBand_subset_openNeighborhood : Set.Icc (-1) 1 ⊆ Set.Ioo (-(3 / 2)) (3 / 2)

theorem NavierStokes.ExtendedHeatDebts.normalizedDebt_derivWithin (d : OutgoingTail.TailData) {K η : ℝ} (hK : 1 ≤ K) (hη : η ∈ enlargedBand) : derivWithin (normalizedDebt d K) enlargedBand η = deriv (normalizedDebt d K) η

theorem NavierStokes.ExtendedHeatDebts.exists_normalized_C1_within_bounds (d : OutgoingTail.TailData) : ∃ (C : ℝ), 0 < C ∧ ∀ (K : ℝ), 1 ≤ K → ∀ η ∈ enlargedBand, ‖normalizedDebt d K η‖ ≤ C / K ∧ ‖derivWithin (normalizedDebt d K) enlargedBand η‖ ≤ C / K

Direct input to the existing compact-parameter compensation solver. The functions are already globally smooth; the within derivative is only the solver's compact-domain convention.

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

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

theorem NavierStokes.ExtendedHeatDebts.normalizedDebt_joint_contDiffOn (d : OutgoingTail.TailData) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × ℝ) => normalizedDebt d p.1 p.2) (Set.Ioi 0 ×ˢ Set.univ)