Concrete squared partitions on the line and on slow-coordinate grids

Integer translates of one compactly supported smooth bump are normalized by the square root of their locally finite sum of squares. Every object below is constructed; no partition-of-unity or derivative-bound hypothesis is assumed.

theorem NavierStokes.SquaredPartition.contDiff_finsum_of_locallyFinite {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ι → E → ℝ} (hf : ∀ (i : ι), ContDiff ℝ (↑⊤) (f i)) (hfin : LocallyFinite fun (i : ι) => Function.support (f i)) : ContDiff ℝ ↑⊤ fun (x : E) => ∑ᶠ (i : ι), f i x

A smooth locally finite sum is smooth. This elementary version uses finite sums on neighborhoods, so no uniform convergence premise is needed.

noncomputable def NavierStokes.SquaredPartition.bump : ContDiffBump 0

One fixed bump: equal to one on [-1/2,1/2], positive on (-1,1).

Equations

• NavierStokes.SquaredPartition.bump = { rIn := 1 / 2, rOut := 1, rIn_pos := NavierStokes.SquaredPartition.bump._proof_1, rIn_lt_rOut := NavierStokes.SquaredPartition.bump._proof_2 }

noncomputable def NavierStokes.SquaredPartition.translatedBump (k : ℤ) (x : ℝ) : ℝ

Translated bump, given by bump (x - k).

Equations

• NavierStokes.SquaredPartition.translatedBump k x = ↑NavierStokes.SquaredPartition.bump (x - ↑k)

theorem NavierStokes.SquaredPartition.translatedBump_nonneg (k : ℤ) (x : ℝ) : 0 ≤ translatedBump k x

theorem NavierStokes.SquaredPartition.translatedBump_smooth (k : ℤ) : ContDiff ℝ (↑⊤) (translatedBump k)

theorem NavierStokes.SquaredPartition.translatedBump_support (k : ℤ) : Function.support (translatedBump k) = Set.Ioo (↑k - 1) (↑k + 1)

theorem NavierStokes.SquaredPartition.integer_intervals_locallyFinite : LocallyFinite fun (k : ℤ) => Set.Icc (↑k - 1) (↑k + 1)

theorem NavierStokes.SquaredPartition.translatedBump_locallyFinite : LocallyFinite fun (k : ℤ) => Function.support (translatedBump k)

theorem NavierStokes.SquaredPartition.squaredBump_locallyFinite : LocallyFinite fun (k : ℤ) => Function.support fun (x : ℝ) => translatedBump k x ^ 2

noncomputable def NavierStokes.SquaredPartition.denominatorSquared (x : ℝ) : ℝ

Denominator squared, given by ∑ᶠ k : ℤ, translatedBump k x ^ 2.

Equations

• NavierStokes.SquaredPartition.denominatorSquared x = ∑ᶠ (k : ℤ), NavierStokes.SquaredPartition.translatedBump k x ^ 2

theorem NavierStokes.SquaredPartition.denominatorSquared_pos (x : ℝ) : 0 < denominatorSquared x

theorem NavierStokes.SquaredPartition.denominatorSquared_smooth : ContDiff ℝ (↑⊤) denominatorSquared

noncomputable def NavierStokes.SquaredPartition.lineMask (k : ℤ) (x : ℝ) : ℝ

Line mask, given by translatedBump k x / Real.sqrt (denominatorSquared x).

Equations

• NavierStokes.SquaredPartition.lineMask k x = NavierStokes.SquaredPartition.translatedBump k x / √(NavierStokes.SquaredPartition.denominatorSquared x)

theorem NavierStokes.SquaredPartition.lineMask_nonneg (k : ℤ) (x : ℝ) : 0 ≤ lineMask k x

theorem NavierStokes.SquaredPartition.lineMask_smooth (k : ℤ) : ContDiff ℝ (↑⊤) (lineMask k)

theorem NavierStokes.SquaredPartition.lineMask_support (k : ℤ) : Function.support (lineMask k) = Set.Ioo (↑k - 1) (↑k + 1)

theorem NavierStokes.SquaredPartition.lineMask_tsupport (k : ℤ) : tsupport (lineMask k) = Set.Icc (↑k - 1) (↑k + 1)

theorem NavierStokes.SquaredPartition.lineMask_compactSupport (k : ℤ) : HasCompactSupport (lineMask k)

theorem NavierStokes.SquaredPartition.lineMask_locallyFinite : LocallyFinite fun (k : ℤ) => tsupport (lineMask k)

