Finite moment repair

This file proves the finite-dimensional algebra behind the manuscript's moment repairs. Nonsingularity is an explicit hypothesis for an arbitrary family of moment functionals and correction profiles. It is proved separately for a two-row weighted point-evaluation matrix. No assertion about the existence of smooth bumps or the conditioning of their moment matrices is implicit here.

def NavierStokes.MomentRepair.moments {ι : Type u_1} {V : Type u_2} [AddCommGroup V] [Module ℝ V] (L : ι → V →ₗ[ℝ] ℝ) (u : V) : ι → ℝ

The vector of prescribed linear moments.

Equations

• NavierStokes.MomentRepair.moments L u i = (L i) u

def NavierStokes.MomentRepair.synthesize {ι : Type u_1} {V : Type u_2} [Fintype ι] [AddCommGroup V] [Module ℝ V] (b : ι → V) (c : ι → ℝ) : V

A finite correction assembled from fixed profiles.

Equations

• NavierStokes.MomentRepair.synthesize b c = ∑ j : ι, c j • b j

def NavierStokes.MomentRepair.momentMatrix {ι : Type u_1} {V : Type u_2} [AddCommGroup V] [Module ℝ V] (L : ι → V →ₗ[ℝ] ℝ) (b : ι → V) : Matrix ι ι ℝ

Each column records the moments of one correction profile.

Equations

• NavierStokes.MomentRepair.momentMatrix L b i j = (L i) (b j)

theorem NavierStokes.MomentRepair.moments_synthesize {ι : Type u_1} {V : Type u_2} [Fintype ι] [AddCommGroup V] [Module ℝ V] (L : ι → V →ₗ[ℝ] ℝ) (b : ι → V) (c : ι → ℝ) : moments L (synthesize b c) = (momentMatrix L b).mulVec c

noncomputable def NavierStokes.MomentRepair.coefficients {ι : Type u_1} [Fintype ι] [DecidableEq ι] (B : Matrix ι ι ℝ) (d : ι → ℝ) : ι → ℝ

Coefficients obtained using the actual matrix inverse.

Equations

• NavierStokes.MomentRepair.coefficients B d = B⁻¹.mulVec d

theorem NavierStokes.MomentRepair.matrix_mul_coefficients {ι : Type u_1} [Fintype ι] [DecidableEq ι] (B : Matrix ι ι ℝ) (hB : B.det ≠ 0) (d : ι → ℝ) : B.mulVec (coefficients B d) = d

theorem NavierStokes.MomentRepair.coefficients_unique {ι : Type u_1} [Fintype ι] [DecidableEq ι] (B : Matrix ι ι ℝ) (hB : B.det ≠ 0) (d c : ι → ℝ) (hc : B.mulVec c = d) : c = coefficients B d

noncomputable def NavierStokes.MomentRepair.repair {ι : Type u_1} {V : Type u_2} [Fintype ι] [DecidableEq ι] [AddCommGroup V] [Module ℝ V] (L : ι → V →ₗ[ℝ] ℝ) (b : ι → V) (u : V) (target : ι → ℝ) : V

Add a finite correction which targets an arbitrary vector of moments.

Equations

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

theorem NavierStokes.MomentRepair.repair_exact {ι : Type u_1} {V : Type u_2} [Fintype ι] [DecidableEq ι] [AddCommGroup V] [Module ℝ V] (L : ι → V →ₗ[ℝ] ℝ) (b : ι → V) (hB : (momentMatrix L b).det ≠ 0) (u : V) (target : ι → ℝ) : moments L (repair L b u target) = target

Exact moment matching follows from nonsingularity, with no smallness needed.

theorem NavierStokes.MomentRepair.repair_unchanged_when_exact {ι : Type u_1} {V : Type u_2} [Fintype ι] [DecidableEq ι] [AddCommGroup V] [Module ℝ V] (L : ι → V →ₗ[ℝ] ℝ) (b : ι → V) (u : V) : repair L b u (moments L u) = u

theorem NavierStokes.MomentRepair.repair_coefficients_unique {ι : Type u_1} {V : Type u_2} [Fintype ι] [DecidableEq ι] [AddCommGroup V] [Module ℝ V] (L : ι → V →ₗ[ℝ] ℝ) (b : ι → V) (hB : (momentMatrix L b).det ≠ 0) (u : V) (target c : ι → ℝ) (hc : moments L (u + synthesize b c) = target) : c = coefficients (momentMatrix L b) (target - moments L u)

An arbitrary correction attaining the target has the computed coefficients.

theorem NavierStokes.MomentRepair.repair_idempotent {ι : Type u_1} {V : Type u_2} [Fintype ι] [DecidableEq ι] [AddCommGroup V] [Module ℝ V] (L : ι → V →ₗ[ℝ] ℝ) (b : ι → V) (hB : (momentMatrix L b).det ≠ 0) (u : V) (target : ι → ℝ) : repair L b (repair L b u target) target = repair L b u target

The repair is idempotent for fixed target moments.

