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

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

theorem HCPolySupport.WeakPoissonEquationOn.forwardDifferenceQuotientOn_weakPoissonEquationOn {d : ℕ} {U V : Set (Vec d)} {u : H1Function U} {f : Vec d → ℝ} (h : WeakPoissonEquationOn U u f) (hV : IsOpenBoundedConvexDomain V) (hVU : V ⊆ U) (hfV : MemScalarL2 V f) (step : ℝ) (i : Fin d) (hVshift : V ⊆ translateSet (-step • basisVec i) U) (hfShiftV : MemScalarL2 V fun (x : Vec d) => f (x - -step • basisVec i)) : WeakPoissonEquationOn V (u.forwardDifferenceQuotientOn step i ⋯ hVU hVshift) (euclideanForwardDifferenceQuotient step i f)

The forward difference quotient of a weak Poisson solution satisfies the corresponding weak equation on an interior domain whose forward shifts remain inside the original domain.

theorem HCPolySupport.WeakPoissonEquationOn.backwardDifferenceQuotientOn_weakPoissonEquationOn {d : ℕ} {U V : Set (Vec d)} {u : H1Function U} {f : Vec d → ℝ} (h : WeakPoissonEquationOn U u f) (hV : IsOpenBoundedConvexDomain V) (hVU : V ⊆ U) (hfV : MemScalarL2 V f) (step : ℝ) (i : Fin d) (hVshift : V ⊆ translateSet (step • basisVec i) U) (hfShiftV : MemScalarL2 V fun (x : Vec d) => f (x - step • basisVec i)) : WeakPoissonEquationOn V (u.backwardDifferenceQuotientOn step i ⋯ hVU hVshift) (euclideanBackwardDifferenceQuotient step i f)

The backward difference quotient of a weak Poisson solution satisfies the corresponding weak equation on an interior domain whose backward shifts remain inside the original domain.

theorem HCPolySupport.WeakPoissonEquationOn.forwardDifferenceQuotientOn_cutoff_energy_identity {d : ℕ} {U V : Set (Vec d)} {u : H1Function U} {f : Vec d → ℝ} (h : WeakPoissonEquationOn U u f) (hV : IsOpenBoundedConvexDomain V) (hVU : V ⊆ U) (hfV : MemScalarL2 V f) (step : ℝ) (i : Fin d) (hVshift : V ⊆ translateSet (-step • basisVec i) U) (hfShiftV : MemScalarL2 V fun (x : Vec d) => f (x - -step • basisVec i)) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_sub : tsupport φ ⊆ V) : (∫ (x : Vec d) in V, vecDot ((u.forwardDifferenceQuotientOn step i ⋯ hVU hVshift).grad x) fun (j : Fin d) => φ x * (u.forwardDifferenceQuotientOn step i ⋯ hVU hVshift).grad x j + euclideanForwardDifferenceQuotient step i u.toFun x * (fderiv ℝ φ x) (basisVec j)) = ∫ (x : Vec d) in V, euclideanForwardDifferenceQuotient step i f x * (φ x * euclideanForwardDifferenceQuotient step i u.toFun x)

Cutoff energy identity for the forward difference quotient D_h^+ u.

theorem HCPolySupport.WeakPoissonEquationOn.forwardDifferenceQuotientOn_cutoff_energy_identity_split_integrand {d : ℕ} {U V : Set (Vec d)} {u : H1Function U} {f : Vec d → ℝ} (h : WeakPoissonEquationOn U u f) (hV : IsOpenBoundedConvexDomain V) (hVU : V ⊆ U) (hfV : MemScalarL2 V f) (step : ℝ) (i : Fin d) (hVshift : V ⊆ translateSet (-step • basisVec i) U) (hfShiftV : MemScalarL2 V fun (x : Vec d) => f (x - -step • basisVec i)) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_sub : tsupport φ ⊆ V) : ∫ (x : Vec d) in V, φ x * vecDot ((u.forwardDifferenceQuotientOn step i ⋯ hVU hVshift).grad x) ((u.forwardDifferenceQuotientOn step i ⋯ hVU hVshift).grad x) + euclideanForwardDifferenceQuotient step i u.toFun x * vecDot ((u.forwardDifferenceQuotientOn step i ⋯ hVU hVshift).grad x) (euclideanGradient φ x) = ∫ (x : Vec d) in V, euclideanForwardDifferenceQuotient step i f x * (φ x * euclideanForwardDifferenceQuotient step i u.toFun x)

