Terminal compensation for genuinely parameter-dependent debts

The physical heat parameter is 1-η². This module retains its contribution to the debt derivative. Smoothness at the ends of a compact parameter range is relative smoothness; all endpoint derivatives are actual derivWithin.

noncomputable def NavierStokes.ParametricTerminalCompensation.FirstJetWithinBound (P : TerminalCompensation.Patch) (a : ℝ → ℝ) (c : ℝ → TerminalCompensation.Coeff) (S : Set ℝ) (η L : ℝ) : Prop

First jet within bound as an element of Prop.

Equations

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

theorem NavierStokes.ParametricTerminalCompensation.FirstJetWithinBound.mono {P : TerminalCompensation.Patch} {a : ℝ → ℝ} {c : ℝ → TerminalCompensation.Coeff} {S : Set ℝ} {η L M : ℝ} (h : FirstJetWithinBound P a c S η L) (hLM : L ≤ M) : FirstJetWithinBound P a c S η M

theorem NavierStokes.ParametricTerminalCompensation.FirstJetWithinBound.toFirstJetBound {P : TerminalCompensation.Patch} {a : ℝ → ℝ} {c : ℝ → TerminalCompensation.Coeff} {S : Set ℝ} {η L : ℝ} (h : FirstJetWithinBound P a c S η L) (hS : S ∈ nhds η) : TerminalCompensation.FirstJetBound P a c η L

theorem NavierStokes.ParametricTerminalCompensation.compact_amplitude_within_bounds {S : Set ℝ} (hS : IsCompact S) (huniq : UniqueDiffOn ℝ S) {a : ℝ → ℝ} (ha : ContDiffOn ℝ (↑⊤) a S) (hpos : ∀ η ∈ S, 0 < a η) : ∃ (D : ℝ), 0 < D ∧ ∀ η ∈ S, ‖TerminalCompensation.amplitudeFactors (a η)‖ ≤ D ∧ ‖derivWithin (fun (θ : ℝ) => TerminalCompensation.amplitudeFactors (a θ)) S η‖ ≤ D ∧ |a η| ≤ D ∧ |derivWithin a S η| ≤ D

theorem NavierStokes.ParametricTerminalCompensation.amplitudeDebt_variable_contDiffOn {S : Set ℝ} {a : ℝ → ℝ} {v : ℝ → TerminalCompensation.Coeff} (ha : ContDiffOn ℝ (↑⊤) a S) (hpos : ∀ η ∈ S, 0 < a η) (hv : ContDiffOn ℝ (↑⊤) v S) : ContDiffOn ℝ (↑⊤) (fun (η : ℝ) => TerminalCompensation.amplitudeDebt (a η) (v η)) S

theorem NavierStokes.ParametricTerminalCompensation.amplitudeDebt_variable_derivWithin {S : Set ℝ} {a : ℝ → ℝ} {v : ℝ → TerminalCompensation.Coeff} {η : ℝ} (huniq : UniqueDiffWithinAt ℝ S η) (ha : DifferentiableWithinAt ℝ (fun (θ : ℝ) => TerminalCompensation.amplitudeFactors (a θ)) S η) (hv : DifferentiableWithinAt ℝ v S η) : derivWithin (fun (θ : ℝ) => TerminalCompensation.amplitudeDebt (a θ) (v θ)) S η = -(derivWithin (fun (θ : ℝ) => TerminalCompensation.amplitudeFactors (a θ)) S η * v η + TerminalCompensation.amplitudeFactors (a η) * derivWithin v S η)

Both terms are present: the amplitude derivative and the genuine debt derivative.

theorem NavierStokes.ParametricTerminalCompensation.amplitudeDebt_variable_bounds {S : Set ℝ} (huniq : UniqueDiffOn ℝ S) {a : ℝ → ℝ} {v : ℝ → TerminalCompensation.Coeff} (ha : ContDiffOn ℝ (↑⊤) a S) (hpos : ∀ η ∈ S, 0 < a η) (hv : ContDiffOn ℝ (↑⊤) v S) {D : ℝ} (hD : ∀ η ∈ S, ‖TerminalCompensation.amplitudeFactors (a η)‖ ≤ D ∧ ‖derivWithin (fun (θ : ℝ) => TerminalCompensation.amplitudeFactors (a θ)) S η‖ ≤ D) {η : ℝ} (hη : η ∈ S) : ‖TerminalCompensation.amplitudeDebt (a η) (v η)‖ ≤ D * ‖v η‖ ∧ ‖derivWithin (fun (θ : ℝ) => TerminalCompensation.amplitudeDebt (a θ) (v θ)) S η‖ ≤ D * (‖v η‖ + ‖derivWithin v S η‖)

