Coarse-graining support: Support.Sobolev.Foundations.DifferenceQuotientH1

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

H¹ coordinate difference quotients

This file lifts the scalar coordinate difference-quotient notation to the project's witness-based H1Function API. The quotients are defined only after restricting to an open set V that is contained in the original domain and in the relevant translated domain.

noncomputable def HCPolySupport.H1Function.forwardDifferenceQuotientOn {d : ℕ} {U V : Set (Vec d)} (u : H1Function U) (h : ℝ) (i : Fin d) (hVopen : IsOpen V) (hVU : V ⊆ U) (hVshift : V ⊆ translateSet (-h • basisVec i) U) : H1Function V

Forward coordinate difference quotient of an H¹(U) function, restricted to an interior open set V on which x + h e_i still belongs to U.

Equations

• u.forwardDifferenceQuotientOn h i hVopen hVU hVshift = h⁻¹ • ((u.translate (-h • HCPolySupport.basisVec i)).restrict hVopen hVshift - u.restrict hVopen hVU)

noncomputable def HCPolySupport.H1Function.backwardDifferenceQuotientOn {d : ℕ} {U V : Set (Vec d)} (u : H1Function U) (h : ℝ) (i : Fin d) (hVopen : IsOpen V) (hVU : V ⊆ U) (hVshift : V ⊆ translateSet (h • basisVec i) U) : H1Function V

Backward coordinate difference quotient of an H¹(U) function, restricted to an interior open set V on which x - h e_i still belongs to U.

Equations

• u.backwardDifferenceQuotientOn h i hVopen hVU hVshift = h⁻¹ • (u.restrict hVopen hVU - (u.translate (h • HCPolySupport.basisVec i)).restrict hVopen hVshift)

@[simp]

theorem HCPolySupport.H1Function.forwardDifferenceQuotientOn_toFun {d : ℕ} {U V : Set (Vec d)} (u : H1Function U) (h : ℝ) (i : Fin d) (hVopen : IsOpen V) (hVU : V ⊆ U) (hVshift : V ⊆ translateSet (-h • basisVec i) U) (x : Vec d) : (u.forwardDifferenceQuotientOn h i hVopen hVU hVshift).toFun x = euclideanForwardDifferenceQuotient h i u.toFun x

@[simp]

theorem HCPolySupport.H1Function.backwardDifferenceQuotientOn_toFun {d : ℕ} {U V : Set (Vec d)} (u : H1Function U) (h : ℝ) (i : Fin d) (hVopen : IsOpen V) (hVU : V ⊆ U) (hVshift : V ⊆ translateSet (h • basisVec i) U) (x : Vec d) : (u.backwardDifferenceQuotientOn h i hVopen hVU hVshift).toFun x = euclideanBackwardDifferenceQuotient h i u.toFun x

@[simp]

theorem HCPolySupport.H1Function.forwardDifferenceQuotientOn_grad {d : ℕ} {U V : Set (Vec d)} (u : H1Function U) (h : ℝ) (i : Fin d) (hVopen : IsOpen V) (hVU : V ⊆ U) (hVshift : V ⊆ translateSet (-h • basisVec i) U) (x : Vec d) : (u.forwardDifferenceQuotientOn h i hVopen hVU hVshift).grad x = h⁻¹ • (u.grad (euclideanCoordShift h i x) - u.grad x)

@[simp]

theorem HCPolySupport.H1Function.backwardDifferenceQuotientOn_grad {d : ℕ} {U V : Set (Vec d)} (u : H1Function U) (h : ℝ) (i : Fin d) (hVopen : IsOpen V) (hVU : V ⊆ U) (hVshift : V ⊆ translateSet (h • basisVec i) U) (x : Vec d) : (u.backwardDifferenceQuotientOn h i hVopen hVU hVshift).grad x = h⁻¹ • (u.grad x - u.grad (euclideanCoordShift (-h) i x))

