High-contrast homogenization:

Provider.PolynomialHomogenization.Root.RowSupply.PhysicalFluxRateAggregationReduction

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

Physical flux-response rate aggregation

The cellwise response coefficient and the cellwise solution energy are kept separate. A uniform physical-frame estimate for the former and a normalized energy-row estimate for the latter combine without any further analytic input.

noncomputable def HCPolySupport.HighContrast.RowSupply.ruledPhysicalFluxResponseCoefficient {d : ℕ} {U : Set (Vec d)} {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (b r Cflux : ℝ) (responseBound : system.CellIndex → ℝ) (i : system.CellIndex) : ℝ

The response-dependent coefficient in the physical flux price, before the solution energy is inserted.

Equations

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

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

A physical-frame response estimate is a uniform power bound on the whole coefficient multiplying the cell solution energy.

Equations

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

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

The normalized row of squared cell-solution energies.

Equations

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

theorem HCPolySupport.HighContrast.RowSupply.responseBoundEnergyRow_le_frame_mul_solutionEnergyRow {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) {epsilon Xval kappaRate Kframe : ℝ} (hbase : 0 ≤ epsilon * Xval) (hframe : PhysicalFluxEpsilonFrameBound system b r Cflux responseBound epsilon Xval kappaRate Kframe) : normalizedWhitneyRowEnergy system (ruledPhysicalFluxResponseBoundEnergyCellEnergy system b r Cflux responseBound aCell wCell) ≤ ENNReal.ofReal (Kframe * (epsilon * Xval) ^ kappaRate) ^ 2 * physicalCellSolutionEnergyRow system aCell wCell

A uniform response factor pulls out of the normalized physical-cell row.

theorem HCPolySupport.HighContrast.RowSupply.physicalFluxResponseRateAggregation {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) {epsilon Xval kappaRate Kframe Kenergy : ℝ} {boundaryEnergy : ENNReal} (hbase : 0 ≤ epsilon * Xval) (hframe : PhysicalFluxEpsilonFrameBound system b r Cflux responseBound epsilon Xval kappaRate Kframe) (hKenergy : 0 ≤ Kenergy) (henergy : physicalCellSolutionEnergyRow system aCell wCell ≤ ENNReal.ofReal Kenergy * boundaryEnergy) : 0 ≤ Kframe ^ 2 * Kenergy ∧ normalizedWhitneyRowEnergy system (ruledPhysicalFluxResponseBoundEnergyCellEnergy system b r Cflux responseBound aCell wCell) ≤ ENNReal.ofReal (Kframe ^ 2 * Kenergy * (epsilon * Xval) ^ (2 * kappaRate)) * boundaryEnergy

The frame estimate and an energy-row estimate give the required squared power rate with an explicit product constant.