Actual histories and moment repair for radial modulation

The normalized angular field is modulated multiplicatively, so the unchanged axis germ is retained. All history differences below are actual integrals.

@[reducible, inline]

abbrev NavierStokes.ModulatedHistories.Point : Type

Point: an abbreviation for ℝ × ℝ.

Equations

• NavierStokes.ModulatedHistories.Point = (ℝ × ℝ)

@[reducible, inline]

abbrev NavierStokes.ModulatedHistories.Field : Type

Field: an abbreviation for Point → ℝ.

Equations

• NavierStokes.ModulatedHistories.Field = (NavierStokes.ModulatedHistories.Point → ℝ)

@[reducible, inline]

abbrev NavierStokes.ModulatedHistories.Debt : Type

Debt: an abbreviation for FiveProfileMoments.Debt.

Equations

• NavierStokes.ModulatedHistories.Debt = NavierStokes.FiveProfileMoments.Debt

@[reducible, inline]

abbrev NavierStokes.ModulatedHistories.Coeff : Type

Coefficient: an abbreviation for FiveProfileMoments.Coeff.

Equations

• NavierStokes.ModulatedHistories.Coeff = NavierStokes.FiveProfileMoments.Coeff

structure NavierStokes.ModulatedHistories.Window : Type

Window data, collecting left, right, left_pos, ordered.

• left : ℝ

  Left of Window, of type ℝ.

• right : ℝ

  Right of Window, of type ℝ.

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

noncomputable def NavierStokes.ModulatedHistories.Window.clamp (W : Window) (X : ℝ) : ℝ

Clamp, given by projIcc W.left W.right W.ordered.le X.

Equations

• W.clamp X = ↑(Set.projIcc W.left W.right ⋯ X)

theorem NavierStokes.ModulatedHistories.Window.clamp_mem (W : Window) (X : ℝ) : W.clamp X ∈ Set.Icc W.left W.right

noncomputable def NavierStokes.ModulatedHistories.densityAt (X f U : ℝ) : Debt

Density at, given by ![U, 2 * X * f, U * (2 * X * f), U ^ 2 - X * f ^ 2, f ^ 2].

Equations

• NavierStokes.ModulatedHistories.densityAt X f U = ![U, 2 * X * f, U * (2 * X * f), U ^ 2 - X * f ^ 2, f ^ 2]

noncomputable def NavierStokes.ModulatedHistories.density (f U : Field) (p : Point) : Debt

Density, given by densityAt p.1 (f p) (U p).

Equations

• NavierStokes.ModulatedHistories.density f U p = NavierStokes.ModulatedHistories.densityAt p.1 (f p) (U p)

theorem NavierStokes.ModulatedHistories.density_contDiff (f U : Field) (hf : ContDiff ℝ (↑⊤) f) (hU : ContDiff ℝ (↑⊤) U) (i : Fin 5) : ContDiff ℝ ↑⊤ fun (p : Point) => density f U p i

theorem NavierStokes.ModulatedHistories.density_eq_physical (X f U : ℝ) (hX : 0 < X) : densityAt X f U = ![U, √(2 * X) * (√(2 * X) * f), U * √(2 * X) * (√(2 * X) * f), U ^ 2 - (√(2 * X) * f) ^ 2 / 2, (√(2 * X) * f) ^ 2 / (2 * X)]

noncomputable def NavierStokes.ModulatedHistories.rawF {a m p₁ p₂ : Point → ℝ} {K B : Set Point} (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f : Field) (N : ℝ) (p : Point) : ℝ

Raw F, given by ParametricModulation.realizedE r f N p.1 p.2.

Equations

• NavierStokes.ModulatedHistories.rawF r f N p = NavierStokes.ParametricModulation.realizedE r f N p.1 p.2

noncomputable def NavierStokes.ModulatedHistories.rawU {a m p₁ p₂ : Point → ℝ} {K B : Set Point} (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (E U : Field) (N : ℝ) (p : Point) : ℝ

Raw U, given by ParametricModulation.realizedU r E U N p.1 p.2.

Equations

• NavierStokes.ModulatedHistories.rawU r E U N p = NavierStokes.ParametricModulation.realizedU r E U N p.1 p.2

theorem NavierStokes.ModulatedHistories.rawF_physical {a m p₁ p₂ : Point → ℝ} {K B : Set Point} (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f E : Field) (N X eta : ℝ) (hE : E (X, eta) = √(2 * X) * f (X, eta)) : √(2 * X) * rawF r f N (X, eta) = ParametricModulation.realizedE r E N X eta

noncomputable def NavierStokes.ModulatedHistories.densityFamily {a m p₁ p₂ : Point → ℝ} {K B : Set Point} (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f E U : Field) (z : RadialModulation.FamilyPoint) : Debt

Density family, constructed using densityAt.

Equations

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

theorem NavierStokes.ModulatedHistories.densityFamily_contDiff {a m p₁ p₂ : Point → ℝ} {K B : Set Point} (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f E U : Field) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₂ : ContDiff ℝ (↑⊤) p₂) (hf : ContDiff ℝ (↑⊤) f) (hE : ContDiff ℝ (↑⊤) E) (hU : ContDiff ℝ (↑⊤) U) (i : Fin 5) : ContDiff ℝ ↑⊤ fun (z : RadialModulation.FamilyPoint) => densityFamily r f E U z i

theorem NavierStokes.ModulatedHistories.densityFamily_periodic {a m p₁ p₂ : Point → ℝ} {K B : Set Point} (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f E U : Field) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₂ : ContDiff ℝ (↑⊤) p₂) (eps X eta : ℝ) (i : Fin 5) : Function.Periodic (fun (theta : ℝ) => densityFamily r f E U (eps, X, eta, theta) i) 1

theorem NavierStokes.ModulatedHistories.densityFamily_zero {a m p₁ p₂ : Point → ℝ} {K B : Set Point} (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f E U : Field) (X eta theta : ℝ) : densityFamily r f E U (0, X, eta, theta) = density f U (X, eta)

theorem NavierStokes.ModulatedHistories.densityFamily_frequency {a m p₁ p₂ : Point → ℝ} {K B : Set Point} (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f E U : Field) (N X eta : ℝ) : densityFamily r f E U (1 / N, X, eta, N * Real.log X) = density (rawF r f N) (rawU r E U N) (X, eta)

