Coarse-graining support: Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.Localizations

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

noncomputable def HCPolySupport.WeakPoissonEquationOn.localizedMulContDiffHasCompactSupportToAmbient {d : ℕ} {U V : Set (Vec d)} (w : H1Function V) (hV_meas : MeasurableSet V) (hVU : V ⊆ U) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_sub : tsupport φ ⊆ V) : H1Function U

Localize an interior H¹(V) function by a smooth compactly supported cutoff and regard the product as an ambient H¹(U) function.

This is the support-sensitive replacement for pretending that the ambient bounded domain is translation-invariant: only the cutoff product is promoted to U, and every weak-gradient test on U is reduced to the interior set V because the product and its gradient are supported in V.

Equations

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

theorem HCPolySupport.WeakPoissonEquationOn.support_euclideanGradient_coord_subset_tsupport {d : ℕ} {φ : Vec d → ℝ} (j : Fin d) : (Function.support fun (x : Vec d) => euclideanGradient φ x j) ⊆ tsupport φ

The support of a coordinate derivative is contained in the topological support of the original scalar function.

theorem HCPolySupport.WeakPoissonEquationOn.memScalarL2_mul_euclideanGradient_coord_of_contDiff_hasCompactSupport_tsupport_subset {d : ℕ} {U V : Set (Vec d)} {φ F : Vec d → ℝ} (hV_meas : MeasurableSet V) (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_sub : tsupport φ ⊆ V) (hF : MemScalarL2 V F) (j : Fin d) : MemScalarL2 U fun (x : Vec d) => euclideanGradient φ x j * F x

A coordinate derivative of a smooth compactly supported cutoff localizes a scalar L²(V) function to an ambient scalar L²(U) function when the original cutoff support lies in V.

@[simp]

theorem HCPolySupport.WeakPoissonEquationOn.localizedMulContDiffHasCompactSupportToAmbient_toFun {d : ℕ} {U V : Set (Vec d)} (w : H1Function V) (hV_meas : MeasurableSet V) (hVU : V ⊆ U) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_sub : tsupport φ ⊆ V) : (localizedMulContDiffHasCompactSupportToAmbient w hV_meas hVU hφ hφ_compact hφ_sub).toFun = fun (x : Vec d) => φ x * w.toFun x

@[simp]

theorem HCPolySupport.WeakPoissonEquationOn.localizedMulContDiffHasCompactSupportToAmbient_grad {d : ℕ} {U V : Set (Vec d)} (w : H1Function V) (hV_meas : MeasurableSet V) (hVU : V ⊆ U) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_sub : tsupport φ ⊆ V) : (localizedMulContDiffHasCompactSupportToAmbient w hV_meas hVU hφ hφ_compact hφ_sub).grad = fun (x : Vec d) (i : Fin d) => φ x * w.grad x i + w.toFun x * (fderiv ℝ φ x) (basisVec i)

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

Ambient H¹ representative of the squared-cutoff forward difference quotient η² D_i^+ u, localized through an interior shift-safe set.

Equations

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

@[simp]

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

@[simp]

theorem HCPolySupport.WeakPoissonEquationOn.localizedSqCutoffForwardDifferenceQuotientToAmbient_grad {d : ℕ} {U V : Set (Vec d)} (u : H1Function U) (hV : IsOpenBoundedConvexDomain V) (hVU : V ⊆ U) (step : ℝ) (i : Fin d) (hVshift : V ⊆ translateSet (-step • basisVec i) U) {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hη_compact : HasCompactSupport η) (hη_sub : tsupport η ⊆ V) : (localizedSqCutoffForwardDifferenceQuotientToAmbient u hV hVU step i hVshift hη hη_compact hη_sub).grad = fun (x : Vec d) (j : Fin d) => η x ^ 2 * (u.forwardDifferenceQuotientOn step i ⋯ hVU hVshift).grad x j + euclideanForwardDifferenceQuotient step i u.toFun x * (2 * η x * euclideanGradient η x j)

theorem HCPolySupport.WeakPoissonEquationOn.support_localizedSqCutoffForwardDifferenceQuotientToAmbient_grad_subset {d : ℕ} {U V : Set (Vec d)} (u : H1Function U) (hV : IsOpenBoundedConvexDomain V) (hVU : V ⊆ U) (step : ℝ) (i j : Fin d) (hVshift : V ⊆ translateSet (-step • basisVec i) U) {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hη_compact : HasCompactSupport η) (hη_sub : tsupport η ⊆ V) : (Function.support fun (x : Vec d) => (localizedSqCutoffForwardDifferenceQuotientToAmbient u hV hVU step i hVshift hη hη_compact hη_sub).grad x j) ⊆ V

Each coordinate of the localized squared-cutoff forward quotient gradient is supported inside the interior set carrying the cutoff.

theorem HCPolySupport.WeakPoissonEquationOn.support_vecDot_localizedSqCutoffForwardDifferenceQuotientToAmbient_grad_subset {d : ℕ} {U V : Set (Vec d)} (G : Vec d → Vec d) (u : H1Function U) (hV : IsOpenBoundedConvexDomain V) (hVU : V ⊆ U) (step : ℝ) (i : Fin d) (hVshift : V ⊆ translateSet (-step • basisVec i) U) {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hη_compact : HasCompactSupport η) (hη_sub : tsupport η ⊆ V) : (Function.support fun (x : Vec d) => vecDot (G x) ((localizedSqCutoffForwardDifferenceQuotientToAmbient u hV hVU step i hVshift hη hη_compact hη_sub).grad x)) ⊆ V

Pairing against the localized squared-cutoff forward quotient gradient is also supported inside the cutoff interior set.

theorem HCPolySupport.WeakPoissonEquationOn.integral_vecDot_localizedSqCutoffForwardDifferenceQuotientToAmbient_grad_eq_integral_on {d : ℕ} {U V : Set (Vec d)} (G : Vec d → Vec d) (u : H1Function U) (hV : IsOpenBoundedConvexDomain V) (hVU : V ⊆ U) (step : ℝ) (i : Fin d) (hVshift : V ⊆ translateSet (-step • basisVec i) U) {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hη_compact : HasCompactSupport η) (hη_sub : tsupport η ⊆ V) : ∫ (x : Vec d) in U, vecDot (G x) ((localizedSqCutoffForwardDifferenceQuotientToAmbient u hV hVU step i hVshift hη hη_compact hη_sub).grad x) = ∫ (x : Vec d) in V, vecDot (G x) ((localizedSqCutoffForwardDifferenceQuotientToAmbient u hV hVU step i hVshift hη hη_compact hη_sub).grad x)

The unshifted localized-gradient pairing may be integrated over the interior set carrying the cutoff.

theorem HCPolySupport.WeakPoissonEquationOn.memH10_localizedMul_of_contDiff_hasCompactSupport_tsupport_subset {d : ℕ} {U V : Set (Vec d)} (hV : IsOpenBoundedConvexDomain V) (hVU : V ⊆ U) {φ F : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_sub : tsupport φ ⊆ V) (hF : MemH1 V F) : MemH10 U fun (x : Vec d) => φ x * F x

Localized zero-trace cutoff product. If w is only known as an H¹ function on an interior set V, multiplying by a smooth compactly supported cutoff with support in V still gives an H¹₀(U) function on the ambient domain.