theorem NavierStokes.ParametricTerminalCompensation.composed_solver_derivWithin_bound {g : TerminalCompensation.Coeff → TerminalCompensation.Coeff} {ε C : ℝ} (hg : ContDiffOn ℝ (↑⊤) g (Metric.ball 0 ε)) (hbound : ∀ v ∈ Metric.ball 0 ε, ‖fderiv ℝ g v‖ ≤ C) {S : Set ℝ} {d : ℝ → TerminalCompensation.Coeff} {η : ℝ} (huniq : UniqueDiffWithinAt ℝ S η) (hd : DifferentiableWithinAt ℝ d S η) (hmem : d η ∈ Metric.ball 0 ε) : ‖derivWithin (g ∘ d) S η‖ ≤ C * ‖derivWithin d S η‖

theorem NavierStokes.ParametricTerminalCompensation.correction_parameter_derivWithin (P : TerminalCompensation.Patch) {S : Set ℝ} {c : ℝ → TerminalCompensation.Coeff} {η : ℝ} (huniq : UniqueDiffWithinAt ℝ S η) (hc : DifferentiableWithinAt ℝ c S η) (x : ℝ) : derivWithin (fun (θ : ℝ) => TerminalCompensation.correction P (c θ) x) S η = TerminalCompensation.correction P (derivWithin c S η) x

theorem NavierStokes.ParametricTerminalCompensation.exists_variable_compensation (P : TerminalCompensation.Patch) (lam : ℝ) (hlam : 0 ≤ lam) {S : Set ℝ} (hS : IsCompact S) (huniq : UniqueDiffOn ℝ S) (a : ℝ → ℝ) (ha : ContDiffOn ℝ (↑⊤) a S) (hpos : ∀ η ∈ S, 0 < a η) : ∃ (ε : ℝ) (C : ℝ), 0 < ε ∧ 0 < C ∧ ∀ (v : ℝ → TerminalCompensation.Coeff), ContDiffOn ℝ (↑⊤) v S → (∀ η ∈ S, ‖v η‖ < ε) → ∃ (c : ℝ → TerminalCompensation.Coeff), ContDiffOn ℝ (↑⊤) c S ∧ ∀ η ∈ S, TerminalCompensation.momentMap P lam (c η) = TerminalCompensation.amplitudeDebt (a η) (v η) ∧ ‖c η‖ ≤ C * ‖v η‖ ∧ ‖derivWithin c S η‖ ≤ C * (‖v η‖ + ‖derivWithin v S η‖) ∧ FirstJetWithinBound P a c S η (C * (‖v η‖ + ‖derivWithin v S η‖)) ∧ ∀ (x : ℝ), 0 < x → 0 < a η * (TerminalCompensation.baseProfile lam x + TerminalCompensation.correction P (c η) x)

The constructed three-row inverse applies to a genuinely varying debt. The derivative estimate includes its actual first parameter derivative.

noncomputable def NavierStokes.ParametricTerminalCompensation.radiusRatioCLM (q : ℝ) : TerminalCompensation.Coeff →L[ℝ] TerminalCompensation.Coeff

Change from the heat-switch normalization to a patch at radius q*K.

Equations

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

theorem NavierStokes.ParametricTerminalCompensation.scaledDebt_radiusRatio (q K : ℝ) (hq : 0 < q) (d : TerminalCompensation.Coeff) : TerminalCompensation.scaledDebt (q * K) d = (radiusRatioCLM q) (TerminalCompensation.scaledDebt K d)

theorem NavierStokes.ParametricTerminalCompensation.radiusRatio_derivWithin (q : ℝ) {S : Set ℝ} {v : ℝ → TerminalCompensation.Coeff} {η : ℝ} (huniq : UniqueDiffWithinAt ℝ S η) (hv : DifferentiableWithinAt ℝ v S η) : derivWithin (fun (θ : ℝ) => (radiusRatioCLM q) (v θ)) S η = (radiusRatioCLM q) (derivWithin v S η)