theorem NavierStokes.ModulatedHistories.density_uniform_eta_jets {a m p₁ p₂ : Point → ℝ} {K B : Set Point} (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f E U : Field) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₂ : ContDiff ℝ (↑⊤) p₂) (hf : ContDiff ℝ (↑⊤) f) (hE : ContDiff ℝ (↑⊤) E) (hU : ContDiff ℝ (↑⊤) U) (KX S : Set ℝ) (hKX : IsCompact KX) (hS : IsCompact S) (q : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (N : ℝ), 1 ≤ N → ∀ X ∈ KX, ∀ eta ∈ S, ∀ j ≤ q, ∀ (i : Fin 5), |iteratedDeriv j (fun (e : ℝ) => density (rawF r f N) (rawU r E U N) (X, e) i) eta - iteratedDeriv j (fun (e : ℝ) => density f U (X, e) i) eta| ≤ C / N

noncomputable def NavierStokes.ModulatedHistories.densityDifference {a m p₁ p₂ : Point → ℝ} {K B : Set Point} (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f E U : Field) (N : ℝ) (p : Point) : Debt

Density difference, given by density (rawF r f N) (rawU r E U N) p - density f U p.

Equations

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

theorem NavierStokes.ModulatedHistories.densityDifference_contDiffAt {a m p₁ p₂ : Point → ℝ} {K B : Set Point} (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f E U : Field) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₂ : ContDiff ℝ (↑⊤) p₂) (hf : ContDiff ℝ (↑⊤) f) (hE : ContDiff ℝ (↑⊤) E) (hU : ContDiff ℝ (↑⊤) U) (N X eta : ℝ) (hX : X ≠ 0) (i : Fin 5) : ContDiffAt ℝ (↑⊤) (fun (p : Point) => densityDifference r f E U N p i) (X, eta)

noncomputable def NavierStokes.ModulatedHistories.historyDifference {a m p₁ p₂ : Point → ℝ} {K B : Set Point} (W : Window) (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f E U : Field) (N X eta : ℝ) : Debt

History difference, defined pointwise by ∫ s in W.left..W.clamp X, densityDifference r f E U N (s, eta) i.

Equations

• NavierStokes.ModulatedHistories.historyDifference W r f E U N X eta i = ∫ (s : ℝ) in W.left..W.clamp X, NavierStokes.ModulatedHistories.densityDifference r f E U N (s, eta) i

theorem NavierStokes.ModulatedHistories.historyDifference_smooth {a m p₁ p₂ : Point → ℝ} {K B : Set Point} (W : Window) (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f E U : Field) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₂ : ContDiff ℝ (↑⊤) p₂) (hf : ContDiff ℝ (↑⊤) f) (hE : ContDiff ℝ (↑⊤) E) (hU : ContDiff ℝ (↑⊤) U) (N X : ℝ) : ContDiff ℝ (↑⊤) (historyDifference W r f E U N X)

theorem NavierStokes.ModulatedHistories.density_raw_slice_smooth {a m p₁ p₂ : Point → ℝ} {K B : Set Point} (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f E U : Field) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₂ : ContDiff ℝ (↑⊤) p₂) (hf : ContDiff ℝ (↑⊤) f) (hE : ContDiff ℝ (↑⊤) E) (hU : ContDiff ℝ (↑⊤) U) (N X : ℝ) (i : Fin 5) : ContDiff ℝ ↑⊤ fun (eta : ℝ) => density (rawF r f N) (rawU r E U N) (X, eta) i

theorem NavierStokes.ModulatedHistories.historyDifference_scalar_jets {a m p₁ p₂ : Point → ℝ} {K B : Set Point} (W : Window) (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f E U : Field) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₂ : ContDiff ℝ (↑⊤) p₂) (hf : ContDiff ℝ (↑⊤) f) (hE : ContDiff ℝ (↑⊤) E) (hU : ContDiff ℝ (↑⊤) U) (S : Set ℝ) (hS : IsCompact S) (q : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (N : ℝ), 1 ≤ N → ∀ (X eta : ℝ), eta ∈ S → ∀ j ≤ q, ∀ (i : Fin 5), |iteratedDeriv j (fun (e : ℝ) => historyDifference W r f E U N X e i) eta| ≤ C / N

theorem NavierStokes.ModulatedHistories.clm_iteratedDeriv {F : Type u_1} {G : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (L : F →L[ℝ] G) {v : ℝ → F} (hv : ContDiff ℝ (↑⊤) v) (j : ℕ) (eta : ℝ) : iteratedDeriv j (fun (e : ℝ) => L (v e)) eta = L (iteratedDeriv j v eta)

theorem NavierStokes.ModulatedHistories.historyDifference_jets {a m p₁ p₂ : Point → ℝ} {K B : Set Point} (W : Window) (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f E U : Field) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₂ : ContDiff ℝ (↑⊤) p₂) (hf : ContDiff ℝ (↑⊤) f) (hE : ContDiff ℝ (↑⊤) E) (hU : ContDiff ℝ (↑⊤) U) (S : Set ℝ) (hS : IsCompact S) (q : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (N : ℝ), 1 ≤ N → ∀ (X : ℝ), JetBounds.FiniteJetBound q (historyDifference W r f E U N X) S (C / N)

Localization and genuine axis histories

noncomputable def NavierStokes.ModulatedHistories.splice (W : Window) (base actual : Field) (p : Point) : ℝ

Splice, with branches according to p.1 ∈ Ioc W.left W.right.

Equations

• NavierStokes.ModulatedHistories.splice W base actual p = if p.1 ∈ Set.Ioc W.left W.right then actual p else base p

theorem NavierStokes.ModulatedHistories.splice_eq_before (W : Window) (base actual : Field) {p : Point} (hp : p.1 ≤ W.left) : splice W base actual p = base p

theorem NavierStokes.ModulatedHistories.splice_eq_after (W : Window) (base actual : Field) {p : Point} (hp : W.right < p.1) : splice W base actual p = base p

theorem NavierStokes.ModulatedHistories.splice_eq_of_eq (W : Window) {base actual : Field} {p : Point} (hp : actual p = base p) : splice W base actual p = base p

theorem NavierStokes.ModulatedHistories.splice_contDiffOn (W : Window) {base actual : Field} {Ω : Set ℝ} (hbase : ContDiff ℝ (↑⊤) base) (hactual : ∀ (p : Point), p.1 ∈ Set.Icc W.left W.right → ContDiffAt ℝ (↑⊤) actual p) (hcollar : ∀ eta ∈ Ω, actual =ᶠ[nhds (W.left, eta)] base ∧ actual =ᶠ[nhds (W.right, eta)] base) : ContDiffOn ℝ (↑⊤) (splice W base actual) (Set.univ ×ˢ Ω)

noncomputable def NavierStokes.ModulatedHistories.localizedF {a m p₁ p₂ : Point → ℝ} {K B : Set Point} (W : Window) (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f : Field) (N : ℝ) : Field

Localized F, given by splice W f (rawF r f N).

Equations

• NavierStokes.ModulatedHistories.localizedF W r f N = NavierStokes.ModulatedHistories.splice W f (NavierStokes.ModulatedHistories.rawF r f N)

noncomputable def NavierStokes.ModulatedHistories.localizedU {a m p₁ p₂ : Point → ℝ} {K B : Set Point} (W : Window) (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (E U : Field) (N : ℝ) : Field

Localized U, given by splice W U (rawU r E U N).

Equations

• NavierStokes.ModulatedHistories.localizedU W r E U N = NavierStokes.ModulatedHistories.splice W U (NavierStokes.ModulatedHistories.rawU r E U N)

theorem NavierStokes.ModulatedHistories.localized_density_difference {a m p₁ p₂ : Point → ℝ} {K B : Set Point} (W : Window) (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f E U : Field) (N X eta : ℝ) (i : Fin 5) : density (localizedF W r f N) (localizedU W r E U N) (X, eta) i - density f U (X, eta) i = (Set.Ioc W.left W.right).indicator (fun (s : ℝ) => densityDifference r f E U N (s, eta) i) X

theorem NavierStokes.ModulatedHistories.integral_indicator_window (W : Window) (F : ℝ → ℝ) {X : ℝ} (hX : 0 ≤ X) : ∫ (s : ℝ) in 0..X, (Set.Ioc W.left W.right).indicator F s = ∫ (s : ℝ) in W.left..W.clamp X, F s

theorem NavierStokes.ModulatedHistories.densityDifference_continuousOn {a m p₁ p₂ : Point → ℝ} {K B : Set Point} (W : Window) (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f E U : Field) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₂ : ContDiff ℝ (↑⊤) p₂) (hf : ContDiff ℝ (↑⊤) f) (hE : ContDiff ℝ (↑⊤) E) (hU : ContDiff ℝ (↑⊤) U) (N eta : ℝ) (i : Fin 5) : ContinuousOn (fun (s : ℝ) => densityDifference r f E U N (s, eta) i) (Set.Icc W.left W.right)

noncomputable def NavierStokes.ModulatedHistories.axisHistory (f U : Field) (p : Point) : Debt

Axis history, defined pointwise by ∫ s in (0 : ℝ)..p.1, density f U (s, p.2) i.

Equations

• NavierStokes.ModulatedHistories.axisHistory f U p i = ∫ (s : ℝ) in 0..p.1, NavierStokes.ModulatedHistories.density f U (s, p.2) i

theorem NavierStokes.ModulatedHistories.axisHistory_localized_sub {a m p₁ p₂ : Point → ℝ} {K B : Set Point} (W : Window) (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f E U : Field) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₂ : ContDiff ℝ (↑⊤) p₂) (hf : ContDiff ℝ (↑⊤) f) (hE : ContDiff ℝ (↑⊤) E) (hU : ContDiff ℝ (↑⊤) U) (N X eta : ℝ) (hX : 0 ≤ X) : axisHistory (localizedF W r f N) (localizedU W r E U N) (X, eta) - axisHistory f U (X, eta) = historyDifference W r f E U N X eta

theorem NavierStokes.ModulatedHistories.actual_axisHistory_jets {a m p₁ p₂ : Point → ℝ} {K B : Set Point} (W : Window) (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f E U : Field) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₂ : ContDiff ℝ (↑⊤) p₂) (hf : ContDiff ℝ (↑⊤) f) (hE : ContDiff ℝ (↑⊤) E) (hU : ContDiff ℝ (↑⊤) U) (S : Set ℝ) (hS : IsCompact S) (q : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (N : ℝ), 1 ≤ N → ∀ (X : ℝ), 0 ≤ X → JetBounds.FiniteJetBound q (fun (eta : ℝ) => axisHistory (localizedF W r f N) (localizedU W r E U N) (X, eta) - axisHistory f U (X, eta)) S (C / N)

A linear finite-jet bound for the actual nonlinear inverse

theorem NavierStokes.ModulatedHistories.iteratedFDeriv_comp_clm_on {F : Type u_1} {G : Type u_2} {H : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedAddCommGroup H] [NormedSpace ℝ H] {g : G → H} {V : Set G} (hV : IsOpen V) (hg : ContDiffOn ℝ (↑⊤) g V) (L : F →L[ℝ] G) {x : F} (hx : L x ∈ V) (j : ℕ) : iteratedFDeriv ℝ j (g ∘ ⇑L) x = (iteratedFDeriv ℝ j g (L x)).compContinuousLinearMap fun (x : Fin j) => L

theorem NavierStokes.ModulatedHistories.smooth_solver_linear_jets {g : Coeff → Coeff} {r C : ℝ} (hr : 0 < r) (hC : 0 < C) (hg : ContDiffOn ℝ (↑⊤) g (Metric.ball 0 r)) (hvalue : ∀ z ∈ Metric.ball 0 r, ‖g z‖ ≤ C * ‖z‖) (q : ℕ) : ∃ (K : ℝ), 0 < K ∧ ∀ (f : ℝ → Coeff), ContDiff ℝ (↑⊤) f → ∀ (delta eta : ℝ), 0 < delta → delta ≤ min 1 (r / 2) → (∀ j ≤ q, ‖iteratedFDeriv ℝ j f eta‖ ≤ delta) → ∀ j ≤ q, ‖iteratedFDeriv ℝ j (g ∘ f) eta‖ ≤ K * delta

All finite jets retain the linear smallness of the input. The proof rescales the input and the inverse branch in opposite directions before applying the genuine higher chain-rule estimate.

Smooth localized profiles and the canonical pressure

theorem NavierStokes.ModulatedHistories.exists_smooth_localization {a m p₁ p₂ : Point → ℝ} {K B : Set Point} (W : Window) (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f E U : Field) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₂ : ContDiff ℝ (↑⊤) p₂) (hf : ContDiff ℝ (↑⊤) f) (hE : ContDiff ℝ (↑⊤) E) (hU : ContDiff ℝ (↑⊤) U) (S : Set ℝ) (hBK : B ⊆ K) (hends : ∀ eta ∈ S, (W.left, eta) ∈ B ∧ (W.right, eta) ∈ B) : ∃ (Ω : Set ℝ) (V : Set Point), IsOpen Ω ∧ S ⊆ Ω ∧ IsOpen V ∧ B ⊆ V ∧ (∀ (N : ℝ), ContDiffOn ℝ (↑⊤) (localizedF W r f N) (Set.univ ×ˢ Ω) ∧ ContDiffOn ℝ (↑⊤) (localizedU W r E U N) (Set.univ ×ˢ Ω)) ∧ ∀ (N : ℝ), ∀ p ∈ V, localizedF W r f N p = f p ∧ localizedU W r E U N p = U p

