High-contrast homogenization: Provider.Quenched.UnitRangeRenormalizedBadEvent

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

The bad generations of the renormalized ellipticity estimate

The renormalization of ellipticity replaces the reference block of a coarse-ellipticity datum by the annealed block at a fixed inner generation, at the cost of a random minimal scale. A generation m is bad when, on the event that the source has burnt in at m, some cell of some inner scale within a window of height h below m exceeds the additive multiple 1 + δ 3^(ρ(m-k)) of the reference block.

This file fixes that event, records the single-cell estimate the argument cites, and performs the two union bounds of the printed proof: over the cells of a scale, whose number is counted by card_centredIndexFinset, and over the scales of the window. The parameter of the single-cell estimate is the printed one, and the two inequalities it must satisfy — that it is at least one, and that the deviation it produces is below the target δ 3^(ρ(m-k)) — are proved here.

Monotonicity of a scaled block

theorem HCPolySupport.HighContrast.Quenched.blockMatLoewnerLE_blockScale_mono {d : ℕ} {c c' : ℝ} (hcc : c ≤ c') {A : BlockMat d} (hA : Book.Ch02.BlockPosDef A) : BlockMatLoewnerLE (blockScale c A) (blockScale c' A)

Scaling a positive block by a larger factor gives a larger block.

The bad events

def HCPolySupport.HighContrast.Quenched.renormBadCell {d : ℕ} (S : CoeffSpace d → ℝ) (Ahat : BlockMat d) (delta rho : ℝ) (m k : ℤ) (w : Fin d → ℤ) : Set (CoeffSpace d)

The bad-cell event: on the event that the source has burnt in at generation m, the coarse block of the scale-k cell of index w exceeds the additive multiple of the reference block.

Equations

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

def HCPolySupport.HighContrast.Quenched.renormBadGeneration {d : ℕ} (S : CoeffSpace d → ℝ) (Ahat : BlockMat d) (delta rho : ℝ) (h : ℕ) (m : ℤ) : Set (CoeffSpace d)

The bad-generation event: some cell of some scale in the window of height h below m, centred in □_m, is bad.

Equations

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

The parameter of the single-cell estimate

noncomputable def HCPolySupport.HighContrast.Quenched.renormParam (gamma nu mu rho delta Gain : ℝ) (n l0 : ℕ) (m k : ℤ) : ℝ

The parameter of the single-cell estimate at generation m and scale k.

Equations

• HCPolySupport.HighContrast.Quenched.renormParam gamma nu mu rho delta Gain n l0 m k = Gain⁻¹ * delta * 3 ^ (gamma - nu + mu * (↑k - (↑n - ↑l0)) + (rho - gamma) * (↑m - ↑k))

noncomputable def HCPolySupport.HighContrast.Quenched.renormFloor (gamma nu mu delta Gain : ℝ) (n l0 h : ℕ) (m : ℤ) : ℝ

The value the parameter is at least, over the whole window at generation m.

Equations

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

def HCPolySupport.HighContrast.Quenched.renormCellCount (d h : ℕ) : ℝ

The number of cells the two union bounds of the printed proof cover.

Equations

• HCPolySupport.HighContrast.Quenched.renormCellCount d h = ↑h * 3 ^ (d * h)

The two inequalities the parameter satisfies

theorem HCPolySupport.HighContrast.Quenched.renorm_gain_le {gamma nu mu rho delta Gain : ℝ} (hGain : 0 < Gain) (hdelta : 0 ≤ delta) (hmu : mu = nu - gamma) (hgn : gamma ≤ nu) (n l0 : ℕ) (m k : ℤ) : Gain * 3 ^ (gamma * (↑m - (↑n - ↑l0))) * 3 ^ (-nu * (↑k - (↑n - ↑l0))) * renormParam gamma nu mu rho delta Gain n l0 m k ≤ delta * 3 ^ (rho * (↑m - ↑k))

The deviation produced by the parameter is below the target. This is the display Θ 3^7 3^(γ(m-l)) 3^(-ν(k-l)) T ≤ δ 3^(ρ(m-k)) of the printed proof, at the inner generation l = n - l₀.

theorem HCPolySupport.HighContrast.Quenched.renormFloor_le_renormParam {gamma nu mu rho delta Gain : ℝ} (hGain : 0 < Gain) (hdelta : 0 ≤ delta) (hmu : 0 < mu) (hrg : gamma ≤ rho) {n l0 h : ℕ} {m k : ℤ} (hkm : k ≤ m) (hwin : m - ↑h + 1 ≤ k) : renormFloor gamma nu mu delta Gain n l0 h m ≤ renormParam gamma nu mu rho delta Gain n l0 m k

The parameter is at least its floor over the window.

theorem HCPolySupport.HighContrast.Quenched.one_le_renormFloor {gamma nu mu delta Gain : ℝ} (hmu : 0 < mu) {n l0 h : ℕ} {m : ℤ} (hnm : ↑n ≤ m) (hl0 : 1 ≤ Gain⁻¹ * delta * 3 ^ (gamma - nu + mu * (↑l0 - ↑h))) : 1 ≤ renormFloor gamma nu mu delta Gain n l0 h m

The floor is at least one from the base generation on. The hypothesis is the printed restriction on l₀.

The single-cell estimate

def HCPolySupport.HighContrast.Quenched.HasCellRenormalization {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (S : CoeffSpace d → ℝ) (Ahat : BlockMat d) (gamma nu Gain : ℝ) (n l0 h : ℕ) : Prop

The single-cell renormalization estimate. This is what the printed proof of the renormalization lemma cites: subadditivity of the coarse block, the concentration estimate for sums of coarse blocks, and the comparison of the reference block with the annealed one at the inner generation l = n - l₀, combined into one statement about a single cell.

Equations

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

The two union bounds

theorem HCPolySupport.HighContrast.Quenched.renormBadCell_subset {d : ℕ} {S : CoeffSpace d → ℝ} {Ahat : BlockMat d} {gamma nu mu rho delta Gain : ℝ} {n l0 : ℕ} {m k : ℤ} (hAhat : Book.Ch02.BlockPosDef Ahat) (hGain : 0 < Gain) (hdelta : 0 ≤ delta) (hmu : mu = nu - gamma) (hgn : gamma ≤ nu) (w : Fin d → ℤ) : renormBadCell S Ahat delta rho m k w ⊆ {a : CoeffSpace d | S a ≤ 3 ^ m ∧ ¬BlockMatLoewnerLE (coarseBlock (standardCell d k w) a) (blockScale (1 + Gain * 3 ^ (gamma * (↑m - (↑n - ↑l0))) * 3 ^ (-nu * (↑k - (↑n - ↑l0))) * renormParam gamma nu mu rho delta Gain n l0 m k) Ahat)}

The bad-cell event at the target multiple is contained in the bad-cell event at the parameter's multiple.

The union bound over the window

theorem HCPolySupport.HighContrast.Quenched.measureReal_renormBadGeneration_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 ≤ Gain⁻¹ * delta * 3 ^ (gamma - nu + mu * (↑l0 - ↑h))) (hcell : HasCellRenormalization P S Ahat gamma nu Gain n l0 h) {m : ℤ} (hnm : ↑n ≤ m) : P.real (renormBadGeneration S Ahat delta rho h m) ≤ renormCellCount d h * (frGauge d (renormFloor gamma nu mu delta Gain n l0 h m))⁻¹

The bad-generation estimate. Two union bounds — over the cells of a scale, counted by card_centredIndexFinset, and over the scales of the window — turn the single-cell estimate into a bound on the whole bad generation, at the parameter's floor.