Documentation

LeanPool.HighContrastHomogenization.Support.Probability.RegCoeffField.SmoothSliceMeasurability

Coarse-graining support: Support.Probability.RegCoeffField.SmoothSliceMeasurability #

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Smooth-local measurability of quantitative ellipticity slices #

For compact rational balls in an open cube, smooth cutoffs supported in the cube approximate the ball indicator. Dominated convergence then transfers the ball-average presentation of the quantitative ellipticity slice to the smooth local sigma algebra.

source
theorem HCPolySupport.measurableSet_smoothLocalSigmaR_aeeSlice {d : ℕ} (Q : TriadicCube d) (k : ℕ) :
MeasurableSet {a : RegCoeffField d | AEEQuantitativeEllipticSlice (cubeSet Q) k a.toFun}

The AEE quantitative ellipticity slice of a triadic cube is measurable for the smooth support-local integral sigma algebra.