Leading covariance of actual partitioned, separated slot fields

The fields are periodized native pulse components times actual angular cosines. The off-diagonal label products vanish by the constructed rational slots, not by an independence assumption about their angular frequencies.

@[reducible, inline]

abbrev NavierStokes.PartitionedCovariance.Plane : Type

Plane: an abbreviation for TorusInverse.Plane.

Equations

• NavierStokes.PartitionedCovariance.Plane = NavierStokes.TorusInverse.Plane

@[reducible, inline]

abbrev NavierStokes.PartitionedCovariance.Vec2 : Type

Vec2: an abbreviation for SmoothCovariance.Vec2.

Equations

• NavierStokes.PartitionedCovariance.Vec2 = NavierStokes.SmoothCovariance.Vec2

@[reducible, inline]

abbrev NavierStokes.PartitionedCovariance.Mat2 : Type

Mat2: an abbreviation for SmoothCovariance.Mat2.

Equations

• NavierStokes.PartitionedCovariance.Mat2 = NavierStokes.SmoothCovariance.Mat2

noncomputable def NavierStokes.PartitionedCovariance.cutoff (r : ℝ) : ℝ → ℝ

Cutoff, given by SquaredPartition.gridMask r 0.

Equations

• NavierStokes.PartitionedCovariance.cutoff r = NavierStokes.SquaredPartition.gridMask r 0

theorem NavierStokes.PartitionedCovariance.cutoff_continuous (r : ℝ) : Continuous (cutoff r)

theorem NavierStokes.PartitionedCovariance.cutoff_compact {r : ℝ} (hr : 0 < r) : HasCompactSupport (cutoff r)

theorem NavierStokes.PartitionedCovariance.cutoff_support {r : ℝ} (hr : 0 < r) : Function.support (cutoff r) = Set.Ioo (-r) r

theorem NavierStokes.PartitionedCovariance.cutoff_sq_integral_pos {r : ℝ} (hr : 0 < r) : 0 < ∫ (ξ : ℝ), cutoff r ξ ^ 2

noncomputable def NavierStokes.PartitionedCovariance.nativePrefactor (vr vt : Plane) (r : ℝ) : ℝ

Native prefactor, given by (|vr.1 * vt.2 - vr.2 * vt.1| / 2) * ∫ ξ : ℝ, cutoff r ξ ^ 2.

Equations

• NavierStokes.PartitionedCovariance.nativePrefactor vr vt r = |vr.1 * vt.2 - vr.2 * vt.1| / 2 * ∫ (ξ : ℝ), NavierStokes.PartitionedCovariance.cutoff r ξ ^ 2

