High-contrast homogenization: Provider.Regularity.CorrectorClassEnergy #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Symmetric energy of a local corrector class #
The normalized symmetric energy is defined directly on the local Hilbert
L² class. Raw-field characterizations are stated only after a caller
supplies a representative and its L² witness.
Generic quotient-carrier energy #
noncomputable def
HCPolySupport.HighContrast.normalizedLocalSymmetricEnergy
{d : ℕ}
{U : Set (Vec d)}
{b : CoeffField d}
{lam Lam : ℝ}
(hEll : IsEllipticFieldOn lam Lam U b)
(F : ↥(HilbertVectorL2 U))
:
The volume-normalized symmetric coefficient energy of a local Hilbert
vector L² class.
Equations
Instances For
theorem
HCPolySupport.HighContrast.normalizedLocalSymmetricEnergy_eq_volumeAverage
{d : ℕ}
{U : Set (Vec d)}
{b : CoeffField d}
{lam Lam : ℝ}
(hEll : IsEllipticFieldOn lam Lam U b)
{f : Vec d → Vec d}
(hf : MemVectorL2 U f)
:
On an explicitly supplied raw representative, the quotient-class energy is the literal normalized coefficient-energy average.
theorem
HCPolySupport.HighContrast.ofReal_normalizedLocalSymmetricEnergy_eq_weightedGradNorm_sq
{d : ℕ}
{U : Set (Vec d)}
{b : CoeffField d}
{lam Lam : ℝ}
(hEll : IsEllipticFieldOn lam Lam U b)
{f : Vec d → Vec d}
(hf : MemVectorL2 U f)
:
ENNReal.ofReal (normalizedLocalSymmetricEnergy hEll (toHilbertVectorL2OfVecField hf)) = weightedGradNorm b U f ^ 2
The real class energy is exactly the square of the weighted
gradient norm after conversion to ℝ≥0∞.
theorem
HCPolySupport.HighContrast.normalizedLocalSymmetricEnergy_nonneg
{d : ℕ}
{U : Set (Vec d)}
{b : CoeffField d}
{lam Lam : ℝ}
(hEll : IsEllipticFieldOn lam Lam U b)
(F : ↥(HilbertVectorL2 U))
:
The normalized symmetric energy is nonnegative on every quotient class.
theorem
HCPolySupport.HighContrast.continuous_normalizedLocalSymmetricEnergy
{d : ℕ}
{U : Set (Vec d)}
{b : CoeffField d}
{lam Lam : ℝ}
(hEll : IsEllipticFieldOn lam Lam U b)
:
Continuous fun (F : ↥(HilbertVectorL2 U)) => normalizedLocalSymmetricEnergy hEll F
The quotient-class symmetric energy is continuous.