Signed covariance updates with the constructed primary waves

The signed solve uses the existing primary square roots, pulse columns, physical masks, covering powers, and angular phases. Distinct labels are separated by the constructed padded slots. A signed square is retained as a separate term; it is not included in the linear covariance identity.

@[reducible, inline]

abbrev NavierStokes.SignedCovariance.Vec2 : Type

Vec2: an abbreviation for Fin 2 → ℝ.

Equations

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

@[reducible, inline]

abbrev NavierStokes.SignedCovariance.Mat2 : Type

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

Equations

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

@[reducible, inline]

abbrev NavierStokes.SignedCovariance.Plane : Type

Plane: an abbreviation for TorusInverse.Plane.

Equations

• NavierStokes.SignedCovariance.Plane = NavierStokes.TorusInverse.Plane

noncomputable def NavierStokes.SignedCovariance.increment (H : Mat2) (T R : Vec2) (j : Fin 2) : ℝ

The numerator is the actual inverse-matrix solve.

Equations

• NavierStokes.SignedCovariance.increment H T R j = Matrix.mulVec H⁻¹ R j / (2 * NavierStokes.SmoothCovariance.amplitudes H T j)

theorem NavierStokes.SignedCovariance.increment_eq_inverse (H : Mat2) (T R : Vec2) (hcone : SmoothCovariance.StrictCone H T) (j : Fin 2) : increment H T R j = Matrix.mulVec H⁻¹ R j / (2 * √(Matrix.mulVec H⁻¹ T j))

theorem NavierStokes.SignedCovariance.increment_eq_flat (H : Mat2) (T R : Vec2) (hcone : SmoothCovariance.StrictCone H T) : increment H T R = FlatCovariance.signedAmplitude 0 0 0 (fun (x : ℝ) => H) (fun (x : ℝ) => T) (fun (x : ℝ) => R) 1

The scalar solve is the already proved flat-edge solve at unit edge weight.

theorem NavierStokes.SignedCovariance.cross_reconstruct (H : Mat2) (T R : Vec2) (hcone : SmoothCovariance.StrictCone H T) : (Matrix.mulVec H fun (j : Fin 2) => 2 * SmoothCovariance.amplitudes H T j * increment H T R j) = R

Exact two-sided covariance, reusing FlatCovariance.signed_cross_reconstruct.

noncomputable def NavierStokes.SignedCovariance.squareColumn (H : Mat2) (T R : Vec2) : Vec2

The signed square is a genuine additional covariance.

Equations

• NavierStokes.SignedCovariance.squareColumn H T R = Matrix.mulVec H fun (j : Fin 2) => NavierStokes.SignedCovariance.increment H T R j ^ 2

A bilinear average of the actual waves

theorem NavierStokes.SignedCovariance.wave_product_rescale (a b : ℝ) (n : ℕ) (f g : Plane → ℝ) (mode : ℤ) (phase : Plane → ℝ) (Y : Plane) (θ : ℝ) : PartitionedCovariance.wave a n f mode phase Y θ * PartitionedCovariance.wave b n g mode phase Y θ = a * b * (PartitionedCovariance.wave 1 n f mode phase Y θ * PartitionedCovariance.wave 1 n g mode phase Y θ)

theorem NavierStokes.SignedCovariance.angularMean_bilinear (a b : ℝ) (n : ℕ) (f g : Plane → ℝ) (mode : ℤ) (hmode : mode ≠ 0) (phase : Plane → ℝ) (Y : Plane) : (SmoothLoop.angularMean fun (θ : ℝ) => PartitionedCovariance.wave a n f mode phase Y θ * PartitionedCovariance.wave b n g mode phase Y θ) = a * b * (PartitionedCovariance.covered n f Y * PartitionedCovariance.covered n g Y * (1 / 2))

theorem NavierStokes.SignedCovariance.angularMean_bilinear_continuous (a b : ℝ) (n : ℕ) {f g : Plane → ℝ} (hf : Continuous f) (hcf : HasCompactSupport f) (hg : Continuous g) (hcg : HasCompactSupport g) (mode : ℤ) (hmode : mode ≠ 0) (phase : Plane → ℝ) : Continuous fun (Y : PartitionedCovariance.Plane) => SmoothLoop.angularMean fun (θ : ℝ) => PartitionedCovariance.wave a n f mode phase Y θ * PartitionedCovariance.wave b n g mode phase Y θ