noncomputable def NavierStokes.ModulatedHistories.stripDomain (Ω : Set ℝ) (hΩ : IsOpen Ω) : ProfileHistories.RadialDomain

Strip domain, bundling carrier, isOpen, scale_mem.

Equations

• NavierStokes.ModulatedHistories.stripDomain Ω hΩ = { carrier := Set.univ ×ˢ Ω, isOpen := ⋯, scale_mem := ⋯ }

noncomputable def NavierStokes.ModulatedHistories.profiles (Ω : Set ℝ) (hΩ : IsOpen Ω) (f U : Field) (P0 : ℝ → ℝ) (hf : ContDiffOn ℝ (↑⊤) f (Set.univ ×ˢ Ω)) (hU : ContDiffOn ℝ (↑⊤) U (Set.univ ×ˢ Ω)) (hP0 : ContDiffOn ℝ (↑⊤) P0 Ω) : ProfileHistories.Profiles (stripDomain Ω hΩ)

Profiles, bundling f, U, f_smooth, U_smooth and the required compatibility proofs.

Equations

• NavierStokes.ModulatedHistories.profiles Ω hΩ f U P0 hf hU hP0 = { f := f, U := U, f_smooth := hf, U_smooth := hU, pressure0 := P0, pressure0_smooth := ⋯ }

