High-contrast homogenization: Provider.Quenched.UnitRangeRenormalizedScale

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

The renormalized minimal scale and its tail

The renormalization of ellipticity produces, at each base generation, a random minimal scale above which the additive comparison with the reference block holds at every generation of the window. The scale is the supremum of the bad generations, and its tail is the sum of the bad-generation estimates over the generations above.

That sum is super-geometric: the floor of the single-cell parameter grows by the fixed triadic factor 3^μ at each generation, so the Gaussian gauge is iterated at a geometrically growing argument and the whole sum is at most twice its first term. The prefactor left by the two union bounds over the window is then absorbed by halving the exponent.

The base value of the parameter floor

noncomputable def HCPolySupport.HighContrast.Quenched.renormBase (gamma nu mu delta Gain : ℝ) (l0 h : ℕ) : ℝ

The value of the parameter floor at the base generation.

Equations

• HCPolySupport.HighContrast.Quenched.renormBase gamma nu mu delta Gain l0 h = Gain⁻¹ * delta * 3 ^ (gamma - nu + mu * (↑l0 - ↑h))

theorem HCPolySupport.HighContrast.Quenched.renormFloor_eq_base_mul (gamma nu mu delta Gain : ℝ) (n l0 h : ℕ) (m : ℤ) : renormFloor gamma nu mu delta Gain n l0 h m = renormBase gamma nu mu delta Gain l0 h * 3 ^ (mu * (↑m - ↑n))

theorem HCPolySupport.HighContrast.Quenched.inv_frGauge_renormFloor (d : ℕ) (gamma nu mu delta Gain : ℝ) (n l0 h : ℕ) (m : ℤ) : (frGauge d (renormFloor gamma nu mu delta Gain n l0 h m))⁻¹ = Real.exp (-(frGaugeConst d * renormBase gamma nu mu delta Gain l0 h ^ 2 * 3 ^ (2 * mu * (↑m - ↑n))))

The bad-generation bound, written as a Gaussian tail in the base value.

Countable subadditivity in the real-valued measure

The minimal scale

noncomputable def HCPolySupport.HighContrast.Quenched.renormScale {d : ℕ} (S : CoeffSpace d → ℝ) (Ahat : BlockMat d) (delta rho : ℝ) (h n : ℕ) (a : CoeffSpace d) : ENNReal

The renormalized minimal scale of the base generation n: the supremum of the bad generations above n.

Equations

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

noncomputable def HCPolySupport.HighContrast.Quenched.renormRadius {d : ℕ} (S : CoeffSpace d → ℝ) (Ahat : BlockMat d) (delta rho : ℝ) (h n : ℕ) (a : CoeffSpace d) : ℝ

The renormalized minimal scale with the endpoint buffer of the endgame: R_n = 3 max{1, R_n^{(0)}}.

Equations

• HCPolySupport.HighContrast.Quenched.renormRadius S Ahat delta rho h n a = 3 * max 1 (HCPolySupport.HighContrast.Quenched.renormScale S Ahat delta rho h n a).toReal

theorem HCPolySupport.HighContrast.Quenched.renormScale_gt_subset {d : ℕ} {S : CoeffSpace d → ℝ} {Ahat : BlockMat d} {delta rho : ℝ} {h n : ℕ} {N : ℤ} : {a : CoeffSpace d | ENNReal.ofReal (3 ^ N) < renormScale S Ahat delta rho h n a} ⊆ ⋃ (j : ℕ), renormBadGeneration S Ahat delta rho h (N + 1 + ↑j)

Above a generation, the minimal scale is witnessed by a bad generation strictly above it.

The tail of the minimal scale

theorem HCPolySupport.HighContrast.Quenched.measureReal_renormScale_gt_le {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsFiniteMeasure P] {S : CoeffSpace d → ℝ} {Ahat : BlockMat d} {gamma nu mu rho delta Gain : ℝ} {n l0 h : ℕ} (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) {N : ℤ} (hnN : ↑n ≤ N) : P.real {a : CoeffSpace d | ENNReal.ofReal (3 ^ N) < renormScale S Ahat delta rho h n a} ≤ renormCellCount d h * (2 * Real.exp (-(frGaugeConst d * renormBase gamma nu mu delta Gain l0 h ^ 2 * 3 ^ (2 * mu * (↑N + 1 - ↑n)))))

The tail of the renormalized minimal scale. Summing the bad-generation estimates over the generations above N gives a Gaussian tail whose argument is the parameter floor at generation N + 1.

The buffer absorbs the union-bound prefactor

theorem HCPolySupport.HighContrast.Quenched.buffer_absorb (d : ℕ) {mu Cnt : ℝ} (hmu : 0 < mu) (hCnt : 0 < Cnt) {b q : ℕ} (hb : Real.log Cnt ≤ frGaugeConst d * (3 ^ (2 * mu * ↑b) - 1)) : Cnt * Real.exp (-(frGaugeConst d * 3 ^ (2 * mu * (↑q + ↑b)))) ≤ Real.exp (-(frGaugeConst d * 3 ^ (2 * mu * ↑q)))

A prefactor is absorbed by a triadic buffer in the exponent.

The shifted tail in the shape the engine consumes

theorem HCPolySupport.HighContrast.Quenched.measureReal_renormRadius_gt_le {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 * (3 ^ (2 * mu * ↑b) - 1)) (q : ℕ) : P.real {a : CoeffSpace d | 3 ^ (n + q + b) < renormRadius S Ahat delta rho h n a} ≤ Real.exp (-(frGaugeConst d * 3 ^ (2 * mu * ↑q)))

The shifted tail of the renormalized minimal scale. With a buffer absorbing the union-bound prefactor, the renormalized minimal scale obeys exactly the shifted tail the bad-tail engine consumes, at the dimensional constant c_fr(d).