Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch04.Law

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

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

Canonical Chapter 4 source laws #

Unprefixed Chapter 4 law names denote the exact coarse-source, integral-local semantics. The separate pointwise-restriction/sup-metric engineering lane is exposed through the Restriction* names imported from RestrictionLaw.

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

A canonical Chapter 4 law on the exact coarse source carrier.

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

    The canonical coarse-source stationarity assumption.

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

      The canonical coarse-source Euclidean unit-range assumption.

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

        The canonical coarse-source joint isotropy and adjoint-invariance assumption.

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

          The canonical coarse-source structural law assumptions.

          Equations
          Instances For
            source
            theorem HCPolySupport.Book.Ch04.StructuralLaw.stationary {d : ℕ} {P : CoeffLaw d} (hP : StructuralLaw P) :
            StationaryLaw P

            Access the canonical stationarity field.

            source
            theorem HCPolySupport.Book.Ch04.StructuralLaw.unit_range {d : ℕ} {P : CoeffLaw d} (hP : StructuralLaw P) :
            UnitRangeDependentLaw P

            Access the canonical unit-range field.

            source
            theorem HCPolySupport.Book.Ch04.StructuralLaw.isotropic_and_adjoint_invariant {d : ℕ} {P : CoeffLaw d} (hP : StructuralLaw P) :
            IsotropicAndAdjointInvariantLaw P

            Access the canonical joint isotropy and adjoint-invariance field.