Actual torus and native-coordinate averages

The integer covering is treated as an actual surjective additive homomorphism of the compact torus. Haar invariance is a conclusion, not an assumption.

Concentration of actual pulse covariance columns

We use r = sqrt L, so that a slot has length r^2. Pointwise Gaussian bounds on the fundamental component and an actual compactly supported cutoff give mass of order r and first centered moment of order r^2. Division by the mass then gives a direction error of order 1/r.

Smooth positive covariance solves

For an actual real two-by-two matrix and target, the signed areas in Cramer's rule give an explicit strict cone. On that cone, the inverse solution and its positive square roots depend smoothly on smooth input data. A compact family has a uniform positive lower bound and a uniform tolerance for perturbing both the matrix and the target.

No assertion here supplies smoothness or error estimates for the manuscript's integrated columns. No assertion concerns extension through a zero-amplitude edge, where the strict cone hypotheses fail.

Two signed covariance slots

The finite-dimensional algebra underlying Lemma 8.7 and equation (29) of the candidate manuscript. In the orthonormal (N,K) coordinates, the two normalized columns are (-a,-b) and (-a,b), with positive column scales. A target (-m,t) lies strictly between them precisely when |a*t| < b*m.

The actual integrated columns in the manuscript include approximation errors. This file does not identify those columns with the exact model, or prove the Gaussian, parameter-derivative, or flat-edge estimates.

def NavierStokes.Covariance.signedMatrix (a b scaleMinus scalePlus : ℝ) : Matrix (Fin 2) (Fin 2) ℝ

The two columns, with their individual positive size factors.

Equations

• NavierStokes.Covariance.signedMatrix a b scaleMinus scalePlus = !![-a * scaleMinus, -a * scalePlus; -b * scaleMinus, b * scalePlus]

def NavierStokes.Covariance.target (m t : ℝ) : Fin 2 → ℝ

The stress target in normal and transverse coordinates.

Equations

• NavierStokes.Covariance.target m t = ![-m, t]

noncomputable def NavierStokes.Covariance.coefficients (a b scaleMinus scalePlus m t : ℝ) : Fin 2 → ℝ

Explicit squared amplitudes for the two signed slots.

Equations

• NavierStokes.Covariance.coefficients a b scaleMinus scalePlus m t = ![(b * m - a * t) / (2 * a * b * scaleMinus), (b * m + a * t) / (2 * a * b * scalePlus)]

theorem NavierStokes.Covariance.determinant_formula (a b scaleMinus scalePlus : ℝ) : (signedMatrix a b scaleMinus scalePlus).det = -(2 * a * b * scaleMinus * scalePlus)

theorem NavierStokes.Covariance.determinant_neg {a b scaleMinus scalePlus : ℝ} (ha : 0 < a) (hb : 0 < b) (hMinus : 0 < scaleMinus) (hPlus : 0 < scalePlus) : (signedMatrix a b scaleMinus scalePlus).det < 0

theorem NavierStokes.Covariance.determinant_ne_zero {a b scaleMinus scalePlus : ℝ} (ha : 0 < a) (hb : 0 < b) (hMinus : 0 < scaleMinus) (hPlus : 0 < scalePlus) : (signedMatrix a b scaleMinus scalePlus).det ≠ 0

theorem NavierStokes.Covariance.reconstruct {a b scaleMinus scalePlus : ℝ} (m t : ℝ) (ha : a ≠ 0) (hb : b ≠ 0) (hMinus : scaleMinus ≠ 0) (hPlus : scalePlus ≠ 0) : (signedMatrix a b scaleMinus scalePlus).mulVec (coefficients a b scaleMinus scalePlus m t) = target m t

The explicit coefficients solve the two covariance equations exactly.

theorem NavierStokes.Covariance.inverse_formula {a b scaleMinus scalePlus : ℝ} (m t : ℝ) (ha : 0 < a) (hb : 0 < b) (hMinus : 0 < scaleMinus) (hPlus : 0 < scalePlus) : (signedMatrix a b scaleMinus scalePlus)⁻¹.mulVec (target m t) = coefficients a b scaleMinus scalePlus m t

Thus the explicit formula is the matrix inverse applied to the stress.

theorem NavierStokes.Covariance.solution_unique {a b scaleMinus scalePlus m t : ℝ} (ha : 0 < a) (hb : 0 < b) (hMinus : 0 < scaleMinus) (hPlus : 0 < scalePlus) (y : Fin 2 → ℝ) (hy : (signedMatrix a b scaleMinus scalePlus).mulVec y = target m t) : y = coefficients a b scaleMinus scalePlus m t

theorem NavierStokes.Covariance.coefficients_pos {a b scaleMinus scalePlus m t : ℝ} (ha : 0 < a) (hb : 0 < b) (hMinus : 0 < scaleMinus) (hPlus : 0 < scalePlus) (hcone : |a * t| < b * m) (i : Fin 2) : 0 < coefficients a b scaleMinus scalePlus m t i

A strict geometric cone condition makes both squared amplitudes positive.

theorem NavierStokes.Covariance.coefficients_pos_iff {a b scaleMinus scalePlus m t : ℝ} (ha : 0 < a) (hb : 0 < b) (hMinus : 0 < scaleMinus) (hPlus : 0 < scalePlus) : (∀ (i : Fin 2), 0 < coefficients a b scaleMinus scalePlus m t i) ↔ |a * t| < b * m

The same strict cone condition is necessary as well as sufficient.

noncomputable def NavierStokes.Covariance.amplitudes (a b scaleMinus scalePlus m t : ℝ) : Fin 2 → ℝ

The primary velocity amplitudes are positive square roots of the solve.

Equations

• NavierStokes.Covariance.amplitudes a b scaleMinus scalePlus m t i = √(NavierStokes.Covariance.coefficients a b scaleMinus scalePlus m t i)

theorem NavierStokes.Covariance.amplitudes_pos {a b scaleMinus scalePlus m t : ℝ} (ha : 0 < a) (hb : 0 < b) (hMinus : 0 < scaleMinus) (hPlus : 0 < scalePlus) (hcone : |a * t| < b * m) (i : Fin 2) : 0 < amplitudes a b scaleMinus scalePlus m t i

theorem NavierStokes.Covariance.amplitudes_sq {a b scaleMinus scalePlus m t : ℝ} (ha : 0 < a) (hb : 0 < b) (hMinus : 0 < scaleMinus) (hPlus : 0 < scalePlus) (hcone : |a * t| < b * m) : (fun (i : Fin 2) => amplitudes a b scaleMinus scalePlus m t i ^ 2) = coefficients a b scaleMinus scalePlus m t

theorem NavierStokes.Covariance.reconstruct_from_amplitudes {a b scaleMinus scalePlus m t : ℝ} (ha : 0 < a) (hb : 0 < b) (hMinus : 0 < scaleMinus) (hPlus : 0 < scalePlus) (hcone : |a * t| < b * m) : ((signedMatrix a b scaleMinus scalePlus).mulVec fun (i : Fin 2) => amplitudes a b scaleMinus scalePlus m t i ^ 2) = target m t

Squared positive velocity amplitudes reproduce the exact model covariance.

theorem NavierStokes.Covariance.scaled_primary_covariance {a b scaleMinus scalePlus m t ε : ℝ} (mask : ℝ) (hε : 0 ≤ ε) (ha : 0 < a) (hb : 0 < b) (hMinus : 0 < scaleMinus) (hPlus : 0 < scalePlus) (hcone : |a * t| < b * m) : ((signedMatrix a b scaleMinus scalePlus).mulVec fun (i : Fin 2) => (√ε * amplitudes a b scaleMinus scalePlus m t i * mask) ^ 2) = (ε * mask ^ 2) • target m t

The square-root viscosity factor and any common partition mask in (29) produce precisely the expected factor ε * mask^2 in covariance.

noncomputable def NavierStokes.Covariance.normalMagnitude (c u : ℝ) : ℝ

Positive normal magnitude in the manuscript's signed directions.

Equations

• NavierStokes.Covariance.normalMagnitude c u = -c * √(1 + u ^ 2)

theorem NavierStokes.Covariance.normalMagnitude_pos {c u : ℝ} (hc : c < 0) : 0 < normalMagnitude c u

theorem NavierStokes.Covariance.cone_of_ratio {c u m t : ℝ} (hm : 0 < m) (hratio : |c * t / m| < u / √(1 + u ^ 2)) : |normalMagnitude c u * t| < u * m

The manuscript's strict ratio choice for u_* implies the exact cone test.

theorem NavierStokes.Covariance.positive_primary {c u scaleMinus scalePlus m t : ℝ} (hc : c < 0) (hu : 0 < u) (hm : 0 < m) (hMinus : 0 < scaleMinus) (hPlus : 0 < scalePlus) (hratio : |c * t / m| < u / √(1 + u ^ 2)) : ∃ (velocity : Fin 2 → ℝ), (∀ (i : Fin 2), 0 < velocity i) ∧ ((signedMatrix (normalMagnitude c u) u scaleMinus scalePlus).mulVec fun (i : Fin 2) => velocity i ^ 2) = target m t

The exact signed-slot model has positive primary amplitudes under the ratio condition stated in Section 8.3. This asserts no analytic error bound.

@[reducible, inline]

abbrev NavierStokes.SmoothCovariance.Mat2 : Type

Mat2: an abbreviation for Matrix (Fin 2) (Fin 2) ℝ.

Equations

• NavierStokes.SmoothCovariance.Mat2 = Matrix (Fin 2) (Fin 2) ℝ

@[reducible, inline]

abbrev NavierStokes.SmoothCovariance.Vec2 : Type

Vec2: an abbreviation for Fin 2 → ℝ /- The entrywise sup norm makes all metric assertions below unambiguous. -/.

Equations

• NavierStokes.SmoothCovariance.Vec2 = (Fin 2 → ℝ)

@[instance_reducible]

def NavierStokes.SmoothCovariance.instSmoothCovariance1 : NormedAddCommGroup Mat2

Cache the standard NormedAddCommGroup Mat2 instance to shorten typeclass synthesis.

Equations

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

@[instance_reducible]

noncomputable def NavierStokes.SmoothCovariance.instSmoothCovariance2 : NormedSpace ℝ Mat2

Cache the standard NormedSpace ℝ Mat2 instance to shorten typeclass synthesis.

Equations

• NavierStokes.SmoothCovariance.instSmoothCovariance2 = { toModule := Matrix.module, norm_smul_le := NavierStokes.SmoothCovariance.instSmoothCovariance2._proof_1 }

@[reducible, inline]

abbrev NavierStokes.SmoothCovariance.Datum : Type

Datum: an abbreviation for Mat2 × Vec2.

Equations

• NavierStokes.SmoothCovariance.Datum = (NavierStokes.SmoothCovariance.Mat2 × NavierStokes.SmoothCovariance.Vec2)

def NavierStokes.SmoothCovariance.cramerNumerator (H : Mat2) (T : Vec2) : Vec2

Oriented areas obtained by replacing each column by the target.

Equations

• NavierStokes.SmoothCovariance.cramerNumerator H T = ![T 0 * H 1 1 - H 0 1 * T 1, H 0 0 * T 1 - T 0 * H 1 0]

noncomputable def NavierStokes.SmoothCovariance.weights (H : Mat2) (T : Vec2) : Vec2

Cramer's explicit formula, including Lean's total division convention.

Equations

• NavierStokes.SmoothCovariance.weights H T i = NavierStokes.SmoothCovariance.cramerNumerator H T i / Matrix.det H

def NavierStokes.SmoothCovariance.StrictCone (H : Mat2) (T : Vec2) : Prop

Both target-column oriented areas have the same nonzero orientation as the two original columns. The definition uses only polynomial inequalities.

Equations

• NavierStokes.SmoothCovariance.StrictCone H T = (0 < NavierStokes.SmoothCovariance.cramerNumerator H T 0 * Matrix.det H ∧ 0 < NavierStokes.SmoothCovariance.cramerNumerator H T 1 * Matrix.det H)

noncomputable def NavierStokes.SmoothCovariance.amplitudes (H : Mat2) (T : Vec2) : Vec2

Amplitudes, defined pointwise by Real.sqrt (weights H T i).

Equations

• NavierStokes.SmoothCovariance.amplitudes H T i = √(NavierStokes.SmoothCovariance.weights H T i)

theorem NavierStokes.SmoothCovariance.StrictCone.det_ne_zero {H : Mat2} {T : Vec2} (h : StrictCone H T) : Matrix.det H ≠ 0

theorem NavierStokes.SmoothCovariance.weights_pos_iff (H : Mat2) (T : Vec2) : (∀ (i : Fin 2), 0 < weights H T i) ↔ StrictCone H T

theorem NavierStokes.SmoothCovariance.StrictCone.weights_pos {H : Mat2} {T : Vec2} (h : StrictCone H T) (i : Fin 2) : 0 < weights H T i

theorem NavierStokes.SmoothCovariance.reconstruct (H : Mat2) (T : Vec2) (hdet : Matrix.det H ≠ 0) : Matrix.mulVec H (weights H T) = T

theorem NavierStokes.SmoothCovariance.inverse_formula (H : Mat2) (T : Vec2) (hdet : Matrix.det H ≠ 0) : Matrix.mulVec H⁻¹ T = weights H T

theorem NavierStokes.SmoothCovariance.StrictCone.amplitudes_pos {H : Mat2} {T : Vec2} (h : StrictCone H T) (i : Fin 2) : 0 < amplitudes H T i

theorem NavierStokes.SmoothCovariance.reconstruct_amplitudes {H : Mat2} {T : Vec2} (h : StrictCone H T) : (Matrix.mulVec H fun (i : Fin 2) => amplitudes H T i ^ 2) = T

theorem NavierStokes.SmoothCovariance.weights_signed_model {a b sm sp : ℝ} (m t : ℝ) (ha : 0 < a) (hb : 0 < b) (hm : 0 < sm) (hp : 0 < sp) : weights (Covariance.signedMatrix a b sm sp) (Covariance.target m t) = Covariance.coefficients a b sm sp m t

Agreement with the earlier exact signed-column formula.

theorem NavierStokes.SmoothCovariance.signed_model_strictCone {a b sm sp m t : ℝ} (ha : 0 < a) (hb : 0 < b) (hm : 0 < sm) (hp : 0 < sp) (hcone : |a * t| < b * m) : StrictCone (Covariance.signedMatrix a b sm sp) (Covariance.target m t)

theorem NavierStokes.SmoothCovariance.contDiffOn_determinant {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} {H : E → Mat2} (hH : ∀ (i j : Fin 2), ContDiffOn ℝ (↑⊤) (fun (x : E) => H x i j) s) : ContDiffOn ℝ (↑⊤) (fun (x : E) => Matrix.det (H x)) s

theorem NavierStokes.SmoothCovariance.contDiffOn_numerator {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} {H : E → Mat2} {T : E → Vec2} (hH : ∀ (i j : Fin 2), ContDiffOn ℝ (↑⊤) (fun (x : E) => H x i j) s) (hT : ∀ (i : Fin 2), ContDiffOn ℝ (↑⊤) (fun (x : E) => T x i) s) (i : Fin 2) : ContDiffOn ℝ (↑⊤) (fun (x : E) => cramerNumerator (H x) (T x) i) s

