High-contrast homogenization: Analytic.ScaledCoeff

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

The rescaled coefficient field is locally uniformly elliptic

The Dirichlet estimate e.random.dirichlet is read for the rescaled field a^ε(x) = a(x/ε), and every closure statement about a weak-gradient pair needs an ellipticity pair for the field it is applied to on the bounded set it is read on.

The route is the one HCPoly.Setup.CoefficientSpace takes for translateField: the transport map is quasi measure preserving for the Lebesgue measure, so almost-everywhere statements pull back along it. There the map is a translation and the input is MeasurePreserving.quasiMeasurePreserving; here it is the dilation x ↦ ε⁻¹ • x, which is not measure preserving but is quasi measure preserving — its pushforward is a finite nonzero multiple of the Lebesgue measure — and the input is MeasureTheory.Measure.quasiMeasurePreserving_smul, available because volume on Fin d → ℝ is an additive Haar measure. The dilation moves no value of a, only where it is read: the ball of radius R for a^ε is served by the constants of a on the ball of radius R/ε.

theorem HCPolySupport.HighContrast.quasiMeasurePreserving_smul_vec {d : ℕ} {c : ℝ} (hc : c ≠ 0) : MeasureTheory.QuasiMeasurePreserving (fun (x : Vec d) => c • x) MeasureTheory.volume MeasureTheory.volume

A nonzero scalar dilation of ℝ^d is quasi measure preserving for the Lebesgue measure.

theorem HCPolySupport.HighContrast.aestronglyMeasurable_scaledCoeff {d : ℕ} {ε : ℝ} (hε : 0 < ε) (a : CoeffSpace d) : MeasureTheory.AEStronglyMeasurable (scaledCoeff ε a) MeasureTheory.volume

The rescaled field is a.e. strongly measurable, so it can be fed to the weak flux pairing estimates.

theorem HCPolySupport.HighContrast.aestronglyMeasurable_scaledCoeff_apply {d : ℕ} {ε : ℝ} (hε : 0 < ε) (a : CoeffSpace d) (i j : Fin d) : MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => scaledCoeff ε a x i j) MeasureTheory.volume

The entries of the rescaled field are a.e. strongly measurable.

theorem HCPolySupport.HighContrast.isAELocallyUniformlyElliptic_scaledCoeff {d : ℕ} {ε : ℝ} (hε : 0 < ε) (a : CoeffSpace d) : IsAELocallyUniformlyElliptic (scaledCoeff ε a)

The rescaled coefficient field a^ε(x) = a(x/ε) is locally uniformly elliptic: the ball of radius R is served by the ellipticity constants of a on the ball of radius R/ε.

theorem HCPolySupport.HighContrast.ae_abs_entry_le_scaledCoeff {d : ℕ} {ε : ℝ} (hε : 0 < ε) (a : CoeffSpace d) {S : Set (Vec d)} (hS : Bornology.IsBounded S) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ᵐ (x : Vec d), x ∈ S → ∀ (i j : Fin d), |scaledCoeff ε a x i j| ≤ M

The essential entry bound of the rescaled field on a bounded set, in the shape the pairing lemmas take it.