Coarse-graining support:

Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.EnergyIntegrand

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

Localized difference-quotient tests for weak Poisson equations

These lemmas are the first formal bridge in the difference-quotient route to the interior H² estimate. They say that after restricting the weak equation to an interior domain V, the smooth-cutoff times forward/backward difference quotient tests constructed in DifferenceQuotientH1 are legal H¹₀(V) tests.

theorem HCPolySupport.WeakPoissonEquationOn.vecDot_cutoff_energy_integrand {d : ℕ} (A B : Vec d) (a b : ℝ) : (vecDot A fun (j : Fin d) => a * A j + b * B j) = a * vecDot A A + b * vecDot A B

Algebraic splitting of the cutoff-energy integrand.

theorem HCPolySupport.WeakPoissonEquationOn.coord_sq_le_vecNormSq {d : ℕ} (A : Vec d) (i : Fin d) : A i ^ 2 ≤ vecNormSq A

A coordinate square is bounded by the full squared Euclidean norm.

theorem HCPolySupport.WeakPoissonEquationOn.abs_sq_cutoff_error_integrand_le {d : ℕ} (η w : ℝ) (A B : Vec d) : |w * vecDot A fun (j : Fin d) => 2 * η * B j| ≤ η ^ 2 * vecNormSq A / 2 + 2 * w ^ 2 * vecNormSq B

Pointwise Young bound for the cutoff-error term when the cutoff is a square, so the gradient contribution has the form 2η ∇η.

theorem HCPolySupport.WeakPoissonEquationOn.sq_cutoff_error_integrand_le {d : ℕ} (η w : ℝ) (A B : Vec d) : (w * vecDot A fun (j : Fin d) => 2 * η * B j) ≤ η ^ 2 * vecNormSq A / 2 + 2 * w ^ 2 * vecNormSq B

Non-absolute-value form of abs_sq_cutoff_error_integrand_le.

theorem HCPolySupport.WeakPoissonEquationOn.neg_sq_cutoff_error_integrand_le {d : ℕ} (η w : ℝ) (A B : Vec d) : (-w * vecDot A fun (j : Fin d) => 2 * η * B j) ≤ η ^ 2 * vecNormSq A / 2 + 2 * w ^ 2 * vecNormSq B

The same pointwise bound for the negative cutoff-error term.

theorem HCPolySupport.WeakPoissonEquationOn.integral_half_main_le_rhs_add_error_of_add_energy_identity {d : ℕ} {V : Set (Vec d)} {m c r e : Vec d → ℝ} (henergy : ∫ (x : Vec d) in V, m x + c x = ∫ (x : Vec d) in V, r x) (hpoint : (fun (x : Vec d) => -c x) ≤ᵐ[MeasureTheory.volume.restrict V] fun (x : Vec d) => m x / 2 + e x) (hm : MeasureTheory.IntegrableOn m V MeasureTheory.volume) (hc : MeasureTheory.IntegrableOn c V MeasureTheory.volume) (he : MeasureTheory.IntegrableOn e V MeasureTheory.volume) : 1 / 2 * ∫ (x : Vec d) in V, m x ≤ (∫ (x : Vec d) in V, r x) + ∫ (x : Vec d) in V, e x

Integral absorption algebra for a cutoff energy identity.

If main + cross = rhs after integration and the pointwise estimate -cross ≤ main / 2 + error is integrable, then half of the main energy is controlled by the right-hand side plus the error term.

theorem HCPolySupport.WeakPoissonEquationOn.integral_half_main_le_scalar_rhs_add_error_of_add_energy_identity {d : ℕ} {V : Set (Vec d)} {m c e : Vec d → ℝ} {R : ℝ} (henergy : ∫ (x : Vec d) in V, m x + c x = R) (hpoint : (fun (x : Vec d) => -c x) ≤ᵐ[MeasureTheory.volume.restrict V] fun (x : Vec d) => m x / 2 + e x) (hm : MeasureTheory.IntegrableOn m V MeasureTheory.volume) (hc : MeasureTheory.IntegrableOn c V MeasureTheory.volume) (he : MeasureTheory.IntegrableOn e V MeasureTheory.volume) : 1 / 2 * ∫ (x : Vec d) in V, m x ≤ R + ∫ (x : Vec d) in V, e x

