RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.TranslationEstimateH1

Extend Euclidean L² translation estimates from C¹_c to the closure-based Euclidean H¹ space.

Main results

• norm_translateL2_sub_h1ToL2_le: for u ∈ H¹, ‖τ_a u - u‖₂ ≤ ‖a‖ · ‖∇u‖₂, where ∇u is the L²(E) component in our H¹ ⊆ L² × L²(E) model.

@[instance_reducible]

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

Borel σ-algebra on the model space E.

Equations

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

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

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

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

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.norm_translateL2_sub_h1ToL2_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddRightInvariant] [MeasureTheory.IsFiniteMeasureOnCompacts μ] [MeasureTheory.SFinite μ] (a : E) (u : ↥(h1 μ)) : ‖(translateL2 μ a) ((h1ToL2 μ) u) - (h1ToL2 μ) u‖ ≤ ‖a‖ * ‖(h1ToL2Grad μ) u‖

H¹ translation estimate via closure: ‖τ_a u - u‖₂ ≤ ‖a‖ · ‖∇u‖₂.