High-contrast homogenization: Provider.Recurrence.CellSliceMeasurability

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

Ellipticity slices of a general cell are smooth-test measurable

The countable presentation of the coarse-grained energy needs the coefficient field to be confined to one quantitative ellipticity slice of the cell, and the gluing over slices needs the slice events themselves to be measurable for the sigma-field the coefficient space actually carries — the one generated by the smooth linear statistics of the field.

That is proved here for an arbitrary open cell. The a.e. ellipticity event on an open set is a countable intersection of ellipticity conditions on averages over rational balls inside it, and the average over a compact ball is a limit of smooth entry tests: a sequence of smooth cutoffs supported in the cell and increasing to the ball indicator gives the convergence by dominated convergence, the dominating function being the entry itself on a compact neighbourhood of the ball, which is integrable because the field is locally integrable.

Smooth cutoffs approximating a compact ball inside an open cell

theorem HCPolySupport.HighContrast.Recurrence.exists_smooth_cutoff_seq {d : ℕ} {U B : Set (Vec d)} (hUopen : IsOpen U) (hBcpt : IsCompact B) (hBU : B ⊆ U) : ∃ (K : Set (Vec d)) (psi : ℕ → Vec d → ℝ), IsCompact K ∧ K ⊆ U ∧ (∀ (n : ℕ), ContDiff ℝ (↑⊤) (psi n) ∧ HasCompactSupport (psi n) ∧ tsupport (psi n) ⊆ U ∧ Function.support (psi n) ⊆ K ∧ ∀ (x : Vec d), psi n x ∈ Set.Icc 0 1) ∧ ∀ (x : Vec d), Filter.Tendsto (fun (n : ℕ) => psi n x) Filter.atTop (nhds (B.indicator (fun (x : Vec d) => 1) x))

A compact set inside an open set is the pointwise limit of smooth cutoffs supported in the open set, all of them supported in one compact neighbourhood and taking values in [0,1].

Ball averages are smooth-test measurable

theorem HCPolySupport.HighContrast.Recurrence.exists_smooth_entryTestR_approximation {d : ℕ} {U B : Set (Vec d)} (hUopen : IsOpen U) (hBcpt : IsCompact B) (hBU : B ⊆ U) : ∃ (psi : ℕ → Vec d → ℝ), (∀ (n : ℕ), ContDiff ℝ (↑⊤) (psi n) ∧ HasCompactSupport (psi n) ∧ tsupport (psi n) ⊆ U) ∧ ∀ (i j : Fin d) (a : RegCoeffField d), Filter.Tendsto (fun (n : ℕ) => entryTestR i j (psi n) a) Filter.atTop (nhds (entryTestR i j (B.indicator fun (x : Vec d) => 1) a))

The entry test against a smooth cutoff sequence converges to the entry test against the ball indicator, uniformly in the field.

theorem HCPolySupport.HighContrast.Recurrence.measurable_avgMat_smoothLocalSigmaR {d : ℕ} {U B : Set (Vec d)} (hUopen : IsOpen U) (hBcpt : IsCompact B) (hBU : B ⊆ U) : Measurable (avgMat B)

The average of a field over a compact ball inside an open cell is measurable for the smooth entry-test sigma-field of the cell.

The slice event is smooth-test measurable

theorem HCPolySupport.HighContrast.Recurrence.measurableSet_slicePart_smoothLocalSigmaR {d : ℕ} {U : Set (Vec d)} (hUopen : IsOpen U) (lam Lam : ℝ) : MeasurableSet (slicePart U lam Lam)

The rational-ball presentation of the a.e. ellipticity event is measurable for the smooth entry-test sigma-field of an open cell.

theorem HCPolySupport.HighContrast.Recurrence.measurableSet_smoothLocalSigmaR_aeeSlice {d : ℕ} {U : Set (Vec d)} (hUopen : IsOpen U) (k : ℕ) : MeasurableSet {a : RegCoeffField d | AEEQuantitativeEllipticSlice U k a.toFun}

The quantitative ellipticity slice of an open cell is measurable for the smooth entry-test sigma-field. This is CoarseGraining's cube statement with the cube removed.

theorem HCPolySupport.HighContrast.Recurrence.measurableSet_sourceLocal_aeeSlice {d : ℕ} {U : Set (Vec d)} (hUopen : IsOpen U) (k : ℕ) : MeasurableSet {a : Source.Coarse.Carrier d | AEEQuantitativeEllipticSlice U k ↑a}

The quantitative ellipticity slice of an open cell is measurable on the exact coarse source, for the source's own local sigma-field.