Constructed smooth moment repairs

The correction profiles are explicit affine rescalings of the constructed smooth cutoff. Their supports lie strictly inside the supplied positive intervals. The generalized-power determinant theorem then gives exact finite-moment repair by an actual compactly supported smooth function.

Generalized-power evaluation matrices

Rolle induction proves uniqueness of an exponential sum at as many ordered nodes as there are distinct real exponents. Taking logarithms gives the generalized-power evaluation-matrix part of manuscript Lemma 3.6.

noncomputable def NavierStokes.PowerMomentMatrix.expSum {n : ℕ} (a c : Fin n → ℝ) (t : ℝ) : ℝ

A finite exponential sum with arbitrary real exponents.

Equations

• NavierStokes.PowerMomentMatrix.expSum a c t = ∑ j : Fin n, c j * Real.exp (a j * t)

theorem NavierStokes.PowerMomentMatrix.expSum_hasDerivAt {n : ℕ} (a c : Fin n → ℝ) (t : ℝ) : HasDerivAt (expSum a c) (expSum a (fun (j : Fin n) => c j * a j) t) t

theorem NavierStokes.PowerMomentMatrix.expSum_shift {n : ℕ} (a c : Fin n → ℝ) (s t : ℝ) : expSum (fun (j : Fin n) => a j - s) c t = expSum a c t * Real.exp (-s * t)

Shifting all exponents multiplies the exponential sum by a nonzero factor.

theorem NavierStokes.PowerMomentMatrix.exists_ordered_derivative_zeros {n : ℕ} (f f' : ℝ → ℝ) (hf : ∀ (t : ℝ), HasDerivAt f (f' t) t) (x : Fin (n + 1) → ℝ) (hx : StrictMono x) (hz : ∀ (j : Fin (n + 1)), f (x j) = 0) : ∃ (y : Fin n → ℝ), StrictMono y ∧ (∀ (j : Fin n), x j.castSucc < y j ∧ y j < x j.succ) ∧ ∀ (j : Fin n), f' (y j) = 0

Consecutive equal values yield strictly ordered derivative zeros.

theorem NavierStokes.PowerMomentMatrix.expSum_coefficients_zero (n : ℕ) (a c x : Fin n → ℝ) : Function.Injective a → StrictMono x → (∀ (j : Fin n), expSum a c (x j) = 0) → c = 0

An exponential sum with n distinct real exponents which vanishes at n strictly ordered nodes has all coefficients zero. This is the full finite Rolle induction, with no nonsingularity premise.

noncomputable def NavierStokes.PowerMomentMatrix.expEvaluationMatrix {n : ℕ} (a x : Fin n → ℝ) : Matrix (Fin n) (Fin n) ℝ

The evaluation matrix, with exponents indexing rows and nodes indexing columns.

Equations

• NavierStokes.PowerMomentMatrix.expEvaluationMatrix a x i j = Real.exp (a i * x j)

theorem NavierStokes.PowerMomentMatrix.expEvaluationMatrix_det_ne_zero {n : ℕ} (a x : Fin n → ℝ) (ha : Function.Injective a) (hx : StrictMono x) : (expEvaluationMatrix a x).det ≠ 0

noncomputable def NavierStokes.PowerMomentMatrix.powerEvaluationMatrix {n : ℕ} (a x : Fin n → ℝ) : Matrix (Fin n) (Fin n) ℝ

Real powers; the row exponents are not restricted to natural numbers.

Equations

• NavierStokes.PowerMomentMatrix.powerEvaluationMatrix a x i j = x j ^ a i

theorem NavierStokes.PowerMomentMatrix.powerEvaluationMatrix_det_ne_zero {n : ℕ} (a x : Fin n → ℝ) (ha : Function.Injective a) (hx : StrictMono x) (hpos : ∀ (j : Fin n), 0 < x j) : (powerEvaluationMatrix a x).det ≠ 0

The generalized-power evaluation determinant is nonzero at positive ordered nodes.