Integral absorption algebra for a cutoff energy identity with a scalar right-hand side.

This variant is useful for the direct difference-quotient test, whose forcing term naturally remains as an ambient integral over the original domain.

theorem HCPolySupport.WeakPoissonEquationOn.neg_integral_mul_le_half_integral_sq_add_half_integral_sq_of_memScalarL2 {d : ℕ} {U : Set (Vec d)} {F G : Vec d → ℝ} (hF : MemScalarL2 U F) (hG : MemScalarL2 U G) : -∫ (x : Vec d) in U, F x * G x ≤ (1 / 2 * ∫ (x : Vec d) in U, F x ^ 2) + 1 / 2 * ∫ (x : Vec d) in U, G x ^ 2

Pointwise Young's inequality integrated over a set, in the sign needed for the direct forcing term.

theorem HCPolySupport.WeakPoissonEquationOn.neg_integral_mul_le_two_integral_sq_add_eighth_integral_sq_of_memScalarL2 {d : ℕ} {U : Set (Vec d)} {F G : Vec d → ℝ} (hF : MemScalarL2 U F) (hG : MemScalarL2 U G) : -∫ (x : Vec d) in U, F x * G x ≤ (2 * ∫ (x : Vec d) in U, F x ^ 2) + 1 / 8 * ∫ (x : Vec d) in U, G x ^ 2

A small-test-coefficient Young bound for the direct forcing term.

This fixed form is tuned for the later Caccioppoli absorption: the forcing constant is worse, but the test-square coefficient is strictly below the energy coefficient.

theorem HCPolySupport.WeakPoissonEquationOn.integrableOn_mul_left_of_continuous_hasCompactSupport {d : ℕ} {V : Set (Vec d)} {φ F : Vec d → ℝ} (hφ : Continuous φ) (hφ_compact : HasCompactSupport φ) (hF : MeasureTheory.IntegrableOn F V MeasureTheory.volume) : MeasureTheory.IntegrableOn (fun (x : Vec d) => φ x * F x) V MeasureTheory.volume

Multiplying an integrable function by a continuous compactly supported factor preserves integrability on a restricted domain.

theorem HCPolySupport.WeakPoissonEquationOn.memLp_restrict_of_support_subset_of_memLp {d : ℕ} {U V : Set (Vec d)} {F : Vec d → ℝ} (hV_meas : MeasurableSet V) (hF_support : Function.support F ⊆ V) (hF : MeasureTheory.MemLp F 2 (MeasureTheory.volume.restrict V)) : MeasureTheory.MemLp F 2 (MeasureTheory.volume.restrict U)

Move an L² function from an interior set to a larger ambient restricted measure when its pointwise support is contained in the interior set.

theorem HCPolySupport.WeakPoissonEquationOn.integral_subset_of_support_subset {d : ℕ} {U V : Set (Vec d)} {F : Vec d → ℝ} (hVU : V ⊆ U) (hF_support : Function.support F ⊆ V) : ∫ (x : Vec d) in U, F x = ∫ (x : Vec d) in V, F x

If a function is supported in an interior set V ⊆ U, its set integral over U is the same as its set integral over V.

theorem HCPolySupport.WeakPoissonEquationOn.eLpNorm_restrict_eq_restrict_of_support_subset {d : ℕ} {U V : Set (Vec d)} {E : Type u_1} [NormedAddCommGroup E] {F : Vec d → E} {p : ENNReal} (hVU : V ⊆ U) (hF_support : Function.support F ⊆ V) : MeasureTheory.eLpNorm F p (MeasureTheory.volume.restrict U) = MeasureTheory.eLpNorm F p (MeasureTheory.volume.restrict V)

If a function is supported in an interior set V ⊆ U, its eLpNorm on the ambient restricted measure agrees with its eLpNorm on V.

