High-contrast homogenization: Provider.Transport.WhitneyFilling

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

The maximal filling of a target by the cells of a second grid

The filling family 𝒱_a(W;q) of l.two.grid.whitney(i): among the aligned q-cells of scale a ≤ n, the selected ones are those contained in the target W whose aligned parent of scale a+1 is not, together with all the scale-n cells contained in W. This is the family the cross-grid rows e.two.grid.whitney.volumes and the finite cross-grid exhaustion are indexed by, and the one the transport reads as 𝒱_r(W;q) in e.two.grid.whitney.average.

Three structural facts are proved here, all of them for an arbitrary target set. The selected cells are pairwise disjoint across all scales: a finer selected cell inside a coarser one would have its parent inside the coarser one too, hence inside W, which the selection rule forbids. Each is contained in W by definition -- this is the containment convention the window hypothesis relies on, and it is a property of the construction rather than an arithmetic fact about triadic ratios. And each scale carries only finitely many selected cells, because a selected cell contains its own center, the centers of one scale form a lattice, and the target is bounded.

def HCPolySupport.HighContrast.Transport.fillingIndex {d : ℕ} (q : Mat d) (n : ℤ) (W : Set (Vec d)) (a : ℤ) : Set (Fin d → ℤ)

The maximal filling 𝒱_a(W;q) of l.two.grid.whitney(i), as the set of indices of the selected cells: an aligned q-cell of scale a ≤ n is selected when it is contained in the target W and either a = n or its aligned parent of scale a+1 is not contained in W.

Equations

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

theorem HCPolySupport.HighContrast.Transport.adaptedCellAt_subset_of_mem_fillingIndex {d : ℕ} {q : Mat d} {n a : ℤ} {W : Set (Vec d)} {w : Fin d → ℤ} (hw : w ∈ fillingIndex q n W a) : adaptedCellAt q a w ⊆ W

A selected cell is contained in the target.

theorem HCPolySupport.HighContrast.Transport.le_of_mem_fillingIndex {d : ℕ} {q : Mat d} {n a : ℤ} {W : Set (Vec d)} {w : Fin d → ℤ} (hw : w ∈ fillingIndex q n W a) : a ≤ n

A selected cell has a scale at most the starting scale of the filling.

The selected cells are pairwise disjoint

theorem HCPolySupport.HighContrast.Transport.disjoint_of_mem_fillingIndex {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {W : Set (Vec d)} {n a b : ℤ} {w v : Fin d → ℤ} (hw : w ∈ fillingIndex q n W a) (hv : v ∈ fillingIndex q n W b) (hne : (a, w) ≠ (b, v)) : Disjoint (adaptedCellAt q a w) (adaptedCellAt q b v)

The selected cells of the maximal filling are pairwise disjoint, across all scales: this is the disjointness clause of l.two.grid.whitney(i).

Each scale carries finitely many selected cells

theorem HCPolySupport.HighContrast.Transport.finite_fillingIndex {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {W : Set (Vec d)} (hW : IsBoundedDomain W) (n a : ℤ) : (fillingIndex q n W a).Finite

A scale of the maximal filling is finite. A selected cell contains its own center, so the selected indices of one scale are lattice points of a bounded region.

The selected ancestor of a cell contained in the target

theorem HCPolySupport.HighContrast.Transport.exists_mem_fillingIndex_of_subset {d : ℕ} {q : Mat d} {W : Set (Vec d)} {n J : ℤ} (hJn : J ≤ n) {w : Fin d → ℤ} (hw : adaptedCellAt q J w ⊆ W) : ∃ (b : ℕ), J + ↑b ≤ n ∧ gridParent^[b] w ∈ fillingIndex q n W (J + ↑b) ∧ adaptedCellAt q J w ⊆ adaptedCellAt q (J + ↑b) (gridParent^[b] w)

A cell contained in the target has a selected ancestor. Taking the coarsest ancestor still contained in W, within the scale range of the filling, produces a selected cell containing the given one: either that ancestor sits at the starting scale n, or its own parent escapes W. This is the step "let b be the largest scale in {J,…,n} such that C^{(b)} ⊆ W" of l.two.grid.whitney(i).