Three exact terminal compensation moments

Three constructed, separated additive bumps in a positive interval repair the pressure, energy, and angular moments. Factoring out the positive shaped-wait amplitude leaves one fixed quadratic map, so its smooth inverse and estimates are uniform in the transverse parameter.

@[reducible, inline]

abbrev NavierStokes.TerminalCompensation.Coeff : Type

Coefficient: an abbreviation for Fin 3 → ℝ.

Equations

• NavierStokes.TerminalCompensation.Coeff = (Fin 3 → ℝ)

structure NavierStokes.TerminalCompensation.Patch : Type

An arbitrary reserved interval in the normalized positive radial coordinate.

• left : ℝ

  Left of Patch, of type ℝ.

• right : ℝ

  Right of Patch, of type ℝ.

• left_pos : 0 < self.left
• ordered : self.left < self.right

noncomputable def NavierStokes.TerminalCompensation.lower (P : Patch) (j : Fin 3) : ℝ

Lower, given by P.left + (2 * (j.val : ℝ) + 1) * (P.right - P.left) / 7.

Equations

• NavierStokes.TerminalCompensation.lower P j = P.left + (2 * ↑↑j + 1) * (P.right - P.left) / 7

noncomputable def NavierStokes.TerminalCompensation.upper (P : Patch) (j : Fin 3) : ℝ

Upper, given by P.left + (2 * (j.val : ℝ) + 2) * (P.right - P.left) / 7.

Equations

• NavierStokes.TerminalCompensation.upper P j = P.left + (2 * ↑↑j + 2) * (P.right - P.left) / 7

theorem NavierStokes.TerminalCompensation.lower_gt_left (P : Patch) (j : Fin 3) : P.left < lower P j

theorem NavierStokes.TerminalCompensation.lower_lt_upper (P : Patch) (j : Fin 3) : lower P j < upper P j

theorem NavierStokes.TerminalCompensation.upper_lt_right (P : Patch) (j : Fin 3) : upper P j < P.right

theorem NavierStokes.TerminalCompensation.intervals_separated (P : Patch) (i j : Fin 3) (hij : i < j) : upper P i ≤ lower P j

noncomputable def NavierStokes.TerminalCompensation.bump (P : Patch) (j : Fin 3) : ℝ → ℝ

Bump, given by LocalizedMomentRepair.bump (lower P j) (upper P j).

Equations

• NavierStokes.TerminalCompensation.bump P j = NavierStokes.LocalizedMomentRepair.bump (NavierStokes.TerminalCompensation.lower P j) (NavierStokes.TerminalCompensation.upper P j)

theorem NavierStokes.TerminalCompensation.bump_contDiff (P : Patch) (j : Fin 3) : ContDiff ℝ (↑⊤) (bump P j)

theorem NavierStokes.TerminalCompensation.bump_nonneg (P : Patch) (j : Fin 3) (x : ℝ) : 0 ≤ bump P j x

theorem NavierStokes.TerminalCompensation.bump_le_one (P : Patch) (j : Fin 3) (x : ℝ) : bump P j x ≤ 1

theorem NavierStokes.TerminalCompensation.bump_tsupport (P : Patch) (j : Fin 3) : tsupport (bump P j) ⊆ Set.Ioo (lower P j) (upper P j)

theorem NavierStokes.TerminalCompensation.bump_support_patch (P : Patch) (j : Fin 3) : Function.support (bump P j) ⊆ Set.Icc P.left P.right

theorem NavierStokes.TerminalCompensation.bumps_disjoint (P : Patch) (i j : Fin 3) (hij : i ≠ j) (x : ℝ) : bump P i x * bump P j x = 0

noncomputable def NavierStokes.TerminalCompensation.correction (P : Patch) (c : Coeff) (x : ℝ) : ℝ

Correction, given by ∑ j, c j * bump P j x.

Equations

• NavierStokes.TerminalCompensation.correction P c x = ∑ j : Fin 3, c j * NavierStokes.TerminalCompensation.bump P j x

