High-contrast homogenization:

Provider.PolynomialHomogenization.Root.RowSupply.PhysicalCellSolutionEnergyAggregation

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

Aggregation of physical cell-solution energies

The normalized sum of the forced-solution energies on the selected cells is the normalized coefficient energy of the physical solution on the domain. This is a measure-theoretic consequence of the disjoint cell covering.

theorem HCPolySupport.HighContrast.RowSupply.volume_mul_cellSolutionEnergy_eq_physicalEnergyIntegral {d : ℕ} [NeZero d] {U : Set (Vec d)} {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (aPhysical : CoeffField d) (u : H1Function U) (aCell : system.CellIndex → Book.Ch03.CoeffFamily d) (wCell : (i : system.CellIndex) → Book.Ch03.ForcedCubeSolution (whitneyCellCube system i) (aCell i) 0) (hfamily : RuledCellPhysicalForcedFamily system aPhysical u aCell wCell) (i : system.CellIndex) : MeasureTheory.volume (system.cell i) * ENNReal.ofReal (Book.Ch03.forcedSolutionEnergyNorm (whitneyCellCube system i) (aCell i) (wCell i)) ^ 2 = ∫⁻ (x : Vec d) in system.cell i, ENNReal.ofReal (coefficientEnergyDensity aPhysical u.grad x)

On one selected cell, its volume times the squared normalized solution energy is the integral of the physical coefficient-energy density.

theorem HCPolySupport.HighContrast.RowSupply.physicalCellSolutionEnergyRow_eq_physicalEnergyAverage {d : ℕ} [NeZero d] {U : Set (Vec d)} {rho Rad : ℝ} (hd : 1 ≤ d) (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (hU : IsOpenBoundedConvexDomain U) (aPhysical : CoeffField d) (u : H1Function U) (aCell : system.CellIndex → Book.Ch03.CoeffFamily d) (wCell : (i : system.CellIndex) → Book.Ch03.ForcedCubeSolution (whitneyCellCube system i) (aCell i) 0) (hfamily : RuledCellPhysicalForcedFamily system aPhysical u aCell wCell) : physicalCellSolutionEnergyRow system aCell wCell = eVolumeAverage U fun (x : Vec d) => ENNReal.ofReal (coefficientEnergyDensity aPhysical u.grad x)

Disjointness and almost-everywhere covering identify the normalized cell energy row with the normalized physical coefficient energy on the domain.

theorem HCPolySupport.HighContrast.RowSupply.physicalCellSolutionEnergyRow_le_of_physicalEnergyAverage_le {d : ℕ} [NeZero d] {U : Set (Vec d)} {rho Rad : ℝ} (hd : 1 ≤ d) (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (hU : IsOpenBoundedConvexDomain U) (aPhysical : CoeffField d) (u : H1Function U) (aCell : system.CellIndex → Book.Ch03.CoeffFamily d) (wCell : (i : system.CellIndex) → Book.Ch03.ForcedCubeSolution (whitneyCellCube system i) (aCell i) 0) (hfamily : RuledCellPhysicalForcedFamily system aPhysical u aCell wCell) {Kenergy : ℝ} {boundaryEnergy : ENNReal} (henergy : (eVolumeAverage U fun (x : Vec d) => ENNReal.ofReal (coefficientEnergyDensity aPhysical u.grad x)) ≤ ENNReal.ofReal Kenergy * boundaryEnergy) : physicalCellSolutionEnergyRow system aCell wCell ≤ ENNReal.ofReal Kenergy * boundaryEnergy

Any global physical-energy estimate immediately supplies the energy-row premise of the response-rate aggregation theorem.