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

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

theorem HCPolySupport.WeakPoissonEquationOn.neg_integral_forwardDifferenceQuotient_mul_fderiv_h1WeakTest_add {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) {S : Set (Vec d)} (hSV : S ⊆ V) (φ ψ : H1WeakTestFunction S) : -∫ (x : Vec d) in V, euclideanForwardDifferenceQuotient step i u.toFun x * (fderiv ℝ (φ.add ψ).toFun x) (basisVec j) = (-∫ (x : Vec d) in V, euclideanForwardDifferenceQuotient step i u.toFun x * (fderiv ℝ φ.toFun x) (basisVec j)) + -∫ (x : Vec d) in V, euclideanForwardDifferenceQuotient step i u.toFun x * (fderiv ℝ ψ.toFun x) (basisVec j)

Additivity of the quotient-Hessian pairing on smooth weak tests.

theorem HCPolySupport.WeakPoissonEquationOn.neg_integral_forwardDifferenceQuotient_mul_fderiv_h1WeakTest_smul {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) {S : Set (Vec d)} (hSV : S ⊆ V) (c : ℝ) (φ : H1WeakTestFunction S) : -∫ (x : Vec d) in V, euclideanForwardDifferenceQuotient step i u.toFun x * (fderiv ℝ (H1WeakTestFunction.smul c φ).toFun x) (basisVec j) = c * -∫ (x : Vec d) in V, euclideanForwardDifferenceQuotient step i u.toFun x * (fderiv ℝ φ.toFun x) (basisVec j)

Scalar-multiplicativity of the quotient-Hessian pairing on smooth weak tests.

theorem HCPolySupport.WeakPoissonEquationOn.abs_neg_integral_forwardDifferenceQuotient_mul_fderiv_le_of_inner_energy_quarter_le {d : ℕ} {U V : Set (Vec d)} (u : H1Function U) (hV : IsOpenBoundedConvexDomain V) (hVU : V ⊆ U) {step R : ℝ} (i j : Fin d) (hVshift : V ⊆ translateSet (-step • basisVec i) U) {S : Set (Vec d)} (hSV : S ⊆ V) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_subS : tsupport φ ⊆ S) (henergy : 1 / 4 * ∫ (x : Vec d) in S, vecNormSq ((u.forwardDifferenceQuotientOn step i ⋯ hVU hVshift).grad x) ≤ R) : |(-∫ (x : Vec d) in V, euclideanForwardDifferenceQuotient step i u.toFun x * (fderiv ℝ φ x) (basisVec j))| ≤ 2 * R + 1 / 2 * ∫ (x : Vec d) in S, φ x ^ 2

Quantitative weak-Hessian handoff from an inner energy estimate: if the forward quotient-gradient energy is controlled on a support set S, then the distributional second-derivative test functional is controlled there.

theorem HCPolySupport.WeakPoissonEquationOn.integral_backwardDifference_cutoffGradient_eq_neg_forwardDifferenceGradient {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) : ∫ (x : Vec d) in U, vecDot (u.grad x) ((backwardDifferenceQuotientSqCutoffForwardDifferenceQuotientToAmbient u hV hVU step i hVshift hη hη_compact hη_sub).grad x) = -∫ (x : Vec d) in V, vecDot ((u.forwardDifferenceQuotientOn step i ⋯ hVU hVshift).grad x) ((localizedSqCutoffForwardDifferenceQuotientToAmbient u hV hVU step i hVshift hη hη_compact hη_sub).grad x)

Specialization of the direct-test summation-by-parts identity to G = ∇u.