theorem NavierStokes.PowerMomentMatrix.exists_zero_of_setIntegral_eq_zero (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] (l u : ℝ) (f : ℝ → ℝ) (hmass : μ (Set.Icc l u) ≠ 0) (hf : ContinuousOn f (Set.Icc l u)) (hzero : ∫ (t : ℝ) in Set.Icc l u, f t ∂μ = 0) : ∃ t ∈ Set.Icc l u, f t = 0

A continuous function with zero integral against a positive finite measure of nonzero mass on an interval has a zero in that interval.

noncomputable def NavierStokes.PowerMomentMatrix.powerSum {n : ℕ} (a c : Fin n → ℝ) (t : ℝ) : ℝ

A finite linear combination of arbitrary real powers.

Equations

• NavierStokes.PowerMomentMatrix.powerSum a c t = ∑ i : Fin n, c i * t ^ a i

theorem NavierStokes.PowerMomentMatrix.continuousOn_powerSum {n : ℕ} (a c : Fin n → ℝ) (l u : ℝ) (hl : 0 < l) : ContinuousOn (powerSum a c) (Set.Icc l u)

noncomputable def NavierStokes.PowerMomentMatrix.intervalMomentMatrix {n : ℕ} (a l u : Fin n → ℝ) (μ : Fin n → MeasureTheory.Measure ℝ) : Matrix (Fin n) (Fin n) ℝ

Columns integrate the real powers over separated intervals against finite positive measures. Positivity is intrinsic in the type Measure.

Equations

• NavierStokes.PowerMomentMatrix.intervalMomentMatrix a l u μ i j = ∫ (t : ℝ) in Set.Icc (l j) (u j), t ^ a i ∂μ j

theorem NavierStokes.PowerMomentMatrix.integral_powerSum {n : ℕ} (a c : Fin n → ℝ) (l u : ℝ) (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] (hl : 0 < l) : ∫ (t : ℝ) in Set.Icc l u, powerSum a c t ∂μ = ∑ i : Fin n, c i * ∫ (t : ℝ) in Set.Icc l u, t ^ a i ∂μ

theorem NavierStokes.PowerMomentMatrix.intervalMomentMatrix_det_ne_zero {n : ℕ} (a l u : Fin n → ℝ) (μ : Fin n → MeasureTheory.Measure ℝ) [∀ (j : Fin n), MeasureTheory.IsFiniteMeasure (μ j)] (ha : Function.Injective a) (hl : ∀ (j : Fin n), 0 < l j) (hsep : ∀ (i j : Fin n), i < j → u i < l j) (hmass : ∀ (j : Fin n), (μ j) (Set.Icc (l j) (u j)) ≠ 0) : (intervalMomentMatrix a l u μ).det ≠ 0

The integrated generalized-power matrix is nonsingular for any finite positive measures with nonzero mass on strictly separated compact positive intervals. This proves the moment-matrix mechanism without assuming determinant sign or invertibility. A zero linear combination of columns supplies one function zero in each interval; the Rolle theorem above then forces all coefficients to vanish.

noncomputable def NavierStokes.PowerMomentMatrix.bumpMomentMatrix {n : ℕ} (a : Fin n → ℝ) (β : Fin n → ℝ → ℝ) : Matrix (Fin n) (Fin n) ℝ

The manuscript's matrix of ordinary Lebesgue integrals against bump profiles.

Equations

• NavierStokes.PowerMomentMatrix.bumpMomentMatrix a β i j = ∫ (t : ℝ), t ^ a i * β j t

theorem NavierStokes.PowerMomentMatrix.bumpMomentMatrix_det_ne_zero {n : ℕ} (a l u : Fin n → ℝ) (β : Fin n → ℝ → ℝ) (ha : Function.Injective a) (hl : ∀ (j : Fin n), 0 < l j) (hsep : ∀ (i j : Fin n), i < j → u i < l j) (hcont : ∀ (j : Fin n), Continuous (β j)) (hnonneg : ∀ (j : Fin n) (t : ℝ), 0 ≤ β j t) (hnonzero : ∀ (j : Fin n), ∃ (t : ℝ), β j t ≠ 0) (hsupp : ∀ (j : Fin n), Function.support (β j) ⊆ Set.Icc (l j) (u j)) : (bumpMomentMatrix a β).det ≠ 0

