High-contrast homogenization: Provider.Quenched.UnitRangeCellRenormalization

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

The single-cell renormalization estimate

The renormalization of ellipticity cites, for a single cell of a single scale, one estimate: that the coarse block of that cell exceeds an additive multiple of the annealed block at the inner generation only with the finite-range Gaussian probability. This file proves that estimate from the frozen carriers alone — stationarity, unit range of dependence, and the coarse-ellipticity datum — and records it in the form the bad-generation union bounds consume.

The argument is the printed one. The coarse blocks of the inner cells that subdivide the parent are read in the coordinates normalized by the reference block, and cut off at a level the coarse-ellipticity datum makes inactive on the event that the source has burnt in; the cut-off readouts are bounded, local to their own cells and centred at their own means, so the concentration estimate of unit range applies to their average entrywise, and the reassembly turns the entrywise deviation into a Loewner deviation against the identity. Un-normalizing returns a deviation against the reference block, and the comparison of the reference block with the annealed one turns that into the printed additive multiple. Subadditivity puts the parent below the average, and the centring identification puts the block of means below the annealed block, so the two ends of the chain meet.

Two bookkeeping points of the printed proof are visible here. The inner cells of a parent centred in □_m are centred in □_{m+1}, so the coarse-ellipticity datum is read one generation higher and the cutoff level carries the factor 3^g. And the reassembly costs the prefactor (2d)², which is absorbed by evaluating the concentration estimate at the shifted parameter T + renormShift d rather than at T.

The quadratic form of a difference and of an average

theorem HCPolySupport.HighContrast.Quenched.blockVecDot_blockMatVecMul_blockSub {d : ℕ} (A B : BlockMat d) (X : BlockVec d) : blockVecDot X (blockMatVecMul (blockSub A B) X) = blockVecDot X (blockMatVecMul A X) - blockVecDot X (blockMatVecMul B X)

The quadratic form of a difference of doubled blocks.

theorem HCPolySupport.HighContrast.Quenched.blockVecDot_blockMatVecMul_avgBlockOf {d : ℕ} {ι : Type u_1} (Z : Finset ι) (M : ι → BlockMat d) (X : BlockVec d) : blockVecDot X (blockMatVecMul (avgBlockOf Z M) X) = (↑Z.card)⁻¹ * ∑ t ∈ Z, blockVecDot X (blockMatVecMul (M t) X)

The quadratic form of an average of doubled blocks is the average of the quadratic forms.

theorem HCPolySupport.HighContrast.Quenched.avgBlockOf_congr {d : ℕ} {ι : Type u_1} {Z : Finset ι} {M N : ι → BlockMat d} (h : ∀ t ∈ Z, M t = N t) : avgBlockOf Z M = avgBlockOf Z N

An average of doubled blocks agreeing on the index set is unchanged.

theorem HCPolySupport.HighContrast.Quenched.isSymmetricBlockMat_avgBlockOf {d : ℕ} {ι : Type u_1} (Z : Finset ι) {M : ι → BlockMat d} (h : ∀ (t : ι), IsSymmetricBlockMat (M t)) : IsSymmetricBlockMat (avgBlockOf Z M)

The average of symmetric doubled blocks is symmetric.

theorem HCPolySupport.HighContrast.Quenched.blockMatLoewnerLE_avgBlockOf_of_forall {d : ℕ} {ι : Type u_1} {Z : Finset ι} (hZ : Z.Nonempty) {M : ι → BlockMat d} {C : BlockMat d} (h : ∀ t ∈ Z, BlockMatLoewnerLE (M t) C) : BlockMatLoewnerLE (avgBlockOf Z M) C

An average of doubled blocks each below a fixed block is below that block.

The single-cell estimate, for an abstract family of inner cells

theorem HCPolySupport.HighContrast.Quenched.measureReal_renormCell_le_of_family {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {g : ℝ} {E : BlockMat d} {Psi : ℝ → ℝ} {Kg : ℝ} {S : CoeffSpace d → ℝ} (hstat : IsStationaryLaw P) (hunit : IsUnitRangeLaw P) (hdag : CoarseEllipticityDagger P g E Psi Kg S) {l m k : ℤ} (hl : 0 ≤ l) (hlm : l ≤ m + 1) (hhalf : (Psi (3 ^ l))⁻¹ ≤ 1 / 2) {Zi : Finset (Fin d → ℤ)} (hZi : Zi.Nonempty) (hZmem : ∀ u ∈ Zi, standardCellCenter l u ∈ centeredCube d (m + 1)) (w : Fin d → ℤ) (hsubadd : ∀ (a : CoeffSpace d), BlockMatLoewnerLE (coarseBlock (standardCell d k w) a) (avgBlockOf Zi fun (u : Fin d → ℤ) => coarseBlock (standardCell d l u) a)) {T C : ℝ} (hT : 1 ≤ T) (hC : 32 * ↑d ^ 2 * 3 ^ (g * (↑(m + 1) - ↑l)) * frThreshold d * (T + renormShift d) * (√↑Zi.card)⁻¹ * kappaRef E ≤ C) : P.real {a : CoeffSpace d | S a ≤ 3 ^ m ∧ ¬BlockMatLoewnerLE (coarseBlock (standardCell d k w) a) (blockScale (1 + C) (annealedBlock P (centeredCube d l)))} ≤ (frGauge d T)⁻¹

The single-cell renormalization estimate. For a finite family of scale-l standard cells whose centres lie in □_{m+1} and whose average dominates the coarse block of the parent, the coarse block of the parent exceeds the additive multiple 1 + C of the annealed block at generation l — on the event that the source has burnt in at m — with probability at most Ψ_fr(T)⁻¹, as soon as C dominates the deviation the concentration estimate produces at the shifted parameter T + renormShift d.

The named input of the renormalization lemma, from the frozen carriers

theorem HCPolySupport.HighContrast.Quenched.hasCellRenormalization_of_frozen {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {g : ℝ} {E : BlockMat d} {Psi : ℝ → ℝ} {Kg : ℝ} {S : CoeffSpace d → ℝ} (hstat : IsStationaryLaw P) (hunit : IsUnitRangeLaw P) (hdag : CoarseEllipticityDagger P g E Psi Kg S) {n l0 h : ℕ} (hl0n : l0 ≤ n) (hhl0 : h ≤ l0 + 1) (hhalf : (Psi (3 ^ (↑n - ↑l0)))⁻¹ ≤ 1 / 2) : HasCellRenormalization P S (annealedBlock P (centeredCube d (↑n - ↑l0))) g (↑d / 2) (32 * ↑d ^ 2 * 3 ^ g * frThreshold d * (1 + renormShift d) * kappaRef E) n l0 h

The single-cell renormalization estimate holds for the frozen carriers. Stationarity, unit range of dependence and the coarse-ellipticity datum supply HasCellRenormalization at the annealed block of the inner generation l = n - l₀, with the exponents γ = g and ν = d/2 and the gain

Gain = 32 d² 3^g C_fr(d) (1 + renormShift d) κ_𝐄,

a constant of the dimension, of the exponent g and of the reference block alone. The two arithmetic side conditions are the printed ones: the inner generation lies below the window (h ≤ l₀ + 1), and the source tail at the inner generation is at most one half.