theorem NavierStokes.SmoothCovariance.contDiffOn_weights {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} {H : E → Mat2} {T : E → Vec2} (hH : ∀ (i j : Fin 2), ContDiffOn ℝ (↑⊤) (fun (x : E) => H x i j) s) (hT : ∀ (i : Fin 2), ContDiffOn ℝ (↑⊤) (fun (x : E) => T x i) s) (hdet : ∀ x ∈ s, Matrix.det (H x) ≠ 0) (i : Fin 2) : ContDiffOn ℝ (↑⊤) (fun (x : E) => weights (H x) (T x) i) s

Smoothness requires a nonvanishing determinant, independently of positivity.

theorem NavierStokes.SmoothCovariance.contDiffOn_inverse_solution {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} {H : E → Mat2} {T : E → Vec2} (hH : ∀ (i j : Fin 2), ContDiffOn ℝ (↑⊤) (fun (x : E) => H x i j) s) (hT : ∀ (i : Fin 2), ContDiffOn ℝ (↑⊤) (fun (x : E) => T x i) s) (hdet : ∀ x ∈ s, Matrix.det (H x) ≠ 0) (i : Fin 2) : ContDiffOn ℝ (↑⊤) (fun (x : E) => Matrix.mulVec (H x)⁻¹ (T x) i) s

theorem NavierStokes.SmoothCovariance.contDiffOn_amplitudes {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} {H : E → Mat2} {T : E → Vec2} (hH : ∀ (i j : Fin 2), ContDiffOn ℝ (↑⊤) (fun (x : E) => H x i j) s) (hT : ∀ (i : Fin 2), ContDiffOn ℝ (↑⊤) (fun (x : E) => T x i) s) (hcone : ∀ x ∈ s, StrictCone (H x) (T x)) (i : Fin 2) : ContDiffOn ℝ (↑⊤) (fun (x : E) => amplitudes (H x) (T x) i) s

Positive square-root amplitudes are smooth on the strict cone.

theorem NavierStokes.SmoothCovariance.contDiffOn_amplitude_vector {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} {H : E → Mat2} {T : E → Vec2} (hH : ∀ (i j : Fin 2), ContDiffOn ℝ (↑⊤) (fun (x : E) => H x i j) s) (hT : ∀ (i : Fin 2), ContDiffOn ℝ (↑⊤) (fun (x : E) => T x i) s) (hcone : ∀ x ∈ s, StrictCone (H x) (T x)) : ContDiffOn ℝ (↑⊤) (fun (x : E) => amplitudes (H x) (T x)) s

The complete amplitude vector, not only its coordinates, is smooth.

theorem NavierStokes.SmoothCovariance.contDiffOn_signed_coefficients {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} {a b sm sp m t : E → ℝ} (ha : ContDiffOn ℝ (↑⊤) a s) (hb : ContDiffOn ℝ (↑⊤) b s) (hsm : ContDiffOn ℝ (↑⊤) sm s) (hsp : ContDiffOn ℝ (↑⊤) sp s) (hm : ContDiffOn ℝ (↑⊤) m s) (ht : ContDiffOn ℝ (↑⊤) t s) (hpos : ∀ x ∈ s, 0 < a x ∧ 0 < b x ∧ 0 < sm x ∧ 0 < sp x) (i : Fin 2) : ContDiffOn ℝ (↑⊤) (fun (x : E) => Covariance.coefficients (a x) (b x) (sm x) (sp x) (m x) (t x) i) s

Smooth dependence of the coefficients as named in the original exact signed-slot module. All six scalar input functions are genuinely smooth.

theorem NavierStokes.SmoothCovariance.contDiffOn_signed_amplitudes {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} {a b sm sp m t : E → ℝ} (ha : ContDiffOn ℝ (↑⊤) a s) (hb : ContDiffOn ℝ (↑⊤) b s) (hsm : ContDiffOn ℝ (↑⊤) sm s) (hsp : ContDiffOn ℝ (↑⊤) sp s) (hm : ContDiffOn ℝ (↑⊤) m s) (ht : ContDiffOn ℝ (↑⊤) t s) (hpos : ∀ x ∈ s, 0 < a x ∧ 0 < b x ∧ 0 < sm x ∧ 0 < sp x) (hcone : ∀ x ∈ s, |a x * t x| < b x * m x) (i : Fin 2) : ContDiffOn ℝ (↑⊤) (fun (x : E) => Covariance.amplitudes (a x) (b x) (sm x) (sp x) (m x) (t x) i) s

theorem NavierStokes.SmoothCovariance.continuousOn_determinant {X : Type u_1} [TopologicalSpace X] {K : Set X} {H : X → Mat2} (hH : ∀ (i j : Fin 2), ContinuousOn (fun (x : X) => H x i j) K) : ContinuousOn (fun (x : X) => Matrix.det (H x)) K

theorem NavierStokes.SmoothCovariance.continuousOn_numerator {X : Type u_1} [TopologicalSpace X] {K : Set X} {H : X → Mat2} {T : X → Vec2} (hH : ∀ (i j : Fin 2), ContinuousOn (fun (x : X) => H x i j) K) (hT : ∀ (i : Fin 2), ContinuousOn (fun (x : X) => T x i) K) (i : Fin 2) : ContinuousOn (fun (x : X) => cramerNumerator (H x) (T x) i) K

theorem NavierStokes.SmoothCovariance.continuousOn_weights {X : Type u_1} [TopologicalSpace X] {K : Set X} {H : X → Mat2} {T : X → Vec2} (hH : ∀ (i j : Fin 2), ContinuousOn (fun (x : X) => H x i j) K) (hT : ∀ (i : Fin 2), ContinuousOn (fun (x : X) => T x i) K) (hdet : ∀ x ∈ K, Matrix.det (H x) ≠ 0) (i : Fin 2) : ContinuousOn (fun (x : X) => weights (H x) (T x) i) K

theorem NavierStokes.SmoothCovariance.compact_uniform_positive {X : Type u_1} [TopologicalSpace X] {K : Set X} {H : X → Mat2} {T : X → Vec2} (hK : IsCompact K) (hH : ∀ (i j : Fin 2), ContinuousOn (fun (x : X) => H x i j) K) (hT : ∀ (i : Fin 2), ContinuousOn (fun (x : X) => T x i) K) (hcone : ∀ x ∈ K, StrictCone (H x) (T x)) : ∃ (δ : ℝ), 0 < δ ∧ ∀ x ∈ K, δ ≤ |Matrix.det (H x)| ∧ ∀ (i : Fin 2), δ ≤ weights (H x) (T x) i

Compactness supplies an actual common lower bound for the determinant magnitude and both solution coordinates, including an empty parameter set.

theorem NavierStokes.SmoothCovariance.compact_uniform_amplitudes {X : Type u_1} [TopologicalSpace X] {K : Set X} {H : X → Mat2} {T : X → Vec2} (hK : IsCompact K) (hH : ∀ (i j : Fin 2), ContinuousOn (fun (x : X) => H x i j) K) (hT : ∀ (i : Fin 2), ContinuousOn (fun (x : X) => T x i) K) (hcone : ∀ x ∈ K, StrictCone (H x) (T x)) : ∃ (δ : ℝ), 0 < δ ∧ ∀ x ∈ K, δ ≤ |Matrix.det (H x)| ∧ ∀ (i : Fin 2), δ ≤ weights (H x) (T x) i ∧ δ ≤ amplitudes (H x) (T x) i

The same compact family keeps every positive amplitude uniformly away from zero; no claim is made for a family touching a zero-stress edge.

def NavierStokes.SmoothCovariance.strictConeRegion : Set Datum

The strict area inequalities define an open set of matrix-target pairs.

Equations

• NavierStokes.SmoothCovariance.strictConeRegion = {z : NavierStokes.SmoothCovariance.Datum | NavierStokes.SmoothCovariance.StrictCone z.1 z.2}

theorem NavierStokes.SmoothCovariance.isOpen_strictConeRegion : IsOpen strictConeRegion

theorem NavierStokes.SmoothCovariance.contDiffOn_universal_weights : ContDiffOn ℝ (↑⊤) (fun (z : Datum) => weights z.1 z.2) strictConeRegion

The solution map itself is C-infinity on the open set of admissible matrix-target data, without a prechosen parameterization.

theorem NavierStokes.SmoothCovariance.contDiffOn_universal_amplitudes : ContDiffOn ℝ (↑⊤) (fun (z : Datum) => amplitudes z.1 z.2) strictConeRegion

The positive square-root solution is C-infinity on that same open set.

