Documentation

LeanPool.HighContrastHomogenization.Provider.Response.ProfileCenterMeasurability

High-contrast homogenization: Provider.Response.ProfileCenterMeasurability #

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

Measurability of metric center fluctuations #

The diagonal metric quadratic form is a continuous polynomial on the finite product carrier. Consequently every measurable optimizer average has a measurable metric fluctuation about a deterministic center.

source
theorem HCPolySupport.HighContrast.Response.continuous_metricBlockNormSq {d : ℕ} (m : Mat d) :
Continuous (metricBlockNormSq m)

The canonical diagonal metric quadratic form is continuous.

source
theorem HCPolySupport.HighContrast.Response.AEMeasurable.sqrt_metricBlockNormSq_sub_const {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {X : CoeffSpace d → BlockVec d} (hX : AEMeasurable X P) (m : Mat d) (center : BlockVec d) :
AEMeasurable (fun (a : CoeffSpace d) => √(metricBlockNormSq m (X a - center))) P

The square-root metric fluctuation of an a.e. measurable doubled vector about a deterministic center is a.e. measurable.