Coarse-graining support: Support.Sobolev.H1.BasicLemmas

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

theorem HCPolySupport.memL2On_mono {d : ℕ} {U V : Set (Vec d)} {u : Vec d → ℝ} (hVU : V ⊆ U) (hu : MemL2On U u) : MemL2On V u

theorem HCPolySupport.gradMemL2On_mono {d : ℕ} {U V : Set (Vec d)} {Du : Vec d → Vec d} (hVU : V ⊆ U) (hDu : GradMemL2On U Du) : GradMemL2On V Du

theorem HCPolySupport.memL2On_openCubeSet_normalizedCubeMeasure {d : ℕ} {Q : TriadicCube d} {u : Vec d → ℝ} (hu : MemL2On (openCubeSet Q) u) : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)

theorem HCPolySupport.HasWeakPartialDerivOn.restrict {d : ℕ} {U V : Set (Vec d)} (hVopen : IsOpen V) (hVU : V ⊆ U) {i : Fin d} {u gi : Vec d → ℝ} (h : HasWeakPartialDerivOn U i u gi) : HasWeakPartialDerivOn V i u gi

theorem HCPolySupport.HasWeakGradientOn.restrict {d : ℕ} {U V : Set (Vec d)} (hVopen : IsOpen V) (hVU : V ⊆ U) {u : Vec d → ℝ} {Du : Vec d → Vec d} (h : HasWeakGradientOn U u Du) : HasWeakGradientOn V u Du

theorem HCPolySupport.HasWeakPartialDerivOn.of_contDiff {d : ℕ} {U : Set (Vec d)} {i : Fin d} {f : Vec d → ℝ} (hf : ContDiff ℝ 1 f) : HasWeakPartialDerivOn U i f fun (x : Vec d) => (fderiv ℝ f x) (basisVec i)

theorem HCPolySupport.HasWeakGradientOn.of_contDiff {d : ℕ} {U : Set (Vec d)} {f : Vec d → ℝ} (hf : ContDiff ℝ 1 f) : HasWeakGradientOn U f fun (x : Vec d) (i : Fin d) => (fderiv ℝ f x) (basisVec i)

theorem HCPolySupport.H1Function.ext {d : ℕ} {U : Set (Vec d)} {u v : H1Function U} (htoFun : u.toFun = v.toFun) (hgrad : u.grad = v.grad) : u = v

theorem HCPolySupport.H1Function.ext_iff {d : ℕ} {U : Set (Vec d)} {u v : H1Function U} : u = v ↔ u.toFun = v.toFun ∧ u.grad = v.grad

theorem HCPolySupport.H1Function.hasWeakPartialDerivOn {d : ℕ} {U : Set (Vec d)} (u : H1Function U) (i : Fin d) : HasWeakPartialDerivOn U i u.toFun fun (x : Vec d) => u.grad x i

theorem HCPolySupport.H1Function.grad_memL2 {d : ℕ} {U : Set (Vec d)} (u : H1Function U) (i : Fin d) : MemL2On U fun (x : Vec d) => u.grad x i

theorem HCPolySupport.H1Function.grad_memVectorL2 {d : ℕ} {U : Set (Vec d)} (u : H1Function U) : MemVectorL2 U u.grad

theorem HCPolySupport.H1Function.memL2_normalizedCubeMeasure {d : ℕ} {Q : TriadicCube d} (u : H1Function (openCubeSet Q)) : MeasureTheory.MemLp (fun (x : Vec d) => u.toFun x) 2 (normalizedCubeMeasure Q)

theorem HCPolySupport.H1Function.grad_memL2_normalizedCubeMeasure {d : ℕ} {Q : TriadicCube d} (u : H1Function (openCubeSet Q)) (i : Fin d) : MeasureTheory.MemLp (fun (x : Vec d) => u.grad x i) 2 (normalizedCubeMeasure Q)

theorem HCPolySupport.H1Function.memH1 {d : ℕ} {U : Set (Vec d)} (u : H1Function U) : MemH1 U u.toFun

noncomputable def HCPolySupport.H1Function.ofContDiff {d : ℕ} {U : Set (Vec d)} (_hU : IsOpen U) {f : Vec d → ℝ} (hf : ContDiff ℝ 1 f) (hf_supp : HasCompactSupport f) : H1Function U

A compactly supported C¹ function viewed as an H¹ function on U, with its classical coordinate derivatives as weak gradient.

Equations

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