theorem HCPolySupport.WeakPoissonEquationOn.directDifferenceQuotient_sqCutoff_energy_identity {d : ℕ} {U V : Set (Vec d)} {u : H1Function U} {f : Vec d → ℝ} (h : WeakPoissonEquationOn U u f) (hU : IsOpen U) (hf : MemScalarL2 U f) (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 V, vecDot ((u.forwardDifferenceQuotientOn step i ⋯ hVU hVshift).grad x) ((localizedSqCutoffForwardDifferenceQuotientToAmbient u hV hVU step i hVshift hη hη_compact hη_sub).grad x) = ∫ (x : Vec d) in U, f x * euclideanBackwardDifferenceQuotient step i (fun (y : Vec d) => η y ^ 2 * euclideanForwardDifferenceQuotient step i u.toFun y) x

Direct difference-quotient energy identity obtained by testing the original weak equation with D_i^-(η²D_i^+u) and summing by parts.

theorem HCPolySupport.WeakPoissonEquationOn.directDifferenceQuotient_sqCutoff_energy_identity_expanded {d : ℕ} {U V : Set (Vec d)} {u : H1Function U} {f : Vec d → ℝ} (h : WeakPoissonEquationOn U u f) (hU : IsOpen U) (hf : MemScalarL2 U f) (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 V, vecDot ((u.forwardDifferenceQuotientOn step i ⋯ hVU hVshift).grad x) fun (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)) = ∫ (x : Vec d) in U, f x * euclideanBackwardDifferenceQuotient step i (fun (y : Vec d) => η y ^ 2 * euclideanForwardDifferenceQuotient step i u.toFun y) x

Direct difference-quotient energy identity with the localized test gradient expanded into its main and cutoff-error pieces.

theorem HCPolySupport.WeakPoissonEquationOn.integrableOn_sq_cutoff_vecNormSq_of_memVectorL2 {d : ℕ} {V : Set (Vec d)} {G : Vec d → Vec d} {η : Vec d → ℝ} (hG : MemVectorL2 V G) (hη : ContDiff ℝ (↑⊤) η) (hη_compact : HasCompactSupport η) : MeasureTheory.IntegrableOn (fun (x : Vec d) => η x ^ 2 * vecNormSq (G x)) V MeasureTheory.volume

A squared smooth compact cutoff times the squared norm of an L² vector field is integrable.

theorem HCPolySupport.WeakPoissonEquationOn.integrableOn_two_mul_sq_mul_vecNormSq_euclideanGradient_of_memScalarL2 {d : ℕ} {V : Set (Vec d)} {w η : Vec d → ℝ} (hw : MemScalarL2 V w) (hη : ContDiff ℝ (↑⊤) η) (hη_compact : HasCompactSupport η) : MeasureTheory.IntegrableOn (fun (x : Vec d) => 2 * w x ^ 2 * vecNormSq (euclideanGradient η x)) V MeasureTheory.volume

The squared quotient term weighted by the squared cutoff-gradient norm is integrable whenever the quotient is scalar L² and the cutoff is smooth compact support.

theorem HCPolySupport.WeakPoissonEquationOn.integrableOn_sq_cutoff_cross_of_memScalarL2_memVectorL2 {d : ℕ} {V : Set (Vec d)} {w : Vec d → ℝ} {G : Vec d → Vec d} {η : Vec d → ℝ} (hw : MemScalarL2 V w) (hG : MemVectorL2 V G) (hη : ContDiff ℝ (↑⊤) η) (hη_compact : HasCompactSupport η) : MeasureTheory.IntegrableOn (fun (x : Vec d) => w x * vecDot (G x) fun (j : Fin d) => 2 * η x * euclideanGradient η x j) V MeasureTheory.volume

The mixed squared-cutoff cross term is integrable when the scalar quotient and vector quotient-gradient are both L².

theorem HCPolySupport.WeakPoissonEquationOn.directDifferenceQuotient_sqCutoff_energy_half_le_neg_forcing_add_error {d : ℕ} {U V : Set (Vec d)} {u : H1Function U} {f : Vec d → ℝ} (h : WeakPoissonEquationOn U u f) (hU : IsOpen U) (hf : MemScalarL2 U f) (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) : 1 / 2 * ∫ (x : Vec d) in V, η x ^ 2 * vecNormSq ((u.forwardDifferenceQuotientOn step i ⋯ hVU hVshift).grad x) ≤ (-∫ (x : Vec d) in U, f x * euclideanBackwardDifferenceQuotient step i (fun (y : Vec d) => η y ^ 2 * euclideanForwardDifferenceQuotient step i u.toFun y) x) + ∫ (x : Vec d) in V, 2 * euclideanForwardDifferenceQuotient step i u.toFun x ^ 2 * vecNormSq (euclideanGradient η x)

Direct squared-cutoff Caccioppoli absorption.

This is the useful output of the direct test D_i^-(η² D_i^+u): it controls the localized L² norm of the gradient difference quotient by the original forcing paired with the same direct test, plus the usual cutoff-gradient error. No difference quotient of f appears.

theorem HCPolySupport.WeakPoissonEquationOn.directDifferenceQuotient_sqCutoff_energy_half_le_forcing_sq_add_test_sq_add_error {d : ℕ} {U V : Set (Vec d)} {u : H1Function U} {f : Vec d → ℝ} (h : WeakPoissonEquationOn U u f) (hU : IsOpen U) (hf : MemScalarL2 U f) (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) : 1 / 2 * ∫ (x : Vec d) in V, η x ^ 2 * vecNormSq ((u.forwardDifferenceQuotientOn step i ⋯ hVU hVshift).grad x) ≤ ((1 / 2 * ∫ (x : Vec d) in U, f x ^ 2) + 1 / 2 * ∫ (x : Vec d) in U, euclideanBackwardDifferenceQuotient step i (fun (y : Vec d) => η y ^ 2 * euclideanForwardDifferenceQuotient step i u.toFun y) x ^ 2) + ∫ (x : Vec d) in V, 2 * euclideanForwardDifferenceQuotient step i u.toFun x ^ 2 * vecNormSq (euclideanGradient η x)

Direct squared-cutoff Caccioppoli after the elementary forcing Young estimate.

The only remaining analytic input needed after this statement is the localized difference-quotient estimate controlling the squared direct test D_i^-(η²D_i^+u) by the gradient of η²D_i^+u.

theorem HCPolySupport.WeakPoissonEquationOn.directDifferenceQuotient_sqCutoff_energy_half_le_two_forcing_sq_add_eighth_test_sq_add_error {d : ℕ} {U V : Set (Vec d)} {u : H1Function U} {f : Vec d → ℝ} (h : WeakPoissonEquationOn U u f) (hU : IsOpen U) (hf : MemScalarL2 U f) (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) : 1 / 2 * ∫ (x : Vec d) in V, η x ^ 2 * vecNormSq ((u.forwardDifferenceQuotientOn step i ⋯ hVU hVshift).grad x) ≤ ((2 * ∫ (x : Vec d) in U, f x ^ 2) + 1 / 8 * ∫ (x : Vec d) in U, euclideanBackwardDifferenceQuotient step i (fun (y : Vec d) => η y ^ 2 * euclideanForwardDifferenceQuotient step i u.toFun y) x ^ 2) + ∫ (x : Vec d) in V, 2 * euclideanForwardDifferenceQuotient step i u.toFun x ^ 2 * vecNormSq (euclideanGradient η x)

Direct squared-cutoff Caccioppoli with a smaller coefficient on the test-square term, tuned for later absorption.

theorem HCPolySupport.WeakPoissonEquationOn.differenceQuotient_energyHalf_le_forcing_sq_add_cutoffGradient_sq_add_error {d : ℕ} {U V : Set (Vec d)} {u : H1Function U} {f : Vec d → ℝ} (h : WeakPoissonEquationOn U u f) (hU : IsOpen U) (hf : MemScalarL2 U f) (hV : IsOpenBoundedConvexDomain V) (hVU : V ⊆ U) {step : ℝ} (hstep : step ≠ 0) (i : Fin d) (hVshift : V ⊆ translateSet (-step • basisVec i) U) {η : 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) ≤ ((1 / 2 * ∫ (x : Vec d) in U, f x ^ 2) + 1 / 2 * ∫ (x : Vec d) in U, (localizedSqCutoffForwardDifferenceQuotientToAmbient u hV hVU step i hVshift hη hη_compact hη_sub).grad x i ^ 2) + ∫ (x : Vec d) in V, 2 * euclideanForwardDifferenceQuotient step i u.toFun x ^ 2 * vecNormSq (euclideanGradient η x)

Direct squared-cutoff Caccioppoli with the test-square term replaced by the product-rule gradient of η²D_i^+u.

theorem HCPolySupport.WeakPoissonEquationOn.differenceQuotientEnergy_le_twoForcingAndCutoffGradientSquares {d : ℕ} {U V : Set (Vec d)} {u : H1Function U} {f : Vec d → ℝ} (h : WeakPoissonEquationOn U u f) (hU : IsOpen U) (hf : MemScalarL2 U f) (hV : IsOpenBoundedConvexDomain V) (hVU : V ⊆ U) {step : ℝ} (hstep : step ≠ 0) (i : Fin d) (hVshift : V ⊆ translateSet (-step • basisVec i) U) {η : 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) ≤ ((2 * ∫ (x : Vec d) in U, f x ^ 2) + 1 / 8 * ∫ (x : Vec d) in U, (localizedSqCutoffForwardDifferenceQuotientToAmbient u hV hVU step i hVshift hη hη_compact hη_sub).grad x i ^ 2) + ∫ (x : Vec d) in V, 2 * euclideanForwardDifferenceQuotient step i u.toFun x ^ 2 * vecNormSq (euclideanGradient η x)

Direct squared-cutoff Caccioppoli with both the small test-square coefficient and the product-rule gradient replacement.

theorem HCPolySupport.WeakPoissonEquationOn.sq_localizedSqCutoffForwardDifferenceQuotientToAmbient_grad_coord_le {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) (hη_abs_le_one : ∀ (x : Vec d), |η x| ≤ 1) (x : Vec d) : (localizedSqCutoffForwardDifferenceQuotientToAmbient u hV hVU step i hVshift hη hη_compact hη_sub).grad x i ^ 2 ≤ 2 * η x ^ 2 * vecNormSq ((u.forwardDifferenceQuotientOn step i ⋯ hVU hVshift).grad x) + 8 * euclideanForwardDifferenceQuotient step i u.toFun x ^ 2 * vecNormSq (euclideanGradient η x)

Pointwise control of the product-rule gradient term produced by η²D_i^+u. The bound only needs the usual cutoff size condition |η| ≤ 1.

theorem HCPolySupport.WeakPoissonEquationOn.eighth_integral_sq_cutoffGradient_coord_le_quarter_energy_add_error {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) (hη_abs_le_one : ∀ (x : Vec d), |η x| ≤ 1) : 1 / 8 * ∫ (x : Vec d) in U, (localizedSqCutoffForwardDifferenceQuotientToAmbient u hV hVU step i hVshift hη hη_compact hη_sub).grad x i ^ 2 ≤ (1 / 4 * ∫ (x : Vec d) in V, η x ^ 2 * vecNormSq ((u.forwardDifferenceQuotientOn step i ⋯ hVU hVshift).grad x)) + ∫ (x : Vec d) in V, euclideanForwardDifferenceQuotient step i u.toFun x ^ 2 * vecNormSq (euclideanGradient η x)

Integral absorption form of sq_localizedSqCutoffForwardDifferenceQuotientToAmbient_grad_coord_le.