High-contrast homogenization: Provider.PolynomialHomogenization.RuledTriadicWhitneyCarrier

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

Disjoint triadic Whitney cells with an enlarged interior margin

The admissible cells are ordinary aligned triadic cells whose concentric ninefold dilation is contained in the domain. The selected cells are the maximal admissible cells. This is the standard disjoint triadic Whitney selection.

def HCPolySupport.HighContrast.enlargedMarginWhitneyInteriorBuffer {d : ℕ} (a : ℤ) (w : Fin d → ℤ) : Set (Vec d)

The concentric interior buffer of a triadic cell has nine times its side length.

Equations

• HCPolySupport.HighContrast.enlargedMarginWhitneyInteriorBuffer a w = HCPolySupport.Book.Ch03.openCubeAtScale (HCPolySupport.HighContrast.standardCellCenter a w) (a + 2)

def HCPolySupport.HighContrast.enlargedMarginWhitneyBoundaryBuffer {d : ℕ} (a : ℤ) (w : Fin d → ℤ) : Set (Vec d)

A factor-81 enlargement is sufficient to contain the interior buffer of the aligned parent.

Equations

• HCPolySupport.HighContrast.enlargedMarginWhitneyBoundaryBuffer a w = HCPolySupport.Book.Ch03.openCubeAtScale (HCPolySupport.HighContrast.standardCellCenter a w) (a + 4)

def HCPolySupport.HighContrast.IsEnlargedMarginWhitneyAdmissible {d : ℕ} (U : Set (Vec d)) (a : ℤ) (w : Fin d → ℤ) : Prop

An aligned triadic cell is admissible when its concentric ninefold enlargement lies in the domain.

Equations

• HCPolySupport.HighContrast.IsEnlargedMarginWhitneyAdmissible U a w = (HCPolySupport.HighContrast.enlargedMarginWhitneyInteriorBuffer a w ⊆ U)

def HCPolySupport.HighContrast.IsMaximalEnlargedMarginWhitneyCell {d : ℕ} (U : Set (Vec d)) (a : ℤ) (w : Fin d → ℤ) : Prop

A Whitney cell is an admissible triadic cell with no strictly larger admissible triadic cell containing it.

Equations

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

theorem HCPolySupport.HighContrast.standardCell_eq_openCubeAtScale {d : ℕ} (a : ℤ) (w : Fin d → ℤ) : standardCell d a w = Book.Ch03.openCubeAtScale (standardCellCenter a w) a

A standard cell is the arbitrary-center cube with its lattice center.

theorem HCPolySupport.HighContrast.standardCell_subset_enlargedMarginWhitneyInteriorBuffer {d : ℕ} (a : ℤ) (w : Fin d → ℤ) : standardCell d a w ⊆ enlargedMarginWhitneyInteriorBuffer a w

Every cell lies in its concentric ninefold enlargement.

theorem HCPolySupport.HighContrast.IsEnlargedMarginWhitneyAdmissible.cell_subset {d : ℕ} {U : Set (Vec d)} {a : ℤ} {w : Fin d → ℤ} (h : IsEnlargedMarginWhitneyAdmissible U a w) : standardCell d a w ⊆ U

Admissibility implies containment of the physical cell.

theorem HCPolySupport.HighContrast.finite_isMaximalEnlargedMarginWhitneyCell {d : ℕ} {U : Set (Vec d)} (hU : IsBoundedDomain U) (a : ℤ) : {w : Fin d → ℤ | IsMaximalEnlargedMarginWhitneyCell U a w}.Finite

At each scale the maximal admissible indices form a finite set.

theorem HCPolySupport.HighContrast.exists_maximalEnlargedMarginWhitneyCell_of_admissible {d : ℕ} (hd : 1 ≤ d) {U : Set (Vec d)} (hU : IsBoundedDomain U) {J : ℤ} {w : Fin d → ℤ} (hw : IsEnlargedMarginWhitneyAdmissible U J w) : ∃ (b : ℕ), IsMaximalEnlargedMarginWhitneyCell U (J + ↑b) (Transport.gridParent^[b] w) ∧ standardCell d J w ⊆ standardCell d (J + ↑b) (Transport.gridParent^[b] w)

Every admissible cell has a maximal admissible aligned ancestor.

theorem HCPolySupport.HighContrast.parentEnlargedMarginBuffer_subset_boundaryBuffer {d : ℕ} (a : ℤ) (w : Fin d → ℤ) : enlargedMarginWhitneyInteriorBuffer (a + 1) (Transport.gridParent w) ⊆ enlargedMarginWhitneyBoundaryBuffer a w

The interior buffer of the aligned parent lies in the factor-81 boundary buffer of the child.

structure HCPolySupport.HighContrast.EnlargedMarginRuledTriadicWhitneySystem {d : ℕ} (U : Set (Vec d)) (rho Rad : ℝ) : Type

The ruled carrier stores only the row function and its maximal-admissible characterization, together with the ball sandwich already carried by its consumers.

• center : Vec d

  Common center of the inner and outer balls bounding U.

• inner_ball : euclideanBallAt self.center rho ⊆ U
• outer_ball : U ⊆ euclideanBallAt self.center Rad
• rows : ℤ → Finset (Fin d → ℤ)

  Finite grid indices of the maximal cells satisfying the enlarged Whitney interior margin in each generation.

