Documentation

LeanPool.HighContrastHomogenization.Provider.Response.CenteredResponseTrace

High-contrast homogenization: Provider.Response.CenteredResponseTrace #

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

The exact centered-response trace identity #

The combined primal--adjoint response at a response-adapted unit load is a quadratic form in that unit vector. Summing it over the standard basis gives exactly trace X + 2 * trace Y.

source
noncomputable def HCPolySupport.HighContrast.Response.centeredResponseTraceValue {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (U : Book.Ch02.Domain d) (S SStar K : Mat d) (e : Vec d) :
ℝ

The primal--adjoint response sum at the response-adapted load generated by e.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def HCPolySupport.HighContrast.Response.centeredResponseTraceMatrix {d : ℕ} (S SStar K : Mat d) :
    Mat d

    The matrix whose quadratic form is the response sum.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem HCPolySupport.HighContrast.Response.centeredResponseTraceValue_eq_quadratic {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (U : Book.Ch02.Domain d) (hint : HasIntegrableCoarseBlock P U.carrier) {S SStar K : Mat d} (hS : Matrix.PosDef S) (hStar : Matrix.PosDef SStar) (hE : toFullBlockMat (annealedBlock P U.carrier) = schurBlock S SStar K) (e : Vec d) :
      centeredResponseTraceValue P U S SStar K e = e ⬝ᵥ Matrix.mulVec (centeredResponseTraceMatrix S SStar K) e

      The response sum is the quadratic form of centeredResponseTraceMatrix.

      source
      theorem HCPolySupport.HighContrast.Response.trace_centeredResponseTraceMatrix {d : ℕ} {S SStar : Mat d} (hS : Matrix.PosDef S) (hStar : Matrix.PosDef SStar) (K : Mat d) :
      Matrix.trace (centeredResponseTraceMatrix S SStar K) = Matrix.trace (centeredResponseX S SStar) + 2 * Matrix.trace (centeredResponseY SStar K)

      The trace matrix has trace trace X + 2 trace Y.

      source
      theorem HCPolySupport.HighContrast.Response.sum_centeredResponseTraceValue {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (U : Book.Ch02.Domain d) (hint : HasIntegrableCoarseBlock P U.carrier) {S SStar K : Mat d} (hS : Matrix.PosDef S) (hStar : Matrix.PosDef SStar) (hE : toFullBlockMat (annealedBlock P U.carrier) = schurBlock S SStar K) :
      ∑ i : Fin d, centeredResponseTraceValue P U S SStar K (Pi.single i 1) = Matrix.trace (centeredResponseX S SStar) + 2 * Matrix.trace (centeredResponseY SStar K)

      The exact standard-basis sum of the response values.