Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch04.SourceLaw

Coarse-graining support: Support.Book.Ch04.SourceLaw #

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

Exact coarse-source Chapter 4 laws #

This is the staging law surface for the coarse-graining source. Its carrier and probability assumptions are deliberately separate from the existing regular/restriction Chapter 4 lane.

source
@[reducible, inline]
abbrev HCPolySupport.Book.Ch04.SourceCoeffLaw (d : ℕ) :
Type

A Chapter 4 law on the exact coarse source carrier.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev HCPolySupport.Book.Ch04.SourceStationaryLaw {d : ℕ} (P : SourceCoeffLaw d) :
    Prop

    The coarse source stationarity assumption (P1).

    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev HCPolySupport.Book.Ch04.SourceUnitRangeDependentLaw {d : ℕ} (P : SourceCoeffLaw d) :
      Prop

      The coarse source Euclidean unit-range dependence assumption (P2).

      Equations
      Instances For
        source
        @[reducible, inline]
        abbrev HCPolySupport.Book.Ch04.SourceIsotropicAndAdjointInvariantLaw {d : ℕ} (P : SourceCoeffLaw d) :
        Prop

        The coarse source joint isotropy and adjoint-invariance assumption (P3).

        Equations
        Instances For
          source
          structure HCPolySupport.Book.Ch04.SourceStructuralLaw {d : ℕ} (P : SourceCoeffLaw d) :
          Prop

          The three structural assumptions of the coarse-graining source.

          Probability is intentionally not bundled here: clients state it separately as an IsProbabilityMeasure instance when it is needed.

          Instances For