High-contrast homogenization:

Provider.PolynomialHomogenization.Root.RowSupply.CellAnchoredPhysicalFluxFrameAlgebra

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

Cell-anchored response to physical flux frame

The response estimate is kept with the physical scale of its observation cube. The difference between the response order and the consumed order is then bounded by the outer radius of the Whitney system.

def HCPolySupport.HighContrast.RowSupply.CellAnchoredObservationRateBound {d : ℕ} {U : Set (Vec d)} {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (b : ℝ) (responseBound : system.CellIndex → ℝ) (epsilon Xval kappaRate Kanchor : ℝ) : Prop

A cell-anchored response rate retains the observation cube's physical scale before the response is inserted into the flux price.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.RowSupply.physicalFluxEpsilonFrameBound_of_cellAnchoredObservationRate {d : ℕ} [NeZero d] {U : Set (Vec d)} {rho Rad b r Cflux : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (hU : IsOpen U) (hRad : 0 ≤ Rad) (hb : 0 < b) (hbr : b < r) (hCflux : 0 ≤ Cflux) (responseBound : system.CellIndex → ℝ) {epsilon Xval kappaRate Kanchor : ℝ} (hanchor : CellAnchoredObservationRateBound system b responseBound epsilon Xval kappaRate Kanchor) : PhysicalFluxEpsilonFrameBound system b r Cflux responseBound epsilon Xval kappaRate (Real.rpow 3 (-b) * (2 * Rad).rpow (r - b) * Cflux * r⁻¹ * Book.Ch03.constantCoeffMatrixNormHalf (identityConstantCoeffMatrix d) * responseOneFromTwoGapFactor b r * Kanchor)

A cell-anchored response rate gives the exact uniform physical flux frame. Only the order gap and the outer-radius bound are used.