Continuous bilinear maps on MeasureTheory.Lp spaces #
Given a continuous bilinear map B : E →L[𝕜] F →L[𝕜] G, we define an associated map
ContinuousLinearMap.holder : Lp E p μ → Lp F q μ → Lp G r μ where p q r are a Hölder triple.
We bundle this into a bilinear map ContinuousLinearMap.holderₗ and a continuous
bilinear map ContinuousLinearMap.holderL under some additional assumptions.
We also declare a heterogeneous scalar multiplication (HSMul) instance on MeasureTheory.Lp
spaces. Although this could use the ContinuousLinearMap.holder construction above, we opt not to
do so in order to minimize the necessary type class assumptions.
When p q : ℝ≥0∞ are Hölder conjugate (i.e., HolderConjugate p q), we also construct the
natural map ContinuousLinearMap.lpPairing : Lp E p μ →L[𝕜] Lp F q μ →L[𝕜] G given by
fun f g ↦ ∫ x, B (f x) (g x) ∂μ. When B := (NormedSpace.inclusionInDoubleDual 𝕜 E).flip, this
is the natural map Lp (Dual 𝕜 E) p μ →L[𝕜] Dual 𝕜 (Lp E q μ).
Induced bilinear maps #
def
ContinuousLinearMap.holder
{α : Type u_1}
{𝕜 : Type u_2}
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{p q : ENNReal}
(r : ENNReal)
[hpqr : p.HolderTriple q r]
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedAddCommGroup F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 F]
[NormedSpace 𝕜 G]
(B : E →L[𝕜] F →L[𝕜] G)
(f : ↥(MeasureTheory.Lp E p μ))
(g : ↥(MeasureTheory.Lp F q μ))
:
↥(MeasureTheory.Lp G r μ)
The map between MeasuryTheory.Lp spaces satisfying ENNReal.HolderTriple
induced by a continuous bilinear map on the underlying spaces.
Equations
- ContinuousLinearMap.holder r B f g = MeasureTheory.MemLp.toLp (fun (x : α) => (B (↑↑f x)) (↑↑g x)) ⋯
Instances For
theorem
ContinuousLinearMap.coeFn_holder
{α : Type u_1}
{𝕜 : Type u_2}
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{p q r : ENNReal}
[hpqr : p.HolderTriple q r]
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedAddCommGroup F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 F]
[NormedSpace 𝕜 G]
(B : E →L[𝕜] F →L[𝕜] G)
(f : ↥(MeasureTheory.Lp E p μ))
(g : ↥(MeasureTheory.Lp F q μ))
:
theorem
ContinuousLinearMap.nnnorm_holder_apply_apply_le
{α : Type u_1}
{𝕜 : Type u_2}
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{p q r : ENNReal}
[hpqr : p.HolderTriple q r]
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedAddCommGroup F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 F]
[NormedSpace 𝕜 G]
(B : E →L[𝕜] F →L[𝕜] G)
(f : ↥(MeasureTheory.Lp E p μ))
(g : ↥(MeasureTheory.Lp F q μ))
:
theorem
ContinuousLinearMap.norm_holder_apply_apply_le
{α : Type u_1}
{𝕜 : Type u_2}
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{p q r : ENNReal}
[hpqr : p.HolderTriple q r]
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedAddCommGroup F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 F]
[NormedSpace 𝕜 G]
(B : E →L[𝕜] F →L[𝕜] G)
(f : ↥(MeasureTheory.Lp E p μ))
(g : ↥(MeasureTheory.Lp F q μ))
:
theorem
ContinuousLinearMap.holder_add_left
{α : Type u_1}
{𝕜 : Type u_2}
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{p q r : ENNReal}
[hpqr : p.HolderTriple q r]
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedAddCommGroup F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 F]
[NormedSpace 𝕜 G]
(B : E →L[𝕜] F →L[𝕜] G)
(f₁ f₂ : ↥(MeasureTheory.Lp E p μ))
(g : ↥(MeasureTheory.Lp F q μ))
:
theorem
ContinuousLinearMap.holder_add_right
{α : Type u_1}
{𝕜 : Type u_2}
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{p q r : ENNReal}
[hpqr : p.HolderTriple q r]
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedAddCommGroup F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 F]
[NormedSpace 𝕜 G]
(B : E →L[𝕜] F →L[𝕜] G)
(f : ↥(MeasureTheory.Lp E p μ))
(g₁ g₂ : ↥(MeasureTheory.Lp F q μ))
:
theorem
ContinuousLinearMap.holder_smul_left
{α : Type u_1}
{𝕜 : Type u_2}
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{p q r : ENNReal}
[hpqr : p.HolderTriple q r]
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedAddCommGroup F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 F]
[NormedSpace 𝕜 G]
(B : E →L[𝕜] F →L[𝕜] G)
(c : 𝕜)
(f : ↥(MeasureTheory.Lp E p μ))
(g : ↥(MeasureTheory.Lp F q μ))
:
theorem
ContinuousLinearMap.holder_smul_right
{α : Type u_1}
{𝕜 : Type u_2}
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{p q r : ENNReal}
[hpqr : p.HolderTriple q r]
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedAddCommGroup F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 F]
[NormedSpace 𝕜 G]
(B : E →L[𝕜] F →L[𝕜] G)
(c : 𝕜)
(f : ↥(MeasureTheory.Lp E p μ))
(g : ↥(MeasureTheory.Lp F q μ))
:
def
ContinuousLinearMap.holderₗ
{α : Type u_1}
{𝕜 : Type u_2}
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
{m : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
(p q r : ENNReal)
[hpqr : p.HolderTriple q r]
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedAddCommGroup F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 F]
[NormedSpace 𝕜 G]
(B : E →L[𝕜] F →L[𝕜] G)
:
MeasureTheory.Lp.holder as a bilinear map.
Equations
- ContinuousLinearMap.holderₗ μ p q r B = LinearMap.mk₂ 𝕜 (ContinuousLinearMap.holder r B) ⋯ ⋯ ⋯ ⋯
Instances For
@[simp]
theorem
ContinuousLinearMap.holderₗ_apply_apply
{α : Type u_1}
{𝕜 : Type u_2}
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
{m : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
(p q r : ENNReal)
[hpqr : p.HolderTriple q r]
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedAddCommGroup F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 F]
[NormedSpace 𝕜 G]
(B : E →L[𝕜] F →L[𝕜] G)
(m✝ : ↥(MeasureTheory.Lp E p μ))
(g : ↥(MeasureTheory.Lp F q μ))
:
def
ContinuousLinearMap.holderL
{α : Type u_1}
{𝕜 : Type u_2}
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
{m : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
(p q r : ENNReal)
[hpqr : p.HolderTriple q r]
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedAddCommGroup F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 F]
[NormedSpace 𝕜 G]
(B : E →L[𝕜] F →L[𝕜] G)
[Fact (1 ≤ p)]
[Fact (1 ≤ q)]
[Fact (1 ≤ r)]
:
MeasureTheory.Lp.holder as a continuous bilinear map.
Equations
- ContinuousLinearMap.holderL μ p q r B = (ContinuousLinearMap.holderₗ μ p q r B).mkContinuous₂ ‖B‖ ⋯
Instances For
@[simp]
theorem
ContinuousLinearMap.holderL_apply_apply
{α : Type u_1}
{𝕜 : Type u_2}
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
{m : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
(p q r : ENNReal)
[hpqr : p.HolderTriple q r]
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedAddCommGroup F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 F]
[NormedSpace 𝕜 G]
(B : E →L[𝕜] F →L[𝕜] G)
[Fact (1 ≤ p)]
[Fact (1 ≤ q)]
[Fact (1 ≤ r)]
(x : ↥(MeasureTheory.Lp E p μ))
(g : ↥(MeasureTheory.Lp F q μ))
:
theorem
ContinuousLinearMap.norm_holderL_le
{α : Type u_1}
{𝕜 : Type u_2}
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{p q r : ENNReal}
[hpqr : p.HolderTriple q r]
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedAddCommGroup F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 F]
[NormedSpace 𝕜 G]
(B : E →L[𝕜] F →L[𝕜] G)
[Fact (1 ≤ p)]
[Fact (1 ≤ q)]
[Fact (1 ≤ r)]
:
def
ContinuousLinearMap.lpPairing
{α : Type u_1}
{𝕜 : Type u_2}
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
{m : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
(p q : ENNReal)
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedAddCommGroup F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 F]
[NormedSpace 𝕜 G]
[Fact (1 ≤ p)]
[Fact (1 ≤ q)]
[p.HolderConjugate q]
[NormedSpace ℝ G]
[SMulCommClass ℝ 𝕜 G]
[CompleteSpace G]
(B : E →L[𝕜] F →L[𝕜] G)
:
The natural pairing between Lp E p μ and Lp F q μ (for Hölder conjugate p q : ℝ≥0∞) with
values in a space G induced by a bilinear map B : E →L[𝕜] F →L[𝕜] G.
This is given by ∫ x, B (f x) (g x) ∂μ.
In the special case when B := (NormedSpace.inclusionInDoubleDual 𝕜 E).flip, which is
definitionally the same as B := ContinuousLinearMap.id 𝕜 (E →L[𝕜] 𝕜), this is the
natural map Lp (Dual 𝕜 E) p μ →L[𝕜] Dual 𝕜 (Lp E q μ).
Equations
- ContinuousLinearMap.lpPairing μ p q B = (ContinuousLinearMap.postcomp (↥(MeasureTheory.Lp F q μ)) (MeasureTheory.L1.integralCLM' 𝕜)).comp (ContinuousLinearMap.holderL μ p q 1 B)
Instances For
theorem
ContinuousLinearMap.lpPairing_eq_integral
{α : Type u_1}
{𝕜 : Type u_2}
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{p q : ENNReal}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedAddCommGroup F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 F]
[NormedSpace 𝕜 G]
(B : E →L[𝕜] F →L[𝕜] G)
[Fact (1 ≤ p)]
[Fact (1 ≤ q)]
[p.HolderConjugate q]
[NormedSpace ℝ G]
[SMulCommClass ℝ 𝕜 G]
[CompleteSpace G]
(f : ↥(MeasureTheory.Lp E p μ))
(g : ↥(MeasureTheory.Lp F q μ))
:
Heterogeneous scalar multiplication #
While the previous section is nominally more general than this one, and indeed, we could
use the constructions of the previous section to define the scalar multiplication herein,
we would lose some slight generality as we would need to require that 𝕜 is a nontrivially
normed field everywhere. Moreover, it would only simplify a few proofs.
instance
MeasureTheory.Lp.instHSMulSubtypeAEEqFunMemAddSubgroup
{α : Type u_1}
{𝕜 : Type u_3}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
{p q r : ENNReal}
[hpqr : p.HolderTriple q r]
[NormedRing 𝕜]
[NormedAddCommGroup E]
[MulActionWithZero 𝕜 E]
[IsBoundedSMul 𝕜 E]
:
Heterogeneous scalar multiplication of MeasureTheory.Lp functions by MeasureTheory.Lp
functions when the exponents satisfy ENNReal.HolderTriple p q r.
Equations
- MeasureTheory.Lp.instHSMulSubtypeAEEqFunMemAddSubgroup = { hSMul := fun (f : ↥(MeasureTheory.Lp 𝕜 p μ)) (g : ↥(MeasureTheory.Lp E q μ)) => MeasureTheory.MemLp.toLp (↑↑f • ↑↑g) ⋯ }
theorem
MeasureTheory.Lp.smul_def
{α : Type u_1}
{𝕜 : Type u_3}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
{p q r : ENNReal}
[hpqr : p.HolderTriple q r]
[NormedRing 𝕜]
[NormedAddCommGroup E]
[MulActionWithZero 𝕜 E]
[IsBoundedSMul 𝕜 E]
{f : ↥(Lp 𝕜 p μ)}
{g : ↥(Lp E q μ)}
:
theorem
MeasureTheory.Lp.coeFn_lpSMul
{α : Type u_1}
{𝕜 : Type u_3}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
{p q r : ENNReal}
[hpqr : p.HolderTriple q r]
[NormedRing 𝕜]
[NormedAddCommGroup E]
[MulActionWithZero 𝕜 E]
[IsBoundedSMul 𝕜 E]
(f : ↥(Lp 𝕜 p μ))
(g : ↥(Lp E q μ))
:
theorem
MeasureTheory.Lp.norm_smul_le
{α : Type u_1}
{𝕜 : Type u_3}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
{p q r : ENNReal}
[hpqr : p.HolderTriple q r]
[NormedRing 𝕜]
[NormedAddCommGroup E]
[MulActionWithZero 𝕜 E]
[IsBoundedSMul 𝕜 E]
(f : ↥(Lp 𝕜 p μ))
(g : ↥(Lp E q μ))
:
theorem
MeasureTheory.Lp.smul_add
{α : Type u_1}
{𝕜 : Type u_3}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
{p q r : ENNReal}
[hpqr : p.HolderTriple q r]
[NormedRing 𝕜]
[NormedAddCommGroup E]
[Module 𝕜 E]
[IsBoundedSMul 𝕜 E]
(f₁ f₂ : ↥(Lp 𝕜 p μ))
(g : ↥(Lp E q μ))
:
theorem
MeasureTheory.Lp.add_smul
{α : Type u_1}
{𝕜 : Type u_3}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
{p q r : ENNReal}
[hpqr : p.HolderTriple q r]
[NormedRing 𝕜]
[NormedAddCommGroup E]
[Module 𝕜 E]
[IsBoundedSMul 𝕜 E]
(f : ↥(Lp 𝕜 p μ))
(g₁ g₂ : ↥(Lp E q μ))
:
@[simp]
theorem
MeasureTheory.Lp.smul_zero
{α : Type u_1}
{𝕜 : Type u_3}
(E : Type u_4)
{m : MeasurableSpace α}
{μ : Measure α}
{p : ENNReal}
(q : ENNReal)
{r : ENNReal}
[hpqr : p.HolderTriple q r]
[NormedRing 𝕜]
[NormedAddCommGroup E]
[Module 𝕜 E]
[IsBoundedSMul 𝕜 E]
(f : ↥(Lp 𝕜 p μ))
:
@[simp]
theorem
MeasureTheory.Lp.zero_smul
{α : Type u_1}
(𝕜 : Type u_3)
{E : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
(p : ENNReal)
{q r : ENNReal}
[hpqr : p.HolderTriple q r]
[NormedRing 𝕜]
[NormedAddCommGroup E]
[Module 𝕜 E]
[IsBoundedSMul 𝕜 E]
(f : ↥(Lp E q μ))
:
@[simp]
theorem
MeasureTheory.Lp.smul_neg
{α : Type u_1}
{𝕜 : Type u_3}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
{p q r : ENNReal}
[hpqr : p.HolderTriple q r]
[NormedRing 𝕜]
[NormedAddCommGroup E]
[Module 𝕜 E]
[IsBoundedSMul 𝕜 E]
(f : ↥(Lp 𝕜 p μ))
(g : ↥(Lp E q μ))
:
@[simp]
theorem
MeasureTheory.Lp.neg_smul
{α : Type u_1}
{𝕜 : Type u_3}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
{p q r : ENNReal}
[hpqr : p.HolderTriple q r]
[NormedRing 𝕜]
[NormedAddCommGroup E]
[Module 𝕜 E]
[IsBoundedSMul 𝕜 E]
(f : ↥(Lp 𝕜 p μ))
(g : ↥(Lp E q μ))
:
theorem
MeasureTheory.Lp.neg_smul_neg
{α : Type u_1}
{𝕜 : Type u_3}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
{p q r : ENNReal}
[hpqr : p.HolderTriple q r]
[NormedRing 𝕜]
[NormedAddCommGroup E]
[Module 𝕜 E]
[IsBoundedSMul 𝕜 E]
(f : ↥(Lp 𝕜 p μ))
(g : ↥(Lp E q μ))
:
theorem
MeasureTheory.Lp.smul_assoc
{α : Type u_1}
{𝕜' : Type u_2}
{𝕜 : Type u_3}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
{p q r : ENNReal}
[hpqr : p.HolderTriple q r]
[NormedRing 𝕜]
[NormedAddCommGroup E]
[Module 𝕜 E]
[IsBoundedSMul 𝕜 E]
[NormedRing 𝕜']
[Module 𝕜' E]
[Module 𝕜' 𝕜]
[IsBoundedSMul 𝕜' E]
[IsBoundedSMul 𝕜' 𝕜]
[IsScalarTower 𝕜' 𝕜 E]
(c : 𝕜')
(f : ↥(Lp 𝕜 p μ))
(g : ↥(Lp E q μ))
:
theorem
MeasureTheory.Lp.smul_comm
{α : Type u_1}
{𝕜' : Type u_2}
{𝕜 : Type u_3}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
{p q r : ENNReal}
[hpqr : p.HolderTriple q r]
[NormedRing 𝕜]
[NormedAddCommGroup E]
[Module 𝕜 E]
[IsBoundedSMul 𝕜 E]
[NormedRing 𝕜']
[Module 𝕜' E]
[Module 𝕜' 𝕜]
[IsBoundedSMul 𝕜' E]
[IsBoundedSMul 𝕜' 𝕜]
[SMulCommClass 𝕜' 𝕜 E]
(c : 𝕜')
(f : ↥(Lp 𝕜 p μ))
(g : ↥(Lp E q μ))
: