Five actual profile moments on a reserved positive patch

Two axial bumps and three angular bumps are supported in disjoint halves of the patch. Positive amplitude factoring removes the background parameters from the normalized quadratic system.

structure NavierStokes.FiveProfileMoments.Patch : Type

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

• 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.FiveProfileMoments.Patch.mid (P : Patch) : ℝ

Mid, given by (P.left + P.right) / 2.

Equations

• P.mid = (P.left + P.right) / 2

noncomputable def NavierStokes.FiveProfileMoments.Patch.leftHalf (P : Patch) : Patch

Left half, given by ⟨P.left, P.mid, P.left_pos, by dsimp [Patch.mid]; linarith [P.ordered]⟩.

Equations

• P.leftHalf = { left := P.left, right := P.mid, left_pos := ⋯, ordered := ⋯ }

noncomputable def NavierStokes.FiveProfileMoments.Patch.rightHalf (P : Patch) : Patch

Right half, given by ⟨P.mid, P.right, by dsimp [Patch.mid]; linarith [P.left_pos, P.ordered], by dsimp [Patch.mid]; linarith [P.ordered]⟩.

Equations

• P.rightHalf = { left := P.mid, right := P.right, left_pos := ⋯, ordered := ⋯ }

noncomputable def NavierStokes.FiveProfileMoments.lower {n : ℕ} (P : Patch) (j : Fin n) : ℝ

Lower, given by FiveRowRank.cellLower P.left P.right j.

Equations

• NavierStokes.FiveProfileMoments.lower P j = NavierStokes.FiveRowRank.cellLower P.left P.right j

noncomputable def NavierStokes.FiveProfileMoments.upper {n : ℕ} (P : Patch) (j : Fin n) : ℝ

Upper, given by FiveRowRank.cellUpper P.left P.right j.

Equations

• NavierStokes.FiveProfileMoments.upper P j = NavierStokes.FiveRowRank.cellUpper P.left P.right j

noncomputable def NavierStokes.FiveProfileMoments.bump {n : ℕ} (P : Patch) (j : Fin n) : ℝ → ℝ

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

Equations

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

theorem NavierStokes.FiveProfileMoments.lower_gt_left {n : ℕ} (P : Patch) (j : Fin n) : P.left < lower P j

theorem NavierStokes.FiveProfileMoments.lower_lt_upper {n : ℕ} (P : Patch) (j : Fin n) : lower P j < upper P j

theorem NavierStokes.FiveProfileMoments.upper_lt_right {n : ℕ} (P : Patch) (j : Fin n) : upper P j < P.right

theorem NavierStokes.FiveProfileMoments.intervals_separated {n : ℕ} (P : Patch) (i j : Fin n) (hij : i < j) : upper P i ≤ lower P j

theorem NavierStokes.FiveProfileMoments.bump_contDiff {n : ℕ} (P : Patch) (j : Fin n) : ContDiff ℝ (↑⊤) (bump P j)

theorem NavierStokes.FiveProfileMoments.bump_tsupport {n : ℕ} (P : Patch) (j : Fin n) : tsupport (bump P j) ⊆ Set.Ioo (lower P j) (upper P j)

theorem NavierStokes.FiveProfileMoments.bump_support_patch {n : ℕ} (P : Patch) (j : Fin n) : Function.support (bump P j) ⊆ Set.Icc P.left P.right

theorem NavierStokes.FiveProfileMoments.bumps_disjoint {n : ℕ} (P : Patch) (i j : Fin n) (hij : i ≠ j) (x : ℝ) : bump P i x * bump P j x = 0

noncomputable def NavierStokes.FiveProfileMoments.correction {n : ℕ} (P : Patch) (c : Fin n → ℝ) (x : ℝ) : ℝ

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

Equations

• NavierStokes.FiveProfileMoments.correction P c x = ∑ j : Fin n, c j * NavierStokes.FiveProfileMoments.bump P j x

theorem NavierStokes.FiveProfileMoments.correction_contDiff {n : ℕ} (P : Patch) (c : Fin n → ℝ) : ContDiff ℝ (↑⊤) (correction P c)

theorem NavierStokes.FiveProfileMoments.correction_support {n : ℕ} (P : Patch) (c : Fin n → ℝ) : Function.support (correction P c) ⊆ Set.Icc P.left P.right

theorem NavierStokes.FiveProfileMoments.correction_tsupport {n : ℕ} (P : Patch) (c : Fin n → ℝ) : tsupport (correction P c) ⊆ Set.Ioo P.left P.right

theorem NavierStokes.FiveProfileMoments.correction_hasCompactSupport {n : ℕ} (P : Patch) (c : Fin n → ℝ) : HasCompactSupport (correction P c)

