Documentation

LeanPool.HighContrastHomogenization.Provider.Response.ProfileMismatch

High-contrast homogenization: Provider.Response.ProfileMismatch #

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

Same-cell center mismatches #

The two mismatch scalars retain the primal and coefficient-transpose centers separately. Each center component is subtracted from the same componentwise annealed cell average that defines it, so both mismatches vanish exactly.

source
noncomputable def HCPolySupport.HighContrast.Response.profilePrimalSameCellMismatch {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (h0 : Mat d) (hh0 : IsSkewMat h0) (pMinus qMinus : Vec d) :
ℝ

The primal same-cell mismatch after a fixed skew recentering.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def HCPolySupport.HighContrast.Response.profileAdjointSameCellMismatch {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (h0 : Mat d) (hh0 : IsSkewMat h0) (pPlus qPlus : Vec d) :
    ℝ

    The coefficient-transpose same-cell mismatch after the same recentering.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem HCPolySupport.HighContrast.Response.profilePrimalSameCellMismatch_eq_zero {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (h0 : Mat d) (hh0 : IsSkewMat h0) (pMinus qMinus : Vec d) :
      profilePrimalSameCellMismatch P hq t h0 hh0 pMinus qMinus = 0

      The primal same-cell mismatch vanishes without a law-invariance hypothesis.

      source
      theorem HCPolySupport.HighContrast.Response.profileAdjointSameCellMismatch_eq_zero {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (h0 : Mat d) (hh0 : IsSkewMat h0) (pPlus qPlus : Vec d) :
      profileAdjointSameCellMismatch P hq t h0 hh0 pPlus qPlus = 0

      The coefficient-transpose same-cell mismatch vanishes without a law-invariance hypothesis.

      source
      theorem HCPolySupport.HighContrast.Response.profileSameCellMismatches_eq_zero {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (h0 : Mat d) (hh0 : IsSkewMat h0) (pMinus qMinus pPlus qPlus : Vec d) :
      profilePrimalSameCellMismatch P hq t h0 hh0 pMinus qMinus = 0 ∧ profileAdjointSameCellMismatch P hq t h0 hh0 pPlus qPlus = 0

      Both independently loaded same-cell mismatches vanish exactly.