The five-row rank repair on an unaltered power-law patch

For V(R) = C R^(-1 - 2 lam) and G = 0, the five linear rows of the manuscript are solved by two concrete smooth compactly supported functions. The three angular and two axial powers are proved distinct when lam > 0. No nonsingularity or preimage is assumed: the profiles use the constructed localized moment inverse.

@[reducible, inline]

abbrev NavierStokes.FiveRowRank.Debt : Type

The three debts, in the order (P, Jθ, Jz).

Equations

• NavierStokes.FiveRowRank.Debt = (Fin 3 → ℝ)

noncomputable def NavierStokes.FiveRowRank.cellStep (a b : ℝ) (n : ℕ) : ℝ

A positive mesh with unused gaps between the correction intervals.

Equations

• NavierStokes.FiveRowRank.cellStep a b n = (b - a) / (2 * ↑n + 1)

noncomputable def NavierStokes.FiveRowRank.cellLower {n : ℕ} (a b : ℝ) (j : Fin n) : ℝ

Cell lower, given by a + (2 * (j.val : ℝ) + 1) * cellStep a b n.

Equations

• NavierStokes.FiveRowRank.cellLower a b j = a + (2 * ↑↑j + 1) * NavierStokes.FiveRowRank.cellStep a b n

noncomputable def NavierStokes.FiveRowRank.cellUpper {n : ℕ} (a b : ℝ) (j : Fin n) : ℝ

Cell upper, given by a + (2 * (j.val : ℝ) + 2) * cellStep a b n.

Equations

• NavierStokes.FiveRowRank.cellUpper a b j = a + (2 * ↑↑j + 2) * NavierStokes.FiveRowRank.cellStep a b n

theorem NavierStokes.FiveRowRank.cellStep_pos (a b : ℝ) (hab : a < b) (n : ℕ) : 0 < cellStep a b n

theorem NavierStokes.FiveRowRank.cellStep_mul (a b : ℝ) (n : ℕ) : (2 * ↑n + 1) * cellStep a b n = b - a

theorem NavierStokes.FiveRowRank.cellLower_gt {n : ℕ} (a b : ℝ) (hab : a < b) (j : Fin n) : a < cellLower a b j

theorem NavierStokes.FiveRowRank.cell_lower_lt_upper {n : ℕ} (a b : ℝ) (hab : a < b) (j : Fin n) : cellLower a b j < cellUpper a b j

theorem NavierStokes.FiveRowRank.cellUpper_lt {n : ℕ} (a b : ℝ) (hab : a < b) (j : Fin n) : cellUpper a b j < b

theorem NavierStokes.FiveRowRank.cell_separated {n : ℕ} (a b : ℝ) (hab : a < b) (i j : Fin n) (hij : i < j) : cellUpper a b i ≤ cellLower a b j

theorem NavierStokes.FiveRowRank.cell_positive {n : ℕ} (a b : ℝ) (ha : 0 < a) (hab : a < b) (j : Fin n) : 0 < cellLower a b j

theorem NavierStokes.FiveRowRank.cell_union_subset {n : ℕ} (a b : ℝ) (hab : a < b) : ⋃ (j : Fin n), Set.Ioo (cellLower a b j) (cellUpper a b j) ⊆ Set.Ioo a b

def NavierStokes.FiveRowRank.angularPowers (lam : ℝ) : Fin 3 → ℝ

Angular powers, given by ![2, -2 - 2 * lam, -2 * lam].

Equations

• NavierStokes.FiveRowRank.angularPowers lam = ![2, -2 - 2 * lam, -2 * lam]

def NavierStokes.FiveRowRank.axialPowers (lam : ℝ) : Fin 2 → ℝ

Axial powers, given by ![1, 1 - 2 * lam].

Equations

• NavierStokes.FiveRowRank.axialPowers lam = ![1, 1 - 2 * lam]

theorem NavierStokes.FiveRowRank.angularPowers_injective (lam : ℝ) (hlam : 0 < lam) : Function.Injective (angularPowers lam)

theorem NavierStokes.FiveRowRank.axialPowers_injective (lam : ℝ) (hlam : 0 < lam) : Function.Injective (axialPowers lam)

noncomputable def NavierStokes.FiveRowRank.angularDebt (C : ℝ) (d : Debt) : Fin 3 → ℝ

Normalized angular moments, including the signs of the pressure and axial rows.