theorem NavierStokes.SmoothCovariance.compact_perturbation_stability {S : Set Datum} (hS : IsCompact S) (hcone : S ⊆ strictConeRegion) : ∃ (ρ : ℝ), 0 < ρ ∧ ∀ z ∈ S, ∀ (z' : Datum), dist z' z ≤ ρ → StrictCone z'.1 z'.2

A single positive perturbation radius works for every datum in a compact subset of the strict cone. The perturbed data may be arbitrary actual matrices.

theorem NavierStokes.SmoothCovariance.compact_family_perturbation_stability {X : Type u_1} [TopologicalSpace X] {K : Set X} (hK : IsCompact K) {H : X → Mat2} {T : X → Vec2} (hH : ∀ (i j : Fin 2), ContinuousOn (fun (x : X) => H x i j) K) (hT : ∀ (i : Fin 2), ContinuousOn (fun (x : X) => T x i) K) (hcone : ∀ x ∈ K, StrictCone (H x) (T x)) : ∃ (ρ : ℝ), 0 < ρ ∧ ∀ x ∈ K, ∀ (H' : Mat2) (T' : Vec2), dist (H', T') (H x, T x) ≤ ρ → Matrix.det H' ≠ 0 ∧ (∀ (i : Fin 2), 0 < weights H' T' i) ∧ ∀ (i : Fin 2), 0 < amplitudes H' T' i

Uniform perturbation stability for a continuous family on a compact parameter set. Competing matrices need not form a continuous family.

Covariance amplitudes across an exponential-flat edge

The normalized matrix and target are actual smooth functions with an explicit strict cone. Columns are then multiplied by edge κᵢ, and the target by edge σ. Exact inverse and square-root identities exhibit a positive remaining exponential whenever κᵢ < σ; in particular the squared-factor convention κᵢ = 2 λᵢ is covered by λᵢ < σ / 2.

The coefficient quotients are proved smooth from these formulas. Their smoothness across the singular matrix at the edge is not assumed.

def NavierStokes.FlatCovariance.columns (G : SmoothCovariance.Mat2) (c : SmoothCovariance.Vec2) : SmoothCovariance.Mat2

Multiplication of column j by its scalar factor c j.

Equations

• NavierStokes.FlatCovariance.columns G c i j = c j * G i j

def NavierStokes.FlatCovariance.scaledTarget (r : ℝ) (T : SmoothCovariance.Vec2) : SmoothCovariance.Vec2

Scaled target, defined pointwise by r * T i.

Equations

• NavierStokes.FlatCovariance.scaledTarget r T i = r * T i

noncomputable def NavierStokes.FlatCovariance.edgeMatrix (κ : SmoothCovariance.Vec2) (G : ℝ → SmoothCovariance.Mat2) (x : ℝ) : SmoothCovariance.Mat2

The actual edge-degenerate covariance matrix.

Equations

• NavierStokes.FlatCovariance.edgeMatrix κ G x = NavierStokes.FlatCovariance.columns (G x) fun (j : Fin 2) => NavierStokes.FlatCutoff.edge (κ j) x

noncomputable def NavierStokes.FlatCovariance.edgeTarget (σ : ℝ) (T : ℝ → SmoothCovariance.Vec2) (x : ℝ) : SmoothCovariance.Vec2

Edge target, given by scaledTarget (edge σ x) (T x).

Equations

• NavierStokes.FlatCovariance.edgeTarget σ T x = NavierStokes.FlatCovariance.scaledTarget (NavierStokes.FlatCutoff.edge σ x) (T x)

noncomputable def NavierStokes.FlatCovariance.inverseCoefficients (σ : ℝ) (κ : SmoothCovariance.Vec2) (G : ℝ → SmoothCovariance.Mat2) (T : ℝ → SmoothCovariance.Vec2) (x : ℝ) : SmoothCovariance.Vec2

The actual matrix-inverse solve, also defined at the zero edge.

Equations

• NavierStokes.FlatCovariance.inverseCoefficients σ κ G T x = Matrix.mulVec (NavierStokes.FlatCovariance.edgeMatrix κ G x)⁻¹ (NavierStokes.FlatCovariance.edgeTarget σ T x)

noncomputable def NavierStokes.FlatCovariance.primaryAmplitude (σ : ℝ) (κ : SmoothCovariance.Vec2) (G : ℝ → SmoothCovariance.Mat2) (T : ℝ → SmoothCovariance.Vec2) (x : ℝ) : SmoothCovariance.Vec2

Primary amplitude, defined pointwise by Real.sqrt (inverseCoefficients σ κ G T x i).

Equations

• NavierStokes.FlatCovariance.primaryAmplitude σ κ G T x i = √(NavierStokes.FlatCovariance.inverseCoefficients σ κ G T x i)

noncomputable def NavierStokes.FlatCovariance.signedAmplitude (σ τ : ℝ) (κ : SmoothCovariance.Vec2) (G : ℝ → SmoothCovariance.Mat2) (T R : ℝ → SmoothCovariance.Vec2) (x : ℝ) : SmoothCovariance.Vec2

The signed covariance update divides by the fixed positive primary.

Equations

• NavierStokes.FlatCovariance.signedAmplitude σ τ κ G T R x i = NavierStokes.FlatCovariance.inverseCoefficients τ κ G R x i / (2 * NavierStokes.FlatCovariance.primaryAmplitude σ κ G T x i)

theorem NavierStokes.FlatCovariance.sqrt_edge (c x : ℝ) : √(FlatCutoff.edge c x) = FlatCutoff.edge (c / 2) x

theorem NavierStokes.FlatCovariance.edge_mul (c d x : ℝ) : FlatCutoff.edge c x * FlatCutoff.edge d x = FlatCutoff.edge (c + d) x

theorem NavierStokes.FlatCovariance.edge_sq (c x : ℝ) : FlatCutoff.edge c x ^ 2 = FlatCutoff.edge (2 * c) x

theorem NavierStokes.FlatCovariance.squared_column_factors (lam : SmoothCovariance.Vec2) (G : ℝ → SmoothCovariance.Mat2) (x : ℝ) : (columns (G x) fun (j : Fin 2) => FlatCutoff.edge (lam j) x ^ 2) = edgeMatrix (fun (j : Fin 2) => 2 * lam j) G x

theorem NavierStokes.FlatCovariance.determinant_columns (G : SmoothCovariance.Mat2) (c : SmoothCovariance.Vec2) : Matrix.det (columns G c) = c 0 * c 1 * Matrix.det G

theorem NavierStokes.FlatCovariance.columns_det_ne_zero {G : SmoothCovariance.Mat2} {c : SmoothCovariance.Vec2} (hG : Matrix.det G ≠ 0) (hc : ∀ (i : Fin 2), c i ≠ 0) : Matrix.det (columns G c) ≠ 0

theorem NavierStokes.FlatCovariance.weights_columns (G : SmoothCovariance.Mat2) (c T : SmoothCovariance.Vec2) (r : ℝ) (hG : Matrix.det G ≠ 0) (hc : ∀ (i : Fin 2), c i ≠ 0) (i : Fin 2) : SmoothCovariance.weights (columns G c) (scaledTarget r T) i = r / c i * SmoothCovariance.weights G T i

Cramer's formula records the exact effect of individual column factors.

theorem NavierStokes.FlatCovariance.edgeMatrix_det_ne_zero {κ : SmoothCovariance.Vec2} {G : ℝ → SmoothCovariance.Mat2} {x : ℝ} (hG : Matrix.det (G x) ≠ 0) (hx : 0 < x) : Matrix.det (edgeMatrix κ G x) ≠ 0

theorem NavierStokes.FlatCovariance.inverseCoefficients_of_nonpos (σ : ℝ) (κ : SmoothCovariance.Vec2) (G : ℝ → SmoothCovariance.Mat2) (T : ℝ → SmoothCovariance.Vec2) {x : ℝ} (hx : x ≤ 0) : inverseCoefficients σ κ G T x = 0

theorem NavierStokes.FlatCovariance.primaryAmplitude_of_nonpos (σ : ℝ) (κ : SmoothCovariance.Vec2) (G : ℝ → SmoothCovariance.Mat2) (T : ℝ → SmoothCovariance.Vec2) {x : ℝ} (hx : x ≤ 0) (i : Fin 2) : primaryAmplitude σ κ G T x i = 0

theorem NavierStokes.FlatCovariance.signedAmplitude_of_nonpos (σ τ : ℝ) (κ : SmoothCovariance.Vec2) (G : ℝ → SmoothCovariance.Mat2) (T R : ℝ → SmoothCovariance.Vec2) {x : ℝ} (hx : x ≤ 0) (i : Fin 2) : signedAmplitude σ τ κ G T R x i = 0

theorem NavierStokes.FlatCovariance.inverseCoefficients_factor (σ : ℝ) (κ : SmoothCovariance.Vec2) (G : ℝ → SmoothCovariance.Mat2) (T : ℝ → SmoothCovariance.Vec2) {x : ℝ} (hG : Matrix.det (G x) ≠ 0) (i : Fin 2) : inverseCoefficients σ κ G T x i = FlatCutoff.edge (σ - κ i) x * SmoothCovariance.weights (G x) (T x) i

Exact cancellation of the column exponential in the actual inverse. This identity includes the edge and the full zero half-line.

theorem NavierStokes.FlatCovariance.primaryAmplitude_factor (σ : ℝ) (κ : SmoothCovariance.Vec2) (G : ℝ → SmoothCovariance.Mat2) (T : ℝ → SmoothCovariance.Vec2) {x : ℝ} (hG : Matrix.det (G x) ≠ 0) (i : Fin 2) : primaryAmplitude σ κ G T x i = FlatCutoff.edge ((σ - κ i) / 2) x * SmoothCovariance.amplitudes (G x) (T x) i

Taking the square root halves the remaining exponential exponent.

theorem NavierStokes.FlatCovariance.signedAmplitude_factor (σ τ : ℝ) (κ : SmoothCovariance.Vec2) (G : ℝ → SmoothCovariance.Mat2) (T R : ℝ → SmoothCovariance.Vec2) {x : ℝ} (hG : Matrix.det (G x) ≠ 0) (i : Fin 2) : signedAmplitude σ τ κ G T R x i = FlatCutoff.edge (τ - (σ + κ i) / 2) x * (SmoothCovariance.weights (G x) (R x) i / (2 * SmoothCovariance.amplitudes (G x) (T x) i))

The signed update retains the explicitly computed exponential margin; the target R may have either sign.

theorem NavierStokes.FlatCovariance.inverseCoefficients_target_factor (σ : ℝ) (κ : SmoothCovariance.Vec2) (G : ℝ → SmoothCovariance.Mat2) (T : ℝ → SmoothCovariance.Vec2) (f : ℝ → ℝ) (x : ℝ) (i : Fin 2) : inverseCoefficients σ κ G (fun (y : ℝ) (j : Fin 2) => f y * T y j) x i = f x * inverseCoefficients σ κ G T x i

Exact linearity in a scalar target factor, with no regularity or nonvanishing assumption on that factor.

theorem NavierStokes.FlatCovariance.signedAmplitude_target_factor (σ τ : ℝ) (κ : SmoothCovariance.Vec2) (G : ℝ → SmoothCovariance.Mat2) (T R : ℝ → SmoothCovariance.Vec2) (f : ℝ → ℝ) (x : ℝ) (i : Fin 2) : signedAmplitude σ τ κ G T (fun (y : ℝ) (j : Fin 2) => f y * R y j) x i = f x * signedAmplitude σ τ κ G T R x i

theorem NavierStokes.FlatCovariance.inverseCoefficients_pos {σ : ℝ} {κ : SmoothCovariance.Vec2} {G : ℝ → SmoothCovariance.Mat2} {T : ℝ → SmoothCovariance.Vec2} {x : ℝ} (hcone : SmoothCovariance.StrictCone (G x) (T x)) (hx : 0 < x) (i : Fin 2) : 0 < inverseCoefficients σ κ G T x i

theorem NavierStokes.FlatCovariance.primaryAmplitude_pos {σ : ℝ} {κ : SmoothCovariance.Vec2} {G : ℝ → SmoothCovariance.Mat2} {T : ℝ → SmoothCovariance.Vec2} {x : ℝ} (hcone : SmoothCovariance.StrictCone (G x) (T x)) (hx : 0 < x) (i : Fin 2) : 0 < primaryAmplitude σ κ G T x i

theorem NavierStokes.FlatCovariance.inverse_reconstruct (σ : ℝ) (κ : SmoothCovariance.Vec2) (G : ℝ → SmoothCovariance.Mat2) (T : ℝ → SmoothCovariance.Vec2) {x : ℝ} (hG : Matrix.det (G x) ≠ 0) : Matrix.mulVec (edgeMatrix κ G x) (inverseCoefficients σ κ G T x) = edgeTarget σ T x

The inverse still reconstructs its target at every real point, including the zero half-line where the matrix itself is singular.

theorem NavierStokes.FlatCovariance.primary_reconstruct {σ : ℝ} {κ : SmoothCovariance.Vec2} {G : ℝ → SmoothCovariance.Mat2} {T : ℝ → SmoothCovariance.Vec2} {x : ℝ} (hcone : SmoothCovariance.StrictCone (G x) (T x)) : (Matrix.mulVec (edgeMatrix κ G x) fun (i : Fin 2) => primaryAmplitude σ κ G T x i ^ 2) = edgeTarget σ T x

theorem NavierStokes.FlatCovariance.signed_cross_reconstruct {σ τ : ℝ} {κ : SmoothCovariance.Vec2} {G : ℝ → SmoothCovariance.Mat2} {T R : ℝ → SmoothCovariance.Vec2} {x : ℝ} (hcone : SmoothCovariance.StrictCone (G x) (T x)) : (Matrix.mulVec (edgeMatrix κ G x) fun (i : Fin 2) => 2 * primaryAmplitude σ κ G T x i * signedAmplitude σ τ κ G T R x i) = edgeTarget τ R x

Exact two-sided cross covariance of the primary and signed increment.

theorem NavierStokes.FlatCovariance.edgeMatrix_contDiffOn {s : Set ℝ} {κ : SmoothCovariance.Vec2} {G : ℝ → SmoothCovariance.Mat2} (hG : ∀ (i j : Fin 2), ContDiffOn ℝ (↑⊤) (fun (x : ℝ) => G x i j) s) (hκ : ∀ (i : Fin 2), 0 < κ i) (i j : Fin 2) : ContDiffOn ℝ (↑⊤) (fun (x : ℝ) => edgeMatrix κ G x i j) s

theorem NavierStokes.FlatCovariance.edgeTarget_contDiffOn {s : Set ℝ} {σ : ℝ} {T : ℝ → SmoothCovariance.Vec2} (hT : ∀ (i : Fin 2), ContDiffOn ℝ (↑⊤) (fun (x : ℝ) => T x i) s) (hσ : 0 < σ) (i : Fin 2) : ContDiffOn ℝ (↑⊤) (fun (x : ℝ) => edgeTarget σ T x i) s

theorem NavierStokes.FlatCovariance.inverseCoefficients_contDiffOn {s : Set ℝ} {σ : ℝ} {κ : SmoothCovariance.Vec2} {G : ℝ → SmoothCovariance.Mat2} {T : ℝ → SmoothCovariance.Vec2} (hG : ∀ (i j : Fin 2), ContDiffOn ℝ (↑⊤) (fun (x : ℝ) => G x i j) s) (hT : ∀ (i : Fin 2), ContDiffOn ℝ (↑⊤) (fun (x : ℝ) => T x i) s) (hdet : ∀ x ∈ s, Matrix.det (G x) ≠ 0) (hgap : ∀ (i : Fin 2), κ i < σ) (i : Fin 2) : ContDiffOn ℝ (↑⊤) (fun (x : ℝ) => inverseCoefficients σ κ G T x i) s

Smooth inverse coefficients at the edge, proved by the surviving exponential factor even though the actual matrix degenerates there.

theorem NavierStokes.FlatCovariance.primaryAmplitude_contDiffOn {s : Set ℝ} {σ : ℝ} {κ : SmoothCovariance.Vec2} {G : ℝ → SmoothCovariance.Mat2} {T : ℝ → SmoothCovariance.Vec2} (hG : ∀ (i j : Fin 2), ContDiffOn ℝ (↑⊤) (fun (x : ℝ) => G x i j) s) (hT : ∀ (i : Fin 2), ContDiffOn ℝ (↑⊤) (fun (x : ℝ) => T x i) s) (hcone : ∀ x ∈ s, SmoothCovariance.StrictCone (G x) (T x)) (hgap : ∀ (i : Fin 2), κ i < σ) (i : Fin 2) : ContDiffOn ℝ (↑⊤) (fun (x : ℝ) => primaryAmplitude σ κ G T x i) s

theorem NavierStokes.FlatCovariance.primaryAmplitude_div_pow_contDiffOn {s : Set ℝ} {σ : ℝ} {κ : SmoothCovariance.Vec2} {G : ℝ → SmoothCovariance.Mat2} {T : ℝ → SmoothCovariance.Vec2} (hG : ∀ (i j : Fin 2), ContDiffOn ℝ (↑⊤) (fun (x : ℝ) => G x i j) s) (hT : ∀ (i : Fin 2), ContDiffOn ℝ (↑⊤) (fun (x : ℝ) => T x i) s) (hcone : ∀ x ∈ s, SmoothCovariance.StrictCone (G x) (T x)) (hgap : ∀ (i : Fin 2), κ i < σ) (i : Fin 2) (loss : ℕ) : ContDiffOn ℝ (↑⊤) (fun (x : ℝ) => primaryAmplitude σ κ G T x i / x ^ loss) s

Every fixed inverse-power loss is absorbed by the concrete primary exponential, including at zero.

theorem NavierStokes.FlatCovariance.signed_normal_contDiffOn {s : Set ℝ} {G : ℝ → SmoothCovariance.Mat2} {T R : ℝ → SmoothCovariance.Vec2} (hG : ∀ (i j : Fin 2), ContDiffOn ℝ (↑⊤) (fun (x : ℝ) => G x i j) s) (hT : ∀ (i : Fin 2), ContDiffOn ℝ (↑⊤) (fun (x : ℝ) => T x i) s) (hR : ∀ (i : Fin 2), ContDiffOn ℝ (↑⊤) (fun (x : ℝ) => R x i) s) (hcone : ∀ x ∈ s, SmoothCovariance.StrictCone (G x) (T x)) (i : Fin 2) : ContDiffOn ℝ (↑⊤) (fun (x : ℝ) => SmoothCovariance.weights (G x) (R x) i / (2 * SmoothCovariance.amplitudes (G x) (T x) i)) s

The normalized signed quotient is smooth because its denominator is proved strictly positive from the explicit normalized cone.

theorem NavierStokes.FlatCovariance.signedAmplitude_contDiffOn {s : Set ℝ} {σ τ : ℝ} {κ : SmoothCovariance.Vec2} {G : ℝ → SmoothCovariance.Mat2} {T R : ℝ → SmoothCovariance.Vec2} (hG : ∀ (i j : Fin 2), ContDiffOn ℝ (↑⊤) (fun (x : ℝ) => G x i j) s) (hT : ∀ (i : Fin 2), ContDiffOn ℝ (↑⊤) (fun (x : ℝ) => T x i) s) (hR : ∀ (i : Fin 2), ContDiffOn ℝ (↑⊤) (fun (x : ℝ) => R x i) s) (hcone : ∀ x ∈ s, SmoothCovariance.StrictCone (G x) (T x)) (hgap : ∀ (i : Fin 2), (σ + κ i) / 2 < τ) (i : Fin 2) : ContDiffOn ℝ (↑⊤) (fun (x : ℝ) => signedAmplitude σ τ κ G T R x i) s

theorem NavierStokes.FlatCovariance.signedAmplitude_div_pow_contDiffOn {s : Set ℝ} {σ τ : ℝ} {κ : SmoothCovariance.Vec2} {G : ℝ → SmoothCovariance.Mat2} {T R : ℝ → SmoothCovariance.Vec2} (hG : ∀ (i j : Fin 2), ContDiffOn ℝ (↑⊤) (fun (x : ℝ) => G x i j) s) (hT : ∀ (i : Fin 2), ContDiffOn ℝ (↑⊤) (fun (x : ℝ) => T x i) s) (hR : ∀ (i : Fin 2), ContDiffOn ℝ (↑⊤) (fun (x : ℝ) => R x i) s) (hcone : ∀ x ∈ s, SmoothCovariance.StrictCone (G x) (T x)) (hgap : ∀ (i : Fin 2), (σ + κ i) / 2 < τ) (i : Fin 2) (loss : ℕ) : ContDiffOn ℝ (↑⊤) (fun (x : ℝ) => signedAmplitude σ τ κ G T R x i / x ^ loss) s

theorem NavierStokes.FlatCovariance.signed_inverse_power_target_contDiffOn {s : Set ℝ} {σ τ : ℝ} {κ : SmoothCovariance.Vec2} {G : ℝ → SmoothCovariance.Mat2} {T R : ℝ → SmoothCovariance.Vec2} (hG : ∀ (i j : Fin 2), ContDiffOn ℝ (↑⊤) (fun (x : ℝ) => G x i j) s) (hT : ∀ (i : Fin 2), ContDiffOn ℝ (↑⊤) (fun (x : ℝ) => T x i) s) (hR : ∀ (i : Fin 2), ContDiffOn ℝ (↑⊤) (fun (x : ℝ) => R x i) s) (hcone : ∀ x ∈ s, SmoothCovariance.StrictCone (G x) (T x)) (hgap : ∀ (i : Fin 2), (σ + κ i) / 2 < τ) (i : Fin 2) (loss : ℕ) : ContDiffOn ℝ (↑⊤) (fun (x : ℝ) => signedAmplitude σ τ κ G T (fun (y : ℝ) (j : Fin 2) => (y ^ loss)⁻¹ * R y j) x i) s

An actual signed-stress numerator with an inverse-power loss still gives a smooth signed amplitude. Smoothness of the singular quotient is a result.

theorem NavierStokes.FlatCovariance.squared_factors_smooth {s : Set ℝ} {σ : ℝ} {G : ℝ → SmoothCovariance.Mat2} {T R : ℝ → SmoothCovariance.Vec2} {lam : SmoothCovariance.Vec2} (hG : ∀ (i j : Fin 2), ContDiffOn ℝ (↑⊤) (fun (x : ℝ) => G x i j) s) (hT : ∀ (i : Fin 2), ContDiffOn ℝ (↑⊤) (fun (x : ℝ) => T x i) s) (hR : ∀ (i : Fin 2), ContDiffOn ℝ (↑⊤) (fun (x : ℝ) => R x i) s) (hcone : ∀ x ∈ s, SmoothCovariance.StrictCone (G x) (T x)) (hgap : ∀ (i : Fin 2), lam i < σ / 2) (i : Fin 2) (loss : ℕ) : ContDiffOn ℝ (↑⊤) (fun (x : ℝ) => primaryAmplitude σ (fun (j : Fin 2) => 2 * lam j) G T x i / x ^ loss) s ∧ ContDiffOn ℝ (↑⊤) (fun (x : ℝ) => signedAmplitude σ σ (fun (j : Fin 2) => 2 * lam j) G T R x i / x ^ loss) s

When a fundamental column factor is edge λᵢ and covariance therefore carries its square, the concrete condition is exactly λᵢ < σ / 2. A signed stress with the same target envelope retains the same flat exponent.

theorem NavierStokes.FlatCovariance.direct_half_factors_smooth {s : Set ℝ} {σ : ℝ} {κ : SmoothCovariance.Vec2} {G : ℝ → SmoothCovariance.Mat2} {T R : ℝ → SmoothCovariance.Vec2} (hG : ∀ (i j : Fin 2), ContDiffOn ℝ (↑⊤) (fun (x : ℝ) => G x i j) s) (hT : ∀ (i : Fin 2), ContDiffOn ℝ (↑⊤) (fun (x : ℝ) => T x i) s) (hR : ∀ (i : Fin 2), ContDiffOn ℝ (↑⊤) (fun (x : ℝ) => R x i) s) (hcone : ∀ x ∈ s, SmoothCovariance.StrictCone (G x) (T x)) (hσ : 0 < σ) (hgap : ∀ (i : Fin 2), κ i < σ / 2) (i : Fin 2) (loss : ℕ) : ContDiffOn ℝ (↑⊤) (fun (x : ℝ) => primaryAmplitude σ κ G T x i / x ^ loss) s ∧ ContDiffOn ℝ (↑⊤) (fun (x : ℝ) => signedAmplitude σ σ κ G T R x i / x ^ loss) s

The requested stricter half-exponent condition also suffices when the exponential appears directly in a covariance column, without a square.

theorem NavierStokes.FlatCovariance.compact_weighted_lower_bounds {K : Set ℝ} (hK : IsCompact K) {σ : ℝ} {κ : SmoothCovariance.Vec2} {G : ℝ → SmoothCovariance.Mat2} {T : ℝ → SmoothCovariance.Vec2} (hG : ∀ (i j : Fin 2), ContinuousOn (fun (x : ℝ) => G x i j) K) (hT : ∀ (i : Fin 2), ContinuousOn (fun (x : ℝ) => T x i) K) (hcone : ∀ x ∈ K, SmoothCovariance.StrictCone (G x) (T x)) : ∃ (δ : ℝ), 0 < δ ∧ ∀ x ∈ K, ∀ (i : Fin 2), δ * FlatCutoff.edge (σ - κ i) x ≤ inverseCoefficients σ κ G T x i ∧ δ * FlatCutoff.edge ((σ - κ i) / 2) x ≤ primaryAmplitude σ κ G T x i

Concrete compact-family lower bounds with the vanishing factors left explicit. In particular the primary square-root denominator is controlled.

theorem NavierStokes.FlatCovariance.iteratedDeriv_zero_of_nonpos_zero {f : ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hzero : ∀ x ≤ 0, f x = 0) (n : ℕ) : iteratedDeriv n f 0 = 0

A smooth function that is zero on the nonpositive half-line has every derivative zero at the joining point.

theorem NavierStokes.FlatCovariance.primaryAmplitude_div_pow_contDiff {σ : ℝ} {κ : SmoothCovariance.Vec2} {G : ℝ → SmoothCovariance.Mat2} {T : ℝ → SmoothCovariance.Vec2} (hG : ∀ (i j : Fin 2), ContDiff ℝ ↑⊤ fun (x : ℝ) => G x i j) (hT : ∀ (i : Fin 2), ContDiff ℝ ↑⊤ fun (x : ℝ) => T x i) (hcone : ∀ (x : ℝ), SmoothCovariance.StrictCone (G x) (T x)) (hgap : ∀ (i : Fin 2), κ i < σ) (i : Fin 2) (loss : ℕ) : ContDiff ℝ ↑⊤ fun (x : ℝ) => primaryAmplitude σ κ G T x i / x ^ loss

theorem NavierStokes.FlatCovariance.signedAmplitude_div_pow_contDiff {σ τ : ℝ} {κ : SmoothCovariance.Vec2} {G : ℝ → SmoothCovariance.Mat2} {T R : ℝ → SmoothCovariance.Vec2} (hG : ∀ (i j : Fin 2), ContDiff ℝ ↑⊤ fun (x : ℝ) => G x i j) (hT : ∀ (i : Fin 2), ContDiff ℝ ↑⊤ fun (x : ℝ) => T x i) (hR : ∀ (i : Fin 2), ContDiff ℝ ↑⊤ fun (x : ℝ) => R x i) (hcone : ∀ (x : ℝ), SmoothCovariance.StrictCone (G x) (T x)) (hgap : ∀ (i : Fin 2), (σ + κ i) / 2 < τ) (i : Fin 2) (loss : ℕ) : ContDiff ℝ ↑⊤ fun (x : ℝ) => signedAmplitude σ τ κ G T R x i / x ^ loss

theorem NavierStokes.FlatCovariance.primary_weighted_derivatives_zero {σ : ℝ} {κ : SmoothCovariance.Vec2} {G : ℝ → SmoothCovariance.Mat2} {T : ℝ → SmoothCovariance.Vec2} (hG : ∀ (i j : Fin 2), ContDiff ℝ ↑⊤ fun (x : ℝ) => G x i j) (hT : ∀ (i : Fin 2), ContDiff ℝ ↑⊤ fun (x : ℝ) => T x i) (hcone : ∀ (x : ℝ), SmoothCovariance.StrictCone (G x) (T x)) (hgap : ∀ (i : Fin 2), κ i < σ) (i : Fin 2) (loss n : ℕ) : iteratedDeriv n (fun (x : ℝ) => primaryAmplitude σ κ G T x i / x ^ loss) 0 = 0

Actual all-order flatness of the primary, also after every fixed inverse-power loss, obtained from the proved smooth zero extension.

theorem NavierStokes.FlatCovariance.signed_weighted_derivatives_zero {σ τ : ℝ} {κ : SmoothCovariance.Vec2} {G : ℝ → SmoothCovariance.Mat2} {T R : ℝ → SmoothCovariance.Vec2} (hG : ∀ (i j : Fin 2), ContDiff ℝ ↑⊤ fun (x : ℝ) => G x i j) (hT : ∀ (i : Fin 2), ContDiff ℝ ↑⊤ fun (x : ℝ) => T x i) (hR : ∀ (i : Fin 2), ContDiff ℝ ↑⊤ fun (x : ℝ) => R x i) (hcone : ∀ (x : ℝ), SmoothCovariance.StrictCone (G x) (T x)) (hgap : ∀ (i : Fin 2), (σ + κ i) / 2 < τ) (i : Fin 2) (loss n : ℕ) : iteratedDeriv n (fun (x : ℝ) => signedAmplitude σ τ κ G T R x i / x ^ loss) 0 = 0

noncomputable def NavierStokes.FlatCovariance.parameterPrimary {E : Type u_1} (σ : ℝ) (κ : SmoothCovariance.Vec2) (d : E → ℝ) (G : E → SmoothCovariance.Mat2) (T : E → SmoothCovariance.Vec2) (z : E) : SmoothCovariance.Vec2

Evaluation of the actual inverse amplitude at a smooth signed edge coordinate, with independent smooth parameters in the normalized data.

Equations

• NavierStokes.FlatCovariance.parameterPrimary σ κ d G T z = NavierStokes.FlatCovariance.primaryAmplitude σ κ (fun (x : ℝ) => G z) (fun (x : ℝ) => T z) (d z)

noncomputable def NavierStokes.FlatCovariance.parameterSigned {E : Type u_1} (σ τ : ℝ) (κ : SmoothCovariance.Vec2) (d : E → ℝ) (G : E → SmoothCovariance.Mat2) (T R : E → SmoothCovariance.Vec2) (z : E) : SmoothCovariance.Vec2

Parameter signed, given by signedAmplitude σ τ κ (fun _ => G z) (fun _ => T z) (fun _ => R z) (d z).

Equations

• NavierStokes.FlatCovariance.parameterSigned σ τ κ d G T R z = NavierStokes.FlatCovariance.signedAmplitude σ τ κ (fun (x : ℝ) => G z) (fun (x : ℝ) => T z) (fun (x : ℝ) => R z) (d z)

theorem NavierStokes.FlatCovariance.parameterPrimary_of_nonpos {E : Type u_1} (σ : ℝ) (κ : SmoothCovariance.Vec2) (d : E → ℝ) (G : E → SmoothCovariance.Mat2) (T : E → SmoothCovariance.Vec2) {z : E} (hz : d z ≤ 0) (i : Fin 2) : parameterPrimary σ κ d G T z i = 0

theorem NavierStokes.FlatCovariance.parameterSigned_of_nonpos {E : Type u_1} (σ τ : ℝ) (κ : SmoothCovariance.Vec2) (d : E → ℝ) (G : E → SmoothCovariance.Mat2) (T R : E → SmoothCovariance.Vec2) {z : E} (hz : d z ≤ 0) (i : Fin 2) : parameterSigned σ τ κ d G T R z i = 0

theorem NavierStokes.FlatCovariance.parameterPrimary_div_pow_contDiffOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} {σ : ℝ} {κ : SmoothCovariance.Vec2} {d : E → ℝ} {G : E → SmoothCovariance.Mat2} {T : E → SmoothCovariance.Vec2} (hd : ContDiffOn ℝ (↑⊤) d s) (hG : ∀ (i j : Fin 2), ContDiffOn ℝ (↑⊤) (fun (z : E) => G z i j) s) (hT : ∀ (i : Fin 2), ContDiffOn ℝ (↑⊤) (fun (z : E) => T z i) s) (hcone : ∀ z ∈ s, SmoothCovariance.StrictCone (G z) (T z)) (hgap : ∀ (i : Fin 2), κ i < σ) (i : Fin 2) (loss : ℕ) : ContDiffOn ℝ (↑⊤) (fun (z : E) => parameterPrimary σ κ d G T z i / d z ^ loss) s