theorem NavierStokes.PartitionedCovariance.nativePrefactor_pos {vr vt : Plane} {r : ℝ} (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (hr : 0 < r) : 0 < nativePrefactor vr vt r

structure NavierStokes.PartitionedCovariance.Pulse : Type

The actual scalar radial and two tangent pulse components. All analytic hypotheses concern these functions, not their covariance integrals.

• ψ : ℝ → ℝ

  Ψ of Pulse, of type ℝ → ℝ.

• x : ℝ → ℝ

  X of Pulse, of type ℝ → ℝ.

• t : ℝ → Vec2

  T of Pulse, of type ℝ → Vec2.

• ψ_continuous : Continuous self.ψ
• x_continuous : Continuous self.x
• t_continuous : Continuous self.t
• ψ_compact : HasCompactSupport self.ψ

noncomputable def NavierStokes.PartitionedCovariance.Pulse.column (P : Pulse) (ci : ℝ) : Vec2

Column, given by PulseCovariance.actualColumn ci P.ψ P.x P.t.

Equations

• P.column ci = NavierStokes.PulseCovariance.actualColumn ci P.ψ P.x P.t

noncomputable def NavierStokes.PartitionedCovariance.Pulse.radialProfile (P : Pulse) (r : ℝ) (z : Plane) : ℝ

Radial profile, given by cutoff r z.1 * P.ψ z.2 * P.x z.2.

Equations

• P.radialProfile r z = NavierStokes.PartitionedCovariance.cutoff r z.1 * P.ψ z.2 * P.x z.2

noncomputable def NavierStokes.PartitionedCovariance.Pulse.tangentProfile (P : Pulse) (r : ℝ) (i : Fin 2) (z : Plane) : ℝ

Tangent profile, given by cutoff r z.1 * P.ψ z.2 * P.t z.2 i.

Equations

• P.tangentProfile r i z = NavierStokes.PartitionedCovariance.cutoff r z.1 * P.ψ z.2 * P.t z.2 i

noncomputable def NavierStokes.PartitionedCovariance.nativePulse (vr vt center : Plane) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (ci r : ℝ) (f : Plane → ℝ) : Plane → ℝ

Native pulse, given by TorusAverages.nativeField (TorusAverages.slotChart vr vt hdet) center (TorusAverages.transverseStretch ci r f).

Equations

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

noncomputable def NavierStokes.PartitionedCovariance.covered (n : ℕ) (f : Plane → ℝ) (Y : Plane) : ℝ

Covered, given by TorusAverages.periodize f (TorusAverages.covering^[n] Y).

Equations

• NavierStokes.PartitionedCovariance.covered n f Y = NavierStokes.TorusAverages.periodize f (NavierStokes.TorusAverages.covering^[n] Y)

noncomputable def NavierStokes.PartitionedCovariance.wave (amplitude : ℝ) (n : ℕ) (f : Plane → ℝ) (mode : ℤ) (phase : Plane → ℝ) (Y : Plane) (θ : ℝ) : ℝ

Wave, given by amplitude * covered n f Y * Real.cos ((mode : ℝ) * θ + phase Y).

Equations

• NavierStokes.PartitionedCovariance.wave amplitude n f mode phase Y θ = amplitude * NavierStokes.PartitionedCovariance.covered n f Y * Real.cos (↑mode * θ + phase Y)

noncomputable def NavierStokes.PartitionedCovariance.doubleAverage (f : Plane → ℝ → ℝ) : ℝ

Double average, given by TorusAverages.squareAverage (fun Y => SmoothLoop.angularMean (f Y)).

Equations

• NavierStokes.PartitionedCovariance.doubleAverage f = NavierStokes.TorusAverages.squareAverage fun (Y : NavierStokes.TorusInverse.Plane) => NavierStokes.SmoothLoop.angularMean (f Y)

theorem NavierStokes.PartitionedCovariance.doubleAverage_const_mul (a : ℝ) (f : Plane → ℝ → ℝ) : (doubleAverage fun (Y : Plane) (θ : ℝ) => a * f Y θ) = a * doubleAverage f

theorem NavierStokes.PartitionedCovariance.nativePulse_mul (vr vt center : Plane) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (ci r : ℝ) (f g : Plane → ℝ) : (fun (Y : Plane) => nativePulse vr vt center hdet ci r f Y * nativePulse vr vt center hdet ci r g Y) = nativePulse vr vt center hdet ci r fun (z : Plane) => f z * g z

theorem NavierStokes.PartitionedCovariance.Pulse.profile_product (P : Pulse) (r : ℝ) (i : Fin 2) : (fun (z : Plane) => P.radialProfile r z * P.tangentProfile r i z) = TorusAverages.pulseProfile (cutoff r) P.ψ P.x P.t i

theorem NavierStokes.PartitionedCovariance.Pulse.wave_covariance (P : Pulse) (vr vt center : Plane) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (ci r : ℝ) (hci : 0 < ci) (hr : 0 < r) (S : Set Plane) (hS : Set.InjOn TorusAverages.quotientPoint S) (hR : Function.support (nativePulse vr vt center hdet ci r (P.radialProfile r)) ⊆ S) (hT : ∀ (i : Fin 2), Function.support (nativePulse vr vt center hdet ci r (P.tangentProfile r i)) ⊆ S) (a : ℝ) (n : ℕ) (phase : Plane → ℝ) (mode : ℤ) (hmode : mode ≠ 0) (i : Fin 2) : (doubleAverage fun (Y : Plane) (θ : ℝ) => wave a n (nativePulse vr vt center hdet ci r (P.radialProfile r)) mode phase Y θ * wave a n (nativePulse vr vt center hdet ci r (P.tangentProfile r i)) mode phase Y θ) = a ^ 2 * nativePrefactor vr vt r * P.column ci i

This evaluates the covariance of the two actual periodized velocity components. Slot injectivity removes all cross-copy terms before averaging.

theorem NavierStokes.PartitionedCovariance.cosine_actual_phase (k ε p pz x0 : ℝ) (F G : PhaseCalculus.Slow → ℝ) (s : PhaseCalculus.Slow) (v : Plane → ℝ) (mode : ℤ) (hmode : k * p = ↑mode) (Y : Plane) (θ : ℝ) : Real.cos (k * PhaseCalculus.phase ε p pz x0 F G (s, θ, v Y)) = Real.cos (↑mode * θ + k * (pz / ε * s.2.1 + x0 * s.1 - v Y * (p * F s + pz * G s)))

The free angular phase used above includes the manuscript's actual (26). The integer frequency is the actual nonzero rounded product k*p.

The actual rational slot system and vanishing cross-label products

theorem NavierStokes.PartitionedCovariance.cover_power_eq_iterate (n : ℕ) (Y : Plane) : (SlotGeometry.cover ^ n) Y = TorusAverages.covering^[n] Y

theorem NavierStokes.PartitionedCovariance.torusEq_lattice_add (k : TorusInverse.Frequency) (z : Plane) : SlotGeometry.torusEq z (TorusAverages.latticePoint k + z)

theorem NavierStokes.PartitionedCovariance.quotient_eq_torusEq {x y : Plane} (h : TorusAverages.quotientPoint x = TorusAverages.quotientPoint y) : SlotGeometry.torusEq x y

theorem NavierStokes.PartitionedCovariance.covered_support {f : Plane → ℝ} {S : Set Plane} (hf : Function.support f ⊆ S) (n : ℕ) : Function.support (covered n f) ⊆ SlotGeometry.liftedSupport n S

noncomputable def NavierStokes.PartitionedCovariance.slotCenter (h : ℝ) (L : SlotColoring.Label) : Plane

Slot center, given by SlotGeometry.center (Fintype.card SlotColoring.Palette) (SlotColoring.nativeGap h) (SlotColoring.color L).

Equations

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

noncomputable def NavierStokes.PartitionedCovariance.slotSet (h r : ℝ) (vr vt : Plane) (L : SlotColoring.Label) : Set Plane

Slot set, given by SlotGeometry.orientedRectangle (slotCenter h L) vr vt (2 * r).

Equations

• NavierStokes.PartitionedCovariance.slotSet h r vr vt L = NavierStokes.SlotGeometry.orientedRectangle (NavierStokes.PartitionedCovariance.slotCenter h L) vr vt (2 * r)

structure NavierStokes.PartitionedCovariance.SlotSystem (D h : ℝ) (vr vt : Plane) : Type

All separation and quotient-injectivity fields below are constructed by exists_slotSystem from the explicit rational centers.

• radius : ℝ

  Radius of SlotSystem, of type ℝ.

• radius_pos : 0 < self.radius
• injective (L : SlotColoring.Label) : Set.InjOn TorusAverages.quotientPoint (slotSet h self.radius vr vt L)
• disjoint (L M : SlotColoring.Label) : SlotColoring.Adj D L M → Disjoint (SlotGeometry.liftedSupport (SlotColoring.nativeIndex h L.1) (slotSet h self.radius vr vt L)) (SlotGeometry.liftedSupport (SlotColoring.nativeIndex h M.1) (slotSet h self.radius vr vt M))

theorem NavierStokes.PartitionedCovariance.exists_slotSystem (D h : ℝ) (hh : 0 ≤ h) (vr vt : Plane) : Nonempty (SlotSystem D h vr vt)

theorem NavierStokes.PartitionedCovariance.native_cutoff_support (vr vt center : Plane) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) {ci r : ℝ} (hci : 0 < ci) (hr : 0 < r) {ψ f : ℝ → ℝ} (hψ : Function.support ψ ⊆ Set.Icc 0 (2 * r / ci)) : Function.support (nativePulse vr vt center hdet ci r fun (z : Plane) => cutoff r z.1 * ψ z.2 * f z.2) ⊆ SlotGeometry.orientedRectangle center vr vt (2 * r)

