Coarse-graining support:

Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.HessianTranslation

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

theorem HCPolySupport.HasWeakPartialDerivOn.congr_of_eqOn {d : ℕ} {U : Set (Vec d)} (hU_meas : MeasurableSet U) {i : Fin d} {u v gi hi : Vec d → ℝ} (huv : Set.EqOn u v U) (hgi : Set.EqOn gi hi U) (h : HasWeakPartialDerivOn U i u gi) : HasWeakPartialDerivOn U i v hi

theorem HCPolySupport.HasWeakPartialDerivOn.translate {d : ℕ} {U : Set (Vec d)} {i : Fin d} {u gi : Vec d → ℝ} (h : HasWeakPartialDerivOn U i u gi) (z : Vec d) : HasWeakPartialDerivOn (translateSet z U) i (fun (x : Vec d) => u (x - z)) fun (x : Vec d) => gi (x - z)

noncomputable def HCPolySupport.HasWeakHessianOn.translate {d : ℕ} {U : Set (Vec d)} {u : H1Function U} (H : HasWeakHessianOn U u) (z : Vec d) : HasWeakHessianOn (translateSet z U) (u.translate z)

Translate a weak Hessian witness from U to U + z.

Equations

• H.translate z = { hess := fun (i j : Fin d) (x : HCPolySupport.Vec d) => H.hess i j (x - z), hess_memL2 := ⋯, weak_second := ⋯ }

theorem HCPolySupport.HasWeakHessianOn.translate_hess {d : ℕ} {U : Set (Vec d)} {u : H1Function U} (H : HasWeakHessianOn U u) (z : Vec d) (i j : Fin d) (x : Vec d) : (H.translate z).hess i j x = H.hess i j (x - z)

theorem HCPolySupport.HasWeakHessianOn.norm_hessCoordToScalarL2_translate_eq {d : ℕ} {U : Set (Vec d)} {u : H1Function U} (H : HasWeakHessianOn U u) (z : Vec d) (i j : Fin d) : ‖(H.translate z).hessCoordToScalarL2 i j‖ = ‖H.hessCoordToScalarL2 i j‖

theorem HCPolySupport.HasWeakHessianOn.hessianCoordL2NormSum_translate_eq {d : ℕ} {U : Set (Vec d)} {u : H1Function U} (H : HasWeakHessianOn U u) (z : Vec d) : (H.translate z).hessianCoordL2NormSum = H.hessianCoordL2NormSum