Cutoff energy identity for D_h^+ u, with the vecDot integrand split into the coercive and cutoff-error terms.

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

Cutoff energy identity for D_h^+ u specialized to a squared smooth cutoff η². This is the form whose cross term is controlled by abs_sq_cutoff_error_integrand_le.

theorem HCPolySupport.WeakPoissonEquationOn.forwardDifferenceQuotientOn_sq_cutoff_energy_half_le_forcing_add_error {d : ℕ} {U V : Set (Vec d)} {u : H1Function U} {f : Vec d → ℝ} (h : WeakPoissonEquationOn U u f) (hV : IsOpenBoundedConvexDomain V) (hVU : V ⊆ U) (hfV : MemScalarL2 V f) (step : ℝ) (i : Fin d) (hVshift : V ⊆ translateSet (-step • basisVec i) U) (hfShiftV : MemScalarL2 V fun (x : Vec d) => f (x - -step • basisVec i)) {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hη_compact : HasCompactSupport η) (hη_sub : tsupport η ⊆ V) : 1 / 2 * ∫ (x : Vec d) in V, η x ^ 2 * vecNormSq ((u.forwardDifferenceQuotientOn step i ⋯ hVU hVshift).grad x) ≤ (∫ (x : Vec d) in V, euclideanForwardDifferenceQuotient step i f x * (η x ^ 2 * euclideanForwardDifferenceQuotient step i u.toFun x)) + ∫ (x : Vec d) in V, 2 * euclideanForwardDifferenceQuotient step i u.toFun x ^ 2 * vecNormSq (euclideanGradient η x)

Forward squared-cutoff Caccioppoli absorption. The integrability needed by the abstract absorption lemma is supplied by the quotient's L² data and the smooth compact cutoff.

theorem HCPolySupport.WeakPoissonEquationOn.backwardDifferenceQuotientOn_cutoff_energy_identity {d : ℕ} {U V : Set (Vec d)} {u : H1Function U} {f : Vec d → ℝ} (h : WeakPoissonEquationOn U u f) (hV : IsOpenBoundedConvexDomain V) (hVU : V ⊆ U) (hfV : MemScalarL2 V f) (step : ℝ) (i : Fin d) (hVshift : V ⊆ translateSet (step • basisVec i) U) (hfShiftV : MemScalarL2 V fun (x : Vec d) => f (x - step • basisVec i)) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_sub : tsupport φ ⊆ V) : (∫ (x : Vec d) in V, vecDot ((u.backwardDifferenceQuotientOn step i ⋯ hVU hVshift).grad x) fun (j : Fin d) => φ x * (u.backwardDifferenceQuotientOn step i ⋯ hVU hVshift).grad x j + euclideanBackwardDifferenceQuotient step i u.toFun x * (fderiv ℝ φ x) (basisVec j)) = ∫ (x : Vec d) in V, euclideanBackwardDifferenceQuotient step i f x * (φ x * euclideanBackwardDifferenceQuotient step i u.toFun x)

Cutoff energy identity for the backward difference quotient D_h^- u.

