High-contrast homogenization: Provider.Window.Successor #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The strict successor gives the improved window discount #
If the strict successor of the bad scales is at most 3^m, then scale m
itself cannot be bad: otherwise its contribution, multiplied by the strict
factor three, would already exceed 3^m. Every entry in the defining
supremum is consequently at most one, which is exactly the printed Loewner
bound after undoing its triadic weight.
theorem
HCPolySupport.HighContrast.Window.improved_discount_of_successorScale_le
{d : ℕ}
{P : MeasureTheory.Measure (CoeffSpace d)}
{g : ℝ}
{E : BlockMat d}
{Ψ : ℝ → ℝ}
{K : ℝ}
{S : CoeffSpace d → ℝ}
(hdag : CoarseEllipticityDagger P g E Ψ K S)
{jStar M m : ℤ}
{a : CoeffSpace d}
(hsucc : successorScale g E (M - jStar) a ≤ ENNReal.ofReal (3 ^ m))
(k : ℤ)
:
k ≤ m →
∀ (w : Fin d → ℤ),
standardCellCenter k w ∈ centeredCube d m →
BlockMatLoewnerLE (coarseBlock (standardCell d k w) a) (blockScale (3 ^ (g * max (↑m - (↑M - ↑jStar) - ↑k) 0)) E)
A bound on the strict successor closes the pathwise improved-discount
clause of e.source.multiplier.