Documentation

LeanPool.HighContrastHomogenization.Support.Probability.RegCoeffField.Restriction

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

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

The restriction σ-algebra on the carrier #

The restriction σ-algebra RestrictionSigmaR U hU is the σ-algebra of carrier events determined by the values of the field on the measurable set U: the comap of the canonical carrier σ-algebra along the restriction endomorphism restrictReg U hU. It is the measurable local σ-algebra used in the explicit pointwise-restriction law lane (see Laws.lean).

RestrictionSigmaR is coarser than the canonical carrier σ-algebra, and monotone under set inclusion (with the MeasurableSet discipline that both restriction maps be well defined, matching the D7-approved coarsening interface). The separation predicate AreUnitSeparated is the ambient sup-norm raw-set predicate of HCPolySupport.Probability.RandomField, reused unchanged.

Reference: the paper (Armstrong–Kuusi–Loher, to appear).

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

The restriction σ-algebra on the carrier: the comap of the canonical carrier σ-algebra along the restriction endomorphism restrictReg U hU.

Equations
Instances For
    source
    theorem HCPolySupport.measurable_restrictReg_restrictionSigmaR {d : ℕ} (U : Set (Vec d)) (hU : MeasurableSet U) :
    Measurable (restrictReg U hU)

    The restriction endomorphism is measurable from the restriction σ-algebra.

    source
    theorem HCPolySupport.measurable_apply_entry_restrictionSigmaR_of_mem {d : ℕ} {U : Set (Vec d)} (hU : MeasurableSet U) {x : Vec d} (hx : x ∈ U) (i j : Fin d) :
    Measurable fun (a : RegCoeffField d) => a.toFun x i j

    Point evaluation inside U remains observable for the restriction σ-algebra: it factors through the restricted field.

    source
    theorem HCPolySupport.restrictionSigmaR_le {d : ℕ} (U : Set (Vec d)) (hU : MeasurableSet U) :
    RestrictionSigmaR U hU ≤ instMeasurableSpaceRegCoeffField d

    The restriction σ-algebra is coarser than the canonical carrier σ-algebra.

    source
    theorem HCPolySupport.restrictReg_comp_restrictReg_of_subset {d : ℕ} {U V : Set (Vec d)} (hU : MeasurableSet U) (hV : MeasurableSet V) (hUV : U ⊆ V) :
    restrictReg U hU ∘ restrictReg V hV = restrictReg U hU

    Composition identity for nested restrictions: restricting to V and then to U ⊆ V is the same as restricting to U.

    source
    theorem HCPolySupport.measurable_restrictReg_restrictionSigmaR_of_subset {d : ℕ} {U V : Set (Vec d)} (hU : MeasurableSet U) (hV : MeasurableSet V) (hUV : U ⊆ V) :
    Measurable (restrictReg U hU)

    The U-restriction endomorphism is measurable from the coarser V-restriction σ-algebra when U ⊆ V.

    source
    theorem HCPolySupport.RestrictionSigmaR_mono {d : ℕ} {U V : Set (Vec d)} (hU : MeasurableSet U) (hV : MeasurableSet V) (hUV : U ⊆ V) :
    RestrictionSigmaR U hU ≤ RestrictionSigmaR V hV

    Monotonicity of the restriction σ-algebra under set inclusion.