.lake/packages/mathlib/Mathlib/Analysis/Normed/Lp/lpSpace.lean

1/-

3Released under Apache 2.0 license as described in the file LICENSE.

4Authors: Heather Macbeth, Jireh Loreaux

5-/

6module

8public import Mathlib.Analysis.MeanInequalities

9public import Mathlib.Analysis.MeanInequalitiesPow

10public import Mathlib.Analysis.SpecialFunctions.Pow.Continuity

11public import Mathlib.Data.Set.Image

12public import Mathlib.Topology.Algebra.ContinuousMonoidHom

13public import Mathlib.Algebra.Order.Group.Pointwise.Bounds

15/-!

16# ℓp space

18This file describes properties of elements `f` of a pi-type `∀ i, E i` with finite "norm",

19defined for `p : ℝ≥0∞` as the size of the support of `f` if `p=0`, `(∑' a, ‖f a‖^p) ^ (1/p)` for

20`0 < p < ∞` and `⨆ a, ‖f a‖` for `p=∞`.

22The Prop-valued `Memℓp f p` states that a function `f : ∀ i, E i` has finite norm according

23to the above definition; that is, `f` has finite support if `p = 0`, `Summable (fun a ↦ ‖f a‖^p)` if

24`0 < p < ∞`, and `BddAbove (norm '' (Set.range f))` if `p = ∞`.

26The space `lp E p` is the subtype of elements of `∀ i : α, E i` which satisfy `Memℓp f p`. For

27`1 ≤ p`, the "norm" is genuinely a norm and `lp` is a complete metric space.

29## Main definitions

31* `Memℓp f p` : property that the function `f` satisfies, as appropriate, `f` finitely supported

32 if `p = 0`, `Summable (fun a ↦ ‖f a‖^p)` if `0 < p < ∞`, and `BddAbove (norm '' (Set.range f))` if

33 `p = ∞`.

34* `lp E p` : elements of `∀ i : α, E i` such that `Memℓp f p`. Defined as an `AddSubgroup` of

35 a type synonym `PreLp` for `∀ i : α, E i`, and equipped with a `NormedAddCommGroup` structure.

36 Under appropriate conditions, this is also equipped with the instances `lp.normedSpace`,

37 `lp.completeSpace`. For `p=∞`, there is also `lp.inftyNormedRing`,

38 `lp.inftyNormedAlgebra`, `lp.inftyStarRing` and `lp.inftyCStarRing`.

40## Main results

42* `Memℓp.of_exponent_ge`: For `q ≤ p`, a function which is `Memℓp` for `q` is also `Memℓp` for `p`.

43* `lp.memℓp_of_tendsto`, `lp.norm_le_of_tendsto`: A pointwise limit of functions in `lp`, all with

44 `lp` norm `≤ C`, is itself in `lp` and has `lp` norm `≤ C`.

45* `lp.tsum_mul_le_mul_norm`: basic form of Hölder's inequality

47## Implementation

49Since `lp` is defined as an `AddSubgroup`, dot notation does not work. Use `lp.norm_neg f` to

50say that `‖-f‖ = ‖f‖`, instead of the non-working `f.norm_neg`.

52## TODO

54* More versions of Hölder's inequality (for example: the case `p = 1`, `q = ∞`; a version for normed

55 rings which has `‖∑' i, f i * g i‖` rather than `∑' i, ‖f i‖ * g i‖` on the RHS; a version for

56 three exponents satisfying `1 / r = 1 / p + 1 / q`)

58-/

60@[expose] public section

62noncomputable section

64open scoped NNReal ENNReal Function