theorem NavierStokes.ParametricTerminalCompensation.scaled_family_ratio_bounds (q : ℝ) (hq : 0 < q) {S : Set ℝ} (huniq : UniqueDiffOn ℝ S) (d : ℝ → ℝ → TerminalCompensation.Coeff) (B : ℝ) (hB : 0 < B) (hreg : ∀ (K : ℝ), 1 ≤ K → ContDiffOn ℝ (↑⊤) (fun (η : ℝ) => TerminalCompensation.scaledDebt K (d K η)) S) (hbound : ∀ (K : ℝ), 1 ≤ K → ∀ η ∈ S, ‖TerminalCompensation.scaledDebt K (d K η)‖ ≤ B / K ∧ ‖derivWithin (fun (θ : ℝ) => TerminalCompensation.scaledDebt K (d K θ)) S η‖ ≤ B / K) : ∃ (Bq : ℝ), 0 < Bq ∧ ∀ (K : ℝ), 1 ≤ K → ContDiffOn ℝ (↑⊤) (fun (η : ℝ) => TerminalCompensation.scaledDebt (q * K) (d K η)) S ∧ ∀ η ∈ S, ‖TerminalCompensation.scaledDebt (q * K) (d K η)‖ ≤ Bq / K ∧ ‖derivWithin (fun (θ : ℝ) => TerminalCompensation.scaledDebt (q * K) (d K θ)) S η‖ ≤ Bq / K

The fixed ratio costs one bounded linear operator in both the value and the actual parameter derivative.

theorem NavierStokes.ParametricTerminalCompensation.exists_compensation_for_scaled_family (P : TerminalCompensation.Patch) (lam : ℝ) (hlam : 0 ≤ lam) (q : ℝ) (hq : 0 < q) {S : Set ℝ} (hS : IsCompact S) (huniq : UniqueDiffOn ℝ S) (a : ℝ → ℝ) (ha : ContDiffOn ℝ (↑⊤) a S) (hpos : ∀ η ∈ S, 0 < a η) (d : ℝ → ℝ → TerminalCompensation.Coeff) (B : ℝ) (hB : 0 < B) (hreg : ∀ (K : ℝ), 1 ≤ K → ContDiffOn ℝ (↑⊤) (fun (η : ℝ) => TerminalCompensation.scaledDebt (q * K) (d K η)) S) (hbound : ∀ (K : ℝ), 1 ≤ K → ∀ η ∈ S, ‖TerminalCompensation.scaledDebt (q * K) (d K η)‖ ≤ B / K ∧ ‖derivWithin (fun (θ : ℝ) => TerminalCompensation.scaledDebt (q * K) (d K θ)) S η‖ ≤ B / K) : ∃ (K₀ : ℝ) (C : ℝ), 0 < K₀ ∧ 0 < C ∧ ∀ (K : ℝ), K₀ ≤ K → ∃ (c : ℝ → TerminalCompensation.Coeff), ContDiffOn ℝ (↑⊤) c S ∧ ∀ η ∈ S, TerminalCompensation.physicalMoments P lam (q * K) (a η) (c η) + d K η = 0 ∧ ‖c η‖ ≤ C / K ∧ ‖derivWithin c S η‖ ≤ C / K ∧ FirstJetWithinBound P a c S η (C / K) ∧ ∀ (X : ℝ), 0 < X → 0 < TerminalCompensation.physicalProfile P lam (q * K) (a η) (c η) X

Uniform O(1/K) value and derivative bounds for a nonconstant physical debt family give exact compensation with the same first-jet cost.