theorem NavierStokes.SquaredPartition.lineMask_sum_sq (x : ℝ) : ∑ᶠ (k : ℤ), lineMask k x ^ 2 = 1

theorem NavierStokes.SquaredPartition.denominatorSquared_add_int (k : ℤ) (x : ℝ) : denominatorSquared (x + ↑k) = denominatorSquared x

theorem NavierStokes.SquaredPartition.denominatorSquared_sub_int (k : ℤ) (x : ℝ) : denominatorSquared (x - ↑k) = denominatorSquared x

theorem NavierStokes.SquaredPartition.lineMask_eq_translate (k : ℤ) (x : ℝ) : lineMask k x = lineMask 0 (x - ↑k)

All masks are translates of a single normalized profile.

noncomputable def NavierStokes.SquaredPartition.gridMask (δ : ℝ) (k : ℤ) (x : ℝ) : ℝ

Grid mask, given by lineMask k (x / δ).

Equations

• NavierStokes.SquaredPartition.gridMask δ k x = NavierStokes.SquaredPartition.lineMask k (x / δ)

theorem NavierStokes.SquaredPartition.gridMask_nonneg (δ : ℝ) (k : ℤ) (x : ℝ) : 0 ≤ gridMask δ k x

theorem NavierStokes.SquaredPartition.gridMask_smooth (δ : ℝ) (k : ℤ) : ContDiff ℝ (↑⊤) (gridMask δ k)

theorem NavierStokes.SquaredPartition.gridMask_sum_sq (δ x : ℝ) : ∑ᶠ (k : ℤ), gridMask δ k x ^ 2 = 1

theorem NavierStokes.SquaredPartition.gridMask_support (δ : ℝ) (hδ : 0 < δ) (k : ℤ) : Function.support (gridMask δ k) = Set.Ioo (δ * ↑k - δ) (δ * ↑k + δ)

theorem NavierStokes.SquaredPartition.gridMask_tsupport (δ : ℝ) (hδ : 0 < δ) (k : ℤ) : tsupport (gridMask δ k) = Set.Icc (δ * ↑k - δ) (δ * ↑k + δ)

theorem NavierStokes.SquaredPartition.gridMask_compactSupport (δ : ℝ) (hδ : 0 < δ) (k : ℤ) : HasCompactSupport (gridMask δ k)

theorem NavierStokes.SquaredPartition.gridMask_locallyFinite (δ : ℝ) : LocallyFinite fun (k : ℤ) => Function.support (gridMask δ k)

theorem NavierStokes.SquaredPartition.locallyFinite_iInter {ι : Type u_1} {κ : Type u_2} {X : Type u_3} [Finite ι] [TopologicalSpace X] {U : ι → κ → Set X} (h : ∀ (i : ι), LocallyFinite (U i)) : LocallyFinite fun (k : ι → κ) => ⋂ (i : ι), U i (k i)

A finite product of locally finite families is locally finite, with the whole tuple as index.

noncomputable def NavierStokes.SquaredPartition.productMask {d : ℕ} (δ : ℝ) (k : Fin d → ℤ) (x : Fin d → ℝ) : ℝ

Product mask, given by ∏ j, gridMask δ (k j) (x j).

Equations

• NavierStokes.SquaredPartition.productMask δ k x = ∏ j : Fin d, NavierStokes.SquaredPartition.gridMask δ (k j) (x j)

theorem NavierStokes.SquaredPartition.productMask_nonneg {d : ℕ} (δ : ℝ) (k : Fin d → ℤ) (x : Fin d → ℝ) : 0 ≤ productMask δ k x

theorem NavierStokes.SquaredPartition.productMask_smooth {d : ℕ} (δ : ℝ) (k : Fin d → ℤ) : ContDiff ℝ (↑⊤) (productMask δ k)

theorem NavierStokes.SquaredPartition.productMask_support {d : ℕ} (δ : ℝ) (k : Fin d → ℤ) : Function.support (productMask δ k) = ⋂ (j : Fin d), (fun (x : Fin d → ℝ) => x j) ⁻¹' Function.support (gridMask δ (k j))

theorem NavierStokes.SquaredPartition.productMask_locallyFinite {d : ℕ} (δ : ℝ) : LocallyFinite fun (k : Fin d → ℤ) => Function.support (productMask δ k)

