L² compactness criterion: bounding the translation-integral by a translation modulus #
This file provides a small but crucial bridge lemma used to connect a uniform translation modulus
on L²(volume) with the kernelMeasure translation-integral bound appearing in the
approximation-identity estimate.
The core observation is that if ψ is supported in a neighborhood where the translation modulus is
≤ η, then the averaged squared translation error against the probability measure
kernelMeasure ψ is ≤ η².
Tracking: Beads lean-103.5.2.26.5.3.2.2.4.
@[implicit_reducible]
def
RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.instMeasurableSpaceEL2CompactnessTranslationIntegral
{E : Type u_1}
[NormedAddCommGroup E]
:
Borel σ-algebra on the model space E.
Equations
Instances For
theorem
RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.integral_norm_sq_translateL2_sub_le_sq_of_tsupport_subset_ball
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[FiniteDimensional ℝ E]
{ψ : E → ℝ}
(hψc : Continuous ψ)
(hψcs : HasCompactSupport ψ)
(hψ0 : ∀ (x : E), 0 ≤ ψ x)
(hψint : ∫ (x : E), ψ x = 1)
{δ η : ℝ}
(hη : 0 ≤ η)
(hψsupp : tsupport ψ ⊆ Metric.ball 0 δ)
(F : ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume))
(hmod : ∀ t ∈ Metric.ball 0 δ, ‖(translateL2 MeasureTheory.volume (-t)) F - F‖ ≤ η)
: