LIHLocalSigma

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The local integral sigma-field for shell fields

lihLocalSigma U is the pullback of CoarseGraining's integral-generated Homogenization.LocalSigmaR U along ShellField.forgetShell. It carries the measurability of supported CoarseGraining entry-test observables and is dominated by the canonical Borel sigma-field on shell fields.

The definition deliberately contains no point-evaluation or restriction sigma-fields.

@[reducible, inline]

abbrev Algsuperdiff.Frozen.Assumptions.ShellField.lihLocalSigma {d : ℕ} (U : Set (HCPolySupport.Vec d)) : MeasurableSpace (ShellField d)

The shell-field pullback of CoarseGraining's local integral sigma-field.

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.lihLocalSigma U = MeasurableSpace.comap Algsuperdiff.Frozen.Assumptions.ShellField.forgetShell (HCPolySupport.LocalSigmaR U)

theorem Algsuperdiff.Frozen.Assumptions.ShellField.measurable_entryTestR_forgetShell_lihLocalSigma {d : ℕ} (U : Set (HCPolySupport.Vec d)) (i k : Fin d) {psi : HCPolySupport.Vec d → ℝ} (hpsi : HCPolySupport.IsProbeR psi) (hpsiSupport : Function.support psi ⊆ U) : Measurable fun (j : ShellField d) => HCPolySupport.entryTestR i k psi j.forgetShell

A supported CoarseGraining entry-test observable, pulled back to shell fields, is measurable from lihLocalSigma U.

theorem Algsuperdiff.Frozen.Assumptions.ShellField.lihLocalSigma_le_borel {d : ℕ} (U : Set (HCPolySupport.Vec d)) : lihLocalSigma U ≤ inferInstance

CoarseGraining's pulled-back local integral sigma-field is contained in the canonical Borel sigma-field on shell fields.