The native cutoffs fit inside the padded rectangles used by the slot construction. Only support of the actual transverse cutoff is required.

noncomputable def NavierStokes.PartitionedCovariance.physicalMask (D : ℝ) (L : SlotColoring.Label) (q : ℝ) (x : SlotColoring.Position) : ℝ

Physical mask, given by SquaredPartition.dyadicMask (L.1 : ℤ) q * SquaredPartition.physicalSlowMask D L.1 L.2.1 x.

Equations

• NavierStokes.PartitionedCovariance.physicalMask D L q x = NavierStokes.SquaredPartition.dyadicMask (↑L.1) q * NavierStokes.SquaredPartition.physicalSlowMask D L.1 L.2.1 x

theorem NavierStokes.PartitionedCovariance.masks_force_adjacency {D q : ℝ} {x : SlotColoring.Position} {L M : SlotColoring.Label} (hq : 0 < q) (hL : 1 ≤ L.1) (hM : 1 ≤ M.1) (hne : L ≠ M) (hmL : physicalMask D L q x ≠ 0) (hmM : physicalMask D M q x ≠ 0) : SlotColoring.Adj D L M

theorem NavierStokes.PartitionedCovariance.SlotSystem.cross_product_zero {D h : ℝ} {vr vt : Plane} (sys : SlotSystem D h vr vt) {L M : SlotColoring.Label} (hL : 1 ≤ L.1) (hM : 1 ≤ M.1) (hne : L ≠ M) {f g : Plane → ℝ} (hf : Function.support f ⊆ slotSet h sys.radius vr vt L) (hg : Function.support g ⊆ slotSet h sys.radius vr vt M) {q : ℝ} (hq : 0 < q) (x : SlotColoring.Position) (Y : Plane) : physicalMask D L q x * covered (SlotColoring.nativeIndex h L.1) f Y * (physicalMask D M q x * covered (SlotColoring.nativeIndex h M.1) g Y) = 0

Actual pulse columns and the positive inverse solve

noncomputable def NavierStokes.PartitionedCovariance.tangentExtension {r a A b B c₀ s₀ slope E : ℝ} (P : PulseCovariance.TangentPulse r a A b B c₀ s₀ slope E) : ℝ → Vec2

Tangent extension, given by ParametricODE.extend (sq_nonneg r) ⟨fun v => P.tangent v, continuous_pi fun i => (P.tangent_continuous i).domRestrict⟩.

Equations

• NavierStokes.PartitionedCovariance.tangentExtension P = NavierStokes.ParametricODE.extend ⋯ { toFun := fun (v : ↑(Set.Icc 0 (r ^ 2))) => P.tangent ↑v, continuous_toFun := ⋯ }

theorem NavierStokes.PartitionedCovariance.tangentExtension_continuous {r a A b B c₀ s₀ slope E : ℝ} (P : PulseCovariance.TangentPulse r a A b B c₀ s₀ slope E) : Continuous (tangentExtension P)

theorem NavierStokes.PartitionedCovariance.tangentExtension_eq {r a A b B c₀ s₀ slope E : ℝ} (P : PulseCovariance.TangentPulse r a A b B c₀ s₀ slope E) {v : ℝ} (hv : v ∈ Set.Icc 0 (r ^ 2)) : tangentExtension P v = P.tangent v

noncomputable def NavierStokes.PartitionedCovariance.ofTangentPulse {r a A b B c₀ s₀ slope E : ℝ} (P : PulseCovariance.TangentPulse r a A b B c₀ s₀ slope E) : Pulse

Of tangent pulse, bundling ψ, x, t, ψ_continuous and the required compatibility proofs.

Equations

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

theorem NavierStokes.PartitionedCovariance.cutoff_zero_outside_slot {r a A b B c₀ s₀ slope E : ℝ} (P : PulseCovariance.TangentPulse r a A b B c₀ s₀ slope E) {v : ℝ} (hv : v ∉ Set.Icc 0 (r ^ 2)) : P.cutoff v = 0

theorem NavierStokes.PartitionedCovariance.ofTangentPulse_column {r a A b B c₀ s₀ slope E : ℝ} (P : PulseCovariance.TangentPulse r a A b B c₀ s₀ slope E) (ci : ℝ) : (ofTangentPulse P).column ci = PulseCovariance.actualColumn ci P.cutoff P.component P.tangent

Clamping the tangent component outside the pulse interval changes neither the cut-off velocity nor its actual covariance column.