theorem NavierStokes.ParametricTerminalCompensation.exists_compensation_for_switch_family (P : TerminalCompensation.Patch) (lam : ℝ) (hlam : 0 ≤ lam) (q : ℝ) (hq : 0 < q) {S : Set ℝ} (hS : IsCompact S) (huniq : UniqueDiffOn ℝ S) (a : ℝ → ℝ) (ha : ContDiffOn ℝ (↑⊤) a S) (hpos : ∀ η ∈ S, 0 < a η) (d : ℝ → ℝ → TerminalCompensation.Coeff) (B : ℝ) (hB : 0 < B) (hreg : ∀ (K : ℝ), 1 ≤ K → ContDiffOn ℝ (↑⊤) (fun (η : ℝ) => TerminalCompensation.scaledDebt K (d K η)) S) (hbound : ∀ (K : ℝ), 1 ≤ K → ∀ η ∈ S, ‖TerminalCompensation.scaledDebt K (d K η)‖ ≤ B / K ∧ ‖derivWithin (fun (θ : ℝ) => TerminalCompensation.scaledDebt K (d K θ)) S η‖ ≤ B / K) : ∃ (K₀ : ℝ) (C : ℝ), 0 < K₀ ∧ 0 < C ∧ ∀ (K : ℝ), K₀ ≤ K → ∃ (c : ℝ → TerminalCompensation.Coeff), ContDiffOn ℝ (↑⊤) c S ∧ ∀ η ∈ S, TerminalCompensation.physicalMoments P lam (q * K) (a η) (c η) + d K η = 0 ∧ ‖c η‖ ≤ C / K ∧ ‖derivWithin c S η‖ ≤ C / K ∧ FirstJetWithinBound P a c S η (C / K) ∧ ∀ (X : ℝ), 0 < X → 0 < TerminalCompensation.physicalProfile P lam (q * K) (a η) (c η) X

Input may be normalized at the heat switch itself; the proved ratio map transports both required bounds to the reserved patch.

theorem NavierStokes.ParametricTerminalCompensation.interior_first_jet {P : TerminalCompensation.Patch} {S : Set ℝ} {a : ℝ → ℝ} {c : ℝ → TerminalCompensation.Coeff} {η L : ℝ} (hS : S ∈ nhds η) (hc : ‖derivWithin c S η‖ ≤ L) (hE : FirstJetWithinBound P a c S η L) : ‖deriv c η‖ ≤ L ∧ TerminalCompensation.FirstJetBound P a c η L

Inside the parameter domain these bounds are on ordinary derivatives.

theorem NavierStokes.ParametricTerminalCompensation.scaled_triple_contDiffOn {S : Set ℝ} (K : ℝ) {p e i : ℝ → ℝ} (hp : ContDiffOn ℝ (↑⊤) p S) (he : ContDiffOn ℝ (↑⊤) e S) (hi : ContDiffOn ℝ (↑⊤) i S) : ContDiffOn ℝ (↑⊤) (fun (η : ℝ) => TerminalCompensation.scaledDebt K ![p η, e η, i η]) S

theorem NavierStokes.ParametricTerminalCompensation.angular_scaling_bound {K B u : ℝ} (hK : 0 < K) (hB : 0 ≤ B) (hu : |u| ≤ B * √K) : |u / (K * √(2 * K))| ≤ B / K

theorem NavierStokes.ParametricTerminalCompensation.scaled_triple_norm_bound {K B p e i : ℝ} (hK : 0 < K) (hB : 0 ≤ B) (hp : |p| ≤ B / K) (he : |e| ≤ B) (hi : |i| ≤ B * √K) : ‖TerminalCompensation.scaledDebt K ![p, e, i]‖ ≤ B / K

theorem NavierStokes.ParametricTerminalCompensation.scaled_triple_derivWithin {S : Set ℝ} (K : ℝ) {p e i : ℝ → ℝ} {η : ℝ} (huniq : UniqueDiffWithinAt ℝ S η) (hp : DifferentiableWithinAt ℝ p S η) (he : DifferentiableWithinAt ℝ e S η) (hi : DifferentiableWithinAt ℝ i S η) : derivWithin (fun (θ : ℝ) => TerminalCompensation.scaledDebt K ![p θ, e θ, i θ]) S η = TerminalCompensation.scaledDebt K ![derivWithin p S η, derivWithin e S η, derivWithin i S η]

