High-contrast homogenization: Provider.Response.AffineResponseDifferenceEnergy

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

Difference energy for a common coefficient representative

When every descendant cube carries the same coefficient representative as its parent, the parent canonical response solution restricts to every descendant. The one-cube second-variation identity then sums exactly to the response partition defect.

theorem HCPolySupport.HighContrast.Response.descendantsAverage_additivityDiffHalfEnergy_eq_responseJPartitionDefect_of_commonCoeff {d : ℕ} (F : Book.Ch02.TriadicCoeffFamily d) (Q : TriadicCube d) (j : ℕ) (p r : Vec d) (hcommon : ∀ R ∈ descendantsAtDepth Q j, (F.coeffOn R).toCoeffField = (F.coeffOn Q).toCoeffField) : (descendantsAverage Q j fun (R : TriadicCube d) => cubeAverage R (Book.Ch05.Section53.JUpperBoundWeakNorms.additivityDiffHalfEnergyDensityOnFamilyOnCube F Q R p r)) = Book.Ch05.Section53.JUpperBoundWeakNorms.responseJPartitionDefectOnFamilyAtDepth F Q j p r

For a family with one exact coefficient representative on a parent and all of its descendants, the averaged gradient-difference half-energy is exactly the child-minus-parent response defect.