High-contrast homogenization: Provider.Quenched.RenormalizedRadiusGauge

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

A gauge for the normalized renormalization radius

The shifted triadic tail of the renormalization radius is converted here into an ordinary source-tail estimate. Below the buffer scale the gauge is one; above it the powered finite-range gauge is read in buffer units.

noncomputable def HCPolySupport.HighContrast.Quenched.renormalizedRadiusGauge (d : ℕ) (mu : ℝ) (b : ℕ) : ℝ → ℝ

The source gauge of the renormalization radius after division by its base triadic scale.

Equations

• HCPolySupport.HighContrast.Quenched.renormalizedRadiusGauge d mu b t = if t < 3 ^ (b + 1) then 1 else HCPolySupport.HighContrast.Quenched.frPoweredGauge d mu (t / 3 ^ (b + 1))

noncomputable def HCPolySupport.HighContrast.Quenched.renormalizedRadiusGrowthWitness (d : ℕ) (mu : ℝ) (b : ℕ) : ℝ

A growth witness for renormalizedRadiusGauge.

Equations

• HCPolySupport.HighContrast.Quenched.renormalizedRadiusGrowthWitness d mu b = 3 ^ (b + 1) * HCPolySupport.HighContrast.Quenched.frPoweredGrowthWitness d mu

theorem HCPolySupport.HighContrast.Quenched.admissiblePsi_renormalizedRadiusGauge (d : ℕ) {mu : ℝ} (hmu : 0 < mu) (b : ℕ) : IndependentSums.AdmissiblePsi (renormalizedRadiusGauge d mu b)

theorem HCPolySupport.HighContrast.Quenched.one_lt_renormalizedRadiusGrowthWitness (d : ℕ) {mu : ℝ} (hmu : 0 < mu) (b : ℕ) : 1 < renormalizedRadiusGrowthWitness d mu b

theorem HCPolySupport.HighContrast.Quenched.hasPsiGrowth_renormalizedRadiusGauge (d : ℕ) {mu : ℝ} (hmu : 0 < mu) (b : ℕ) : IndependentSums.HasPsiGrowth (renormalizedRadiusGauge d mu b) (renormalizedRadiusGrowthWitness d mu b)

theorem HCPolySupport.HighContrast.Quenched.measureReal_normalized_renormRadius_gt_le {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure 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)) (t : ℝ) : 0 < t → P.real (IndependentSums.upperTailEvent (fun (a : CoeffSpace d) => renormRadius S Ahat delta rho h n a / 3 ^ n) t) ≤ (renormalizedRadiusGauge d mu b t)⁻¹

The normalized renormalization radius has an ordinary source tail at the buffered powered finite-range gauge.

theorem HCPolySupport.HighContrast.Quenched.ae_renormScale_ne_top {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure 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) : ∀ᵐ (a : CoeffSpace d) ∂P, renormScale S Ahat delta rho h n a ≠ ⊤

The supremum defining the renormalization scale is finite almost surely. This closes the exceptional top branch that is deliberately erased by ENNReal.toReal in the real-valued radius.