noncomputable def NavierStokes.ModulatedHistories.profileRows {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (p : Point) : Debt

Profile rows, given by ![P.M p, P.I p, P.J p, P.S p, P.pressure p].

Equations

• NavierStokes.ModulatedHistories.profileRows P p = ![P.M p, P.I p, P.J p, P.S p, P.pressure p]

theorem NavierStokes.ModulatedHistories.profileRows_eq_axisHistory {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (p : Point) : profileRows P p = axisHistory P.f P.U p + Pi.single 4 (P.pressure0 p.2)

theorem NavierStokes.ModulatedHistories.profileRows_sub {D D' : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (Q : ProfileHistories.Profiles D') (hp : P.pressure0 = Q.pressure0) (p : Point) : profileRows P p - profileRows Q p = axisHistory P.f P.U p - axisHistory Q.f Q.U p

An actual small five-row correction

theorem NavierStokes.ModulatedHistories.smooth_extension_ball {g : Coeff → Coeff} {r : ℝ} (hr : 0 < r) (hg : ContDiffOn ℝ (↑⊤) g (Metric.ball 0 r)) : ∃ (G : Coeff → Coeff), ContDiff ℝ (↑⊤) G ∧ Set.EqOn G g (Metric.ball 0 (r / 2))

theorem NavierStokes.ModulatedHistories.repair_family_rate (P : FiveProfileMoments.Patch) (b : ℝ) (hb : FiveProfileMoments.GoodExponent b) (S : Set ℝ) (hS : IsCompact S) (A G : ℝ → ℝ) (hA : ContDiff ℝ (↑⊤) A) (hG : ContDiff ℝ (↑⊤) G) (hApos : ∀ (eta : ℝ), 0 < A eta) (q : ℕ) (d : ℝ → ℝ → Debt) (hd : ∀ (N : ℝ), ContDiff ℝ (↑⊤) (d N)) (D : ℝ) (hD : 0 < D) (hdb : ∀ (N : ℝ), 1 ≤ N → JetBounds.FiniteJetBound q (d N) S (D / N)) : ∃ (N0 : ℝ) (C : ℝ), 1 ≤ N0 ∧ 0 < C ∧ ∀ (N : ℝ), N0 ≤ N → ∃ (c : ℝ → Coeff) (V : Set ℝ), ContDiff ℝ (↑⊤) c ∧ IsOpen V ∧ S ⊆ V ∧ (∀ eta ∈ V, FiveProfileMoments.physicalMoments P b (A eta) (G eta) (c eta) = d N eta ∧ ∀ (X : ℝ), 0 < X → 0 < FiveProfileMoments.physicalE P b (A eta) (c eta) X) ∧ JetBounds.FiniteJetBound q c S (C / N)

The inverse branch is constructed once, then applied to the actual debt family. The extension outside its small ball only supplies a globally smooth coefficient curve; every asserted moment identity is inside the original branch.

noncomputable def NavierStokes.ModulatedHistories.repairDebt {a m p₁ p₂ : Point → ℝ} {K B : Set Point} (W : Window) (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f E U : Field) (N eta : ℝ) : Debt

Repair debt, given by -historyDifference W r f E U N W.right eta.

Equations

• NavierStokes.ModulatedHistories.repairDebt W r f E U N eta = -NavierStokes.ModulatedHistories.historyDifference W r f E U N W.right eta

theorem NavierStokes.ModulatedHistories.actual_repair_family {a m p₁ p₂ : Point → ℝ} {K B : Set Point} (W : Window) (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f E U : Field) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₂ : ContDiff ℝ (↑⊤) p₂) (hf : ContDiff ℝ (↑⊤) f) (hE : ContDiff ℝ (↑⊤) E) (hU : ContDiff ℝ (↑⊤) U) (P : FiveProfileMoments.Patch) (b : ℝ) (hb : FiveProfileMoments.GoodExponent b) (S : Set ℝ) (hS : IsCompact S) (A G : ℝ → ℝ) (hA : ContDiff ℝ (↑⊤) A) (hG : ContDiff ℝ (↑⊤) G) (hApos : ∀ (eta : ℝ), 0 < A eta) (q : ℕ) : ∃ (N0 : ℝ) (C : ℝ), 1 ≤ N0 ∧ 0 < C ∧ ∀ (N : ℝ), N0 ≤ N → ∃ (c : ℝ → Coeff) (V : Set ℝ), ContDiff ℝ (↑⊤) c ∧ IsOpen V ∧ S ⊆ V ∧ (∀ eta ∈ V, FiveProfileMoments.physicalMoments P b (A eta) (G eta) (c eta) = repairDebt W r f E U N eta ∧ ∀ (X : ℝ), 0 < X → 0 < FiveProfileMoments.physicalE P b (A eta) (c eta) X) ∧ JetBounds.FiniteJetBound q c S (C / N)

theorem NavierStokes.ModulatedHistories.finiteJet_smul {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {q : ℕ} {A : ℝ → ℝ} {c : ℝ → F} {S : Set ℝ} {B C : ℝ} (hA : ContDiff ℝ (↑⊤) A) (hc : ContDiff ℝ (↑⊤) c) (hB : 0 ≤ B) (hC : 0 ≤ C) (hAb : JetBounds.FiniteJetBound q A S B) (hcb : JetBounds.FiniteJetBound q c S C) : JetBounds.FiniteJetBound q (fun (eta : ℝ) => A eta • c eta) S (2 ^ q * B * C)

noncomputable def NavierStokes.ModulatedHistories.editU (P : FiveProfileMoments.Patch) (A : ℝ → ℝ) (c : ℝ → Coeff) (p : Point) : ℝ

Edit U, given by A p.2 * FiveProfileMoments.u P (c p.2) p.1.

Equations

• NavierStokes.ModulatedHistories.editU P A c p = A p.2 * NavierStokes.FiveProfileMoments.u P (c p.2) p.1

noncomputable def NavierStokes.ModulatedHistories.editE (P : FiveProfileMoments.Patch) (A : ℝ → ℝ) (c : ℝ → Coeff) (p : Point) : ℝ

Edit E, given by A p.2 * FiveProfileMoments.e P (c p.2) p.1.

Equations

• NavierStokes.ModulatedHistories.editE P A c p = A p.2 * NavierStokes.FiveProfileMoments.e P (c p.2) p.1

noncomputable def NavierStokes.ModulatedHistories.editF (P : FiveProfileMoments.Patch) (A : ℝ → ℝ) (c : ℝ → Coeff) (p : Point) : ℝ

Edit F, given by editE P A c p / Real.sqrt (2 * p.1).

Equations

• NavierStokes.ModulatedHistories.editF P A c p = NavierStokes.ModulatedHistories.editE P A c p / √(2 * p.1)

noncomputable def NavierStokes.ModulatedHistories.applyRepairF (P : FiveProfileMoments.Patch) (A : ℝ → ℝ) (c : ℝ → Coeff) (f : Field) (p : Point) : ℝ

Apply repair F, given by f p + editF P A c p.

Equations

• NavierStokes.ModulatedHistories.applyRepairF P A c f p = f p + NavierStokes.ModulatedHistories.editF P A c p

noncomputable def NavierStokes.ModulatedHistories.applyRepairU (P : FiveProfileMoments.Patch) (A : ℝ → ℝ) (c : ℝ → Coeff) (U : Field) (p : Point) : ℝ

Apply repair U, given by U p + editU P A c p.

Equations

• NavierStokes.ModulatedHistories.applyRepairU P A c U p = U p + NavierStokes.ModulatedHistories.editU P A c p

theorem NavierStokes.ModulatedHistories.editU_contDiff (P : FiveProfileMoments.Patch) (A : ℝ → ℝ) (c : ℝ → Coeff) (hA : ContDiff ℝ (↑⊤) A) (hc : ContDiff ℝ (↑⊤) c) : ContDiff ℝ (↑⊤) (editU P A c)

theorem NavierStokes.ModulatedHistories.editE_contDiff (P : FiveProfileMoments.Patch) (A : ℝ → ℝ) (c : ℝ → Coeff) (hA : ContDiff ℝ (↑⊤) A) (hc : ContDiff ℝ (↑⊤) c) : ContDiff ℝ (↑⊤) (editE P A c)

theorem NavierStokes.ModulatedHistories.edits_zero_outside (P : FiveProfileMoments.Patch) (A : ℝ → ℝ) (c : ℝ → Coeff) {p : Point} (hp : p.1 ∉ Set.Ioo P.left P.right) : editU P A c p = 0 ∧ editE P A c p = 0 ∧ editF P A c p = 0

theorem NavierStokes.ModulatedHistories.editF_contDiff (P : FiveProfileMoments.Patch) (A : ℝ → ℝ) (c : ℝ → Coeff) (hA : ContDiff ℝ (↑⊤) A) (hc : ContDiff ℝ (↑⊤) c) : ContDiff ℝ (↑⊤) (editF P A c)

theorem NavierStokes.ModulatedHistories.repair_preserves_outside (P : FiveProfileMoments.Patch) (A : ℝ → ℝ) (c : ℝ → Coeff) (f U : Field) {p : Point} (hp : p.1 ∉ Set.Ioo P.left P.right) : applyRepairF P A c f p = f p ∧ applyRepairU P A c U p = U p

theorem NavierStokes.ModulatedHistories.repair_preserves_radial_germ (P : FiveProfileMoments.Patch) (A : ℝ → ℝ) (c : ℝ → Coeff) (f U : Field) (X eta : ℝ) (hX : X ∉ Set.Ioo P.left P.right) : ((fun (x : ℝ) => applyRepairF P A c f (x, eta)) =ᶠ[nhds X] fun (x : ℝ) => f (x, eta)) ∧ (fun (x : ℝ) => applyRepairU P A c U (x, eta)) =ᶠ[nhds X] fun (x : ℝ) => U (x, eta)

theorem NavierStokes.ModulatedHistories.physical_mixed_edits_bound (P : FiveProfileMoments.Patch) (S : Set ℝ) (hS : IsCompact S) (A : ℝ → ℝ) (hA : ContDiff ℝ (↑⊤) A) (q : ℕ) : ∃ (K : ℝ), 0 < K ∧ ∀ (c : ℝ → Coeff), ContDiff ℝ (↑⊤) c → ∀ (eps : ℝ), 0 ≤ eps → JetBounds.FiniteJetBound q c S eps → ∀ eta ∈ S, ∀ k ≤ q, ∀ j ≤ q, ∀ (X : ℝ), ‖iteratedFDeriv ℝ j (fun (e : ℝ) => iteratedDeriv k (fun (x : ℝ) => editU P A c (x, e)) X) eta‖ ≤ K * eps ∧ ‖iteratedFDeriv ℝ j (fun (e : ℝ) => iteratedDeriv k (fun (x : ℝ) => editE P A c (x, e)) X) eta‖ ≤ K * eps

Exact restoration beyond the reserved patch

theorem NavierStokes.ModulatedHistories.normalized_density_change (X f U dE dU : ℝ) (hX : 0 < X) : densityAt X (f + dE / √(2 * X)) (U + dU) - densityAt X f U = FiveProfileMoments.profileChangeDensity (fun (x : ℝ) => U) (fun (x : ℝ) => √(2 * X) * f) (fun (x : ℝ) => dU) (fun (x : ℝ) => dE) X

theorem NavierStokes.ModulatedHistories.density_repair_change (P : FiveProfileMoments.Patch) (b : ℝ) (A G : ℝ → ℝ) (c : ℝ → Coeff) (f U : Field) (eta : ℝ) (hU : ∀ X ∈ Set.Ioo P.left P.right, U (X, eta) = G eta) (hE : ∀ X ∈ Set.Ioo P.left P.right, √(2 * X) * f (X, eta) = A eta * X ^ b) (X : ℝ) : density (applyRepairF P A c f) (applyRepairU P A c U) (X, eta) - density f U (X, eta) = FiveProfileMoments.physicalDensity P b (A eta) (G eta) (c eta) X

theorem NavierStokes.ModulatedHistories.axisHistory_repair_sub (P : FiveProfileMoments.Patch) (b : ℝ) (A G : ℝ → ℝ) (c : ℝ → Coeff) (f U : Field) (eta X : ℝ) (hX : P.right ≤ X) (hA : A eta ≠ 0) (hU : ∀ x ∈ Set.Ioo P.left P.right, U (x, eta) = G eta) (hE : ∀ x ∈ Set.Ioo P.left P.right, √(2 * x) * f (x, eta) = A eta * x ^ b) (hi : ∀ (i : Fin 5), IntervalIntegrable (fun (x : ℝ) => density f U (x, eta) i) MeasureTheory.volume 0 X) : axisHistory (applyRepairF P A c f) (applyRepairU P A c U) (X, eta) - axisHistory f U (X, eta) = FiveProfileMoments.physicalMoments P b (A eta) (G eta) (c eta)

theorem NavierStokes.ModulatedHistories.localized_density_integrable {a m p₁ p₂ : Point → ℝ} {K B : Set Point} (W : Window) (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f E U : Field) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₂ : ContDiff ℝ (↑⊤) p₂) (hf : ContDiff ℝ (↑⊤) f) (hE : ContDiff ℝ (↑⊤) E) (hU : ContDiff ℝ (↑⊤) U) (N X eta : ℝ) (i : Fin 5) : IntervalIntegrable (fun (s : ℝ) => density (localizedF W r f N) (localizedU W r E U N) (s, eta) i) MeasureTheory.volume 0 X

theorem NavierStokes.ModulatedHistories.actual_histories_restored {a m p₁ p₂ : Point → ℝ} {K B : Set Point} (W : Window) (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f E U : Field) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₂ : ContDiff ℝ (↑⊤) p₂) (hf : ContDiff ℝ (↑⊤) f) (hE : ContDiff ℝ (↑⊤) E) (hU : ContDiff ℝ (↑⊤) U) (P : FiveProfileMoments.Patch) (hWP : W.right < P.left) (b : ℝ) (A G : ℝ → ℝ) (c : ℝ → Coeff) (N eta X : ℝ) (hX : P.right ≤ X) (hA : A eta ≠ 0) (hpatchU : ∀ x ∈ Set.Ioo P.left P.right, U (x, eta) = G eta) (hpatchE : ∀ x ∈ Set.Ioo P.left P.right, √(2 * x) * f (x, eta) = A eta * x ^ b) (hrepair : FiveProfileMoments.physicalMoments P b (A eta) (G eta) (c eta) = repairDebt W r f E U N eta) : axisHistory (applyRepairF P A c (localizedF W r f N)) (applyRepairU P A c (localizedU W r E U N)) (X, eta) = axisHistory f U (X, eta)