noncomputable def HCPolySupport.H1Function.ofContDiffOnIsSobolevRegularDomain {d : ℕ} {U : Set (Vec d)} (hU : IsSobolevRegularDomain U) {f : Vec d → ℝ} (hf : ContDiff ℝ 1 f) : H1Function U

Package a globally smooth function as an H¹(U) witness on a bounded measurable domain. Unlike ofContDiff, this constructor does not require compact support, because boundedness of U gives the needed L² control on the restriction.

Equations

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

noncomputable def HCPolySupport.H1Function.ofContDiffOnIsOpenBoundedConvexDomain {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {f : Vec d → ℝ} (hf : ContDiff ℝ 1 f) : H1Function U

Bounded open convex domains admit the bounded-domain smooth constructor for H¹.

Equations

• HCPolySupport.H1Function.ofContDiffOnIsOpenBoundedConvexDomain hU hf = HCPolySupport.H1Function.ofContDiffOnIsSobolevRegularDomain ⋯ hf

def HCPolySupport.H1Function.restrict {d : ℕ} {U V : Set (Vec d)} (u : H1Function U) (hVopen : IsOpen V) (hVU : V ⊆ U) : H1Function V

Restriction of an H¹ witness to an open subset, retaining its value and weak-gradient representatives.

Equations

• u.restrict hVopen hVU = { toFun := u.toFun, grad := u.grad, memL2 := ⋯, gradMemL2 := ⋯, hasWeakGradient := ⋯ }

noncomputable def HCPolySupport.H1Function.restrictToOpenSubcube {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (u : H1Function (openCubeSet Q)) (hR : R ∈ descendantsAtDepth Q j) : H1Function (openCubeSet R)

Restriction of an H¹ witness on the open parent cube to the open cube of a descendant.

Equations

• u.restrictToOpenSubcube hR = u.restrict ⋯ ⋯

@[simp]

theorem HCPolySupport.H1Function.restrictToOpenSubcube_toFun {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (u : H1Function (openCubeSet Q)) (hR : R ∈ descendantsAtDepth Q j) : (u.restrictToOpenSubcube hR).toFun = u.toFun

@[simp]

theorem HCPolySupport.H1Function.restrictToOpenSubcube_grad {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (u : H1Function (openCubeSet Q)) (hR : R ∈ descendantsAtDepth Q j) : (u.restrictToOpenSubcube hR).grad = u.grad

theorem HCPolySupport.H1Function.grad_memL2_normalizedCubeMeasure_of_mem_descendantsAtDepth {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (u : H1Function (openCubeSet Q)) (hR : R ∈ descendantsAtDepth Q j) (i : Fin d) : MeasureTheory.MemLp (fun (x : Vec d) => u.grad x i) 2 (normalizedCubeMeasure R)

theorem HCPolySupport.H10Function.memH1 {d : ℕ} {U : Set (Vec d)} (u : H10Function U) : MemH1 U u.toFun

noncomputable def HCPolySupport.H10Function.ofContDiff {d : ℕ} {U : Set (Vec d)} (hU : IsOpen U) {f : Vec d → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hf_supp : HasCompactSupport f) (hf_sub : tsupport f ⊆ U) : H10Function U

A smooth function with compact topological support in U, viewed in H¹₀ using its constant approximation sequence.

Equations

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

theorem HCPolySupport.memH1_of_memH10 {d : ℕ} {U : Set (Vec d)} {u : Vec d → ℝ} (hu : MemH10 U u) : MemH1 U u

theorem HCPolySupport.memH1_restrict {d : ℕ} {U V : Set (Vec d)} {u : Vec d → ℝ} (hVopen : IsOpen V) (hVU : V ⊆ U) (hu : MemH1 U u) : MemH1 V u

theorem HCPolySupport.H10Function.memH10 {d : ℕ} {U : Set (Vec d)} (u : H10Function U) : MemH10 U u.toFun

theorem HCPolySupport.memH10_of_contDiff {d : ℕ} {U : Set (Vec d)} (hU : IsOpen U) {f : Vec d → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hf_supp : HasCompactSupport f) (hf_sub : tsupport f ⊆ U) : MemH10 U f

theorem HCPolySupport.memH1_of_contDiffOnIsSobolevRegularDomain {d : ℕ} {U : Set (Vec d)} (hU : IsSobolevRegularDomain U) {f : Vec d → ℝ} (hf : ContDiff ℝ 1 f) : MemH1 U f

theorem HCPolySupport.memH1_of_contDiffOnIsOpenBoundedConvexDomain {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {f : Vec d → ℝ} (hf : ContDiff ℝ 1 f) : MemH1 U f