Coarse-graining support: Support.Book.Ch03.Theorems.PublicInternalBridges.Energy

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Public energy bridges for Chapter 3

This file contains the energy-density and energy-norm identities that convert public a.e. coefficient data to deterministic pointwise coefficient fields.

theorem HCPolySupport.Book.Ch03.volumeAverage_eq_of_ae_eq {d : ℕ} {U : Set (Vec d)} {f g : Vec d → ℝ} (hfg : f =ᵐ[volumeMeasureOn U] g) : volumeAverage U f = volumeAverage U g

theorem HCPolySupport.Book.Ch03.localizedCoeffEnergyValue_eq_volumeAverage_coefficientEnergyDensity {d : ℕ} {U : Ch02.Domain d} (V : Set (Vec d)) (a : Ch02.CoeffOn U) (u : H1Function U.carrier) : localizedCoeffEnergyValue V a u = volumeAverage V (coefficientEnergyDensity a.toCoeffField u.grad)

theorem HCPolySupport.Book.Ch03.cubeAverage_coefficientEnergyDensity_publicCoeffField_eq_localizedCoeffEnergyValue {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) (u : H1Function (Ch02.cubeDomain Q).carrier) : cubeAverage Q (coefficientEnergyDensity (publicCoeffField Q a) u.grad) = localizedCoeffEnergyValue (openCubeSet Q) (a.coeffOn Q) u

theorem HCPolySupport.Book.Ch03.h1EnergyNormOnCube_eq_sqrt_cubeAverage_coefficientEnergyDensity_publicCoeffField {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) (u : H1Function (Ch02.cubeDomain Q).carrier) : h1EnergyNormOnCube Q a u = √(cubeAverage Q (coefficientEnergyDensity (publicCoeffField Q a) u.grad))

theorem HCPolySupport.Book.Ch03.forcedSolutionEnergyNorm_eq_sqrt_cubeAverage_coefficientEnergyDensity_publicCoeffField {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) {g : Vec d → Vec d} (u : ForcedCubeSolution Q a g) : forcedSolutionEnergyNorm Q a u = √(cubeAverage Q (coefficientEnergyDensity (publicCoeffField Q a) (forcedSolutionGradientField u)))

theorem HCPolySupport.Book.Ch03.forcedSolution_energyNorm_eq_sqrt_coefficientEnergy {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) {g : Vec d → Vec d} (u : ZeroTraceForcedCubeSolution Q a g) : zeroTraceForcedSolutionEnergyNorm Q a u = √(cubeAverage Q (coefficientEnergyDensity (publicCoeffField Q a) u.toH10.grad))

theorem HCPolySupport.Book.Ch03.dirichletForced_energyNorm_eq_sqrt_coefficientEnergy {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) {g : Vec d → Vec d} (u : DirichletForcedCubeSolution Q a g) : dirichletForcedSolutionEnergyNorm Q a u = √(cubeAverage Q (coefficientEnergyDensity (publicCoeffField Q a) u.toH1.grad))

theorem HCPolySupport.Book.Ch03.neumannForcedSolutionEnergyNorm_eq_sqrt_cubeAverage_coefficientEnergyDensity_publicCoeffField {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) {g : Vec d → Vec d} (u : NeumannForcedCubeSolution Q a g) : neumannForcedSolutionEnergyNorm Q a u = √(cubeAverage Q (coefficientEnergyDensity (publicCoeffField Q a) u.toH1MeanZero.toH1Function.grad))