Gradients of slices with the same trace #
Two H¹ slices that agree almost everywhere have almost everywhere equal weak
gradients (lem:lps-continuation).
theorem
ESS.lps_h1_gradient_ae_eq_of_slice_ae_eq
{u v : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3}
{Du Dv : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3}
(hU :
∀ (i : Fin 3),
∃ (h : CKN.H1Function Set.univ),
(h.toFun = fun (x : CKN.Foundation.Parabolic.Vec3) => u x i) ∧ h.grad = fun (x : CKN.Foundation.Parabolic.Vec3) (j : Fin 3) => Du x i j)
(hV :
∀ (i : Fin 3),
∃ (h : CKN.H1Function Set.univ),
(h.toFun = fun (x : CKN.Foundation.Parabolic.Vec3) => v x i) ∧ h.grad = fun (x : CKN.Foundation.Parabolic.Vec3) (j : Fin 3) => Dv x i j)
(htrace : u =ᵐ[MeasureTheory.volume] v)
(i j : Fin 3)
:
(fun (x : CKN.Foundation.Parabolic.Vec3) => Du x i j) =ᵐ[MeasureTheory.volume]
fun (x : CKN.Foundation.Parabolic.Vec3) => Dv x i j
Two H¹ functions that agree almost everywhere have almost everywhere equal weak
gradients (lem:lps-continuation).