theorem NavierStokes.MomentRepair.repair_eq_of_profiles_zero {ι : Type u_1} {X : Type u_2} [Fintype ι] [DecidableEq ι] (L : ι → (X → ℝ) →ₗ[ℝ] ℝ) (b : ι → X → ℝ) (u : X → ℝ) (target : ι → ℝ) (x : X) (hb : ∀ (j : ι), b j x = 0) : repair L b u target x = u x

Correction cannot change the function where every correction profile vanishes.

theorem NavierStokes.MomentRepair.repair_support_subset {ι : Type u_1} {X : Type u_2} [Fintype ι] [DecidableEq ι] (L : ι → (X → ℝ) →ₗ[ℝ] ℝ) (b : ι → X → ℝ) (u : X → ℝ) (target : ι → ℝ) (S : Set X) (hb : ∀ (j : ι), Function.support (b j) ⊆ S) : Function.support (repair L b u target - u) ⊆ S

A common support set is preserved by finite moment repair.

def NavierStokes.MomentRepair.twoPointMatrix (x₁ x₂ w₁ w₂ : ℝ) : Matrix (Fin 2) (Fin 2) ℝ

The two-row weighted evaluation matrix for exponents 0 and 1.

Equations

• NavierStokes.MomentRepair.twoPointMatrix x₁ x₂ w₁ w₂ = !![w₁, w₂; x₁ * w₁, x₂ * w₂]

theorem NavierStokes.MomentRepair.twoPointMatrix_det (x₁ x₂ w₁ w₂ : ℝ) : (twoPointMatrix x₁ x₂ w₁ w₂).det = w₁ * w₂ * (x₂ - x₁)

theorem NavierStokes.MomentRepair.twoPointMatrix_det_pos (x₁ x₂ w₁ w₂ : ℝ) (hx : x₁ < x₂) (hw₁ : 0 < w₁) (hw₂ : 0 < w₂) : 0 < (twoPointMatrix x₁ x₂ w₁ w₂).det

Ordered nodes and positive weights genuinely imply nonsingularity in two rows.

def NavierStokes.MomentRepair.correctionIteration {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (B : E ≃L[ℝ] E) (Q : E → E) (d c : E) : E

The fixed-point iteration used to solve B c + Q c = d.

Equations

• NavierStokes.MomentRepair.correctionIteration B Q d c = B.symm (d - Q c)

theorem NavierStokes.MomentRepair.correctionIteration_norm_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (B : E ≃L[ℝ] E) (Q : E → E) (d : E) (β K r : ℝ) (hβ : 0 ≤ β) (hK : 0 ≤ K) (hr : 0 ≤ r) (hB : ∀ (x : E), ‖B.symm x‖ ≤ β * ‖x‖) (hQ : ∀ (x : E), ‖x‖ ≤ r → ‖Q x‖ ≤ K * ‖x‖ ^ 2) (hsmall : 4 * β * K * r ≤ 1) (hd : 2 * β * ‖d‖ ≤ r) (c : E) (hc : ‖c‖ ≤ r) : ‖correctionIteration B Q d c‖ ≤ r

The quantitative hypotheses in Lemma 3.7 make the correction ball invariant.

theorem NavierStokes.MomentRepair.correctionIteration_sub_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (B : E ≃L[ℝ] E) (Q : E → E) (d : E) (β K r : ℝ) (hβ : 0 ≤ β) (hK : 0 ≤ K) (hB : ∀ (x : E), ‖B.symm x‖ ≤ β * ‖x‖) (hQ : ∀ (x : E), ‖x‖ ≤ r → ∀ (y : E), ‖y‖ ≤ r → ‖Q x - Q y‖ ≤ K * (‖x‖ + ‖y‖) * ‖x - y‖) (hsmall : 4 * β * K * r ≤ 1) (x y : E) (hx : ‖x‖ ≤ r) (hy : ‖y‖ ≤ r) : ‖correctionIteration B Q d x - correctionIteration B Q d y‖ ≤ 1 / 2 * ‖x - y‖

On the correction ball the iteration has Lipschitz constant at most 1/2.

theorem NavierStokes.MomentRepair.exists_unique_small_correction {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (B : E ≃L[ℝ] E) (Q : E → E) (d : E) (β K r : ℝ) (hβ : 0 ≤ β) (hK : 0 ≤ K) (hr : 0 ≤ r) (hB : ∀ (x : E), ‖B.symm x‖ ≤ β * ‖x‖) (hQnorm : ∀ (x : E), ‖x‖ ≤ r → ‖Q x‖ ≤ K * ‖x‖ ^ 2) (hQdiff : ∀ (x : E), ‖x‖ ≤ r → ∀ (y : E), ‖y‖ ≤ r → ‖Q x - Q y‖ ≤ K * (‖x‖ + ‖y‖) * ‖x - y‖) (hsmall : 4 * β * K * r ≤ 1) (hd : 2 * β * ‖d‖ ≤ r) : ∃! c : E, ‖c‖ ≤ r ∧ B c + Q c = d

The existence and local uniqueness part of the manuscript's quadratic moment adjustment, proved by Banach's fixed-point theorem. The hypotheses are explicit inverse and quadratic remainder bounds. Smooth dependence on extra parameters is not asserted.