Equations

• NavierStokes.FiveRowRank.angularDebt C d = ![0, -d 0 / (2 * C), d 2 / C]

noncomputable def NavierStokes.FiveRowRank.axialDebt (C : ℝ) (d : Debt) : Fin 2 → ℝ

Normalized axial moments.

Equations

• NavierStokes.FiveRowRank.axialDebt C d = ![0, -d 1 / C]

noncomputable def NavierStokes.FiveRowRank.deltaV (lam C a b : ℝ) (d : Debt) : ℝ → ℝ

The angular increment ∆v_m, constructed from three separated smooth bumps.

Equations

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

noncomputable def NavierStokes.FiveRowRank.gamma (lam C a b : ℝ) (d : Debt) : ℝ → ℝ

The desired axial increment γ_d, constructed from two separated smooth bumps.

Equations

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

noncomputable def NavierStokes.FiveRowRank.background (lam C R : ℝ) : ℝ

The unaltered power-law angular mean on the repair patch.

Equations

• NavierStokes.FiveRowRank.background lam C R = C * R ^ (-1 - 2 * lam)

theorem NavierStokes.FiveRowRank.deltaV_contDiff (lam C a b : ℝ) (d : Debt) : ContDiff ℝ (↑⊤) (deltaV lam C a b d)

theorem NavierStokes.FiveRowRank.gamma_contDiff (lam C a b : ℝ) (d : Debt) : ContDiff ℝ (↑⊤) (gamma lam C a b d)

theorem NavierStokes.FiveRowRank.deltaV_hasCompactSupport (lam C a b : ℝ) (d : Debt) (hab : a < b) : HasCompactSupport (deltaV lam C a b d)

theorem NavierStokes.FiveRowRank.gamma_hasCompactSupport (lam C a b : ℝ) (d : Debt) (hab : a < b) : HasCompactSupport (gamma lam C a b d)

theorem NavierStokes.FiveRowRank.deltaV_tsupport_subset (lam C a b : ℝ) (d : Debt) (hab : a < b) : tsupport (deltaV lam C a b d) ⊆ Set.Ioo a b

theorem NavierStokes.FiveRowRank.gamma_tsupport_subset (lam C a b : ℝ) (d : Debt) (hab : a < b) : tsupport (gamma lam C a b d) ⊆ Set.Ioo a b

theorem NavierStokes.FiveRowRank.deltaV_eq_zero_of_not_mem (lam C a b : ℝ) (d : Debt) (hab : a < b) {R : ℝ} (hR : R ∉ Set.Ioo a b) : deltaV lam C a b d R = 0

theorem NavierStokes.FiveRowRank.gamma_eq_zero_of_not_mem (lam C a b : ℝ) (d : Debt) (hab : a < b) {R : ℝ} (hR : R ∉ Set.Ioo a b) : gamma lam C a b d R = 0

theorem NavierStokes.FiveRowRank.angular_moments (lam C a b : ℝ) (d : Debt) (hlam : 0 < lam) (ha : 0 < a) (hab : a < b) (i : Fin 3) : ∫ (R : ℝ), R ^ angularPowers lam i * deltaV lam C a b d R = angularDebt C d i

theorem NavierStokes.FiveRowRank.axial_moments (lam C a b : ℝ) (d : Debt) (hlam : 0 < lam) (ha : 0 < a) (hab : a < b) (i : Fin 2) : ∫ (R : ℝ), R ^ axialPowers lam i * gamma lam C a b d R = axialDebt C d i

theorem NavierStokes.FiveRowRank.angular_mass_zero (lam C a b : ℝ) (d : Debt) (hlam : 0 < lam) (ha : 0 < a) (hab : a < b) : ∫ (R : ℝ), R ^ 2 * deltaV lam C a b d R = 0

theorem NavierStokes.FiveRowRank.axial_mass_zero (lam C a b : ℝ) (d : Debt) (hlam : 0 < lam) (ha : 0 < a) (hab : a < b) : ∫ (R : ℝ), R * gamma lam C a b d R = 0

theorem NavierStokes.FiveRowRank.pressure_weight (lam C R : ℝ) (hR : 0 < R) : 2 * background lam C R / R = 2 * C * R ^ (-2 - 2 * lam)

theorem NavierStokes.FiveRowRank.angular_weight (lam C R : ℝ) (hR : 0 < R) : R ^ 2 * background lam C R = C * R ^ (1 - 2 * lam)

