Skip to content

Commit 859caf7

Browse files
j-loreauxpre-commit-ci-lite[bot]
j-loreaux
and
pre-commit-ci-lite[bot]
committed
feat: Hölder framework for lp spaces (#35197)
Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>
1 parent 890f6be commit 859caf7

6 files changed

Lines changed: 311 additions & 9 deletions

File tree

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2167,6 +2167,7 @@ public import Mathlib.Analysis.Normed.Lp.PiLp
21672167
public import Mathlib.Analysis.Normed.Lp.ProdLp
21682168
public import Mathlib.Analysis.Normed.Lp.SmoothApprox
21692169
public import Mathlib.Analysis.Normed.Lp.WithLp
2170+
public import Mathlib.Analysis.Normed.Lp.lpHolder
21702171
public import Mathlib.Analysis.Normed.Lp.lpSpace
21712172
public import Mathlib.Analysis.Normed.Module.Alternating.Basic
21722173
public import Mathlib.Analysis.Normed.Module.Alternating.Curry

‎Mathlib/Analysis/Normed/Lp/LpEquiv.lean‎

Lines changed: 0 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -53,13 +53,6 @@ section Finite
5353

5454
variable [Finite α]
5555

56-
/-- When `α` is `Finite`, every `f : PreLp E p` satisfies `Memℓp f p`. -/
57-
theorem Memℓp.all (f : ∀ i, E i) : Memℓp f p := by
58-
rcases p.trichotomy with (rfl | rfl | _h)
59-
· exact memℓp_zero_iff.mpr { i : α | f i ≠ 0 }.toFinite
60-
· exact memℓp_infty_iff.mpr (Set.Finite.bddAbove (Set.range fun i : α ↦ ‖f i‖).toFinite)
61-
· cases nonempty_fintype α; exact memℓp_gen ⟨Finset.univ.sum _, hasSum_fintype _⟩
62-
6356
/-- The canonical `Equiv` between `lp E p ≃ PiLp p E` when `E : α → Type u` with `[Finite α]`. -/
6457
def Equiv.lpPiLp : lp E p ≃ PiLp p E where
6558
toFun f := toLp p ⇑f

‎Mathlib/Analysis/Normed/Lp/lpHolder.lean‎

Lines changed: 285 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,285 @@
1+
/-
2+
Copyright (c) 2026 Jireh Loreaux. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Jireh Loreaux
5+
-/
6+
module
7+
8+
public import Mathlib.Analysis.Normed.Lp.lpSpace
9+
public import Mathlib.Analysis.Normed.Operator.Bilinear
10+
public import Mathlib.Tactic.Positivity.Finset
11+
12+
/-! # Hölder's inequality for `lp` spaces
13+
14+
This file proves Hölder's inequality for `lp` spaces. We follow the established pattern for
15+
Hölder's inequality for `MeasureTheory.Lp` of generalizing multiplication to any continuous bilinear
16+
map. Since `lp` is a dependent Π-type, we actually need a uniformly bounded family of bilinear maps.
17+
18+
## Implementation notes
19+
20+
Although it would be possible to bundle the uniformly bounded family of bilinear maps into a term
21+
`B : lp (fun i ↦ E i →L[𝕜] F i →L[𝕜] G i) ∞`, this has some downsides. For example, we would
22+
then have to bundle `fun i ↦ (B i).flip` into a term of this type in order to use it, so we opt to
23+
leave `B` unbundled.
24+
25+
-/
26+
27+
@[expose] public section
28+
29+
open scoped lp ENNReal NNReal
30+
31+
namespace lp
32+
-- the material in this section could be moved to `lpSpace`, but would require some extra imports
33+
34+
section NontriviallyNormedField
35+
36+
variable {α 𝕜 : Type*} {E F : α → Type*} [NontriviallyNormedField 𝕜]
37+
variable [∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace 𝕜 (E i)]
38+
[∀ i, NormedAddCommGroup (F i)] [∀ i, NormedSpace 𝕜 (F i)]
39+
variable {p q r : ℝ≥0∞}
40+
41+
/-- A uniformly bounded family of continuous linear maps, as a continuous linear map
42+
on the `lp` space. -/
43+
@[simps!]
44+
noncomputable def mapCLM (p : ℝ≥0∞) [Fact (1 ≤ p)]
45+
(T : ∀ i, E i →L[𝕜] F i) {K : ℝ} (hK : 0 ≤ K) (hTK : ∀ i, ‖T i‖ ≤ K) :
46+
lp E p →L[𝕜] lp F p :=
47+
haveI key (i : α) (x : E i) : ‖T i x‖ ≤ K * ‖x‖ := (T i).le_of_opNorm_le (hTK i) _
48+
LinearMap.mkContinuous
49+
{ toFun x := ⟨fun i ↦ T i (⇑x i), lp.memℓp x |>.norm.const_mul K |>.mono
50+
(fun _ ↦ by simpa [abs_of_nonneg hK] using key ..) |>.of_norm⟩
51+
map_add' _ _ := by ext; simp
52+
map_smul' _ _ := by ext; simp }
53+
K
54+
fun x ↦ by
55+
rw [← norm_toNorm]
56+
conv_rhs => rw [← norm_toNorm, ← abs_of_nonneg hK, ← Real.norm_eq_abs, ← norm_smul]
57+
apply norm_mono (zero_lt_one.trans_le Fact.out).ne' fun i ↦ ?_
58+
simpa [abs_of_nonneg hK] using key ..
59+
60+
lemma norm_mapCLM_le (p : ℝ≥0∞) [Fact (1 ≤ p)]
61+
(T : ∀ i, E i →L[𝕜] F i) {K : ℝ} (hK : 0 ≤ K) (hTK : ∀ i, ‖T i‖ ≤ K) :
62+
‖mapCLM p T hK hTK‖ ≤ K :=
63+
LinearMap.mkContinuous_norm_le _ hK _
64+
65+
end NontriviallyNormedField
66+
67+
lemma norm_tsumCLM_le {α 𝕜 E : Type*} [NontriviallyNormedField 𝕜]
68+
[NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] :
69+
‖tsumCLM 𝕜 α E‖ ≤ 1 :=
70+
LinearMap.mkContinuous_norm_le _ zero_le_one _
71+
72+
end lp
73+
74+
variable {ι 𝕜 : Type*} {E F G : ι → Type*} [RCLike 𝕜]
75+
variable [∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace 𝕜 (E i)]
76+
[∀ i, NormedAddCommGroup (F i)] [∀ i, NormedSpace 𝕜 (F i)]
77+
[∀ i, NormedAddCommGroup (G i)] [∀ i, NormedSpace 𝕜 (G i)]
78+
79+
open ENNReal
80+
81+
variable {p q : ℝ≥0∞} (r : ℝ≥0∞) [hpqr : p.HolderTriple q r]
82+
83+
namespace Memℓp
84+
85+
theorem bilin_of_top_left (B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i)
86+
{K : ℝ} (hBK : ∀ i, ‖B i‖ ≤ K) {e : Π i, E i} {f : Π i, F i}
87+
(he : Memℓp e ∞) (hf : Memℓp f q) :
88+
Memℓp (fun i ↦ B i (e i) (f i)) q := by
89+
obtain (h | h) := isEmpty_or_nonempty ι
90+
· exact all _
91+
obtain ⟨C, hC⟩ := by
92+
simpa [memℓp_infty_iff, BddAbove, Set.Nonempty, Set.range, upperBounds] using he
93+
refine hf.norm.const_mul (K * C) |>.mono fun i ↦ ?_
94+
have hK_nonneg : 0 ≤ K := norm_nonneg (B (Classical.arbitrary ι)) |>.trans <| hBK _
95+
calc
96+
‖B i (e i) (f i)‖ ≤ ‖B i‖ * ‖e i‖ * ‖f i‖ := (B i (e i)).le_of_opNorm_le ((B i).le_opNorm _) _
97+
_ ≤ K * C * ‖f i‖ := by gcongr; exacts [hBK i, hC i]
98+
99+
theorem bilin_of_top_right (B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i)
100+
{K : ℝ} (hBK : ∀ i, ‖B i‖ ≤ K) {e : Π i, E i} {f : Π i, F i}
101+
(he : Memℓp e p) (hf : Memℓp f ∞) :
102+
Memℓp (fun i ↦ B i (e i) (f i)) p :=
103+
hf.bilin_of_top_left (fun i ↦ (B i).flip) (by simpa using hBK) he
104+
105+
theorem bilin_of_zero_left (B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i)
106+
{e : Π i, E i} {f : Π i, F i} (he : Memℓp e 0) :
107+
Memℓp (fun i ↦ B i (e i) (f i)) 0 := by
108+
rw [memℓp_zero_iff] at he ⊢
109+
exact he.subset fun i hi h ↦ hi <| by simp [h]
110+
111+
theorem bilin_of_zero_right (B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i)
112+
{e : Π i, E i} {f : Π i, F i} (hf : Memℓp f 0) :
113+
Memℓp (fun i ↦ B i (e i) (f i)) 0 :=
114+
hf.bilin_of_zero_left (fun i ↦ (B i).flip)
115+
116+
lemma holder_top_left_bound
117+
{e : (i : ι) → E i} {f : (i : ι) → F i} (B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i)
118+
{K C D : ℝ} (hBK : ∀ i, ‖B i‖ ≤ K) (hK : 0 ≤ K) (hC : 0 ≤ C)
119+
(hCe : ∀ i, ‖e i‖ ≤ C) (hDf : ∀ s, ∑ i ∈ s, ‖f i‖ ^ q.toReal ≤ D) (s : Finset ι) :
120+
∑ i ∈ s, ‖B i (e i) (f i)‖ ^ q.toReal ≤ (K * C) ^ q.toReal * D := by
121+
grw [← hDf s, s.mul_sum]
122+
apply s.sum_le_sum fun i hi ↦ ?_
123+
rw [← Real.mul_rpow (by positivity) (by positivity)]
124+
gcongr
125+
exact (B i (e i)).le_of_opNorm_le ((B i).le_of_opNorm_le_of_le (hBK i) (hCe i)) _
126+
127+
lemma holder_top_right_bound
128+
{e : (i : ι) → E i} {f : (i : ι) → F i} (B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i)
129+
{K C D : ℝ} (hBK : ∀ i, ‖B i‖ ≤ K) (hK : 0 ≤ K) (hD : 0 ≤ D)
130+
(hCe : ∀ s, ∑ i ∈ s, ‖e i‖ ^ p.toReal ≤ C) (hDf : ∀ i, ‖f i‖ ≤ D) (s : Finset ι) :
131+
∑ i ∈ s, ‖B i (e i) (f i)‖ ^ p.toReal ≤ (K * D) ^ p.toReal * C :=
132+
holder_top_left_bound (B · |>.flip) (by simpa) hK hD hDf hCe s
133+
134+
lemma holder_gen_bound {e : (i : ι) → E i} {f : (i : ι) → F i}
135+
(hp : 0 < p.toReal) (hq : 0 < q.toReal)
136+
(B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i) {K C D : ℝ} (hBK : ∀ i, ‖B i‖ ≤ K)
137+
(hK : 0 ≤ K) (hC : 0 ≤ C) (hCe : ∀ s, ∑ i ∈ s, ‖e i‖ ^ p.toReal ≤ C)
138+
(hDf : ∀ s, ∑ i ∈ s, ‖f i‖ ^ q.toReal ≤ D) (s : Finset ι) :
139+
∑ i ∈ s, ‖B i (e i) (f i)‖ ^ r.toReal ≤
140+
K ^ r.toReal * C ^ (r.toReal / p.toReal) * D ^ (r.toReal / q.toReal) := by
141+
have hpqr := hpqr.toReal r hp hq
142+
have hr := hpqr.pos'
143+
suffices ∑ i ∈ s, (‖e i‖ * ‖f i‖) ^ r.toReal ≤
144+
C ^ (r.toReal / p.toReal) * D ^ (r.toReal / q.toReal) from calc
145+
∑ i ∈ s, ‖B i (e i) (f i)‖ ^ r.toReal
146+
_ ≤ K ^ r.toReal * ∑ i ∈ s, (‖e i‖ * ‖f i‖) ^ r.toReal := by
147+
rw [s.mul_sum]
148+
gcongr with i hi
149+
rw [← Real.mul_rpow (by positivity) (by positivity), ← mul_assoc]
150+
gcongr
151+
exact (B i (e i)).le_of_opNorm_le ((B i).le_of_opNorm_le (hBK i) _) _
152+
_ ≤ _ := by
153+
rw [mul_assoc]
154+
gcongr
155+
calc
156+
_ ≤ (∑ i ∈ s, ‖e i‖ ^ p.toReal) ^ (r.toReal / p.toReal) *
157+
(∑ i ∈ s, ‖f i‖ ^ q.toReal) ^ (r.toReal / q.toReal) := by
158+
apply Real.Lr_rpow_le_Lp_mul_Lq_of_nonneg s hpqr <;> (intros; positivity)
159+
_ ≤ _ := by
160+
gcongr
161+
· exact hCe s
162+
· exact hDf s
163+
164+
lemma holder {e : (i : ι) → E i} {f : (i : ι) → F i} (he : Memℓp e p) (hf : Memℓp f q)
165+
(B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i) {K : ℝ} (hBK : ∀ i, ‖B i‖ ≤ K) :
166+
Memℓp (fun i ↦ B i (e i) (f i)) r := by
167+
obtain (h | h) := isEmpty_or_nonempty ι
168+
· exact all _
169+
have hK : 0 ≤ K := norm_nonneg (B (Classical.arbitrary ι)) |>.trans <| hBK _
170+
have hpqr' := hpqr.inv_eq
171+
obtain (rfl | rfl | hp) := p.trichotomy
172+
· simp_all only [ENNReal.inv_zero, top_add, inv_eq_top]
173+
exact he.bilin_of_zero_left B
174+
· simp_all only [inv_top, zero_add, inv_inj]
175+
exact he.bilin_of_top_left B hBK hf
176+
obtain (rfl | rfl | hq) := q.trichotomy
177+
· simp_all only [ENNReal.inv_zero, add_top, inv_eq_top]
178+
exact hf.bilin_of_zero_right B
179+
· simp_all only [inv_top, add_zero, inv_inj]
180+
exact he.bilin_of_top_right B hBK hf
181+
obtain ⟨C, hC, hCe⟩ := memℓp_gen_iff'' hp |>.mp he
182+
obtain ⟨D, hD, hDf⟩ := memℓp_gen_iff'' hq |>.mp hf
183+
exact memℓp_gen' <| holder_gen_bound r hp hq B hBK hK hC hCe hDf
184+
185+
end Memℓp
186+
187+
namespace lp
188+
189+
/-- The map between `lp` spaces satisfying `ENNReal.HolderTriple` induced by a
190+
uniformly bounded family of continuous bilinear maps on the underlying spaces. -/
191+
@[simps]
192+
def holder (B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i) {K : ℝ} (hBK : ∀ i, ‖B i‖ ≤ K)
193+
(e : lp E p) (f : lp F q) :
194+
lp G r where
195+
val := fun i ↦ B i (e i) (f i)
196+
property := (lp.memℓp e).holder _ (lp.memℓp f) B hBK
197+
198+
/-- `lp.holder` as a bilinear map. -/
199+
@[simps!]
200+
noncomputable def holderₗ (B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i) {K : ℝ} (hBK : ∀ i, ‖B i‖ ≤ K) :
201+
lp E p →ₗ[𝕜] lp F q →ₗ[𝕜] lp G r :=
202+
.mk₂ 𝕜 (holder r B hBK) ?_ ?_ ?_ ?_ where finally
203+
all_goals intros; ext; simp
204+
205+
/-- `lp.holder` as a continuous bilinear map. -/
206+
noncomputable def holderL [Fact (1 ≤ p)] [Fact (1 ≤ q)] [Fact (1 ≤ r)]
207+
(B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i) {K : ℝ≥0} (hBK : ∀ i, ‖B i‖ ≤ K) :
208+
lp E p →L[𝕜] lp F q →L[𝕜] lp G r :=
209+
holderₗ r B hBK |>.mkContinuous₂ K fun e f ↦ by
210+
obtain ⟨(rfl | hp), (rfl | hq)⟩ := And.intro p.dichotomy q.dichotomy
211+
· obtain rfl : r = ⊤ := ENNReal.HolderTriple.unique ∞ ∞ r ∞
212+
refine norm_le_of_forall_le (by positivity) fun i ↦ ?_
213+
refine (B i).le_of_opNorm₂_le_of_le (hBK i) ?_ ?_
214+
all_goals exact norm_apply_le_norm (by simp) ..
215+
· obtain rfl : r = q := ENNReal.HolderTriple.unique ∞ q r q
216+
refine norm_le_of_forall_sum_le (zero_lt_one.trans_le hq) (by positivity) fun s ↦ ?_
217+
rw [Real.mul_rpow (by positivity) (by positivity)]
218+
refine Memℓp.holder_top_left_bound B hBK
219+
(by positivity) (by positivity) (norm_apply_le_norm (by simp) _) ?_ s
220+
exact sum_rpow_le_norm_rpow (zero_lt_one.trans_le hq) f
221+
· obtain rfl : r = p := ENNReal.HolderTriple.unique p ∞ r p
222+
refine norm_le_of_forall_sum_le (zero_lt_one.trans_le hp) (by positivity) fun s ↦ ?_
223+
rw [mul_right_comm, Real.mul_rpow (by positivity) (by positivity)]
224+
refine Memℓp.holder_top_right_bound B hBK
225+
(by positivity) (by positivity) ?_ (norm_apply_le_norm (by simp) _) s
226+
exact sum_rpow_le_norm_rpow (zero_lt_one.trans_le hp) e
227+
· have hpqr := hpqr.toReal r (zero_lt_one.trans_le hp) (zero_lt_one.trans_le hq)
228+
have hp := hpqr.pos
229+
have hq := hpqr.symm.pos
230+
refine norm_le_of_forall_sum_le hpqr.pos' (by positivity) fun s ↦ ?_
231+
simp only [holderₗ_apply_apply_coe]
232+
calc
233+
_ ≤ K ^ r.toReal * (‖e‖ ^ p.toReal) ^ (r.toReal / p.toReal) *
234+
(‖f‖ ^ q.toReal) ^ (r.toReal / q.toReal) :=
235+
Memℓp.holder_gen_bound r hp hq B hBK (by positivity) (by positivity)
236+
(sum_rpow_le_norm_rpow hp e) (sum_rpow_le_norm_rpow hq f) s
237+
_ ≤ _ := by
238+
rw [← Real.rpow_mul, ← Real.rpow_mul]
239+
· simp only [← mul_div_assoc, ne_eq, hp.ne', not_false_eq_true, mul_div_cancel_left₀,
240+
hq.ne', fieldLe]
241+
rw [Real.mul_rpow, Real.mul_rpow]
242+
all_goals positivity
243+
all_goals positivity
244+
245+
lemma norm_holderL_le [Fact (1 ≤ p)] [Fact (1 ≤ q)] [Fact (1 ≤ r)]
246+
(B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i) {K : ℝ≥0} (hBK : ∀ i, ‖B i‖ ≤ K) :
247+
‖holderL (p := p) (q := q) r B hBK‖ ≤ K :=
248+
LinearMap.mkContinuous₂_norm_le _ K.2 _
249+
250+
variable {H : Type*} [NormedAddCommGroup H] [NormedSpace 𝕜 H] [CompleteSpace H]
251+
252+
variable (p q) in
253+
/-- The natural pairing between `lp E p` and `lp F q` (for Hölder conjugate `p q : ℝ≥0∞`) with
254+
values in a space `H` induced by a family of bilinear maps `B : (i : ι) → E i →L[𝕜] F i →L[𝕜] H`.
255+
256+
This is given by `∑' i, B (e i) (f i)`.
257+
258+
In the special case when `B := (NormedSpace.inclusionInDoubleDual 𝕜 E).flip`, which is
259+
definitionally the same as `B := ContinuousLinearMap.id 𝕜 (E →L[𝕜] 𝕜)`, this is the natural map
260+
`lp (fun _ ↦ StrongDual 𝕜 E) p →L[𝕜] StrongDual 𝕜 (lp E q)`.
261+
-/
262+
noncomputable def dualPairing [Fact (1 ≤ p)] [Fact (1 ≤ q)] [p.HolderConjugate q]
263+
(B : (i : ι) → E i →L[𝕜] F i →L[𝕜] H) {K : ℝ≥0} (hBK : ∀ i, ‖B i‖ ≤ K) :
264+
lp E p →L[𝕜] lp F q →L[𝕜] H :=
265+
(tsumCLM 𝕜 ι H |>.postcomp <| lp F q) ∘L (holderL 1 B hBK)
266+
267+
lemma dualPairing_apply [Fact (1 ≤ p)] [Fact (1 ≤ q)] [p.HolderConjugate q]
268+
(B : (i : ι) → E i →L[𝕜] F i →L[𝕜] H) {K : ℝ≥0} (hBK : ∀ i, ‖B i‖ ≤ K)
269+
(e : lp E p) (f : lp F q) :
270+
dualPairing p q B hBK e f = ∑' i, B i (e i) (f i) :=
271+
rfl
272+
273+
lemma norm_dualPairing [Fact (1 ≤ p)] [Fact (1 ≤ q)] [p.HolderConjugate q]
274+
(B : (i : ι) → E i →L[𝕜] F i →L[𝕜] H) {K : ℝ≥0} (hBK : ∀ i, ‖B i‖ ≤ K) :
275+
‖dualPairing p q B hBK‖ ≤ K := calc
276+
‖dualPairing p q B hBK‖
277+
_ ≤ ‖(tsumCLM 𝕜 ι H).postcomp (lp F q)‖ * ‖holderL 1 B hBK‖ :=
278+
ContinuousLinearMap.opNorm_comp_le _ _
279+
_ ≤ 1 * K := by
280+
gcongr
281+
· exact ContinuousLinearMap.norm_postcomp_le _ |>.trans norm_tsumCLM_le
282+
· exact norm_holderL_le 1 B hBK
283+
_ = K := one_mul _
284+
285+
end lp

‎Mathlib/Analysis/Normed/Lp/lpSpace.lean‎

Lines changed: 20 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
/-
22
Copyright (c) 2021 Heather Macbeth. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
4-
Authors: Heather Macbeth
4+
Authors: Heather Macbeth, Jireh Loreaux
55
-/
66
module
77

@@ -133,6 +133,13 @@ theorem memℓp_gen_iff'' {f : (i : α) → E i} (hp : 0 < p.toReal) :
133133
refine ⟨fun hf ↦ ?_, fun ⟨C, _, hC⟩ ↦ memℓp_gen' hC⟩
134134
exact ⟨_, tsum_nonneg fun i ↦ (by positivity), memℓp_gen_iff' hp |>.mp hf⟩
135135

136+
/-- When `α` is `Finite`, every `f : PreLp E p` satisfies `Memℓp f p`. -/
137+
theorem Memℓp.all [Finite α] (f : ∀ i, E i) : Memℓp f p := by
138+
rcases p.trichotomy with (rfl | rfl | _h)
139+
· exact memℓp_zero_iff.mpr { i : α | f i ≠ 0 }.toFinite
140+
· exact memℓp_infty_iff.mpr (Set.Finite.bddAbove (Set.range fun i : α ↦ ‖f i‖).toFinite)
141+
· cases nonempty_fintype α; exact memℓp_gen ⟨Finset.univ.sum _, hasSum_fintype _⟩
142+
136143
theorem zero_memℓp : Memℓp (0 : ∀ i, E i) p := by
137144
rcases p.trichotomy with (rfl | rfl | hp)
138145
· apply memℓp_zero
@@ -338,9 +345,20 @@ def PreLp (E : α → Type*) [∀ i, NormedAddCommGroup (E i)] : Type _ :=
338345
∀ i, E i
339346
deriving AddCommGroup
340347

341-
instance PreLp.unique [IsEmpty α] : Unique (PreLp E) :=
348+
namespace PreLp
349+
350+
@[simp] lemma add_apply {x y : PreLp E} {i : α} : (x + y) i = x i + y i := rfl
351+
@[simp] lemma zero_apply {i : α} : (0 : PreLp E) i = 0 := rfl
352+
@[simp] lemma sub_apply {x y : PreLp E} {i : α} : (x - y) i = x i - y i := rfl
353+
@[simp] lemma neg_apply {x : PreLp E} {i : α} : (-x) i = -(x i) := rfl
354+
@[simp] lemma nsmul_apply {n : ℕ} {x : PreLp E} {i : α} : (n • x) i = n • (x i) := rfl
355+
@[simp] lemma zsmul_apply {n : ℤ} {x : PreLp E} {i : α} : (n • x) i = n • (x i) := rfl
356+
357+
instance unique [IsEmpty α] : Unique (PreLp E) :=
342358
inferInstanceAs <| Unique (∀ _, _)
343359

360+
end PreLp
361+
344362
/-- **The (little) ℓᵖ space**: The additive subgroup of a type synonym of `Π i, E i`, which consists
345363
of those functions `f` such that `Memℓp f p` (i.e., `f` has finite `p`-norm).
346364

‎Mathlib/Analysis/Normed/Operator/Basic.lean‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -484,6 +484,10 @@ lemma norm_pi_le_of_le {ι : Type*} [Fintype ι]
484484
refine (pi_norm_le_iff_of_nonneg (by positivity)).mpr (fun i ↦ ?_)
485485
exact (L i).le_of_opNorm_le (hL i) _
486486

487+
lemma norm_postcomp_le [RingHomIsometric σ₁₂] [RingHomIsometric σ₁₃] [RingHomIsometric σ₂₃]
488+
(L : F →SL[σ₂₃] G) : ‖L.postcomp (σ := σ₁₂) E‖ ≤ ‖L‖ :=
489+
L.postcomp (σ := σ₁₂) E |>.opNorm_le_bound (by positivity) <| opNorm_comp_le L
490+
487491
end ContinuousLinearMap
488492

489493
namespace LinearMap

‎Mathlib/Tactic/Linter/TextBased.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -570,6 +570,7 @@ def modulesNotUpperCamelCase (opts : LinterOptions) (modules : Array Lean.Name)
570570
let exceptions := [
571571
`Mathlib.Analysis.CStarAlgebra.lpSpace,
572572
`Mathlib.Analysis.InnerProductSpace.l2Space,
573+
`Mathlib.Analysis.Normed.Lp.lpHolder,
573574
`Mathlib.Analysis.Normed.Lp.lpSpace
574575
]
575576
-- We allow only names in UpperCamelCase, possibly with a trailing underscore.

0 commit comments

Comments
 (0)