theorem NavierStokes.SquaredPartition.productMask_tsupport_subset {d : ℕ} (δ : ℝ) (hδ : 0 < δ) (k : Fin d → ℤ) : tsupport (productMask δ k) ⊆ Set.univ.pi fun (j : Fin d) => Set.Icc (δ * ↑(k j) - δ) (δ * ↑(k j) + δ)

theorem NavierStokes.SquaredPartition.productMask_compactSupport {d : ℕ} (δ : ℝ) (hδ : 0 < δ) (k : Fin d → ℤ) : HasCompactSupport (productMask δ k)

theorem NavierStokes.SquaredPartition.productMask_sum_sq {d : ℕ} (δ : ℝ) (x : Fin d → ℝ) : ∑ᶠ (k : Fin d → ℤ), productMask δ k x ^ 2 = 1

theorem NavierStokes.SquaredPartition.exists_uniform_jet_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hc : HasCompactSupport f) (m : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ m f x‖ ≤ C

Compact smooth profiles have a finite bound at every fixed derivative order.

theorem NavierStokes.SquaredPartition.rescale_jet_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} (hf : ContDiff ℝ (↑⊤) f) {m : ℕ} {C : ℝ} (hC : ∀ (x : E), ‖iteratedFDeriv ℝ m f x‖ ≤ C) (a : ℝ) (c x : E) : ‖iteratedFDeriv ℝ m (fun (y : E) => f (a • y - c)) x‖ ≤ C * |a| ^ m

Full Fréchet jets of a translated rescaling cost one inverse scale per derivative, with no dependence on the translation.