theorem NavierStokes.FiveRowRank.axial_weight (lam C R : ℝ) (hR : 0 < R) : -(R * background lam C R) = -C * R ^ (-2 * lam)

theorem NavierStokes.FiveRowRank.pressure_row (lam C a b : ℝ) (d : Debt) (hlam : 0 < lam) (hC : C ≠ 0) (ha : 0 < a) (hab : a < b) : ∫ (R : ℝ), 2 * background lam C R / R * deltaV lam C a b d R = -d 0

theorem NavierStokes.FiveRowRank.angular_row (lam C a b : ℝ) (d : Debt) (hlam : 0 < lam) (hC : C ≠ 0) (ha : 0 < a) (hab : a < b) : ∫ (R : ℝ), R ^ 2 * background lam C R * gamma lam C a b d R = -d 1

theorem NavierStokes.FiveRowRank.axial_row (lam C a b : ℝ) (d : Debt) (hlam : 0 < lam) (hC : C ≠ 0) (ha : 0 < a) (hab : a < b) : ∫ (R : ℝ), -(R * background lam C R) * deltaV lam C a b d R = -d 2

def NavierStokes.FiveRowRank.FiveRows (V G : ℝ → ℝ) (d : Debt) (dv ga : ℝ → ℝ) : Prop

The five linear equations (35), retaining the general background fields.

Equations

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

theorem NavierStokes.FiveRowRank.five_rows_on_patch (lam C a b : ℝ) (d : Debt) (hlam : 0 < lam) (hC : C ≠ 0) (ha : 0 < a) (hab : a < b) (V G : ℝ → ℝ) (hV : ∀ R ∈ Set.Ioo a b, V R = background lam C R) (hG : ∀ R ∈ Set.Ioo a b, G R = 0) : FiveRows V G d (deltaV lam C a b d) (gamma lam C a b d)

Only the values of the background fields on the patch are used.

theorem NavierStokes.FiveRowRank.five_rows (lam C a b : ℝ) (d : Debt) (hlam : 0 < lam) (hC : C ≠ 0) (ha : 0 < a) (hab : a < b) : FiveRows (background lam C) (fun (x : ℝ) => 0) d (deltaV lam C a b d) (gamma lam C a b d)

In particular the concrete unaltered background supports all five rows.

theorem NavierStokes.FiveRowRank.integrable_power_mul_of_patch (p a b : ℝ) (f : ℝ → ℝ) (ha : 0 < a) (hf : Continuous f) (hs : Function.support f ⊆ Set.Ioo a b) : MeasureTheory.Integrable (fun (R : ℝ) => R ^ p * f R) MeasureTheory.volume

theorem NavierStokes.FiveRowRank.deltaV_power_integrable (lam C a b p : ℝ) (d : Debt) (ha : 0 < a) (hab : a < b) : MeasureTheory.Integrable (fun (R : ℝ) => R ^ p * deltaV lam C a b d R) MeasureTheory.volume

theorem NavierStokes.FiveRowRank.gamma_power_integrable (lam C a b p : ℝ) (d : Debt) (ha : 0 < a) (hab : a < b) : MeasureTheory.Integrable (fun (R : ℝ) => R ^ p * gamma lam C a b d R) MeasureTheory.volume

theorem NavierStokes.FiveRowRank.exists_five_row_repair (lam C a b : ℝ) (d : Debt) (hlam : 0 < lam) (hC : C ≠ 0) (ha : 0 < a) (hab : a < b) (V G : ℝ → ℝ) (hV : ∀ R ∈ Set.Ioo a b, V R = background lam C R) (hG : ∀ R ∈ Set.Ioo a b, G R = 0) : ∃ (dv : ℝ → ℝ) (ga : ℝ → ℝ), ContDiff ℝ (↑⊤) dv ∧ ContDiff ℝ (↑⊤) ga ∧ HasCompactSupport dv ∧ HasCompactSupport ga ∧ tsupport dv ⊆ Set.Ioo a b ∧ tsupport ga ⊆ Set.Ioo a b ∧ FiveRows V G d dv ga

The complete existence statement has no moment-rank assumption.

noncomputable def NavierStokes.FiveRowRank.angularDebtLinearMap (C : ℝ) : Debt →ₗ[ℝ] Fin 3 → ℝ

