High-contrast homogenization: Entry.TwoGridWhitney #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The two-grid Whitney lemma #
The type of l.two.grid.whitney.
The source-constant family is chosen before K₀; the geometric constant
is chosen before γ. The constant-one family only supplies the unused
standing threshold of this pure geometry theorem, not a stochastic source
estimate. No definition or selection rule is replaced.
theorem
HCPolySupport.HighContrast.Entry.two_grid_whitney
(d : ℕ)
(hd : 2 ≤ d)
:
∃ (Csrc : ℝ → ℝ),
(∀ γ ∈ Set.Ico 0 1, 0 < Csrc γ) ∧ ∀ (K₀ : ℝ),
1 ≤ K₀ →
∃ (C : ℝ),
0 < C ∧ ∀ γ ∈ Set.Ico 0 1,
∀ (K : ℝ),
1 < K →
∀ (jStar : ℕ),
2 * d ≤ 3 ^ jStar →
⌈Csrc γ * Real.logb 3 (2 * K)⌉ ≤ ↑jStar →
∀ (m m' : Mat d),
Matrix.PosDef m →
Matrix.PosDef m' →
gridRatio (Geometry.explicitRoundedGrid jStar m) (Geometry.explicitRoundedGrid jStar m') ≤ K₀ →
∀ (j : ℤ) (ℓ : ℕ),
1 ≤ ℓ →
(∀ y ∈ adaptedLatticeAtScale (Geometry.explicitRoundedGrid jStar m') j,
∃ (hfin :
∀ r ≤ j - ↑ℓ,
(maximalAdaptedCellCenters
(adaptedCellTranslate (Geometry.explicitRoundedGrid jStar m') j y)
(Geometry.explicitRoundedGrid jStar m) (j - ↑ℓ) r).Finite),
(∀ (r : ℤ) (w : Fin d → ℤ),
IsMaximalAdaptedCellIn
(adaptedCellTranslate (Geometry.explicitRoundedGrid jStar m') j y)
(Geometry.explicitRoundedGrid jStar m) (j - ↑ℓ) r w →
adaptedCellAtCenter (Geometry.explicitRoundedGrid jStar m) r w ⊆
adaptedCellTranslate (Geometry.explicitRoundedGrid jStar m') j y) ∧ ({p : ℤ × (Fin d → ℤ) | IsMaximalAdaptedCellIn
(adaptedCellTranslate (Geometry.explicitRoundedGrid jStar m') j y)
(Geometry.explicitRoundedGrid jStar m) (j - ↑ℓ) p.1
p.2}.PairwiseDisjoint
fun (p : ℤ × (Fin d → ℤ)) =>
adaptedCellAtCenter (Geometry.explicitRoundedGrid jStar m) p.1 p.2) ∧ MeasureTheory.volume
(adaptedCellTranslate (Geometry.explicitRoundedGrid jStar m') j y \ ⋃
p ∈
{p : ℤ × (Fin d → ℤ) | IsMaximalAdaptedCellIn
(adaptedCellTranslate
(Geometry.explicitRoundedGrid jStar m') j y)
(Geometry.explicitRoundedGrid jStar m) (j - ↑ℓ) p.1 p.2},
adaptedCellAtCenter (Geometry.explicitRoundedGrid jStar m) p.1
p.2) = 0 ∧ (∀ r ≤ j - ↑ℓ,
(MeasureTheory.volume
(adaptedCell (Geometry.explicitRoundedGrid jStar m)
r)).toReal / (MeasureTheory.volume
(adaptedCellTranslate
(Geometry.explicitRoundedGrid jStar m') j y)).toReal ≤ C * 3 ^ (-↑d * (↑j - ↑r))) ∧ ↑⋯.toFinset.card ≤ C * 3 ^ (↑d * ↑ℓ) ∧ (∀ (r : ℤ) (hr : r < j - ↑ℓ),
↑⋯.toFinset.card ≤ C * 3 ^ ((↑d - 1) * (↑j - ↑r))) ∧ ∑' (r : { r : ℤ // r ≤ j - ↑ℓ }), ∑ _z ∈ ⋯.toFinset,
(MeasureTheory.volume
(adaptedCell (Geometry.explicitRoundedGrid jStar m)
↑r)).toReal / (MeasureTheory.volume
(adaptedCellTranslate
(Geometry.explicitRoundedGrid jStar m') j
y)).toReal = 1 ∧ ∀ (r : ℤ) (hr : r < j - ↑ℓ),
∑ _z ∈ ⋯.toFinset,
(MeasureTheory.volume
(adaptedCell (Geometry.explicitRoundedGrid jStar m)
r)).toReal / (MeasureTheory.volume
(adaptedCellTranslate
(Geometry.explicitRoundedGrid jStar m') j
y)).toReal ≤ C * 3 ^ (↑r - ↑j)) ∧ ∀ y ∈ adaptedLatticeAtScale (Geometry.explicitRoundedGrid jStar m) j,
∃ (hfin :
∀ r ≤ j - ↑ℓ,
(maximalAdaptedCellCenters
(adaptedUncoveredPart
(adaptedCellTranslate (Geometry.explicitRoundedGrid jStar m) j y)
(Geometry.explicitRoundedGrid jStar m') (j - ↑ℓ))
(Geometry.explicitRoundedGrid jStar m) (j - ↑ℓ) r).Finite),
(∀ (r : ℤ) (w : Fin d → ℤ),
IsMaximalAdaptedCellIn
(adaptedUncoveredPart
(adaptedCellTranslate (Geometry.explicitRoundedGrid jStar m) j y)
(Geometry.explicitRoundedGrid jStar m') (j - ↑ℓ))
(Geometry.explicitRoundedGrid jStar m) (j - ↑ℓ) r w →
adaptedCellAtCenter (Geometry.explicitRoundedGrid jStar m) r w ⊆
adaptedUncoveredPart
(adaptedCellTranslate (Geometry.explicitRoundedGrid jStar m) j y)
(Geometry.explicitRoundedGrid jStar m') (j - ↑ℓ)) ∧ ({p : ℤ × (Fin d → ℤ) | IsMaximalAdaptedCellIn
(adaptedUncoveredPart
(adaptedCellTranslate (Geometry.explicitRoundedGrid jStar m) j
y)
(Geometry.explicitRoundedGrid jStar m') (j - ↑ℓ))
(Geometry.explicitRoundedGrid jStar m) (j - ↑ℓ) p.1
p.2}.PairwiseDisjoint
fun (p : ℤ × (Fin d → ℤ)) =>
adaptedCellAtCenter (Geometry.explicitRoundedGrid jStar m) p.1 p.2) ∧ MeasureTheory.volume
(adaptedCellTranslate (Geometry.explicitRoundedGrid jStar m) j y \ (adaptedCoveredPart
(adaptedCellTranslate (Geometry.explicitRoundedGrid jStar m) j
y)
(Geometry.explicitRoundedGrid jStar m') (j - ↑ℓ) ∪ ⋃
p ∈
{p : ℤ × (Fin d → ℤ) | IsMaximalAdaptedCellIn
(adaptedUncoveredPart
(adaptedCellTranslate
(Geometry.explicitRoundedGrid jStar m) j y)
(Geometry.explicitRoundedGrid jStar m') (j - ↑ℓ))
(Geometry.explicitRoundedGrid jStar m) (j - ↑ℓ) p.1
p.2},
adaptedCellAtCenter (Geometry.explicitRoundedGrid jStar m) p.1
p.2)) = 0 ∧ ∀ (r : ℤ) (hr : r ≤ j - ↑ℓ),
∑ _z ∈ ⋯.toFinset,
(MeasureTheory.volume
(adaptedCell (Geometry.explicitRoundedGrid jStar m)
r)).toReal / (MeasureTheory.volume
(adaptedCellTranslate (Geometry.explicitRoundedGrid jStar m)
j y)).toReal ≤ C * 3 ^ (↑r - ↑j)
Both Whitney constructions, with finite center rows, null exhaustion, the genuine infinite mass identity, and all printed bounds.