Joint smoothness in the edge coordinate and all additional parameters, after any fixed inverse power of the edge coordinate.

theorem NavierStokes.FlatCovariance.parameterSigned_div_pow_contDiffOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} {σ τ : ℝ} {κ : SmoothCovariance.Vec2} {d : E → ℝ} {G : E → SmoothCovariance.Mat2} {T R : E → SmoothCovariance.Vec2} (hd : ContDiffOn ℝ (↑⊤) d s) (hG : ∀ (i j : Fin 2), ContDiffOn ℝ (↑⊤) (fun (z : E) => G z i j) s) (hT : ∀ (i : Fin 2), ContDiffOn ℝ (↑⊤) (fun (z : E) => T z i) s) (hR : ∀ (i : Fin 2), ContDiffOn ℝ (↑⊤) (fun (z : E) => R z i) s) (hcone : ∀ z ∈ s, SmoothCovariance.StrictCone (G z) (T z)) (hgap : ∀ (i : Fin 2), (σ + κ i) / 2 < τ) (i : Fin 2) (loss : ℕ) : ContDiffOn ℝ (↑⊤) (fun (z : E) => parameterSigned σ τ κ d G T R z i / d z ^ loss) s

noncomputable def NavierStokes.PulseCovariance.gaussian (b m r v : ℝ) : ℝ

Gaussian, given by Real.exp (-b * ((v - m) / r) ^ 2).

Equations

• NavierStokes.PulseCovariance.gaussian b m r v = Real.exp (-b * ((v - m) / r) ^ 2)

noncomputable def NavierStokes.PulseCovariance.firstGaussianMoment (b : ℝ) : ℝ

First gaussian moment, given by ∫ v : ℝ, |v| * Real.exp (-b * v ^ 2).

Equations

• NavierStokes.PulseCovariance.firstGaussianMoment b = ∫ (v : ℝ), |v| * Real.exp (-b * v ^ 2)

theorem NavierStokes.PulseCovariance.gaussian_pos (b m r v : ℝ) : 0 < gaussian b m r v

theorem NavierStokes.PulseCovariance.gaussian_eq_length (b m r v : ℝ) : gaussian b m r v = Real.exp (-b * (v - m) ^ 2 / r ^ 2)

theorem NavierStokes.PulseCovariance.reference_envelope_gaussian_bounds {lam u : ℝ} (hlam : 0 < lam) (hu : 0 < u) : ∃ (b : ℝ) (B : ℝ), 0 < b ∧ 0 < B ∧ ∀ (r : ℝ), 0 < r → ∀ v ∈ Set.Icc 0 (r ^ 2), gaussian B (r ^ 2 / 2) r v ≤ GaussianEnvelope.envelope (GaussianEnvelope.referenceRate lam u (r ^ 2)) (r ^ 2 / 2) v ∧ GaussianEnvelope.envelope (GaussianEnvelope.referenceRate lam u (r ^ 2)) (r ^ 2 / 2) v ≤ gaussian b (r ^ 2 / 2) r v

The reference ODE envelope already constructed in GaussianEnvelope supplies the pointwise Gaussian hypotheses with constants independent of slot length.

theorem NavierStokes.PulseCovariance.integrable_gaussian {b r : ℝ} (hb : 0 < b) (hr : 0 < r) (m : ℝ) : MeasureTheory.Integrable (gaussian b m r) MeasureTheory.volume

theorem NavierStokes.PulseCovariance.integral_gaussian_scaled (b m r : ℝ) (hr : 0 < r) : ∫ (v : ℝ), gaussian b m r v = r * √(Real.pi / b)

theorem NavierStokes.PulseCovariance.integrable_first_gaussian {b : ℝ} (hb : 0 < b) : MeasureTheory.Integrable (fun (v : ℝ) => |v| * Real.exp (-b * v ^ 2)) MeasureTheory.volume

