High-contrast homogenization: Provider.Quenched.RenormalizedRadiusFamilyVarying #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Generation-dependent renormalized-radius tails #
For a growing window the union-bound cardinality is absorbed jointly by the window's renormalization base and the fixed tail buffer. This retains the base factor that the fixed-window interface may harmlessly discard.
theorem
HCPolySupport.HighContrast.Quenched.measureReal_renormRadius_gt_le_varying
{d : ℕ}
{P : MeasureTheory.Measure (CoeffSpace d)}
[MeasureTheory.IsFiniteMeasure P]
{S : CoeffSpace d → ℝ}
{Ahat : BlockMat d}
{gamma nu mu rho delta Gain : ℝ}
{n l0 h b : ℕ}
(hAhat : Book.Ch02.BlockPosDef Ahat)
(hGain : 0 < Gain)
(hdelta : 0 ≤ delta)
(hmu : mu = nu - gamma)
(hmupos : 0 < mu)
(hgn : gamma ≤ nu)
(hrg : gamma ≤ rho)
(hl0 : 1 ≤ renormBase gamma nu mu delta Gain l0 h)
(hthr : Real.log 2 ≤ frGaugeConst d * renormBase gamma nu mu delta Gain l0 h ^ 2 * (3 ^ (2 * mu) - 1))
(hcell : HasCellRenormalization P S Ahat gamma nu Gain n l0 h)
(hb1 : 1 ≤ b)
(hh1 : 1 ≤ h)
(hbuf :
Real.log (2 * renormCellCount d h) ≤ frGaugeConst d * (renormBase gamma nu mu delta Gain l0 h ^ 2 * 3 ^ (2 * mu * ↑b) - 1))
(q : ℕ)
:
The shifted tail of a single member of a generation-dependent renormalized-radius family.