High-contrast homogenization: Provider.Quenched.RebaseSourceHalf #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Source burn-in for the one-time rebase #
theorem
HCPolySupport.HighContrast.Quenched.inv_gauge_at_entry_add_bracket_le_half
{d : ℕ}
[NeZero d]
{P : MeasureTheory.Measure (CoeffSpace d)}
[MeasureTheory.IsProbabilityMeasure P]
{g : ℝ}
{E : BlockMat d}
{Psi : ℝ → ℝ}
{K : ℝ}
{S : CoeffSpace d → ℝ}
(hdag : CoarseEllipticityDagger P g E Psi K S)
{mEnt q : ℕ}
(hq : (2 + aspectRatio E * K) ^ 2 ≤ 3 ^ ↑q)
:
The polynomial-base bracket burns the original source tail before the inner annealed reference block is selected.