theorem NavierStokes.PulseCovariance.firstGaussianMoment_nonneg (b : ℝ) : 0 ≤ firstGaussianMoment b

theorem NavierStokes.PulseCovariance.abs_sub_scaled {r : ℝ} (hr : 0 < r) (v m : ℝ) : |v - m| = r * |(v - m) / r|

theorem NavierStokes.PulseCovariance.integrable_first_gaussian_scaled {b r : ℝ} (hb : 0 < b) (hr : 0 < r) (m : ℝ) : MeasureTheory.Integrable (fun (v : ℝ) => |v - m| * gaussian b m r v) MeasureTheory.volume

theorem NavierStokes.PulseCovariance.integral_first_gaussian_scaled (b m r : ℝ) (hr : 0 < r) : ∫ (v : ℝ), |v - m| * gaussian b m r v = r ^ 2 * firstGaussianMoment b

noncomputable def NavierStokes.PulseCovariance.weight (ψ x : ℝ → ℝ) (v : ℝ) : ℝ

Weight, given by ψ v ^ 2 * x v ^ 2.

Equations

• NavierStokes.PulseCovariance.weight ψ x v = ψ v ^ 2 * x v ^ 2

noncomputable def NavierStokes.PulseCovariance.mass (ψ x : ℝ → ℝ) : ℝ

Mass, given by ∫ v : ℝ, weight ψ x v.

Equations

• NavierStokes.PulseCovariance.mass ψ x = ∫ (v : ℝ), NavierStokes.PulseCovariance.weight ψ x v

noncomputable def NavierStokes.PulseCovariance.centeredMoment (ψ x : ℝ → ℝ) (m : ℝ) : ℝ

Centered moment, given by ∫ v : ℝ, |v - m| * weight ψ x v.

Equations

• NavierStokes.PulseCovariance.centeredMoment ψ x m = ∫ (v : ℝ), |v - m| * NavierStokes.PulseCovariance.weight ψ x v

structure NavierStokes.PulseCovariance.PulseBounds (r a A b B : ℝ) (ψ x : ℝ → ℝ) : Prop

All assumptions concern actual pointwise functions on the slot. No integrated covariance bound is an input.

• radius_one_le : 1 ≤ r
• lower_pos : 0 < a
• upper_pos : 0 < A
• decay_pos : 0 < b
• lower_decay_pos : 0 < B
• cutoff_continuous : Continuous ψ
• component_continuous : Continuous x
• cutoff_abs_le (v : ℝ) : |ψ v| ≤ 1
• cutoff_zero (v : ℝ) : v ∉ Set.Icc (r ^ 2 / 6) (5 * r ^ 2 / 6) → ψ v = 0
• cutoff_one (v : ℝ) : v ∈ Set.Icc (r ^ 2 / 3) (2 * r ^ 2 / 3) → ψ v = 1
• component_lower (v : ℝ) : v ∈ Set.Icc 0 (r ^ 2) → a * gaussian B (r ^ 2 / 2) r v ≤ x v
• component_upper (v : ℝ) : v ∈ Set.Icc 0 (r ^ 2) → x v ≤ A * gaussian b (r ^ 2 / 2) r v

structure NavierStokes.PulseCovariance.CutoffBounds (r : ℝ) (ψ : ℝ → ℝ) : Prop

The cutoff conditions, separated from the ODE envelope for the adapter.

• continuous : Continuous ψ
• abs_le (v : ℝ) : |ψ v| ≤ 1
• zero_outside (v : ℝ) : v ∉ Set.Icc (r ^ 2 / 6) (5 * r ^ 2 / 6) → ψ v = 0
• one_inside (v : ℝ) : v ∈ Set.Icc (r ^ 2 / 3) (2 * r ^ 2 / 3) → ψ v = 1

theorem NavierStokes.PulseCovariance.pulseBounds_of_envelope {r a A b B : ℝ} {ψ x P : ℝ → ℝ} (hr : 1 ≤ r) (ha : 0 < a) (hA : 0 < A) (hb : 0 < b) (hB : 0 < B) (hψ : CutoffBounds r ψ) (hx : Continuous x) (hP : ∀ v ∈ Set.Icc 0 (r ^ 2), gaussian B (r ^ 2 / 2) r v ≤ P v ∧ P v ≤ gaussian b (r ^ 2 / 2) r v) (hcompare : ∀ v ∈ Set.Icc 0 (r ^ 2), a * P v ≤ x v ∧ x v ≤ A * P v) : PulseBounds r a A b B ψ x

Direct adapter from the growing-mode comparison a P ≤ x ≤ A P and two-sided Gaussian estimates on the actual reference envelope P.

theorem NavierStokes.PulseCovariance.PulseBounds.radius_pos {r a A b B : ℝ} {ψ x : ℝ → ℝ} (h : PulseBounds r a A b B ψ x) : 0 < r

theorem NavierStokes.PulseCovariance.PulseBounds.component_pos {r a A b B : ℝ} {ψ x : ℝ → ℝ} (h : PulseBounds r a A b B ψ x) {v : ℝ} (hv : v ∈ Set.Icc 0 (r ^ 2)) : 0 < x v

theorem NavierStokes.PulseCovariance.PulseBounds.weight_nonneg {ψ x : ℝ → ℝ} (v : ℝ) : 0 ≤ weight ψ x v

theorem NavierStokes.PulseCovariance.PulseBounds.weight_continuous {r a A b B : ℝ} {ψ x : ℝ → ℝ} (h : PulseBounds r a A b B ψ x) : Continuous (weight ψ x)

theorem NavierStokes.PulseCovariance.PulseBounds.weight_gaussian_upper {r a A b B : ℝ} {ψ x : ℝ → ℝ} (h : PulseBounds r a A b B ψ x) (v : ℝ) : weight ψ x v ≤ A ^ 2 * gaussian (2 * b) (r ^ 2 / 2) r v

theorem NavierStokes.PulseCovariance.PulseBounds.weight_integrable {r a A b B : ℝ} {ψ x : ℝ → ℝ} (h : PulseBounds r a A b B ψ x) : MeasureTheory.Integrable (weight ψ x) MeasureTheory.volume

theorem NavierStokes.PulseCovariance.PulseBounds.moment_integrable {r a A b B : ℝ} {ψ x : ℝ → ℝ} (h : PulseBounds r a A b B ψ x) : MeasureTheory.Integrable (fun (v : ℝ) => |v - r ^ 2 / 2| * weight ψ x v) MeasureTheory.volume

theorem NavierStokes.PulseCovariance.PulseBounds.mass_upper {r a A b B : ℝ} {ψ x : ℝ → ℝ} (h : PulseBounds r a A b B ψ x) : mass ψ x ≤ A ^ 2 * √(Real.pi / (2 * b)) * r

theorem NavierStokes.PulseCovariance.PulseBounds.moment_upper {r a A b B : ℝ} {ψ x : ℝ → ℝ} (h : PulseBounds r a A b B ψ x) : centeredMoment ψ x (r ^ 2 / 2) ≤ A ^ 2 * firstGaussianMoment (2 * b) * r ^ 2

theorem NavierStokes.PulseCovariance.PulseBounds.core_mem_middle {r a A b B : ℝ} {ψ x : ℝ → ℝ} (h : PulseBounds r a A b B ψ x) {v : ℝ} (hv : v ∈ Set.Icc (r ^ 2 / 2 - r / 6) (r ^ 2 / 2 + r / 6)) : v ∈ Set.Icc (r ^ 2 / 3) (2 * r ^ 2 / 3)

theorem NavierStokes.PulseCovariance.PulseBounds.core_scaled_sq {r a A b B : ℝ} {ψ x : ℝ → ℝ} (h : PulseBounds r a A b B ψ x) {v : ℝ} (hv : v ∈ Set.Icc (r ^ 2 / 2 - r / 6) (r ^ 2 / 2 + r / 6)) : ((v - r ^ 2 / 2) / r) ^ 2 ≤ 1 / 36

theorem NavierStokes.PulseCovariance.PulseBounds.core_weight_lower {r a A b B : ℝ} {ψ x : ℝ → ℝ} (h : PulseBounds r a A b B ψ x) {v : ℝ} (hv : v ∈ Set.Icc (r ^ 2 / 2 - r / 6) (r ^ 2 / 2 + r / 6)) : a ^ 2 * Real.exp (-B / 18) ≤ weight ψ x v

noncomputable def NavierStokes.PulseCovariance.PulseBounds.lowerMassConstant (a B : ℝ) : ℝ

Lower mass constant, given by a ^ 2 * Real.exp (-B / 18) / 3.

Equations

• NavierStokes.PulseCovariance.PulseBounds.lowerMassConstant a B = a ^ 2 * Real.exp (-B / 18) / 3

theorem NavierStokes.PulseCovariance.PulseBounds.lowerMassConstant_pos {r a A b B : ℝ} {ψ x : ℝ → ℝ} (h : PulseBounds r a A b B ψ x) : 0 < lowerMassConstant a B

theorem NavierStokes.PulseCovariance.PulseBounds.mass_lower {r a A b B : ℝ} {ψ x : ℝ → ℝ} (h : PulseBounds r a A b B ψ x) : lowerMassConstant a B * r ≤ mass ψ x

theorem NavierStokes.PulseCovariance.PulseBounds.mass_pos {r a A b B : ℝ} {ψ x : ℝ → ℝ} (h : PulseBounds r a A b B ψ x) : 0 < mass ψ x

theorem NavierStokes.PulseCovariance.PulseBounds.cutoff_compact {r a A b B : ℝ} {ψ x : ℝ → ℝ} (h : PulseBounds r a A b B ψ x) : HasCompactSupport ψ

theorem NavierStokes.PulseCovariance.PulseBounds.weight_compact {r a A b B : ℝ} {ψ x : ℝ → ℝ} (h : PulseBounds r a A b B ψ x) : HasCompactSupport (weight ψ x)

theorem NavierStokes.PulseCovariance.PulseBounds.weight_direction_integrable {r a A b B : ℝ} {ψ x : ℝ → ℝ} (h : PulseBounds r a A b B ψ x) {q : ℝ → ℝ} (hq : ContinuousOn q (Set.Icc 0 (r ^ 2))) : MeasureTheory.Integrable (fun (v : ℝ) => weight ψ x v * q v) MeasureTheory.volume

theorem NavierStokes.PulseCovariance.PulseBounds.scalar_size_bounds {r a A b B : ℝ} {ψ x : ℝ → ℝ} (h : PulseBounds r a A b B ψ x) {ci clo chi : ℝ} (hclo : 0 < clo) (hchi : 0 < chi) (hci_lower : clo / r ^ 2 ≤ ci) (hci_upper : ci ≤ chi / r ^ 2) : 0 < ci * mass ψ x ∧ clo * lowerMassConstant a B / r ≤ ci * mass ψ x ∧ ci * mass ψ x ≤ chi * (A ^ 2 * √(Real.pi / (2 * b))) / r

The positive scalar prefactor has precisely the required reciprocal-square - root size when the column coefficient has reciprocal-slot-length size.

noncomputable def NavierStokes.PulseCovariance.averagedDirection (ψ x q : ℝ → ℝ) : ℝ

Averaged direction, given by (∫ v : ℝ, weight ψ x v * q v) / mass ψ x.

Equations

• NavierStokes.PulseCovariance.averagedDirection ψ x q = (∫ (v : ℝ), NavierStokes.PulseCovariance.weight ψ x v * q v) / NavierStokes.PulseCovariance.mass ψ x

noncomputable def NavierStokes.PulseCovariance.concentrationConstant (a A b B : ℝ) : ℝ

Concentration constant, given by A ^ 2 * firstGaussianMoment (2 * b) / PulseBounds.lowerMassConstant a B.

Equations

• NavierStokes.PulseCovariance.concentrationConstant a A b B = A ^ 2 * NavierStokes.PulseCovariance.firstGaussianMoment (2 * b) / NavierStokes.PulseCovariance.PulseBounds.lowerMassConstant a B

theorem NavierStokes.PulseCovariance.PulseBounds.concentrationConstant_nonneg {r a A b B : ℝ} {ψ x : ℝ → ℝ} (h : PulseBounds r a A b B ψ x) : 0 ≤ concentrationConstant a A b B

theorem NavierStokes.PulseCovariance.PulseBounds.normalized_moment_bound {r a A b B : ℝ} {ψ x : ℝ → ℝ} (h : PulseBounds r a A b B ψ x) : centeredMoment ψ x (r ^ 2 / 2) / mass ψ x ≤ concentrationConstant a A b B * r

theorem NavierStokes.PulseCovariance.PulseBounds.averagedDirection_sub {r a A b B : ℝ} {ψ x : ℝ → ℝ} (h : PulseBounds r a A b B ψ x) {q : ℝ → ℝ} (hq : ContinuousOn q (Set.Icc 0 (r ^ 2))) (q₀ : ℝ) : averagedDirection ψ x q - q₀ = (∫ (v : ℝ), weight ψ x v * (q v - q₀)) / mass ψ x

theorem NavierStokes.PulseCovariance.PulseBounds.averagedDirection_error {r a A b B : ℝ} {ψ x : ℝ → ℝ} (h : PulseBounds r a A b B ψ x) {q : ℝ → ℝ} (hq : ContinuousOn q (Set.Icc 0 (r ^ 2))) {q₀ ε K : ℝ} (hK : 0 ≤ K) (hqbound : ∀ v ∈ Set.Icc 0 (r ^ 2), |q v - q₀| ≤ ε + K * |v - r ^ 2 / 2| / r ^ 2) : |averagedDirection ψ x q - q₀| ≤ ε + K * concentrationConstant a A b B / r

A pointwise directional error plus a pointwise linear drift gives an actual integrated error. The moment bounds used below are derived above, not assumed.

theorem NavierStokes.PulseCovariance.PulseBounds.averagedDirection_error_order {r a A b B : ℝ} {ψ x : ℝ → ℝ} (h : PulseBounds r a A b B ψ x) {q : ℝ → ℝ} (hq : ContinuousOn q (Set.Icc 0 (r ^ 2))) {q₀ E K : ℝ} (hE : 0 ≤ E) (hK : 0 ≤ K) (hqbound : ∀ v ∈ Set.Icc 0 (r ^ 2), |q v - q₀| ≤ E / r ^ 2 + K * |v - r ^ 2 / 2| / r ^ 2) : |averagedDirection ψ x q - q₀| ≤ (E + K * concentrationConstant a A b B) / r

The ODE directional error E/L is smaller than the Gaussian concentration error 1/sqrt L.

@[reducible, inline]

abbrev NavierStokes.PulseCovariance.Vec2 : Type

Vec2: an abbreviation for SmoothCovariance.Vec2.

Equations

• NavierStokes.PulseCovariance.Vec2 = NavierStokes.SmoothCovariance.Vec2

@[reducible, inline]

abbrev NavierStokes.PulseCovariance.Mat2 : Type

Mat2: an abbreviation for SmoothCovariance.Mat2.

Equations

• NavierStokes.PulseCovariance.Mat2 = NavierStokes.SmoothCovariance.Mat2

noncomputable def NavierStokes.PulseCovariance.radiusProfile (s : ℝ) : ℝ

Radius profile, given by Real.sqrt (1 + s ^ 2).