theorem NavierStokes.ParametricTerminalCompensation.scaled_triple_first_jet_bound {S : Set ℝ} {K B : ℝ} {p e i : ℝ → ℝ} {η : ℝ} (hK : 0 < K) (hB : 0 ≤ B) (huniq : UniqueDiffWithinAt ℝ S η) (hp : DifferentiableWithinAt ℝ p S η) (he : DifferentiableWithinAt ℝ e S η) (hi : DifferentiableWithinAt ℝ i S η) (hpb : |p η| ≤ B / K ∧ |derivWithin p S η| ≤ B / K) (heb : |e η| ≤ B ∧ |derivWithin e S η| ≤ B) (hib : |i η| ≤ B * √K ∧ |derivWithin i S η| ≤ B * √K) : ‖TerminalCompensation.scaledDebt K ![p η, e η, i η]‖ ≤ B / K ∧ ‖derivWithin (fun (θ : ℝ) => TerminalCompensation.scaledDebt K ![p θ, e θ, i θ]) S η‖ ≤ B / K

Scalar physical estimates at their natural three scales give the vector estimate required by the compensation solver, including the actual derivative.

noncomputable def NavierStokes.ParametricTerminalCompensation.physicalDebt (T : OutgoingTail.TailData) (K η : ℝ) : TerminalCompensation.Coeff

The actual three physical debts use the diffusion parameter 1-η².

Equations

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

theorem NavierStokes.ParametricTerminalCompensation.physicalDebt_eq_actual (T : OutgoingTail.TailData) (K η : ℝ) : physicalDebt T K η = ![HeatTailEdit.pressureDebt (HeatTailEdit.outgoingProfile T K η) T.h (1 - η ^ 2) K, HeatTailEdit.energyDebt (HeatTailEdit.outgoingProfile T K η) T.h (1 - η ^ 2) K, HeatTailEdit.angularDebt (HeatTailEdit.outgoingProfile T K η) T.h (1 - η ^ 2) K]

theorem NavierStokes.ParametricTerminalCompensation.physical_scaled_debt_contDiffOn (T : OutgoingTail.TailData) {K : ℝ} (hK : 1 ≤ K) : ContDiffOn ℝ (↑⊤) (fun (η : ℝ) => TerminalCompensation.scaledDebt K (physicalDebt T K η)) (Set.Icc (-1) 1)

theorem NavierStokes.ParametricTerminalCompensation.physical_scaled_debt_C1_bounds (T : OutgoingTail.TailData) : ∃ (B : ℝ), 0 < B ∧ ∀ (K : ℝ), 1 ≤ K → ∀ η ∈ Set.Icc (-1) 1, ‖TerminalCompensation.scaledDebt K (physicalDebt T K η)‖ ≤ B / K ∧ ‖derivWithin (fun (θ : ℝ) => TerminalCompensation.scaledDebt K (physicalDebt T K θ)) (Set.Icc (-1) 1) η‖ ≤ B / K

Both estimates concern the actual nonconstant physical debt.

theorem NavierStokes.ParametricTerminalCompensation.exists_physical_heat_compensation (P : TerminalCompensation.Patch) (lam : ℝ) (hlam : 0 ≤ lam) (T : OutgoingTail.TailData) (q : ℝ) (hq : 0 < q) (a : ℝ → ℝ) (ha : ContDiffOn ℝ (↑⊤) a (Set.Icc (-1) 1)) (hpos : ∀ η ∈ Set.Icc (-1) 1, 0 < a η) : ∃ (K₀ : ℝ) (C : ℝ), 0 < K₀ ∧ 0 < C ∧ ∀ (K : ℝ), K₀ ≤ K → ∃ (c : ℝ → TerminalCompensation.Coeff), ContDiffOn ℝ (↑⊤) c (Set.Icc (-1) 1) ∧ ∀ η ∈ Set.Icc (-1) 1, TerminalCompensation.physicalMoments P lam (q * K) (a η) (c η) + physicalDebt T K η = 0 ∧ ‖c η‖ ≤ C / K ∧ ‖derivWithin c (Set.Icc (-1) 1) η‖ ≤ C / K ∧ FirstJetWithinBound P a c (Set.Icc (-1) 1) η (C / K) ∧ ∀ (X : ℝ), 0 < X → 0 < TerminalCompensation.physicalProfile P lam (q * K) (a η) (c η) X

The physical heat edit with diffusion 1-η² allows exact three-moment compensation, including the closed parameter endpoints and uniform first jets.