High-contrast homogenization: Consistency.WitnessSigmaField

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

The local sigma-fields separate points

The sigma-field F(U) of the coefficient space of s.introduction — the development's coeffSigma d U — is generated by the smooth linear statistics coeffPairing with test support inside U; the global sigma-field F is the instance instMeasurableSpaceCoeffSpace, that is, coeffSigma d Set.univ, generated by all of them.

That is an uncountable generating family, so it is not immediate that F distinguishes two coefficient fields; and without that, no law on the coefficient space can be pinned to a prescribed field, and the almost sure hypotheses of e.coarse.ellipticity cannot be tested on a concrete law. In particular the singleton of a prescribed field would fail to be measurable for F, so an almost sure statement under an atomic law would be untestable and the class MeasurableSingletonClass (CoeffSpace d) would be empty.

This module is a consistency check of that definition and is not a result of the paper.

This file supplies the countable determining family: the statistics against the translates of a fixed sequence of normalized smooth bumps, centred at the points of a countable dense set. Continuity of the mollification identifies it on all of space from its values on the dense set, and the almost everywhere convergence of mollifications at Lebesgue points recovers the field. Consequently every singleton of the coefficient space is measurable for F.

A countable family of mollifiers

noncomputable def HCPolySupport.HighContrast.witnessBump (d n : ℕ) : ContDiffBump 0

The mollifier scale sequence: inner radius 1/(n+1), outer radius 2/(n+1).

Equations

• HCPolySupport.HighContrast.witnessBump d n = { rIn := 1 / (↑n + 1), rOut := 2 / (↑n + 1), rIn_pos := ⋯, rIn_lt_rOut := ⋯ }

noncomputable def HCPolySupport.HighContrast.witnessMollifier (d n : ℕ) : Vec d → ℝ

The normalized mollifier of scale index n.

Equations

• HCPolySupport.HighContrast.witnessMollifier d n = (HCPolySupport.HighContrast.witnessBump d n).normed MeasureTheory.volume

noncomputable def HCPolySupport.HighContrast.mollifierTest (d n : ℕ) (q : Vec d) : Vec d → ℝ

The test function pairing a field against the mollifier centred at q.

Equations

• HCPolySupport.HighContrast.mollifierTest d n q y = HCPolySupport.HighContrast.witnessMollifier d n (q - y)

theorem HCPolySupport.HighContrast.contDiff_witnessMollifier {d : ℕ} (n : ℕ) : ContDiff ℝ (↑⊤) (witnessMollifier d n)

theorem HCPolySupport.HighContrast.hasCompactSupport_witnessMollifier {d : ℕ} (n : ℕ) : HasCompactSupport (witnessMollifier d n)

theorem HCPolySupport.HighContrast.isLocalTest_mollifierTest {d : ℕ} (n : ℕ) (q : Vec d) : IsLocalTest Set.univ (mollifierTest d n q)

Each mollifier test function is an admissible generator of the global sigma-field.

theorem HCPolySupport.HighContrast.tendsto_witnessBump_rOut {d : ℕ} : Filter.Tendsto (fun (n : ℕ) => (witnessBump d n).rOut) Filter.atTop (nhds 0)

theorem HCPolySupport.HighContrast.witnessBump_rOut_le {d : ℕ} (n : ℕ) : (witnessBump d n).rOut ≤ 2 * (witnessBump d n).rIn

theorem HCPolySupport.HighContrast.ae_eq_zero_of_mollifierTest_eq_zero {d : ℕ} (f : Vec d → ℝ) (hf : MeasureTheory.LocallyIntegrable f MeasureTheory.volume) (Q : Set (Vec d)) (hQ : Dense Q) (h : ∀ (n : ℕ), ∀ q ∈ Q, ∫ (y : Vec d), mollifierTest d n q y * f y = 0) : ∀ᵐ (x : Vec d), f x = 0

The countable determining family. A locally integrable function whose mollifier statistics vanish at every point of a dense set, at every scale of the sequence, vanishes almost everywhere.

Entries of a coefficient field

theorem HCPolySupport.HighContrast.coeffPairing_basis {d : ℕ} (i j : Fin d) (φ : Vec d → ℝ) (a : CoeffSpace d) : coeffPairing (Pi.single i 1) (Pi.single j 1) φ a = ∫ (x : Vec d), ↑↑a x j i * φ x

theorem HCPolySupport.HighContrast.locallyIntegrable_entry {d : ℕ} (a : CoeffSpace d) (i j : Fin d) : MeasureTheory.LocallyIntegrable (fun (x : Vec d) => ↑↑a x i j) MeasureTheory.volume

Every entry of a field of the coefficient space is locally integrable.

theorem HCPolySupport.HighContrast.integrable_entry_mul {d : ℕ} (a : CoeffSpace d) (i j : Fin d) {φ : Vec d → ℝ} (hφ : IsLocalTest Set.univ φ) : MeasureTheory.Integrable (fun (x : Vec d) => ↑↑a x j i * φ x) MeasureTheory.volume

Singletons are measurable

theorem HCPolySupport.HighContrast.measurableSet_coeffPairing_eq {d : ℕ} (e e' : Vec d) {φ : Vec d → ℝ} (hφ : IsLocalTest Set.univ φ) (c : ℝ) : MeasurableSet {a : CoeffSpace d | coeffPairing e e' φ a = c}

theorem HCPolySupport.HighContrast.eq_of_forall_mollifierTest_pairing_eq {d : ℕ} {a b : CoeffSpace d} {Q : Set (Vec d)} (hQ : Dense Q) (h : ∀ (i j : Fin d) (n : ℕ), ∀ q ∈ Q, coeffPairing (Pi.single i 1) (Pi.single j 1) (mollifierTest d n q) a = coeffPairing (Pi.single i 1) (Pi.single j 1) (mollifierTest d n q) b) : a = b

The mollifier statistics determine the field. Two coefficient fields with the same mollifier statistics at every scale and every point of a dense set are equal.

theorem HCPolySupport.HighContrast.measurableSet_singleton_coeffSpace {d : ℕ} (b : CoeffSpace d) : MeasurableSet {b}

The global sigma-field separates points: every singleton of the coefficient space is measurable. Without this, e.coarse.ellipticity could not be verified on any concrete law, because an almost sure statement under an atomic law would be untestable.

instance HCPolySupport.HighContrast.instMeasurableSingletonClassCoeffSpace {d : ℕ} : MeasurableSingletonClass (CoeffSpace d)

theorem HCPolySupport.HighContrast.coeffSigma_le_global (d : ℕ) (U : Set (Vec d)) : coeffSigma d U ≤ instMeasurableSpaceCoeffSpace d

A local sigma-field is coarser than the global one.