Coarse-graining support: Support.Probability.Source.Coarse.RegIntegralAdapter

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Coarse-to-regular integral adapter

This module compares the source coarse integral sigma algebra with the smooth integral sigma algebra on regular coefficient fields. It deliberately does not equip the adapter with measurability into the canonical regular carrier.

theorem HCPolySupport.Source.Coarse.locallyIntegrable_coarse_entry {d : ℕ} (a : Carrier d) (i j : Fin d) : MeasureTheory.LocallyIntegrable (fun (x : Vec d) => ↑a x i j) MeasureTheory.volume

def HCPolySupport.Source.Coarse.coarseToRegular {d : ℕ} (a : Carrier d) : RegCoeffField d

The total regular-field realization of a coarse source carrier.

Equations

• HCPolySupport.Source.Coarse.coarseToRegular a = { toFun := ↑a, entry_measurable := ⋯, entry_locInt := ⋯ }

@[simp]

theorem HCPolySupport.Source.Coarse.coarseToRegular_apply {d : ℕ} (a : Carrier d) (x : Vec d) : (coarseToRegular a).toFun x = ↑a x

The coarse-to-regular realization preserves every literal field value.

noncomputable def HCPolySupport.Source.Coarse.regularBilinearTest {d : ℕ} (e e' : Vec d) (φ : Vec d → ℝ) (a : RegCoeffField d) : ℝ

The integral of the bilinear coefficient probe (e' · a(x)e) φ(x) over Euclidean space.

Equations

• HCPolySupport.Source.Coarse.regularBilinearTest e e' φ a = ∫ (x : HCPolySupport.Vec d), HCPolySupport.vecDot e' (HCPolySupport.matVecMul (a.toFun x) e) * φ x

theorem HCPolySupport.Source.Coarse.measurable_coarseToRegular_smoothLocal {d : ℕ} (U : Set (Vec d)) (hU : MeasurableSet U) : Measurable coarseToRegular

The coarse-to-regular realization is measurable from coarse local integral information into the smooth regular local integral sigma algebra.

theorem HCPolySupport.Source.Coarse.coarseLocalSigma_eq_comap_smoothLocalSigmaR {d : ℕ} (U : Set (Vec d)) (hU : MeasurableSet U) : localSigma U hU = MeasurableSpace.comap coarseToRegular (SmoothLocalSigmaR U)

The coarse local integral sigma algebra is exactly the pullback of the smooth compact-support integral sigma algebra on regular coefficient fields.

theorem HCPolySupport.Source.Coarse.globalSigma_eq_comap_smoothGlobalSigmaR (d : ℕ) : globalSigma d = MeasurableSpace.comap coarseToRegular (SmoothGlobalSigmaR d)

The global coarse integral sigma algebra is the pullback of the global smooth regular integral sigma algebra.

theorem HCPolySupport.Source.Coarse.measurable_coarseToRegular_smoothGlobal {d : ℕ} : Measurable coarseToRegular

The coarse-to-regular realization is measurable for the global smooth integral sigma algebras.

theorem HCPolySupport.Source.Coarse.coarseLocalSigma_le_comap_localSigmaR {d : ℕ} (U : Set (Vec d)) (hU : MeasurableSet U) : localSigma U hU ≤ MeasurableSpace.comap coarseToRegular (LocalSigmaR U)

Coarse local integral information is measurable in the pullback of the existing enriched regular local sigma algebra.