theorem NavierStokes.PartitionedCovariance.ofTangentPulse_fits {r a A b B c₀ s₀ slope E ci r0 : ℝ} (P : PulseCovariance.TangentPulse r a A b B c₀ s₀ slope E) (hci : 0 < ci) (hfit : ci * r ^ 2 = 2 * r0) : Function.support (ofTangentPulse P).ψ ⊆ Set.Icc 0 (2 * r0 / ci)

noncomputable def NavierStokes.PartitionedCovariance.pairMatrix (vr vt : Plane) (r : ℝ) (ci : Vec2) (P : Fin 2 → Pulse) : Mat2

Pair matrix, defined pointwise by nativePrefactor vr vt r * (P j).column (ci j) i.

Equations

• NavierStokes.PartitionedCovariance.pairMatrix vr vt r ci P i j = NavierStokes.PartitionedCovariance.nativePrefactor vr vt r * (P j).column (ci j) i

theorem NavierStokes.PartitionedCovariance.pairMatrix_of_actual_pulses {r a A b B c₀ u E : ℝ} (P : PulseCovariance.SignedPulsePair r a A b B c₀ u E) (vr vt : Plane) (r0 : ℝ) (ci : Vec2) : (pairMatrix vr vt r0 ci fun (j : Fin 2) => ofTangentPulse (P j)) = PulseCovariance.actualMatrix P fun (j : Fin 2) => nativePrefactor vr vt r0 * ci j

theorem NavierStokes.PartitionedCovariance.pairMatrix_strictCone_of_actual {r a A b B c₀ u E r0 : ℝ} (P : PulseCovariance.SignedPulsePair r a A b B c₀ u E) {vr vt : Plane} (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (hr0 : 0 < r0) {ci : Vec2} (hci : ∀ (j : Fin 2), 0 < ci j) {T : Vec2} (hcone : SmoothCovariance.StrictCone (PulseCovariance.normalizedMatrix P) T) : SmoothCovariance.StrictCone (pairMatrix vr vt r0 ci fun (j : Fin 2) => ofTangentPulse (P j)) T

noncomputable def NavierStokes.PartitionedCovariance.amplitude (ε mask : ℝ) (H : Mat2) (T : Vec2) (j : Fin 2) : ℝ

Amplitude, given by Real.sqrt ε * SmoothCovariance.amplitudes H T j * mask.

Equations

• NavierStokes.PartitionedCovariance.amplitude ε mask H T j = √ε * NavierStokes.SmoothCovariance.amplitudes H T j * mask

theorem NavierStokes.PartitionedCovariance.amplitude_sq (ε mask : ℝ) (hε : 0 ≤ ε) (H : Mat2) (T : Vec2) (j : Fin 2) : amplitude ε mask H T j ^ 2 = ε * mask ^ 2 * SmoothCovariance.amplitudes H T j ^ 2

theorem NavierStokes.PartitionedCovariance.amplitudes_are_inverse_weights {H : Mat2} {T : Vec2} (h : SmoothCovariance.StrictCone H T) (j : Fin 2) : 0 < Matrix.mulVec H⁻¹ T j ∧ SmoothCovariance.amplitudes H T j = √(Matrix.mulVec H⁻¹ T j)

theorem NavierStokes.PartitionedCovariance.weighted_columns_reconstruct (ε mask : ℝ) (hε : 0 ≤ ε) {H : Mat2} {T : Vec2} (hcone : SmoothCovariance.StrictCone H T) (i : Fin 2) : ∑ j : Fin 2, amplitude ε mask H T j ^ 2 * H i j = ε * mask ^ 2 * T i

Finite sums of the actual velocity components

theorem NavierStokes.PartitionedCovariance.angularMean_sum {ι : Type u_1} (s : Finset ι) (f : ι → ℝ → ℝ) (hf : ∀ a ∈ s, Continuous (f a)) : (SmoothLoop.angularMean fun (θ : ℝ) => ∑ a ∈ s, f a θ) = ∑ a ∈ s, SmoothLoop.angularMean (f a)

theorem NavierStokes.PartitionedCovariance.squareAverage_sum {ι : Type u_1} (s : Finset ι) (f : ι → Plane → ℝ) (hf : ∀ a ∈ s, Continuous (f a)) : (TorusAverages.squareAverage fun (Y : TorusInverse.Plane) => ∑ a ∈ s, f a Y) = ∑ a ∈ s, TorusAverages.squareAverage (f a)

theorem NavierStokes.PartitionedCovariance.doubleAverage_sum {ι : Type u_1} (s : Finset ι) (f : ι → Plane → ℝ → ℝ) (hθ : ∀ a ∈ s, ∀ (Y : Plane), Continuous (f a Y)) (hY : ∀ a ∈ s, Continuous fun (Y : Plane) => SmoothLoop.angularMean (f a Y)) : (doubleAverage fun (Y : Plane) (θ : ℝ) => ∑ a ∈ s, f a Y θ) = ∑ a ∈ s, doubleAverage (f a)

theorem NavierStokes.PartitionedCovariance.sum_product_diagonal {ι : Type u_1} (s : Finset ι) (f g : ι → ℝ) (hcross : ∀ a ∈ s, ∀ b ∈ s, a ≠ b → f a * g b = 0) : (∑ a ∈ s, f a) * ∑ a ∈ s, g a = ∑ a ∈ s, f a * g a

theorem NavierStokes.PartitionedCovariance.Pulse.radialProfile_continuous (P : Pulse) (r : ℝ) : Continuous (P.radialProfile r)

theorem NavierStokes.PartitionedCovariance.Pulse.tangentProfile_continuous (P : Pulse) (r : ℝ) (i : Fin 2) : Continuous (P.tangentProfile r i)

theorem NavierStokes.PartitionedCovariance.Pulse.radialProfile_compact (P : Pulse) {r : ℝ} (hr : 0 < r) : HasCompactSupport (P.radialProfile r)

theorem NavierStokes.PartitionedCovariance.Pulse.tangentProfile_compact (P : Pulse) {r : ℝ} (hr : 0 < r) (i : Fin 2) : HasCompactSupport (P.tangentProfile r i)

theorem NavierStokes.PartitionedCovariance.nativePulse_continuous (vr vt center : Plane) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) {ci r : ℝ} (hci : ci ≠ 0) {f : Plane → ℝ} (hf : Continuous f) : Continuous (nativePulse vr vt center hdet ci r f)

