High-contrast homogenization: Entry.SourceWhitney

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

l.source.whitney

This file attaches the rounded-grid geometry theorem to the HCPoly/Entry/Statements/SourceWhitney.lean interface. It does not import or consume that statement.

theorem HCPolySupport.HighContrast.Entry.source_whitney (d : ℕ) (hd : 2 ≤ d) (jStar : ℕ) (hj : 2 * d ≤ 3 ^ jStar) (m : Mat d) (hm : Matrix.PosDef m) (j : ℤ) (y : Vec d) : (∀ p ∈ Geometry.maximalCellPairs (adaptedCellTranslate (Geometry.explicitRoundedGrid jStar m) j y) j, standardCell d p.1 p.2 ⊆ adaptedCellTranslate (Geometry.explicitRoundedGrid jStar m) j y) ∧ ((Geometry.maximalCellPairs (adaptedCellTranslate (Geometry.explicitRoundedGrid jStar m) j y) j).PairwiseDisjoint fun (p : ℤ × (Fin d → ℤ)) => standardCell d p.1 p.2) ∧ MeasureTheory.volume (adaptedCellTranslate (Geometry.explicitRoundedGrid jStar m) j y \ ⋃ p ∈ Geometry.maximalCellPairs (adaptedCellTranslate (Geometry.explicitRoundedGrid jStar m) j y) j, standardCell d p.1 p.2) = 0 ∧ ∀ r ≤ j, ∃ (hfin : (Geometry.maximalCellIndices (adaptedCellTranslate (Geometry.explicitRoundedGrid jStar m) j y) j r).Finite), ∑ w ∈ hfin.toFinset, (MeasureTheory.volume (standardCell d r w)).toReal / (MeasureTheory.volume (adaptedCellTranslate (Geometry.explicitRoundedGrid jStar m) j y)).toReal ≤ 12 * ↑d ^ (3 / 2) * 3 ^ (r - j)

Proof of l.source.whitney.

The statement carries the standing paper assumption hd : 2 <= d; the geometry theorem needs only the resulting local NeZero d instance.