Documentation

LeanPool.HighContrastHomogenization.Provider.PolynomialHomogenization.Root.RowSupply.FormulaicAnchoredObservationToPhysicalFluxRate

High-contrast homogenization: #

Provider.PolynomialHomogenization.Root.RowSupply.FormulaicAnchoredObservationToPhysicalFluxRate

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

Observation response to the physical flux rate #

The ruled observation cube contains the centered physical cell at one finer generation. The corresponding fixed factor is inserted into the frame bound before the response--energy aggregation is used.

source
theorem HCPolySupport.HighContrast.RowSupply.physicalFluxEpsilonFrameBound_const_mul {d : ℕ} {U : Set (Vec d)} {rho Rad b r Cflux : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (responseBound : system.CellIndex → ℝ) {epsilon Xval kappaRate Kframe factor : ℝ} (hfactor : 0 ≤ factor) (hframe : PhysicalFluxEpsilonFrameBound system b r Cflux responseBound epsilon Xval kappaRate Kframe) :
PhysicalFluxEpsilonFrameBound system b r Cflux (fun (i : system.CellIndex) => factor * responseBound i) epsilon Xval kappaRate (factor * Kframe)

Multiplying every response bound by a fixed nonnegative scalar multiplies the physical-frame constant by the same scalar.