theorem NavierStokes.TerminalCompensation.correction_contDiff (P : Patch) (c : Coeff) : ContDiff ℝ (↑⊤) (correction P c)

theorem NavierStokes.TerminalCompensation.correction_support (P : Patch) (c : Coeff) : Function.support (correction P c) ⊆ Set.Icc P.left P.right

theorem NavierStokes.TerminalCompensation.correction_tsupport (P : Patch) (c : Coeff) : tsupport (correction P c) ⊆ Set.Ioo P.left P.right

theorem NavierStokes.TerminalCompensation.correction_hasCompactSupport (P : Patch) (c : Coeff) : HasCompactSupport (correction P c)

theorem NavierStokes.TerminalCompensation.weighted_integrable (P : Patch) (s : ℝ) (g : ℝ → ℝ) (hg : Continuous g) (hs : Function.support g ⊆ Set.Icc P.left P.right) : MeasureTheory.Integrable (fun (x : ℝ) => x ^ s * g x) MeasureTheory.volume

theorem NavierStokes.TerminalCompensation.weighted_bump_integrable (P : Patch) (s : ℝ) (j : Fin 3) : MeasureTheory.Integrable (fun (x : ℝ) => x ^ s * bump P j x) MeasureTheory.volume

theorem NavierStokes.TerminalCompensation.weighted_bump_sq_integrable (P : Patch) (s : ℝ) (j : Fin 3) : MeasureTheory.Integrable (fun (x : ℝ) => x ^ s * bump P j x ^ 2) MeasureTheory.volume

theorem NavierStokes.TerminalCompensation.correction_square (P : Patch) (c : Coeff) (x : ℝ) : correction P c x ^ 2 = ∑ j : Fin 3, c j ^ 2 * bump P j x ^ 2

noncomputable def NavierStokes.TerminalCompensation.bumpMoment (P : Patch) (s : ℝ) (j : Fin 3) : ℝ

Bump moment, given by ∫ x, x ^ s * bump P j x.

Equations

• NavierStokes.TerminalCompensation.bumpMoment P s j = ∫ (x : ℝ), x ^ s * NavierStokes.TerminalCompensation.bump P j x

noncomputable def NavierStokes.TerminalCompensation.squareMoment (P : Patch) (s : ℝ) (j : Fin 3) : ℝ

Square moment, given by ∫ x, x ^ s * (bump P j x) ^ 2.

Equations

• NavierStokes.TerminalCompensation.squareMoment P s j = ∫ (x : ℝ), x ^ s * NavierStokes.TerminalCompensation.bump P j x ^ 2

theorem NavierStokes.TerminalCompensation.correction_moment (P : Patch) (s : ℝ) (c : Coeff) : ∫ (x : ℝ), x ^ s * correction P c x = ∑ j : Fin 3, c j * bumpMoment P s j

theorem NavierStokes.TerminalCompensation.correction_square_moment (P : Patch) (s : ℝ) (c : Coeff) : ∫ (x : ℝ), x ^ s * correction P c x ^ 2 = ∑ j : Fin 3, c j ^ 2 * squareMoment P s j

noncomputable def NavierStokes.TerminalCompensation.slope (lam : ℝ) : ℝ

Slope, given by -1 / 2 - lam.

Equations

• NavierStokes.TerminalCompensation.slope lam = -1 / 2 - lam

noncomputable def NavierStokes.TerminalCompensation.powers (lam : ℝ) : Coeff

Powers, given by ![-1 + slope lam, slope lam, 1 / 2].

Equations

• NavierStokes.TerminalCompensation.powers lam = ![-1 + NavierStokes.TerminalCompensation.slope lam, NavierStokes.TerminalCompensation.slope lam, 1 / 2]

theorem NavierStokes.TerminalCompensation.powers_injective (lam : ℝ) (hlam : 0 ≤ lam) : Function.Injective (powers lam)

noncomputable def NavierStokes.TerminalCompensation.linearMatrix (P : Patch) (lam : ℝ) : Matrix (Fin 3) (Fin 3) ℝ

Linear matrix, given by LocalizedMomentRepair.matrix (powers lam) (lower P) (upper P).

