Documentation

LeanPool.HighContrastHomogenization.Provider.Regularity.RoundedCenteredCoeffFamily

High-contrast homogenization: Provider.Regularity.RoundedCenteredCoeffFamily #

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

Chapter 3 family for the rounded centered coefficient #

The R3-A coefficient is first constructed on the almost-everywhere quotient carrier. This module packages that same quotient representative as one compatible Chapter 3 coefficient family and records its almost-everywhere identification with the literal rounded field.

source
theorem HCPolySupport.HighContrast.exists_coeffFamily_of_coeffSpace {d : ℕ} (a : CoeffSpace d) :
∃ (aRef : Book.Ch03.CoeffFamily d), ∀ (Q : TriadicCube d), (aRef.coeffOn Q).toCoeffField = ↑↑a

Every qualitative coefficient sample has a compatible Chapter 3 family whose representative is unchanged on every reference cube.