High-contrast homogenization: Provider.Window.BadScaleTiles #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
theorem
HCPolySupport.HighContrast.Window.ae_coarse_bound_all_translates
{d : ℕ}
{P : MeasureTheory.Measure (CoeffSpace d)}
(hstat : IsStationaryLaw P)
{g : ℝ}
{E : BlockMat d}
{Ψ : ℝ → ℝ}
{K : ℝ}
{S : CoeffSpace d → ℝ}
(hdag : CoarseEllipticityDagger P g E Ψ K S)
:
∀ᵐ (a : CoeffSpace d) ∂P, ∀ (v : Fin d → ℤ) (m : ℤ),
S (translateCoeff v a) ≤ 3 ^ m →
∀ k ≤ m,
∀ (w : Fin d → ℤ),
standardCellCenter k w ∈ centeredCube d m →
BlockMatLoewnerLE (coarseBlock (standardCell d k w) (translateCoeff v a))
(blockScale (3 ^ (g * (↑m - ↑k))) E)
The coarse ellipticity bound holds simultaneously after every integer translation of the sample.
theorem
HCPolySupport.HighContrast.Window.measureReal_badScaleEvent_le_tiles
{d : ℕ}
[NeZero d]
{P : MeasureTheory.Measure (CoeffSpace d)}
[MeasureTheory.IsProbabilityMeasure P]
(hstat : IsStationaryLaw P)
{g : ℝ}
{E : BlockMat d}
{Ψ : ℝ → ℝ}
{K : ℝ}
{S : CoeffSpace d → ℝ}
(hdag : CoarseEllipticityDagger P g E Ψ K S)
{h m : ℤ}
(hh0 : 0 ≤ h)
(hhm : h ≤ m)
:
A bad window scale is bounded by the union of the translated source tails over the aligned tiles of the window.