Hölder's inequality for lp spaces

This file proves Hölder's inequality for lp spaces. We follow the established pattern for Hölder's inequality for MeasureTheory.Lp of generalizing multiplication to any continuous bilinear map. Since lp is a dependent Π-type, we actually need a uniformly bounded family of bilinear maps.

Implementation notes

Although it would be possible to bundle the uniformly bounded family of bilinear maps into a term B : lp (fun i ↦ E i →L[𝕜] F i →L[𝕜] G i) ∞, this has some downsides. For example, we would then have to bundle fun i ↦ (B i).flip into a term of this type in order to use it, so we opt to leave B unbundled.

noncomputable def lp.mapCLM {α : Type u_1} {𝕜 : Type u_2} {E : α → Type u_3} {F : α → Type u_4} [NontriviallyNormedField 𝕜] [(i : α) → NormedAddCommGroup (E i)] [(i : α) → NormedSpace 𝕜 (E i)] [(i : α) → NormedAddCommGroup (F i)] [(i : α) → NormedSpace 𝕜 (F i)] (p : ENNReal) [Fact (1 ≤ p)] (T : (i : α) → E i →L[𝕜] F i) {K : ℝ} (hK : 0 ≤ K) (hTK : ∀ (i : α), ‖T i‖ ≤ K) : ↥(lp E p) →L[𝕜] ↥(lp F p)

A uniformly bounded family of continuous linear maps, as a continuous linear map on the lp space.

Equations

• lp.mapCLM p T hK hTK = { toFun := fun (x : ↥(lp E p)) => ⟨fun (i : α) => (T i) (↑x i), ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous K ⋯

@[simp]

theorem lp.mapCLM_apply_coe {α : Type u_1} {𝕜 : Type u_2} {E : α → Type u_3} {F : α → Type u_4} [NontriviallyNormedField 𝕜] [(i : α) → NormedAddCommGroup (E i)] [(i : α) → NormedSpace 𝕜 (E i)] [(i : α) → NormedAddCommGroup (F i)] [(i : α) → NormedSpace 𝕜 (F i)] (p : ENNReal) [Fact (1 ≤ p)] (T : (i : α) → E i →L[𝕜] F i) {K : ℝ} (hK : 0 ≤ K) (hTK : ∀ (i : α), ‖T i‖ ≤ K) (x : ↥(lp E p)) (i : α) : ↑((mapCLM p T hK hTK) x) i = (T i) (↑x i)

theorem lp.norm_mapCLM_le {α : Type u_1} {𝕜 : Type u_2} {E : α → Type u_3} {F : α → Type u_4} [NontriviallyNormedField 𝕜] [(i : α) → NormedAddCommGroup (E i)] [(i : α) → NormedSpace 𝕜 (E i)] [(i : α) → NormedAddCommGroup (F i)] [(i : α) → NormedSpace 𝕜 (F i)] (p : ENNReal) [Fact (1 ≤ p)] (T : (i : α) → E i →L[𝕜] F i) {K : ℝ} (hK : 0 ≤ K) (hTK : ∀ (i : α), ‖T i‖ ≤ K) : ‖mapCLM p T hK hTK‖ ≤ K

theorem lp.norm_tsumCLM_le {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] : ‖tsumCLM 𝕜 α E‖ ≤ 1

theorem Memℓp.bilin_of_top_left {ι : Type u_1} {𝕜 : Type u_2} {E : ι → Type u_3} {F : ι → Type u_4} {G : ι → Type u_5} [RCLike 𝕜] [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι) → NormedAddCommGroup (F i)] [(i : ι) → NormedSpace 𝕜 (F i)] [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace 𝕜 (G i)] {q : ENNReal} (B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i) {K : ℝ} (hBK : ∀ (i : ι), ‖B i‖ ≤ K) {e : (i : ι) → E i} {f : (i : ι) → F i} (he : Memℓp e ⊤) (hf : Memℓp f q) : Memℓp (fun (i : ι) => ((B i) (e i)) (f i)) q

theorem Memℓp.bilin_of_top_right {ι : Type u_1} {𝕜 : Type u_2} {E : ι → Type u_3} {F : ι → Type u_4} {G : ι → Type u_5} [RCLike 𝕜] [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι) → NormedAddCommGroup (F i)] [(i : ι) → NormedSpace 𝕜 (F i)] [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace 𝕜 (G i)] {p : ENNReal} (B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i) {K : ℝ} (hBK : ∀ (i : ι), ‖B i‖ ≤ K) {e : (i : ι) → E i} {f : (i : ι) → F i} (he : Memℓp e p) (hf : Memℓp f ⊤) : Memℓp (fun (i : ι) => ((B i) (e i)) (f i)) p

