Measurability of the local ellipticity event

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. The countable quantitative-slice characterization is shared by the cutoff, flux-corrected and corridor laws without importing the corridor construction.

theorem HCPolySupport.measurableSet_aeLocallyUniformlyEllipticField {d : ℕ} : MeasurableSet {b : RegCoeffField d | Book.Ch04.AELocallyUniformlyEllipticField b}

The set of locally a.e.-uniformly elliptic carrier fields is genuinely measurable: it equals the countable ⋂_Q ⋃_k of the AEE quantitative-slice sets (AELocallyUniformlyEllipticField.exists_aeeQuantitativeEllipticSlice_cubeSet forward; the definition AEEQuantitativeEllipticSlice = IsAEEllipticFieldOn (k+1)⁻¹ (k+1) plus IsAEEllipticFieldOn.mono to the open core backward), each slice set being genuinely LocalSigmaR-measurable on the carrier (measurableSet_localSigmaR_aeeQuantitativeEllipticSlice, Packet P4b) and LocalSigmaR ≤ the canonical carrier σ-algebra.