RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.Translation

Translation utilities for the Euclidean Sobolev model spaces.

This file is intentionally “pre-Rellich”: it provides the algebraic/measure-theoretic translation operators and their interaction with the C¹_c graph embedding used to define H¹.

Main results

• translateC1c: translation as a linear endomorphism of C¹_c.
• translateL2: translation as a linear isometry of L² (under an invariant measure).
• translateL2_toL2 / translateL2_toL2Grad: translation commutes with toL2 / toL2Grad.
• grad_translate: the Euclidean gradient commutes with translation.

def RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.translate {E : Type u_1} [NormedAddCommGroup E] {F : Type u_2} (a : E) (f : E → F) : E → F

Translate a function by a (right translation): x ↦ f (x + a).

Equations

• RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.translate a f x = f (x + a)

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.contDiff_translate {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} (hf : ContDiff ℝ 1 f) (a : E) : ContDiff ℝ 1 (translate a f)

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.hasCompactSupport_translate {E : Type u_1} [NormedAddCommGroup E] {F : Type u_2} [Zero F] {f : E → F} (hf : HasCompactSupport f) (a : E) : HasCompactSupport (translate a f)

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.grad_translate {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (a : E) (f : E → ℝ) (x : E) : grad (translate a f) x = grad f (x + a)

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.mem_C1c_translate {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} (hf : f ∈ C1c) (a : E) : translate a f ∈ C1c

noncomputable def RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.translateC1c {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (a : E) : ↥C1c →ₗ[ℝ] ↥C1c

Translation as a linear endomorphism of C¹_c.

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

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

Borel σ-algebra on the model space E.

Equations

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

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

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

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

noncomputable def RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.translateL2 {E : Type u_1} [NormedAddCommGroup E] (μ : MeasureTheory.Measure E) [μ.IsAddRightInvariant] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (a : E) : ↥(MeasureTheory.Lp F 2 μ) →ₗᵢ[ℝ] ↥(MeasureTheory.Lp F 2 μ)

Translation on L² as a linear isometry, under an additive right-invariant measure.

Equations

• RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.translateL2 μ a = MeasureTheory.Lp.compMeasurePreservingₗᵢ ℝ (fun (x : E) => x + a) ⋯

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.translateL2_ae_eq {E : Type u_1} [NormedAddCommGroup E] (μ : MeasureTheory.Measure E) [μ.IsAddRightInvariant] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (a : E) (g : ↥(MeasureTheory.Lp F 2 μ)) : ↑↑((translateL2 μ a) g) =ᵐ[μ] fun (x : E) => ↑↑g (x + a)

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.translateL2_toL2 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddRightInvariant] [MeasureTheory.IsFiniteMeasureOnCompacts μ] (a : E) (f : ↥C1c) : (translateL2 μ a) (toL2 μ f) = toL2 μ ((translateC1c a) f)

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.translateL2_toL2Grad {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddRightInvariant] [MeasureTheory.IsFiniteMeasureOnCompacts μ] (a : E) (f : ↥C1c) : (translateL2 μ a) (toL2Grad μ f) = toL2Grad μ ((translateC1c a) f)