theorem HCPolySupport.WeakPoissonEquationOn.eLpNorm_comp_euclideanCoordShift_of_aestronglyMeasurable {d : ℕ} {F : Vec d → ℝ} (hF : MeasureTheory.AEStronglyMeasurable F MeasureTheory.volume) (step : ℝ) (i : Fin d) (p : ENNReal) : MeasureTheory.eLpNorm (fun (x : Vec d) => F (euclideanCoordShift step i x)) p MeasureTheory.volume = MeasureTheory.eLpNorm F p MeasureTheory.volume

Translation invariance of global eLpNorm for a coordinate shift.

theorem HCPolySupport.WeakPoissonEquationOn.eLpNorm_backwardDifferenceQuotient_sub_le {d : ℕ} {F G : Vec d → ℝ} (hΔ : MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => F x - G x) MeasureTheory.volume) (step : ℝ) (i : Fin d) : MeasureTheory.eLpNorm (fun (x : Vec d) => euclideanBackwardDifferenceQuotient step i F x - euclideanBackwardDifferenceQuotient step i G x) 2 MeasureTheory.volume ≤ ‖step⁻¹‖ₑ * (MeasureTheory.eLpNorm (fun (x : Vec d) => F x - G x) 2 MeasureTheory.volume + MeasureTheory.eLpNorm (fun (x : Vec d) => F x - G x) 2 MeasureTheory.volume)

Backward coordinate difference quotients are continuous on global L².

This is the approximation bridge needed for the direct test: if smooth approximants converge in L², then their backward difference quotients also converge in L², with the elementary translation bound.

theorem HCPolySupport.WeakPoissonEquationOn.aestronglyMeasurable_backwardDifferenceQuotient_sub_of_aestronglyMeasurable {d : ℕ} {F G : Vec d → ℝ} (hΔ : MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => F x - G x) MeasureTheory.volume) (step : ℝ) (i : Fin d) : MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => euclideanBackwardDifferenceQuotient step i F x - euclideanBackwardDifferenceQuotient step i G x) MeasureTheory.volume

The difference of two backward difference quotients is globally a.e.-strongly-measurable when the underlying scalar difference is.

theorem HCPolySupport.WeakPoissonEquationOn.tendsto_eLpNorm_backwardDifferenceQuotient_sub_zero {d : ℕ} {F : ℕ → Vec d → ℝ} {G : Vec d → ℝ} (hΔ : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => F n x - G x) MeasureTheory.volume) (hΔ_tendsto : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => F n x - G x) 2 MeasureTheory.volume) Filter.atTop (nhds 0)) (step : ℝ) (i : Fin d) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => euclideanBackwardDifferenceQuotient step i (F n) x - euclideanBackwardDifferenceQuotient step i G x) 2 MeasureTheory.volume) Filter.atTop (nhds 0)

Convergence in global L² is preserved by a fixed backward coordinate difference quotient, with the elementary translation bound above.

theorem HCPolySupport.WeakPoissonEquationOn.eLpNorm_eq_restrict_of_support_subset {d : ℕ} {U : Set (Vec d)} {F : Vec d → ℝ} (hF_support : Function.support F ⊆ U) : MeasureTheory.eLpNorm F 2 MeasureTheory.volume = MeasureTheory.eLpNorm F 2 (MeasureTheory.volume.restrict U)

If a function is supported in U, then its global L² norm is the same as its L² norm over U. This is just mathlib's support-restriction lemma with the equality oriented for H¹₀ approximation limits.

theorem HCPolySupport.WeakPoissonEquationOn.aestronglyMeasurable_of_restrict_of_support_subset {d : ℕ} {U : Set (Vec d)} {F : Vec d → ℝ} (hU_meas : MeasurableSet U) (hF_restrict : MeasureTheory.AEStronglyMeasurable F (MeasureTheory.volume.restrict U)) (hF_support : Function.support F ⊆ U) : MeasureTheory.AEStronglyMeasurable F MeasureTheory.volume

A restricted a.e.-strongly-measurable scalar function with genuine support in U is globally a.e.-strongly-measurable after extension by zero.