theorem NavierStokes.PartitionedCovariance.nativePulse_compact (vr vt center : Plane) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) {ci r : ℝ} (hci : ci ≠ 0) {f : Plane → ℝ} (hf : HasCompactSupport f) : HasCompactSupport (nativePulse vr vt center hdet ci r f)

theorem NavierStokes.PartitionedCovariance.covered_continuous {f : Plane → ℝ} (hf : Continuous f) (hc : HasCompactSupport f) (n : ℕ) : Continuous (covered n f)

theorem NavierStokes.PartitionedCovariance.wave_continuous_theta (a : ℝ) (n : ℕ) (f : Plane → ℝ) (mode : ℤ) (phase : Plane → ℝ) (Y : Plane) : Continuous (wave a n f mode phase Y)

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

theorem NavierStokes.PartitionedCovariance.angularMean_wave_product_continuous (a : ℝ) (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 : Plane) => SmoothLoop.angularMean fun (θ : ℝ) => wave a n f mode phase Y θ * wave a n g mode phase Y θ

theorem NavierStokes.PartitionedCovariance.SlotSystem.wave_cross_zero {D h : ℝ} {vr vt : Plane} (sys : SlotSystem D h vr vt) {L M : SlotColoring.Label} (hL : 1 ≤ L.1) (hM : 1 ≤ M.1) (hne : L ≠ M) {f g : Plane → ℝ} (hf : Function.support f ⊆ slotSet h sys.radius vr vt L) (hg : Function.support g ⊆ slotSet h sys.radius vr vt M) {q : ℝ} (hq : 0 < q) (x : SlotColoring.Position) (Y : Plane) (θ a b : ℝ) (modeL modeM : ℤ) (phaseL phaseM : Plane → ℝ) : wave (a * physicalMask D L q x) (SlotColoring.nativeIndex h L.1) f modeL phaseL Y θ * wave (b * physicalMask D M q x) (SlotColoring.nativeIndex h M.1) g modeM phaseM Y θ = 0

@[reducible, inline]

abbrev NavierStokes.PartitionedCovariance.UnsignedLabel : Type

Unsigned label: an abbreviation for ℕ × SlotColoring.Grid.

Equations

• NavierStokes.PartitionedCovariance.UnsignedLabel = (ℕ × NavierStokes.SlotColoring.Grid)

noncomputable def NavierStokes.PartitionedCovariance.signedLabel (U : UnsignedLabel) (j : Fin 2) : SlotColoring.Label

Signed label, given by (U.1, U.2, if j = 0 then false else true).

Equations

• NavierStokes.PartitionedCovariance.signedLabel U j = (U.1, U.2, if j = 0 then false else true)

theorem NavierStokes.PartitionedCovariance.signedLabel_injective (U : UnsignedLabel) : Function.Injective (signedLabel U)

noncomputable def NavierStokes.PartitionedCovariance.mask (D : ℝ) (U : UnsignedLabel) (q : ℝ) (x : SlotColoring.Position) : ℝ

Mask, given by physicalMask D (signedLabel U 0) q x.

Equations

• NavierStokes.PartitionedCovariance.mask D U q x = NavierStokes.PartitionedCovariance.physicalMask D (NavierStokes.PartitionedCovariance.signedLabel U 0) q x

theorem NavierStokes.PartitionedCovariance.physicalMask_signedLabel (D : ℝ) (U : UnsignedLabel) (j : Fin 2) (q : ℝ) (x : SlotColoring.Position) : physicalMask D (signedLabel U j) q x = mask D U q x

structure NavierStokes.PartitionedCovariance.PairData {D h : ℝ} {vr vt : Plane} (sys : SlotSystem D h vr vt) (U : UnsignedLabel) : Type

Pair data, collecting pulses, ci, ci_pos, fits, modes, modes_ne and their compatibility conditions.

• pulses : Fin 2 → Pulse

  Pulses of PairData, of type Fin 2 → Pulse.

• ci : Vec2

  Ci of PairData, of type Vec2.

• ci_pos (j : Fin 2) : 0 < self.ci j
• fits (j : Fin 2) : Function.support (self.pulses j).ψ ⊆ Set.Icc 0 (2 * sys.radius / self.ci j)
• modes : Fin 2 → ℤ

  Modes of PairData, of type Fin 2 → ℤ.

• modes_ne (j : Fin 2) : self.modes j ≠ 0
• phases : Fin 2 → Plane → ℝ

  Phases of PairData, of type Fin 2 → Plane → ℝ.

noncomputable def NavierStokes.PartitionedCovariance.PairData.matrix {D h : ℝ} {vr vt : Plane} {sys : SlotSystem D h vr vt} {U : UnsignedLabel} (P : PairData sys U) : Mat2

Matrix, given by pairMatrix vr vt sys.radius P.ci P.pulses.

Equations

• P.matrix = NavierStokes.PartitionedCovariance.pairMatrix vr vt sys.radius P.ci P.pulses

