Coarse-graining support: Support.PDE.EnergyIdentities

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

PDE energy identities

This file collects coefficient-weighted energy densities and weak-solution energy identities that are not specific to the Coarse Poincare recurrence.

noncomputable def HCPolySupport.coefficientEnergyDensity {d : ℕ} (a : CoeffField d) (F : Vec d → Vec d) : Vec d → ℝ

The intrinsic coefficient energy density F · symm(a) F.

Equations

• HCPolySupport.coefficientEnergyDensity a F x = HCPolySupport.vecDot (F x) (HCPolySupport.matVecMul (HCPolySupport.symmPart (a x)) (F x))

theorem HCPolySupport.abs_le_half_add_half_of_sq_le_mul {u A B : ℝ} (hu_sq : u ^ 2 ≤ A * B) (hA : 0 ≤ A) (hB : 0 ≤ B) : |u| ≤ A / 2 + B / 2

theorem HCPolySupport.abs_vecDot_matVecMul_symmPart_le_half_add_half_of_isEllipticMatrix {d : ℕ} {lam Lam : ℝ} {A : Mat d} (hA : IsEllipticMatrix lam Lam A) (ξ η : Vec d) : |vecDot ξ (matVecMul (symmPart A) η)| ≤ vecDot ξ (matVecMul (symmPart A) ξ) / 2 + vecDot η (matVecMul (symmPart A) η) / 2

theorem HCPolySupport.vecDot_matVecMul_symmPart_sub_le_two_mul_add_of_isEllipticMatrix {d : ℕ} {lam Lam : ℝ} {A : Mat d} (hA : IsEllipticMatrix lam Lam A) (ξ η : Vec d) : vecDot (ξ - η) (matVecMul (symmPart A) (ξ - η)) ≤ 2 * (vecDot ξ (matVecMul (symmPart A) ξ) + vecDot η (matVecMul (symmPart A) η))

theorem HCPolySupport.coefficientEnergyDensity_eq_unsymmetrized {d : ℕ} (a : CoeffField d) (F : Vec d → Vec d) (x : Vec d) : coefficientEnergyDensity a F x = vecDot (F x) (matVecMul (a x) (F x))

theorem HCPolySupport.IsZeroTraceDirichletRhsWeakSolution.coefficientEnergy_identity_sub_const {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} {u : H10Function U} {g : Vec d → Vec d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (h : IsZeroTraceDirichletRhsWeakSolution a U u g) (hmem : MemVectorL2 U g) (c : Vec d) : ∫ (x : Vec d) in U, coefficientEnergyDensity a (fun (x : Vec d) => u.grad x) x = ∫ (x : Vec d) in U, vecDot (g x - c) (u.grad x)

Zero-trace RHS weak solutions identify the intrinsic coefficient energy with the forcing pairing after subtracting any constant vector.

theorem HCPolySupport.coefficientEnergyDensity_nonneg_of_isEllipticFieldOn {d : ℕ} {lam Lam : ℝ} {U : Set (Vec d)} {a : CoeffField d} (hEll : IsEllipticFieldOn lam Lam U a) (F : Vec d → Vec d) (x : Vec d) : x ∈ U → 0 ≤ coefficientEnergyDensity a F x

theorem HCPolySupport.integrableOn_coefficientEnergyDensity_of_isEllipticFieldOn {d : ℕ} {lam Lam : ℝ} {U : Set (Vec d)} {a : CoeffField d} (hEll : IsEllipticFieldOn lam Lam U a) {F : Vec d → Vec d} (hF : MemVectorL2 U F) : MeasureTheory.IntegrableOn (coefficientEnergyDensity a F) U MeasureTheory.volume

theorem HCPolySupport.coefficientEnergyDensity_sub_le_two_mul_add_of_isEllipticFieldOn {d : ℕ} {lam Lam : ℝ} {U : Set (Vec d)} {a : CoeffField d} (hEll : IsEllipticFieldOn lam Lam U a) (F G : Vec d → Vec d) (x : Vec d) : x ∈ U → coefficientEnergyDensity a (fun (y : Vec d) => F y - G y) x ≤ 2 * (coefficientEnergyDensity a F x + coefficientEnergyDensity a G x)