Documentation

LeanPool.HighContrastHomogenization.Provider.Quenched.TriadicRebasedLaw

High-contrast homogenization: Provider.Quenched.TriadicRebasedLaw #

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

Triadic rebasing of coefficient laws #

The rebased law is the pushforward by the quotient-level coefficient dilation. The probability, stationarity, and unit-range properties are transported directly on the coefficient-space carrier.

source
noncomputable def HCPolySupport.HighContrast.triadicRebasedLaw {d : ℕ} (n : ℕ) (P : MeasureTheory.Measure (CoeffSpace d)) :
MeasureTheory.Measure (CoeffSpace d)

The coefficient law viewed at the triadically dilated spatial scale.

Equations
Instances For
    source
    theorem HCPolySupport.HighContrast.isProbabilityMeasure_triadicRebasedLaw {d : ℕ} (n : ℕ) (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] :
    MeasureTheory.IsProbabilityMeasure (triadicRebasedLaw n P)

    A triadically rebased probability law is again a probability law.

    source
    theorem HCPolySupport.HighContrast.stationaryLaw_triadicRebasedLaw {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} (hP : IsStationaryLaw P) (n : ℕ) :
    IsStationaryLaw (triadicRebasedLaw n P)

    Frozen integer stationarity is preserved by triadic rebasing.

    source
    theorem HCPolySupport.HighContrast.UnitSeparated.triadicDilateSet {d : ℕ} {U V : Set (Vec d)} (hUV : UnitSeparated U V) (n : ℕ) :
    UnitSeparated (HCPolySupport.triadicDilateSet n U) (HCPolySupport.triadicDilateSet n V)

    Triadic dilation preserves unit separation of ambient sets.

    source
    theorem HCPolySupport.HighContrast.unitRangeLaw_triadicRebasedLaw {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} (hP : IsUnitRangeLaw P) (n : ℕ) :
    IsUnitRangeLaw (triadicRebasedLaw n P)

    Frozen unit-range dependence is preserved by triadic rebasing.