Documentation

LeanPool.HighContrastHomogenization.Support.Probability.RegCoeffField.SmoothSigma

Coarse-graining support: Support.Probability.RegCoeffField.SmoothSigma #

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

Smooth integral sigma algebras on regular coefficient fields #

This file isolates the smooth, compactly supported entry-test information used by source-facing integral-local probability APIs. It intentionally installs no ambient measurable-space instance and remains separate from pointwise and restriction-local constructions.

source
@[reducible, inline]
abbrev HCPolySupport.SmoothLocalSigmaR {d : ℕ} (U : Set (Vec d)) :
MeasurableSpace (RegCoeffField d)

The local sigma algebra generated by entry tests against globally smooth, compactly supported probes whose topological support lies in U.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[reducible, inline]
    abbrev HCPolySupport.SmoothGlobalSigmaR (d : ℕ) :
    MeasurableSpace (RegCoeffField d)

    The global smooth integral sigma algebra on regular coefficient fields.

    Equations
    Instances For
      source
      theorem HCPolySupport.smoothLocalSigmaR_mono {d : ℕ} {U V : Set (Vec d)} (hUV : U ⊆ V) :
      SmoothLocalSigmaR U ≤ SmoothLocalSigmaR V

      Smooth local integral information is monotone under enlargement of the observation set.

      source
      theorem HCPolySupport.smoothLocalSigmaR_le_smoothGlobalSigmaR {d : ℕ} (U : Set (Vec d)) :
      SmoothLocalSigmaR U ≤ SmoothGlobalSigmaR d

      Every smooth local integral event is measurable for the global smooth integral sigma algebra.

      source
      theorem HCPolySupport.smoothLocalSigmaR_le_localSigmaR {d : ℕ} (U : Set (Vec d)) :
      SmoothLocalSigmaR U ≤ LocalSigmaR U

      The smooth support-local entry-test sigma algebra is contained in the existing enriched entry-test sigma algebra.