Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch04.Theorems.Scalarization

Coarse-graining support: Support.Book.Ch04.Theorems.Scalarization #

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

Scalarization from isotropy #

This file turns the structural symmetries of the law into the primitive scalarization data used by the scalarized Chapter 4 moment surface.

source
theorem HCPolySupport.Book.Ch04.Internal.annealedPrimitiveScalarizationData_of_isotropic_adjoint {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hIso : RestrictionIsotropicLaw P) (hAdj : RestrictionAdjointInvariantLaw P) (n : ℤ) :
AnnealedPrimitiveScalarizationData P n

Isotropy and adjoint invariance scalarize the primitive annealed blocks at a fixed scale. The a.s. deterministic coarse-block existence needed by the covariance identities is supplied by RestrictionLawCarrier.

source
theorem HCPolySupport.Book.Ch04.Internal.annealedPrimitiveScalarizationData_of_structuralLaw {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hStruct : RestrictionStructuralLaw P) (n : ℤ) :
AnnealedPrimitiveScalarizationData P n

Structural-law version of Internal.annealedPrimitiveScalarizationData_of_isotropic_adjoint.

source
theorem HCPolySupport.Book.Ch04.Internal.hasAnnealedScalarizationAtScale_of_isotropic_adjoint {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hIso : RestrictionIsotropicLaw P) (hAdj : RestrictionAdjointInvariantLaw P) (n : ℤ) :
HasAnnealedScalarizationAtScale P n

Isotropy and adjoint invariance give scalarization at a fixed scale.

source
theorem HCPolySupport.Book.Ch04.Internal.hasAnnealedScalarizationAtScale_of_structuralLaw {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hStruct : RestrictionStructuralLaw P) (n : ℤ) :
HasAnnealedScalarizationAtScale P n

Structural-law version of scalarization at a fixed scale.

source
theorem HCPolySupport.Book.Ch04.Internal.annealedScalarizationTheory_of_isotropic_adjoint {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hIso : RestrictionIsotropicLaw P) (hAdj : RestrictionAdjointInvariantLaw P) :
AnnealedScalarizationTheory P

Isotropy and adjoint invariance give scalarization at every scale.

source
theorem HCPolySupport.Book.Ch04.Internal.annealedScalarizationTheory_of_structuralLaw {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hStruct : RestrictionStructuralLaw P) :
AnnealedScalarizationTheory P

Structural-law version of scalarization at every scale.

source
noncomputable def HCPolySupport.Book.Ch04.RestrictionLawCarrier.barSigmaAtScale {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hStruct : RestrictionStructuralLaw P) (n : ℤ) :
ℝ

Structural-law scalar \bar\sigma_n.

Equations
Instances For
    source
    noncomputable def HCPolySupport.Book.Ch04.RestrictionLawCarrier.barSigmaStarAtScale {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hStruct : RestrictionStructuralLaw P) (n : ℤ) :
    ℝ

    Structural-law scalar \bar\sigma_{*,n}.

    Equations
    Instances For
      source
      noncomputable def HCPolySupport.Book.Ch04.RestrictionLawCarrier.barBAtScale {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hStruct : RestrictionStructuralLaw P) (n : ℤ) :
      ℝ

      Structural-law scalar upper-left coefficient \bar b_n.

      Equations
      Instances For
        source
        noncomputable def HCPolySupport.Book.Ch04.RestrictionLawCarrier.barSigmaStarInvAtScale {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hStruct : RestrictionStructuralLaw P) (n : ℤ) :
        ℝ

        Structural-law scalar inverse-star coefficient \bar\sigma_{*,n}^{-1}.

        Equations
        Instances For
          source
          noncomputable def HCPolySupport.Book.Ch04.RestrictionLawCarrier.thetaAtScale {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hStruct : RestrictionStructuralLaw P) (n : ℤ) :
          ℝ

          Structural-law contrast \Theta_n = \bar\sigma_n \bar\sigma_{*,n}^{-1}.

          Equations
          Instances For
            source
            theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.annealedSigmaAtScale_eq_barSigmaAtScale {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hStruct : RestrictionStructuralLaw P) (n : ℤ) :
            annealedSigmaAtScale P n = hP.barSigmaAtScale hStruct n • 1

            The structural-law scalar \bar\sigma_n scalarizes the annealed matrix.

            source
            theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.annealedSigmaStarAtScale_eq_barSigmaStarAtScale {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hStruct : RestrictionStructuralLaw P) (n : ℤ) :
            annealedSigmaStarAtScale P n = hP.barSigmaStarAtScale hStruct n • 1

            The structural-law scalar \bar\sigma_{*,n} scalarizes the annealed starred matrix.

            source
            theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.annealedBAtScale_eq_barBAtScale {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hStruct : RestrictionStructuralLaw P) (n : ℤ) :
            annealedBAtScale P n = hP.barBAtScale hStruct n • 1

            The structural-law scalar \bar b_n scalarizes the annealed upper-left block.

            source
            theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.annealedSigmaStarInvAtScale_eq_barSigmaStarInvAtScale {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hStruct : RestrictionStructuralLaw P) (n : ℤ) :
            annealedSigmaStarInvAtScale P n = hP.barSigmaStarInvAtScale hStruct n • 1

            The structural-law scalar \bar\sigma_{*,n}^{-1} scalarizes the annealed inverse-star matrix.

            source
            theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.barSigmaAtScale_eq_barBAtScale {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hStruct : RestrictionStructuralLaw P) (n : ℤ) :
            hP.barSigmaAtScale hStruct n = hP.barBAtScale hStruct n

            Under the structural law, the scalarized conductivity agrees with the primitive upper-left scalar.

            source
            theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.barSigmaStarAtScale_eq_inv_barSigmaStarInvAtScale {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hStruct : RestrictionStructuralLaw P) (n : ℤ) :
            hP.barSigmaStarAtScale hStruct n = (hP.barSigmaStarInvAtScale hStruct n)⁻¹

            Under the structural law, \bar\sigma_{*,n} is the inverse of the primitive inverse-star scalar.

            source
            theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.annealedKappaAtScale_eq_zero {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hStruct : RestrictionStructuralLaw P) (n : ℤ) :
            annealedKappaAtScale P n = 0

            Under the structural law, the annealed coupling matrix vanishes.

            source
            theorem HCPolySupport.Book.Ch04.Internal.thetaAtScale_eq_scalarization_contrast {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hStruct : RestrictionStructuralLaw P) (n : ℤ) :
            hP.thetaAtScale hStruct n = ⋯.contrast n

            Internal compatibility between the structural-law contrast and the scalarization route contrast.