Quantitative histories throughout the repair

theorem NavierStokes.ModulatedHistories.deriv_add_bound {f g : ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (n : ℕ) (eta B C : ℝ) (hB : |iteratedDeriv n f eta| ≤ B) (hC : |iteratedDeriv n g eta| ≤ C) : |iteratedDeriv n (fun (e : ℝ) => f e + g e) eta| ≤ B + C

theorem NavierStokes.ModulatedHistories.deriv_sub_bound {f g : ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (n : ℕ) (eta B C : ℝ) (hB : |iteratedDeriv n f eta| ≤ B) (hC : |iteratedDeriv n g eta| ≤ C) : |iteratedDeriv n (fun (e : ℝ) => f e - g e) eta| ≤ B + C

theorem NavierStokes.ModulatedHistories.deriv_const_mul_bound {f : ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (eta t B : ℝ) (hB : |iteratedDeriv n f eta| ≤ B) : |iteratedDeriv n (fun (e : ℝ) => t * f e) eta| ≤ |t| * B

theorem NavierStokes.ModulatedHistories.density_perturbation_jet_bound (f U df dU : ℝ → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hU : ContDiff ℝ (↑⊤) U) (hdf : ContDiff ℝ (↑⊤) df) (hdU : ContDiff ℝ (↑⊤) dU) (n : ℕ) (eta X R B eps : ℝ) (hR : 0 ≤ R) (hX : |X| ≤ R) (hB : 0 ≤ B) (heps : 0 ≤ eps) (heps1 : eps ≤ 1) (hfb : ∀ j ≤ n, |iteratedDeriv j f eta| ≤ B) (hUb : ∀ j ≤ n, |iteratedDeriv j U eta| ≤ B) (hdfb : ∀ j ≤ n, |iteratedDeriv j df eta| ≤ eps) (hdUb : ∀ j ≤ n, |iteratedDeriv j dU eta| ≤ eps) (i : Fin 5) : |iteratedDeriv n (fun (e : ℝ) => (densityAt X (f e + df e) (U e + dU e) - densityAt X (f e) (U e)) i) eta| ≤ (1 + 2 * R) * (1 + 2 ^ n * (2 * B + 1)) * eps

theorem NavierStokes.ModulatedHistories.compact_eta_jet_bound (F : Field) (hF : ContDiff ℝ (↑⊤) F) (KX S : Set ℝ) (hKX : IsCompact KX) (hS : IsCompact S) (q : ℕ) : ∃ (B : ℝ), 0 < B ∧ ∀ X ∈ KX, ∀ eta ∈ S, ∀ j ≤ q, |iteratedDeriv j (fun (e : ℝ) => F (X, e)) eta| ≤ B

theorem NavierStokes.ModulatedHistories.normalized_edits_eta_bound (P : FiveProfileMoments.Patch) (S : Set ℝ) (hS : IsCompact S) (A : ℝ → ℝ) (hA : ContDiff ℝ (↑⊤) A) (q : ℕ) : ∃ (K : ℝ), 0 < K ∧ ∀ (c : ℝ → Coeff), ContDiff ℝ (↑⊤) c → ∀ (eps : ℝ), 0 ≤ eps → JetBounds.FiniteJetBound q c S eps → ∀ eta ∈ S, ∀ j ≤ q, ∀ (X : ℝ), |iteratedDeriv j (fun (e : ℝ) => editF P A c (X, e)) eta| ≤ K * eps ∧ |iteratedDeriv j (fun (e : ℝ) => editU P A c (X, e)) eta| ≤ K * eps

noncomputable def NavierStokes.ModulatedHistories.patchWindow (P : FiveProfileMoments.Patch) : Window

Patch window, given by ⟨P.left, P.right, P.left_pos, P.ordered⟩.

Equations

• NavierStokes.ModulatedHistories.patchWindow P = { left := P.left, right := P.right, left_pos := ⋯, ordered := ⋯ }

noncomputable def NavierStokes.ModulatedHistories.repairDensity (P : FiveProfileMoments.Patch) (A : ℝ → ℝ) (c : ℝ → Coeff) (f U : Field) (p : Point) : Debt

Repair density, given by density (applyRepairF P A c f) (applyRepairU P A c U) p - density f U p.

Equations

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

noncomputable def NavierStokes.ModulatedHistories.repairHistoryDifference (P : FiveProfileMoments.Patch) (A : ℝ → ℝ) (c : ℝ → Coeff) (f U : Field) (X eta : ℝ) : Debt

Repair history difference, defined pointwise by ∫ s in P.left..(patchWindow P).clamp X, repairDensity P A c f U (s, eta) i.

Equations

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

theorem NavierStokes.ModulatedHistories.repairDensity_contDiff (P : FiveProfileMoments.Patch) (A : ℝ → ℝ) (c : ℝ → Coeff) (f U : Field) (hA : ContDiff ℝ (↑⊤) A) (hc : ContDiff ℝ (↑⊤) c) (hf : ContDiff ℝ (↑⊤) f) (hU : ContDiff ℝ (↑⊤) U) (i : Fin 5) : ContDiff ℝ ↑⊤ fun (p : Point) => repairDensity P A c f U p i

theorem NavierStokes.ModulatedHistories.repairHistory_smooth (P : FiveProfileMoments.Patch) (A : ℝ → ℝ) (c : ℝ → Coeff) (f U : Field) (hA : ContDiff ℝ (↑⊤) A) (hc : ContDiff ℝ (↑⊤) c) (hf : ContDiff ℝ (↑⊤) f) (hU : ContDiff ℝ (↑⊤) U) (X : ℝ) : ContDiff ℝ (↑⊤) (repairHistoryDifference P A c f U X)

theorem NavierStokes.ModulatedHistories.repairHistory_scalar_jets (P : FiveProfileMoments.Patch) (S : Set ℝ) (hS : IsCompact S) (A : ℝ → ℝ) (f U : Field) (hA : ContDiff ℝ (↑⊤) A) (hf : ContDiff ℝ (↑⊤) f) (hU : ContDiff ℝ (↑⊤) U) (q : ℕ) : ∃ (delta : ℝ) (K : ℝ), 0 < delta ∧ 0 < K ∧ ∀ (c : ℝ → Coeff), ContDiff ℝ (↑⊤) c → ∀ (eps : ℝ), 0 ≤ eps → eps ≤ delta → JetBounds.FiniteJetBound q c S eps → ∀ (X eta : ℝ), eta ∈ S → ∀ j ≤ q, ∀ (i : Fin 5), |iteratedDeriv j (fun (e : ℝ) => repairHistoryDifference P A c f U X e i) eta| ≤ K * eps

theorem NavierStokes.ModulatedHistories.repairHistory_jets (P : FiveProfileMoments.Patch) (S : Set ℝ) (hS : IsCompact S) (A : ℝ → ℝ) (f U : Field) (hA : ContDiff ℝ (↑⊤) A) (hf : ContDiff ℝ (↑⊤) f) (hU : ContDiff ℝ (↑⊤) U) (q : ℕ) : ∃ (delta : ℝ) (K : ℝ), 0 < delta ∧ 0 < K ∧ ∀ (c : ℝ → Coeff), ContDiff ℝ (↑⊤) c → ∀ (eps : ℝ), 0 ≤ eps → eps ≤ delta → JetBounds.FiniteJetBound q c S eps → ∀ (X : ℝ), JetBounds.FiniteJetBound q (repairHistoryDifference P A c f U X) S (K * eps)

theorem NavierStokes.ModulatedHistories.repairDensity_zero_outside (P : FiveProfileMoments.Patch) (A : ℝ → ℝ) (c : ℝ → Coeff) (f U : Field) {p : Point} (hp : p.1 ∉ Set.Ioo P.left P.right) : repairDensity P A c f U p = 0

theorem NavierStokes.ModulatedHistories.repairDensity_localized {a m p₁ p₂ : Point → ℝ} {K B : Set Point} (W : Window) (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f E U : Field) (P : FiveProfileMoments.Patch) (hWP : W.right < P.left) (A : ℝ → ℝ) (c : ℝ → Coeff) (N : ℝ) (p : Point) : repairDensity P A c (localizedF W r f N) (localizedU W r E U N) p = repairDensity P A c f U p

theorem NavierStokes.ModulatedHistories.actual_repair_history_identity {a m p₁ p₂ : Point → ℝ} {K B : Set Point} (W : Window) (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f E U : Field) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₂ : ContDiff ℝ (↑⊤) p₂) (hf : ContDiff ℝ (↑⊤) f) (hE : ContDiff ℝ (↑⊤) E) (hU : ContDiff ℝ (↑⊤) U) (P : FiveProfileMoments.Patch) (hWP : W.right < P.left) (A : ℝ → ℝ) (c : ℝ → Coeff) (hA : ContDiff ℝ (↑⊤) A) (hc : ContDiff ℝ (↑⊤) c) (N X eta : ℝ) (hX : 0 ≤ X) : axisHistory (applyRepairF P A c (localizedF W r f N)) (applyRepairU P A c (localizedU W r E U N)) (X, eta) - axisHistory (localizedF W r f N) (localizedU W r E U N) (X, eta) = repairHistoryDifference P A c f U X eta

theorem NavierStokes.ModulatedHistories.repaired_axisHistory_identity {a m p₁ p₂ : Point → ℝ} {K B : Set Point} (W : Window) (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f E U : Field) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₂ : ContDiff ℝ (↑⊤) p₂) (hf : ContDiff ℝ (↑⊤) f) (hE : ContDiff ℝ (↑⊤) E) (hU : ContDiff ℝ (↑⊤) U) (P : FiveProfileMoments.Patch) (hWP : W.right < P.left) (A : ℝ → ℝ) (c : ℝ → Coeff) (hA : ContDiff ℝ (↑⊤) A) (hc : ContDiff ℝ (↑⊤) c) (N X eta : ℝ) (hX : 0 ≤ X) : axisHistory (applyRepairF P A c (localizedF W r f N)) (applyRepairU P A c (localizedU W r E U N)) (X, eta) - axisHistory f U (X, eta) = historyDifference W r f E U N X eta + repairHistoryDifference P A c f U X eta

theorem NavierStokes.ModulatedHistories.repaired_axisHistory_jets {a m p₁ p₂ : Point → ℝ} {K B : Set Point} (W : Window) (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f E U : Field) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₂ : ContDiff ℝ (↑⊤) p₂) (hf : ContDiff ℝ (↑⊤) f) (hE : ContDiff ℝ (↑⊤) E) (hU : ContDiff ℝ (↑⊤) U) (P : FiveProfileMoments.Patch) (hWP : W.right < P.left) (A : ℝ → ℝ) (hA : ContDiff ℝ (↑⊤) A) (S : Set ℝ) (hS : IsCompact S) (q : ℕ) : ∃ (delta : ℝ) (C1 : ℝ) (C2 : ℝ), 0 < delta ∧ 0 < C1 ∧ 0 < C2 ∧ ∀ (N : ℝ), 1 ≤ N → ∀ (c : ℝ → Coeff), ContDiff ℝ (↑⊤) c → ∀ (eps : ℝ), 0 ≤ eps → eps ≤ delta → JetBounds.FiniteJetBound q c S eps → ∀ (X : ℝ), 0 ≤ X → JetBounds.FiniteJetBound q (fun (eta : ℝ) => axisHistory (applyRepairF P A c (localizedF W r f N)) (applyRepairU P A c (localizedU W r E U N)) (X, eta) - axisHistory f U (X, eta)) S (C1 / N + C2 * eps)