theorem Memℓp.bilin_of_zero_left {ι : Type u_1} {𝕜 : Type u_2} {E : ι → Type u_3} {F : ι → Type u_4} {G : ι → Type u_5} [RCLike 𝕜] [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι) → NormedAddCommGroup (F i)] [(i : ι) → NormedSpace 𝕜 (F i)] [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace 𝕜 (G i)] (B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i) {e : (i : ι) → E i} {f : (i : ι) → F i} (he : Memℓp e 0) : Memℓp (fun (i : ι) => ((B i) (e i)) (f i)) 0

theorem Memℓp.bilin_of_zero_right {ι : Type u_1} {𝕜 : Type u_2} {E : ι → Type u_3} {F : ι → Type u_4} {G : ι → Type u_5} [RCLike 𝕜] [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι) → NormedAddCommGroup (F i)] [(i : ι) → NormedSpace 𝕜 (F i)] [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace 𝕜 (G i)] (B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i) {e : (i : ι) → E i} {f : (i : ι) → F i} (hf : Memℓp f 0) : Memℓp (fun (i : ι) => ((B i) (e i)) (f i)) 0

theorem Memℓp.holder_top_left_bound {ι : Type u_1} {𝕜 : Type u_2} {E : ι → Type u_3} {F : ι → Type u_4} {G : ι → Type u_5} [RCLike 𝕜] [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι) → NormedAddCommGroup (F i)] [(i : ι) → NormedSpace 𝕜 (F i)] [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace 𝕜 (G i)] {q : ENNReal} {e : (i : ι) → E i} {f : (i : ι) → F i} (B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i) {K C D : ℝ} (hBK : ∀ (i : ι), ‖B i‖ ≤ K) (hK : 0 ≤ K) (hC : 0 ≤ C) (hCe : ∀ (i : ι), ‖e i‖ ≤ C) (hDf : ∀ (s : Finset ι), ∑ i ∈ s, ‖f i‖ ^ q.toReal ≤ D) (s : Finset ι) : ∑ i ∈ s, ‖((B i) (e i)) (f i)‖ ^ q.toReal ≤ (K * C) ^ q.toReal * D

theorem Memℓp.holder_top_right_bound {ι : Type u_1} {𝕜 : Type u_2} {E : ι → Type u_3} {F : ι → Type u_4} {G : ι → Type u_5} [RCLike 𝕜] [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι) → NormedAddCommGroup (F i)] [(i : ι) → NormedSpace 𝕜 (F i)] [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace 𝕜 (G i)] {p : ENNReal} {e : (i : ι) → E i} {f : (i : ι) → F i} (B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i) {K C D : ℝ} (hBK : ∀ (i : ι), ‖B i‖ ≤ K) (hK : 0 ≤ K) (hD : 0 ≤ D) (hCe : ∀ (s : Finset ι), ∑ i ∈ s, ‖e i‖ ^ p.toReal ≤ C) (hDf : ∀ (i : ι), ‖f i‖ ≤ D) (s : Finset ι) : ∑ i ∈ s, ‖((B i) (e i)) (f i)‖ ^ p.toReal ≤ (K * D) ^ p.toReal * C

theorem Memℓp.holder_gen_bound {ι : Type u_1} {𝕜 : Type u_2} {E : ι → Type u_3} {F : ι → Type u_4} {G : ι → Type u_5} [RCLike 𝕜] [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι) → NormedAddCommGroup (F i)] [(i : ι) → NormedSpace 𝕜 (F i)] [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace 𝕜 (G i)] {p q : ENNReal} (r : ENNReal) [hpqr : p.HolderTriple q r] {e : (i : ι) → E i} {f : (i : ι) → F i} (hp : 0 < p.toReal) (hq : 0 < q.toReal) (B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i) {K C D : ℝ} (hBK : ∀ (i : ι), ‖B i‖ ≤ K) (hK : 0 ≤ K) (hC : 0 ≤ C) (hCe : ∀ (s : Finset ι), ∑ i ∈ s, ‖e i‖ ^ p.toReal ≤ C) (hDf : ∀ (s : Finset ι), ∑ i ∈ s, ‖f i‖ ^ q.toReal ≤ D) (s : Finset ι) : ∑ i ∈ s, ‖((B i) (e i)) (f i)‖ ^ r.toReal ≤ K ^ r.toReal * C ^ (r.toReal / p.toReal) * D ^ (r.toReal / q.toReal)

