High-contrast homogenization:

Provider.PolynomialHomogenization.Root.RowSupply.PhysicalFluxResponseCapPrice

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

Physical-cell flux-response cap price

For zero forcing, the coarse flux-response right-hand side is exactly a cube response multiplied by the forced-solution energy. The exponent-gap estimate converts the outer-one response at the regularity order to the supplied outer-two response at a lower order before the Whitney cells are summed.

noncomputable def HCPolySupport.HighContrast.RowSupply.ruledPhysicalFluxResponseBoundEnergyProduct {d : ℕ} {U : Set (Vec d)} {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (b r Cflux : ℝ) (responseBound : system.CellIndex → ℝ) (aCell : system.CellIndex → Book.Ch03.CoeffFamily d) (wCell : (i : system.CellIndex) → Book.Ch03.ForcedCubeSolution (whitneyCellCube system i) (aCell i) 0) (i : system.CellIndex) : ℝ

The physical-cell response--energy product after inserting a supplied outer-two response bound.

Equations

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

noncomputable def HCPolySupport.HighContrast.RowSupply.ruledPhysicalFluxResponseBoundEnergyCellEnergy {d : ℕ} {U : Set (Vec d)} {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (b r Cflux : ℝ) (responseBound : system.CellIndex → ℝ) (aCell : system.CellIndex → Book.Ch03.CoeffFamily d) (wCell : (i : system.CellIndex) → Book.Ch03.ForcedCubeSolution (whitneyCellCube system i) (aCell i) 0) (i : system.CellIndex) : ENNReal

The squared physical-cell response--energy contribution.

Equations

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

theorem HCPolySupport.HighContrast.RowSupply.physicalFluxResponseCap_le_responseBoundEnergyRow {d : ℕ} [NeZero d] {U : Set (Vec d)} {rho Rad b r Cflux : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (responseBound : system.CellIndex → ℝ) (aCell : system.CellIndex → Book.Ch03.CoeffFamily d) (wCell : (i : system.CellIndex) → Book.Ch03.ForcedCubeSolution (whitneyCellCube system i) (aCell i) 0) (hb : 0 < b) (hbr : b < r) (hCflux : 0 ≤ Cflux) (hResponse : ∀ (i : system.CellIndex), Book.Ch02.HomogenizationErrorOnCube (whitneyCellCube system i) b Book.Ch02.MultiscaleExponent.infinity (Book.Ch02.MultiscaleExponent.finite 2) (aCell i) (identityConstantCoeffMatrix d).matrix ≤ responseBound i) : (normalizedWhitneyRowEnergy system fun (i : system.CellIndex) => ENNReal.ofReal (physicalDualBesovScaleFactor (whitneyCellCube system i) r * Book.Ch03.coarseFluxResponseWithRHSRHS Cflux (whitneyCellCube system i) (aCell i) (identityConstantCoeffMatrix d) r 0 (wCell i)) ^ 2) ≤ normalizedWhitneyRowEnergy system (ruledPhysicalFluxResponseBoundEnergyCellEnergy system b r Cflux responseBound aCell wCell)

A response bound on each physical cell prices the exact coarse-response cap used by the four-row join.