The ordered bump moment matrix is nonsingular. The bump hypotheses are stated using explicit separated compact intervals; continuity suffices, so smoothness is unnecessary. All finite sizes and arbitrary distinct real exponents are covered. No moment-determinant or inverse estimate is assumed.

noncomputable def NavierStokes.LocalizedMomentRepair.innerLower (l u : ℝ) : ℝ

Inner lower, given by (3 * l + u) / 4.

Equations

• NavierStokes.LocalizedMomentRepair.innerLower l u = (3 * l + u) / 4

noncomputable def NavierStokes.LocalizedMomentRepair.innerUpper (l u : ℝ) : ℝ

Inner upper, given by (l + 3 * u) / 4.

Equations

• NavierStokes.LocalizedMomentRepair.innerUpper l u = (l + 3 * u) / 4

noncomputable def NavierStokes.LocalizedMomentRepair.bump (l u t : ℝ) : ℝ

A concrete smooth bump in the middle half of (l,u).

Equations

• NavierStokes.LocalizedMomentRepair.bump l u t = NavierStokes.SmoothCutoffs.cutoff ((t - (l + u) / 2) / ((u - l) / 4))

theorem NavierStokes.LocalizedMomentRepair.bump_contDiff (l u : ℝ) : ContDiff ℝ (↑⊤) (bump l u)

theorem NavierStokes.LocalizedMomentRepair.bump_nonneg (l u t : ℝ) : 0 ≤ bump l u t

theorem NavierStokes.LocalizedMomentRepair.bump_le_one (l u t : ℝ) : bump l u t ≤ 1

theorem NavierStokes.LocalizedMomentRepair.bump_at_center (l u : ℝ) : bump l u ((l + u) / 2) = 1

theorem NavierStokes.LocalizedMomentRepair.bump_support_subset (l u : ℝ) (hlu : l < u) : Function.support (bump l u) ⊆ Set.Icc (innerLower l u) (innerUpper l u)

theorem NavierStokes.LocalizedMomentRepair.bump_tsupport_subset (l u : ℝ) (hlu : l < u) : tsupport (bump l u) ⊆ Set.Icc (innerLower l u) (innerUpper l u)

theorem NavierStokes.LocalizedMomentRepair.bump_hasCompactSupport (l u : ℝ) (hlu : l < u) : HasCompactSupport (bump l u)

theorem NavierStokes.LocalizedMomentRepair.innerInterval_subset_open (l u : ℝ) (hlu : l < u) : Set.Icc (innerLower l u) (innerUpper l u) ⊆ Set.Ioo l u

theorem NavierStokes.LocalizedMomentRepair.bump_tsupport_subset_open (l u : ℝ) (hlu : l < u) : tsupport (bump l u) ⊆ Set.Ioo l u

def NavierStokes.LocalizedMomentRepair.repairRegion {n : ℕ} (l u : Fin n → ℝ) : Set ℝ

A fixed compact set, independent of the moment debt.

Equations

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

theorem NavierStokes.LocalizedMomentRepair.repairRegion_isCompact {n : ℕ} (l u : Fin n → ℝ) : IsCompact (repairRegion l u)

theorem NavierStokes.LocalizedMomentRepair.repairRegion_subset_open {n : ℕ} (l u : Fin n → ℝ) (hlu : ∀ (j : Fin n), l j < u j) : repairRegion l u ⊆ ⋃ (j : Fin n), Set.Ioo (l j) (u j)

noncomputable def NavierStokes.LocalizedMomentRepair.matrix {n : ℕ} (a l u : Fin n → ℝ) : Matrix (Fin n) (Fin n) ℝ

The actual generalized-power moment matrix of the constructed profiles.

Equations

• NavierStokes.LocalizedMomentRepair.matrix a l u = NavierStokes.PowerMomentMatrix.bumpMomentMatrix a fun (j : Fin n) => NavierStokes.LocalizedMomentRepair.bump (l j) (u j)