• rows_eq (a : ℤ) (w : Fin d → ℤ) : w ∈ self.rows a ↔ IsMaximalEnlargedMarginWhitneyCell U a w

theorem HCPolySupport.HighContrast.exists_enlargedMarginRuledTriadicWhitneySystem {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {rho Rad : ℝ} (hsand : HasBallSandwich U rho Rad) : Nonempty (EnlargedMarginRuledTriadicWhitneySystem U rho Rad)

The ruled carrier exists for every bounded domain with the supplied ball sandwich.

@[reducible, inline]

abbrev HCPolySupport.HighContrast.EnlargedMarginRuledTriadicWhitneySystem.CellIndex {d : ℕ} {U : Set (Vec d)} {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) : Type

The countable index of all selected Whitney cells.

Equations

• system.CellIndex = ((a : ℤ) × ↥(system.rows a))

def HCPolySupport.HighContrast.EnlargedMarginRuledTriadicWhitneySystem.scale {d : ℕ} {U : Set (Vec d)} {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (i : system.CellIndex) : ℤ

The scale of a selected Whitney cell.

Equations

• system.scale i = i.fst

def HCPolySupport.HighContrast.EnlargedMarginRuledTriadicWhitneySystem.index {d : ℕ} {U : Set (Vec d)} {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (i : system.CellIndex) : Fin d → ℤ

The lattice index of a selected Whitney cell.

Equations

• system.index i = ↑i.snd

def HCPolySupport.HighContrast.EnlargedMarginRuledTriadicWhitneySystem.cell {d : ℕ} {U : Set (Vec d)} {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (i : system.CellIndex) : Set (Vec d)

The selected physical cell.

Equations

• system.cell i = HCPolySupport.HighContrast.standardCell d (system.scale i) (system.index i)

def HCPolySupport.HighContrast.EnlargedMarginRuledTriadicWhitneySystem.interiorBuffer {d : ℕ} {U : Set (Vec d)} {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (i : system.CellIndex) : Set (Vec d)

The observation buffer contained in the domain.

Equations

• system.interiorBuffer i = HCPolySupport.HighContrast.enlargedMarginWhitneyInteriorBuffer (system.scale i) (system.index i)

def HCPolySupport.HighContrast.EnlargedMarginRuledTriadicWhitneySystem.boundaryBuffer {d : ℕ} {U : Set (Vec d)} {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (i : system.CellIndex) : Set (Vec d)

The fixed enlargement used to meet the boundary.

Equations

• system.boundaryBuffer i = HCPolySupport.HighContrast.enlargedMarginWhitneyBoundaryBuffer (system.scale i) (system.index i)

theorem HCPolySupport.HighContrast.EnlargedMarginRuledTriadicWhitneySystem.interiorBuffer_subset {d : ℕ} {U : Set (Vec d)} {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (i : system.CellIndex) : system.interiorBuffer i ⊆ U

Every selected cell has its observation buffer inside the domain.

theorem HCPolySupport.HighContrast.EnlargedMarginRuledTriadicWhitneySystem.cell_subset {d : ℕ} {U : Set (Vec d)} {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (i : system.CellIndex) : system.cell i ⊆ U

Every selected physical cell is contained in the domain.

theorem HCPolySupport.HighContrast.EnlargedMarginRuledTriadicWhitneySystem.pairwise_disjoint {d : ℕ} {U : Set (Vec d)} {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (i j : system.CellIndex) (hij : i ≠ j) : Disjoint (system.cell i) (system.cell j)

Distinct selected cells have disjoint interiors, even when their scales differ.

theorem HCPolySupport.HighContrast.EnlargedMarginRuledTriadicWhitneySystem.parent_not_admissible {d : ℕ} {U : Set (Vec d)} {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (i : system.CellIndex) : ¬IsEnlargedMarginWhitneyAdmissible U (system.scale i + 1) (Transport.gridParent (system.index i))

The aligned parent of a selected cell is not admissible.

theorem HCPolySupport.HighContrast.EnlargedMarginRuledTriadicWhitneySystem.boundaryBuffer_meets_frontier {d : ℕ} {U : Set (Vec d)} {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (i : system.CellIndex) : (system.boundaryBuffer i ∩ frontier U).Nonempty

Maximality makes the fixed factor-81 enlargement meet the boundary.

theorem HCPolySupport.HighContrast.EnlargedMarginRuledTriadicWhitneySystem.boundaryDistance_compare {d : ℕ} {U : Set (Vec d)} {rho Rad : ℝ} [NeZero d] (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (hU : IsOpen U) (i : system.CellIndex) {x : Vec d} (hx : x ∈ system.cell i) : (∀ y ∈ frontier U, 4 * 3 ^ system.scale i < euclideanDist x y) ∧ ∃ y ∈ frontier U, euclideanDist x y < 41 * √↑d * 3 ^ system.scale i

The ruled buffers compare the cell scale with point-to-boundary distance. The constants are the exact gap of the factor-9 inner buffer and the safe factor-81 outer enlargement.

theorem HCPolySupport.HighContrast.EnlargedMarginRuledTriadicWhitneySystem.ae_exhaustion {d : ℕ} {U : Set (Vec d)} {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (hd : 1 ≤ d) (hU : IsOpenBoundedConvexDomain U) : MeasureTheory.volume (U \ ⋃ (a : ℤ), ⋃ w ∈ ↑(system.rows a), standardCell d a w) = 0

The maximal admissible cells exhaust the open domain away from the countable union of triadic grid faces.