theorem Memℓp.holder {ι : Type u_1} {𝕜 : Type u_2} {E : ι → Type u_3} {F : ι → Type u_4} {G : ι → Type u_5} [RCLike 𝕜] [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι) → NormedAddCommGroup (F i)] [(i : ι) → NormedSpace 𝕜 (F i)] [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace 𝕜 (G i)] {p q : ENNReal} (r : ENNReal) [hpqr : p.HolderTriple q r] {e : (i : ι) → E i} {f : (i : ι) → F i} (he : Memℓp e p) (hf : Memℓp f q) (B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i) {K : ℝ} (hBK : ∀ (i : ι), ‖B i‖ ≤ K) : Memℓp (fun (i : ι) => ((B i) (e i)) (f i)) r

def lp.holder {ι : Type u_1} {𝕜 : Type u_2} {E : ι → Type u_3} {F : ι → Type u_4} {G : ι → Type u_5} [RCLike 𝕜] [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι) → NormedAddCommGroup (F i)] [(i : ι) → NormedSpace 𝕜 (F i)] [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace 𝕜 (G i)] {p q : ENNReal} (r : ENNReal) [hpqr : p.HolderTriple q r] (B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i) {K : ℝ} (hBK : ∀ (i : ι), ‖B i‖ ≤ K) (e : ↥(lp E p)) (f : ↥(lp F q)) : ↥(lp G r)

The map between lp spaces satisfying ENNReal.HolderTriple induced by a uniformly bounded family of continuous bilinear maps on the underlying spaces.

Equations

• lp.holder r B hBK e f = ⟨fun (i : ι) => ((B i) (↑e i)) (↑f i), ⋯⟩

@[simp]

theorem lp.holder_coe {ι : Type u_1} {𝕜 : Type u_2} {E : ι → Type u_3} {F : ι → Type u_4} {G : ι → Type u_5} [RCLike 𝕜] [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι) → NormedAddCommGroup (F i)] [(i : ι) → NormedSpace 𝕜 (F i)] [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace 𝕜 (G i)] {p q : ENNReal} (r : ENNReal) [hpqr : p.HolderTriple q r] (B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i) {K : ℝ} (hBK : ∀ (i : ι), ‖B i‖ ≤ K) (e : ↥(lp E p)) (f : ↥(lp F q)) (i : ι) : ↑(holder r B hBK e f) i = ((B i) (↑e i)) (↑f i)

noncomputable def lp.holderₗ {ι : Type u_1} {𝕜 : Type u_2} {E : ι → Type u_3} {F : ι → Type u_4} {G : ι → Type u_5} [RCLike 𝕜] [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι) → NormedAddCommGroup (F i)] [(i : ι) → NormedSpace 𝕜 (F i)] [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace 𝕜 (G i)] {p q : ENNReal} (r : ENNReal) [hpqr : p.HolderTriple q r] (B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i) {K : ℝ} (hBK : ∀ (i : ι), ‖B i‖ ≤ K) : ↥(lp E p) →ₗ[𝕜] ↥(lp F q) →ₗ[𝕜] ↥(lp G r)

lp.holder as a bilinear map.

Equations

• lp.holderₗ r B hBK = LinearMap.mk₂ 𝕜 (lp.holder r B hBK) ⋯ ⋯ ⋯ ⋯

@[simp]

theorem lp.holderₗ_apply_apply_coe {ι : Type u_1} {𝕜 : Type u_2} {E : ι → Type u_3} {F : ι → Type u_4} {G : ι → Type u_5} [RCLike 𝕜] [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι) → NormedAddCommGroup (F i)] [(i : ι) → NormedSpace 𝕜 (F i)] [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace 𝕜 (G i)] {p q : ENNReal} (r : ENNReal) [hpqr : p.HolderTriple q r] (B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i) {K : ℝ} (hBK : ∀ (i : ι), ‖B i‖ ≤ K) (m : ↥(lp E p)) (f : ↥(lp F q)) (i : ι) : ↑(((holderₗ r B hBK) m) f) i = ((B i) (↑m i)) (↑f i)

