Weak Derivatives

Support for the Armstrong–Vicol anomalous-diffusion formalization.

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

Coordinate basis vector with value one in the specified coordinate.

Equations

• Homogenization.basisVec i = Pi.single i 1

@[simp]

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

theorem Homogenization.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 Homogenization.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 Homogenization.vecNormSq_basisVec {d : ℕ} (i : Fin d) : vecNormSq (basisVec i) = 1

A coordinate basis vector has squared coordinate norm one.

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

Weak coordinate derivative characterized by integration against smooth compactly supported tests.

Equations

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

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

Coordinatewise weak partial derivatives forming a supplied gradient field.

Equations

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

theorem Homogenization.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.