Equations

• NavierStokes.PulseCovariance.radiusProfile s = √(1 + s ^ 2)

theorem NavierStokes.PulseCovariance.radiusProfile_pos (s : ℝ) : 0 < radiusProfile s

theorem NavierStokes.PulseCovariance.radiusProfile_sq (s : ℝ) : radiusProfile s ^ 2 = 1 + s ^ 2

theorem NavierStokes.PulseCovariance.abs_le_radiusProfile (s : ℝ) : |s| ≤ radiusProfile s

theorem NavierStokes.PulseCovariance.radiusProfile_lipschitz (s t : ℝ) : |radiusProfile s - radiusProfile t| ≤ |s - t|

The square-root profile used in the actual tangent model is globally one-Lipschitz; smoothness of a normalized direction is not assumed here.

noncomputable def NavierStokes.PulseCovariance.modelDirection (c₀ s : ℝ) : Vec2

Coordinates in the fixed tangent frame (N,K) of h N - s K, where h = c₀ sqrt(1+s²).

Equations

• NavierStokes.PulseCovariance.modelDirection c₀ s = ![c₀ * NavierStokes.PulseCovariance.radiusProfile s, -s]

theorem NavierStokes.PulseCovariance.modelDirection_lipschitz (c₀ s t : ℝ) (i : Fin 2) : |modelDirection c₀ s i - modelDirection c₀ t i| ≤ (|c₀| + 1) * |s - t|

noncomputable def NavierStokes.PulseCovariance.affineSlope (s₀ slope r v : ℝ) : ℝ

Affine slope, given by s₀ + slope * (v - r ^ 2 / 2) / r ^ 2.

Equations

• NavierStokes.PulseCovariance.affineSlope s₀ slope r v = s₀ + slope * (v - r ^ 2 / 2) / r ^ 2

theorem NavierStokes.PulseCovariance.affineSlope_midpoint (s₀ slope r : ℝ) : affineSlope s₀ slope r (r ^ 2 / 2) = s₀

theorem NavierStokes.PulseCovariance.hasDerivAt_affineSlope (s₀ slope r v : ℝ) : HasDerivAt (affineSlope s₀ slope r) (slope / r ^ 2) v

theorem NavierStokes.PulseCovariance.affineSlope_deriv_bound (s₀ slope r v : ℝ) {C : ℝ} (hC : |slope| ≤ C) : |deriv (affineSlope s₀ slope r) v| ≤ C / r ^ 2

theorem NavierStokes.PulseCovariance.affineSlope_distance (s₀ slope r v : ℝ) : |affineSlope s₀ slope r v - s₀| = |slope| * |v - r ^ 2 / 2| / r ^ 2

theorem NavierStokes.PulseCovariance.modelDirection_affine_drift (c₀ s₀ slope r v : ℝ) (i : Fin 2) : |modelDirection c₀ (affineSlope s₀ slope r v) i - modelDirection c₀ s₀ i| ≤ (|c₀| + 1) * |slope| * |v - r ^ 2 / 2| / r ^ 2

noncomputable def NavierStokes.PulseCovariance.actualColumn (ci : ℝ) (ψ x : ℝ → ℝ) (t : ℝ → Vec2) : Vec2

Actual column, defined pointwise by ci * ∫ v : ℝ, ψ v ^ 2 * x v * t v i.

Equations

• NavierStokes.PulseCovariance.actualColumn ci ψ x t i = ci * ∫ (v : ℝ), ψ v ^ 2 * x v * t v i

noncomputable def NavierStokes.PulseCovariance.normalizedColumn (ψ x : ℝ → ℝ) (t : ℝ → Vec2) : Vec2

Normalized column, defined pointwise by averagedDirection ψ x (fun v => t v i / x v).

Equations

• NavierStokes.PulseCovariance.normalizedColumn ψ x t i = NavierStokes.PulseCovariance.averagedDirection ψ x fun (v : ℝ) => t v i / x v

theorem NavierStokes.PulseCovariance.PulseBounds.raw_integrand_eq {r a A b B : ℝ} {ψ x : ℝ → ℝ} (h : PulseBounds r a A b B ψ x) {t : ℝ → Vec2} (v : ℝ) (i : Fin 2) : ψ v ^ 2 * x v * t v i = weight ψ x v * (t v i / x v)

theorem NavierStokes.PulseCovariance.PulseBounds.actualColumn_factorization {r a A b B : ℝ} {ψ x : ℝ → ℝ} (h : PulseBounds r a A b B ψ x) (ci : ℝ) (t : ℝ → Vec2) : actualColumn ci ψ x t = fun (i : Fin 2) => ci * mass ψ x * normalizedColumn ψ x t i

Exact factorization of the actual covariance integral into its positive mass and normalized direction.

theorem NavierStokes.PulseCovariance.PulseBounds.actualColumn_eq_intervalIntegral {r a A b B : ℝ} {ψ x : ℝ → ℝ} (h : PulseBounds r a A b B ψ x) (ci : ℝ) (t : ℝ → Vec2) (i : Fin 2) : actualColumn ci ψ x t i = ci * ∫ (v : ℝ) in 0..r ^ 2, ψ v ^ 2 * x v * t v i

theorem NavierStokes.PulseCovariance.PulseBounds.ratio_continuousOn {r a A b B : ℝ} {ψ x : ℝ → ℝ} (h : PulseBounds r a A b B ψ x) {t : ℝ → Vec2} (ht : ∀ (i : Fin 2), ContinuousOn (fun (v : ℝ) => t v i) (Set.Icc 0 (r ^ 2))) (i : Fin 2) : ContinuousOn (fun (v : ℝ) => t v i / x v) (Set.Icc 0 (r ^ 2))

theorem NavierStokes.PulseCovariance.PulseBounds.normalizedColumn_error {r a A b B : ℝ} {ψ x : ℝ → ℝ} (h : PulseBounds r a A b B ψ x) {t : ℝ → Vec2} (ht : ∀ (i : Fin 2), ContinuousOn (fun (v : ℝ) => t v i) (Set.Icc 0 (r ^ 2))) {E c₀ s₀ slope : ℝ} (hE : 0 ≤ E) (htmodel : ∀ v ∈ Set.Icc 0 (r ^ 2), ∀ (i : Fin 2), |t v i / x v - modelDirection c₀ (affineSlope s₀ slope r v) i| ≤ E / r ^ 2) (i : Fin 2) : |normalizedColumn ψ x t i - modelDirection c₀ s₀ i| ≤ (E + (|c₀| + 1) * |slope| * concentrationConstant a A b B) / r

Directional concentration for actual fundamental tangent components. The sole tangent estimate assumed is the pointwise ODE approximation to h(v)N-s(v)K, with affine s and the exact square-root profile h.

theorem NavierStokes.PulseCovariance.PulseBounds.normalizedColumn_error_of_outer_scale {r a A b B : ℝ} {ψ x : ℝ → ℝ} (h : PulseBounds r a A b B ψ x) {t : ℝ → Vec2} (ht : ∀ (i : Fin 2), ContinuousOn (fun (v : ℝ) => t v i) (Set.Icc 0 (r ^ 2))) {E S κ c₀ s₀ slope : ℝ} (hE : 0 ≤ E) (hS : 0 < S) (hκ : 0 ≤ κ) (hL : r ^ 2 ≤ κ * S) (htmodel : ∀ v ∈ Set.Icc 0 (r ^ 2), ∀ (i : Fin 2), |t v i / x v - modelDirection c₀ (affineSlope s₀ slope r v) i| ≤ E / S) (i : Fin 2) : |normalizedColumn ψ x t i - modelDirection c₀ s₀ i| ≤ (E * κ + (|c₀| + 1) * |slope| * concentrationConstant a A b B) / r

The ODE error may instead be supplied as E/S on a slot with L ≤ κ S. This converts it to the preceding concentration estimate.

structure NavierStokes.PulseCovariance.TangentPulse (r a A b B c₀ s₀ slope E : ℝ) : Type

A single actual pulse. Every estimate in this record is pointwise; neither its covariance integral nor its average direction is assumed.

• cutoff : ℝ → ℝ

  Cutoff of TangentPulse, of type ℝ → ℝ.

• component : ℝ → ℝ

  Component of TangentPulse, of type ℝ → ℝ.

• tangent : ℝ → Vec2

  Tangent of TangentPulse, of type ℝ → Vec2.

• bounds : PulseBounds r a A b B self.cutoff self.component
• tangent_continuous (i : Fin 2) : ContinuousOn (fun (v : ℝ) => self.tangent v i) (Set.Icc 0 (r ^ 2))
• tangent_model (v : ℝ) : v ∈ Set.Icc 0 (r ^ 2) → ∀ (i : Fin 2), |self.tangent v i / self.component v - modelDirection c₀ (affineSlope s₀ slope r v) i| ≤ E / r ^ 2

noncomputable def NavierStokes.PulseCovariance.signedSlopes (u : ℝ) : Vec2

Signed slopes, given by ![u, -u].

Equations

• NavierStokes.PulseCovariance.signedSlopes u = ![u, -u]

noncomputable def NavierStokes.PulseCovariance.signedModel (c₀ u : ℝ) : Mat2

Signed model, defined pointwise by modelDirection c₀ (signedSlopes u j) i.

Equations

• NavierStokes.PulseCovariance.signedModel c₀ u i j = NavierStokes.PulseCovariance.modelDirection c₀ (NavierStokes.PulseCovariance.signedSlopes u j) i

theorem NavierStokes.PulseCovariance.signedModel_eq_covariance (c₀ u : ℝ) : signedModel c₀ u = Covariance.signedMatrix (Covariance.normalMagnitude c₀ u) u 1 1

theorem NavierStokes.PulseCovariance.signedModel_strictCone {c₀ u m t : ℝ} (hc₀ : c₀ < 0) (hu : 0 < u) (hcone : |Covariance.normalMagnitude c₀ u * t| < u * m) : SmoothCovariance.StrictCone (signedModel c₀ u) (Covariance.target m t)

theorem NavierStokes.PulseCovariance.signedModel_continuousOn {X : Type u_1} [TopologicalSpace X] {K : Set X} {c₀ u : X → ℝ} (hc₀ : ContinuousOn c₀ K) (hu : ContinuousOn u K) (i j : Fin 2) : ContinuousOn (fun (p : X) => signedModel (c₀ p) (u p) i j) K

@[reducible, inline]

abbrev NavierStokes.PulseCovariance.SignedPulsePair (r a A b B c₀ u E : ℝ) : Type

Signed pulse pair: an abbreviation for (j : Fin 2) → TangentPulse r a A b B c₀ (signedSlopes u j) (signedSlopes u j) E.

Equations

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

noncomputable def NavierStokes.PulseCovariance.actualMatrix {r a A b B c₀ u E : ℝ} (pulses : SignedPulsePair r a A b B c₀ u E) (ci : Vec2) : Mat2

Actual matrix, defined pointwise by actualColumn (ci j) (pulses j).cutoff (pulses j).component (pulses j).tangent i.

Equations

• NavierStokes.PulseCovariance.actualMatrix pulses ci i j = NavierStokes.PulseCovariance.actualColumn (ci j) (pulses j).cutoff (pulses j).component (pulses j).tangent i

noncomputable def NavierStokes.PulseCovariance.normalizedMatrix {r a A b B c₀ u E : ℝ} (pulses : SignedPulsePair r a A b B c₀ u E) : Mat2

Normalized matrix, defined pointwise by normalizedColumn (pulses j).cutoff (pulses j).component (pulses j).tangent i.

Equations

• NavierStokes.PulseCovariance.normalizedMatrix pulses i j = NavierStokes.PulseCovariance.normalizedColumn (pulses j).cutoff (pulses j).component (pulses j).tangent i

noncomputable def NavierStokes.PulseCovariance.columnScales {r a A b B c₀ u E : ℝ} (pulses : SignedPulsePair r a A b B c₀ u E) (ci : Vec2) : Vec2

Column scales, defined pointwise by ci j * mass (pulses j).cutoff (pulses j).component.

Equations

• NavierStokes.PulseCovariance.columnScales pulses ci j = ci j * NavierStokes.PulseCovariance.mass (pulses j).cutoff (pulses j).component

theorem NavierStokes.PulseCovariance.signedSlopes_abs (u : ℝ) (j : Fin 2) : |signedSlopes u j| = |u|

theorem NavierStokes.PulseCovariance.actualMatrix_factorization {r a A b B c₀ u E : ℝ} (pulses : SignedPulsePair r a A b B c₀ u E) (ci : Vec2) : actualMatrix pulses ci = FlatCovariance.columns (normalizedMatrix pulses) (columnScales pulses ci)

theorem NavierStokes.PulseCovariance.columnScales_pos {r a A b B c₀ u E : ℝ} (pulses : SignedPulsePair r a A b B c₀ u E) {ci : Vec2} (hci : ∀ (j : Fin 2), 0 < ci j) (j : Fin 2) : 0 < columnScales pulses ci j

theorem NavierStokes.PulseCovariance.normalizedMatrix_entry_error {r a A b B c₀ u E : ℝ} (pulses : SignedPulsePair r a A b B c₀ u E) (hE : 0 ≤ E) (i j : Fin 2) : |normalizedMatrix pulses i j - signedModel c₀ u i j| ≤ (E + (|c₀| + 1) * |u| * concentrationConstant a A b B) / r

theorem NavierStokes.PulseCovariance.actualMatrix_positive_of_normalized {r a A b B c₀ u E : ℝ} (pulses : SignedPulsePair r a A b B c₀ u E) {ci : Vec2} (hci : ∀ (j : Fin 2), 0 < ci j) (T : Vec2) (hdet : Matrix.det (normalizedMatrix pulses) ≠ 0) (hw : ∀ (i : Fin 2), 0 < SmoothCovariance.weights (normalizedMatrix pulses) T i) : Matrix.det (actualMatrix pulses ci) ≠ 0 ∧ (∀ (i : Fin 2), 0 < SmoothCovariance.weights (actualMatrix pulses ci) T i) ∧ ∀ (i : Fin 2), 0 < SmoothCovariance.amplitudes (actualMatrix pulses ci) T i

@[instance_reducible]

def NavierStokes.PulseCovariance.instPulseCovariance1 : NormedAddCommGroup Mat2

Cache the standard NormedAddCommGroup Mat2 instance to shorten typeclass synthesis.

Equations

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

@[instance_reducible]

noncomputable def NavierStokes.PulseCovariance.instPulseCovariance2 : NormedSpace ℝ Mat2

Cache the standard NormedSpace ℝ Mat2 instance to shorten typeclass synthesis.

Equations

• NavierStokes.PulseCovariance.instPulseCovariance2 = { toModule := Matrix.module, norm_smul_le := NavierStokes.PulseCovariance.instPulseCovariance2._proof_1 }

