Documentation

LeanPool.HighContrastHomogenization.Provider.Response.ProfileRowCarriers

High-contrast homogenization: Provider.Response.ProfileRowCarriers #

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

All-earlier response-row carriers #

This file records the Schur load, its finite lower-cutoff rows, the fail-closed all-earlier row, and the response-row constant assembled from the drift and the source row. The adjoint block is the coefficient-transpose sign congruence; it is distinct from the sharp block reflection used by source control.

source
def HCPolySupport.HighContrast.Response.profileAdjointBlock {d : ℕ} (H : BlockMat d) :
BlockMat d

The coefficient-transpose image of a doubled response block.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def HCPolySupport.HighContrast.Response.profileRowWeight (k s : ℤ) :
    ℝ

    The geometric response-row weight at scale k relative to s.

    Equations
    Instances For
      source
      noncomputable def HCPolySupport.HighContrast.Response.profileSchurLoad {d : ℕ} (H : BlockMat d) (Pcen Qcen : Vec d) :
      ℝ

      The Schur diagonal load of a block at a pair of independent centers. The two actual carriers are the top-left block and schurSigmaStar; the inverse square root in the second slot is therefore written literally.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def HCPolySupport.HighContrast.Response.profileQuadraticLoad {d : ℕ} (H : BlockMat d) (Pcen Qcen : Vec d) :
        ℝ

        The two diagonal quadratic forms comprising the row load.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def HCPolySupport.HighContrast.Response.profileRowGamma {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (rhoDr : ℝ) (q : Mat d) (Cd g : ℝ) (E : BlockMat d) (jStar : ℤ) (m0 : Mat d) (s : ℤ) :
          ℝ

          The cap-two response coefficient Γ_s^ᵎ.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem HCPolySupport.HighContrast.Response.profileRowGamma_eq {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (rhoDr : ℝ) (q : Mat d) (Cd g : ℝ) (E : BlockMat d) (jStar : ℤ) (m0 : Mat d) (s : ℤ) :
            profileRowGamma P rhoDr q Cd g E jStar m0 s = (1 + linearDrift P rhoDr q jStar s) / (1 - 3 ^ (-(3 / 2))) + kappaRef E * boundaryConst Cd g m0 ^ 2 * 2 ^ 2 / (3 ^ (3 / 2 - g) - 1) * 3 ^ (-(3 / 2) * (↑s - ↑jStar))