High-contrast homogenization:

Provider.PolynomialHomogenization.Root.EnergyPrice.TranslatedCubeEnergyPrice

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

Gate R1: the price on a translate of a triadic cube

At the frozen witness the gauge domain is a translate by an arbitrary real vector of a triadic cube (matImage_inv_affineImage), and the Chapter 3 cube carriers (CoeffFamily, IsForcedEquation, DirichletForcedCubeSolution) are hard-indexed by genuine TriadicCubes, so the estimate must be transported rather than restated.

This file supplies the transport for the two carriers the price uses — the extended-real coefficient-energy average and the Euclidean fractional norm — and assembles the translated-cube inhabitant of GaugePhysicalEnergyPriceAtWitness.

eVolumeAverage_translateSet and its lintegral helper exist only as private declarations elsewhere, so they are re-proved here.

Translation transport of the extended-real carriers

theorem HCPolySupport.HighContrast.EnergyPrice.lintegral_translateSet {d : ℕ} (z : Vec d) (V : Set (Vec d)) (g : Vec d → ENNReal) : ∫⁻ (x : Vec d) in translateSet z V, g x = ∫⁻ (x : Vec d) in V, g (x + z)

Lower integrals transport along a translation.

theorem HCPolySupport.HighContrast.EnergyPrice.eVolumeAverage_translateSet {d : ℕ} (z : Vec d) (V : Set (Vec d)) (g : Vec d → ENNReal) : eVolumeAverage (translateSet z V) g = eVolumeAverage V fun (x : Vec d) => g (x + z)

Volume averages transport along a translation.

theorem HCPolySupport.HighContrast.EnergyPrice.eVolumeAverage_coefficientEnergyDensity_translateSet {d : ℕ} (z : Vec d) (V : Set (Vec d)) (b : CoeffField d) (F : Vec d → Vec d) : (eVolumeAverage (translateSet z V) fun (x : Vec d) => ENNReal.ofReal (coefficientEnergyDensity b F x)) = eVolumeAverage V fun (y : Vec d) => ENNReal.ofReal (coefficientEnergyDensity (fun (w : Vec d) => b (w + z)) (fun (w : Vec d) => F (w + z)) y)

The energy average on a translated set.

theorem HCPolySupport.HighContrast.EnergyPrice.hsNormSq_translateSet_add {d : ℕ} (z : Vec d) (V : Set (Vec d)) (s : ℝ) (F : Vec d → Vec d) : hsNormSq (translateSet z V) s F = hsNormSq V s fun (x : Vec d) => F (x + z)

The fractional norm on a translated set, in the F (· + z) direction.

The translated-cube price