High-contrast homogenization: Setup.LocalSigmaFields

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

The local sigma-fields of the coefficient space

The sigma-fields F(U) of the coefficient-law setup in s.introduction are generated by the smooth linear statistics of the coefficient field with test support inside U. This file fixes those generators, the canonical global measurable structure, the unit separation relation used by the unit range of dependence, and the two facts the sigma-fields must have to be non-degenerate: the generating integrals converge, and the integer translation action is measurable.

structure HCPolySupport.HighContrast.IsLocalTest {d : ℕ} (U : Set (Vec d)) (φ : Vec d → ℝ) : Prop

A test function for the local sigma-field F(U): smooth, compactly supported, with support contained in U (the paper's C_c^∞(U)).

• contDiff : ContDiff ℝ (↑⊤) φ
• hasCompactSupport : HasCompactSupport φ
• tsupport_subset : tsupport φ ⊆ U

noncomputable def HCPolySupport.HighContrast.coeffPairing {d : ℕ} (e e' : Vec d) (φ : Vec d → ℝ) (a : CoeffSpace d) : ℝ

The generating linear statistics of F(U): a ↦ ∫ e' · a(x) e φ(x) dx over ℝ^d.

Equations

• HCPolySupport.HighContrast.coeffPairing e e' φ a = ∫ (x : HCPolySupport.Vec d), HCPolySupport.vecDot e' (HCPolySupport.matVecMul (↑↑a x) e) * φ x

@[reducible, inline]

abbrev HCPolySupport.HighContrast.coeffSigma (d : ℕ) (U : Set (Vec d)) : MeasurableSpace (CoeffSpace d)

The local sigma-field F(U) generated by the smooth linear statistics with test support inside U.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance HCPolySupport.HighContrast.instMeasurableSpaceCoeffSpace (d : ℕ) : MeasurableSpace (CoeffSpace d)

The global sigma-field F = F(ℝ^d) is the canonical measurable structure of the coefficient space.

Equations

• HCPolySupport.HighContrast.instMeasurableSpaceCoeffSpace d = HCPolySupport.HighContrast.coeffSigma d Set.univ

def HCPolySupport.HighContrast.UnitSeparated {d : ℕ} (U V : Set (Vec d)) : Prop

dist_∞(U, V) ≥ 1, in the pointwise form.

Equations

• HCPolySupport.HighContrast.UnitSeparated U V = ∀ ⦃x y : HCPolySupport.Vec d⦄, x ∈ U → y ∈ V → 1 ≤ HCPolySupport.Source.AKL.supDist x y

The generating statistics converge

theorem HCPolySupport.HighContrast.integrable_coeffPairing_integrand {d : ℕ} (e e' : Vec d) {U : Set (Vec d)} {φ : Vec d → ℝ} (hφ : IsLocalTest U φ) (a : CoeffSpace d) : MeasureTheory.Integrable (fun (x : Vec d) => vecDot e' (matVecMul (↑↑a x) e) * φ x) MeasureTheory.volume

The generating linear statistics have an integrable integrand: the test function is continuous, vanishes outside a compact set, and the coefficient entries are essentially bounded on any ball containing that set.

Measurability of the translation action

theorem HCPolySupport.HighContrast.coeffPairing_translateCoeff {d : ℕ} (z : Fin d → ℤ) (e e' : Vec d) (φ : Vec d → ℝ) (a : CoeffSpace d) : coeffPairing e e' φ (translateCoeff z a) = coeffPairing e e' (fun (y : Vec d) => φ (y - Source.AKL.intTranslation z)) a

The pairing of a translated field against a test function is the pairing of the field against the translated test function.

theorem HCPolySupport.HighContrast.measurable_translateCoeff {d : ℕ} (z : Fin d → ℤ) : Measurable (translateCoeff z)

The integer translation action is measurable for the global sigma-field. Without it, stationarity of the coefficient law would be unsatisfiable and every theorem carrying it vacuous.