noncomputable def NavierStokes.PartitionedCovariance.PairData.rawRadial {D h : ℝ} {vr vt : Plane} {sys : SlotSystem D h vr vt} {U : UnsignedLabel} (P : PairData sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (j : Fin 2) : Plane → ℝ

Raw radial, given by nativePulse vr vt (slotCenter h (signedLabel U j)) hdet (P.ci j) sys.radius ((P.pulses j).radialProfile sys.radius).

Equations

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

noncomputable def NavierStokes.PartitionedCovariance.PairData.rawTangent {D h : ℝ} {vr vt : Plane} {sys : SlotSystem D h vr vt} {U : UnsignedLabel} (P : PairData sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (j i : Fin 2) : Plane → ℝ

Raw tangent, given by nativePulse vr vt (slotCenter h (signedLabel U j)) hdet (P.ci j) sys.radius ((P.pulses j).tangentProfile sys.radius i).

Equations

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

theorem NavierStokes.PartitionedCovariance.PairData.rawRadial_support {D h : ℝ} {vr vt : Plane} {sys : SlotSystem D h vr vt} {U : UnsignedLabel} (P : PairData sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (j : Fin 2) : Function.support (P.rawRadial hdet j) ⊆ slotSet h sys.radius vr vt (signedLabel U j)

theorem NavierStokes.PartitionedCovariance.PairData.rawTangent_support {D h : ℝ} {vr vt : Plane} {sys : SlotSystem D h vr vt} {U : UnsignedLabel} (P : PairData sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (j i : Fin 2) : Function.support (P.rawTangent hdet j i) ⊆ slotSet h sys.radius vr vt (signedLabel U j)

theorem NavierStokes.PartitionedCovariance.PairData.rawRadial_continuous {D h : ℝ} {vr vt : Plane} {sys : SlotSystem D h vr vt} {U : UnsignedLabel} (P : PairData sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (j : Fin 2) : Continuous (P.rawRadial hdet j)

theorem NavierStokes.PartitionedCovariance.PairData.rawTangent_continuous {D h : ℝ} {vr vt : Plane} {sys : SlotSystem D h vr vt} {U : UnsignedLabel} (P : PairData sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (j i : Fin 2) : Continuous (P.rawTangent hdet j i)

theorem NavierStokes.PartitionedCovariance.PairData.rawRadial_compact {D h : ℝ} {vr vt : Plane} {sys : SlotSystem D h vr vt} {U : UnsignedLabel} (P : PairData sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (j : Fin 2) : HasCompactSupport (P.rawRadial hdet j)

theorem NavierStokes.PartitionedCovariance.PairData.rawTangent_compact {D h : ℝ} {vr vt : Plane} {sys : SlotSystem D h vr vt} {U : UnsignedLabel} (P : PairData sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (j i : Fin 2) : HasCompactSupport (P.rawTangent hdet j i)

theorem NavierStokes.PartitionedCovariance.SlotSystem.finite_wave_covariance {ι : Type u_1} {D h : ℝ} {vr vt : Plane} (sys : SlotSystem D h vr vt) (s : Finset ι) (label : ι → SlotColoring.Label) (hlabel : Set.InjOn label ↑s) (hlevel : ∀ a ∈ s, 1 ≤ (label a).1) (f g : ι → Plane → ℝ) (hf : ∀ a ∈ s, Function.support (f a) ⊆ slotSet h sys.radius vr vt (label a)) (hg : ∀ a ∈ s, Function.support (g a) ⊆ slotSet h sys.radius vr vt (label a)) (hfc : ∀ a ∈ s, Continuous (f a)) (hfs : ∀ a ∈ s, HasCompactSupport (f a)) (hgc : ∀ a ∈ s, Continuous (g a)) (hgs : ∀ a ∈ s, HasCompactSupport (g a)) (mode : ι → ℤ) (hmode : ∀ a ∈ s, mode a ≠ 0) (phase : ι → Plane → ℝ) (scale : ι → ℝ) {q : ℝ} (hq : 0 < q) (x : SlotColoring.Position) : (doubleAverage fun (Y : Plane) (θ : ℝ) => (∑ a ∈ s, wave (scale a * physicalMask D (label a) q x) (SlotColoring.nativeIndex h (label a).1) (f a) (mode a) (phase a) Y θ) * ∑ a ∈ s, wave (scale a * physicalMask D (label a) q x) (SlotColoring.nativeIndex h (label a).1) (g a) (mode a) (phase a) Y θ) = ∑ a ∈ s, doubleAverage fun (Y : Plane) (θ : ℝ) => wave (scale a * physicalMask D (label a) q x) (SlotColoring.nativeIndex h (label a).1) (f a) (mode a) (phase a) Y θ * wave (scale a * physicalMask D (label a) q x) (SlotColoring.nativeIndex h (label a).1) (g a) (mode a) (phase a) Y θ

A finite family with the actual physical masks and actual slot supports. All cross terms vanish pointwise, regardless of repeated angular modes.

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

Radial wave, constructed using wave.

Equations

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

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

Tangent wave, constructed using wave.

Equations

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

theorem NavierStokes.PartitionedCovariance.PairData.diagonal_covariance {D h : ℝ} {vr vt : Plane} {sys : SlotSystem D h vr vt} {U : UnsignedLabel} (P : PairData sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : ℝ) (T : Vec2) (q : ℝ) (x : SlotColoring.Position) (j i : Fin 2) : (doubleAverage fun (Y : Plane) (θ : ℝ) => P.radialWave hdet outer ε T q x j Y θ * P.tangentWave hdet outer ε T q x j i Y θ) = (outer * amplitude ε (mask D U q x) P.matrix T j) ^ 2 * P.matrix i j

theorem NavierStokes.PartitionedCovariance.PairData.diagonal_pair_reconstruct {D h : ℝ} {vr vt : Plane} {sys : SlotSystem D h vr vt} {U : UnsignedLabel} (P : PairData sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : ℝ) (hε : 0 ≤ ε) {T : Vec2} (hcone : SmoothCovariance.StrictCone P.matrix T) (q : ℝ) (x : SlotColoring.Position) (i : Fin 2) : (∑ j : Fin 2, doubleAverage fun (Y : Plane) (θ : ℝ) => P.radialWave hdet outer ε T q x j Y θ * P.tangentWave hdet outer ε T q x j i Y θ) = outer ^ 2 * ε * mask D U q x ^ 2 * T i

The actual physical partition and the physical covariance scale

theorem NavierStokes.PartitionedCovariance.mask_locallyFinite (D : ℝ) : LocallyFinite fun (U : UnsignedLabel) => Function.support fun (z : ↑(Set.Ioi 0) × SlotColoring.Position) => mask D U (↑z.1) z.2

noncomputable def NavierStokes.PartitionedCovariance.tailLabel (N : ℕ) (U : UnsignedLabel) : UnsignedLabel

Tail label, given by (U.1 + N, U.2).

Equations

• NavierStokes.PartitionedCovariance.tailLabel N U = (U.1 + N, U.2)

theorem NavierStokes.PartitionedCovariance.tailLabel_injective (N : ℕ) : Function.Injective (tailLabel N)

theorem NavierStokes.PartitionedCovariance.finite_active_masks (D : ℝ) (N : ℕ) {q : ℝ} (hq : 0 < q) (x : SlotColoring.Position) : (Function.support fun (U : UnsignedLabel) => mask D (tailLabel N U) q x).Finite

theorem NavierStokes.PartitionedCovariance.physical_mask_tail_sum_sq (D : ℝ) (N : ℕ) {q : ℝ} (hq : 0 < q) (hqN : q ≤ ChartScales.Q N) (x : SlotColoring.Position) : ∑ᶠ (U : UnsignedLabel), mask D (tailLabel N U) q x ^ 2 = 1

noncomputable def NavierStokes.PartitionedCovariance.velocityExponent (h : ℝ) : ℝ

Velocity exponent, given by 1 / 2 + h.

Equations

• NavierStokes.PartitionedCovariance.velocityExponent h = 1 / 2 + h

theorem NavierStokes.PartitionedCovariance.physical_scale_identity {Q q : ℝ} (hQ : 0 < Q) (hq : 0 < q) (h : ℝ) : (Q ^ (-velocityExponent h)) ^ 2 * Q ^ h * (Q / q) ^ (velocityExponent h + 1 / 2) = q ^ (-velocityExponent h - 1 / 2)

The exact scalar change from chart covariance to physical covariance. The chart target contains (Q/q)^(A+1/2) and A=1/2+h.

theorem NavierStokes.PartitionedCovariance.physical_viscosity_scale {Q : ℝ} (hQ : 0 < Q) (h : ℝ) : (Q ^ (-velocityExponent h)) ^ 2 * Q ^ h = Q ^ (-2 * velocityExponent h) * Q ^ h

noncomputable def NavierStokes.PartitionedCovariance.constructedSlotSystem (D h : ℝ) (hh : 0 ≤ h) (vr vt : Plane) : SlotSystem D h vr vt

Constructed slot system, given by Classical.choice (exists_slotSystem D h hh vr vt).

Equations

• NavierStokes.PartitionedCovariance.constructedSlotSystem D h hh vr vt = Classical.choice ⋯

noncomputable def NavierStokes.PartitionedCovariance.signedTailLabel (N : ℕ) (a : UnsignedLabel × Fin 2) : SlotColoring.Label

Signed tail label, given by signedLabel (tailLabel N a.1) a.2.

Equations

• NavierStokes.PartitionedCovariance.signedTailLabel N a = NavierStokes.PartitionedCovariance.signedLabel (NavierStokes.PartitionedCovariance.tailLabel N a.1) a.2

theorem NavierStokes.PartitionedCovariance.signedTailLabel_injective (N : ℕ) : Function.Injective (signedTailLabel N)

theorem NavierStokes.PartitionedCovariance.finite_pair_covariance {D h : ℝ} {vr vt : Plane} (sys : SlotSystem D h vr vt) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (N : ℕ) (hN : 1 ≤ N) (P : (U : UnsignedLabel) → PairData sys (tailLabel N U)) (outer ε : UnsignedLabel → ℝ) (T : UnsignedLabel → Vec2) (F : Finset UnsignedLabel) (hε : ∀ U ∈ F, 0 ≤ ε U) (hcone : ∀ U ∈ F, SmoothCovariance.StrictCone (P U).matrix (T U)) {q : ℝ} (hq : 0 < q) (x : SlotColoring.Position) (i : Fin 2) : (doubleAverage fun (Y : Plane) (θ : ℝ) => (∑ a ∈ F.product Finset.univ, (P a.1).radialWave hdet (outer a.1) (ε a.1) (T a.1) q x a.2 Y θ) * ∑ a ∈ F.product Finset.univ, (P a.1).tangentWave hdet (outer a.1) (ε a.1) (T a.1) q x a.2 i Y θ) = ∑ U ∈ F, outer U ^ 2 * ε U * mask D (tailLabel N U) q x ^ 2 * T U i

The complete finite-active-label formula, including both signs and every cross-label product. No pairwise distinction of angular frequencies is used.

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

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

Equations

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

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

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

Equations

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

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

At a fixed positive physical point the same finite active set works for every auxiliary point and angle. Thus no limit/interchange assumption enters the assembled covariance formula.

noncomputable def NavierStokes.PartitionedCovariance.physicalOuter (h : ℝ) (N : ℕ) (U : UnsignedLabel) : ℝ

Physical outer, given by ChartScales.Q (U.1 + N) ^ (-velocityExponent h).

Equations

• NavierStokes.PartitionedCovariance.physicalOuter h N U = NavierStokes.ChartScales.Q (U.1 + N) ^ (-NavierStokes.PartitionedCovariance.velocityExponent h)

noncomputable def NavierStokes.PartitionedCovariance.physicalViscosity (h : ℝ) (N : ℕ) (U : UnsignedLabel) : ℝ

Physical viscosity, given by ChartScales.epsilon h (U.1 + N).

Equations

• NavierStokes.PartitionedCovariance.physicalViscosity h N U = NavierStokes.ChartScales.epsilon h (U.1 + N)

noncomputable def NavierStokes.PartitionedCovariance.chartTarget (h q : ℝ) (N : ℕ) (T0 : Vec2) (U : UnsignedLabel) : Vec2

Chart target, given by (ChartScales.Q (U.1 + N) / q) ^ (velocityExponent h + 1 / 2) • T0.

Equations

• NavierStokes.PartitionedCovariance.chartTarget h q N T0 U = (NavierStokes.ChartScales.Q (U.1 + N) / q) ^ (NavierStokes.PartitionedCovariance.velocityExponent h + 1 / 2) • T0

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

Exact leading radial/tangential physical covariance of the assembled primary velocities. The matrix entries are the actual native pulse integrals, the masks are the constructed physical partitions, and the cross terms vanish by the constructed padded slots.

Instantiation by the actual pulse and rounding interfaces

noncomputable def NavierStokes.PartitionedCovariance.PairData.ofSignedPulses {D h : ℝ} {vr vt : Plane} (sys : SlotSystem D h vr vt) (U : UnsignedLabel) {r a A b B c₀ u E : ℝ} (pulses : PulseCovariance.SignedPulsePair r a A b B c₀ u E) (ci : Vec2) (hci : ∀ (j : Fin 2), 0 < ci j) (hfit : ∀ (j : Fin 2), ci j * r ^ 2 = 2 * sys.radius) (modes : Fin 2 → ℤ) (hmodes : ∀ (j : Fin 2), modes j ≠ 0) (phases : Fin 2 → Plane → ℝ) : PairData sys U

Of signed pulses, bundling pulses, ci, ci_pos, fits and the required compatibility proofs.

Equations

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

theorem NavierStokes.PartitionedCovariance.compact_actual_pair_strictCone {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) {vr vt : Plane} (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) {r0 : ℝ} (hr0 : 0 < r0) : ∃ (R : ℝ), 1 ≤ R ∧ ∀ p ∈ K, ∀ (r : ℝ), R ≤ r → ∀ (pulses : PulseCovariance.SignedPulsePair r a A b B (c₀ p) (u p) E) (ci : Vec2), (∀ (j : Fin 2), 0 < ci j) → SmoothCovariance.StrictCone (pairMatrix vr vt r0 ci fun (j : Fin 2) => ofTangentPulse (pulses j)) (Covariance.target (m p) (t p))

A compact strict-cone family yields one slot-length threshold for positive inverse weights of the actual integrated columns, including the native Haar and cosine prefactor. No model-column equality is assumed.

noncomputable def NavierStokes.PartitionedCovariance.roundedPhaseRemainder (k ε target pz x0 : ℝ) (F G : PhaseCalculus.Slow → ℝ) (s : PhaseCalculus.Slow) (v : Plane → ℝ) (Y : Plane) : ℝ

Rounded phase remainder, given by k * ((pz / ε) * s.2.1 + x0 * s.1 - v Y * (PhaseEstimates.roundedFrequency k target * F s + pz * G s)).

Equations

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

theorem NavierStokes.PartitionedCovariance.cosine_rounded_phase (k ε target pz x0 : ℝ) (hk : k ≠ 0) (F G : PhaseCalculus.Slow → ℝ) (s : PhaseCalculus.Slow) (v : Plane → ℝ) (Y : Plane) (θ : ℝ) : Real.cos (k * PhaseCalculus.phase ε (PhaseEstimates.roundedFrequency k target) pz x0 F G (s, θ, v Y)) = Real.cos (↑(PhaseEstimates.nonzeroRound (k * target)) * θ + roundedPhaseRemainder k ε target pz x0 F G s v Y)

theorem NavierStokes.PartitionedCovariance.rounded_phase_cos_sq_mean (k ε target pz x0 : ℝ) (hk : k ≠ 0) (F G : PhaseCalculus.Slow → ℝ) (s : PhaseCalculus.Slow) (v : Plane → ℝ) (Y : Plane) : (SmoothLoop.angularMean fun (θ : ℝ) => Real.cos (k * PhaseCalculus.phase ε (PhaseEstimates.roundedFrequency k target) pz x0 F G (s, θ, v Y)) ^ 2) = 1 / 2

theorem NavierStokes.PartitionedCovariance.actual_carrier_ne_zero (h : ℝ) (n : ℕ) : ↑(ChartScales.carrier h n) ≠ 0

theorem NavierStokes.PartitionedCovariance.actual_carrier_cos_sq_mean (h : ℝ) (n : ℕ) (target pz x0 : ℝ) (F G : PhaseCalculus.Slow → ℝ) (s : PhaseCalculus.Slow) (v : Plane → ℝ) (Y : Plane) : (SmoothLoop.angularMean fun (θ : ℝ) => Real.cos (↑(ChartScales.carrier h n) * PhaseCalculus.phase (ChartScales.epsilon h n) (PhaseEstimates.roundedFrequency (↑(ChartScales.carrier h n)) target) pz x0 F G (s, θ, v Y)) ^ 2) = 1 / 2