theorem HCPolySupport.WeakPoissonEquationOn.backwardDifferenceQuotientOn_cutoff_energy_identity_split_integrand {d : ℕ} {U V : Set (Vec d)} {u : H1Function U} {f : Vec d → ℝ} (h : WeakPoissonEquationOn U u f) (hV : IsOpenBoundedConvexDomain V) (hVU : V ⊆ U) (hfV : MemScalarL2 V f) (step : ℝ) (i : Fin d) (hVshift : V ⊆ translateSet (step • basisVec i) U) (hfShiftV : MemScalarL2 V fun (x : Vec d) => f (x - step • basisVec i)) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_sub : tsupport φ ⊆ V) : ∫ (x : Vec d) in V, φ x * vecDot ((u.backwardDifferenceQuotientOn step i ⋯ hVU hVshift).grad x) ((u.backwardDifferenceQuotientOn step i ⋯ hVU hVshift).grad x) + euclideanBackwardDifferenceQuotient step i u.toFun x * vecDot ((u.backwardDifferenceQuotientOn step i ⋯ hVU hVshift).grad x) (euclideanGradient φ x) = ∫ (x : Vec d) in V, euclideanBackwardDifferenceQuotient step i f x * (φ x * euclideanBackwardDifferenceQuotient step i u.toFun x)

Cutoff energy identity for D_h^- u, with the vecDot integrand split into the coercive and cutoff-error terms.

theorem HCPolySupport.WeakPoissonEquationOn.backwardDifferenceQuotientOn_sq_cutoff_energy_identity {d : ℕ} {U V : Set (Vec d)} {u : H1Function U} {f : Vec d → ℝ} (h : WeakPoissonEquationOn U u f) (hV : IsOpenBoundedConvexDomain V) (hVU : V ⊆ U) (hfV : MemScalarL2 V f) (step : ℝ) (i : Fin d) (hVshift : V ⊆ translateSet (step • basisVec i) U) (hfShiftV : MemScalarL2 V fun (x : Vec d) => f (x - step • basisVec i)) {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hη_compact : HasCompactSupport η) (hη_sub : tsupport η ⊆ V) : (∫ (x : Vec d) in V, η x ^ 2 * vecNormSq ((u.backwardDifferenceQuotientOn step i ⋯ hVU hVshift).grad x) + euclideanBackwardDifferenceQuotient step i u.toFun x * vecDot ((u.backwardDifferenceQuotientOn step i ⋯ hVU hVshift).grad x) fun (j : Fin d) => 2 * η x * euclideanGradient η x j) = ∫ (x : Vec d) in V, euclideanBackwardDifferenceQuotient step i f x * (η x ^ 2 * euclideanBackwardDifferenceQuotient step i u.toFun x)

Cutoff energy identity for D_h^- u specialized to a squared smooth cutoff η².

theorem HCPolySupport.WeakPoissonEquationOn.backwardDifferenceQuotientOn_sq_cutoff_energy_half_le_forcing_add_error {d : ℕ} {U V : Set (Vec d)} {u : H1Function U} {f : Vec d → ℝ} (h : WeakPoissonEquationOn U u f) (hV : IsOpenBoundedConvexDomain V) (hVU : V ⊆ U) (hfV : MemScalarL2 V f) (step : ℝ) (i : Fin d) (hVshift : V ⊆ translateSet (step • basisVec i) U) (hfShiftV : MemScalarL2 V fun (x : Vec d) => f (x - step • basisVec i)) {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hη_compact : HasCompactSupport η) (hη_sub : tsupport η ⊆ V) : 1 / 2 * ∫ (x : Vec d) in V, η x ^ 2 * vecNormSq ((u.backwardDifferenceQuotientOn step i ⋯ hVU hVshift).grad x) ≤ (∫ (x : Vec d) in V, euclideanBackwardDifferenceQuotient step i f x * (η x ^ 2 * euclideanBackwardDifferenceQuotient step i u.toFun x)) + ∫ (x : Vec d) in V, 2 * euclideanBackwardDifferenceQuotient step i u.toFun x ^ 2 * vecNormSq (euclideanGradient η x)

Backward squared-cutoff Caccioppoli absorption. The integrability needed by the abstract absorption lemma is supplied by the quotient's L² data and the smooth compact cutoff.