High-contrast homogenization: Provider.Quenched.UnitRangeCellProbability

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

The probabilistic normalized cell estimate

The unit-range concentration bound is applied at a shifted parameter so that the finite block-entry union bound is absorbed into the Gaussian gauge.

noncomputable def HCPolySupport.HighContrast.Quenched.unitRangeRenormShift (d : ℕ) : ℝ

The dimensional parameter shift absorbing whole-block reassembly.

Equations

• HCPolySupport.HighContrast.Quenched.unitRangeRenormShift d = Real.log (4 * ↑d ^ 2 + 1) / (2 * HCPolySupport.HighContrast.Quenched.frGaugeConst d)

theorem HCPolySupport.HighContrast.Quenched.unitRangeRenormShift_nonneg (d : ℕ) : 0 ≤ unitRangeRenormShift d