Documentation

LeanPool.HighContrastHomogenization.Support.Internal.Ch02.Adapters

Coarse-graining support: Support.Internal.Ch02.Adapters #

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

source
theorem HCPolySupport.Internal.Ch02.book_average_eq_volumeAverage {d : ℕ} (U : Book.Ch02.Domain d) (f : Vec d → ℝ) :
Book.Ch02.average U f = volumeAverage U.carrier f

The public Chapter 2 average is definitionally the old volume average.

source
theorem HCPolySupport.Internal.Ch02.book_responseIntegrand_eq_scalarResponseIntegrand {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (p q : Vec d) (v : Book.Ch02.Solution U a) :
Book.Ch02.responseIntegrand U a p q v = scalarResponseIntegrand U.carrier a.toCoeffField p q v

The public Chapter 2 response integrand is definitionally the old scalar response integrand.

source
theorem HCPolySupport.Internal.Ch02.book_responseValue_eq_volumeAverage_scalarResponseIntegrand {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (p q : Vec d) (v : Book.Ch02.Solution U a) :
Book.Ch02.responseValue U a p q v = volumeAverage U.carrier (scalarResponseIntegrand U.carrier a.toCoeffField p q v)

Adapter from the new public response value to the old proof-engine value.

source
theorem HCPolySupport.Internal.Ch02.book_responseValueSet_eq_responseJValueSet {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (p q : Vec d) :
Book.Ch02.responseValueSet U a p q = responseJValueSet U.carrier p q a.toCoeffField

The public value set is the old value set, behind the internal boundary.

source
theorem HCPolySupport.Internal.Ch02.book_responseJ_eq_ResponseJ {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (p q : Vec d) :
Book.Ch02.responseJ U a p q = ResponseJ U.carrier p q a.toCoeffField

The public response functional is the old response functional, internally.

source
theorem HCPolySupport.Internal.Ch02.book_sigmaStarInvCoarse_eq_sigmaStarInvCoarse {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) :
Book.Ch02.sigmaStarInvCoarse U a = sigmaStarInvCoarse U.carrier a.toCoeffField

The public sigmaStarInv matrix is the old canonical matrix, internally.

source
theorem HCPolySupport.Internal.Ch02.book_sigmaStarInvKappaCoarse_eq_sigmaStarInvKappaCoarse {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) :
Book.Ch02.sigmaStarInvKappaCoarse U a = sigmaStarInvKappaCoarse U.carrier a.toCoeffField

The public mixed-response matrix is the old canonical mixed matrix, internally.

source
theorem HCPolySupport.Internal.Ch02.book_sigmaStarCoarse_eq_sigmaStarCoarse {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) :
Book.Ch02.sigmaStarCoarse U a = sigmaStarCoarse U.carrier a.toCoeffField

The public sigmaStar matrix is the old canonical matrix, internally.

source
theorem HCPolySupport.Internal.Ch02.book_kappaCoarse_eq_kappaCoarse {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) :
Book.Ch02.kappaCoarse U a = kappaCoarse U.carrier a.toCoeffField

The public kappa matrix is the old canonical matrix, internally.

source
theorem HCPolySupport.Internal.Ch02.book_canonicalSigmaCorrectedResponse_eq_sigmaCorrectedResponse {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (p : Vec d) :
Book.Ch02.canonicalSigmaCorrectedResponse U a p = sigmaCorrectedResponse U.carrier a.toCoeffField p

The public corrected sigma response is the old corrected response, internally.

source
theorem HCPolySupport.Internal.Ch02.book_sigmaCoarse_eq_sigmaCoarse {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) :
Book.Ch02.sigmaCoarse U a = sigmaCoarse U.carrier a.toCoeffField

The public sigma matrix is the old canonical matrix, internally.

source
theorem HCPolySupport.Internal.Ch02.book_averagedSymmPartInv_eq_averagedSymmPartInv {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) :
Book.Ch02.averagedSymmPartInv U a = averagedSymmPartInv U.carrier a.toCoeffField

The public harmonic-mean average is the old averaged inverse symmetric part, internally.

source
theorem HCPolySupport.Internal.Ch02.book_averagedSymmPartPlusCorrection_eq_averagedSymmPartPlusCorrection {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) :
Book.Ch02.averagedSymmPartPlusCorrection U a = averagedSymmPartPlusCorrection U.carrier a.toCoeffField

The public upper coefficient average is the old averaged upper-left coefficient, internally.

source
theorem HCPolySupport.Internal.Ch02.book_coarseMatrices_b_eq_bCoarse_of_isSigmaStarCoarse {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (hS : IsSigmaStarCoarse U.carrier a.toCoeffField (sigmaStarCoarse U.carrier a.toCoeffField)) :
(Book.Ch02.coarseMatrices U a).b = bCoarse (sigmaCoarse U.carrier a.toCoeffField) (sigmaStarCoarse U.carrier a.toCoeffField) (kappaCoarse U.carrier a.toCoeffField)

The public derived b matrix is the old canonical bCoarse, once the old sigmaStar witness identifies its inverse with sigmaStarInvCoarse.