theorem NavierStokes.LocalizedMomentRepair.matrix_det_ne_zero {n : ℕ} (a l u : Fin n → ℝ) (ha : Function.Injective a) (hl : ∀ (j : Fin n), 0 < l j) (hlu : ∀ (j : Fin n), l j < u j) (hsep : ∀ (i j : Fin n), i < j → u i ≤ l j) : (matrix a l u).det ≠ 0

noncomputable def NavierStokes.LocalizedMomentRepair.coefficients {n : ℕ} (a l u d : Fin n → ℝ) : Fin n → ℝ

Coefficients are computed from the proved nonsingular moment matrix.

Equations

• NavierStokes.LocalizedMomentRepair.coefficients a l u d = (NavierStokes.LocalizedMomentRepair.matrix a l u)⁻¹.mulVec d

noncomputable def NavierStokes.LocalizedMomentRepair.repair {n : ℕ} (a l u d : Fin n → ℝ) (t : ℝ) : ℝ

The constructed smooth correction for the prescribed finite vector of debts.

Equations

• NavierStokes.LocalizedMomentRepair.repair a l u d t = ∑ j : Fin n, NavierStokes.LocalizedMomentRepair.coefficients a l u d j * NavierStokes.LocalizedMomentRepair.bump (l j) (u j) t

theorem NavierStokes.LocalizedMomentRepair.repair_contDiff {n : ℕ} (a l u d : Fin n → ℝ) : ContDiff ℝ (↑⊤) (repair a l u d)

theorem NavierStokes.LocalizedMomentRepair.repair_support_subset {n : ℕ} (a l u d : Fin n → ℝ) (hlu : ∀ (j : Fin n), l j < u j) : Function.support (repair a l u d) ⊆ repairRegion l u

theorem NavierStokes.LocalizedMomentRepair.repair_tsupport_subset {n : ℕ} (a l u d : Fin n → ℝ) (hlu : ∀ (j : Fin n), l j < u j) : tsupport (repair a l u d) ⊆ repairRegion l u

theorem NavierStokes.LocalizedMomentRepair.repair_hasCompactSupport {n : ℕ} (a l u d : Fin n → ℝ) (hlu : ∀ (j : Fin n), l j < u j) : HasCompactSupport (repair a l u d)

theorem NavierStokes.LocalizedMomentRepair.repair_tsupport_subset_open {n : ℕ} (a l u d : Fin n → ℝ) (hlu : ∀ (j : Fin n), l j < u j) : tsupport (repair a l u d) ⊆ ⋃ (j : Fin n), Set.Ioo (l j) (u j)

theorem NavierStokes.LocalizedMomentRepair.integrable_power_mul_bump (p l u : ℝ) (hl : 0 < l) (hlu : l < u) : MeasureTheory.Integrable (fun (t : ℝ) => t ^ p * bump l u t) MeasureTheory.volume

theorem NavierStokes.LocalizedMomentRepair.repair_exact {n : ℕ} (a l u d : Fin n → ℝ) (ha : Function.Injective a) (hl : ∀ (j : Fin n), 0 < l j) (hlu : ∀ (j : Fin n), l j < u j) (hsep : ∀ (i j : Fin n), i < j → u i ≤ l j) (i : Fin n) : ∫ (t : ℝ), t ^ a i * repair a l u d t = d i

The prescribed moments hold as exact ordinary Lebesgue integral identities.

theorem NavierStokes.LocalizedMomentRepair.exists_smooth_compact_repair {n : ℕ} (a l u d : Fin n → ℝ) (ha : Function.Injective a) (hl : ∀ (j : Fin n), 0 < l j) (hlu : ∀ (j : Fin n), l j < u j) (hsep : ∀ (i j : Fin n), i < j → u i ≤ l j) : ∃ (f : ℝ → ℝ), ContDiff ℝ (↑⊤) f ∧ HasCompactSupport f ∧ tsupport f ⊆ ⋃ (j : Fin n), Set.Ioo (l j) (u j) ∧ ∀ (i : Fin n), ∫ (t : ℝ), t ^ a i * f t = d i

Existence from exponents and intervals alone, with an actual function witness.

