High-contrast homogenization: Provider.Quenched.UnitRangeRenormalizedWitness

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

The coupled mixing-scale witness from the frozen carriers

The renormalization of ellipticity feeds the bad-tail engine with a generation-indexed family of minimal scales whose shifted tail is the engine's hRtail at the dimensional constant c_fr(d). Its only analytic input is the single-cell estimate HasCellRenormalization, and that estimate is now a theorem of the frozen carriers.

This file performs the substitution: the reference family is the annealed block at the inner generation n - l₀, the exponents are γ = g and ν = d/2, and the gain is the dimensional constant renormGain. What is left of the hypothesis list is the engine's own bookkeeping — the parameters of the window, the buffer, the block decay and the normalizer — together with three arithmetic side conditions on the window: the inner generation lies below the base generation, the window is no higher than l₀ + 1, and the source tail at the lowest inner generation is at most one half.

noncomputable def HCPolySupport.HighContrast.Quenched.renormGain (d : ℕ) (g : ℝ) (E : BlockMat d) : ℝ

The gain of the single-cell renormalization estimate on the frozen carriers: a constant of the dimension, of the ellipticity exponent and of the reference block alone.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.Quenched.renormGain_pos {d : ℕ} [NeZero d] {g : ℝ} {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) (hsharp : BlockMatLoewnerLE (blockSharp E) E) : 0 < renormGain d g E

theorem HCPolySupport.HighContrast.Quenched.blockPosDef_annealedBlock_of_frozen {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {g : ℝ} {E : BlockMat d} {Psi : ℝ → ℝ} {Kg : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Psi Kg S) (l : ℤ) (hhalf : (Psi (3 ^ l))⁻¹ ≤ 1 / 2) : Book.Ch02.BlockPosDef (annealedBlock P (centeredCube d l))

The annealed block at an inner generation is positive definite, the reference comparison putting the positive reference block below it.