Coarse-graining support: Support.Sobolev.WeakDerivatives

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

def HCPolySupport.basisVec {d : ℕ} (i : Fin d) : Vec d

The coordinate basis vector eᵢ, with entry one at i and zero at every other coordinate.

Equations

• HCPolySupport.basisVec i = Pi.single i 1

@[simp]

theorem HCPolySupport.basisVec_apply {d : ℕ} (i j : Fin d) : basisVec i j = if j = i then 1 else 0

theorem HCPolySupport.vecDot_basisVec_left {d : ℕ} (i : Fin d) (x : Vec d) : vecDot (basisVec i) x = x i

The coordinate dot product against a basis vector reads off the matching coordinate.

theorem HCPolySupport.vecDot_basisVec_right {d : ℕ} (x : Vec d) (i : Fin d) : vecDot x (basisVec i) = x i

The coordinate dot product against a basis vector reads off the matching coordinate.

theorem HCPolySupport.vecNormSq_basisVec {d : ℕ} (i : Fin d) : vecNormSq (basisVec i) = 1

A coordinate basis vector has squared coordinate norm one.

def HCPolySupport.HasWeakPartialDerivOn {d : ℕ} (U : Set (Vec d)) (i : Fin d) (u gi : Vec d → ℝ) : Prop

The integration-by-parts identity ∫ u ∂ᵢφ = -∫ gi φ holds for every smooth test with compact topological support in U.

Equations

• One or more equations did not get rendered due to their size.

def HCPolySupport.HasWeakGradientOn {d : ℕ} (U : Set (Vec d)) (u : Vec d → ℝ) (Du : Vec d → Vec d) : Prop

Each component of Du satisfies the weak partial derivative identity for the corresponding coordinate of u on U.

Equations

• HCPolySupport.HasWeakGradientOn U u Du = ∀ (i : Fin d), HCPolySupport.HasWeakPartialDerivOn U i u fun (x : HCPolySupport.Vec d) => Du x i

theorem HCPolySupport.HasWeakPartialDerivOn.ae_eq {d : ℕ} {U : Set (Vec d)} (hU : IsOpen U) {i : Fin d} {u gi hi : Vec d → ℝ} (hgiLoc : MeasureTheory.LocallyIntegrableOn gi U MeasureTheory.volume) (hhiLoc : MeasureTheory.LocallyIntegrableOn hi U MeasureTheory.volume) (hgi : HasWeakPartialDerivOn U i u gi) (hhi : HasWeakPartialDerivOn U i u hi) : gi =ᵐ[MeasureTheory.volume.restrict U] hi

Weak partial derivatives are unique a.e. on open sets.