Documentation

LeanPool.HighContrastHomogenization.Provider.Response.ProfileDefectCarriers

High-contrast homogenization: Provider.Response.ProfileDefectCarriers #

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

Positive response-defect carriers #

The response defects compare the annealed variational values on two adapted cells after a fixed skew recentering. The primal and coefficient-transpose problems retain separate load pairs.

source
noncomputable def HCPolySupport.HighContrast.Response.profileRecenteredMean {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (q g : Mat d) (k : ℤ) :
BlockMat d

The recentered annealed block Ê_k = G_gᵀ E_k G_g.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def HCPolySupport.HighContrast.Response.profileRecenteredAdjointMean {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (q g : Mat d) (k : ℤ) :
    BlockMat d

    The coefficient-transpose recentered mean Ê_kᵃᵈ = D Ê_k D.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem HCPolySupport.HighContrast.Response.profileRecenteredAdjointMean_eq {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (q g : Mat d) (k : ℤ) :
      profileRecenteredAdjointMean P q g k = Book.Ch02.blockMatMul (Book.Ch02.blockDiag 1 (-1)) (Book.Ch02.blockMatMul (profileRecenteredMean P q g k) (Book.Ch02.blockDiag 1 (-1)))

      The defining equation for the coefficient-transpose recentered mean.

      source
      noncomputable def HCPolySupport.HighContrast.Response.profilePrimalResponseDefect {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) {q : Mat d} (hq : Matrix.PosDef q) (g : Mat d) (hg : IsSkewMat g) (s t : ℤ) (p r : Vec d) :
      ℝ

      The primal positive response defect τ⁻_{t,s}.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem HCPolySupport.HighContrast.Response.profilePrimalResponseDefect_eq {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) {q : Mat d} (hq : Matrix.PosDef q) (g : Mat d) (hg : IsSkewMat g) (s t : ℤ) (p r : Vec d) :
        profilePrimalResponseDefect P hq g hg s t p r = ∫ (a : CoeffSpace d), Book.Ch02.responseJ (adaptedDomain hq s) ((a.subSkew g hg).coeffOn (adaptedDomain hq s)) p r - Book.Ch02.responseJ (adaptedDomain hq t) ((a.subSkew g hg).coeffOn (adaptedDomain hq t)) p r ∂P

        The defining equation for τ⁻_{t,s}.

        source
        noncomputable def HCPolySupport.HighContrast.Response.profileAdjointResponseDefect {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) {q : Mat d} (hq : Matrix.PosDef q) (g : Mat d) (hg : IsSkewMat g) (s t : ℤ) (p r : Vec d) :
        ℝ

        The coefficient-transpose positive response defect τ⁺_{t,s}.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem HCPolySupport.HighContrast.Response.profileAdjointResponseDefect_eq {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) {q : Mat d} (hq : Matrix.PosDef q) (g : Mat d) (hg : IsSkewMat g) (s t : ℤ) (p r : Vec d) :
          profileAdjointResponseDefect P hq g hg s t p r = ∫ (a : CoeffSpace d), Book.Ch02.responseJ (adaptedDomain hq s) ((a.subSkew g hg).transpose.coeffOn (adaptedDomain hq s)) p r - Book.Ch02.responseJ (adaptedDomain hq t) ((a.subSkew g hg).transpose.coeffOn (adaptedDomain hq t)) p r ∂P

          The defining equation for τ⁺_{t,s}.