theorem NavierStokes.PulseCovariance.compact_actual_positive_inverse {X : Type u_1} [TopologicalSpace X] {K : Set X} (hK : IsCompact K) {c₀ u : X → ℝ} {T : X → Vec2} (hmodel : ∀ (i j : Fin 2), ContinuousOn (fun (p : X) => signedModel (c₀ p) (u p) i j) K) (hT : ∀ (i : Fin 2), ContinuousOn (fun (p : X) => T p i) K) (hcone : ∀ p ∈ K, SmoothCovariance.StrictCone (signedModel (c₀ p) (u p)) (T p)) {a A b B E C U : ℝ} (hE : 0 ≤ E) (hC : 0 ≤ C) (hU : 0 ≤ U) (hc₀ : ∀ p ∈ K, |c₀ p| ≤ C) (hu : ∀ p ∈ K, |u p| ≤ U) : ∃ (R : ℝ), 1 ≤ R ∧ ∀ p ∈ K, ∀ (r : ℝ), R ≤ r → ∀ (pulses : SignedPulsePair r a A b B (c₀ p) (u p) E) (ci : Vec2), (∀ (j : Fin 2), 0 < ci j) → Matrix.det (actualMatrix pulses ci) ≠ 0 ∧ (∀ (i : Fin 2), 0 < SmoothCovariance.weights (actualMatrix pulses ci) (T p) i) ∧ ∀ (i : Fin 2), 0 < SmoothCovariance.amplitudes (actualMatrix pulses ci) (T p) i

A uniform slot threshold for the actual signed pulse pair over a compact strict-cone family. Its matrix approximation is a conclusion of the Gaussian moment and pointwise tangent estimates in TangentPulse, not a hypothesis.

theorem NavierStokes.PulseCovariance.compact_actual_positive_inverse_of_scalar_cone {X : Type u_1} [TopologicalSpace X] {K : Set X} (hK : IsCompact K) {c₀ u m t : X → ℝ} (hc₀ : ContinuousOn c₀ K) (hu : ContinuousOn u K) (hm : ContinuousOn m K) (ht : ContinuousOn t K) (hc₀neg : ∀ p ∈ K, c₀ p < 0) (hupos : ∀ p ∈ K, 0 < u p) (hcone : ∀ p ∈ K, |Covariance.normalMagnitude (c₀ p) (u p) * t p| < u p * m p) {a A b B E : ℝ} (hE : 0 ≤ E) : ∃ (R : ℝ), 1 ≤ R ∧ ∀ p ∈ K, ∀ (r : ℝ), R ≤ r → ∀ (pulses : SignedPulsePair r a A b B (c₀ p) (u p) E) (ci : Vec2), (∀ (j : Fin 2), 0 < ci j) → Matrix.det (actualMatrix pulses ci) ≠ 0 ∧ (∀ (i : Fin 2), 0 < SmoothCovariance.weights (actualMatrix pulses ci) (Covariance.target (m p) (t p)) i) ∧ ∀ (i : Fin 2), 0 < SmoothCovariance.amplitudes (actualMatrix pulses ci) (Covariance.target (m p) (t p)) i

Scalar cone inequalities and continuity of the four scalar model data suffice. Compactness supplies both the uniform cone tolerance and the uniform bounds on c₀,u, hence one slot threshold for every actual pulse pair.

theorem NavierStokes.TorusAverages.instTorusAverages1 : Fact (0 < 1)

theorem NavierStokes.TorusAverages.instTorusAverages2 : TorusInverse.torusMeasure.IsAddHaarMeasure

theorem NavierStokes.TorusAverages.planeVolumeHaar : MeasureTheory.volume.IsAddHaarMeasure

noncomputable def NavierStokes.TorusAverages.quotientPoint (z : TorusInverse.Plane) : TorusInverse.Torus

Quotient point, given by ((z.1 : UnitAddCircle), (z.2 : UnitAddCircle)).

Equations

• NavierStokes.TorusAverages.quotientPoint z = (↑z.1, ↑z.2)

noncomputable def NavierStokes.TorusAverages.covering (z : TorusInverse.Plane) : TorusInverse.Plane

The manuscript's real covering matrix [[3,1],[1,5]].

Equations

• NavierStokes.TorusAverages.covering z = (3 * z.1 + z.2, z.1 + 5 * z.2)

noncomputable def NavierStokes.TorusAverages.torusCovering : TorusInverse.Torus →+ TorusInverse.Torus

Torus covering, bundling toFun, map_zero, map_add.

Equations

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

theorem NavierStokes.TorusAverages.torusCovering_continuous : Continuous ⇑torusCovering

theorem NavierStokes.TorusAverages.quotient_covering (z : TorusInverse.Plane) : quotientPoint (covering z) = torusCovering (quotientPoint z)

theorem NavierStokes.TorusAverages.torusCovering_surjective : Function.Surjective ⇑torusCovering

Surjectivity is explicit: choose real lifts and apply the inverse matrix (1/14)[[5,-1],[-1,3]] before projecting to the torus.

theorem NavierStokes.TorusAverages.torusCovering_measurePreserving : MeasureTheory.MeasurePreserving (⇑torusCovering) TorusInverse.torusMeasure TorusInverse.torusMeasure

theorem NavierStokes.TorusAverages.quotient_covering_iterate (n : ℕ) (z : TorusInverse.Plane) : quotientPoint (covering^[n] z) = (⇑torusCovering)^[n] (quotientPoint z)

theorem NavierStokes.TorusAverages.covering_continuous : Continuous covering

theorem NavierStokes.TorusAverages.integral_torusCovering_iterate {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : TorusInverse.Torus → V) (hf : Continuous f) (n : ℕ) : ∫ (z : TorusInverse.Torus), f ((⇑torusCovering)^[n] z) ∂TorusInverse.torusMeasure = ∫ (z : TorusInverse.Torus), f z ∂TorusInverse.torusMeasure

Every covering power preserves the actual Haar integral. Continuity is already sufficient; no Fourier-decay premise or assumed average identity occurs.

noncomputable def NavierStokes.TorusAverages.squareAverage {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : TorusInverse.Plane → V) : V

Square average, given by ∫ y in (0 : ℝ)..1, ∫ x in (0 : ℝ)..1, f (x, y).

Equations

• NavierStokes.TorusAverages.squareAverage f = ∫ (y : ℝ) (x : ℝ) in 0..1, f (x, y)

theorem NavierStokes.TorusAverages.squareAverage_torusLift (f : C(TorusInverse.Torus, ℂ)) : squareAverage (SmoothFourierData.torusLift ⇑f) = ∫ (z : TorusInverse.Torus), f z ∂TorusInverse.torusMeasure

theorem NavierStokes.TorusAverages.squareAverage_covering_iterate {f : TorusInverse.Plane → ℂ} (hf : Continuous f) (hp : SmoothFourierData.UnitPeriodic f) (n : ℕ) : (squareAverage fun (z : TorusInverse.Plane) => f (covering^[n] z)) = squareAverage f

Unit-square version for a genuine continuous unit-periodic complex field.

theorem NavierStokes.TorusAverages.squareAverage_covering_iterate_smooth {f : TorusInverse.Plane → ℂ} (hf : ContDiff ℝ (↑⊤) f) (hp : SmoothFourierData.UnitPeriodic f) (n : ℕ) : (squareAverage fun (z : TorusInverse.Plane) => f (covering^[n] z)) = squareAverage f

theorem NavierStokes.TorusAverages.squareAverage_covering_iterate_real {f : TorusInverse.Plane → ℝ} (hf : Continuous f) (hp : ∀ (z : TorusInverse.Plane) (k : TorusInverse.Frequency), f (z + (↑k.1, ↑k.2)) = f z) (n : ℕ) : (squareAverage fun (z : TorusInverse.Plane) => f (covering^[n] z)) = squareAverage f

Real-valued form, with the same actual unit-square integral.

Lattice periodization and its actual integral

noncomputable def NavierStokes.TorusAverages.latticePoint (k : TorusInverse.Frequency) : TorusInverse.Plane

Lattice point, given by ((k.1 : ℝ), (k.2 : ℝ)).

Equations

• NavierStokes.TorusAverages.latticePoint k = (↑k.1, ↑k.2)

theorem NavierStokes.TorusAverages.latticePoint_add (k l : TorusInverse.Frequency) : latticePoint (k + l) = latticePoint k + latticePoint l

theorem NavierStokes.TorusAverages.latticePoint_injective : Function.Injective latticePoint

theorem NavierStokes.TorusAverages.quotientPoint_lattice_add (k : TorusInverse.Frequency) (z : TorusInverse.Plane) : quotientPoint (latticePoint k + z) = quotientPoint z

theorem NavierStokes.TorusAverages.quotientPoint_injOn_square (a : TorusInverse.Plane) : Set.InjOn quotientPoint (Set.Ico a.1 (a.1 + 1) ×ˢ Set.Ico a.2 (a.2 + 1))

Each translated half-open unit square is an injective coordinate chart for the quotient to the torus.

theorem NavierStokes.TorusAverages.quotientPoint_injOn_small_chart (L : TorusInverse.Plane ≃L[ℝ] TorusInverse.Plane) (center : TorusInverse.Plane) (r : ℝ) (hr : ‖↑L‖ * r < 1 / 2) : Set.InjOn quotientPoint ((fun (z : TorusInverse.Plane) => center + L z) '' Metric.ball 0 r)

A concrete smallness criterion for the native parallelogram. The product norm on Plane is the maximum norm, so ball 0 r is the open native square.

theorem NavierStokes.TorusAverages.exists_injective_native_radius (L : TorusInverse.Plane ≃L[ℝ] TorusInverse.Plane) (center : TorusInverse.Plane) : ∃ (r : ℝ), 0 < r ∧ Set.InjOn quotientPoint ((fun (z : TorusInverse.Plane) => center + L z) '' Metric.ball 0 r)

A positive injective native radius always exists; this proof supplies the explicit radius 1 / (4 * (‖L‖ + 1)).

theorem NavierStokes.TorusAverages.latticeTranslate_unique {s : Set TorusInverse.Plane} (hs : Set.InjOn quotientPoint s) {z : TorusInverse.Plane} {k l : TorusInverse.Frequency} (hk : latticePoint k + z ∈ s) (hl : latticePoint l + z ∈ s) : k = l

@[instance_reducible]

noncomputable def NavierStokes.TorusAverages.latticeAddAction : AddAction TorusInverse.Frequency TorusInverse.Plane

The AddAction Frequency Plane structure used in torus averages.

Equations

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

theorem NavierStokes.TorusAverages.instTorusAverages3 : MeasurableVAdd TorusInverse.Frequency TorusInverse.Plane

theorem NavierStokes.TorusAverages.instTorusAverages4 : MeasureTheory.VAddInvariantMeasure TorusInverse.Frequency TorusInverse.Plane MeasureTheory.volume

noncomputable def NavierStokes.TorusAverages.fundamentalSquare : Set TorusInverse.Plane

Fundamental square, given by Ico (0 : ℝ) 1 ×ˢ Ico (0 : ℝ) 1.

Equations

• NavierStokes.TorusAverages.fundamentalSquare = Set.Ico 0 1 ×ˢ Set.Ico 0 1

theorem NavierStokes.TorusAverages.fundamentalSquare_isAddFundamentalDomain : MeasureTheory.IsAddFundamentalDomain TorusInverse.Frequency fundamentalSquare MeasureTheory.volume

The half-open unit square is proved to tile the plane, using integer floors.

noncomputable def NavierStokes.TorusAverages.periodize {V : Type u_1} [NormedAddCommGroup V] (f : TorusInverse.Plane → V) (z : TorusInverse.Plane) : V

The periodization is the actual sum over integer translates.

Equations

• NavierStokes.TorusAverages.periodize f z = ∑' (k : NavierStokes.TorusInverse.Frequency), f (NavierStokes.TorusAverages.latticePoint k + z)

theorem NavierStokes.TorusAverages.finite_translates_on_ball {V : Type u_1} [Zero V] {f : TorusInverse.Plane → V} (hf : HasCompactSupport f) (R : ℝ) : ∃ (s : Finset TorusInverse.Frequency), ∀ (z : TorusInverse.Plane), ‖z‖ ≤ R → ∀ k ∉ s, f (latticePoint k + z) = 0

A compactly supported field has only finitely many active translates on every bounded set. This supplies an actual local finite-sum formula.

theorem NavierStokes.TorusAverages.periodize_eventually_eq_sum {V : Type u_1} [NormedAddCommGroup V] {f : TorusInverse.Plane → V} (hf : HasCompactSupport f) (z : TorusInverse.Plane) : ∃ (s : Finset TorusInverse.Frequency), periodize f =ᶠ[nhds z] fun (w : TorusInverse.Plane) => ∑ k ∈ s, f (latticePoint k + w)

theorem NavierStokes.TorusAverages.periodize_continuous {V : Type u_1} [NormedAddCommGroup V] {f : TorusInverse.Plane → V} (hf : Continuous f) (hcf : HasCompactSupport f) : Continuous (periodize f)

theorem NavierStokes.TorusAverages.periodize_contDiff {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : TorusInverse.Plane → V} (hf : ContDiff ℝ (↑⊤) f) (hcf : HasCompactSupport f) : ContDiff ℝ (↑⊤) (periodize f)

theorem NavierStokes.TorusAverages.periodize_periodic {V : Type u_1} [NormedAddCommGroup V] (f : TorusInverse.Plane → V) (z : TorusInverse.Plane) (k : TorusInverse.Frequency) : periodize f (z + latticePoint k) = periodize f z

theorem NavierStokes.TorusAverages.periodize_eq_native_copy {V : Type u_1} [NormedAddCommGroup V] {s : Set TorusInverse.Plane} (hs : Set.InjOn quotientPoint s) {f : TorusInverse.Plane → V} (hf : Function.support f ⊆ s) {z : TorusInverse.Plane} {k : TorusInverse.Frequency} (hk : latticePoint k + z ∈ s) : periodize f z = f (latticePoint k + z)

On an injective slot, a periodization equals the one native copy present there. The result includes the case that the native value itself is zero.

theorem NavierStokes.TorusAverages.periodize_mul_of_injective_support {s : Set TorusInverse.Plane} (hs : Set.InjOn quotientPoint s) {f g : TorusInverse.Plane → ℝ} (hf : Function.support f ⊆ s) (hg : Function.support g ⊆ s) (z : TorusInverse.Plane) : periodize f z * periodize g z = periodize (fun (w : TorusInverse.Plane) => f w * g w) z

Products of actual periodized fields have no cross-copy terms when both native fields are supported in the same injective slot.

theorem NavierStokes.TorusAverages.squareAverage_eq_setIntegral {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : TorusInverse.Plane → V} (hf : Continuous f) : squareAverage f = ∫ (z : TorusInverse.Plane) in fundamentalSquare, f z

The set-integral and iterated-integral descriptions of the unit-square average agree. Endpoint choices have zero Lebesgue measure.

theorem NavierStokes.TorusAverages.integral_periodize {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : TorusInverse.Plane → V} (hf : MeasureTheory.Integrable f MeasureTheory.volume) : ∫ (z : TorusInverse.Plane) in fundamentalSquare, periodize f z = ∫ (z : TorusInverse.Plane), f z

Every integrable field, in particular a smooth compactly supported slot, has exactly its plane integral as the integral of its lattice periodization.

theorem NavierStokes.TorusAverages.squareAverage_periodize {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : TorusInverse.Plane → V} (hf : Continuous f) (hcf : HasCompactSupport f) : squareAverage (periodize f) = ∫ (z : TorusInverse.Plane), f z

