High-contrast homogenization:

Provider.PolynomialHomogenization.Root.RowSupply.PhysicalCellResponseRealization

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

Physical-cell realization of observation response bounds

The observation and cell coefficient families may be constructed independently. Their local identifications with one physical coefficient, the centered-child relation, and translation covariance identify the cell response with the centered descendant response.

theorem HCPolySupport.HighContrast.RowSupply.physicalCellHomogenizationError_eq_centeredChild {d : ℕ} {U : Set (Vec d)} {rho Rad b : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (aObs aCell : system.CellIndex → Book.Ch02.TriadicCoeffFamily d) (f : system.CellIndex → CoeffField d) (hObs : ∀ (i : system.CellIndex), ((aObs i).coeffOn (ruledObservationCube system i)).toCoeffField =ᵐ[volumeMeasureOn (openCubeSet (ruledObservationCube system i))] translateCoeffField (ruledObservationCenter system i) (f i)) (hCell : ∀ (i : system.CellIndex), ((aCell i).coeffOn (whitneyCellCube system i)).toCoeffField =ᵐ[volumeMeasureOn (openCubeSet (whitneyCellCube system i))] f i) (i : system.CellIndex) : Book.Ch02.HomogenizationErrorOnCube (whitneyCellCube system i) b Book.Ch02.MultiscaleExponent.infinity (Book.Ch02.MultiscaleExponent.finite 2) (aCell i) (identityConstantCoeffMatrix d).matrix = Book.Ch02.HomogenizationErrorOnCube (originCube d (system.scale i)) b Book.Ch02.MultiscaleExponent.infinity (Book.Ch02.MultiscaleExponent.finite 2) (aObs i) (identityConstantCoeffMatrix d).matrix

Local identifications of the independently constructed observation and cell families give the exact translated centered-child response identity.

theorem HCPolySupport.HighContrast.RowSupply.physicalCellHomogenizationError_le_of_observationBound {d : ℕ} [NeZero d] {U : Set (Vec d)} {rho Rad b : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (hb : 0 < b) (aObs aCell : system.CellIndex → Book.Ch02.TriadicCoeffFamily d) (f : system.CellIndex → CoeffField d) (responseBound : system.CellIndex → ℝ) (hObs : ∀ (i : system.CellIndex), ((aObs i).coeffOn (ruledObservationCube system i)).toCoeffField =ᵐ[volumeMeasureOn (openCubeSet (ruledObservationCube system i))] translateCoeffField (ruledObservationCenter system i) (f i)) (hCell : ∀ (i : system.CellIndex), ((aCell i).coeffOn (whitneyCellCube system i)).toCoeffField =ᵐ[volumeMeasureOn (openCubeSet (whitneyCellCube system i))] f i) (hResponse : ∀ (i : system.CellIndex), Book.Ch02.HomogenizationErrorOnCube (ruledObservationCube system i) b Book.Ch02.MultiscaleExponent.infinity (Book.Ch02.MultiscaleExponent.finite 2) (aObs i) (identityConstantCoeffMatrix d).matrix ≤ responseBound i) (i : system.CellIndex) : Book.Ch02.HomogenizationErrorOnCube (whitneyCellCube system i) b Book.Ch02.MultiscaleExponent.infinity (Book.Ch02.MultiscaleExponent.finite 2) (aCell i) (identityConstantCoeffMatrix d).matrix ≤ Real.rpow 3 b * responseBound i

A response bound on every observation cube yields the exact physical-cell premise after the one-generation all-depth loss.