theorem NavierStokes.SignedCovariance.PairData.bilinear_diagonal {D h : ℝ} {vr vt : Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {U : PartitionedCovariance.UnsignedLabel} (P : PartitionedCovariance.PairData sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (a b : ℝ) (j i : Fin 2) : (PartitionedCovariance.doubleAverage fun (Y : PartitionedCovariance.Plane) (θ : ℝ) => PartitionedCovariance.wave a (SlotColoring.nativeIndex h U.1) (P.rawRadial hdet j) (P.modes j) (P.phases j) Y θ * PartitionedCovariance.wave b (SlotColoring.nativeIndex h U.1) (P.rawTangent hdet j i) (P.modes j) (P.phases j) Y θ) = a * b * P.matrix i j

Both scalar coefficients multiply precisely the same native pulse.

The same physical masks, slots, and phases for arbitrary coefficients

noncomputable def NavierStokes.SignedCovariance.radialWith {D h : ℝ} {vr vt : Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {U : PartitionedCovariance.UnsignedLabel} (P : PartitionedCovariance.PairData sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : ℝ) (a : Vec2) (q : ℝ) (x : SlotColoring.Position) (j : Fin 2) : Plane → ℝ → ℝ

Radial with, given by wave (outer * (Real.sqrt ε * a j * mask D U q x)) (SlotColoring.nativeIndex h U.1) (P.rawRadial hdet j) (P.modes j) (P.phases j).

Equations

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

noncomputable def NavierStokes.SignedCovariance.tangentWith {D h : ℝ} {vr vt : Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {U : PartitionedCovariance.UnsignedLabel} (P : PartitionedCovariance.PairData sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : ℝ) (a : Vec2) (q : ℝ) (x : SlotColoring.Position) (j i : Fin 2) : Plane → ℝ → ℝ

Tangent with, constructed using wave.

Equations

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

theorem NavierStokes.SignedCovariance.radialWith_primary {D h : ℝ} {vr vt : Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {U : PartitionedCovariance.UnsignedLabel} (P : PartitionedCovariance.PairData sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : ℝ) (T : Vec2) (q : ℝ) (x : SlotColoring.Position) (j : Fin 2) : radialWith P hdet outer ε (SmoothCovariance.amplitudes P.matrix T) q x j = P.radialWave hdet outer ε T q x j

theorem NavierStokes.SignedCovariance.tangentWith_primary {D h : ℝ} {vr vt : Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {U : PartitionedCovariance.UnsignedLabel} (P : PartitionedCovariance.PairData sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : ℝ) (T : Vec2) (q : ℝ) (x : SlotColoring.Position) (j i : Fin 2) : tangentWith P hdet outer ε (SmoothCovariance.amplitudes P.matrix T) q x j i = P.tangentWave hdet outer ε T q x j i

theorem NavierStokes.SignedCovariance.finite_product_diagonal {D h : ℝ} {vr vt : Plane} (sys : PartitionedCovariance.SlotSystem D h vr vt) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (N : ℕ) (hN : 1 ≤ N) (P : (U : PartitionedCovariance.UnsignedLabel) → PartitionedCovariance.PairData sys (PartitionedCovariance.tailLabel N U)) (outer ε : PartitionedCovariance.UnsignedLabel → ℝ) (a b : PartitionedCovariance.UnsignedLabel → Vec2) (F : Finset PartitionedCovariance.UnsignedLabel) {q : ℝ} (hq : 0 < q) (x : SlotColoring.Position) (i : Fin 2) (Y : Plane) (θ : ℝ) : (∑ v ∈ F.product Finset.univ, radialWith (P v.1) hdet (outer v.1) (ε v.1) (a v.1) q x v.2 Y θ) * ∑ v ∈ F.product Finset.univ, tangentWith (P v.1) hdet (outer v.1) (ε v.1) (b v.1) q x v.2 i Y θ = ∑ v ∈ F.product Finset.univ, radialWith (P v.1) hdet (outer v.1) (ε v.1) (a v.1) q x v.2 Y θ * tangentWith (P v.1) hdet (outer v.1) (ε v.1) (b v.1) q x v.2 i Y θ

Pointwise diagonal reduction uses padded-slot disjointness, including when different labels carry the same angular harmonic.

theorem NavierStokes.SignedCovariance.finite_bilinear_covariance {D h : ℝ} {vr vt : Plane} (sys : PartitionedCovariance.SlotSystem D h vr vt) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (N : ℕ) (hN : 1 ≤ N) (P : (U : PartitionedCovariance.UnsignedLabel) → PartitionedCovariance.PairData sys (PartitionedCovariance.tailLabel N U)) (outer ε : PartitionedCovariance.UnsignedLabel → ℝ) (a b : PartitionedCovariance.UnsignedLabel → Vec2) (F : Finset PartitionedCovariance.UnsignedLabel) (hε : ∀ U ∈ F, 0 ≤ ε U) {q : ℝ} (hq : 0 < q) (x : SlotColoring.Position) (i : Fin 2) : (PartitionedCovariance.doubleAverage fun (Y : PartitionedCovariance.Plane) (θ : ℝ) => (∑ v ∈ F.product Finset.univ, radialWith (P v.1) hdet (outer v.1) (ε v.1) (a v.1) q x v.2 Y θ) * ∑ v ∈ F.product Finset.univ, tangentWith (P v.1) hdet (outer v.1) (ε v.1) (b v.1) q x v.2 i Y θ) = ∑ U ∈ F, outer U ^ 2 * ε U * PartitionedCovariance.mask D (PartitionedCovariance.tailLabel N U) q x ^ 2 * Matrix.mulVec (P U).matrix (fun (j : Fin 2) => a U j * b U j) i

noncomputable def NavierStokes.SignedCovariance.assembledRadialWith {D h : ℝ} {vr vt : Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {N : ℕ} (P : (U : PartitionedCovariance.UnsignedLabel) → PartitionedCovariance.PairData sys (PartitionedCovariance.tailLabel N U)) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : PartitionedCovariance.UnsignedLabel → ℝ) (a : PartitionedCovariance.UnsignedLabel → Vec2) (q : ℝ) (x : SlotColoring.Position) (Y : Plane) (θ : ℝ) : ℝ

Assembled radial with, given by ∑ᶠ v : UnsignedLabel × Fin 2, radialWith (P v.1) hdet (outer v.1) (ε v.1) (a v.1) q x v.2 Y θ.

Equations

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

noncomputable def NavierStokes.SignedCovariance.assembledTangentWith {D h : ℝ} {vr vt : Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {N : ℕ} (P : (U : PartitionedCovariance.UnsignedLabel) → PartitionedCovariance.PairData sys (PartitionedCovariance.tailLabel N U)) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : PartitionedCovariance.UnsignedLabel → ℝ) (a : PartitionedCovariance.UnsignedLabel → Vec2) (q : ℝ) (x : SlotColoring.Position) (i : Fin 2) (Y : Plane) (θ : ℝ) : ℝ

Assembled tangent with, given by ∑ᶠ v : UnsignedLabel × Fin 2, tangentWith (P v.1) hdet (outer v.1) (ε v.1) (a v.1) q x v.2 i Y θ.

Equations

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

theorem NavierStokes.SignedCovariance.assembledRadialWith_finite {D h : ℝ} {vr vt : Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {N : ℕ} (P : (U : PartitionedCovariance.UnsignedLabel) → PartitionedCovariance.PairData sys (PartitionedCovariance.tailLabel N U)) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : PartitionedCovariance.UnsignedLabel → ℝ) (a : PartitionedCovariance.UnsignedLabel → Vec2) {q : ℝ} (hq : 0 < q) (x : SlotColoring.Position) (Y : Plane) (θ : ℝ) : assembledRadialWith P hdet outer ε a q x Y θ = ∑ v ∈ ⋯.toFinset.product Finset.univ, radialWith (P v.1) hdet (outer v.1) (ε v.1) (a v.1) q x v.2 Y θ

theorem NavierStokes.SignedCovariance.assembledTangentWith_finite {D h : ℝ} {vr vt : Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {N : ℕ} (P : (U : PartitionedCovariance.UnsignedLabel) → PartitionedCovariance.PairData sys (PartitionedCovariance.tailLabel N U)) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : PartitionedCovariance.UnsignedLabel → ℝ) (a : PartitionedCovariance.UnsignedLabel → Vec2) {q : ℝ} (hq : 0 < q) (x : SlotColoring.Position) (i : Fin 2) (Y : Plane) (θ : ℝ) : assembledTangentWith P hdet outer ε a q x i Y θ = ∑ v ∈ ⋯.toFinset.product Finset.univ, tangentWith (P v.1) hdet (outer v.1) (ε v.1) (a v.1) q x v.2 i Y θ

theorem NavierStokes.SignedCovariance.assembled_bilinear_covariance {D h : ℝ} {vr vt : Plane} (sys : PartitionedCovariance.SlotSystem D h vr vt) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (N : ℕ) (hN : 1 ≤ N) (P : (U : PartitionedCovariance.UnsignedLabel) → PartitionedCovariance.PairData sys (PartitionedCovariance.tailLabel N U)) (outer ε : PartitionedCovariance.UnsignedLabel → ℝ) (a b : PartitionedCovariance.UnsignedLabel → Vec2) {q : ℝ} (hq : 0 < q) (x : SlotColoring.Position) (hε : ∀ (U : PartitionedCovariance.UnsignedLabel), PartitionedCovariance.mask D (PartitionedCovariance.tailLabel N U) q x ≠ 0 → 0 ≤ ε U) (i : Fin 2) : (PartitionedCovariance.doubleAverage fun (Y : PartitionedCovariance.Plane) (θ : ℝ) => assembledRadialWith P hdet outer ε a q x Y θ * assembledTangentWith P hdet outer ε b q x i Y θ) = ∑ᶠ (U : PartitionedCovariance.UnsignedLabel), outer U ^ 2 * ε U * PartitionedCovariance.mask D (PartitionedCovariance.tailLabel N U) q x ^ 2 * Matrix.mulVec (P U).matrix (fun (j : Fin 2) => a U j * b U j) i

theorem NavierStokes.SignedCovariance.assembled_bilinear_symmetry {D h : ℝ} {vr vt : Plane} (sys : PartitionedCovariance.SlotSystem D h vr vt) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (N : ℕ) (hN : 1 ≤ N) (P : (U : PartitionedCovariance.UnsignedLabel) → PartitionedCovariance.PairData sys (PartitionedCovariance.tailLabel N U)) (outer ε : PartitionedCovariance.UnsignedLabel → ℝ) (a b : PartitionedCovariance.UnsignedLabel → Vec2) {q : ℝ} (hq : 0 < q) (x : SlotColoring.Position) (i : Fin 2) (Y : Plane) (θ : ℝ) : assembledRadialWith P hdet outer ε a q x Y θ * assembledTangentWith P hdet outer ε b q x i Y θ = assembledRadialWith P hdet outer ε b q x Y θ * assembledTangentWith P hdet outer ε a q x i Y θ

Off-diagonal products vanish before either integral, so interchanging the two scalar coefficient families leaves the product unchanged pointwise.

noncomputable def NavierStokes.SignedCovariance.signedRadial {D h : ℝ} {vr vt : Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {N : ℕ} (P : (U : PartitionedCovariance.UnsignedLabel) → PartitionedCovariance.PairData sys (PartitionedCovariance.tailLabel N U)) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : PartitionedCovariance.UnsignedLabel → ℝ) (T R : PartitionedCovariance.UnsignedLabel → Vec2) (q : ℝ) (x : SlotColoring.Position) : Plane → ℝ → ℝ

Signed radial, given by assembledRadialWith P hdet outer ε (fun U => increment (P U).matrix (T U) (R U)) q x.

Equations

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

noncomputable def NavierStokes.SignedCovariance.signedTangent {D h : ℝ} {vr vt : Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {N : ℕ} (P : (U : PartitionedCovariance.UnsignedLabel) → PartitionedCovariance.PairData sys (PartitionedCovariance.tailLabel N U)) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : PartitionedCovariance.UnsignedLabel → ℝ) (T R : PartitionedCovariance.UnsignedLabel → Vec2) (q : ℝ) (x : SlotColoring.Position) (i : Fin 2) : Plane → ℝ → ℝ

Signed tangent, given by assembledTangentWith P hdet outer ε (fun U => increment (P U).matrix (T U) (R U)) q x i.

Equations

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

theorem NavierStokes.SignedCovariance.cross_reconstruct_component (H : Mat2) (T R : Vec2) (hcone : SmoothCovariance.StrictCone H T) (i : Fin 2) : 2 * Matrix.mulVec H (fun (j : Fin 2) => SmoothCovariance.amplitudes H T j * increment H T R j) i = R i

theorem NavierStokes.SignedCovariance.assembled_cross_covariance {D h : ℝ} {vr vt : Plane} (sys : PartitionedCovariance.SlotSystem D h vr vt) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (N : ℕ) (hN : 1 ≤ N) (P : (U : PartitionedCovariance.UnsignedLabel) → PartitionedCovariance.PairData sys (PartitionedCovariance.tailLabel N U)) (outer ε : PartitionedCovariance.UnsignedLabel → ℝ) (T R : PartitionedCovariance.UnsignedLabel → Vec2) {q : ℝ} (hq : 0 < q) (x : SlotColoring.Position) (hε : ∀ (U : PartitionedCovariance.UnsignedLabel), PartitionedCovariance.mask D (PartitionedCovariance.tailLabel N U) q x ≠ 0 → 0 ≤ ε U) (hcone : ∀ (U : PartitionedCovariance.UnsignedLabel), PartitionedCovariance.mask D (PartitionedCovariance.tailLabel N U) q x ≠ 0 → SmoothCovariance.StrictCone (P U).matrix (T U)) (i : Fin 2) : (PartitionedCovariance.doubleAverage fun (Y : PartitionedCovariance.Plane) (θ : ℝ) => PartitionedCovariance.assembledRadial P hdet outer ε T q x Y θ * signedTangent P hdet outer ε T R q x i Y θ + signedRadial P hdet outer ε T R q x Y θ * PartitionedCovariance.assembledTangent P hdet outer ε T q x i Y θ) = ∑ᶠ (U : PartitionedCovariance.UnsignedLabel), outer U ^ 2 * ε U * PartitionedCovariance.mask D (PartitionedCovariance.tailLabel N U) q x ^ 2 * R U i

The assembled two-sided primary/signed cross covariance. Positivity is required only for primary weights; the signed target is arbitrary.

theorem NavierStokes.SignedCovariance.assembled_signed_square {D h : ℝ} {vr vt : Plane} (sys : PartitionedCovariance.SlotSystem D h vr vt) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (N : ℕ) (hN : 1 ≤ N) (P : (U : PartitionedCovariance.UnsignedLabel) → PartitionedCovariance.PairData sys (PartitionedCovariance.tailLabel N U)) (outer ε : PartitionedCovariance.UnsignedLabel → ℝ) (T R : PartitionedCovariance.UnsignedLabel → Vec2) {q : ℝ} (hq : 0 < q) (x : SlotColoring.Position) (hε : ∀ (U : PartitionedCovariance.UnsignedLabel), PartitionedCovariance.mask D (PartitionedCovariance.tailLabel N U) q x ≠ 0 → 0 ≤ ε U) (i : Fin 2) : (PartitionedCovariance.doubleAverage fun (Y : PartitionedCovariance.Plane) (θ : ℝ) => signedRadial P hdet outer ε T R q x Y θ * signedTangent P hdet outer ε T R q x i Y θ) = ∑ᶠ (U : PartitionedCovariance.UnsignedLabel), outer U ^ 2 * ε U * PartitionedCovariance.mask D (PartitionedCovariance.tailLabel N U) q x ^ 2 * squareColumn (P U).matrix (T U) (R U) i

The signed-square covariance is retained exactly, with no sign restriction on the prescribed stress.

The physical signed target

noncomputable def NavierStokes.SignedCovariance.chartStress (h : ℝ) (N : ℕ) (σ : Vec2) (U : PartitionedCovariance.UnsignedLabel) : Vec2

Section 10.2's chart stress Q^(2 A) σ / ε.

Equations

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

theorem NavierStokes.SignedCovariance.physical_signed_scale (h : ℝ) (N : ℕ) (σ : Vec2) (U : PartitionedCovariance.UnsignedLabel) (i : Fin 2) : PartitionedCovariance.physicalOuter h N U ^ 2 * PartitionedCovariance.physicalViscosity h N U * chartStress h N σ U i = σ i

theorem NavierStokes.SignedCovariance.physical_signed_cross_covariance {D h : ℝ} {vr vt : Plane} (sys : PartitionedCovariance.SlotSystem D h vr vt) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (N : ℕ) (hN : 1 ≤ N) (P : (U : PartitionedCovariance.UnsignedLabel) → PartitionedCovariance.PairData sys (PartitionedCovariance.tailLabel N U)) {q : ℝ} (hq : 0 < q) (hqN : q ≤ ChartScales.Q N) (x : SlotColoring.Position) (T0 σ : Vec2) (hcone : ∀ (U : PartitionedCovariance.UnsignedLabel), PartitionedCovariance.mask D (PartitionedCovariance.tailLabel N U) q x ≠ 0 → SmoothCovariance.StrictCone (P U).matrix (PartitionedCovariance.chartTarget h q N T0 U)) (i : Fin 2) : (PartitionedCovariance.doubleAverage fun (Y : PartitionedCovariance.Plane) (θ : ℝ) => PartitionedCovariance.assembledRadial P hdet (PartitionedCovariance.physicalOuter h N) (PartitionedCovariance.physicalViscosity h N) (PartitionedCovariance.chartTarget h q N T0) q x Y θ * signedTangent P hdet (PartitionedCovariance.physicalOuter h N) (PartitionedCovariance.physicalViscosity h N) (PartitionedCovariance.chartTarget h q N T0) (chartStress h N σ) q x i Y θ + signedRadial P hdet (PartitionedCovariance.physicalOuter h N) (PartitionedCovariance.physicalViscosity h N) (PartitionedCovariance.chartTarget h q N T0) (chartStress h N σ) q x Y θ * PartitionedCovariance.assembledTangent P hdet (PartitionedCovariance.physicalOuter h N) (PartitionedCovariance.physicalViscosity h N) (PartitionedCovariance.chartTarget h q N T0) q x i Y θ) = σ i

The actual two-sided primary/signed covariance equals the prescribed physical stress, for the same constructed squared partition as the primary.

Uniform weighted jets from input classes and a primary lower bound

noncomputable def NavierStokes.SignedCovariance.InverseControl {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : WeightedClasses.StripData E) (w g : ℕ → E → ℝ) : Prop

A polynomial reciprocal bound, imposed only on the positive primary weight. No regularity of a quotient by the envelope is assumed.

Equations

• NavierStokes.SignedCovariance.InverseControl s w g = ∃ (C : ℝ), 0 ≤ C ∧ ∃ (p : ℕ), ∀ (n : ℕ), ∀ x ∈ s.domain, w n x / g n x ≤ C * s.growth n x ^ p

theorem NavierStokes.SignedCovariance.inverseControl_of_lower {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData E} {w g : ℕ → E → ℝ} (hg : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 < g n x) {c : ℝ} (hc : 0 < c) (p : ℕ) (hlower : ∀ (n : ℕ), ∀ x ∈ s.domain, c * w n x / s.growth n x ^ p ≤ g n x) : InverseControl s w g

theorem NavierStokes.SignedCovariance.class_input_envelope {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData E} {w g r : ℕ → E → ℝ} (hw : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 < w n x) (hp : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 < g n x) (hg : WeightedClasses.MemClass s w 0 g) (hr : WeightedClasses.MemClass s w 0 r) (hlower : InverseControl s w g) (m : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∃ (p : ℕ), ∀ (n : ℕ), ∀ x ∈ s.domain, 1 ≤ C * s.growth n x ^ p ∧ w n x / (C * s.growth n x ^ p) ≤ g n x ∧ (∀ j ≤ m, ‖iteratedFDeriv ℝ j (g n) x‖ ≤ w n x * (C * s.growth n x ^ p)) ∧ ∀ j ≤ m, ‖iteratedFDeriv ℝ j (r n) x‖ ≤ w n x * (C * s.growth n x ^ p)

A common finite envelope for input jets and the positive lower bound, uniform in the discrete band and every point of the strip.

noncomputable def NavierStokes.SignedCovariance.signedJetCost (j : ℕ) : ℝ

Signed jet cost, given by WeightedQuotients.chooseSum j * WeightedQuotients.orderBound (-(1 / 2 : ℝ)) j / 2.

Equations

• NavierStokes.SignedCovariance.signedJetCost j = NavierStokes.WeightedQuotients.chooseSum j * NavierStokes.WeightedQuotients.orderBound (-(1 / 2)) j / 2

noncomputable def NavierStokes.SignedCovariance.prefixJetCost (m : ℕ) : ℝ

Prefix jet cost, given by 1 + ∑ j ∈ Finset.range (m + 1), |signedJetCost j|.

Equations

• NavierStokes.SignedCovariance.prefixJetCost m = 1 + ∑ j ∈ Finset.range (m + 1), |NavierStokes.SignedCovariance.signedJetCost j|

theorem NavierStokes.SignedCovariance.prefixJetCost_pos (m : ℕ) : 0 < prefixJetCost m

theorem NavierStokes.SignedCovariance.signedJetCost_le {j m : ℕ} (hj : j ≤ m) : signedJetCost j ≤ prefixJetCost m

theorem NavierStokes.SignedCovariance.signedJetCost_nonneg (j : ℕ) : 0 ≤ signedJetCost j

theorem NavierStokes.SignedCovariance.signed_quotient_class_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData E} {w g r : ℕ → E → ℝ} (hw : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 < w n x) (hp : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 < g n x) (hg : WeightedClasses.MemClass s w 0 g) (hr : WeightedClasses.MemClass s w 0 r) (hlower : InverseControl s w g) : WeightedClasses.MemClass s (fun (n : ℕ) (x : E) => √(w n x)) 0 fun (n : ℕ) (x : E) => r n x / (2 * √(g n x))

Derive the all-order signed quotient class from weighted input jets. The weight is never differentiated or divided out as a variable function.

theorem NavierStokes.SignedCovariance.signed_quotient_class {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData E} {w g r : ℕ → E → ℝ} {β : ℝ} (hw : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 < w n x) (hp : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 < g n x) (hg : WeightedClasses.MemClass s w 0 g) (hr : WeightedClasses.MemClass s w β r) (hlower : InverseControl s w g) : WeightedClasses.MemClass s (fun (n : ℕ) (x : E) => √(w n x)) β fun (n : ℕ) (x : E) => r n x / (2 * √(g n x))

Discrete powers of epsilon pass through the quotient without a jet loss.

theorem NavierStokes.SignedCovariance.sqrt_class {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData E} {w g : ℕ → E → ℝ} (hw : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 < w n x) (hp : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 < g n x) (hg : WeightedClasses.MemClass s w 0 g) (hlower : InverseControl s w g) : WeightedClasses.MemClass s (fun (n : ℕ) (x : E) => √(w n x)) 0 fun (n : ℕ) (x : E) => √(g n x)

A companion primary square-root bound from the same genuine inputs.

theorem NavierStokes.SignedCovariance.memClass_congrOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData E} {w f g : ℕ → E → ℝ} {β : ℝ} (hf : WeightedClasses.MemClass s w β f) (heq : ∀ (n : ℕ), ∀ x ∈ s.domain, f n x = g n x) : WeightedClasses.MemClass s w β g

theorem NavierStokes.SignedCovariance.increment_wave_class {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData E} {H : ℕ → E → Mat2} {T R : ℕ → E → Vec2} {β : ℝ} (j : Fin 2) (hζ : ∀ x ∈ s.domain, 0 < s.zeta x) (hcone : ∀ (n : ℕ), ∀ x ∈ s.domain, SmoothCovariance.StrictCone (H n x) (T n x)) (hY : WeightedClasses.MeanClass s 0 fun (n : ℕ) (x : E) => Matrix.mulVec (H n x)⁻¹ (T n x) j) (hR : WeightedClasses.MeanClass s β fun (n : ℕ) (x : E) => Matrix.mulVec (H n x)⁻¹ (R n x) j) (hlower : InverseControl s (fun (x : ℕ) (x_1 : E) => s.zeta x_1) fun (n : ℕ) (x : E) => Matrix.mulVec (H n x)⁻¹ (T n x) j) : WeightedClasses.WaveClass s (fun (x : ℕ) (x_1 : E) => 1) β fun (n : ℕ) (x : E) => increment (H n x) (T n x) (R n x) j

The actual matrix-inverse signed coefficient has the half-weight class, derived from the inverse numerator jets and positive primary inverse jets.

theorem NavierStokes.SignedCovariance.increment_times_pulse_class {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData E} {H : ℕ → E → Mat2} {T R : ℕ → E → Vec2} {β γ : ℝ} {P f : ℕ → E → ℝ} (j : Fin 2) (hζ : ∀ x ∈ s.domain, 0 < s.zeta x) (hcone : ∀ (n : ℕ), ∀ x ∈ s.domain, SmoothCovariance.StrictCone (H n x) (T n x)) (hY : WeightedClasses.MeanClass s 0 fun (n : ℕ) (x : E) => Matrix.mulVec (H n x)⁻¹ (T n x) j) (hR : WeightedClasses.MeanClass s β fun (n : ℕ) (x : E) => Matrix.mulVec (H n x)⁻¹ (R n x) j) (hlower : InverseControl s (fun (x : ℕ) (x_1 : E) => s.zeta x_1) fun (n : ℕ) (x : E) => Matrix.mulVec (H n x)⁻¹ (T n x) j) (hf : WeightedClasses.MemClass s P γ f) : WeightedClasses.WaveClass s P (β + γ) fun (n : ℕ) (x : E) => increment (H n x) (T n x) (R n x) j * f n x

Multiplying a signed coefficient by the original pulse envelope gives the wave weight sqrt ζ * P with the expected epsilon exponent.

theorem NavierStokes.SignedCovariance.signed_square_class {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData E} {H : ℕ → E → Mat2} {T R : ℕ → E → Vec2} {β : ℝ} (i : Fin 2) (hζ : ∀ x ∈ s.domain, 0 < s.zeta x) (hcone : ∀ (n : ℕ), ∀ x ∈ s.domain, SmoothCovariance.StrictCone (H n x) (T n x)) (hY : ∀ (j : Fin 2), WeightedClasses.MeanClass s 0 fun (n : ℕ) (x : E) => Matrix.mulVec (H n x)⁻¹ (T n x) j) (hR : ∀ (j : Fin 2), WeightedClasses.MeanClass s β fun (n : ℕ) (x : E) => Matrix.mulVec (H n x)⁻¹ (R n x) j) (hlower : ∀ (j : Fin 2), InverseControl s (fun (x : ℕ) (x_1 : E) => s.zeta x_1) fun (n : ℕ) (x : E) => Matrix.mulVec (H n x)⁻¹ (T n x) j) (hH : ∀ (j : Fin 2), WeightedClasses.UnweightedClass s 0 fun (n : ℕ) (x : E) => H n x i j) : WeightedClasses.MeanClass s (2 * β) fun (n : ℕ) (x : E) => squareColumn (H n x) (T n x) (R n x) i

The exact signed-square column satisfies a mean-class estimate. The assumptions are estimates for the input inverse solves and actual columns.

theorem NavierStokes.SignedCovariance.native_signed_square_class {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData E} {H : ℕ → E → Mat2} {T R : ℕ → E → Vec2} (B loss : ℝ) (i : Fin 2) (hζ : ∀ x ∈ s.domain, 0 < s.zeta x) (hcone : ∀ (n : ℕ), ∀ x ∈ s.domain, SmoothCovariance.StrictCone (H n x) (T n x)) (hY : ∀ (j : Fin 2), WeightedClasses.MeanClass s 0 fun (n : ℕ) (x : E) => Matrix.mulVec (H n x)⁻¹ (T n x) j) (hR : ∀ (j : Fin 2), WeightedClasses.MeanClass s (B - 1 / 2 - loss) fun (n : ℕ) (x : E) => Matrix.mulVec (H n x)⁻¹ (R n x) j) (hlower : ∀ (j : Fin 2), InverseControl s (fun (x : ℕ) (x_1 : E) => s.zeta x_1) fun (n : ℕ) (x : E) => Matrix.mulVec (H n x)⁻¹ (T n x) j) (hH : ∀ (j : Fin 2), WeightedClasses.UnweightedClass s 0 fun (n : ℕ) (x : E) => H n x i j) : WeightedClasses.MeanClass s (2 * B - 2 * loss) fun (n : ℕ) (x : E) => s.epsilon n * squareColumn (H n x) (T n x) (R n x) i

Native velocity amplitudes contain sqrt ε, so their signed-square covariance is ε H(δa²) and has order 2B - 2loss.

theorem NavierStokes.SignedCovariance.balanced_signed_square_class {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData E} {H : ℕ → E → Mat2} {T R : ℕ → E → Vec2} {w v : Fin 2 → ℕ → E → ℝ} {β : ℝ} (i : Fin 2) (hw : ∀ (j : Fin 2) (n : ℕ), ∀ x ∈ s.domain, 0 < w j n x) (hcone : ∀ (n : ℕ), ∀ x ∈ s.domain, SmoothCovariance.StrictCone (H n x) (T n x)) (hY : ∀ (j : Fin 2), WeightedClasses.MemClass s (w j) 0 fun (n : ℕ) (x : E) => Matrix.mulVec (H n x)⁻¹ (T n x) j) (hR : ∀ (j : Fin 2), WeightedClasses.MemClass s (w j) β fun (n : ℕ) (x : E) => Matrix.mulVec (H n x)⁻¹ (R n x) j) (hlower : ∀ (j : Fin 2), InverseControl s (w j) fun (n : ℕ) (x : E) => Matrix.mulVec (H n x)⁻¹ (T n x) j) (hH : ∀ (j : Fin 2), WeightedClasses.MemClass s (v j) 0 fun (n : ℕ) (x : E) => H n x i j) (hbalance : ∀ (j : Fin 2) (n : ℕ), ∀ x ∈ s.domain, v j n x * w j n x ≤ s.zeta x) : WeightedClasses.MeanClass s (2 * β) fun (n : ℕ) (x : E) => squareColumn (H n x) (T n x) (R n x) i

This version keeps the flat weights of the individual columns. The column weight and its inverse-solve weight multiply back to the mean weight; an exponentially singular inverse is therefore not assumed unweighted.

theorem NavierStokes.SignedCovariance.balanced_edge_weights (σ κ δ : ℝ) : FlatCutoff.edge κ δ * FlatCutoff.edge (σ - κ) δ = FlatCutoff.edge σ δ

Exact cancellation of the column's flat factor with the remaining inverse-solve factor, including the zero edge.

theorem NavierStokes.SignedCovariance.balanced_native_signed_square_class {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData E} {H : ℕ → E → Mat2} {T R : ℕ → E → Vec2} {w v : Fin 2 → ℕ → E → ℝ} (B loss : ℝ) (i : Fin 2) (hw : ∀ (j : Fin 2) (n : ℕ), ∀ x ∈ s.domain, 0 < w j n x) (hcone : ∀ (n : ℕ), ∀ x ∈ s.domain, SmoothCovariance.StrictCone (H n x) (T n x)) (hY : ∀ (j : Fin 2), WeightedClasses.MemClass s (w j) 0 fun (n : ℕ) (x : E) => Matrix.mulVec (H n x)⁻¹ (T n x) j) (hR : ∀ (j : Fin 2), WeightedClasses.MemClass s (w j) (B - 1 / 2 - loss) fun (n : ℕ) (x : E) => Matrix.mulVec (H n x)⁻¹ (R n x) j) (hlower : ∀ (j : Fin 2), InverseControl s (w j) fun (n : ℕ) (x : E) => Matrix.mulVec (H n x)⁻¹ (T n x) j) (hH : ∀ (j : Fin 2), WeightedClasses.MemClass s (v j) 0 fun (n : ℕ) (x : E) => H n x i j) (hbalance : ∀ (j : Fin 2) (n : ℕ), ∀ x ∈ s.domain, v j n x * w j n x ≤ s.zeta x) : WeightedClasses.MeanClass s (2 * B - 2 * loss) fun (n : ℕ) (x : E) => s.epsilon n * squareColumn (H n x) (T n x) (R n x) i

A quantitative bound for the complete assembled signed square

theorem NavierStokes.SignedCovariance.increment_sq_bound (H : Mat2) (T R : Vec2) (hcone : SmoothCovariance.StrictCone H T) (j : Fin 2) {l d : ℝ} (hl : 0 < l) (_hd : 0 ≤ d) (hY : l ≤ Matrix.mulVec H⁻¹ T j) (hR : |Matrix.mulVec H⁻¹ R j| ≤ d) : increment H T R j ^ 2 ≤ d ^ 2 / (4 * l)

theorem NavierStokes.SignedCovariance.squareColumn_abs_bound (H : Mat2) (T R : Vec2) (hcone : SmoothCovariance.StrictCone H T) (i : Fin 2) {l d K : ℝ} (hl : 0 < l) (hd : 0 ≤ d) (hK : 0 ≤ K) (hY : ∀ (j : Fin 2), l ≤ Matrix.mulVec H⁻¹ T j) (hR : ∀ (j : Fin 2), |Matrix.mulVec H⁻¹ R j| ≤ d) (hH : ∀ (j : Fin 2), |H i j| ≤ K) : |squareColumn H T R i| ≤ 2 * K * d ^ 2 / (4 * l)

theorem NavierStokes.SignedCovariance.mask_average_bound (D : ℝ) (N : ℕ) {q : ℝ} (hq : 0 < q) (hqN : q ≤ ChartScales.Q N) (x : SlotColoring.Position) (f : PartitionedCovariance.UnsignedLabel → ℝ) (B : ℝ) (hb : ∀ (U : PartitionedCovariance.UnsignedLabel), PartitionedCovariance.mask D (PartitionedCovariance.tailLabel N U) q x ≠ 0 → |f U| ≤ B) : |∑ᶠ (U : PartitionedCovariance.UnsignedLabel), PartitionedCovariance.mask D (PartitionedCovariance.tailLabel N U) q x ^ 2 * f U| ≤ B

theorem NavierStokes.SignedCovariance.assembled_signed_square_bound {D h : ℝ} {vr vt : Plane} (sys : PartitionedCovariance.SlotSystem D h vr vt) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (N : ℕ) (hN : 1 ≤ N) (P : (U : PartitionedCovariance.UnsignedLabel) → PartitionedCovariance.PairData sys (PartitionedCovariance.tailLabel N U)) (outer ε : PartitionedCovariance.UnsignedLabel → ℝ) (T R : PartitionedCovariance.UnsignedLabel → Vec2) {q : ℝ} (hq : 0 < q) (hqN : q ≤ ChartScales.Q N) (x : SlotColoring.Position) (hε : ∀ (U : PartitionedCovariance.UnsignedLabel), PartitionedCovariance.mask D (PartitionedCovariance.tailLabel N U) q x ≠ 0 → 0 ≤ ε U) (hcone : ∀ (U : PartitionedCovariance.UnsignedLabel), PartitionedCovariance.mask D (PartitionedCovariance.tailLabel N U) q x ≠ 0 → SmoothCovariance.StrictCone (P U).matrix (T U)) {l d K Λ : ℝ} (hl : 0 < l) (hd : 0 ≤ d) (hK : 0 ≤ K) (hΛ : 0 ≤ Λ) (hY : ∀ (U : PartitionedCovariance.UnsignedLabel), PartitionedCovariance.mask D (PartitionedCovariance.tailLabel N U) q x ≠ 0 → ∀ (j : Fin 2), l ≤ Matrix.mulVec (P U).matrix⁻¹ (T U) j) (hR : ∀ (U : PartitionedCovariance.UnsignedLabel), PartitionedCovariance.mask D (PartitionedCovariance.tailLabel N U) q x ≠ 0 → ∀ (j : Fin 2), |Matrix.mulVec (P U).matrix⁻¹ (R U) j| ≤ d) (hH : ∀ (U : PartitionedCovariance.UnsignedLabel), PartitionedCovariance.mask D (PartitionedCovariance.tailLabel N U) q x ≠ 0 → ∀ (i j : Fin 2), |(P U).matrix i j| ≤ K) (hscale : ∀ (U : PartitionedCovariance.UnsignedLabel), PartitionedCovariance.mask D (PartitionedCovariance.tailLabel N U) q x ≠ 0 → outer U ^ 2 * ε U ≤ Λ) (i : Fin 2) : |PartitionedCovariance.doubleAverage fun (Y : PartitionedCovariance.Plane) (θ : ℝ) => signedRadial P hdet outer ε T R q x Y θ * signedTangent P hdet outer ε T R q x i Y θ| ≤ Λ * (2 * K * d ^ 2 / (4 * l))

A bound for the full actual averaged remainder, proved from the primary inverse lower bound, signed inverse numerator bound, and actual column bound. The number of active labels costs nothing because their squared masks sum to one.

Smooth edge extension of the actual inverse amplitudes

noncomputable def NavierStokes.SignedCovariance.extendedIncrement {E : Type u_1} (H : E × ℝ → Mat2) (T R : E × ℝ → Vec2) (j : Fin 2) : E × ℝ → ℝ

Extended increment, given by FlatZeroExtension.zeroExtension (fun p => ((H p)⁻¹.mulVec (R p)) j / (2 * Real.sqrt (((H p)⁻¹.mulVec (T p)) j))).

Equations

• NavierStokes.SignedCovariance.extendedIncrement H T R j = NavierStokes.FlatZeroExtension.zeroExtension fun (p : E × ℝ) => Matrix.mulVec (H p)⁻¹ (R p) j / (2 * √(Matrix.mulVec (H p)⁻¹ (T p) j))

theorem NavierStokes.SignedCovariance.extendedIncrement_of_pos {E : Type u_1} (H : E × ℝ → Mat2) (T R : E × ℝ → Vec2) (j : Fin 2) {p : E × ℝ} (hp : 0 < p.2) (hcone : SmoothCovariance.StrictCone (H p) (T p)) : extendedIncrement H T R j p = increment (H p) (T p) (R p) j

theorem NavierStokes.SignedCovariance.extendedIncrement_of_nonpos {E : Type u_1} (H : E × ℝ → Mat2) (T R : E × ℝ → Vec2) (j : Fin 2) {p : E × ℝ} (hp : p.2 ≤ 0) : extendedIncrement H T R j p = 0

theorem NavierStokes.SignedCovariance.extendedIncrement_regular {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set E} (hU : IsOpen U) {c : ℝ} (hc : 0 < c) {H : E × ℝ → Mat2} {T R : E × ℝ → Vec2} {S : E × ℝ → ℝ} (j : Fin 2) (hS : ∀ p ∈ WeightedQuotients.edgeStrip U, 1 ≤ S p) (hscale : WeightedQuotients.LocallyBoundedScale U S) (hH : ∀ (i j : Fin 2), ContDiffOn ℝ (↑⊤) (fun (p : E × ℝ) => H p i j) (U ×ˢ Set.Ioi 0)) (hT : ∀ (i : Fin 2), ContDiffOn ℝ (↑⊤) (fun (p : E × ℝ) => T p i) (U ×ˢ Set.Ioi 0)) (hR : ∀ (i : Fin 2), ContDiffOn ℝ (↑⊤) (fun (p : E × ℝ) => R p i) (U ×ˢ Set.Ioi 0)) (hcone : ∀ p ∈ U ×ˢ Set.Ioi 0, SmoothCovariance.StrictCone (H p) (T p)) (hlower : WeightedQuotients.PolyBound (WeightedQuotients.edgeStrip U) S (fun (p : E × ℝ) => p.2⁻¹) fun (p : E × ℝ) => FlatCutoff.edge c p.2 / Matrix.mulVec (H p)⁻¹ (T p) j) (hYjets : WeightedQuotients.WeightedJets c U S fun (p : E × ℝ) => Matrix.mulVec (H p)⁻¹ (T p) j) (hRjets : WeightedQuotients.WeightedJets c U S fun (p : E × ℝ) => Matrix.mulVec (H p)⁻¹ (R p) j) : ContDiffOn ℝ (↑⊤) (extendedIncrement H T R j) (U ×ˢ Set.univ) ∧ WeightedQuotients.WeightedJets (c / 2) U S (extendedIncrement H T R j) ∧ ∀ (m : ℕ), ∀ x ∈ U, iteratedFDeriv ℝ m (extendedIncrement H T R j) (x, 0) = 0

Joint smoothness, every parameter jet, and zero tensors at the edge, from actual inverse-solve derivatives and the primary's weighted lower bound.

noncomputable def NavierStokes.SignedCovariance.maskedExtendedIncrement {E : Type u_1} (D : ℝ) (L : PartitionedCovariance.UnsignedLabel) (q : E × ℝ → ℝ) (x : E × ℝ → SlotColoring.Position) (H : E × ℝ → Mat2) (T R : E × ℝ → Vec2) (j : Fin 2) (p : E × ℝ) : ℝ

Masked extended increment, given by mask D L (q p) (x p) * extendedIncrement H T R j p.

Equations

• NavierStokes.SignedCovariance.maskedExtendedIncrement D L q x H T R j p = NavierStokes.PartitionedCovariance.mask D L (q p) (x p) * NavierStokes.SignedCovariance.extendedIncrement H T R j p

theorem NavierStokes.SignedCovariance.physical_mask_smooth (D : ℝ) (L : PartitionedCovariance.UnsignedLabel) : ContDiff ℝ ↑⊤ fun (p : ℝ × SlotColoring.Position) => PartitionedCovariance.mask D L p.1 p.2

theorem NavierStokes.SignedCovariance.physical_mask_compactSupport (D : ℝ) (L : PartitionedCovariance.UnsignedLabel) (hL : 1 ≤ L.1) : HasCompactSupport fun (p : ℝ × SlotColoring.Position) => PartitionedCovariance.mask D L p.1 p.2

theorem NavierStokes.SignedCovariance.masked_physical_coefficient_compactSupport (D : ℝ) (L : PartitionedCovariance.UnsignedLabel) (hL : 1 ≤ L.1) (f : ℝ × SlotColoring.Position → ℝ) : HasCompactSupport fun (p : ℝ × SlotColoring.Position) => PartitionedCovariance.mask D L p.1 p.2 * f p

theorem NavierStokes.SignedCovariance.masked_physical_coefficients_locallyFinite (D : ℝ) (N : ℕ) (f : PartitionedCovariance.UnsignedLabel → ↑(Set.Ioi 0) × SlotColoring.Position → ℝ) : LocallyFinite fun (L : PartitionedCovariance.UnsignedLabel) => Function.support fun (p : ↑(Set.Ioi 0) × SlotColoring.Position) => PartitionedCovariance.mask D (PartitionedCovariance.tailLabel N L) (↑p.1) p.2 * f L p

theorem NavierStokes.SignedCovariance.masked_physical_jet_support (D : ℝ) (L : PartitionedCovariance.UnsignedLabel) (f : ℝ × SlotColoring.Position → ℝ) (m : ℕ) : tsupport (iteratedFDeriv ℝ m fun (p : ℝ × SlotColoring.Position) => PartitionedCovariance.mask D L p.1 p.2 * f p) ⊆ tsupport fun (p : ℝ × SlotColoring.Position) => PartitionedCovariance.mask D L p.1 p.2

theorem NavierStokes.SignedCovariance.maskedExtendedIncrement_smooth {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (D : ℝ) (L : PartitionedCovariance.UnsignedLabel) {U : Set E} {q : E × ℝ → ℝ} {x : E × ℝ → SlotColoring.Position} {H : E × ℝ → Mat2} {T R : E × ℝ → Vec2} (j : Fin 2) (hq : ContDiffOn ℝ (↑⊤) q (U ×ˢ Set.univ)) (hx : ContDiffOn ℝ (↑⊤) x (U ×ˢ Set.univ)) (he : ContDiffOn ℝ (↑⊤) (extendedIncrement H T R j) (U ×ˢ Set.univ)) : ContDiffOn ℝ (↑⊤) (maskedExtendedIncrement D L q x H T R j) (U ×ˢ Set.univ)

theorem NavierStokes.SignedCovariance.maskedExtendedIncrement_support {E : Type u_1} (D : ℝ) (L : PartitionedCovariance.UnsignedLabel) (q : E × ℝ → ℝ) (x : E × ℝ → SlotColoring.Position) (H : E × ℝ → Mat2) (T R : E × ℝ → Vec2) (j : Fin 2) : Function.support (maskedExtendedIncrement D L q x H T R j) ⊆ {p : E × ℝ | PartitionedCovariance.mask D L (q p) (x p) ≠ 0 ∧ 0 < p.2 ∧ Matrix.mulVec (H p)⁻¹ (R p) j ≠ 0}

The signed update cannot create support outside the original mask or on the zero side of the edge. Its inverse numerator also controls support.