66variable {𝕜 𝕜' : Type*} {α : Type*} {E : α → Type*} {p q : ℝ≥0∞} [∀ i, NormedAddCommGroup (E i)]

68/-!

69### `Memℓp` predicate

71-/

74/-- The property that `f : ∀ i : α, E i`

75* is finitely supported, if `p = 0`, or

76* admits an upper bound for `Set.range (fun i ↦ ‖f i‖)`, if `p = ∞`, or

77* has the series `∑' i, ‖f i‖ ^ p` be summable, if `0 < p < ∞`. -/

78def Memℓp (f : ∀ i, E i) (p : ℝ≥0∞) : Prop :=

79 if p = 0 then Set.Finite { i | f i ≠ 0 }

80 else if p = ∞ then BddAbove (Set.range fun i => ‖f i‖)

81 else Summable fun i => ‖f i‖ ^ p.toReal

83theorem memℓp_zero_iff {f : ∀ i, E i} : Memℓp f 0 ↔ Set.Finite { i | f i ≠ 0 } := by

84 dsimp [Memℓp]

85 rw [ite_eq_left rfl]

87theorem memℓp_zero {f : ∀ i, E i} (hf : Set.Finite { i | f i ≠ 0 }) : Memℓp f 0 :=

88 memℓp_zero_iff.2 hf

90theorem memℓp_infty_iff {f : ∀ i, E i} : Memℓp f ∞ ↔ BddAbove (Set.range fun i => ‖f i‖) := by

91 simp [Memℓp]

93theorem memℓp_infty {f : ∀ i, E i} (hf : BddAbove (Set.range fun i => ‖f i‖)) : Memℓp f ∞ :=

94 memℓp_infty_iff.2 hf

96theorem memℓp_gen_iff (hp : 0 < p.toReal) {f : ∀ i, E i} :

97 Memℓp f p ↔ Summable fun i => ‖f i‖ ^ p.toReal := by

98 rw [ENNReal.toReal_pos_iff] at hp

99 dsimp [Memℓp]

100 rw [ite_eq_right hp.1.ne', ite_eq_right hp.2.ne]

101

102theorem memℓp_gen {f : ∀ i, E i} (hf : Summable fun i => ‖f i‖ ^ p.toReal) : Memℓp f p := by

103 rcases p.trichotomy with (rfl | rfl | hp)

104 · apply memℓp_zero

105 have H : Summable fun _ : α => (1 : ℝ) := by simpa using hf

106 exact (Set.Finite.of_summable_const (by simp) H).subset (Set.subset_univ _)

107 · apply memℓp_infty

108 have H : Summable fun _ : α => (1 : ℝ) := by simpa using hf

109 simpa using ((Set.Finite.of_summable_const (by simp) H).image fun i => ‖f i‖).bddAbove

110 exact (memℓp_gen_iff hp).2 hf

111

112theorem memℓp_gen' {C : ℝ} {f : ∀ i, E i} (hf : ∀ s : Finset α, ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C) :

113 Memℓp f p := by

114 apply memℓp_gen

115 use ⨆ s : Finset α, ∑ i ∈ s, ‖f i‖ ^ p.toReal

116 apply hasSum_of_isLUB_of_nonneg

117 · intro b

118 positivity

119 apply isLUB_ciSup

120 use C

121 rintro - ⟨s, rfl⟩

122 exact hf s

123

124theorem memℓp_gen_iff' {f : (i : α) → E i} (hp : 0 < p.toReal) :

125 Memℓp f p ↔ ∀ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ ∑' i, ‖f i‖ ^ p.toReal := by

126 refine ⟨fun hf ↦ ?_, memℓp_gen'⟩

127 obtain ⟨hp₁, hp₂⟩ := ENNReal.toReal_pos_iff.mp hp

128 simp only [Memℓp, hp₁.ne', ↓reduceIte, hp₂.ne] at hf

129 simpa [upperBounds] using isLUB_hasSum (by intro; positivity) hf.hasSum |>.1

130

131theorem memℓp_gen_iff'' {f : (i : α) → E i} (hp : 0 < p.toReal) :

132 Memℓp f p ↔ ∃ C, 0 ≤ C ∧ ∀ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C := by

133 refine ⟨fun hf ↦ ?_, fun ⟨C, _, hC⟩ ↦ memℓp_gen' hC⟩

134 exact ⟨_, tsum_nonneg fun i ↦ (by positivity), memℓp_gen_iff' hp |>.mp hf⟩

135

136/-- When `α` is `Finite`, every `f : PreLp E p` satisfies `Memℓp f p`. -/

137theorem 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

143theorem zero_memℓp : Memℓp (0 : ∀ i, E i) p := by

144 rcases p.trichotomy with (rfl | rfl | hp)

145 · apply memℓp_zero

146 simp

147 · apply memℓp_infty

148 simp only [norm_zero, Pi.zero_apply]

149 exact bddAbove_singleton.mono Set.range_const_subset

150 · apply memℓp_gen

151 simp [Real.zero_rpow hp.ne', summable_zero]

152

153theorem zero_mem_ℓp' : Memℓp (fun i : α => (0 : E i)) p :=

154 zero_memℓp

155

156theorem memℓp_norm_iff {f : (i : α) → E i} :

157 Memℓp (‖f ·‖) p ↔ Memℓp f p := by

158 obtain (rfl | rfl | hp) := p.trichotomy

159 · simp [memℓp_zero_iff]

160 · simp [memℓp_infty_iff]

161 · simp [memℓp_gen_iff hp]

162

163alias ⟨Memℓp.of_norm, Memℓp.norm⟩ := memℓp_norm_iff

164namespace Memℓp

165

166theorem mono {f : (i : α) → E i} {g : α → ℝ}

167 (hg : Memℓp g p) (hfg : ∀ i, ‖f i‖ ≤ g i) :

168 Memℓp f p := by

169 replace hfg (i) : ‖f i‖ ≤ ‖g i‖ := (hfg i).trans (Real.le_norm_self _)

170 obtain (rfl | rfl | hp) := p.trichotomy

171 · simp_rw [memℓp_zero_iff, ← norm_pos_iff] at hg ⊢

172 refine hg.subset fun i hi ↦ hi.trans_le <| hfg i

173 · rw [memℓp_infty_iff] at hg ⊢

174 exact hg.range_mono _ hfg

175 · rw [memℓp_gen_iff hp] at hg ⊢

176 apply hg.of_norm_bounded fun i ↦ ?_

177 rw [Real.norm_eq_abs, abs_of_nonneg (by positivity)]

178 gcongr

179 exact hfg i

180

181/-- Often it is more convenient to use `Memℓp.mono`, where the bounding function is real-valued.

182This version is provable from that one using `Memℓp.toNorm` applied to the argument with type

183`Memℓp g p`. -/

184theorem mono' {F : α → Type*} [∀ i, NormedAddCommGroup (F i)] {f : (i : α) → E i}

185 {g : (i : α) → F i} (hg : Memℓp g p) (hfg : ∀ i, ‖f i‖ ≤ ‖g i‖) :

186 Memℓp f p :=

187 hg.norm.mono hfg

188

189theorem finite_dsupport {f : ∀ i, E i} (hf : Memℓp f 0) : Set.Finite { i | f i ≠ 0 } :=

190 memℓp_zero_iff.1 hf

191

192theorem bddAbove {f : ∀ i, E i} (hf : Memℓp f ∞) : BddAbove (Set.range fun i => ‖f i‖) :=

193 memℓp_infty_iff.1 hf

194

195theorem summable (hp : 0 < p.toReal) {f : ∀ i, E i} (hf : Memℓp f p) :

196 Summable fun i => ‖f i‖ ^ p.toReal :=

197 (memℓp_gen_iff hp).1 hf

198

199lemma summable_of_one {E : Type*} [NormedAddCommGroup E] [CompleteSpace E]

200 {x : α → E} (hx : Memℓp x 1) : Summable x :=

201 .of_norm <| by simpa using hx.summable

202

203theorem neg {f : ∀ i, E i} (hf : Memℓp f p) : Memℓp (-f) p := by

204 rcases p.trichotomy with (rfl | rfl | hp)

205 · apply memℓp_zero

206 simp [hf.finite_dsupport]

207 · apply memℓp_infty

208 simpa using hf.bddAbove

209 · apply memℓp_gen

210 simpa using hf.summable hp

211

212@[simp]

213theorem neg_iff {f : ∀ i, E i} : Memℓp (-f) p ↔ Memℓp f p :=

214 ⟨fun h => neg_neg f ▸ h.neg, Memℓp.neg⟩

215

216theorem of_exponent_ge {p q : ℝ≥0∞} {f : ∀ i, E i} (hfq : Memℓp f q) (hpq : q ≤ p) : Memℓp f p := by

217 rcases ENNReal.trichotomy₂ hpq with

218 (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, hp⟩ | ⟨rfl, rfl⟩ | ⟨hq, rfl⟩ | ⟨hq, _, hpq'⟩)

219 · exact hfq

220 · apply memℓp_infty

221 obtain ⟨C, hC⟩ := (hfq.finite_dsupport.image fun i => ‖f i‖).bddAbove

222 use max 0 C

223 rintro x ⟨i, rfl⟩

224 by_cases hi : f i = 0

225 · simp [hi]

226 · exact (hC ⟨i, hi, rfl⟩).trans (le_max_right _ _)

227 · apply memℓp_gen

228 have : ∀ i ∉ hfq.finite_dsupport.toFinset, ‖f i‖ ^ p.toReal = 0 := by

229 intro i hi

230 have : f i = 0 := by simpa using hi

231 simp [this, Real.zero_rpow hp.ne']

232 exact summable_of_ne_finset_zero this

233 · exact hfq

234 · apply memℓp_infty

235 obtain ⟨A, hA⟩ := (hfq.summable hq).tendsto_cofinite_zero.bddAbove_range_of_cofinite

236 use A ^ q.toReal⁻¹

237 rintro x ⟨i, rfl⟩

238 have : 0 ≤ ‖f i‖ ^ q.toReal := by positivity

239 simpa [← Real.rpow_mul, mul_inv_cancel₀ hq.ne'] using

240 Real.rpow_le_rpow this (hA ⟨i, rfl⟩) (inv_nonneg.mpr hq.le)

241 · apply memℓp_gen

242 have hf' := hfq.summable hq

243 refine .of_norm_bounded_eventually hf' (@Set.Finite.subset _ { i | 1 ≤ ‖f i‖ } ?_ _ ?_)

244 · have H : { x : α | 1 ≤ ‖f x‖ ^ q.toReal }.Finite := by

245 simpa using hf'.tendsto_cofinite_zero.eventually_lt_const (by simp)

246 exact H.subset fun i hi => Real.one_le_rpow hi hq.le

247 · change ∀ i, ¬|‖f i‖ ^ p.toReal| ≤ ‖f i‖ ^ q.toReal → 1 ≤ ‖f i‖

248 intro i hi

249 have : 0 ≤ ‖f i‖ ^ p.toReal := by positivity

250 simp only [abs_of_nonneg, this] at hi

251 contrapose! hi

252 exact Real.rpow_le_rpow_of_exponent_ge' (norm_nonneg _) hi.le hq.le hpq'

253

254theorem add {f g : ∀ i, E i} (hf : Memℓp f p) (hg : Memℓp g p) : Memℓp (f + g) p := by

255 rcases p.trichotomy with (rfl | rfl | hp)

256 · apply memℓp_zero

257 refine (hf.finite_dsupport.union hg.finite_dsupport).subset fun i => ?_

258 simp only [Pi.add_apply, Ne, Set.mem_union, Set.mem_ofPred_eq]

259 contrapose!

260 rintro ⟨hf', hg'⟩

261 simp [hf', hg']

262 · apply memℓp_infty

263 obtain ⟨A, hA⟩ := hf.bddAbove

264 obtain ⟨B, hB⟩ := hg.bddAbove

265 refine ⟨A + B, ?_⟩

266 rintro a ⟨i, rfl⟩

267 exact le_trans (norm_add_le _ _) (add_le_add (hA ⟨i, rfl⟩) (hB ⟨i, rfl⟩))

268 apply memℓp_gen

269 let C : ℝ := if p.toReal < 1 then 1 else (2 : ℝ) ^ (p.toReal - 1)

270 refine .of_nonneg_of_le ?_ (fun i => ?_) (((hf.summable hp).add (hg.summable hp)).mul_left C)

271 · intro; positivity

272 · refine (Real.rpow_le_rpow (norm_nonneg _) (norm_add_le _ _) hp.le).trans ?_

273 dsimp only [C]

274 split_ifs with h

275 · simpa using! NNReal.coe_le_coe.2 (NNReal.rpow_add_le_add_rpow ‖f i‖₊ ‖g i‖₊ hp.le h.le)

276 · let F : Fin 2 → ℝ≥0 := ![‖f i‖₊, ‖g i‖₊]

277 simp only [not_lt] at h

278 simpa [Fin.sum_univ_succ] using!

279 Real.rpow_sum_le_const_mul_sum_rpow_of_nonneg Finset.univ h fun i _ => (F i).coe_nonneg

280

281theorem sub {f g : ∀ i, E i} (hf : Memℓp f p) (hg : Memℓp g p) : Memℓp (f - g) p := by

282 rw [sub_eq_add_neg]; exact hf.add hg.neg

283

284theorem finsetSum {ι} (s : Finset ι) {f : ι → ∀ i, E i} (hf : ∀ i ∈ s, Memℓp (f i) p) :

285 Memℓp (fun a => ∑ i ∈ s, f i a) p := by

286 have : DecidableEq ι := Classical.decEq _

287 revert hf

288 refine Finset.induction_on s ?_ ?_

289 · simp only [zero_mem_ℓp', Finset.sum_empty, imp_true_iff]

290 · intro i s his ih hf

291 simp only [his, Finset.sum_insert, not_false_iff]

292 exact (hf i (s.mem_insert_self i)).add (ih fun j hj => hf j (Finset.mem_insert_of_mem hj))

293

294@[deprecated (since := "2026-04-08")] alias finset_sum := finsetSum

295

296section IsBoundedSMul

297

298variable [NormedRing 𝕜] [∀ i, Module 𝕜 (E i)] [∀ i, IsBoundedSMul 𝕜 (E i)]

299

300theorem const_smul {f : ∀ i, E i} (hf : Memℓp f p) (c : 𝕜) : Memℓp (c • f) p := by

301 rcases p.trichotomy with (rfl | rfl | hp)

302 · apply memℓp_zero

303 refine hf.finite_dsupport.subset fun i => (?_ : ¬c • f i = 0 → ¬f i = 0)

304 exact not_imp_not.mpr fun hf' => hf'.symm ▸ smul_zero c

305 · obtain ⟨A, hA⟩ := hf.bddAbove

306 refine memℓp_infty ⟨‖c‖ * A, ?_⟩

307 rintro a ⟨i, rfl⟩

308 dsimp only [Pi.smul_apply]

309 refine (norm_smul_le _ _).trans ?_

310 gcongr

311 exact hA ⟨i, rfl⟩

312 · apply memℓp_gen

313 dsimp only [Pi.smul_apply]

314 have := (hf.summable hp).mul_left (↑(‖c‖₊ ^ p.toReal) : ℝ)

315 simp_rw [← coe_nnnorm, ← NNReal.coe_rpow, ← NNReal.coe_mul, NNReal.summable_coe,

316 ← NNReal.mul_rpow] at this ⊢

317 refine NNReal.summable_of_le ?_ this

318 intro i

319 gcongr

320 apply nnnorm_smul_le

321

322theorem const_mul {f : α → 𝕜} (hf : Memℓp f p) (c : 𝕜) : Memℓp (fun x => c * f x) p :=

323 hf.const_smul c

324

325end IsBoundedSMul

326

327end Memℓp

328

329/-!

330### lp space

331

332The space of elements of `∀ i, E i` satisfying the predicate `Memℓp`.

333-/

334

335

336/-- We define `PreLp E` to be a type synonym for `∀ i, E i` which, importantly, does not inherit

337the `pi` topology on `∀ i, E i` (otherwise this topology would descend to `lp E p` and conflict

338with the normed group topology we will later equip it with.)

339

340We choose to deal with this issue by making a type synonym for `∀ i, E i` rather than for the `lp`

341subgroup itself, because this allows all the spaces `lp E p` (for varying `p`) to be subgroups of

342the same ambient group, which permits lemma statements like `lp.monotone` (below). -/

343@[nolint unusedArguments]

344def PreLp (E : α → Type*) [∀ i, NormedAddCommGroup (E i)] : Type _ :=

345 ∀ i, E i

346

347namespace PreLp

348

349-- The `SMul` instance exists to avoid a zsmul diamond.

350variable [NormedRing 𝕜] [∀ i, Module 𝕜 (E i)] in

351deriving instance SMul 𝕜, AddCommMonoid, AddCommGroup for PreLp E

352

353@[simp] lemma add_apply {x y : PreLp E} {i : α} : (x + y) i = x i + y i := rfl

354@[simp] lemma zero_apply {i : α} : (0 : PreLp E) i = 0 := rfl

355@[simp] lemma sub_apply {x y : PreLp E} {i : α} : (x - y) i = x i - y i := rfl

356@[simp] lemma neg_apply {x : PreLp E} {i : α} : (-x) i = -(x i) := rfl

357@[simp] lemma nsmul_apply {n : ℕ} {x : PreLp E} {i : α} : (n • x) i = n • (x i) := rfl

358@[simp] lemma zsmul_apply {n : ℤ} {x : PreLp E} {i : α} : (n • x) i = n • (x i) := rfl

359

360instance unique [IsEmpty α] : Unique (PreLp E) :=

361 inferInstanceAs <| Unique (∀ _, _)

362

363end PreLp

364

365/-- **The (little) ℓᵖ space**: The additive subgroup of a type synonym of `Π i, E i`, which consists

366of those functions `f` such that `Memℓp f p` (i.e., `f` has finite `p`-norm).

367

368The non-dependent version comes equipped with the notation `ℓ^p(ι, E)` in the `lp` namespace. When

369`p` takes the values `0`, `1` or `2`, the notation `ℓ⁰(ι, E)`, `ℓ¹(ι, E)`, `ℓ²(ι, E)` is also

370available. -/

371def lp (E : α → Type*) [∀ i, NormedAddCommGroup (E i)] (p : ℝ≥0∞) : AddSubgroup (PreLp E) where

372 carrier := { f | Memℓp f p }

373 zero_mem' := zero_memℓp

374 add_mem' := Memℓp.add

375 neg_mem' := Memℓp.neg

376

377@[inherit_doc] scoped[lp] notation "ℓ^" p "(" ι ", " E ")" => lp (fun _ : ι ↦ E) p

378/-- `ℓ⁰(ι, E)` is the space of finitely supported functions `ι → E`. In general, this should not

379be used outside of the context of `ℓ^p(ι, E)` spaces, and one should instead prefer `Finsupp`

380in other situations. -/

381scoped[lp] notation "ℓ⁰(" ι ", " E ")" => lp (fun _ : ι ↦ E) 0

382/-- `ℓ¹(ι, E)` is the space of summable functions `ι → E`. To be more precise, it is the space

383of functions whose *norms* are summable, but when `E` is complete these coincide. -/

384scoped[lp] notation "ℓ¹(" ι ", " E ")" => lp (fun _ : ι ↦ E) 1

385/-- `ℓ²(ι, E)` is the space of square-summable functions `ι → E`. When `E := 𝕜`, with `RCLike 𝕜`,

386this is a Hilbert space. -/

387scoped[lp] notation "ℓ²(" ι ", " E ")" => lp (fun _ : ι ↦ E) 2

388

389namespace lp

390

391-- TODO: this instance is bad because it inserts `Subtype.val` as the casting function,

392-- which abuses definitional equality.

393instance coeFun : CoeFun (lp E p) fun _ => ∀ i, E i :=

394 ⟨Subtype.val (α := ∀ i, E i)⟩

395

396@[ext]

397theorem ext {f g : lp E p} (h : (f : ∀ i, E i) = g) : f = g :=

398 Subtype.ext h

399

400theorem eq_zero' [IsEmpty α] (f : lp E p) : f = 0 :=

401 Subsingleton.elim f 0

402

403protected theorem monotone {p q : ℝ≥0∞} (hpq : q ≤ p) : lp E q ≤ lp E p :=

404 fun _ hf => Memℓp.of_exponent_ge hf hpq

405

406protected theorem memℓp (f : lp E p) : Memℓp f p :=

407 f.prop

408

409variable (E p)

410

411@[simp]

412theorem coeFn_zero : ⇑(0 : lp E p) = 0 :=

413 rfl

414

415variable {E p}

416

417@[simp]

418theorem coeFn_neg (f : lp E p) : ⇑(-f) = -f :=

419 rfl

420

421@[simp]

422theorem coeFn_add (f g : lp E p) : ⇑(f + g) = f + g :=

423 rfl

424

425variable (p E) in

426/-- Coercion to function as an `AddMonoidHom`. -/

427def coeFnAddMonoidHom : lp E p →+ (∀ i, E i) where

428 toFun := (⇑)

429 __ := AddSubgroup.subtype _

430

431@[simp]

432theorem coeFnAddMonoidHom_apply (x : lp E p) : coeFnAddMonoidHom E p x = ⇑x := rfl

433

434theorem coeFn_sum {ι : Type*} (f : ι → lp E p) (s : Finset ι) :

435 ⇑(∑ i ∈ s, f i) = ∑ i ∈ s, ⇑(f i) :=

436 (lp E p).val_finsetSum f s

437

438@[simp]

439theorem coeFn_sub (f g : lp E p) : ⇑(f - g) = f - g :=

440 rfl

441

442instance : Norm (lp E p) where

443 norm f :=

444 if hp : p = 0 then by

445 subst hp

446 exact ((lp.memℓp f).finite_dsupport.toFinset.card : ℝ)

447 else if p = ∞ then ⨆ i, ‖f i‖ else (∑' i, ‖f i‖ ^ p.toReal) ^ (1 / p.toReal)

448

449theorem norm_eq_card_dsupport (f : lp E 0) : ‖f‖ = (lp.memℓp f).finite_dsupport.toFinset.card :=

450 dite_eq_left rfl

451

452theorem norm_eq_ciSup (f : lp E ∞) : ‖f‖ = ⨆ i, ‖f i‖ := rfl

453

454theorem isLUB_norm [Nonempty α] (f : lp E ∞) : IsLUB (Set.range fun i => ‖f i‖) ‖f‖ := by

455 rw [lp.norm_eq_ciSup]

456 exact isLUB_ciSup (lp.memℓp f)

457

458theorem norm_eq_tsum_rpow (hp : 0 < p.toReal) (f : lp E p) :

459 ‖f‖ = (∑' i, ‖f i‖ ^ p.toReal) ^ (1 / p.toReal) := by

460 dsimp [norm]

461 rw [ENNReal.toReal_pos_iff] at hp

462 rw [dite_eq_right hp.1.ne', ite_eq_right hp.2.ne]

463

464theorem norm_rpow_eq_tsum (hp : 0 < p.toReal) (f : lp E p) :

465 ‖f‖ ^ p.toReal = ∑' i, ‖f i‖ ^ p.toReal := by

466 rw [norm_eq_tsum_rpow hp, ← Real.rpow_mul]

467 · field_simp

468 simp

469 positivity

470

471theorem hasSum_norm (hp : 0 < p.toReal) (f : lp E p) :

472 HasSum (fun i => ‖f i‖ ^ p.toReal) (‖f‖ ^ p.toReal) := by

473 rw [norm_rpow_eq_tsum hp]

474 exact ((lp.memℓp f).summable hp).hasSum

475

476/-- The sequence of norms of `x : lp E p` as a term of `ℓ^p(α, ℝ)`. Here `E : α → Type*`

477is a dependent type and `ℓ^p(α, ℝ)` is the non-dependent `ℝ`-valued `lp` space. -/

478@[simps]

479def toNorm {p : ℝ≥0∞} (x : lp E p) : ℓ^p(α, ℝ) :=

480 ⟨fun i ↦ ‖x i‖, lp.memℓp x |>.norm⟩

481

482lemma norm_toNorm {p : ℝ≥0∞} {x : lp E p} :

483 ‖toNorm x‖ = ‖x‖ := by

484 obtain (rfl | rfl | hp) := p.trichotomy

485 · simp [norm_eq_card_dsupport]

486 · simp [norm_eq_ciSup]

487 · simp [norm_eq_tsum_rpow hp]

488

489theorem norm_nonneg' (f : lp E p) : 0 ≤ ‖f‖ := by

490 rcases p.trichotomy with (rfl | rfl | hp)

491 · simp [lp.norm_eq_card_dsupport f]

492 · rcases isEmpty_or_nonempty α with _i | _i

493 · simp [lp.norm_eq_ciSup]

494 inhabit α

495 exact (norm_nonneg (f default)).trans ((lp.isLUB_norm f).1 ⟨default, rfl⟩)

496 · rw [lp.norm_eq_tsum_rpow hp f]

497 exact Real.rpow_nonneg (tsum_nonneg fun i ↦ by positivity) _

498

499@[simp]

500theorem norm_zero : ‖(0 : lp E p)‖ = 0 := by

501 rcases p.trichotomy with (rfl | rfl | hp)

502 · simp [lp.norm_eq_card_dsupport]

503 · simp [lp.norm_eq_ciSup]

504 · rw [lp.norm_eq_tsum_rpow hp]

505 have hp' : 1 / p.toReal ≠ 0 := one_div_ne_zero hp.ne'

506 simpa [Real.zero_rpow hp.ne'] using Real.zero_rpow hp'

507

508theorem norm_eq_zero_iff {f : lp E p} : ‖f‖ = 0 ↔ f = 0 := by

509 refine ⟨fun h => ?_, by rintro rfl; exact norm_zero⟩

510 rcases p.trichotomy with (rfl | rfl | hp)

511 · ext i

512 have : { i : α | ¬f i = 0 } = ∅ := by simpa [lp.norm_eq_card_dsupport f] using! h

513 have : ¬¬f i = 0 := Set.eq_empty_iff_forall_notMem.mp this i

514 tauto

515 · rcases isEmpty_or_nonempty α with _i | _i

516 · simp [eq_iff_true_of_subsingleton]

517 have H : IsLUB (Set.range fun i => ‖f i‖) 0 := by simpa [h] using! lp.isLUB_norm f

518 ext i

519 have : ‖f i‖ = 0 := le_antisymm (H.1 ⟨i, rfl⟩) (norm_nonneg _)

520 simpa using! this

521 · have hf : HasSum (fun i : α => ‖f i‖ ^ p.toReal) 0 := by

522 have := lp.hasSum_norm hp f

523 rwa [h, Real.zero_rpow hp.ne'] at this

524 have : ∀ i, 0 ≤ ‖f i‖ ^ p.toReal := fun i ↦ by positivity

525 rw [hasSum_zero_iff_of_nonneg this] at hf

526 ext i

527 have : f i = 0 ∧ p.toReal ≠ 0 := by

528 simpa [Real.rpow_eq_zero_iff_of_nonneg (norm_nonneg (f i))] using! congr_fun hf i

529 exact this.1

530

531theorem eq_zero_iff_coeFn_eq_zero {f : lp E p} : f = 0 ↔ ⇑f = 0 := by

532 rw [lp.ext_iff, coeFn_zero]

533

534@[simp]

535theorem norm_neg ⦃f : lp E p⦄ : ‖-f‖ = ‖f‖ := by

536 rcases p.trichotomy with (rfl | rfl | hp)

537 · simp only [norm_eq_card_dsupport, coeFn_neg, Pi.neg_apply, ne_eq, neg_eq_zero]

538 · cases isEmpty_or_nonempty α

539 · simp only [lp.eq_zero' f, neg_zero, norm_zero]

540 apply (lp.isLUB_norm (-f)).unique

541 simpa only [coeFn_neg, Pi.neg_apply, norm_neg] using lp.isLUB_norm f

542 · suffices ‖-f‖ ^ p.toReal = ‖f‖ ^ p.toReal by

543 exact Real.rpow_left_injOn hp.ne' (norm_nonneg' _) (norm_nonneg' _) this

544 apply (lp.hasSum_norm hp (-f)).unique

545 simpa only [coeFn_neg, Pi.neg_apply, _root_.norm_neg] using lp.hasSum_norm hp f

546

547instance normedAddCommGroup [hp : Fact (1 ≤ p)] : NormedAddCommGroup (lp E p) :=

548 fast_instance% AddGroupNorm.toNormedAddCommGroup

549 { toFun := norm

550 map_zero' := norm_zero

551 neg' := norm_neg

552 add_le' := fun f g => by

553 rcases p.dichotomy with (rfl | hp')

554 · cases isEmpty_or_nonempty α

555 · simp only [lp.eq_zero' f, zero_add, norm_zero, le_refl]

556 refine (lp.isLUB_norm (f + g)).2 ?_

557 rintro x ⟨i, rfl⟩

558 refine le_trans ?_ (add_mem_upperBounds_add

559 (lp.isLUB_norm f).1 (lp.isLUB_norm g).1 ⟨_, ⟨i, rfl⟩, _, ⟨i, rfl⟩, rfl⟩)

560 exact norm_add_le (f i) (g i)

561 · have hp'' : 0 < p.toReal := zero_lt_one.trans_le hp'

562 have hf₁ : ∀ i, 0 ≤ ‖f i‖ := fun i => norm_nonneg _

563 have hg₁ : ∀ i, 0 ≤ ‖g i‖ := fun i => norm_nonneg _

564 have hf₂ := lp.hasSum_norm hp'' f

565 have hg₂ := lp.hasSum_norm hp'' g

566 -- apply Minkowski's inequality

567 obtain ⟨C, hC₁, hC₂, hCfg⟩ :=

568 Real.Lp_add_le_hasSum_of_nonneg hp' hf₁ hg₁ (norm_nonneg' _) (norm_nonneg' _) hf₂ hg₂

569 refine le_trans ?_ hC₂

570 rw [← Real.rpow_le_rpow_iff (norm_nonneg' (f + g)) hC₁ hp'']

571 refine hasSum_le ?_ (lp.hasSum_norm hp'' (f + g)) hCfg

572 intro i

573 gcongr

574 apply norm_add_le

575 eq_zero_of_map_eq_zero' := fun _ => norm_eq_zero_iff.1 }

576

577-- TODO: define an `ENNReal` version of `HolderConjugate`, and then express this inequality

578-- in a better version which also covers the case `p = 1, q = ∞`.

579/-- Hölder inequality -/

580protected theorem tsum_mul_le_mul_norm {p q : ℝ≥0∞} (hpq : p.toReal.HolderConjugate q.toReal)

581 (f : lp E p) (g : lp E q) :

582 (Summable fun i => ‖f i‖ * ‖g i‖) ∧ ∑' i, ‖f i‖ * ‖g i‖ ≤ ‖f‖ * ‖g‖ := by

583 have hf₁ : ∀ i, 0 ≤ ‖f i‖ := fun i => norm_nonneg _

584 have hg₁ : ∀ i, 0 ≤ ‖g i‖ := fun i => norm_nonneg _

585 have hf₂ := lp.hasSum_norm hpq.pos f

586 have hg₂ := lp.hasSum_norm hpq.symm.pos g

587 obtain ⟨C, -, hC', hC⟩ :=

588 Real.inner_le_Lp_mul_Lq_hasSum_of_nonneg hpq (norm_nonneg' _) (norm_nonneg' _) hf₁ hg₁ hf₂ hg₂

589 rw [← hC.tsum_eq] at hC'

590 exact ⟨hC.summable, hC'⟩

591

592protected theorem summable_mul {p q : ℝ≥0∞} (hpq : p.toReal.HolderConjugate q.toReal)

593 (f : lp E p) (g : lp E q) : Summable fun i => ‖f i‖ * ‖g i‖ :=

594 (lp.tsum_mul_le_mul_norm hpq f g).1

595

596protected theorem tsum_mul_le_mul_norm' {p q : ℝ≥0∞} (hpq : p.toReal.HolderConjugate q.toReal)

597 (f : lp E p) (g : lp E q) : ∑' i, ‖f i‖ * ‖g i‖ ≤ ‖f‖ * ‖g‖ :=

598 (lp.tsum_mul_le_mul_norm hpq f g).2

599

600section ComparePointwise

601

602theorem norm_apply_le_norm (hp : p ≠ 0) (f : lp E p) (i : α) : ‖f i‖ ≤ ‖f‖ := by

603 rcases eq_or_ne p ∞ with (rfl | hp')

604 · have : Nonempty α := ⟨i⟩

605 exact (isLUB_norm f).1 ⟨i, rfl⟩

606 have hp'' : 0 < p.toReal := ENNReal.toReal_pos hp hp'

607 have : ∀ i, 0 ≤ ‖f i‖ ^ p.toReal := fun i ↦ by positivity

608 rw [← Real.rpow_le_rpow_iff (norm_nonneg _) (norm_nonneg' _) hp'']

609 convert! le_hasSum (hasSum_norm hp'' f) i fun i _ => this i

610

611lemma lipschitzWith_one_eval (p : ℝ≥0∞) [Fact (1 ≤ p)] (i : α) :

612 LipschitzWith 1 (fun x : lp E p ↦ x i) :=

613 .mk_one fun _ _ ↦ by

614 simp_rw [dist_eq_norm, ← Pi.sub_apply, ← lp.coeFn_sub]

615 exact norm_apply_le_norm (zero_lt_one.trans_le Fact.out).ne' ..

616

617theorem sum_rpow_le_norm_rpow (hp : 0 < p.toReal) (f : lp E p) (s : Finset α) :

618 ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ ‖f‖ ^ p.toReal := by

619 rw [lp.norm_rpow_eq_tsum hp f]

620 have : ∀ i, 0 ≤ ‖f i‖ ^ p.toReal := fun i ↦ by positivity

621 refine Summable.sum_le_tsum _ (fun i _ => this i) ?_

622 exact (lp.memℓp f).summable hp

623

624theorem norm_le_of_forall_le' [Nonempty α] {f : lp E ∞} (C : ℝ) (hCf : ∀ i, ‖f i‖ ≤ C) :

625 ‖f‖ ≤ C := by

626 refine (isLUB_norm f).2 ?_

627 rintro - ⟨i, rfl⟩

628 exact hCf i

629

630theorem norm_le_of_forall_le {f : lp E ∞} {C : ℝ} (hC : 0 ≤ C) (hCf : ∀ i, ‖f i‖ ≤ C) :

631 ‖f‖ ≤ C := by

632 cases isEmpty_or_nonempty α

633 · simpa [eq_zero' f] using hC

634 · exact norm_le_of_forall_le' C hCf

635

636theorem norm_le_of_tsum_le (hp : 0 < p.toReal) {C : ℝ} (hC : 0 ≤ C) {f : lp E p}

637 (hf : ∑' i, ‖f i‖ ^ p.toReal ≤ C ^ p.toReal) : ‖f‖ ≤ C := by

638 rw [← Real.rpow_le_rpow_iff (norm_nonneg' _) hC hp, norm_rpow_eq_tsum hp]

639 exact hf

640

641theorem norm_le_of_forall_sum_le (hp : 0 < p.toReal) {C : ℝ} (hC : 0 ≤ C) {f : lp E p}

642 (hf : ∀ s : Finset α, ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C ^ p.toReal) : ‖f‖ ≤ C :=

643 norm_le_of_tsum_le hp hC (((lp.memℓp f).summable hp).tsum_le_of_sum_le hf)

644

645lemma norm_mono {F : α → Type*} [∀ i, NormedAddCommGroup (F i)]

646 {p : ℝ≥0∞} (hp : p ≠ 0) {x : lp E p} {y : lp F p} (h : ∀ i, ‖x i‖ ≤ ‖y i‖) :

647 ‖x‖ ≤ ‖y‖ := by

648 obtain (rfl | rfl | hp) := p.trichotomy

649 · exact hp rfl |>.elim

650 · exact norm_le_of_forall_le (by positivity) fun i ↦ (h i).trans <| norm_apply_le_norm hp y i

651 · exact norm_le_of_forall_sum_le hp (norm_nonneg' _) fun s ↦ calc

652 ∑ i ∈ s, ‖x i‖ ^ p.toReal

653 _ ≤ ∑ i ∈ s, ‖y i‖ ^ p.toReal := by gcongr with i _; exact h i

654 _ ≤ ‖y‖ ^ p.toReal := sum_rpow_le_norm_rpow hp y s

655

656end ComparePointwise

657

658section IsBoundedSMul

659

660variable [NormedRing 𝕜] [NormedRing 𝕜']

661variable [∀ i, Module 𝕜 (E i)] [∀ i, Module 𝕜' (E i)]

662

663instance : Module 𝕜 (PreLp E) :=

664 inferInstanceAs <| Module 𝕜 (∀ i, E i)

665

666instance [∀ i, SMulCommClass 𝕜' 𝕜 (E i)] : SMulCommClass 𝕜' 𝕜 (PreLp E) :=

667 inferInstanceAs <| SMulCommClass 𝕜' 𝕜 (∀ i, E i)

668

669instance [SMul 𝕜' 𝕜] [∀ i, IsScalarTower 𝕜' 𝕜 (E i)] : IsScalarTower 𝕜' 𝕜 (PreLp E) :=

670 inferInstanceAs <| IsScalarTower 𝕜' 𝕜 (∀ i, E i)

671

672instance [∀ i, Module 𝕜ᵐᵒᵖ (E i)] [∀ i, IsCentralScalar 𝕜 (E i)] : IsCentralScalar 𝕜 (PreLp E) :=

673 inferInstanceAs <| IsCentralScalar 𝕜 (∀ i, E i)

674

675variable [∀ i, IsBoundedSMul 𝕜 (E i)] [∀ i, IsBoundedSMul 𝕜' (E i)]

676

677theorem mem_lp_const_smul (c : 𝕜) (f : lp E p) : c • (f : PreLp E) ∈ lp E p :=

678 (lp.memℓp f).const_smul c

679

680variable (𝕜 E p)

681

682/-- The `𝕜`-submodule of elements of `∀ i : α, E i` whose `lp` norm is finite. This is `lp E p`,

683with extra structure. -/

684def _root_.lpSubmodule : Submodule 𝕜 (PreLp E) :=

685 { lp E p with smul_mem' := fun c f hf => by simpa using mem_lp_const_smul c ⟨f, hf⟩ }

686

687variable {𝕜 E p}

688

689theorem coe_lpSubmodule : (lpSubmodule 𝕜 E p).toAddSubgroup = lp E p :=

690 rfl

691

692instance : Module 𝕜 (lp E p) :=

693 inferInstanceAs <| Module 𝕜 (lpSubmodule 𝕜 E p)

694

695@[simp]

696theorem coeFn_smul (c : 𝕜) (f : lp E p) : ⇑(c • f) = c • ⇑f :=

697 rfl

698

699instance [∀ i, SMulCommClass 𝕜' 𝕜 (E i)] : SMulCommClass 𝕜' 𝕜 (lp E p) :=

700 ⟨fun _ _ _ => Subtype.ext <| smul_comm _ _ _⟩

701

702instance [SMul 𝕜' 𝕜] [∀ i, IsScalarTower 𝕜' 𝕜 (E i)] : IsScalarTower 𝕜' 𝕜 (lp E p) :=

703 ⟨fun _ _ _ => Subtype.ext <| smul_assoc _ _ _⟩

704

705instance [∀ i, Module 𝕜ᵐᵒᵖ (E i)] [∀ i, IsCentralScalar 𝕜 (E i)] : IsCentralScalar 𝕜 (lp E p) :=

706 ⟨fun _ _ => Subtype.ext <| op_smul_eq_smul _ _⟩

707

708theorem norm_const_smul_le (hp : p ≠ 0) (c : 𝕜) (f : lp E p) : ‖c • f‖ ≤ ‖c‖ * ‖f‖ := by

709 rcases p.trichotomy with (rfl | rfl | hp)

710 · exact absurd rfl hp

711 · cases isEmpty_or_nonempty α

712 · simp [lp.eq_zero' f]

713 have hfc := (lp.isLUB_norm f).mul_left (norm_nonneg c)

714 simp_rw [← Set.range_comp, Function.comp_def] at hfc

715 exact norm_le_of_forall_le (by positivity)

716 fun i ↦ norm_smul_le c (f i) |>.trans <| hfc.1 ⟨i, rfl⟩

717 · let inst : NNNorm (lp E p) := ⟨fun f => ⟨‖f‖, norm_nonneg' _⟩⟩

718 have coe_nnnorm : ∀ f : lp E p, ↑‖f‖₊ = ‖f‖ := fun _ => rfl

719 suffices ‖c • f‖₊ ^ p.toReal ≤ (‖c‖₊ * ‖f‖₊) ^ p.toReal by

720 rwa [NNReal.rpow_le_rpow_iff hp] at this

721 clear_value inst

722 rw [NNReal.mul_rpow]

723 have hLHS := lp.hasSum_norm hp (c • f)

724 have hRHS := (lp.hasSum_norm hp f).mul_left (‖c‖ ^ p.toReal)

725 simp_rw [← coe_nnnorm, ← _root_.coe_nnnorm, ← NNReal.coe_rpow, ← NNReal.coe_mul,

726 NNReal.hasSum_coe] at hRHS hLHS

727 refine hasSum_mono hLHS hRHS fun i => ?_

728 dsimp only

729 rw [← NNReal.mul_rpow, lp.coeFn_smul, Pi.smul_apply]

730 gcongr

731 apply nnnorm_smul_le

732

733instance [Fact (1 ≤ p)] : IsBoundedSMul 𝕜 (lp E p) :=

734 IsBoundedSMul.of_norm_smul_le <| norm_const_smul_le (zero_lt_one.trans_le <| Fact.out).ne'

735

736end IsBoundedSMul

737

738section Sum

739

740variable {E : Type*} [NormedAddCommGroup E]

741

742set_option backward.isDefEq.respectTransparency false in

743lemma norm_tsum_le (f : ℓ¹(α, E)) :

744 ‖∑' i, f i‖ ≤ ‖f‖ := calc

745 ‖∑' i, f i‖ ≤ ∑' i, ‖f i‖ := norm_tsum_le_tsum_norm (.of_norm (by simpa using f.2.summable))

746 _ = ‖f‖ := by simp [norm_eq_tsum_rpow]

747

748variable [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [CompleteSpace E]

749

750variable (α 𝕜 E) in

751/-- Summation (i.e., `tsum`) in `ℓ¹(α, E)` as a continuous linear map. -/

752@[simps!]

753noncomputable def tsumCLM : ℓ¹(α, E) →L[𝕜] E :=

754 LinearMap.mkContinuous

755 { toFun f := ∑' i, f i

756 map_add' f g := by

757 rw [← Summable.tsum_add]

758 exacts [rfl, .of_norm (by simpa using f.2.summable), .of_norm (by simpa using g.2.summable)]

759 map_smul' c f := by

760 simp only [coeFn_smul]

761 exact Summable.tsum_const_smul _ (.of_norm (by simpa using f.2.summable)) }

762 1 (fun f ↦ by simpa using norm_tsum_le f)

763

764end Sum

765

766section DivisionRing

767

768variable [NormedDivisionRing 𝕜] [∀ i, Module 𝕜 (E i)] [∀ i, IsBoundedSMul 𝕜 (E i)]

769

770theorem norm_const_smul (hp : p ≠ 0) {c : 𝕜} (f : lp E p) : ‖c • f‖ = ‖c‖ * ‖f‖ := by

771 obtain rfl | hc := eq_or_ne c 0

772 · simp

773 refine le_antisymm (norm_const_smul_le hp c f) ?_

774 have := mul_le_mul_of_nonneg_left (norm_const_smul_le hp c⁻¹ (c • f)) (norm_nonneg c)

775 rwa [inv_smul_smul₀ hc, norm_inv, mul_inv_cancel_left₀ (norm_ne_zero_iff.mpr hc)] at this

776

777end DivisionRing

778

779section NormedSpace

780

781variable [NormedField 𝕜] [∀ i, NormedSpace 𝕜 (E i)]

782

783instance instNormedSpace [Fact (1 ≤ p)] : NormedSpace 𝕜 (lp E p) where

784 norm_smul_le c f := norm_smul_le c f

785

786end NormedSpace

787

788section NormedStarGroup

789

790variable [∀ i, StarAddMonoid (E i)] [∀ i, NormedStarGroup (E i)]

791

792theorem _root_.Memℓp.star_mem {f : ∀ i, E i} (hf : Memℓp f p) : Memℓp (star f) p := by

793 rcases p.trichotomy with (rfl | rfl | hp)

794 · apply memℓp_zero

795 simp [hf.finite_dsupport]

796 · apply memℓp_infty

797 simpa using hf.bddAbove

798 · apply memℓp_gen

799 simpa using hf.summable hp

800

801@[simp]

802theorem _root_.Memℓp.star_iff {f : ∀ i, E i} : Memℓp (star f) p ↔ Memℓp f p :=

803 ⟨fun h => star_star f ▸ Memℓp.star_mem h, Memℓp.star_mem⟩

804

805instance : Star (lp E p) where

806 star f := ⟨(star f : ∀ i, E i), f.property.star_mem⟩

807

808@[simp]

809theorem coeFn_star (f : lp E p) : ⇑(star f) = star (⇑f) :=

810 rfl

811

812@[simp]

813protected theorem star_apply (f : lp E p) (i : α) : star f i = star (f i) :=

814 rfl

815

816instance instInvolutiveStar : InvolutiveStar (lp E p) where

817 star_involutive x := by simp [star]

818

819instance instStarAddMonoid : StarAddMonoid (lp E p) where

820 star_add _f _g := ext <| star_add (R := ∀ i, E i) _ _

821

822instance [hp : Fact (1 ≤ p)] : NormedStarGroup (lp E p) where

823 norm_star_le f := le_of_eq <| by

824 rcases p.trichotomy with (rfl | rfl | h)

825 · exfalso

826 have := ENNReal.toReal_mono ENNReal.zero_ne_top hp.elim

827 norm_num at this

828 · simp only [lp.norm_eq_ciSup, lp.star_apply, norm_star]

829 · simp only [lp.norm_eq_tsum_rpow h, lp.star_apply, norm_star]

830

831variable [Star 𝕜] [NormedRing 𝕜]

832variable [∀ i, Module 𝕜 (E i)] [∀ i, IsBoundedSMul 𝕜 (E i)] [∀ i, StarModule 𝕜 (E i)]

833

834instance : StarModule 𝕜 (lp E p) where

835 star_smul _r _f := ext <| star_smul (R := 𝕜) (A := ∀ i, E i) _ _

836

837end NormedStarGroup

838

839section NonUnitalNormedRing

840

841variable {I : Type*} {B : I → Type*} [∀ i, NonUnitalNormedRing (B i)]

842

843theorem _root_.Memℓp.infty_mul {f g : ∀ i, B i} (hf : Memℓp f ∞) (hg : Memℓp g ∞) :

844 Memℓp (f * g) ∞ := by

845 rw [memℓp_infty_iff]

846 obtain ⟨⟨Cf, hCf⟩, ⟨Cg, hCg⟩⟩ := hf.bddAbove, hg.bddAbove

847 refine ⟨Cf * Cg, ?_⟩

848 rintro _ ⟨i, rfl⟩

849 calc

850 ‖(f * g) i‖ ≤ ‖f i‖ * ‖g i‖ := norm_mul_le (f i) (g i)

851 _ ≤ Cf * Cg :=

852 mul_le_mul (hCf ⟨i, rfl⟩) (hCg ⟨i, rfl⟩) (norm_nonneg _)

853 ((norm_nonneg _).trans (hCf ⟨i, rfl⟩))

854

855instance : Mul (lp B ∞) where

856 mul f g := ⟨HMul.hMul (α := ∀ i, B i) _ _, f.property.infty_mul g.property⟩

857

858@[simp]

859theorem infty_coeFn_mul (f g : lp B ∞) : ⇑(f * g) = ⇑f * ⇑g :=

860 rfl

861

862instance nonUnitalRing : NonUnitalRing (lp B ∞) := fast_instance%

863 Function.Injective.nonUnitalRing lp.coeFun.coe Subtype.coe_injective (lp.coeFn_zero B ∞)

864 lp.coeFn_add infty_coeFn_mul lp.coeFn_neg lp.coeFn_sub (fun _ _ => rfl) fun _ _ => rfl

865

866instance nonUnitalNormedRing : NonUnitalNormedRing (lp B ∞) :=

867 { lp.nonUnitalRing, lp.normedAddCommGroup with

868 norm_mul_le f g := lp.norm_le_of_forall_le (by positivity) fun i ↦ calc

869 ‖(f * g) i‖ ≤ ‖f i‖ * ‖g i‖ := norm_mul_le _ _

870 _ ≤ ‖f‖ * ‖g‖ := mul_le_mul (lp.norm_apply_le_norm ENNReal.top_ne_zero f i)

871 (lp.norm_apply_le_norm ENNReal.top_ne_zero g i) (norm_nonneg _) (norm_nonneg _) }

872

873instance nonUnitalNormedCommRing {B : I → Type*} [∀ i, NonUnitalNormedCommRing (B i)] :

874 NonUnitalNormedCommRing (lp B ∞) where

875 mul_comm _ _ := ext <| mul_comm ..

876

877

-- we also want a `NonUnitalNormedCommRing` instance, but this has to wait for https://github.com/leanprover-community/mathlib3/pull/13719

878instance infty_isScalarTower {𝕜} [NormedRing 𝕜] [∀ i, Module 𝕜 (B i)] [∀ i, IsBoundedSMul 𝕜 (B i)]

879 [∀ i, IsScalarTower 𝕜 (B i) (B i)] : IsScalarTower 𝕜 (lp B ∞) (lp B ∞) :=

880 ⟨fun r f g => lp.ext <| smul_assoc (N := ∀ i, B i) (α := ∀ i, B i) r (⇑f) (⇑g)⟩

881

882instance infty_smulCommClass {𝕜} [NormedRing 𝕜] [∀ i, Module 𝕜 (B i)] [∀ i, IsBoundedSMul 𝕜 (B i)]

883 [∀ i, SMulCommClass 𝕜 (B i) (B i)] : SMulCommClass 𝕜 (lp B ∞) (lp B ∞) :=

884 ⟨fun r f g => lp.ext <| smul_comm (N := ∀ i, B i) (α := ∀ i, B i) r (⇑f) (⇑g)⟩

885

886section StarRing

887

888variable [∀ i, StarRing (B i)] [∀ i, NormedStarGroup (B i)]

889

890instance inftyStarRing : StarRing (lp B ∞) :=

891 { lp.instStarAddMonoid with

892 star_mul := fun _f _g => ext <| star_mul (R := ∀ i, B i) _ _ }

893

894instance inftyCStarRing [∀ i, CStarRing (B i)] : CStarRing (lp B ∞) where

895 norm_mul_self_le f := by

896 rw [← sq, ← Real.le_sqrt (norm_nonneg _) (norm_nonneg _)]

897 refine lp.norm_le_of_forall_le ‖star f * f‖.sqrt_nonneg fun i => ?_

898 rw [Real.le_sqrt (norm_nonneg _) (norm_nonneg _), sq, ← CStarRing.norm_star_mul_self]

899 exact lp.norm_apply_le_norm ENNReal.top_ne_zero (star f * f) i

900

901end StarRing

902

903end NonUnitalNormedRing

904

905section NormedRing

906

907variable {I : Type*} {B : I → Type*} [∀ i, NormedRing (B i)]

908

909instance _root_.PreLp.ring : Ring (PreLp B) :=

910 inferInstanceAs (Ring (∀ i, B i))

911

912variable [∀ i, NormOneClass (B i)]

913

914theorem _root_.one_memℓp_infty : Memℓp (1 : ∀ i, B i) ∞ :=

915 ⟨1, by rintro i ⟨i, rfl⟩; exact norm_one.le⟩

916

917variable (B) in

918/-- The `𝕜`-subring of elements of `∀ i : α, B i` whose `lp` norm is finite. This is `lp E ∞`,

919with extra structure. -/

920def _root_.lpInftySubring : Subring (PreLp B) :=

921 { lp B ∞ with

922 carrier := { f | Memℓp f ∞ }

923 one_mem' := one_memℓp_infty

924 mul_mem' := Memℓp.infty_mul }

925

926instance inftyRing : Ring (lp B ∞) :=

927 inferInstanceAs <| Ring (lpInftySubring B)

928

929theorem _root_.Memℓp.infty_pow {f : ∀ i, B i} (hf : Memℓp f ∞) (n : ℕ) : Memℓp (f ^ n) ∞ :=

930 (lpInftySubring B).pow_mem hf n

931

932theorem _root_.natCast_memℓp_infty (n : ℕ) : Memℓp (n : ∀ i, B i) ∞ :=

933 natCast_mem (lpInftySubring B) n

934

935theorem _root_.intCast_memℓp_infty (z : ℤ) : Memℓp (z : ∀ i, B i) ∞ :=

936 intCast_mem (lpInftySubring B) z

937

938@[simp]

939theorem infty_coeFn_one : ⇑(1 : lp B ∞) = 1 :=

940 rfl

941

942@[simp]

943theorem infty_coeFn_pow (f : lp B ∞) (n : ℕ) : ⇑(f ^ n) = (⇑f) ^ n :=

944 rfl

945

946@[simp]

947theorem infty_coeFn_natCast (n : ℕ) : ⇑(n : lp B ∞) = n :=

948 rfl

949

950@[simp]

951theorem infty_coeFn_intCast (z : ℤ) : ⇑(z : lp B ∞) = z :=

952 rfl

953

954instance [Nonempty I] : NormOneClass (lp B ∞) where

955 norm_one := by simp_rw [lp.norm_eq_ciSup, infty_coeFn_one, Pi.one_apply, norm_one, ciSup_const]

956

957instance inftyNormedRing : NormedRing (lp B ∞) :=

958 { lp.inftyRing, lp.nonUnitalNormedRing with }

959

960end NormedRing

961

962section NormedCommRing

963

964variable {I : Type*} {B : I → Type*} [∀ i, NormedCommRing (B i)] [∀ i, NormOneClass (B i)]

965

966instance inftyNormedCommRing : NormedCommRing (lp B ∞) where

967 mul_comm := mul_comm

968

969end NormedCommRing

970

971section Algebra

972

973variable {I : Type*} {B : I → Type*}

974variable [NormedField 𝕜] [∀ i, NormedRing (B i)] [∀ i, NormedAlgebra 𝕜 (B i)]

975

976instance _root_.PreLp.algebra : Algebra 𝕜 (PreLp B) :=

977 inferInstanceAs <| Algebra 𝕜 (∀ i, B i)

978

979variable [∀ i, NormOneClass (B i)]

980

981theorem _root_.algebraMap_memℓp_infty (k : 𝕜) : Memℓp (algebraMap 𝕜 (∀ i, B i) k) ∞ := by

982 rw [Algebra.algebraMap_eq_smul_one]

983 exact (one_memℓp_infty.const_smul k : Memℓp (k • (1 : ∀ i, B i)) ∞)

984

985variable (𝕜 B)

986

987/-- The `𝕜`-subalgebra of elements of `∀ i : α, B i` whose `lp` norm is finite. This is `lp E ∞`,

988with extra structure. -/

989def _root_.lpInftySubalgebra : Subalgebra 𝕜 (PreLp B) :=

990 { lpInftySubring B with

991 carrier := { f | Memℓp f ∞ }

992 algebraMap_mem' := algebraMap_memℓp_infty }

993

994variable {𝕜 B}

995

996instance : Algebra 𝕜 (lp B ∞) := inferInstanceAs <| Algebra 𝕜 (lpInftySubalgebra 𝕜 B)

997

998instance inftyNormedAlgebra : NormedAlgebra 𝕜 (lp B ∞) where

999 norm_smul_le := norm_smul_le

1000

1001end Algebra

1002

1003section Single

1004

1005variable [NormedRing 𝕜] [∀ i, Module 𝕜 (E i)] [∀ i, IsBoundedSMul 𝕜 (E i)]

1006variable [DecidableEq α]

1007

1008/-- The element of `lp E p` which is `a : E i` at the index `i`, and zero elsewhere. -/

1009protected def single (p) (i : α) (a : E i) : lp E p :=

1010 ⟨Pi.single i a, by

1011 refine (memℓp_zero ?_).of_exponent_ge zero_le

1012 refine (Set.finite_singleton i).subset ?_

1013 intro j

1014 simp only [Set.mem_singleton_iff, Ne,

1015 Set.mem_ofPred_eq]

1016 rw [not_imp_comm]

1017 intro h

1018 exact Pi.single_eq_of_ne h _⟩

1019

1020@[norm_cast]

1021protected theorem coeFn_single (p) (i : α) (a : E i) :

1022 ⇑(lp.single p i a) = Pi.single i a := rfl

1023

1024@[simp]

1025protected theorem single_apply (p) (i : α) (a : E i) (j : α) :

1026 lp.single p i a j = Pi.single i a j :=

1027 rfl

1028

1029protected theorem single_apply_self (p) (i : α) (a : E i) : lp.single p i a i = a :=

1030 Pi.single_eq_same _ _

1031

1032protected theorem single_apply_ne (p) (i : α) (a : E i) {j : α} (hij : j ≠ i) :

1033 lp.single p i a j = 0 :=

1034 Pi.single_eq_of_ne hij _

1035

1036@[simp]

1037protected theorem single_zero (p) (i : α) :

1038 lp.single p i (0 : E i) = 0 :=

1039 ext <| Pi.single_zero _

1040

1041@[simp]

1042protected theorem single_add (p) (i : α) (a b : E i) :

1043 lp.single p i (a + b) = lp.single p i a + lp.single p i b :=

1044 ext <| Pi.single_add _ _ _

1045

1046/-- `single` as an `AddMonoidHom`. -/

1047@[simps]

1048def singleAddMonoidHom (p) (i : α) : E i →+ lp E p where

1049 toFun := lp.single p i

1050 map_zero' := lp.single_zero _ _

1051 map_add' := lp.single_add _ _

1052

1053@[simp]

1054protected theorem single_neg (p) (i : α) (a : E i) : lp.single p i (-a) = -lp.single p i a :=

1055 ext <| Pi.single_neg _ _

1056

1057@[simp]

1058protected theorem single_sub (p) (i : α) (a b : E i) :

1059 lp.single p i (a - b) = lp.single p i a - lp.single p i b :=

1060 ext <| Pi.single_sub _ _ _

1061

1062@[simp]

1063protected theorem single_smul (p) (i : α) (c : 𝕜) (a : E i) :

1064 lp.single p i (c • a) = c • lp.single p i a :=

1065 ext <| Pi.single_smul _ _ _

1066

1067/-- `single` as a `LinearMap`. -/

1068@[simps]

1069def lsingle (p) (i : α) : E i →ₗ[𝕜] lp E p where

1070 toFun := lp.single p i

1071 __ := singleAddMonoidHom p i

1072 map_smul' := lp.single_smul p i

1073

1074/-- The basis for `ℓ⁰(α, 𝕜)` given by `lp.single`. -/

1075@[simps repr_apply]

1076noncomputable def zeroBasis : Module.Basis α 𝕜 ℓ⁰(α, 𝕜) where

1077 repr :=

1078 { toFun x := .ofSupportFinite ⇑x <| memℓp_zero_iff.mp x.2

1079 invFun x := ⟨⇑x, memℓp_zero_iff.mpr x.hasFiniteSupport⟩

1080 map_add' _ _ := Finsupp.ext fun _ ↦ rfl

1081 map_smul' _ _ := Finsupp.ext fun _ ↦ rfl

1082 left_inv _ := rfl

1083 right_inv _ := Finsupp.ext fun _ ↦ rfl }

1084

1085set_option backward.isDefEq.respectTransparency false in

1086lemma zeroBasis_apply (i : α) : zeroBasis i = lp.single 0 i (1 : 𝕜) := by

1087 ext; simp [zeroBasis, Finsupp.single_apply, Pi.single, Function.update, eq_comm]

1088

1089protected theorem norm_sum_single (hp : 0 < p.toReal) (f : ∀ i, E i) (s : Finset α) :

1090 ‖∑ i ∈ s, lp.single p i (f i)‖ ^ p.toReal = ∑ i ∈ s, ‖f i‖ ^ p.toReal := by

1091 refine (hasSum_norm hp (∑ i ∈ s, lp.single p i (f i))).unique ?_

1092 simp only [lp.coeFn_single, coeFn_sum, Finset.sum_apply, Finset.sum_pi_single]

1093 have h : ∀ i ∉ s, ‖ite (i ∈ s) (f i) 0‖ ^ p.toReal = 0 := fun i hi ↦ by

1094 simp [ite_eq_right hi, Real.zero_rpow hp.ne']

1095 have h' : ∀ i ∈ s, ‖f i‖ ^ p.toReal = ‖ite (i ∈ s) (f i) 0‖ ^ p.toReal := by

1096 intro i hi

1097 rw [ite_eq_left hi]

1098 simpa [Finset.sum_congr rfl h'] using hasSum_sum_of_ne_finset_zero h

1099

1100@[simp]

1101protected theorem norm_single (hp : 0 < p) (i : α) (x : E i) : ‖lp.single p i x‖ = ‖x‖ := by

1102 have : Nonempty α := ⟨i⟩

1103 induction p with

1104 | top =>

1105 simp only [norm_eq_ciSup, lp.coeFn_single]

1106 refine

1107 ciSup_eq_of_forall_le_of_forall_lt_exists_gt (fun j => ?_) fun n hn => ⟨i, hn.trans_eq ?_⟩

1108 · obtain rfl | hij := Decidable.eq_or_ne i j

1109 · rw [Pi.single_eq_same]

1110 · rw [Pi.single_eq_of_ne' hij, _root_.norm_zero]

1111 exact norm_nonneg _

1112 · rw [Pi.single_eq_same]

1113 | coe p =>

1114 have : 0 < (p : ℝ≥0∞).toReal := by simpa using hp

1115 rw [norm_eq_tsum_rpow this, tsum_eq_single i, lp.coeFn_single, one_div,

1116 Real.rpow_rpow_inv _ this.ne', Pi.single_eq_same]

1117 · exact norm_nonneg _

1118 · intro j hji

1119 rw [lp.coeFn_single, Pi.single_eq_of_ne hji, _root_.norm_zero, Real.zero_rpow this.ne']

1120

1121theorem isometry_single [Fact (1 ≤ p)] (i : α) : Isometry (lp.single (E := E) p i) :=

1122 AddMonoidHomClass.isometry_of_norm (lp.singleAddMonoidHom (E := E) p i) fun _ ↦

1123 lp.norm_single (zero_lt_one.trans_le Fact.out) _ _

1124

1125variable (p E) in

1126/-- `lp.single` as a continuous morphism of additive monoids. -/

1127def singleContinuousAddMonoidHom [Fact (1 ≤ p)] (i : α) :

1128 ContinuousAddMonoidHom (E i) (lp E p) where

1129 __ := singleAddMonoidHom p i

1130 continuous_toFun := isometry_single i |>.continuous

1131

1132@[simp]

1133theorem singleContinuousAddMonoidHom_apply [Fact (1 ≤ p)] (i : α) (x : E i) :

1134 singleContinuousAddMonoidHom E p i x = lp.single p i x :=

1135 rfl

1136

1137variable (𝕜 p E) in

1138/-- `lp.single` as a continuous linear map. -/

1139def singleContinuousLinearMap [Fact (1 ≤ p)] (i : α) : E i →L[𝕜] lp E p where

1140 __ := lsingle p i

1141 cont := isometry_single i |>.continuous

1142

1143@[simp]

1144theorem singleContinuousLinearMap_apply [Fact (1 ≤ p)] (i : α) (x : E i) :

1145 singleContinuousLinearMap 𝕜 E p i x = lp.single p i x :=

1146 rfl

1147

1148protected theorem norm_sub_norm_compl_sub_single (hp : 0 < p.toReal) (f : lp E p) (s : Finset α) :

1149 ‖f‖ ^ p.toReal - ‖f - ∑ i ∈ s, lp.single p i (f i)‖ ^ p.toReal =

1150 ∑ i ∈ s, ‖f i‖ ^ p.toReal := by

1151 refine ((hasSum_norm hp f).sub (hasSum_norm hp (f - ∑ i ∈ s, lp.single p i (f i)))).unique ?_

1152 let F : α → ℝ := fun i => ‖f i‖ ^ p.toReal - ‖(f - ∑ i ∈ s, lp.single p i (f i)) i‖ ^ p.toReal

1153 have hF : ∀ i ∉ s, F i = 0 := by

1154 intro i hi

1155 suffices ‖f i‖ ^ p.toReal - ‖f i - ite (i ∈ s) (f i) 0‖ ^ p.toReal = 0 by

1156 simpa only [coeFn_sub, coeFn_sum, lp.coeFn_single, Pi.sub_apply, Finset.sum_apply,

1157 Finset.sum_pi_single, F] using this

1158 simp only [ite_eq_right hi, sub_zero, sub_self]

1159 have hF' : ∀ i ∈ s, F i = ‖f i‖ ^ p.toReal := by

1160 intro i hi

1161 simp only [F, coeFn_sum, lp.single_apply, ite_eq_left hi, sub_self, coeFn_sub,

1162 Pi.sub_apply, Finset.sum_apply, Finset.sum_pi_single, sub_eq_self]

1163 simp [Real.zero_rpow hp.ne']

1164 have : HasSum F (∑ i ∈ s, F i) := hasSum_sum_of_ne_finset_zero hF

1165 rwa [Finset.sum_congr rfl hF'] at this

1166

1167protected theorem norm_compl_sum_single (hp : 0 < p.toReal) (f : lp E p) (s : Finset α) :

1168 ‖f - ∑ i ∈ s, lp.single p i (f i)‖ ^ p.toReal = ‖f‖ ^ p.toReal - ∑ i ∈ s, ‖f i‖ ^ p.toReal := by

1169 linarith [lp.norm_sub_norm_compl_sub_single hp f s]

1170

1171/-- The canonical finitely-supported approximations to an element `f` of `lp` converge to it, in the

1172`lp` topology. -/

1173protected theorem hasSum_single [Fact (1 ≤ p)] (hp : p ≠ ⊤) (f : lp E p) :

1174 HasSum (fun i : α => lp.single p i (f i : E i)) f := by

1175 have hp₀ : 0 < p := zero_lt_one.trans_le Fact.out

1176 have hp' : 0 < p.toReal := ENNReal.toReal_pos hp₀.ne' hp

1177 have := lp.hasSum_norm hp' f

1178 rw [HasSum, Metric.tendsto_nhds] at this ⊢

1179 intro ε hε

1180 refine (this _ (Real.rpow_pos_of_pos hε p.toReal)).mono ?_

1181 intro s hs

1182 rw [← Real.rpow_lt_rpow_iff dist_nonneg (le_of_lt hε) hp']

1183 rw [dist_comm] at hs

1184 simp only [dist_eq_norm, Real.norm_eq_abs] at hs ⊢

1185 have H : ‖(∑ i ∈ s, lp.single p i (f i : E i)) - f‖ ^ p.toReal =

1186 ‖f‖ ^ p.toReal - ∑ i ∈ s, ‖f i‖ ^ p.toReal := by

1187 simpa only [coeFn_neg, Pi.neg_apply, lp.single_neg, Finset.sum_neg_distrib, neg_sub_neg,

1188 norm_neg, _root_.norm_neg] using lp.norm_compl_sum_single hp' (-f) s

1189 rw [← H] at hs

1190 have : |‖(∑ i ∈ s, lp.single p i (f i : E i)) - f‖ ^ p.toReal| =

1191 ‖(∑ i ∈ s, lp.single p i (f i : E i)) - f‖ ^ p.toReal := by

1192 simp only [Real.abs_rpow_of_nonneg (norm_nonneg _), abs_norm]

1193 exact this ▸ hs

1194

1195/-- Two continuous additive maps from `lp E p` agree if they agree on `lp.single`.

1196

1197See note [partially-applied ext lemmas]. -/

1198@[local ext] -- not globally `ext` due to `hp`

1199theorem ext_continuousAddMonoidHom

1200 {F : Type*} [AddCommMonoid F] [TopologicalSpace F] [T2Space F]

1201 [Fact (1 ≤ p)] (hp : p ≠ ⊤) ⦃f g : ContinuousAddMonoidHom (lp E p) F⦄

1202 (h : ∀ i,

1203 f.comp (singleContinuousAddMonoidHom E p i) = g.comp (singleContinuousAddMonoidHom E p i)) :

1204 f = g := by

1205 ext x

1206 have := lp.hasSum_single hp x

1207 rw [← (this.map f f.continuous).tsum_eq, ← (this.map g g.continuous).tsum_eq]

1208 congr! 2 with i

1209 exact DFunLike.congr_fun (h i) (x i)

1210

1211/-- Two continuous linear maps from `lp E p` agree if they agree on `lp.single`.

1212

1213See note [partially-applied ext lemmas]. -/

1214@[local ext] -- not globally `ext` due to `hp`

1215theorem ext_continuousLinearMap

1216 {F : Type*} [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] [T2Space F]

1217 [Fact (1 ≤ p)] (hp : p ≠ ⊤) ⦃f g : lp E p →L[𝕜] F⦄

1218 (h : ∀ i,

1219 f.comp (singleContinuousLinearMap 𝕜 E p i) = g.comp (singleContinuousLinearMap 𝕜 E p i)) :

1220 f = g :=

1221 ContinuousLinearMap.toContinuousAddMonoidHom_injective <|

1222 ext_continuousAddMonoidHom hp fun i => ContinuousLinearMap.toContinuousAddMonoidHom_inj.2 (h i)

1223

1224end Single

1225

1226section OfLE

1227

1228variable [NormedRing 𝕜] [∀ i, Module 𝕜 (E i)] [∀ i, IsBoundedSMul 𝕜 (E i)] {p q r : ℝ≥0∞}

1229

1230variable (𝕜 E) in

1231/-- The `AddSubgroup.inclusion` between `lp` spaces, as a linear map. -/

1232def linearMapOfLE (h : p ≤ q) : lp E p →ₗ[𝕜] lp E q where

1233 toFun f := ⟨f, lp.memℓp f |>.of_exponent_ge h⟩

1234 map_add' _ _ := by ext; rfl

1235 map_smul' _ _ := by ext; rfl

1236

1237@[simp]

1238lemma coe_linearMapOfLE_apply (h : p ≤ q) (f : lp E p) :

1239 ⇑(linearMapOfLE 𝕜 E h f) = f := by

1240 ext; rfl

1241

1242

1243@[simp]

1244lemma toAddMonoidHom_linearMapOfLE (h : p ≤ q) :

1245 (linearMapOfLE 𝕜 E h).toAddMonoidHom = AddSubgroup.inclusion (lp.monotone h) := by

1246 ext; rfl

1247

1248lemma linearMapOfLE_comp (hpq : p ≤ q) (hqr : q ≤ r) :

1249 (linearMapOfLE 𝕜 E hqr).comp (linearMapOfLE 𝕜 E hpq) = linearMapOfLE 𝕜 E (hpq.trans hqr) := by

1250 ext; rfl

1251

1252end OfLE

1253

1254section Eval

1255

1256variable [NormedRing 𝕜] [∀ i, Module 𝕜 (E i)] [∀ i, IsBoundedSMul 𝕜 (E i)] {p : ℝ≥0∞}

1257

1258variable (E p) in

1259/-- Evaluation at a single coordinate, as a linear map on `lp E p`. -/

1260@[simps]

1261def evalₗ (i : α) : lp E p →ₗ[𝕜] E i where

1262 toFun f := f i

1263 map_add' _ _ := rfl

1264 map_smul' _ _ := rfl

1265

1266variable (𝕜 E p) in

1267/-- Evaluation at a single coordinate, as a continuous linear map on `lp E p`. -/

1268def evalCLM [Fact (1 ≤ p)] (i : α) : lp E p →L[𝕜] E i :=

1269 (evalₗ E p i).mkContinuous 1 fun x ↦ by

1270 have hp : p ≠ 0 := zero_lt_one.trans_le Fact.out |>.ne'

1271 simpa only [evalₗ_apply, one_mul, ge_iff_le] using norm_apply_le_norm hp x i

1272

1273end Eval

1274

1275section Topology

1276

1277open Filter

1278

1279open scoped Topology uniformity

1280

1281/-- The coercion from `lp E p` to `∀ i, E i` is uniformly continuous. -/

1282theorem uniformContinuous_coe [_i : Fact (1 ≤ p)] :

1283 UniformContinuous (α := lp E p) ((↑) : lp E p → ∀ i, E i) :=

1284 uniformContinuous_pi.2 fun i ↦ (lipschitzWith_one_eval p i).uniformContinuous

1285

1286variable {ι : Type*} {l : Filter ι} [Filter.NeBot l]

1287

1288theorem norm_apply_le_of_tendsto {C : ℝ} {F : ι → lp E ∞} (hCF : ∀ᶠ k in l, ‖F k‖ ≤ C)

1289 {f : ∀ a, E a} (hf : Tendsto (id fun i => F i : ι → ∀ a, E a) l (𝓝 f)) (a : α) : ‖f a‖ ≤ C := by

1290 have : Tendsto (fun k => ‖F k a‖) l (𝓝 ‖f a‖) :=

1291 (Tendsto.comp (continuous_apply a).continuousAt hf).norm

1292 refine le_of_tendsto this (hCF.mono ?_)

1293 intro k hCFk

1294 exact (norm_apply_le_norm ENNReal.top_ne_zero (F k) a).trans hCFk

1295

1296variable [_i : Fact (1 ≤ p)]

1297

1298theorem sum_rpow_le_of_tendsto (hp : p ≠ ∞) {C : ℝ} {F : ι → lp E p} (hCF : ∀ᶠ k in l, ‖F k‖ ≤ C)

1299 {f : ∀ a, E a} (hf : Tendsto (id fun i => F i : ι → ∀ a, E a) l (𝓝 f)) (s : Finset α) :

1300 ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C ^ p.toReal := by

1301 have hp' : p ≠ 0 := (zero_lt_one.trans_le _i.elim).ne'

1302 have hp'' : 0 < p.toReal := ENNReal.toReal_pos hp' hp

1303 let G : (∀ a, E a) → ℝ := fun f => ∑ a ∈ s, ‖f a‖ ^ p.toReal

1304 have hG : Continuous G := by

1305 refine continuous_finsetSum s ?_

1306 intro a _

1307 have : Continuous fun f : ∀ a, E a => f a := continuous_apply a

1308 exact this.norm.rpow_const fun _ => Or.inr hp''.le

1309 refine le_of_tendsto (hG.continuousAt.tendsto.comp hf) ?_

1310 refine hCF.mono ?_

1311 intro k hCFk

1312 refine (lp.sum_rpow_le_norm_rpow hp'' (F k) s).trans ?_

1313 gcongr

1314

1315/-- "Semicontinuity of the `lp` norm": If all sufficiently large elements of a sequence in `lp E p`

1316have `lp` norm `≤ C`, then the pointwise limit, if it exists, also has `lp` norm `≤ C`. -/

1317theorem norm_le_of_tendsto {C : ℝ} {F : ι → lp E p} (hCF : ∀ᶠ k in l, ‖F k‖ ≤ C) {f : lp E p}

1318 (hf : Tendsto (id fun i => F i : ι → ∀ a, E a) l (𝓝 f)) : ‖f‖ ≤ C := by

1319 obtain ⟨i, hi⟩ := hCF.exists

1320 have hC : 0 ≤ C := (norm_nonneg _).trans hi

1321 rcases eq_top_or_lt_top p with (rfl | hp)

1322 · apply norm_le_of_forall_le hC

1323 exact norm_apply_le_of_tendsto hCF hf

1324 · have : 0 < p := zero_lt_one.trans_le _i.elim

1325 have hp' : 0 < p.toReal := ENNReal.toReal_pos this.ne' hp.ne

1326 apply norm_le_of_forall_sum_le hp' hC

1327 exact sum_rpow_le_of_tendsto hp.ne hCF hf

1328

1329/-- If `f` is the pointwise limit of a bounded sequence in `lp E p`, then `f` is in `lp E p`. -/

1330theorem memℓp_of_tendsto {F : ι → lp E p} (hF : Bornology.IsBounded (Set.range F)) {f : ∀ a, E a}

1331 (hf : Tendsto (id fun i => F i : ι → ∀ a, E a) l (𝓝 f)) : Memℓp f p := by

1332 obtain ⟨C, hCF⟩ : ∃ C, ∀ k, ‖F k‖ ≤ C := hF.exists_norm_le.imp fun _ ↦ Set.forall_mem_range.1

1333 rcases eq_top_or_lt_top p with (rfl | hp)

1334 · apply memℓp_infty

1335 use C

1336 rintro _ ⟨a, rfl⟩

1337 exact norm_apply_le_of_tendsto (Eventually.of_forall hCF) hf a

1338 · apply memℓp_gen'

1339 exact sum_rpow_le_of_tendsto hp.ne (Eventually.of_forall hCF) hf

1340

1341/-- If a sequence is Cauchy in the `lp E p` topology and pointwise convergent to an element `f` of

1342`lp E p`, then it converges to `f` in the `lp E p` topology. -/

1343theorem tendsto_lp_of_tendsto_pi {F : ℕ → lp E p} (hF : CauchySeq F) {f : lp E p}

1344 (hf : Tendsto (id fun i => F i : ℕ → ∀ a, E a) atTop (𝓝 f)) : Tendsto F atTop (𝓝 f) := by

1345 rw [Metric.nhds_basis_closedBall.tendsto_right_iff]

1346 intro ε hε

1347 have hε' : { p : lp E p × lp E p | ‖p.1 - p.2‖ < ε } ∈ uniformity (lp E p) :=

1348 NormedAddCommGroup.uniformity_basis_dist.mem_of_mem hε

1349 refine (hF.eventually_eventually hε').mono ?_

1350 rintro n (hn : ∀ᶠ l in atTop, ‖(fun f => F n - f) (F l)‖ < ε)

1351 rw [mem_closedBall_iff_norm]

1352 refine norm_le_of_tendsto (hn.mono fun k hk => hk.le) ?_

1353 rw [tendsto_pi_nhds]

1354 intro a

1355 exact (hf.apply_nhds a).const_sub (F n a)

1356

1357variable [∀ a, CompleteSpace (E a)]

1358

1359instance completeSpace : CompleteSpace (lp E p) :=

1360 Metric.complete_of_cauchySeq_tendsto (by

1361 intro F hF

1362 -- A Cauchy sequence in `lp E p` is pointwise convergent; let `f` be the pointwise limit.

1363 obtain ⟨f, hf⟩ := cauchySeq_tendsto_of_complete

1364 ((uniformContinuous_coe (p := p)).comp_cauchySeq hF)

1365 -- Since the Cauchy sequence is bounded, its pointwise limit `f` is in `lp E p`.

1366 have hf' : Memℓp f p := memℓp_of_tendsto hF.isBounded_range hf

1367 -- And therefore `f` is its limit in the `lp E p` topology as well as pointwise.

1368 exact ⟨⟨f, hf'⟩, tendsto_lp_of_tendsto_pi hF hf⟩)

1369

1370end Topology

1371

1372end lp

1373

1374section Lipschitz

1375

1376open ENNReal lp

1377variable {ι : Type*}

1378

1379lemma LipschitzWith.uniformly_bounded [PseudoMetricSpace α] (g : α → ι → ℝ) {K : ℝ≥0}

1380 (hg : ∀ i, LipschitzWith K (g · i)) (a₀ : α) (hga₀b : Memℓp (g a₀) ∞) (a : α) :

1381 Memℓp (g a) ∞ := by

1382 rcases hga₀b with ⟨M, hM⟩

1383 use ↑K * dist a a₀ + M

1384 rintro - ⟨i, rfl⟩

1385 calc

1386 |g a i| = |g a i - g a₀ i + g a₀ i| := by simp

1387 _ ≤ |g a i - g a₀ i| + |g a₀ i| := abs_add_le _ _

1388 _ ≤ ↑K * dist a a₀ + M := by

1389 gcongr

1390 · exact lipschitzWith_iff_dist_le_mul.1 (hg i) a a₀

1391 · exact hM ⟨i, rfl⟩

1392

1393theorem LipschitzOnWith.coordinate [PseudoMetricSpace α] (f : α → ℓ^∞(ι, ℝ)) (s : Set α) (K : ℝ≥0) :

1394 LipschitzOnWith K f s ↔ ∀ i : ι, LipschitzOnWith K (fun a : α ↦ f a i) s := by

1395 simp_rw [lipschitzOnWith_iff_dist_le_mul]

1396 constructor

1397 · intro hfl i x hx y hy

1398 calc

1399 dist (f x i) (f y i) ≤ dist (f x) (f y) := by

1400 simp only [dist_eq_norm]

1401 exact lp.norm_apply_le_norm top_ne_zero (f x - f y) i

1402 _ ≤ K * dist x y := hfl x hx y hy

1403 · intro hgl x hx y hy

1404 rw [dist_eq_norm]

1405 apply lp.norm_le_of_forall_le

1406 · positivity

1407 intro i

1408 apply hgl i x hx y hy

1409

1410theorem LipschitzWith.coordinate [PseudoMetricSpace α] {f : α → ℓ^∞(ι, ℝ)} (K : ℝ≥0) :

1411 LipschitzWith K f ↔ ∀ i : ι, LipschitzWith K (fun a : α ↦ f a i) := by

1412 simp_rw [← lipschitzOnWith_univ]

1413 apply LipschitzOnWith.coordinate

1414

1415end Lipschitz