noncomputable def HCPolySupport.H1Function.mulContDiffHasCompactSupportToH10 {d : ℕ} {U : Set (Vec d)} (u : H1Function U) (hU : IsOpenBoundedConvexDomain U) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_sub : tsupport φ ⊆ U) : H10Function U

Choose an H¹₀(U) representative of φ * u when φ is a smooth compactly supported cutoff inside a bounded open convex domain. This packages the existing membership theorem as data, so it can be passed directly to WeakPoissonEquationOn.h10.

Equations

• u.mulContDiffHasCompactSupportToH10 hU hφ hφ_compact hφ_sub = Classical.choose ⋯

@[simp]

theorem HCPolySupport.H1Function.mulContDiffHasCompactSupportToH10_toFun {d : ℕ} {U : Set (Vec d)} (u : H1Function U) (hU : IsOpenBoundedConvexDomain U) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_sub : tsupport φ ⊆ U) : (u.mulContDiffHasCompactSupportToH10 hU hφ hφ_compact hφ_sub).toFun = fun (x : Vec d) => φ x * u.toFun x

noncomputable def HCPolySupport.H1Function.cutoffForwardDifferenceQuotientToH10 {d : ℕ} {U V : Set (Vec d)} (u : H1Function U) (h : ℝ) (i : Fin d) (hV : IsOpenBoundedConvexDomain V) (hVU : V ⊆ U) (hVshift : V ⊆ translateSet (-h • basisVec i) U) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_sub : tsupport φ ⊆ V) : H10Function V

A smooth cutoff times a forward H¹ difference quotient, packaged as an H¹₀(V) test.

Equations

• u.cutoffForwardDifferenceQuotientToH10 h i hV hVU hVshift hφ hφ_compact hφ_sub = (u.forwardDifferenceQuotientOn h i ⋯ hVU hVshift).mulContDiffHasCompactSupportToH10 hV hφ hφ_compact hφ_sub

@[simp]

theorem HCPolySupport.H1Function.cutoffForwardDifferenceQuotientToH10_toFun {d : ℕ} {U V : Set (Vec d)} (u : H1Function U) (h : ℝ) (i : Fin d) (hV : IsOpenBoundedConvexDomain V) (hVU : V ⊆ U) (hVshift : V ⊆ translateSet (-h • basisVec i) U) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_sub : tsupport φ ⊆ V) : (u.cutoffForwardDifferenceQuotientToH10 h i hV hVU hVshift hφ hφ_compact hφ_sub).toFun = fun (x : Vec d) => φ x * euclideanForwardDifferenceQuotient h i u.toFun x

noncomputable def HCPolySupport.H1Function.cutoffBackwardDifferenceQuotientToH10 {d : ℕ} {U V : Set (Vec d)} (u : H1Function U) (h : ℝ) (i : Fin d) (hV : IsOpenBoundedConvexDomain V) (hVU : V ⊆ U) (hVshift : V ⊆ translateSet (h • basisVec i) U) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_sub : tsupport φ ⊆ V) : H10Function V

A smooth cutoff times a backward H¹ difference quotient, packaged as an H¹₀(V) test.

Equations

• u.cutoffBackwardDifferenceQuotientToH10 h i hV hVU hVshift hφ hφ_compact hφ_sub = (u.backwardDifferenceQuotientOn h i ⋯ hVU hVshift).mulContDiffHasCompactSupportToH10 hV hφ hφ_compact hφ_sub

@[simp]

theorem HCPolySupport.H1Function.cutoffBackwardDifferenceQuotientToH10_toFun {d : ℕ} {U V : Set (Vec d)} (u : H1Function U) (h : ℝ) (i : Fin d) (hV : IsOpenBoundedConvexDomain V) (hVU : V ⊆ U) (hVshift : V ⊆ translateSet (h • basisVec i) U) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_sub : tsupport φ ⊆ V) : (u.cutoffBackwardDifferenceQuotientToH10 h i hV hVU hVshift hφ hφ_compact hφ_sub).toFun = fun (x : Vec d) => φ x * euclideanBackwardDifferenceQuotient h i u.toFun x