Bessel potential spaces

We define the Bessel potential space or Fourier-theoretic Sobolev space, with smoothness parameter s and integrability parameter p. Informally, this space is given as the set of all tempered distributions u such that 𝓕⁻ (1 + ‖ξ‖ ^ 2) ^ (s / 2) 𝓕 u is an Lp function.

Implementation notes

In Mathlib.Analysis.Distribution.Sobolev the unbundled version TemperedDistribution.MemSobolev is defined as ∃ v : Lp, besselPotential E F s u = v. While it would be possible to define the bundled space in the same way, the existence quantifier makes proving theorems more involved and hence we bundle the Lp function v into the structure.

We also note that since every Lp function uniquely defines a distribution via u = besselPotential E F (-s) v, it would be possible to define the Bessel potential space as a one-field structure of Lp. The approach of having both u and v as part of the structure gives better definitional equalities.

structure BesselPotentialSpace (E : Type u_1) (F : Type u_2) [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [NormedSpace ℂ F] (s : ℝ) (p : ENNReal) [hp : Fact (1 ≤ p)] : Type (max u_1 u_2)

The Bessel potential space of order s : ℝ and p : ℝ≥0∞, also known as the Sobolev space and usually denoted by H^{s,p}.

It is defined as the set of all tempered distributions u such that 𝓕⁻ (1 + ‖x‖ ^ 2) ^ (s / 2) 𝓕 u can be represented by a Lp function v. Both u and v are stored as data to avoid using Classical.choose.

• toDistr : TemperedDistribution E F

  The underlying tempered distribution

• toLp : ↥(MeasureTheory.Lp F p MeasureTheory.volume)

  The underlying Lp function

• bessel_toDistr_eq_toLp : (TemperedDistribution.besselPotential E F s) ↑self = MeasureTheory.Lp.toTemperedDistribution self.toLp

  The Lp function is obtained by applying the Bessel potential operator to the distribution

def BesselPotentialSpace.«termH^{_,_}(_,_)» : Lean.ParserDescr

The Bessel potential space of order s : ℝ and p : ℝ≥0∞, also known as the Sobolev space and usually denoted by H^{s,p}.

It is defined as the set of all tempered distributions u such that 𝓕⁻ (1 + ‖x‖ ^ 2) ^ (s / 2) 𝓕 u can be represented by a Lp function v. Both u and v are stored as data to avoid using Classical.choose.

Equations

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

def BesselPotentialSpace.«termH^{_,_}(_)» : Lean.ParserDescr

The Bessel potential space of order s : ℝ and p : ℝ≥0∞, also known as the Sobolev space and usually denoted by H^{s,p}.

It is defined as the set of all tempered distributions u such that 𝓕⁻ (1 + ‖x‖ ^ 2) ^ (s / 2) 𝓕 u can be represented by a Lp function v. Both u and v are stored as data to avoid using Classical.choose.

Equations

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

def BesselPotentialSpace.«termH^{_}(_,_)» : Lean.ParserDescr

The Bessel potential space of order s : ℝ and p : ℝ≥0∞, also known as the Sobolev space and usually denoted by H^{s,p}.

It is defined as the set of all tempered distributions u such that 𝓕⁻ (1 + ‖x‖ ^ 2) ^ (s / 2) 𝓕 u can be represented by a Lp function v. Both u and v are stored as data to avoid using Classical.choose.

Equations

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

def BesselPotentialSpace.«termH^{_}(_)» : Lean.ParserDescr

The Bessel potential space of order s : ℝ and p : ℝ≥0∞, also known as the Sobolev space and usually denoted by H^{s,p}.

It is defined as the set of all tempered distributions u such that 𝓕⁻ (1 + ‖x‖ ^ 2) ^ (s / 2) 𝓕 u can be represented by a Lp function v. Both u and v are stored as data to avoid using Classical.choose.

Equations

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

@[instance_reducible]

instance BesselPotentialSpace.instCoeHeadTemperedDistribution {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [NormedSpace ℂ F] {s : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)] : CoeHead (BesselPotentialSpace E F s p) (TemperedDistribution E F)

Equations

• BesselPotentialSpace.instCoeHeadTemperedDistribution = { coe := fun (f : BesselPotentialSpace E F s p) => ↑f }

theorem BesselPotentialSpace.memSobolev_toDistr {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [NormedSpace ℂ F] {s : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)] (f : BesselPotentialSpace E F s p) : TemperedDistribution.MemSobolev s p ↑f

@[simp]

theorem BesselPotentialSpace.besselPotential_neg_toLp_eq {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [NormedSpace ℂ F] {s : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)] {f : BesselPotentialSpace E F s p} : (TemperedDistribution.besselPotential E F (-s)) (MeasureTheory.Lp.toTemperedDistribution f.toLp) = ↑f

theorem BesselPotentialSpace.ext {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [NormedSpace ℂ F] {s : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)] {f g : BesselPotentialSpace E F s p} (h₁ : ↑f = ↑g) : f = g

theorem BesselPotentialSpace.ext_iff {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [NormedSpace ℂ F] {s : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)] {f g : BesselPotentialSpace E F s p} : f = g ↔ ↑f = ↑g

def BesselPotentialSpace.copy {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [NormedSpace ℂ F] {s : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)] (s' : ℝ) (f : BesselPotentialSpace E F s p) (hs : s = s' := by grind) : BesselPotentialSpace E F s' p

Transfer a Sobolev function in H^{s,p} to H^{s', p} given that s = s'.

Equations

• BesselPotentialSpace.copy s' f hs = { toDistr := ↑f, toLp := f.toLp, bessel_toDistr_eq_toLp := ⋯ }

@[simp]

theorem BesselPotentialSpace.toDistr_copy {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [NormedSpace ℂ F] {s s' : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)] (f : BesselPotentialSpace E F s p) (hs : s = s') : ↑(copy s' f ⋯) = ↑f

@[simp]

theorem BesselPotentialSpace.toLp_copy {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [NormedSpace ℂ F] {s s' : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)] (f : BesselPotentialSpace E F s p) (hs : s = s') : (copy s' f ⋯).toLp = f.toLp

theorem BesselPotentialSpace.injective_toLp (E : Type u_1) (F : Type u_2) [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [NormedSpace ℂ F] (s : ℝ) (p : ENNReal) [hp : Fact (1 ≤ p)] : Function.Injective toLp

@[instance_reducible]

noncomputable instance BesselPotentialSpace.instZero {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [NormedSpace ℂ F] {s : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)] : Zero (BesselPotentialSpace E F s p)

Equations

• BesselPotentialSpace.instZero = { zero := { toDistr := 0, toLp := 0, bessel_toDistr_eq_toLp := ⋯ } }

@[simp]

theorem BesselPotentialSpace.toDistr_zero {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [NormedSpace ℂ F] {s : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)] : ↑0 = 0

@[simp]

theorem BesselPotentialSpace.toLp_zero {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [NormedSpace ℂ F] {s : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)] : toLp 0 = 0

@[instance_reducible]

noncomputable instance BesselPotentialSpace.instAdd {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [NormedSpace ℂ F] {s : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)] : Add (BesselPotentialSpace E F s p)

Equations

• BesselPotentialSpace.instAdd = { add := fun (f g : BesselPotentialSpace E F s p) => { toDistr := ↑f + ↑g, toLp := f.toLp + g.toLp, bessel_toDistr_eq_toLp := ⋯ } }

@[simp]

theorem BesselPotentialSpace.toDistr_add {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [NormedSpace ℂ F] {s : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)] (f g : BesselPotentialSpace E F s p) : ↑(f + g) = ↑f + ↑g

@[simp]

theorem BesselPotentialSpace.toLp_add {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [NormedSpace ℂ F] {s : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)] (f g : BesselPotentialSpace E F s p) : (f + g).toLp = f.toLp + g.toLp

@[instance_reducible]

noncomputable instance BesselPotentialSpace.instSub {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [NormedSpace ℂ F] {s : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)] : Sub (BesselPotentialSpace E F s p)

Equations

• BesselPotentialSpace.instSub = { sub := fun (f g : BesselPotentialSpace E F s p) => { toDistr := ↑f - ↑g, toLp := f.toLp - g.toLp, bessel_toDistr_eq_toLp := ⋯ } }

@[simp]

theorem BesselPotentialSpace.toDistr_sub {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [NormedSpace ℂ F] {s : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)] (f g : BesselPotentialSpace E F s p) : ↑(f - g) = ↑f - ↑g

@[simp]

theorem BesselPotentialSpace.toLp_sub {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [NormedSpace ℂ F] {s : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)] (f g : BesselPotentialSpace E F s p) : (f - g).toLp = f.toLp - g.toLp

@[instance_reducible]

noncomputable instance BesselPotentialSpace.instNeg {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [NormedSpace ℂ F] {s : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)] : Neg (BesselPotentialSpace E F s p)

Equations

• BesselPotentialSpace.instNeg = { neg := fun (f : BesselPotentialSpace E F s p) => { toDistr := -↑f, toLp := -f.toLp, bessel_toDistr_eq_toLp := ⋯ } }

@[simp]

theorem BesselPotentialSpace.toDistr_neg {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [NormedSpace ℂ F] {s : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)] (f : BesselPotentialSpace E F s p) : ↑(-f) = -↑f

@[simp]

theorem BesselPotentialSpace.toLp_neg {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [NormedSpace ℂ F] {s : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)] (f : BesselPotentialSpace E F s p) : (-f).toLp = -f.toLp

@[instance_reducible]

instance BesselPotentialSpace.instSMul {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [NormedSpace ℂ F] {s : ℝ} {R : Type u_3} {p : ENNReal} [hp : Fact (1 ≤ p)] [SMul R ℂ] [SMul R (TemperedDistribution E F)] [SMul R ↥(MeasureTheory.Lp F p MeasureTheory.volume)] [IsScalarTower R ℂ (TemperedDistribution E F)] [IsScalarTower R ℂ ↥(MeasureTheory.Lp F p MeasureTheory.volume)] : SMul R (BesselPotentialSpace E F s p)

Equations

• BesselPotentialSpace.instSMul = { smul := fun (c : R) (f : BesselPotentialSpace E F s p) => { toDistr := c • ↑f, toLp := c • f.toLp, bessel_toDistr_eq_toLp := ⋯ } }

@[simp]

theorem BesselPotentialSpace.toDistr_smul {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [NormedSpace ℂ F] {s : ℝ} {R : Type u_3} {p : ENNReal} [hp : Fact (1 ≤ p)] [SMul R ℂ] [SMul R (TemperedDistribution E F)] [SMul R ↥(MeasureTheory.Lp F p MeasureTheory.volume)] [IsScalarTower R ℂ (TemperedDistribution E F)] [IsScalarTower R ℂ ↥(MeasureTheory.Lp F p MeasureTheory.volume)] (c : R) (f : BesselPotentialSpace E F s p) : ↑(c • f) = c • ↑f

@[simp]

theorem BesselPotentialSpace.toLp_smul {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [NormedSpace ℂ F] {s : ℝ} {R : Type u_3} {p : ENNReal} [hp : Fact (1 ≤ p)] [SMul R ℂ] [SMul R (TemperedDistribution E F)] [SMul R ↥(MeasureTheory.Lp F p MeasureTheory.volume)] [IsScalarTower R ℂ (TemperedDistribution E F)] [IsScalarTower R ℂ ↥(MeasureTheory.Lp F p MeasureTheory.volume)] (c : R) (f : BesselPotentialSpace E F s p) : (c • f).toLp = c • f.toLp

@[instance_reducible]

noncomputable instance BesselPotentialSpace.instAddCommGroup {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [NormedSpace ℂ F] {s : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)] : AddCommGroup (BesselPotentialSpace E F s p)

Equations

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

def BesselPotentialSpace.coeAddMonoidHom (E : Type u_1) (F : Type u_2) [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [NormedSpace ℂ F] (s : ℝ) (p : ENNReal) [hp : Fact (1 ≤ p)] : BesselPotentialSpace E F s p →+ TemperedDistribution E F

Coercion to tempered distributions as an additive homomorphism.

Equations

• BesselPotentialSpace.coeAddMonoidHom E F s p = { toFun := fun (f : BesselPotentialSpace E F s p) => ↑f, map_zero' := ⋯, map_add' := ⋯ }

theorem BesselPotentialSpace.coeAddMonoidHom_injective {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [NormedSpace ℂ F] {s : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)] : Function.Injective ⇑(coeAddMonoidHom E F s p)

@[instance_reducible]

noncomputable instance BesselPotentialSpace.instModuleComplex {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [NormedSpace ℂ F] {s : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)] : Module ℂ (BesselPotentialSpace E F s p)

Equations

• BesselPotentialSpace.instModuleComplex = { toSMul := BesselPotentialSpace.instSMul, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

def BesselPotentialSpace.toLpₗ (E : Type u_1) (F : Type u_2) [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [NormedSpace ℂ F] (s : ℝ) (p : ENNReal) [hp : Fact (1 ≤ p)] : BesselPotentialSpace E F s p →ₗ[ℂ] ↥(MeasureTheory.Lp F p MeasureTheory.volume)

The map u ↦ 𝓕⁻ (1 + ‖x‖ ^ 2) ^ (s / 2) 𝓕 u as a linear map from H^{s,p} to Lp.

See toLpₗᵢ for the linear isometry equivalence.

Equations

• BesselPotentialSpace.toLpₗ E F s p = { toFun := BesselPotentialSpace.toLp, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def BesselPotentialSpace.ofLp {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [NormedSpace ℂ F] (s : ℝ) {p : ENNReal} [hp : Fact (1 ≤ p)] (f : ↥(MeasureTheory.Lp F p MeasureTheory.volume)) : BesselPotentialSpace E F s p

Every Lp function defines a Sobolev function by f ↦ besselPotential E F (-s) f.

Equations

• BesselPotentialSpace.ofLp s f = { toDistr := (TemperedDistribution.besselPotential E F (-s)) (MeasureTheory.Lp.toTemperedDistribution f), toLp := f, bessel_toDistr_eq_toLp := ⋯ }

@[simp]

theorem BesselPotentialSpace.toLp_ofLp {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [NormedSpace ℂ F] {s : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)] (f : ↥(MeasureTheory.Lp F p MeasureTheory.volume)) : (ofLp s f).toLp = f

@[simp]

theorem BesselPotentialSpace.toDistr_ofLp {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [NormedSpace ℂ F] {s : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)] (f : ↥(MeasureTheory.Lp F p MeasureTheory.volume)) : ↑(ofLp s f) = (TemperedDistribution.besselPotential E F (-s)) (MeasureTheory.Lp.toTemperedDistribution f)

@[simp]

theorem BesselPotentialSpace.ofLp_toLp {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [NormedSpace ℂ F] {s : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)] (f : BesselPotentialSpace E F s p) : ofLp s f.toLp = f

@[simp]

theorem BesselPotentialSpace.toLpₗ_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [NormedSpace ℂ F] {s : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)] (f : BesselPotentialSpace E F s p) : (toLpₗ E F s p) f = f.toLp

@[instance_reducible]

noncomputable instance BesselPotentialSpace.instNormedAddCommGroup {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [NormedSpace ℂ F] {s : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)] : NormedAddCommGroup (BesselPotentialSpace E F s p)

Equations

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

@[simp]

theorem BesselPotentialSpace.norm_toLp_eq {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [NormedSpace ℂ F] {s : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)] (f : BesselPotentialSpace E F s p) : ‖f.toLp‖ = ‖f‖

@[instance_reducible]

noncomputable instance BesselPotentialSpace.instNormedSpaceComplex {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [NormedSpace ℂ F] {s : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)] : NormedSpace ℂ (BesselPotentialSpace E F s p)

Equations

• BesselPotentialSpace.instNormedSpaceComplex = { toModule := BesselPotentialSpace.instModuleComplex, norm_smul_le := ⋯ }

noncomputable def BesselPotentialSpace.toLpₗᵢ (E : Type u_1) (F : Type u_2) [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [NormedSpace ℂ F] (s : ℝ) (p : ENNReal) [hp : Fact (1 ≤ p)] : BesselPotentialSpace E F s p ≃ₗᵢ[ℂ] ↥(MeasureTheory.Lp F p MeasureTheory.volume)

The linear isometry between H^{s,p} and Lp.

Equations

• BesselPotentialSpace.toLpₗᵢ E F s p = { toLinearMap := BesselPotentialSpace.toLpₗ E F s p, invFun := BesselPotentialSpace.ofLp s, left_inv := ⋯, right_inv := ⋯, norm_map' := ⋯ }

@[simp]

theorem BesselPotentialSpace.toLpₗᵢ_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [NormedSpace ℂ F] {s : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)] (f : BesselPotentialSpace E F s p) : (toLpₗᵢ E F s p) f = f.toLp

@[simp]

theorem BesselPotentialSpace.toLpₗᵢ_symm_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [NormedSpace ℂ F] {s : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)] (f : ↥(MeasureTheory.Lp F p MeasureTheory.volume)) : ↑((toLpₗᵢ E F s p).symm f) = (TemperedDistribution.besselPotential E F (-s)) (MeasureTheory.Lp.toTemperedDistribution f)

instance BesselPotentialSpace.instCompleteSpace {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [NormedSpace ℂ F] {s : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)] : CompleteSpace (BesselPotentialSpace E F s p)

theorem BesselPotentialSpace.norm_fourier_toLp_eq {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [InnerProductSpace ℂ F] {s : ℝ} (f : BesselPotentialSpace E F s 2) : ‖FourierTransform.fourier f.toLp‖ = ‖f‖

@[instance_reducible]

noncomputable instance BesselPotentialSpace.instInnerProductSpaceComplexOfNatENNReal {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [InnerProductSpace ℂ F] (s : ℝ) : InnerProductSpace ℂ (BesselPotentialSpace E F s 2)

Equations

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

noncomputable def TemperedDistribution.MemSobolev.toBesselPotentialSpace {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [NormedSpace ℂ F] {s : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)] {f : TemperedDistribution E F} (hf : MemSobolev s p f) : BesselPotentialSpace E F s p

Every unbundled Sobolev tempered distribution defines an element in H^{s, p}.

Equations

• hf.toBesselPotentialSpace = { toDistr := f, toLp := Exists.choose hf, bessel_toDistr_eq_toLp := ⋯ }

@[simp]

theorem TemperedDistribution.MemSobolev.toBesselPotentialSpace_toDistr {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [NormedSpace ℂ F] {s : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)] {f : TemperedDistribution E F} (hf : MemSobolev s p f) : ↑hf.toBesselPotentialSpace = f

theorem TemperedDistribution.MemSobolev.toBesselPotentialSpace_injective {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [NormedSpace ℂ F] {s : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)] {f g : TemperedDistribution E F} (hf : MemSobolev s p f) (hg : MemSobolev s p g) (h : hf.toBesselPotentialSpace = hg.toBesselPotentialSpace) : f = g