Angular debt linear map, bundling toFun, map_add, map_smul.

Equations

• NavierStokes.FiveRowRank.angularDebtLinearMap C = { toFun := NavierStokes.FiveRowRank.angularDebt C, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def NavierStokes.FiveRowRank.axialDebtLinearMap (C : ℝ) : Debt →ₗ[ℝ] Fin 2 → ℝ

Axial debt linear map, bundling toFun, map_add, map_smul.

Equations

• NavierStokes.FiveRowRank.axialDebtLinearMap C = { toFun := NavierStokes.FiveRowRank.axialDebt C, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def NavierStokes.FiveRowRank.deltaVLinearMap (lam C a b : ℝ) : Debt →ₗ[ℝ] ℝ → ℝ

The concrete angular correction as a linear map in (P,Jθ,Jz).

Equations

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

noncomputable def NavierStokes.FiveRowRank.gammaLinearMap (lam C a b : ℝ) : Debt →ₗ[ℝ] ℝ → ℝ

The concrete axial correction as a linear map in (P,Jθ,Jz).

Equations

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

@[simp]

theorem NavierStokes.FiveRowRank.deltaVLinearMap_apply (lam C a b : ℝ) (d : Debt) : (deltaVLinearMap lam C a b) d = deltaV lam C a b d

@[simp]

theorem NavierStokes.FiveRowRank.gammaLinearMap_apply (lam C a b : ℝ) (d : Debt) : (gammaLinearMap lam C a b) d = gamma lam C a b d

theorem NavierStokes.FiveRowRank.deltaV_add (lam C a b : ℝ) (d e : Debt) : deltaV lam C a b (d + e) = deltaV lam C a b d + deltaV lam C a b e

theorem NavierStokes.FiveRowRank.gamma_add (lam C a b : ℝ) (d e : Debt) : gamma lam C a b (d + e) = gamma lam C a b d + gamma lam C a b e

theorem NavierStokes.FiveRowRank.deltaV_smul (lam C a b r : ℝ) (d : Debt) : deltaV lam C a b (r • d) = r • deltaV lam C a b d

theorem NavierStokes.FiveRowRank.gamma_smul (lam C a b r : ℝ) (d : Debt) : gamma lam C a b (r • d) = r • gamma lam C a b d

@[simp]

theorem NavierStokes.FiveRowRank.deltaV_zero (lam C a b : ℝ) : deltaV lam C a b 0 = 0

@[simp]

theorem NavierStokes.FiveRowRank.gamma_zero (lam C a b : ℝ) : gamma lam C a b 0 = 0

theorem NavierStokes.FiveRowRank.angularDebt_rescale (C : ℝ) (d : Debt) : angularDebt C d = C⁻¹ • angularDebt 1 d

theorem NavierStokes.FiveRowRank.axialDebt_rescale (C : ℝ) (d : Debt) : axialDebt C d = C⁻¹ • axialDebt 1 d

theorem NavierStokes.FiveRowRank.deltaV_rescale (lam C a b : ℝ) (d : Debt) : deltaV lam C a b d = C⁻¹ • deltaV lam 1 a b d

theorem NavierStokes.FiveRowRank.gamma_rescale (lam C a b : ℝ) (d : Debt) : gamma lam C a b d = C⁻¹ • gamma lam 1 a b d

theorem NavierStokes.FiveRowRank.angularDebt_one_norm (d : Debt) : ‖angularDebt 1 d‖ ≤ ‖d‖

theorem NavierStokes.FiveRowRank.axialDebt_one_norm (d : Debt) : ‖axialDebt 1 d‖ ≤ ‖d‖

theorem NavierStokes.FiveRowRank.angularDebt_norm_le (C : ℝ) (d : Debt) : ‖angularDebt C d‖ ≤ ‖C⁻¹‖ * ‖d‖

The normalization loses at most the explicit factor ‖C⁻¹‖.

theorem NavierStokes.FiveRowRank.axialDebt_norm_le (C : ℝ) (d : Debt) : ‖axialDebt C d‖ ≤ ‖C⁻¹‖ * ‖d‖

theorem NavierStokes.FiveRowRank.finite_jet_bound (lam a b : ℝ) (hab : a < b) (N : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (C : ℝ), ∀ k ≤ N, ∀ (d e : Debt) (R : ℝ), |iteratedDeriv k (deltaV lam C a b d) R - iteratedDeriv k (deltaV lam C a b e) R| + |iteratedDeriv k (gamma lam C a b d) R - iteratedDeriv k (gamma lam C a b e) R| ≤ K * ‖C⁻¹‖ * ‖d - e‖

Every prescribed finite spatial jet is bounded linearly in the debt, uniformly in space. The geometric constant is independent of the nonzero amplitude C; all amplitude dependence is the displayed inverse factor.

theorem NavierStokes.FiveRowRank.uniform_finite_jet_bound (lam a b η : ℝ) (hab : a < b) (hη : 0 < η) (N : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (C : ℝ), η ≤ |C| → ∀ k ≤ N, ∀ (d e : Debt) (R : ℝ), |iteratedDeriv k (deltaV lam C a b d) R - iteratedDeriv k (deltaV lam C a b e) R| + |iteratedDeriv k (gamma lam C a b d) R - iteratedDeriv k (gamma lam C a b e) R| ≤ K * ‖d - e‖

If the amplitude stays a positive distance from zero, the finite-jet estimate has a single constant valid for all amplitudes in that range.

theorem NavierStokes.FiveRowRank.repair_joint_contDiffOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (a l u : Fin n → ℝ) {S : Set E} {d : E → Fin n → ℝ} (hd : ContDiffOn ℝ (↑⊤) d S) : ContDiffOn ℝ (↑⊤) (fun (z : E × ℝ) => LocalizedMomentRepair.repair a l u (d z.1) z.2) (S ×ˢ Set.univ)

Smooth debts give joint smoothness of a fixed localized repair in the parameter and spatial variables. This uses the actual finite coordinate family.

theorem NavierStokes.FiveRowRank.angularDebt_contDiffOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {S : Set E} {C : E → ℝ} {d : E → Debt} (hC : ContDiffOn ℝ (↑⊤) C S) (hd : ContDiffOn ℝ (↑⊤) d S) (hCn : ∀ p ∈ S, C p ≠ 0) : ContDiffOn ℝ (↑⊤) (fun (p : E) => angularDebt (C p) (d p)) S

theorem NavierStokes.FiveRowRank.axialDebt_contDiffOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {S : Set E} {C : E → ℝ} {d : E → Debt} (hC : ContDiffOn ℝ (↑⊤) C S) (hd : ContDiffOn ℝ (↑⊤) d S) (hCn : ∀ p ∈ S, C p ≠ 0) : ContDiffOn ℝ (↑⊤) (fun (p : E) => axialDebt (C p) (d p)) S

theorem NavierStokes.FiveRowRank.deltaV_joint_contDiffOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (lam a b : ℝ) {S : Set E} {C : E → ℝ} {d : E → Debt} (hC : ContDiffOn ℝ (↑⊤) C S) (hd : ContDiffOn ℝ (↑⊤) d S) (hCn : ∀ p ∈ S, C p ≠ 0) : ContDiffOn ℝ (↑⊤) (fun (z : E × ℝ) => deltaV lam (C z.1) a b (d z.1) z.2) (S ×ˢ Set.univ)

Joint smoothness in every auxiliary parameter and the radial coordinate, for any smooth nonvanishing amplitude and smooth debt vector.

theorem NavierStokes.FiveRowRank.gamma_joint_contDiffOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (lam a b : ℝ) {S : Set E} {C : E → ℝ} {d : E → Debt} (hC : ContDiffOn ℝ (↑⊤) C S) (hd : ContDiffOn ℝ (↑⊤) d S) (hCn : ∀ p ∈ S, C p ≠ 0) : ContDiffOn ℝ (↑⊤) (fun (z : E × ℝ) => gamma lam (C z.1) a b (d z.1) z.2) (S ×ˢ Set.univ)

theorem NavierStokes.FiveRowRank.repair_pair_joint_contDiffOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (lam a b : ℝ) {S : Set E} {C : E → ℝ} {d : E → Debt} (hC : ContDiffOn ℝ (↑⊤) C S) (hd : ContDiffOn ℝ (↑⊤) d S) (hCn : ∀ p ∈ S, C p ≠ 0) : ContDiffOn ℝ (↑⊤) (fun (z : E × ℝ) => (deltaV lam (C z.1) a b (d z.1) z.2, gamma lam (C z.1) a b (d z.1) z.2)) (S ×ˢ Set.univ)