RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.TranslationEstimateL2

L² translation estimates for Euclidean C¹_c functions (and derived H¹) under invariant measures.

This file lifts the pointwise fundamental-theorem-of-calculus bound from Euclidean.TranslationEstimate to an L² bound using Tonelli and the measure-preserving property of translations.

Main results

• enorm_translateL2_sub_toL2_le: for f ∈ C¹_c, ‖τ_a f - f‖₂ ≤ ‖a‖ · ‖∇f‖₂ (as an ℝ≥0∞ inequality on L² norms), under a right-invariant measure.

@[implicit_reducible]

def RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.instMeasurableSpaceTranslationEstimateL2 {E : Type u_1} [NormedAddCommGroup E] : MeasurableSpace E

Borel σ-algebra on the model space E.

Equations

• RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.instMeasurableSpaceTranslationEstimateL2 = borel E

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.instBorelSpaceTranslationEstimateL2 {E : Type u_1} [NormedAddCommGroup E] : BorelSpace E

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.instOpensMeasurableSpaceTranslationEstimateL2 {E : Type u_1} [NormedAddCommGroup E] : OpensMeasurableSpace E

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.instMeasurableAddTranslationEstimateL2 {E : Type u_1} [NormedAddCommGroup E] : MeasurableAdd E

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.enorm_translateL2_sub_toL2_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddRightInvariant] [MeasureTheory.IsFiniteMeasureOnCompacts μ] [MeasureTheory.SFinite μ] (a : E) (f : ↥C1c) : ‖(translateL2 μ a) (toL2 μ f) - toL2 μ f‖ₑ ≤ ‖a‖ₑ * ‖toL2Grad μ f‖ₑ

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.norm_translateL2_sub_toL2_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddRightInvariant] [MeasureTheory.IsFiniteMeasureOnCompacts μ] [MeasureTheory.SFinite μ] (a : E) (f : ↥C1c) : ‖(translateL2 μ a) (toL2 μ f) - toL2 μ f‖ ≤ ‖a‖ * ‖toL2Grad μ f‖

Real-norm form of enorm_translateL2_sub_toL2_le.