Equations

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

theorem NavierStokes.TerminalCompensation.linearMatrix_entry (P : Patch) (lam : ℝ) (i j : Fin 3) : linearMatrix P lam i j = bumpMoment P (powers lam i) j

theorem NavierStokes.TerminalCompensation.linearMatrix_det_ne_zero (P : Patch) (lam : ℝ) (hlam : 0 ≤ lam) : (linearMatrix P lam).det ≠ 0

The three powers are those of pressure, energy, and angular momentum.

noncomputable def NavierStokes.TerminalCompensation.linearEquiv (P : Patch) (lam : ℝ) (hlam : 0 ≤ lam) : Coeff ≃L[ℝ] Coeff

Linear equiv, constructed using LinearEquiv.toContinuousLinearEquiv.

Equations

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

theorem NavierStokes.TerminalCompensation.linearEquiv_apply (P : Patch) (lam : ℝ) (hlam : 0 ≤ lam) (c : Coeff) : (linearEquiv P lam hlam) c = (linearMatrix P lam).mulVec c

noncomputable def NavierStokes.TerminalCompensation.quadraticBilin (P : Patch) : Coeff →ₗ[ℝ] Coeff →ₗ[ℝ] Coeff

Quadratic bilin, bundling toFun, map_add, map_smul, map_add and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.TerminalCompensation.quadraticCLM (P : Patch) : Coeff →L[ℝ] Coeff →L[ℝ] Coeff

Quadratic continuous linear map, constructed using LinearMap.toContinuousLinearMap.

Equations

• NavierStokes.TerminalCompensation.quadraticCLM P = LinearMap.toContinuousLinearMap (↑LinearMap.toContinuousLinearMap ∘ₗ NavierStokes.TerminalCompensation.quadraticBilin P)

theorem NavierStokes.TerminalCompensation.quadraticCLM_apply (P : Patch) (c d : Coeff) : ((quadraticCLM P) c) d = ![1 / 2 * ∑ j : Fin 3, squareMoment P (-1) j * c j * d j, 1 / 2 * ∑ j : Fin 3, squareMoment P 0 j * c j * d j, 0]

noncomputable def NavierStokes.TerminalCompensation.baseProfile (lam x : ℝ) : ℝ

Base profile, given by x ^ slope lam.

Equations

• NavierStokes.TerminalCompensation.baseProfile lam x = x ^ NavierStokes.TerminalCompensation.slope lam

noncomputable def NavierStokes.TerminalCompensation.weightedChange (P : Patch) (lam : ℝ) (c : Coeff) (w x : ℝ) : ℝ

One half of a squared-profile change, against a power weight.

Equations

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

theorem NavierStokes.TerminalCompensation.weightedChange_identity (P : Patch) (lam : ℝ) (c : Coeff) (w x : ℝ) : weightedChange P lam c w x = x ^ (w + slope lam) * correction P c x + x ^ w * correction P c x ^ 2 / 2

theorem NavierStokes.TerminalCompensation.weighted_correction_integrable (P : Patch) (s : ℝ) (c : Coeff) : MeasureTheory.Integrable (fun (x : ℝ) => x ^ s * correction P c x) MeasureTheory.volume

theorem NavierStokes.TerminalCompensation.weighted_correction_sq_integrable (P : Patch) (s : ℝ) (c : Coeff) : MeasureTheory.Integrable (fun (x : ℝ) => x ^ s * correction P c x ^ 2) MeasureTheory.volume

theorem NavierStokes.TerminalCompensation.weightedChange_integrable (P : Patch) (lam : ℝ) (c : Coeff) (w : ℝ) : MeasureTheory.Integrable (weightedChange P lam c w) MeasureTheory.volume

theorem NavierStokes.TerminalCompensation.weightedChange_integral (P : Patch) (lam : ℝ) (c : Coeff) (w : ℝ) : ∫ (x : ℝ), weightedChange P lam c w x = ∑ j : Fin 3, c j * bumpMoment P (w + slope lam) j + (∑ j : Fin 3, c j ^ 2 * squareMoment P w j) / 2

noncomputable def NavierStokes.TerminalCompensation.momentMap (P : Patch) (lam : ℝ) (c : Coeff) : Coeff

Actual normalized pressure, energy, and angular moment changes.

Equations

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

theorem NavierStokes.TerminalCompensation.momentMap_identity (P : Patch) (lam : ℝ) (hlam : 0 ≤ lam) (c : Coeff) : (linearEquiv P lam hlam) c + ((quadraticCLM P) c) c = momentMap P lam c

theorem NavierStokes.TerminalCompensation.correction_iteratedDeriv (P : Patch) (c : Coeff) (k : ℕ) (x : ℝ) : iteratedDeriv k (correction P c) x = ∑ j : Fin 3, c j * iteratedDeriv k (bump P j) x

theorem NavierStokes.TerminalCompensation.correction_derivative_bound (P : Patch) (k : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (c : Coeff) (x : ℝ), |iteratedDeriv k (correction P c) x| ≤ C * ‖c‖

theorem NavierStokes.TerminalCompensation.correction_first_jet_bound (P : Patch) : ∃ (D : ℝ), 0 < D ∧ ∀ (c : Coeff) (x : ℝ), |correction P c x| ≤ D * ‖c‖ ∧ |deriv (correction P c) x| ≤ D * ‖c‖

theorem NavierStokes.TerminalCompensation.baseProfile_positive (lam : ℝ) {x : ℝ} (hx : 0 < x) : 0 < baseProfile lam x

theorem NavierStokes.TerminalCompensation.baseProfile_lower_bound (P : Patch) (lam : ℝ) : ∃ (m : ℝ), 0 < m ∧ ∀ x ∈ Set.Icc P.left P.right, m ≤ baseProfile lam x

theorem NavierStokes.TerminalCompensation.exists_normalized_compensation (P : Patch) (lam : ℝ) (hlam : 0 ≤ lam) : ∃ (g : Coeff → Coeff) (ε : ℝ) (C : ℝ), 0 < ε ∧ 0 < C ∧ ContDiffOn ℝ (↑⊤) g (Metric.ball 0 ε) ∧ g 0 = 0 ∧ ∀ d ∈ Metric.ball 0 ε, momentMap P lam (g d) = d ∧ ‖g d‖ ≤ C * ‖d‖ ∧ ‖fderiv ℝ g d‖ ≤ C ∧ ∀ (x : ℝ), (|correction P (g d) x| ≤ C * ‖d‖ ∧ |deriv (correction P (g d)) x| ≤ C * ‖d‖) ∧ (0 < x → 0 < baseProfile lam x + correction P (g d) x)

A single smooth inverse repairs all three actual moments and has uniform value, derivative, and spatial first-jet bounds. Smallness also preserves positivity.

noncomputable def NavierStokes.TerminalCompensation.correctionCLM (P : Patch) (x : ℝ) : Coeff →L[ℝ] ℝ

Evaluation of the finite bump combination is an actual bounded linear map.

Equations

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

theorem NavierStokes.TerminalCompensation.correctionCLM_apply (P : Patch) (x : ℝ) (c : Coeff) : (correctionCLM P x) c = correction P c x

theorem NavierStokes.TerminalCompensation.correction_parameter_deriv (P : Patch) {c : ℝ → Coeff} {η : ℝ} (hc : DifferentiableAt ℝ c η) (x : ℝ) : deriv (fun (s : ℝ) => correction P (c s) x) η = correction P (deriv c η) x

theorem NavierStokes.TerminalCompensation.correction_family_contDiffOn (P : Patch) {U : Set ℝ} {c : ℝ → Coeff} (hc : ContDiffOn ℝ (↑⊤) c U) : ContDiffOn ℝ (↑⊤) (fun (z : ℝ × ℝ) => correction P (c z.1) z.2) (U ×ˢ Set.univ)

theorem NavierStokes.TerminalCompensation.composed_solver_deriv_bound {g : Coeff → Coeff} {ε C : ℝ} (hg : ContDiffOn ℝ (↑⊤) g (Metric.ball 0 ε)) (hbound : ∀ v ∈ Metric.ball 0 ε, ‖fderiv ℝ g v‖ ≤ C) {d : ℝ → Coeff} {η : ℝ} (hd : DifferentiableAt ℝ d η) (hmem : d η ∈ Metric.ball 0 ε) : ‖deriv (g ∘ d) η‖ ≤ C * ‖deriv d η‖

Composition with the debt gives the true parameter derivative, with no regularity hypothesis on a previously chosen solution branch.

noncomputable def NavierStokes.TerminalCompensation.physicalProfile (P : Patch) (lam R a : ℝ) (c : Coeff) (X : ℝ) : ℝ

The physical profile uses the actual additive bumps at scale R.

Equations

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

noncomputable def NavierStokes.TerminalCompensation.cleanProfile (lam R a X : ℝ) : ℝ

Clean profile, given by a * baseProfile lam (X / R).

Equations

• NavierStokes.TerminalCompensation.cleanProfile lam R a X = a * NavierStokes.TerminalCompensation.baseProfile lam (X / R)

noncomputable def NavierStokes.TerminalCompensation.physicalMoments (P : Patch) (lam R a : ℝ) (c : Coeff) : Coeff

Physical moments as an element of Coeff.

Equations

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

theorem NavierStokes.TerminalCompensation.integral_rescale (R : ℝ) (hR : 0 < R) (F : ℝ → ℝ) : ∫ (X : ℝ), F X = R * ∫ (x : ℝ), F (R * x)

theorem NavierStokes.TerminalCompensation.pressure_density_rescale (P : Patch) (lam R a : ℝ) (hR : 0 < R) (c : Coeff) (x : ℝ) : (physicalProfile P lam R a c (R * x) ^ 2 - cleanProfile lam R a (R * x) ^ 2) / (R * x) = 2 * a ^ 2 / R * weightedChange P lam c (-1) x

theorem NavierStokes.TerminalCompensation.energy_density_rescale (P : Patch) (lam R a : ℝ) (hR : 0 < R) (c : Coeff) (x : ℝ) : physicalProfile P lam R a c (R * x) ^ 2 - cleanProfile lam R a (R * x) ^ 2 = 2 * a ^ 2 * weightedChange P lam c 0 x

theorem NavierStokes.TerminalCompensation.angular_density_rescale (P : Patch) (lam R a : ℝ) (hR : 0 < R) (c : Coeff) (x : ℝ) : √(2 * (R * x)) * (physicalProfile P lam R a c (R * x) - cleanProfile lam R a (R * x)) = √(2 * R) * a * (x ^ (1 / 2) * correction P c x)

theorem NavierStokes.TerminalCompensation.physicalMoments_eq (P : Patch) (lam R a : ℝ) (hR : 0 < R) (c : Coeff) : physicalMoments P lam R a c = ![2 * a ^ 2 * momentMap P lam c 0, 2 * R * a ^ 2 * momentMap P lam c 1, R * √(2 * R) * a * momentMap P lam c 2]

The normalization constants follow from the actual change of variable X=R*x.

noncomputable def NavierStokes.TerminalCompensation.normalizationFactors (R a : ℝ) : Coeff

Normalization factors, given by `![(2 * a ^ 2)⁻¹, (2 * R * a ^ 2)⁻¹, (R * Real.sqrt (2 * R)

• a)⁻¹]`.

Equations

• NavierStokes.TerminalCompensation.normalizationFactors R a = ![(2 * a ^ 2)⁻¹, (2 * R * a ^ 2)⁻¹, (R * √(2 * R) * a)⁻¹]

noncomputable def NavierStokes.TerminalCompensation.normalizedDebt (R a : ℝ) (d : Coeff) : Coeff

Signed debts are negated so that their sum with the patch changes is zero.

Equations

• NavierStokes.TerminalCompensation.normalizedDebt R a d = -(NavierStokes.TerminalCompensation.normalizationFactors R a * d)

theorem NavierStokes.TerminalCompensation.physicalMoments_cancel (P : Patch) (lam R a : ℝ) (hR : 0 < R) (ha : 0 < a) (c d : Coeff) (heq : momentMap P lam c = normalizedDebt R a d) : physicalMoments P lam R a c + d = 0

noncomputable def NavierStokes.TerminalCompensation.scaledDebt (R : ℝ) (d : Coeff) : Coeff

Radial normalization, independent of the shaped-wait amplitude.

Equations

• NavierStokes.TerminalCompensation.scaledDebt R d = ![d 0, d 1 / R, d 2 / (R * √(2 * R))]

noncomputable def NavierStokes.TerminalCompensation.amplitudeFactors (a : ℝ) : Coeff

Amplitude factors, given by ![(2 * a ^ 2)⁻¹, (2 * a ^ 2)⁻¹, a⁻¹].

Equations

• NavierStokes.TerminalCompensation.amplitudeFactors a = ![(2 * a ^ 2)⁻¹, (2 * a ^ 2)⁻¹, a⁻¹]

noncomputable def NavierStokes.TerminalCompensation.amplitudeDebt (a : ℝ) (v : Coeff) : Coeff

Amplitude debt, given by -(amplitudeFactors a * v).

Equations

• NavierStokes.TerminalCompensation.amplitudeDebt a v = -(NavierStokes.TerminalCompensation.amplitudeFactors a * v)

theorem NavierStokes.TerminalCompensation.normalizedDebt_eq (R a : ℝ) (d : Coeff) : normalizedDebt R a d = amplitudeDebt a (scaledDebt R d)

theorem NavierStokes.TerminalCompensation.amplitudeFactors_contDiffOn {U : Set ℝ} {a : ℝ → ℝ} (ha : ContDiffOn ℝ (↑⊤) a U) (hpos : ∀ η ∈ U, 0 < a η) : ContDiffOn ℝ (↑⊤) (fun (η : ℝ) => amplitudeFactors (a η)) U

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

theorem NavierStokes.TerminalCompensation.compact_amplitude_bounds {U S : Set ℝ} (hU : IsOpen U) (hS : IsCompact S) (hSU : S ⊆ U) {a : ℝ → ℝ} (ha : ContDiffOn ℝ (↑⊤) a U) (hpos : ∀ η ∈ U, 0 < a η) : ∃ (D : ℝ), 0 < D ∧ ∀ η ∈ S, ‖amplitudeFactors (a η)‖ ≤ D ∧ ‖deriv (fun (θ : ℝ) => amplitudeFactors (a θ)) η‖ ≤ D ∧ |a η| ≤ D ∧ |deriv a η| ≤ D

theorem NavierStokes.TerminalCompensation.amplitudeDebt_bounds {U S : Set ℝ} (hU : IsOpen U) (hSU : S ⊆ U) {a : ℝ → ℝ} (ha : ContDiffOn ℝ (↑⊤) a U) (hpos : ∀ η ∈ U, 0 < a η) {D : ℝ} (hD : ∀ η ∈ S, ‖amplitudeFactors (a η)‖ ≤ D ∧ ‖deriv (fun (θ : ℝ) => amplitudeFactors (a θ)) η‖ ≤ D) (v : Coeff) {η : ℝ} (hη : η ∈ S) : ‖amplitudeDebt (a η) v‖ ≤ D * ‖v‖ ∧ ‖deriv (fun (θ : ℝ) => amplitudeDebt (a θ) v) η‖ ≤ D * ‖v‖

noncomputable def NavierStokes.TerminalCompensation.FirstJetBound (P : Patch) (a : ℝ → ℝ) (c : ℝ → Coeff) (η L : ℝ) : Prop

The value, normalized radial derivative, and parameter derivative of the actual additive profile perturbation are all small.

Equations

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

theorem NavierStokes.TerminalCompensation.exists_uniform_parameter_compensation (P : Patch) (lam : ℝ) (hlam : 0 ≤ lam) {U S : Set ℝ} (hU : IsOpen U) (hS : IsCompact S) (hSU : S ⊆ U) (a : ℝ → ℝ) (ha : ContDiffOn ℝ (↑⊤) a U) (hpos : ∀ η ∈ U, 0 < a η) : ∃ (ε : ℝ) (C : ℝ), 0 < ε ∧ 0 < C ∧ ∀ (v : Coeff), ‖v‖ < ε → ∃ (c : ℝ → Coeff) (V : Set ℝ), IsOpen V ∧ S ⊆ V ∧ V ⊆ U ∧ ContDiffOn ℝ (↑⊤) c V ∧ ∀ η ∈ S, momentMap P lam (c η) = amplitudeDebt (a η) v ∧ ‖c η‖ ≤ C * ‖v‖ ∧ ‖deriv c η‖ ≤ C * ‖v‖ ∧ FirstJetBound P a c η (C * ‖v‖) ∧ ∀ (x : ℝ), 0 < x → 0 < a η * (baseProfile lam x + correction P (c η) x)

One debt threshold and one first-jet constant work on the entire compact parameter range. Both are independent of the physical radial scale.

theorem NavierStokes.TerminalCompensation.physicalProfile_eq_clean_outside (P : Patch) (lam R a : ℝ) (c : Coeff) (X : ℝ) (hX : X / R ∉ Set.Ioo P.left P.right) : physicalProfile P lam R a c X = cleanProfile lam R a X

theorem NavierStokes.TerminalCompensation.physicalDifference_hasCompactSupport (P : Patch) (lam R a : ℝ) (hR : 0 < R) (c : Coeff) : HasCompactSupport fun (X : ℝ) => physicalProfile P lam R a c X - cleanProfile lam R a X

theorem NavierStokes.TerminalCompensation.mixed_moment_unchanged (P : Patch) (lam R a : ℝ) (c : Coeff) (U : ℝ → ℝ) (hU : ∀ (X : ℝ), X / R ∈ Set.Ioo P.left P.right → U X = 0) : ∫ (X : ℝ), U X * physicalProfile P lam R a c X = ∫ (X : ℝ), U X * cleanProfile lam R a X

On the reserved patch U=0, so the mixed axial-angular moment is unchanged.

theorem NavierStokes.TerminalCompensation.angular_scale_eq (R : ℝ) (hR : 0 < R) : R * √(2 * R) = √2 * R ^ (3 / 2)

noncomputable def NavierStokes.TerminalCompensation.heatDebt (T : OutgoingTail.TailData) (ν K η : ℝ) : Coeff

Heat debt as an element of Coeff.

Equations

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

theorem NavierStokes.TerminalCompensation.heatDebt_independent (T : OutgoingTail.TailData) (ν : ℝ) {K : ℝ} (hK : 0 < K) (η : ℝ) : heatDebt T ν K η = heatDebt T ν K 0

theorem NavierStokes.TerminalCompensation.scaled_heatDebt_bound (T : OutgoingTail.TailData) (ν q : ℝ) (hν : 0 < ν) (hq : 0 < q) : ∃ (C : ℝ), 0 < C ∧ ∀ (K : ℝ), 0 < K → ‖scaledDebt (q * K) (heatDebt T ν K 0)‖ ≤ C / K

The actual heat-tail debts become uniformly O(1/K) in the fixed patch coordinate when the patch radius is q*K. No debt estimate is assumed.

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

theorem NavierStokes.TerminalCompensation.exists_heat_compensation (P : Patch) (lam : ℝ) (hlam : 0 ≤ lam) (T : OutgoingTail.TailData) (ν q : ℝ) (hν : 0 < ν) (hq : 0 < q) {U S : Set ℝ} (hU : IsOpen U) (hS : IsCompact S) (hSU : S ⊆ U) (a : ℝ → ℝ) (ha : ContDiffOn ℝ (↑⊤) a U) (hpos : ∀ η ∈ U, 0 < a η) : ∃ (K₀ : ℝ) (C : ℝ), 0 < K₀ ∧ 0 < C ∧ ∀ (K : ℝ), K₀ ≤ K → ∃ (c : ℝ → Coeff) (V : Set ℝ), IsOpen V ∧ S ⊆ V ∧ V ⊆ U ∧ ContDiffOn ℝ (↑⊤) c V ∧ ∀ η ∈ S, physicalMoments P lam (q * K) (a η) (c η) + heatDebt T ν K η = 0 ∧ ‖c η‖ ≤ C / K ∧ ‖deriv c η‖ ≤ C / K ∧ FirstJetBound P a c η (C / K) ∧ ∀ (X : ℝ), 0 < X → 0 < physicalProfile P lam (q * K) (a η) (c η) X

The actual outgoing heat edit is compensated for every sufficiently large radius, uniformly on the compact parameter range, with O(1/K) first-jet cost.

theorem NavierStokes.TerminalCompensation.physicalMoments_integrable (P : Patch) (lam R a : ℝ) (hR : 0 < R) (c : Coeff) : MeasureTheory.Integrable (fun (X : ℝ) => (physicalProfile P lam R a c X ^ 2 - cleanProfile lam R a X ^ 2) / X) MeasureTheory.volume ∧ MeasureTheory.Integrable (fun (X : ℝ) => physicalProfile P lam R a c X ^ 2 - cleanProfile lam R a X ^ 2) MeasureTheory.volume ∧ MeasureTheory.Integrable (fun (X : ℝ) => √(2 * X) * (physicalProfile P lam R a c X - cleanProfile lam R a X)) MeasureTheory.volume

All three physical moment changes are genuine integrable functions.

theorem NavierStokes.TerminalCompensation.physicalProfile_eq_clean_of_nonpos (P : Patch) (lam R a : ℝ) (hR : 0 < R) (c : Coeff) {X : ℝ} (hX : X ≤ 0) : physicalProfile P lam R a c X = cleanProfile lam R a X

theorem NavierStokes.TerminalCompensation.physicalMoments_positive_radius (P : Patch) (lam R a : ℝ) (hR : 0 < R) (c : Coeff) : physicalMoments P lam R a c = ![∫ (X : ℝ) in Set.Ioi 0, (physicalProfile P lam R a c X ^ 2 - cleanProfile lam R a X ^ 2) / X, ∫ (X : ℝ) in Set.Ioi 0, physicalProfile P lam R a c X ^ 2 - cleanProfile lam R a X ^ 2, ∫ (X : ℝ) in Set.Ioi 0, √(2 * X) * (physicalProfile P lam R a c X - cleanProfile lam R a X)]

The whole-line definitions equal the usual positive-radius moment integrals.

theorem NavierStokes.TerminalCompensation.patch_heat_disjoint (P : Patch) (lam q K a h ν : ℝ) (hq : 0 < q) (hK : 0 < K) (hpatch : q * P.right ≤ 1) (c : Coeff) (E : ℝ → ℝ) {X : ℝ} (hX : 0 < X) : (physicalProfile P lam (q * K) a c X - cleanProfile lam (q * K) a X) * HeatTailEdit.change E h ν K X = 0

A reserved patch ending before the heat switch has no overlap with the actual heat perturbation on positive radii.

theorem NavierStokes.TerminalCompensation.square_change_add_of_disjoint (b p t : ℝ) (hpt : p * t = 0) : (b + p + t) ^ 2 - b ^ 2 = (b + p) ^ 2 - b ^ 2 + ((b + t) ^ 2 - b ^ 2)

theorem NavierStokes.TerminalCompensation.physicalProfile_family_contDiffOn (P : Patch) (lam R : ℝ) (hR : 0 < R) {U : Set ℝ} {a : ℝ → ℝ} {c : ℝ → Coeff} (ha : ContDiffOn ℝ (↑⊤) a U) (hc : ContDiffOn ℝ (↑⊤) c U) : ContDiffOn ℝ (↑⊤) (fun (z : ℝ × ℝ) => physicalProfile P lam R (a z.1) (c z.1) z.2) (U ×ˢ Set.Ioi 0)

The constructed physical profile is jointly smooth in the parameter and positive radius, whenever the amplitude and solved coefficients are smooth.