theorem NavierStokes.FiveProfileMoments.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.FiveProfileMoments.correction_square {n : ℕ} (P : Patch) (c : Fin n → ℝ) (x : ℝ) : correction P c x ^ 2 = ∑ j : Fin n, c j ^ 2 * bump P j x ^ 2

noncomputable def NavierStokes.FiveProfileMoments.bumpMoment {n : ℕ} (P : Patch) (s : ℝ) (j : Fin n) : ℝ

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

Equations

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

noncomputable def NavierStokes.FiveProfileMoments.squareMoment {n : ℕ} (P : Patch) (s : ℝ) (j : Fin n) : ℝ

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

Equations

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

theorem NavierStokes.FiveProfileMoments.weighted_correction_integrable {n : ℕ} (P : Patch) (s : ℝ) (c : Fin n → ℝ) : MeasureTheory.Integrable (fun (x : ℝ) => x ^ s * correction P c x) MeasureTheory.volume

theorem NavierStokes.FiveProfileMoments.weighted_square_integrable {n : ℕ} (P : Patch) (s : ℝ) (c : Fin n → ℝ) : MeasureTheory.Integrable (fun (x : ℝ) => x ^ s * correction P c x ^ 2) MeasureTheory.volume

theorem NavierStokes.FiveProfileMoments.correction_moment {n : ℕ} (P : Patch) (s : ℝ) (c : Fin n → ℝ) : ∫ (x : ℝ), x ^ s * correction P c x = ∑ j : Fin n, c j * bumpMoment P s j

theorem NavierStokes.FiveProfileMoments.correction_square_moment {n : ℕ} (P : Patch) (s : ℝ) (c : Fin n → ℝ) : ∫ (x : ℝ), x ^ s * correction P c x ^ 2 = ∑ j : Fin n, c j ^ 2 * squareMoment P s j

noncomputable def NavierStokes.FiveProfileMoments.momentMatrix {n : ℕ} (P : Patch) (a : Fin n → ℝ) : Matrix (Fin n) (Fin n) ℝ

Moment matrix, given by LocalizedMomentRepair.matrix a (lower P) (upper P).

Equations

• NavierStokes.FiveProfileMoments.momentMatrix P a = NavierStokes.LocalizedMomentRepair.matrix a (NavierStokes.FiveProfileMoments.lower P) (NavierStokes.FiveProfileMoments.upper P)

theorem NavierStokes.FiveProfileMoments.momentMatrix_det_ne_zero {n : ℕ} (P : Patch) (a : Fin n → ℝ) (ha : Function.Injective a) : (momentMatrix P a).det ≠ 0

noncomputable def NavierStokes.FiveProfileMoments.matrixEquiv {n : ℕ} (P : Patch) (a : Fin n → ℝ) (ha : Function.Injective a) : (Fin n → ℝ) ≃L[ℝ] Fin n → ℝ

Matrix equiv, constructed using LinearEquiv.toContinuousLinearEquiv.

Equations

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

theorem NavierStokes.FiveProfileMoments.matrixEquiv_apply {n : ℕ} (P : Patch) (a : Fin n → ℝ) (ha : Function.Injective a) (c : Fin n → ℝ) (i : Fin n) : (matrixEquiv P a ha) c i = ∫ (x : ℝ), x ^ a i * correction P c x

theorem NavierStokes.FiveProfileMoments.correction_iteratedDeriv {n : ℕ} (P : Patch) (c : Fin n → ℝ) (k : ℕ) (x : ℝ) : iteratedDeriv k (correction P c) x = ∑ j : Fin n, c j * iteratedDeriv k (bump P j) x

theorem NavierStokes.FiveProfileMoments.correction_derivative_bound {n : ℕ} (P : Patch) (k : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (c : Fin n → ℝ) (x : ℝ), |iteratedDeriv k (correction P c) x| ≤ C * ‖c‖

@[reducible, inline]

abbrev NavierStokes.FiveProfileMoments.Coeff : Type

Coefficient: an abbreviation for (Fin 2 → ℝ) × (Fin 3 → ℝ).

Equations

• NavierStokes.FiveProfileMoments.Coeff = ((Fin 2 → ℝ) × (Fin 3 → ℝ))

@[reducible, inline]

abbrev NavierStokes.FiveProfileMoments.Debt : Type

Debt: an abbreviation for Fin 5 → ℝ.

Equations

• NavierStokes.FiveProfileMoments.Debt = (Fin 5 → ℝ)

def NavierStokes.FiveProfileMoments.GoodExponent (b : ℝ) : Prop

Good exponent, given by b ≠ -1 / 2 ∧ b ≠ 1 / 2 ∧ b ≠ 3 / 2.

Equations

• NavierStokes.FiveProfileMoments.GoodExponent b = (b ≠ -1 / 2 ∧ b ≠ 1 / 2 ∧ b ≠ 3 / 2)

theorem NavierStokes.FiveProfileMoments.good_initial : GoodExponent (1 / 10)

theorem NavierStokes.FiveProfileMoments.good_outgoing (lam : ℝ) (hlam : 0 < lam) : GoodExponent (-1 / 2 - lam)

noncomputable def NavierStokes.FiveProfileMoments.axialPowers (b : ℝ) : Fin 2 → ℝ

Axial powers, given by ![0, b + 1 / 2].

Equations

• NavierStokes.FiveProfileMoments.axialPowers b = ![0, b + 1 / 2]

noncomputable def NavierStokes.FiveProfileMoments.angularPowers (b : ℝ) : Fin 3 → ℝ

Angular powers, given by ![1 / 2, b, b - 1].

Equations

• NavierStokes.FiveProfileMoments.angularPowers b = ![1 / 2, b, b - 1]

theorem NavierStokes.FiveProfileMoments.axialPowers_injective (b : ℝ) (hb : GoodExponent b) : Function.Injective (axialPowers b)

theorem NavierStokes.FiveProfileMoments.angularPowers_injective (b : ℝ) (hb : GoodExponent b) : Function.Injective (angularPowers b)

noncomputable def NavierStokes.FiveProfileMoments.u (P : Patch) (c : Coeff) : ℝ → ℝ

U, given by correction P.leftHalf c.1.

Equations

• NavierStokes.FiveProfileMoments.u P c = NavierStokes.FiveProfileMoments.correction P.leftHalf c.1

noncomputable def NavierStokes.FiveProfileMoments.e (P : Patch) (c : Coeff) : ℝ → ℝ

E, given by correction P.rightHalf c.2.

Equations

• NavierStokes.FiveProfileMoments.e P c = NavierStokes.FiveProfileMoments.correction P.rightHalf c.2

theorem NavierStokes.FiveProfileMoments.u_mul_e (P : Patch) (c d : Coeff) (x : ℝ) : u P c x * e P d x = 0

noncomputable def NavierStokes.FiveProfileMoments.linearEquiv (P : Patch) (b : ℝ) (hb : GoodExponent b) : Coeff ≃L[ℝ] Coeff

Linear equiv as an element of Coeff ≃L[ℝ] Coeff.

Equations

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

noncomputable def NavierStokes.FiveProfileMoments.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.FiveProfileMoments.quadraticCLM (P : Patch) : Coeff →L[ℝ] Coeff →L[ℝ] Coeff

Quadratic continuous linear map, constructed using LinearMap.toContinuousLinearMap.

Equations

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

noncomputable def NavierStokes.FiveProfileMoments.normalizedMap (P : Patch) (b : ℝ) (c : Coeff) : Coeff

Normalized map as an element of Coeff.

Equations

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

theorem NavierStokes.FiveProfileMoments.linearEquiv_apply (P : Patch) (b : ℝ) (hb : GoodExponent b) (c : Coeff) : (linearEquiv P b hb) c = (![∫ (x : ℝ), u P c x, ∫ (x : ℝ), x ^ (b + 1 / 2) * u P c x], ![∫ (x : ℝ), x ^ (1 / 2) * e P c x, ∫ (x : ℝ), x ^ b * e P c x, ∫ (x : ℝ), x ^ (b - 1) * e P c x])

theorem NavierStokes.FiveProfileMoments.normalizedMap_identity (P : Patch) (b : ℝ) (hb : GoodExponent b) (c : Coeff) : (linearEquiv P b hb) c + ((quadraticCLM P) c) c = normalizedMap P b c

theorem NavierStokes.FiveProfileMoments.spatial_jet_bound (P : Patch) (k : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (c : Coeff) (x : ℝ), |iteratedDeriv k (u P c) x| ≤ C * ‖c‖ ∧ |iteratedDeriv k (e P c) x| ≤ C * ‖c‖

theorem NavierStokes.FiveProfileMoments.finite_spatial_jet_bound (P : Patch) (N : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ k ≤ N, ∀ (c : Coeff) (x : ℝ), |iteratedDeriv k (u P c) x| ≤ C * ‖c‖ ∧ |iteratedDeriv k (e P c) x| ≤ C * ‖c‖

theorem NavierStokes.FiveProfileMoments.power_lower_bound (P : Patch) (b : ℝ) : ∃ (m : ℝ), 0 < m ∧ ∀ x ∈ Set.Icc P.left P.right, m ≤ x ^ b

theorem NavierStokes.FiveProfileMoments.exists_normalized_repair (P : Patch) (b : ℝ) (hb : GoodExponent b) : ∃ (g : Coeff → Coeff) (ε : ℝ) (C : ℝ), 0 < ε ∧ 0 < C ∧ ContDiffOn ℝ (↑⊤) g (Metric.ball 0 ε) ∧ g 0 = 0 ∧ ∀ d ∈ Metric.ball 0 ε, normalizedMap P b (g d) = d ∧ ‖g d‖ ≤ C * ‖d‖ ∧ ‖fderiv ℝ g d‖ ≤ C ∧ ∀ (x : ℝ), 0 < x → 0 < x ^ b + e P (g d) x

One fixed nonlinear inverse works for all amplitudes and constant axial backgrounds, because they have been factored out of the actual moments.

noncomputable def NavierStokes.FiveProfileMoments.physicalU (P : Patch) (A G : ℝ) (c : Coeff) (x : ℝ) : ℝ

Physical U, given by G + A * u P c x.

Equations

• NavierStokes.FiveProfileMoments.physicalU P A G c x = G + A * NavierStokes.FiveProfileMoments.u P c x

noncomputable def NavierStokes.FiveProfileMoments.physicalE (P : Patch) (b A : ℝ) (c : Coeff) (x : ℝ) : ℝ

Physical E, given by A * (x ^ b + e P c x).

Equations

• NavierStokes.FiveProfileMoments.physicalE P b A c x = A * (x ^ b + NavierStokes.FiveProfileMoments.e P c x)

noncomputable def NavierStokes.FiveProfileMoments.physicalDensity (P : Patch) (b A G : ℝ) (c : Coeff) (x : ℝ) : Debt

Physical density as an element of Debt.

Equations

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

noncomputable def NavierStokes.FiveProfileMoments.physicalMoments (P : Patch) (b A G : ℝ) (c : Coeff) : Debt

Physical moments, defined pointwise by ∫ x, physicalDensity P b A G c x i.

Equations

• NavierStokes.FiveProfileMoments.physicalMoments P b A G c i = ∫ (x : ℝ), NavierStokes.FiveProfileMoments.physicalDensity P b A G c x i

noncomputable def NavierStokes.FiveProfileMoments.physicalDebt (A G : ℝ) (z : Coeff) : Debt

Physical debt as an element of Debt.

Equations

• NavierStokes.FiveProfileMoments.physicalDebt A G z = ![A * z.1 0, √2 * A * z.2 0, √2 * A ^ 2 * z.1 1 + G * (√2 * A * z.2 0), 2 * G * A * z.1 0 - A ^ 2 * z.2 1, A ^ 2 * z.2 2]

noncomputable def NavierStokes.FiveProfileMoments.normalizedDebt (A G : ℝ) (d : Debt) : Coeff

Normalized debt, given by (![d 0 / A, (d 2 - G * d 1) / (Real.sqrt 2 * A ^ 2)], ![d 1 / (Real.sqrt 2 * A), (2 * G * d 0 - d 3) / A ^ 2, d 4 / A ^ 2]).

Equations

• NavierStokes.FiveProfileMoments.normalizedDebt A G d = (![d 0 / A, (d 2 - G * d 1) / (√2 * A ^ 2)], ![d 1 / (√2 * A), (2 * G * d 0 - d 3) / A ^ 2, d 4 / A ^ 2])

theorem NavierStokes.FiveProfileMoments.physical_normalized_debt (A G : ℝ) (hA : A ≠ 0) (d : Debt) : physicalDebt A G (normalizedDebt A G d) = d

theorem NavierStokes.FiveProfileMoments.normalized_physical_debt (A G : ℝ) (hA : A ≠ 0) (c : Coeff) : normalizedDebt A G (physicalDebt A G c) = c

noncomputable def NavierStokes.FiveProfileMoments.physicalEquiv (A G : ℝ) (hA : A ≠ 0) : Coeff ≃L[ℝ] Debt

Physical equiv, constructed using LinearEquiv.toContinuousLinearEquiv.

Equations

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

noncomputable def NavierStokes.FiveProfileMoments.normalizedDensity (P : Patch) (b : ℝ) (c : Coeff) (x : ℝ) : Coeff

Normalized density as an element of Coeff.

Equations

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

theorem NavierStokes.FiveProfileMoments.physicalDensity_eq (P : Patch) (b A G : ℝ) (c : Coeff) (x : ℝ) : physicalDensity P b A G c x = physicalDebt A G (normalizedDensity P b c x)

theorem NavierStokes.FiveProfileMoments.integrable_fin_vector {n : ℕ} (f : ℝ → Fin n → ℝ) (hf : ∀ (i : Fin n), MeasureTheory.Integrable (fun (x : ℝ) => f x i) MeasureTheory.volume) : MeasureTheory.Integrable f MeasureTheory.volume

theorem NavierStokes.FiveProfileMoments.integral_fin_apply {n : ℕ} {f : ℝ → Fin n → ℝ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (i : Fin n) : (∫ (x : ℝ), f x) i = ∫ (x : ℝ), f x i

theorem NavierStokes.FiveProfileMoments.integral_fst_apply {f : ℝ → Coeff} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (i : Fin 2) : (∫ (x : ℝ), f x).1 i = ∫ (x : ℝ), (f x).1 i

theorem NavierStokes.FiveProfileMoments.integral_snd_apply {f : ℝ → Coeff} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (i : Fin 3) : (∫ (x : ℝ), f x).2 i = ∫ (x : ℝ), (f x).2 i

theorem NavierStokes.FiveProfileMoments.normalizedDensity_integrable (P : Patch) (b : ℝ) (c : Coeff) : MeasureTheory.Integrable (normalizedDensity P b c) MeasureTheory.volume

theorem NavierStokes.FiveProfileMoments.normalizedDensity_integral (P : Patch) (b : ℝ) (c : Coeff) : ∫ (x : ℝ), normalizedDensity P b c x = normalizedMap P b c

theorem NavierStokes.FiveProfileMoments.physicalMoments_eq (P : Patch) (b A G : ℝ) (hA : A ≠ 0) (c : Coeff) : physicalMoments P b A G c = physicalDebt A G (normalizedMap P b c)

noncomputable def NavierStokes.FiveProfileMoments.actualLinearEquiv (P : Patch) (b A G : ℝ) (hb : GoodExponent b) (hA : A ≠ 0) : Coeff ≃L[ℝ] Debt

The full physical derivative in the five raw bump coefficients is an explicit continuous linear equivalence. Its two actual moment determinants were proved nonzero above.

Equations

• NavierStokes.FiveProfileMoments.actualLinearEquiv P b A G hb hA = (NavierStokes.FiveProfileMoments.linearEquiv P b hb).trans (NavierStokes.FiveProfileMoments.physicalEquiv A G hA)

theorem NavierStokes.FiveProfileMoments.physicalMoments_hasFDerivAt_zero (P : Patch) (b A G : ℝ) (hb : GoodExponent b) (hA : A ≠ 0) : HasFDerivAt (physicalMoments P b A G) (↑(actualLinearEquiv P b A G hb hA)) 0

theorem NavierStokes.FiveProfileMoments.physicalDensity_zero_outside (P : Patch) (b A G : ℝ) (c : Coeff) {x : ℝ} (hx : x ∉ Set.Ioo P.left P.right) : physicalDensity P b A G c x = 0

theorem NavierStokes.FiveProfileMoments.physicalMoments_positive_axis (P : Patch) (b A G : ℝ) (c : Coeff) (i : Fin 5) : ∫ (x : ℝ) in Set.Ioi 0, physicalDensity P b A G c x i = physicalMoments P b A G c i

theorem NavierStokes.FiveProfileMoments.physicalDensity_integrable (P : Patch) (b A G : ℝ) (hA : A ≠ 0) (c : Coeff) (i : Fin 5) : MeasureTheory.Integrable (fun (x : ℝ) => physicalDensity P b A G c x i) MeasureTheory.volume

noncomputable def NavierStokes.FiveProfileMoments.normalizationLinearMap (A G : ℝ) : Debt →ₗ[ℝ] Coeff

Normalization linear map, bundling toFun, map_add, map_smul.

Equations

• NavierStokes.FiveProfileMoments.normalizationLinearMap A G = { toFun := NavierStokes.FiveProfileMoments.normalizedDebt A G, map_add' := ⋯, map_smul' := ⋯ }

theorem NavierStokes.FiveProfileMoments.normalizedDebt_contDiffOn {S : Set ℝ} {A G : ℝ → ℝ} {d : ℝ → Debt} (hA : ContDiffOn ℝ (↑⊤) A S) (hG : ContDiffOn ℝ (↑⊤) G S) (hd : ContDiffOn ℝ (↑⊤) d S) (hAn : ∀ p ∈ S, A p ≠ 0) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ) => normalizedDebt (A p) (G p) (d p)) S

theorem NavierStokes.FiveProfileMoments.normalizedDebt_contDiff {A G : ℝ → ℝ} {d : ℝ → Debt} (hA : ContDiff ℝ (↑⊤) A) (hG : ContDiff ℝ (↑⊤) G) (hd : ContDiff ℝ (↑⊤) d) (hAn : ∀ (p : ℝ), A p ≠ 0) : ContDiff ℝ ↑⊤ fun (p : ℝ) => normalizedDebt (A p) (G p) (d p)

theorem NavierStokes.FiveProfileMoments.normalizedDebt_eq_sum (A G : ℝ) (d : Debt) : normalizedDebt A G d = ∑ i : Fin 5, d i • normalizedDebt A G (Pi.single i 1)

theorem NavierStokes.FiveProfileMoments.compact_normalization_bound (S : Set ℝ) (hS : IsCompact S) {A G : ℝ → ℝ} (hA : ContDiffOn ℝ (↑⊤) A S) (hG : ContDiffOn ℝ (↑⊤) G S) (hAn : ∀ p ∈ S, A p ≠ 0) : ∃ (K : ℝ), 0 < K ∧ ∀ p ∈ S, ∀ (d : Debt), ‖normalizedDebt (A p) (G p) d‖ ≤ K * ‖d‖

theorem NavierStokes.FiveProfileMoments.correction_family_contDiffOn {n : ℕ} (P : Patch) {S : Set ℝ} {c : ℝ → Fin n → ℝ} (hc : ContDiffOn ℝ (↑⊤) c S) : ContDiffOn ℝ (↑⊤) (fun (z : ℝ × ℝ) => correction P (c z.1) z.2) (S ×ˢ Set.univ)

theorem NavierStokes.FiveProfileMoments.physicalU_family_contDiffOn (P : Patch) {S : Set ℝ} {A G : ℝ → ℝ} {c : ℝ → Coeff} (hA : ContDiffOn ℝ (↑⊤) A S) (hG : ContDiffOn ℝ (↑⊤) G S) (hc : ContDiffOn ℝ (↑⊤) c S) : ContDiffOn ℝ (↑⊤) (fun (z : ℝ × ℝ) => physicalU P (A z.1) (G z.1) (c z.1) z.2) (S ×ˢ Set.univ)

theorem NavierStokes.FiveProfileMoments.physicalE_family_contDiffOn (P : Patch) (b : ℝ) {S : Set ℝ} {A : ℝ → ℝ} {c : ℝ → Coeff} (hA : ContDiffOn ℝ (↑⊤) A S) (hc : ContDiffOn ℝ (↑⊤) c S) : ContDiffOn ℝ (↑⊤) (fun (z : ℝ × ℝ) => physicalE P b (A z.1) (c z.1) z.2) (S ×ˢ Set.Ioi 0)

theorem NavierStokes.FiveProfileMoments.compact_parameter_repair (P : Patch) (b : ℝ) (hb : GoodExponent b) (S : Set ℝ) (hS : IsCompact S) (A G : ℝ → ℝ) (hA : ContDiff ℝ (↑⊤) A) (hG : ContDiff ℝ (↑⊤) G) (hApos : ∀ (p : ℝ), 0 < A p) (N : ℕ) : ∃ (ε : ℝ) (K : ℝ), 0 < ε ∧ 0 < K ∧ ∀ (d : ℝ → Debt), ContDiff ℝ (↑⊤) d → (∀ p ∈ S, ‖d p‖ < ε) → ∃ (c : ℝ → Coeff) (V : Set ℝ), IsOpen V ∧ S ⊆ V ∧ ContDiffOn ℝ (↑⊤) c V ∧ (∀ p ∈ V, physicalMoments P b (A p) (G p) (c p) = d p ∧ ∀ (x : ℝ), 0 < x → 0 < physicalE P b (A p) (c p) x) ∧ ∀ p ∈ S, ‖c p‖ ≤ K * ‖d p‖ ∧ ∀ k ≤ N, ∀ (x : ℝ), |iteratedDeriv k (fun (y : ℝ) => A p * u P (c p) y) x| ≤ K * ‖d p‖ ∧ |iteratedDeriv k (fun (y : ℝ) => A p * e P (c p) y) x| ≤ K * ‖d p‖

Every fixed finite spatial jet of the physical edits is small with the physical debt, uniformly on compact parameter sets. The actual coefficient branch is smooth on an open neighborhood of the compact set.

theorem NavierStokes.FiveProfileMoments.smooth_solver_jet_bound {g : Coeff → Coeff} {r : ℝ} (hr : 0 < r) (hg : ContDiffOn ℝ (↑⊤) g (Metric.ball 0 r)) (N : ℕ) : ∃ (B : ℝ), 0 < B ∧ ∀ k ≤ N, ∀ z ∈ Metric.closedBall 0 (r / 2), ‖iteratedFDeriv ℝ k g z‖ ≤ B

theorem NavierStokes.FiveProfileMoments.smooth_solver_parameter_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‖) (N : ℕ) : ∃ (K : ℝ), 0 < K ∧ ∀ (f : ℝ → Coeff), ContDiff ℝ (↑⊤) f → ∀ (tau x : ℝ), 0 < tau → tau ≤ min 1 (r / 2) → (∀ j ≤ N, ‖iteratedFDeriv ℝ j f x‖ ≤ tau ^ (N + 1)) → ∀ k ≤ N, ‖iteratedFDeriv ℝ k (g ∘ f) x‖ ≤ K * tau

Genuine higher parameter jets of the nonlinear branch are small when the corresponding normalized-debt jets are small. The stronger input scale tau^(N+1) gives a simple uniform linear output scale for every order ≤N. No derivatives of the solution are supplied as hypotheses.

noncomputable def NavierStokes.FiveProfileMoments.jetEval {n : ℕ} (P : Patch) (k : ℕ) (x : ℝ) : (Fin n → ℝ) →L[ℝ] ℝ

Jet eval, constructed using LinearMap.toContinuousLinearMap.

Equations

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

noncomputable def NavierStokes.FiveProfileMoments.uJetEval (P : Patch) (k : ℕ) (x : ℝ) : Coeff →L[ℝ] ℝ

U jet eval, given by (jetEval P.leftHalf k x).comp (ContinuousLinearMap.fst ℝ _ _).

Equations

• NavierStokes.FiveProfileMoments.uJetEval P k x = NavierStokes.FiveProfileMoments.jetEval P.leftHalf k x ∘SL ContinuousLinearMap.fst ℝ (Fin 2 → ℝ) (Fin 3 → ℝ)

noncomputable def NavierStokes.FiveProfileMoments.eJetEval (P : Patch) (k : ℕ) (x : ℝ) : Coeff →L[ℝ] ℝ

E jet eval, given by (jetEval P.rightHalf k x).comp (ContinuousLinearMap.snd ℝ _ _).

Equations

• NavierStokes.FiveProfileMoments.eJetEval P k x = NavierStokes.FiveProfileMoments.jetEval P.rightHalf k x ∘SL ContinuousLinearMap.snd ℝ (Fin 2 → ℝ) (Fin 3 → ℝ)

theorem NavierStokes.FiveProfileMoments.uJetEval_apply (P : Patch) (k : ℕ) (x : ℝ) (c : Coeff) : (uJetEval P k x) c = iteratedDeriv k (u P c) x

theorem NavierStokes.FiveProfileMoments.eJetEval_apply (P : Patch) (k : ℕ) (x : ℝ) (c : Coeff) : (eJetEval P k x) c = iteratedDeriv k (e P c) x

theorem NavierStokes.FiveProfileMoments.linear_parameter_jet_bound (L : Coeff →L[ℝ] ℝ) {v : ℝ → Coeff} {eta : ℝ} (hv : ContDiffAt ℝ (↑⊤) v eta) (m : ℕ) : ‖iteratedFDeriv ℝ m (⇑L ∘ v) eta‖ ≤ ‖L‖ * ‖iteratedFDeriv ℝ m v eta‖

theorem NavierStokes.FiveProfileMoments.mixed_jet_bound (P : Patch) (N : ℕ) : ∃ (J : ℝ), 0 < J ∧ ∀ k ≤ N, ∀ (m : ℕ) (v : ℝ → Coeff) (eta : ℝ), ContDiffAt ℝ (↑⊤) v eta → ∀ (x : ℝ), ‖iteratedFDeriv ℝ m (fun (p : ℝ) => iteratedDeriv k (u P (v p)) x) eta‖ ≤ J * ‖iteratedFDeriv ℝ m v eta‖ ∧ ‖iteratedFDeriv ℝ m (fun (p : ℝ) => iteratedDeriv k (e P (v p)) x) eta‖ ≤ J * ‖iteratedFDeriv ℝ m v eta‖

Every mixed parameter/radial jet of the actual fixed bump family is controlled by the corresponding parameter jet of its coefficients.

theorem NavierStokes.FiveProfileMoments.physical_mixed_jets_small (P : Patch) {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‖) (N : ℕ) : ∃ (K : ℝ), 0 < K ∧ ∀ (V : Set ℝ), IsOpen V → ∀ (f : ℝ → Coeff) (A : ℝ → ℝ), ContDiff ℝ (↑⊤) f → ContDiffOn ℝ (↑⊤) A V → ∀ (B tau : ℝ), 0 ≤ B → 0 < tau → tau ≤ min 1 (r / 2) → JetBounds.FiniteJetBound N A V B → JetBounds.FiniteJetBound N f V (tau ^ (N + 1)) → ∀ eta ∈ V, ∀ k ≤ N, ∀ m ≤ N, ∀ (x : ℝ), ‖iteratedFDeriv ℝ m (fun (p : ℝ) => iteratedDeriv k (fun (y : ℝ) => A p * u P (g (f p)) y) x) eta‖ ≤ K * B * tau ∧ ‖iteratedFDeriv ℝ m (fun (p : ℝ) => iteratedDeriv k (fun (y : ℝ) => A p * e P (g (f p)) y) x) eta‖ ≤ K * B * tau

Full mixed jets of both physical edits tend to zero with finite jets of the normalized debt. Bounds on the fixed smooth amplitude are kept explicit. This applies directly to the solver constructed in exists_normalized_repair.

theorem NavierStokes.FiveProfileMoments.u_tsupport_patch (P : Patch) (c : Coeff) : tsupport (u P c) ⊆ Set.Ioo P.left P.right

theorem NavierStokes.FiveProfileMoments.e_tsupport_patch (P : Patch) (c : Coeff) : tsupport (e P c) ⊆ Set.Ioo P.left P.right

theorem NavierStokes.FiveProfileMoments.u_zero_outside (P : Patch) (c : Coeff) {x : ℝ} (hx : x ∉ Set.Ioo P.left P.right) : u P c x = 0

theorem NavierStokes.FiveProfileMoments.e_zero_outside (P : Patch) (c : Coeff) {x : ℝ} (hx : x ∉ Set.Ioo P.left P.right) : e P c x = 0

theorem NavierStokes.FiveProfileMoments.physical_profiles_unchanged (P : Patch) (b A G : ℝ) (c : Coeff) {x : ℝ} (hx : x ∉ Set.Ioo P.left P.right) : physicalU P A G c x = G ∧ physicalE P b A c x = A * x ^ b

theorem NavierStokes.FiveProfileMoments.physical_edits_tsupport (P : Patch) (A : ℝ) (c : Coeff) : (tsupport fun (x : ℝ) => A * u P c x) ⊆ Set.Ioo P.left P.right ∧ (tsupport fun (x : ℝ) => A * e P c x) ⊆ Set.Ioo P.left P.right

noncomputable def NavierStokes.FiveProfileMoments.profileChangeDensity (U E dU dE : ℝ → ℝ) (x : ℝ) : Debt

Profile change density as an element of Debt.

Equations

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

theorem NavierStokes.FiveProfileMoments.local_profile_change (P : Patch) (b A G : ℝ) (c : Coeff) (U E : ℝ → ℝ) (hU : ∀ x ∈ Set.Ioo P.left P.right, U x = G) (hE : ∀ x ∈ Set.Ioo P.left P.right, E x = A * x ^ b) (x : ℝ) : profileChangeDensity U E (fun (y : ℝ) => A * u P c y) (fun (y : ℝ) => A * e P c y) x = physicalDensity P b A G c x

Only agreement with the power background on the reserved patch is needed; the profiles outside the patch are arbitrary and are preserved exactly.

theorem NavierStokes.FiveProfileMoments.local_profile_moments (P : Patch) (b A G : ℝ) (c : Coeff) (U E : ℝ → ℝ) (hU : ∀ x ∈ Set.Ioo P.left P.right, U x = G) (hE : ∀ x ∈ Set.Ioo P.left P.right, E x = A * x ^ b) (i : Fin 5) : ∫ (x : ℝ) in Set.Ioi 0, profileChangeDensity U E (fun (y : ℝ) => A * u P c y) (fun (y : ℝ) => A * e P c y) x i = physicalMoments P b A G c i

noncomputable def NavierStokes.FiveProfileMoments.normalizationCLM (A G : ℝ) : Debt →L[ℝ] Coeff

Normalization continuous linear map, given by ∑ i : Fin 5, ContinuousLinearMap.smulRightL ℝ Debt Coeff (ContinuousLinearMap.proj i) (normalizedDebt A G (Pi.single i 1)).

Equations

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

theorem NavierStokes.FiveProfileMoments.normalizationCLM_apply (A G : ℝ) (d : Debt) : (normalizationCLM A G) d = normalizedDebt A G d

theorem NavierStokes.FiveProfileMoments.normalizationCLM_contDiff {A G : ℝ → ℝ} (hA : ContDiff ℝ (↑⊤) A) (hG : ContDiff ℝ (↑⊤) G) (hAn : ∀ (p : ℝ), A p ≠ 0) : ContDiff ℝ ↑⊤ fun (p : ℝ) => normalizationCLM (A p) (G p)

theorem NavierStokes.FiveProfileMoments.compact_global_jet_bound {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (S : Set ℝ) (hS : IsCompact S) {f : ℝ → F} (hf : ContDiff ℝ (↑⊤) f) (N : ℕ) : ∃ (K : ℝ), 0 < K ∧ JetBounds.FiniteJetBound N f S K

theorem NavierStokes.FiveProfileMoments.compact_normalizedDebt_jets (S : Set ℝ) (hS : IsCompact S) {A G : ℝ → ℝ} (hA : ContDiff ℝ (↑⊤) A) (hG : ContDiff ℝ (↑⊤) G) (hAn : ∀ (p : ℝ), A p ≠ 0) (N : ℕ) : ∃ (K : ℝ), 0 < K ∧ ∀ (d : ℝ → Debt), ContDiff ℝ (↑⊤) d → ∀ (D : ℝ), 0 ≤ D → JetBounds.FiniteJetBound N d S D → JetBounds.FiniteJetBound N (fun (p : ℝ) => normalizedDebt (A p) (G p) (d p)) S (K * D)

The fixed smooth weights in the normalization preserve smallness of every finite parameter jet. This bridges physical row estimates to the nonlinear solver's normalized-debt estimates.