noncomputable def lp.holderL {ι : Type u_1} {𝕜 : Type u_2} {E : ι → Type u_3} {F : ι → Type u_4} {G : ι → Type u_5} [RCLike 𝕜] [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι) → NormedAddCommGroup (F i)] [(i : ι) → NormedSpace 𝕜 (F i)] [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace 𝕜 (G i)] {p q : ENNReal} (r : ENNReal) [hpqr : p.HolderTriple q r] [Fact (1 ≤ p)] [Fact (1 ≤ q)] [Fact (1 ≤ r)] (B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i) {K : NNReal} (hBK : ∀ (i : ι), ‖B i‖ ≤ ↑K) : ↥(lp E p) →L[𝕜] ↥(lp F q) →L[𝕜] ↥(lp G r)

lp.holder as a continuous bilinear map.

Equations

• lp.holderL r B hBK = (lp.holderₗ r B hBK).mkContinuous₂ ↑K ⋯

theorem lp.norm_holderL_le {ι : Type u_1} {𝕜 : Type u_2} {E : ι → Type u_3} {F : ι → Type u_4} {G : ι → Type u_5} [RCLike 𝕜] [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι) → NormedAddCommGroup (F i)] [(i : ι) → NormedSpace 𝕜 (F i)] [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace 𝕜 (G i)] {p q : ENNReal} (r : ENNReal) [hpqr : p.HolderTriple q r] [Fact (1 ≤ p)] [Fact (1 ≤ q)] [Fact (1 ≤ r)] (B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i) {K : NNReal} (hBK : ∀ (i : ι), ‖B i‖ ≤ ↑K) : ‖holderL r B hBK‖ ≤ ↑K

noncomputable def lp.dualPairing {ι : Type u_1} {𝕜 : Type u_2} {E : ι → Type u_3} {F : ι → Type u_4} [RCLike 𝕜] [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι) → NormedAddCommGroup (F i)] [(i : ι) → NormedSpace 𝕜 (F i)] (p q : ENNReal) {H : Type u_6} [NormedAddCommGroup H] [NormedSpace 𝕜 H] [CompleteSpace H] [Fact (1 ≤ p)] [Fact (1 ≤ q)] [p.HolderConjugate q] (B : (i : ι) → E i →L[𝕜] F i →L[𝕜] H) {K : NNReal} (hBK : ∀ (i : ι), ‖B i‖ ≤ ↑K) : ↥(lp E p) →L[𝕜] ↥(lp F q) →L[𝕜] H

The natural pairing between lp E p and lp F q (for Hölder conjugate p q : ℝ≥0∞) with values in a space H induced by a family of bilinear maps B : (i : ι) → E i →L[𝕜] F i →L[𝕜] H.

This is given by ∑' i, B (e i) (f i).

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 (fun _ ↦ StrongDual 𝕜 E) p →L[𝕜] StrongDual 𝕜 (lp E q).

Equations

• lp.dualPairing p q B hBK = ContinuousLinearMap.postcomp (↥(lp F q)) (lp.tsumCLM 𝕜 ι H) ∘SL lp.holderL 1 B hBK

theorem lp.dualPairing_apply {ι : Type u_1} {𝕜 : Type u_2} {E : ι → Type u_3} {F : ι → Type u_4} [RCLike 𝕜] [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι) → NormedAddCommGroup (F i)] [(i : ι) → NormedSpace 𝕜 (F i)] {p q : ENNReal} {H : Type u_6} [NormedAddCommGroup H] [NormedSpace 𝕜 H] [CompleteSpace H] [Fact (1 ≤ p)] [Fact (1 ≤ q)] [p.HolderConjugate q] (B : (i : ι) → E i →L[𝕜] F i →L[𝕜] H) {K : NNReal} (hBK : ∀ (i : ι), ‖B i‖ ≤ ↑K) (e : ↥(lp E p)) (f : ↥(lp F q)) : ((dualPairing p q B hBK) e) f = ∑' (i : ι), ((B i) (↑e i)) (↑f i)

theorem lp.norm_dualPairing {ι : Type u_1} {𝕜 : Type u_2} {E : ι → Type u_3} {F : ι → Type u_4} [RCLike 𝕜] [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι) → NormedAddCommGroup (F i)] [(i : ι) → NormedSpace 𝕜 (F i)] {p q : ENNReal} {H : Type u_6} [NormedAddCommGroup H] [NormedSpace 𝕜 H] [CompleteSpace H] [Fact (1 ≤ p)] [Fact (1 ≤ q)] [p.HolderConjugate q] (B : (i : ι) → E i →L[𝕜] F i →L[𝕜] H) {K : NNReal} (hBK : ∀ (i : ι), ‖B i‖ ≤ ↑K) : ‖dualPairing p q B hBK‖ ≤ ↑K