theorem NavierStokes.LocalizedMomentRepair.repair_add {n : ℕ} (a l u d e : Fin n → ℝ) : repair a l u (d + e) = repair a l u d + repair a l u e

theorem NavierStokes.LocalizedMomentRepair.repair_smul {n : ℕ} (a l u d : Fin n → ℝ) (r : ℝ) : repair a l u (r • d) = r • repair a l u d

theorem NavierStokes.LocalizedMomentRepair.repair_sub {n : ℕ} (a l u d e : Fin n → ℝ) : repair a l u (d - e) = repair a l u d - repair a l u e

noncomputable def NavierStokes.LocalizedMomentRepair.repairLinearMap {n : ℕ} (a l u : Fin n → ℝ) : (Fin n → ℝ) →ₗ[ℝ] ℝ → ℝ

The fixed-interval, fixed-exponent repair depends linearly on the moment debt.

Equations

• NavierStokes.LocalizedMomentRepair.repairLinearMap a l u = { toFun := NavierStokes.LocalizedMomentRepair.repair a l u, map_add' := ⋯, map_smul' := ⋯ }

theorem NavierStokes.LocalizedMomentRepair.continuous_repair_eval {n : ℕ} (a l u : Fin n → ℝ) (t : ℝ) : Continuous fun (d : Fin n → ℝ) => repair a l u d t

theorem NavierStokes.LocalizedMomentRepair.continuous_repair {n : ℕ} (a l u : Fin n → ℝ) : Continuous (repair a l u)

Continuity in the pointwise function topology; the later jet bounds are stronger.

theorem NavierStokes.LocalizedMomentRepair.repair_eq_sum_coordinate {n : ℕ} (a l u d : Fin n → ℝ) : repair a l u d = fun (t : ℝ) => ∑ j : Fin n, d j * repair a l u (Pi.single j 1) t

Decomposition into the finite family of repairs of coordinate debts.

theorem NavierStokes.LocalizedMomentRepair.iteratedDeriv_finite_sum {ι : Type u_1} (s : Finset ι) (f : ι → ℝ → ℝ) (hf : ∀ (i : ι), ContDiff ℝ (↑⊤) (f i)) (k : ℕ) (t : ℝ) : iteratedDeriv k (fun (x : ℝ) => ∑ i ∈ s, f i x) t = ∑ i ∈ s, iteratedDeriv k (f i) t

Iterated differentiation commutes with finite sums of smooth real functions.

theorem NavierStokes.LocalizedMomentRepair.smooth_compact_derivative_bound (f : ℝ → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hc : HasCompactSupport f) (k : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (t : ℝ), |iteratedDeriv k f t| ≤ C

Every derivative of a smooth compactly supported function has a global finite bound.

theorem NavierStokes.LocalizedMomentRepair.repair_iteratedDeriv_coordinate {n : ℕ} (a l u d : Fin n → ℝ) (k : ℕ) (t : ℝ) : iteratedDeriv k (repair a l u d) t = ∑ j : Fin n, d j * iteratedDeriv k (repair a l u (Pi.single j 1)) t

Every derivative of the repair is the same linear combination of fixed coordinate repairs.

theorem NavierStokes.LocalizedMomentRepair.repair_derivative_bound {n : ℕ} (a l u : Fin n → ℝ) (hlu : ∀ (j : Fin n), l j < u j) (k : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (d : Fin n → ℝ) (t : ℝ), |iteratedDeriv k (repair a l u d) t| ≤ C * ‖d‖

A uniform-in-space linear estimate for each derivative, with all geometric data fixed.

theorem NavierStokes.LocalizedMomentRepair.repair_finite_jet_bound {n : ℕ} (a l u : Fin n → ℝ) (hlu : ∀ (j : Fin n), l j < u j) (N : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ k ≤ N, ∀ (d e : Fin n → ℝ) (t : ℝ), |iteratedDeriv k (repair a l u d) t - iteratedDeriv k (repair a l u e) t| ≤ C * ‖d - e‖

All derivatives through any prescribed finite order depend Lipschitz-continuously on the moment debt, uniformly over the spatial coordinate.