Documentation

LeanPool.RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.TranslationEstimate

RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.TranslationEstimate #

Pointwise translation estimates for C¹_c functions on Euclidean spaces.

This file provides the key analytic inequality used later in the Euclidean Rellich step: translation differences are controlled by the L²-gradient.

At this stage we only prove pointwise inequalities along the segment t ↦ x + t • a. The measure-theoretic lifting to L² is tracked separately under lean-103.5.2.26.5.3.2.3.

source
@[instance_reducible]
def RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.instMeasurableSpaceTranslationEstimate {E : Type u_1} [NormedAddCommGroup E] :
MeasurableSpace E

Borel σ-algebra on the model space E.

Equations
Instances For
    source
    theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.instBorelSpaceTranslationEstimate {E : Type u_1} [NormedAddCommGroup E] :
    BorelSpace E
    source
    theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.instOpensMeasurableSpaceTranslationEstimate {E : Type u_1} [NormedAddCommGroup E] :
    OpensMeasurableSpace E

    Derivative along a translated line #

    source
    def RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.line {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x a : E) (t : ℝ) :
    E

    The affine line t ↦ x + t • a.

    Equations
    Instances For
      source
      theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.hasDerivAt_line {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x a : E) (t : ℝ) :
      HasDerivAt (line x a) a t
      source
      theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.deriv_line {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x a : E) (t : ℝ) :
      deriv (line x a) t = a
      source
      theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.hasDerivAt_comp_line {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} (hf : ContDiff ℝ 1 f) (x a : E) (t : ℝ) :
      HasDerivAt (fun (t : ℝ) => f (line x a t)) ((fderiv ℝ f (line x a t)) a) t
      source
      theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.deriv_comp_line {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} (hf : ContDiff ℝ 1 f) (x a : E) (t : ℝ) :
      deriv (fun (t : ℝ) => f (line x a t)) t = (fderiv ℝ f (line x a t)) a

      Pointwise translation bound via the gradient #

      source
      theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.enorm_fderiv_apply_le_enorm_grad_mul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (x a : E) :
      ‖(fderiv ℝ f x) a‖ₑ ≤ ‖grad f x‖ₑ * ‖a‖ₑ
      source
      theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.enorm_deriv_comp_line_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (x a : E) {f : E → ℝ} (hf : ContDiff ℝ 1 f) (t : ℝ) :
      ‖deriv (fun (t : ℝ) => f (line x a t)) t‖ₑ ≤ ‖a‖ₑ * ‖grad f (line x a t)‖ₑ
      source
      theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.enorm_sub_le_enorm_mul_lintegral_grad {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (x a : E) {f : E → ℝ} (hf : ContDiff ℝ 1 f) :
      ‖f (x + a) - f x‖ₑ ≤ ‖a‖ₑ * ∫⁻ (t : ℝ) in Set.Icc 0 1, ‖grad f (x + t • a)‖ₑ