Documentation

LeanPool.HighContrastHomogenization.Provider.Response.ProfileRowSkewCarriers

High-contrast homogenization: Provider.Response.ProfileRowSkewCarriers #

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

Fixed-skew all-earlier response-row carriers #

The response profile is written for the recentered coefficient. Its annealed blocks are therefore the common shear congruences of the original annealed blocks. Coefficient transposition is applied only after this congruence.

source
def HCPolySupport.HighContrast.Response.profileHattedBlock {d : ℕ} (h : Mat d) (H : BlockMat d) :
BlockMat d

The hatted block G_hᵀ H G_h.

Equations
Instances For
    source
    def HCPolySupport.HighContrast.Response.profileHattedAdjointBlock {d : ℕ} (h : Mat d) (H : BlockMat d) :
    BlockMat d

    The coefficient-transpose image of a hatted block.

    Equations
    Instances For
      source
      theorem HCPolySupport.HighContrast.Response.profileHattedBlock_adaptedMean {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (q h : Mat d) (k : ℤ) :
      profileHattedBlock h (adaptedMean P q k) = profileRecenteredMean P q h k

      The hatted terminal block is the recentered adapted mean.

      source
      theorem HCPolySupport.HighContrast.Response.profileHattedAdjointBlock_adaptedMean {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (q h : Mat d) (k : ℤ) :
      profileHattedAdjointBlock h (adaptedMean P q k) = profileRecenteredAdjointMean P q h k

      The hatted adjoint terminal block is the recentered adjoint mean.

      source
      noncomputable def HCPolySupport.HighContrast.Response.profilePrimalHattedRowPartial {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (q h : Mat d) (Klo s : ℤ) (Pcen Qcen : Vec d) :
      ℝ

      A finite lower-cutoff primal row of hatted Schur loads.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def HCPolySupport.HighContrast.Response.profileAdjointHattedRowPartial {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (q h : Mat d) (Klo s : ℤ) (Pcen Qcen : Vec d) :
        ℝ

        A finite lower-cutoff coefficient-transpose row of hatted Schur loads.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def HCPolySupport.HighContrast.Response.profilePrimalHattedEarlierRow {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (q h : Mat d) (s : ℤ) (Pcen Qcen : Vec d) :
          ENNReal

          The primal all-earlier hatted row. Divergence is represented by ⊤.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            noncomputable def HCPolySupport.HighContrast.Response.profileAdjointHattedEarlierRow {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (q h : Mat d) (s : ℤ) (Pcen Qcen : Vec d) :
            ENNReal

            The adjoint all-earlier hatted row. Divergence is represented by ⊤ independently of the primal row.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For