High-contrast homogenization: Provider.Quenched.UnitRangeRenormalizedMeasurability

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

Measurability of the renormalized radius

The bad cells in the one-time ellipticity rebase are scalar excess events. Writing them in that form makes the bad generations, their countable supremum, and the buffered radius measurable on the coefficient space.

theorem HCPolySupport.HighContrast.Quenched.measurableSet_renormBadCell {d : ℕ} [NeZero d] {S : CoeffSpace d → ℝ} (hS : Measurable S) {A : BlockMat d} (hA : IsSymmetricBlockMat A) (hApd : Book.Ch02.BlockPosDef A) {delta rho : ℝ} (hdelta : 0 ≤ delta) (m k : ℤ) (w : Fin d → ℤ) : MeasurableSet (renormBadCell S A delta rho m k w)

A bad cell is measurable once the source scale is measurable and the reference block is positive symmetric.

theorem HCPolySupport.HighContrast.Quenched.measurableSet_renormBadGeneration {d : ℕ} [NeZero d] {S : CoeffSpace d → ℝ} (hS : Measurable S) {A : BlockMat d} (hA : IsSymmetricBlockMat A) (hApd : Book.Ch02.BlockPosDef A) {delta rho : ℝ} (hdelta : 0 ≤ delta) (h : ℕ) (m : ℤ) : MeasurableSet (renormBadGeneration S A delta rho h m)

Every bad-generation event is measurable.

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

Supremum of 3 ^ m over bad renormalized generations m at or above n, expressed as an extended nonnegative real.

Equations

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

theorem HCPolySupport.HighContrast.Quenched.measurable_renormScale {d : ℕ} [NeZero d] {S : CoeffSpace d → ℝ} (hS : Measurable S) {A : BlockMat d} (hA : IsSymmetricBlockMat A) (hApd : Book.Ch02.BlockPosDef A) {delta rho : ℝ} (hdelta : 0 ≤ delta) (h n : ℕ) : Measurable (renormScale S A delta rho h n)

The renormalized minimal scale is measurable.

theorem HCPolySupport.HighContrast.Quenched.measurable_renormRadius {d : ℕ} [NeZero d] {S : CoeffSpace d → ℝ} (hS : Measurable S) {A : BlockMat d} (hA : IsSymmetricBlockMat A) (hApd : Book.Ch02.BlockPosDef A) {delta rho : ℝ} (hdelta : 0 ≤ delta) (h n : ℕ) : Measurable (renormRadius S A delta rho h n)

The buffered real-valued renormalized radius is measurable.