theorem NavierStokes.TorusAverages.squareAverage_periodize_covering {f : TorusInverse.Plane → ℂ} (hf : Continuous f) (hcf : HasCompactSupport f) (n : ℕ) : (squareAverage fun (z : TorusInverse.Plane) => periodize f (covering^[n] z)) = ∫ (z : TorusInverse.Plane), f z

theorem NavierStokes.TorusAverages.squareAverage_periodize_covering_real {f : TorusInverse.Plane → ℝ} (hf : Continuous f) (hcf : HasCompactSupport f) (n : ℕ) : (squareAverage fun (z : TorusInverse.Plane) => periodize f (covering^[n] z)) = ∫ (z : TorusInverse.Plane), f z

Native coordinates and the determinant prefactor

noncomputable def NavierStokes.TorusAverages.nativeField {V : Type u_1} (L : TorusInverse.Plane ≃L[ℝ] TorusInverse.Plane) (center : TorusInverse.Plane) (f : TorusInverse.Plane → V) (z : TorusInverse.Plane) : V

A native field placed at center in the linear coordinate chart L.

Equations

• NavierStokes.TorusAverages.nativeField L center f z = f (L.symm (z - center))

theorem NavierStokes.TorusAverages.nativeField_continuous {V : Type u_1} [TopologicalSpace V] (L : TorusInverse.Plane ≃L[ℝ] TorusInverse.Plane) (center : TorusInverse.Plane) {f : TorusInverse.Plane → V} (hf : Continuous f) : Continuous (nativeField L center f)

theorem NavierStokes.TorusAverages.nativeField_contDiff {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (L : TorusInverse.Plane ≃L[ℝ] TorusInverse.Plane) (center : TorusInverse.Plane) {f : TorusInverse.Plane → V} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (nativeField L center f)

theorem NavierStokes.TorusAverages.nativeField_hasCompactSupport {V : Type u_1} [Zero V] (L : TorusInverse.Plane ≃L[ℝ] TorusInverse.Plane) (center : TorusInverse.Plane) {f : TorusInverse.Plane → V} (hf : HasCompactSupport f) : HasCompactSupport (nativeField L center f)

theorem NavierStokes.TorusAverages.integral_nativeField {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (L : TorusInverse.Plane ≃L[ℝ] TorusInverse.Plane) (center : TorusInverse.Plane) (f : TorusInverse.Plane → V) : ∫ (z : TorusInverse.Plane), nativeField L center f z = |LinearMap.det ↑↑L| • ∫ (z : TorusInverse.Plane), f z

Actual linear change of variables, including the absolute determinant.

theorem NavierStokes.TorusAverages.integral_periodize_nativeField {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (L : TorusInverse.Plane ≃L[ℝ] TorusInverse.Plane) (center : TorusInverse.Plane) {f : TorusInverse.Plane → V} (hf : Continuous f) (hcf : HasCompactSupport f) : ∫ (z : TorusInverse.Plane) in fundamentalSquare, periodize (nativeField L center f) z = |LinearMap.det ↑↑L| • ∫ (z : TorusInverse.Plane), f z

The native compact-slot average is obtained from periodization and a Jacobian theorem, with no assumed averaging identity.

noncomputable def NavierStokes.TorusAverages.slotLinearMap (vr vt : TorusInverse.Plane) : TorusInverse.Plane →ₗ[ℝ] TorusInverse.Plane

The linear map with the radial and longitudinal vectors as its columns.

Equations

• NavierStokes.TorusAverages.slotLinearMap vr vt = (Matrix.toLin (Module.Basis.finTwoProd ℝ) (Module.Basis.finTwoProd ℝ)) !![vr.1, vt.1; vr.2, vt.2]

theorem NavierStokes.TorusAverages.slotLinearMap_apply (vr vt z : TorusInverse.Plane) : (slotLinearMap vr vt) z = z.1 • vr + z.2 • vt

theorem NavierStokes.TorusAverages.det_slotLinearMap (vr vt : TorusInverse.Plane) : LinearMap.det (slotLinearMap vr vt) = vr.1 * vt.2 - vr.2 * vt.1

noncomputable def NavierStokes.TorusAverages.slotChart (vr vt : TorusInverse.Plane) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) : TorusInverse.Plane ≃L[ℝ] TorusInverse.Plane

The genuine nondegenerate native chart.

Equations

• NavierStokes.TorusAverages.slotChart vr vt hdet = ((NavierStokes.TorusAverages.slotLinearMap vr vt).equivOfDetNeZero ⋯).toContinuousLinearEquiv

theorem NavierStokes.TorusAverages.slotChart_apply (vr vt : TorusInverse.Plane) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (z : TorusInverse.Plane) : (slotChart vr vt hdet) z = z.1 • vr + z.2 • vt

theorem NavierStokes.TorusAverages.det_slotChart (vr vt : TorusInverse.Plane) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) : LinearMap.det ↑↑(slotChart vr vt hdet) = vr.1 * vt.2 - vr.2 * vt.1

theorem NavierStokes.TorusAverages.integral_periodize_slot {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (vr vt center : TorusInverse.Plane) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) {f : TorusInverse.Plane → V} (hf : Continuous f) (hcf : HasCompactSupport f) : ∫ (z : TorusInverse.Plane) in fundamentalSquare, periodize (nativeField (slotChart vr vt hdet) center f) z = |vr.1 * vt.2 - vr.2 * vt.1| • ∫ (z : TorusInverse.Plane), f z

noncomputable def NavierStokes.TorusAverages.transverseChart (ci : ℝ) (hci : ci ≠ 0) : TorusInverse.Plane ≃L[ℝ] TorusInverse.Plane

Rescaling the transverse coordinate by ci.

Equations

• NavierStokes.TorusAverages.transverseChart ci hci = NavierStokes.TorusAverages.slotChart (1, 0) (0, ci) ⋯

theorem NavierStokes.TorusAverages.transverseChart_apply (ci : ℝ) (hci : ci ≠ 0) (z : TorusInverse.Plane) : (transverseChart ci hci) z = (z.1, ci * z.2)

theorem NavierStokes.TorusAverages.transverseChart_symm_apply (ci : ℝ) (hci : ci ≠ 0) (z : TorusInverse.Plane) : (transverseChart ci hci).symm z = (z.1, z.2 / ci)

theorem NavierStokes.TorusAverages.det_transverseChart (ci : ℝ) (hci : ci ≠ 0) : LinearMap.det ↑↑(transverseChart ci hci) = ci

noncomputable def NavierStokes.TorusAverages.transverseStretch {V : Type u_1} (ci r0 : ℝ) (f : TorusInverse.Plane → V) (z : TorusInverse.Plane) : V

η = ci * v - r0, written as the field in the native (ξ,η) coordinates.

Equations

• NavierStokes.TorusAverages.transverseStretch ci r0 f z = f (z.1, (z.2 + r0) / ci)

theorem NavierStokes.TorusAverages.transverseStretch_eq_nativeField {V : Type u_1} (ci r0 : ℝ) (hci : ci ≠ 0) (f : TorusInverse.Plane → V) : transverseStretch ci r0 f = nativeField (transverseChart ci hci) (0, -r0) f

theorem NavierStokes.TorusAverages.transverseStretch_continuous {V : Type u_1} [TopologicalSpace V] (ci r0 : ℝ) (hci : ci ≠ 0) {f : TorusInverse.Plane → V} (hf : Continuous f) : Continuous (transverseStretch ci r0 f)

theorem NavierStokes.TorusAverages.transverseStretch_contDiff {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (ci r0 : ℝ) (hci : ci ≠ 0) {f : TorusInverse.Plane → V} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (transverseStretch ci r0 f)

theorem NavierStokes.TorusAverages.transverseStretch_hasCompactSupport {V : Type u_1} [Zero V] (ci r0 : ℝ) (hci : ci ≠ 0) {f : TorusInverse.Plane → V} (hf : HasCompactSupport f) : HasCompactSupport (transverseStretch ci r0 f)

theorem NavierStokes.TorusAverages.integral_transverseStretch {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (ci r0 : ℝ) (hci : ci ≠ 0) (f : TorusInverse.Plane → V) : ∫ (z : TorusInverse.Plane), transverseStretch ci r0 f z = |ci| • ∫ (z : TorusInverse.Plane), f z

theorem NavierStokes.TorusAverages.squareAverage_covered_nativeSlot (vr vt center : TorusInverse.Plane) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (ci r0 : ℝ) (hci : 0 < ci) {f : TorusInverse.Plane → ℝ} (hf : Continuous f) (hcf : HasCompactSupport f) (n : ℕ) : (squareAverage fun (z : TorusInverse.Plane) => periodize (nativeField (slotChart vr vt hdet) center (transverseStretch ci r0 f)) (covering^[n] z)) = |vr.1 * vt.2 - vr.2 * vt.1| * ci * ∫ (z : TorusInverse.Plane), f z

The actual native-slot average after every integer covering power. The transverse-coordinate Jacobian is positive ci, not an assumed model scale.

theorem NavierStokes.TorusAverages.productProfile_hasCompactSupport {a b : ℝ → ℝ} (ha : HasCompactSupport a) (hb : HasCompactSupport b) : HasCompactSupport fun (z : TorusInverse.Plane) => a z.1 * b z.2

theorem NavierStokes.TorusAverages.squareAverage_covered_product (vr vt center : TorusInverse.Plane) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (ci r0 : ℝ) (hci : 0 < ci) {a b : ℝ → ℝ} (ha : Continuous a) (hb : Continuous b) (hca : HasCompactSupport a) (hcb : HasCompactSupport b) (n : ℕ) : (squareAverage fun (z : TorusInverse.Plane) => periodize (nativeField (slotChart vr vt hdet) center (transverseStretch ci r0 fun (w : TorusInverse.Plane) => a w.1 * b w.2)) (covering^[n] z)) = (|vr.1 * vt.2 - vr.2 * vt.1| * ∫ (ξ : ℝ), a ξ) * (ci * ∫ (v : ℝ), b v)

Separation of the actual longitudinal and transverse integrals.

noncomputable def NavierStokes.TorusAverages.pulseProfile (χ ψ x : ℝ → ℝ) (t : ℝ → PulseCovariance.Vec2) (i : Fin 2) (z : TorusInverse.Plane) : ℝ

The native covariance coefficient before angular averaging.

Equations

• NavierStokes.TorusAverages.pulseProfile χ ψ x t i z = χ z.1 ^ 2 * (ψ z.2 ^ 2 * x z.2 * t z.2 i)

theorem NavierStokes.TorusAverages.squareAverage_covered_pulseColumn (vr vt center : TorusInverse.Plane) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (ci r0 : ℝ) (hci : 0 < ci) {χ ψ x : ℝ → ℝ} {t : ℝ → PulseCovariance.Vec2} (hχ : Continuous χ) (hψ : Continuous ψ) (hx : Continuous x) (ht : Continuous t) (hcχ : HasCompactSupport χ) (hcψ : HasCompactSupport ψ) (i : Fin 2) (n : ℕ) : (squareAverage fun (z : TorusInverse.Plane) => periodize (nativeField (slotChart vr vt hdet) center (transverseStretch ci r0 (pulseProfile χ ψ x t i))) (covering^[n] z)) = (|vr.1 * vt.2 - vr.2 * vt.1| * ∫ (ξ : ℝ), χ ξ ^ 2) * PulseCovariance.actualColumn ci ψ x t i

The real-cosine factor in Lemma 8.7

theorem NavierStokes.TorusAverages.angularMean_cos_sq_harmonic (j : ℤ) (hj : j ≠ 0) (phase : ℝ) : (SmoothLoop.angularMean fun (θ : ℝ) => Real.cos (↑j * θ + phase) ^ 2) = 1 / 2

An arbitrary phase shift does not change the average of a nonzero integer angular harmonic squared.

theorem NavierStokes.TorusAverages.squareAverage_const_mul (c : ℝ) (f : TorusInverse.Plane → ℝ) : (squareAverage fun (z : TorusInverse.Plane) => c * f z) = c * squareAverage f

theorem NavierStokes.TorusAverages.angular_cosine_covariance (a phase : TorusInverse.Plane → ℝ) (j : ℤ) (hj : j ≠ 0) : (squareAverage fun (z : TorusInverse.Plane) => SmoothLoop.angularMean fun (θ : ℝ) => a z * Real.cos (↑j * θ + phase z) ^ 2) = 1 / 2 * squareAverage a

theorem NavierStokes.TorusAverages.primary_covariance_average (vr vt center : TorusInverse.Plane) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (ci r0 : ℝ) (hci : 0 < ci) {χ ψ x : ℝ → ℝ} {t : ℝ → PulseCovariance.Vec2} (hχ : Continuous χ) (hψ : Continuous ψ) (hx : Continuous x) (ht : Continuous t) (hcχ : HasCompactSupport χ) (hcψ : HasCompactSupport ψ) (i : Fin 2) (n : ℕ) (phase : TorusInverse.Plane → ℝ) (j : ℤ) (hj : j ≠ 0) : have a := fun (z : TorusInverse.Plane) => periodize (nativeField (slotChart vr vt hdet) center (transverseStretch ci r0 (pulseProfile χ ψ x t i))) (covering^[n] z); (squareAverage fun (z : TorusInverse.Plane) => SmoothLoop.angularMean fun (θ : ℝ) => a z * Real.cos (↑j * θ + phase z) ^ 2) = (|vr.1 * vt.2 - vr.2 * vt.1| / 2 * ∫ (ξ : ℝ), χ ξ ^ 2) * PulseCovariance.actualColumn ci ψ x t i

The displayed native prefactor in Lemma 8.7, for actual periodized slot coefficients and actual angular averages. The harmonic is the rounded integer k*p, so its only required property here is nonzero integrality.

theorem NavierStokes.TorusAverages.primary_covariance_average_interval (vr vt center : TorusInverse.Plane) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (ci r0 : ℝ) (hci : 0 < ci) {r a A b B : ℝ} {χ ψ x : ℝ → ℝ} {t : ℝ → PulseCovariance.Vec2} (hp : PulseCovariance.PulseBounds r a A b B ψ x) (hχ : Continuous χ) (ht : Continuous t) (hcχ : HasCompactSupport χ) (i : Fin 2) (n : ℕ) (phase : TorusInverse.Plane → ℝ) (j : ℤ) (hj : j ≠ 0) : have amp := fun (z : TorusInverse.Plane) => periodize (nativeField (slotChart vr vt hdet) center (transverseStretch ci r0 (pulseProfile χ ψ x t i))) (covering^[n] z); (squareAverage fun (z : TorusInverse.Plane) => SmoothLoop.angularMean fun (θ : ℝ) => amp z * Real.cos (↑j * θ + phase z) ^ 2) = (|vr.1 * vt.2 - vr.2 * vt.1| / 2 * ∫ (ξ : ℝ), χ ξ ^ 2) * (ci * ∫ (v : ℝ) in 0..r ^ 2, ψ v ^ 2 * x v * t v i)

The same exact prefactor with the transverse integral restricted to the actual pulse interval, using the already verified compact pulse support.