Uniform in the frequency, the upper endpoint, and every actual smooth coefficient curve with the stated small finite jets. In particular choosing the constructed repair with eps=C/N retains the 1/N rate.

theorem NavierStokes.ModulatedHistories.exists_actual_restoring_repair {a m p₁ p₂ : Point → ℝ} {K B : Set Point} (W : Window) (r : ParametricModulation.TrueConeRealization a m p₁ p₂ K B) (f E U : Field) (ha : ContDiff ℝ (↑⊤) a) (hm : ContDiff ℝ (↑⊤) m) (hp₂ : ContDiff ℝ (↑⊤) p₂) (hf : ContDiff ℝ (↑⊤) f) (hE : ContDiff ℝ (↑⊤) E) (hU : ContDiff ℝ (↑⊤) U) (P : FiveProfileMoments.Patch) (hWP : W.right < P.left) (b : ℝ) (hb : FiveProfileMoments.GoodExponent b) (A G : ℝ → ℝ) (hA : ContDiff ℝ (↑⊤) A) (hG : ContDiff ℝ (↑⊤) G) (hApos : ∀ (eta : ℝ), 0 < A eta) (S J : Set ℝ) (hS : IsCompact S) (hJ : IsOpen J) (hSJ : S ⊆ J) (hpatchU : ∀ eta ∈ J, ∀ X ∈ Set.Ioo P.left P.right, U (X, eta) = G eta) (hpatchE : ∀ eta ∈ J, ∀ X ∈ Set.Ioo P.left P.right, √(2 * X) * f (X, eta) = A eta * X ^ b) (q : ℕ) : ∃ (N0 : ℝ) (C : ℝ), 1 ≤ N0 ∧ 0 < C ∧ ∀ (N : ℝ), N0 ≤ N → ∃ (c : ℝ → Coeff) (V : Set ℝ), ContDiff ℝ (↑⊤) c ∧ IsOpen V ∧ S ⊆ V ∧ V ⊆ J ∧ JetBounds.FiniteJetBound q c S (C / N) ∧ ∀ eta ∈ V, ∀ (X : ℝ), P.right ≤ X → axisHistory (applyRepairF P A c (localizedF W r f N)) (applyRepairU P A c (localizedU W r E U N)) (X, eta) = axisHistory f U (X, eta)

An actual smooth correction for every sufficiently large frequency, with exact restoration on an open parameter neighborhood. Its debt is the integral of the constructed modulation, rather than an assumed small row.

theorem NavierStokes.ModulatedHistories.profileRows_eq_of_axisHistory_eq {D D' : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (Q : ProfileHistories.Profiles D') (hP0 : P.pressure0 = Q.pressure0) {p : Point} (h : axisHistory P.f P.U p = axisHistory Q.f Q.U p) : profileRows P p = profileRows Q p