theorem NavierStokes.SquaredPartition.gridMask_all_jet_bounds (m : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (δ : ℝ), 0 < δ → ∀ (k : ℤ) (x : ℝ), ‖iteratedFDeriv ℝ m (gridMask δ k) x‖ ≤ C / δ ^ m

theorem NavierStokes.SquaredPartition.productMask_eq_rescale {d : ℕ} (δ : ℝ) (k : Fin d → ℤ) (x : Fin d → ℝ) : productMask δ k x = productMask 1 0 (δ⁻¹ • x - fun (j : Fin d) => ↑(k j))

theorem NavierStokes.SquaredPartition.productMask_all_jet_bounds (d m : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (δ : ℝ), 0 < δ → ∀ (k : Fin d → ℤ) (x : Fin d → ℝ), ‖iteratedFDeriv ℝ m (productMask δ k) x‖ ≤ C / δ ^ m

noncomputable def NavierStokes.SquaredPartition.logCoordinate (q : ℝ) : ℝ

Log coordinate, given by -Real.log q / Real.log 2.

Equations

• NavierStokes.SquaredPartition.logCoordinate q = -Real.log q / Real.log 2

theorem NavierStokes.SquaredPartition.logCoordinate_window {q : ℝ} (hq : 0 < q) : logCoordinate q ∈ Set.Ioo (-1) 1 ↔ q ∈ Set.Ioo (1 / 2) 2

noncomputable def NavierStokes.SquaredPartition.dyadicProfile (q : ℝ) : ℝ

A single compact annular profile; its zero extension is smooth at zero.

Equations

• NavierStokes.SquaredPartition.dyadicProfile q = if 0 < q then NavierStokes.SquaredPartition.lineMask 0 (NavierStokes.SquaredPartition.logCoordinate q) else 0

theorem NavierStokes.SquaredPartition.dyadicProfile_nonneg (q : ℝ) : 0 ≤ dyadicProfile q

theorem NavierStokes.SquaredPartition.dyadicProfile_support : Function.support dyadicProfile = Set.Ioo (1 / 2) 2

theorem NavierStokes.SquaredPartition.dyadicProfile_zero_of_le_half {q : ℝ} (hq : q ≤ 1 / 2) : dyadicProfile q = 0

theorem NavierStokes.SquaredPartition.dyadicProfile_smooth : ContDiff ℝ (↑⊤) dyadicProfile

theorem NavierStokes.SquaredPartition.dyadicProfile_tsupport : tsupport dyadicProfile = Set.Icc (1 / 2) 2

theorem NavierStokes.SquaredPartition.dyadicProfile_compactSupport : HasCompactSupport dyadicProfile

noncomputable def NavierStokes.SquaredPartition.integerQ (n : ℤ) : ℝ

Integer Q, given by (2 : ℝ) ^ (-(n : ℝ)).

Equations

• NavierStokes.SquaredPartition.integerQ n = 2 ^ (-↑n)

theorem NavierStokes.SquaredPartition.integerQ_pos (n : ℤ) : 0 < integerQ n

theorem NavierStokes.SquaredPartition.log_integerQ (n : ℤ) : Real.log (integerQ n) = -↑n * Real.log 2

theorem NavierStokes.SquaredPartition.integerQ_nat (n : ℕ) : integerQ ↑n = ChartScales.Q n

noncomputable def NavierStokes.SquaredPartition.dyadicMask (n : ℤ) (q : ℝ) : ℝ

Dyadic mask, given by dyadicProfile (q / integerQ n).

Equations

• NavierStokes.SquaredPartition.dyadicMask n q = NavierStokes.SquaredPartition.dyadicProfile (q / NavierStokes.SquaredPartition.integerQ n)

theorem NavierStokes.SquaredPartition.dyadicMask_nonneg (n : ℤ) (q : ℝ) : 0 ≤ dyadicMask n q

theorem NavierStokes.SquaredPartition.dyadicMask_smooth (n : ℤ) : ContDiff ℝ (↑⊤) (dyadicMask n)

theorem NavierStokes.SquaredPartition.dyadicMask_eq_line (n : ℤ) {q : ℝ} (hq : 0 < q) : dyadicMask n q = lineMask n (logCoordinate q)

theorem NavierStokes.SquaredPartition.dyadicMask_support (n : ℤ) : Function.support (dyadicMask n) = Set.Ioo (integerQ n / 2) (2 * integerQ n)

theorem NavierStokes.SquaredPartition.dyadicMask_tsupport (n : ℤ) : tsupport (dyadicMask n) = Set.Icc (integerQ n / 2) (2 * integerQ n)

theorem NavierStokes.SquaredPartition.dyadicMask_compactSupport (n : ℤ) : HasCompactSupport (dyadicMask n)

theorem NavierStokes.SquaredPartition.dyadicMask_sum_sq {q : ℝ} (hq : 0 < q) : ∑ᶠ (n : ℤ), dyadicMask n q ^ 2 = 1

theorem NavierStokes.SquaredPartition.dyadicMask_locallyFinite : LocallyFinite fun (n : ℤ) => Function.support fun (q : ↑(Set.Ioi 0)) => dyadicMask n ↑q

Dyadic local finiteness holds on the positive q domain. The supports accumulate at zero, so no global local-finiteness claim is made there.

theorem NavierStokes.SquaredPartition.dyadicMask_all_jet_bounds (m : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℤ) (q : ℝ), ‖iteratedFDeriv ℝ m (dyadicMask n) q‖ ≤ C / integerQ n ^ m

theorem NavierStokes.SquaredPartition.dyadicMask_zero_of_neg {q : ℝ} (hq : 0 < q) (hq1 : q ≤ 1) {n : ℤ} (hn : n < 0) : dyadicMask n q = 0

theorem NavierStokes.SquaredPartition.dyadicMask_nat_sum_sq {q : ℝ} (hq : 0 < q) (hq1 : q ≤ 1) : ∑ᶠ (n : ℕ), dyadicMask (↑n) q ^ 2 = 1

Natural bands already form a partition on 0<q≤1.

theorem NavierStokes.SquaredPartition.integerQ_add (n m : ℤ) : integerQ (n + m) = integerQ n * integerQ m

theorem NavierStokes.SquaredPartition.dyadicMask_add (n m : ℤ) (q : ℝ) : dyadicMask (n + m) q = dyadicMask n (q / integerQ m)

theorem NavierStokes.SquaredPartition.dyadicMask_tail_sum_sq (N : ℕ) {q : ℝ} (hq : 0 < q) (hqN : q ≤ ChartScales.Q N) : ∑ᶠ (n : ℕ), dyadicMask (↑(n + N)) q ^ 2 = 1

After any chosen starting band, the retained bands partition the smaller active range 0<q≤Q_N. In particular one can retain only n≥4.

noncomputable def NavierStokes.SquaredPartition.nativeSpacing (n : ℕ) : ℝ

Native spacing, given by (ChartScales.S n ^ 3)⁻¹.

Equations

• NavierStokes.SquaredPartition.nativeSpacing n = (NavierStokes.ChartScales.S n ^ 3)⁻¹

theorem NavierStokes.SquaredPartition.nativeSpacing_pos {n : ℕ} (hn : 1 ≤ n) : 0 < nativeSpacing n

noncomputable def NavierStokes.SquaredPartition.slowMask (n : ℕ) (k : SlotColoring.Grid) (x : SlotColoring.Position) : ℝ

The actual three-coordinate partition at slow mesh S_n^(-3).

Equations

• NavierStokes.SquaredPartition.slowMask n k x = NavierStokes.SquaredPartition.productMask (NavierStokes.SquaredPartition.nativeSpacing n) k x

theorem NavierStokes.SquaredPartition.slowMask_nonneg (n : ℕ) (k : SlotColoring.Grid) (x : SlotColoring.Position) : 0 ≤ slowMask n k x

theorem NavierStokes.SquaredPartition.slowMask_smooth (n : ℕ) (k : SlotColoring.Grid) : ContDiff ℝ (↑⊤) (slowMask n k)

theorem NavierStokes.SquaredPartition.slowMask_sum_sq (n : ℕ) (x : SlotColoring.Position) : ∑ᶠ (k : SlotColoring.Grid), slowMask n k x ^ 2 = 1

theorem NavierStokes.SquaredPartition.slowMask_locallyFinite (n : ℕ) : LocallyFinite fun (k : SlotColoring.Grid) => tsupport (slowMask n k)

theorem NavierStokes.SquaredPartition.slowMask_compactSupport {n : ℕ} (hn : 1 ≤ n) (k : SlotColoring.Grid) : HasCompactSupport (slowMask n k)

theorem NavierStokes.SquaredPartition.slowMask_tsupport_subset {n : ℕ} (hn : 1 ≤ n) (k : SlotColoring.Grid) : tsupport (slowMask n k) ⊆ Set.univ.pi fun (j : Fin 3) => Set.Icc (nativeSpacing n * ↑(k j) - nativeSpacing n) (nativeSpacing n * ↑(k j) + nativeSpacing n)

theorem NavierStokes.SquaredPartition.slowMask_jet_tsupport_subset {n : ℕ} (hn : 1 ≤ n) (k : SlotColoring.Grid) (m : ℕ) : tsupport (iteratedFDeriv ℝ m (slowMask n k)) ⊆ Set.univ.pi fun (j : Fin 3) => Set.Icc (nativeSpacing n * ↑(k j) - nativeSpacing n) (nativeSpacing n * ↑(k j) + nativeSpacing n)

theorem NavierStokes.SquaredPartition.slowMask_all_jet_bounds (m : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ), 1 ≤ n → ∀ (k : SlotColoring.Grid) (x : SlotColoring.Position), ‖iteratedFDeriv ℝ m (slowMask n k) x‖ ≤ C * ChartScales.S n ^ (3 * m)

Every fixed jet costs the fixed power S^(3m), uniformly in all grid nodes.

noncomputable def NavierStokes.SquaredPartition.slowCoordinates (D : ℝ) (n : ℕ) (x : SlotColoring.Position) : SlotColoring.Position

The manuscript's three physical-to-slow coordinate rescalings.

Equations

• NavierStokes.SquaredPartition.slowCoordinates D n x j = x j / NavierStokes.ChartScales.Q n ^ NavierStokes.SlotColoring.axisExponent D j

theorem NavierStokes.SquaredPartition.slowCoordinates_smooth (D : ℝ) (n : ℕ) : ContDiff ℝ (↑⊤) (slowCoordinates D n)

noncomputable def NavierStokes.SquaredPartition.physicalSlowMask (D : ℝ) (n : ℕ) (k : SlotColoring.Grid) (x : SlotColoring.Position) : ℝ

Physical slow mask, given by slowMask n k (slowCoordinates D n x).

Equations

• NavierStokes.SquaredPartition.physicalSlowMask D n k x = NavierStokes.SquaredPartition.slowMask n k (NavierStokes.SquaredPartition.slowCoordinates D n x)

theorem NavierStokes.SquaredPartition.physicalSlowMask_smooth (D : ℝ) (n : ℕ) (k : SlotColoring.Grid) : ContDiff ℝ (↑⊤) (physicalSlowMask D n k)

theorem NavierStokes.SquaredPartition.physicalSlowMask_sum_sq (D : ℝ) (n : ℕ) (x : SlotColoring.Position) : ∑ᶠ (k : SlotColoring.Grid), physicalSlowMask D n k x ^ 2 = 1

theorem NavierStokes.SquaredPartition.physicalSlowMask_locallyFinite (D : ℝ) (n : ℕ) : LocallyFinite fun (k : SlotColoring.Grid) => Function.support (physicalSlowMask D n k)

theorem NavierStokes.SquaredPartition.physicalSlowMask_tsupport_smallBox (D : ℝ) {n : ℕ} (hn : 1 ≤ n) (k : SlotColoring.Grid) : tsupport (physicalSlowMask D n k) ⊆ Set.univ.pi fun (j : Fin 3) => Set.Icc (SlotColoring.width D j n * ↑(k j) - SlotColoring.width D j n) (SlotColoring.width D j n * ↑(k j) + SlotColoring.width D j n)

theorem NavierStokes.SquaredPartition.physicalSlowMask_compactSupport (D : ℝ) {n : ℕ} (hn : 1 ≤ n) (k : SlotColoring.Grid) : HasCompactSupport (physicalSlowMask D n k)

theorem NavierStokes.SquaredPartition.physicalSlowMask_tsupport_subset_physicalBox (D : ℝ) {n : ℕ} (hn : 1 ≤ n) (k : SlotColoring.Grid) (sign : Bool) : tsupport (physicalSlowMask D n k) ⊆ SlotColoring.physicalBox D (n, k, sign)

The constructed masks fit inside the exact enlarged boxes already colored in SlotColoring, for either pulse sign.

theorem NavierStokes.SquaredPartition.physicalSlowMask_jet_tsupport_subset_physicalBox (D : ℝ) {n : ℕ} (hn : 1 ≤ n) (k : SlotColoring.Grid) (sign : Bool) (m : ℕ) : tsupport (iteratedFDeriv ℝ m (physicalSlowMask D n k)) ⊆ SlotColoring.physicalBox D (n, k, sign)

noncomputable def NavierStokes.SquaredPartition.labelMask (n : ℕ) (k : SlotColoring.Grid) (p : ℝ × SlotColoring.Position) : ℝ

Label mask, given by dyadicMask (n : ℤ) p.1 * slowMask n k p.2.

Equations

• NavierStokes.SquaredPartition.labelMask n k p = NavierStokes.SquaredPartition.dyadicMask (↑n) p.1 * NavierStokes.SquaredPartition.slowMask n k p.2

theorem NavierStokes.SquaredPartition.labelMask_nonneg (n : ℕ) (k : SlotColoring.Grid) (p : ℝ × SlotColoring.Position) : 0 ≤ labelMask n k p

theorem NavierStokes.SquaredPartition.labelMask_smooth (n : ℕ) (k : SlotColoring.Grid) : ContDiff ℝ (↑⊤) (labelMask n k)

theorem NavierStokes.SquaredPartition.labelMask_compactSupport {n : ℕ} (hn : 1 ≤ n) (k : SlotColoring.Grid) : HasCompactSupport (labelMask n k)

theorem NavierStokes.SquaredPartition.locallyFinite_pair_inter {ι : Type u_1} {κ : Type u_2} {X : Type u_3} [TopologicalSpace X] {U : ι → Set X} {V : ι → κ → Set X} (hU : LocallyFinite U) (hV : ∀ (i : ι), LocallyFinite (V i)) : LocallyFinite fun (p : ι × κ) => U p.1 ∩ V p.1 p.2

theorem NavierStokes.SquaredPartition.labelMask_locallyFinite : LocallyFinite fun (p : ℕ × SlotColoring.Grid) => Function.support fun (z : ↑(Set.Ioi 0) × SlotColoring.Position) => labelMask p.1 p.2 (↑z.1, z.2)

theorem NavierStokes.SquaredPartition.finsum_pair_eq {ι : Type u_1} {κ : Type u_2} {f : ι × κ → ℝ} (hf : (Function.support f).Finite) : ∑ᶠ (p : ι × κ), f p = ∑ᶠ (i : ι) (k : κ), f (i, k)

Finite support makes an ordinary sum over pairs equal its iterated sum.

theorem NavierStokes.SquaredPartition.labelMask_tail_sum_sq (N : ℕ) {p : ℝ × SlotColoring.Position} (hq : 0 < p.1) (hqN : p.1 ≤ ChartScales.Q N) : ∑ᶠ (n : ℕ) (k : SlotColoring.Grid), labelMask (n + N) k p ^ 2 = 1

The exact normalized squared partition obtained by multiplying dyadic and slow-grid masks; any lower band cutoff can be imposed by shrinking q.

theorem NavierStokes.SquaredPartition.labelMask_tail_total_sum_sq (N : ℕ) {p : ℝ × SlotColoring.Position} (hq : 0 < p.1) (hqN : p.1 ≤ ChartScales.Q N) : ∑ᶠ (a : ℕ × SlotColoring.Grid), labelMask (a.1 + N) a.2 p ^ 2 = 1