High-contrast homogenization: Provider.Window.ScaleMeasurability

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

Measurability of the strict successor scale

The response on every standard cell is measurable entry by entry. Reading its relative size as the spectral norm of the normalized response makes each bad scale measurable, and the strict successor is then a countable supremum of measurable extended-real functions.

theorem HCPolySupport.HighContrast.Window.measurable_blockSize_coarseBlock {d : ℕ} {U : Set (Vec d)} (hUopen : IsOpen U) (hUbdd : IsBoundedDomain U) (hUvol : 0 < (MeasureTheory.volume U).toReal) {F : BlockMat d} (hF : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) : Measurable fun (a : CoeffSpace d) => blockSize (coarseBlock U a) F

The relative size of the response on a bounded open cell is measurable.

theorem HCPolySupport.HighContrast.Window.measurable_badScaleSize {d : ℕ} (g : ℝ) (E : BlockMat d) (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) (h m : ℤ) : Measurable fun (a : CoeffSpace d) => ⨆ (k : ℤ), ⨆ (_ : k ≤ m), ⨆ (w : Fin d → ℤ), ⨆ (_ : standardCellCenter k w ∈ centeredCube d m), ENNReal.ofReal (3 ^ (-g * max (↑m - ↑h - ↑k) 0) * blockSize (coarseBlock (standardCell d k w) a) E)

The discounted maximal response at a fixed scale is measurable.

theorem HCPolySupport.HighContrast.Window.measurableSet_badScaleEvent {d : ℕ} (g : ℝ) (E : BlockMat d) (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) (h m : ℤ) : MeasurableSet {a : CoeffSpace d | badScaleEvent g E h m a}

Every fixed bad-scale event is measurable.

theorem HCPolySupport.HighContrast.Window.measurable_successorScale {d : ℕ} (g : ℝ) (E : BlockMat d) (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) (h : ℤ) : Measurable fun (a : CoeffSpace d) => successorScale g E h a

The strict successor of the bad scales is measurable.