From ac19b4a965de2dec48c4a502e58bc7bc7a76e89d Mon Sep 17 00:00:00 2001 From: sgouezel Date: Sat, 13 Feb 2021 19:32:58 +0000 Subject: [PATCH] refactor(measure_theory/l1_space): remove one of the two definitions of L1 space (#6058) Currently, we have two independent versions of the `L^1` space in mathlib: one coming from the general family of `L^p` spaces, the other one is an ad hoc construction based on the `integrable` predicate used in the construction of the Bochner integral. We remove the second construction, and use instead the `L^1` space coming from the family of `L^p` spaces to construct the Bochner integral. Still, we keep the `integrable` predicate as it is generally useful, and show that it coincides with the `mem_Lp 1` predicate. --- docs/overview.yaml | 2 +- src/analysis/convex/integral.lean | 4 +- src/analysis/normed_space/basic.lean | 12 + src/measure_theory/ae_eq_fun.lean | 3 + src/measure_theory/bochner_integration.lean | 431 ++++++++++---------- src/measure_theory/l1_space.lean | 405 ++++++------------ src/measure_theory/prod.lean | 11 +- src/measure_theory/set_integral.lean | 109 ++--- src/measure_theory/simple_func_dense.lean | 14 +- src/order/galois_connection.lean | 2 +- 10 files changed, 387 insertions(+), 606 deletions(-) diff --git a/docs/overview.yaml b/docs/overview.yaml index a042723445498..481e1cfe86ed6 100644 --- a/docs/overview.yaml +++ b/docs/overview.yaml @@ -284,7 +284,7 @@ Analysis: monotone convergence theorem: 'measure_theory.lintegral_infi_ae' Fatou's lemma: 'measure_theory.lintegral_liminf_le' vector-valued integrable function (Bochner integral): 'measure_theory.integrable' - $L^1$ space: 'measure_theory.l1' + $L^p$ space: 'measure_theory.Lp' Bochner integral: 'measure_theory.integral' dominated convergence theorem: 'measure_theory.tendsto_integral_of_dominated_convergence' fundamental theorem of calculus, part 1: 'interval_integral.integral_has_fderiv_at_of_tendsto_ae' diff --git a/src/analysis/convex/integral.lean b/src/analysis/convex/integral.lean index 3a5aa3e7f265b..e3a5f71a2bd1f 100644 --- a/src/analysis/convex/integral.lean +++ b/src/analysis/convex/integral.lean @@ -57,9 +57,9 @@ begin have : tendsto (λ n, (F n).integral μ) at_top (𝓝 $ ∫ x, f x ∂μ), { simp only [simple_func.integral_eq_integral _ (simple_func.integrable_approx_on hfm hfi h₀ hc _)], - exact tendsto_integral_of_l1 _ hfi + exact tendsto_integral_of_L1 _ hfi (eventually_of_forall $ simple_func.integrable_approx_on hfm hfi h₀ hc) - (simple_func.tendsto_approx_on_l1_edist hfm h₀ hfs (hfi.sub hc).2) }, + (simple_func.tendsto_approx_on_L1_edist hfm h₀ hfs (hfi.sub hc).2) }, refine hsc.mem_of_tendsto (tendsto_const_nhds.smul this) (eventually_of_forall $ λ n, _), have : ∑ y in (F n).range, (μ ((F n) ⁻¹' {y})).to_real = (μ univ).to_real, by rw [← (F n).sum_range_measure_preimage_singleton, @ennreal.to_real_sum _ _ diff --git a/src/analysis/normed_space/basic.lean b/src/analysis/normed_space/basic.lean index 510c16a791f78..b930d637deda4 100644 --- a/src/analysis/normed_space/basic.lean +++ b/src/analysis/normed_space/basic.lean @@ -373,6 +373,18 @@ begin ... ≤ _ : le_trans (le_abs_self _) (abs_dist_sub_le_dist_add_add _ _ _ _) end +/-- A subgroup of a normed group is also a normed group, with the restriction of the norm. -/ +instance add_subgroup.normed_group {E : Type*} [normed_group E] (s : add_subgroup E) : + normed_group s := +{ norm := λx, norm (x : E), + dist_eq := λx y, dist_eq_norm (x : E) (y : E) } + +/-- If `x` is an element of a subgroup `s` of a normed group `E`, its norm in `s` is equal to its +norm in `E`. -/ +@[simp] lemma coe_norm_subgroup {E : Type*} [normed_group E] {s : add_subgroup E} (x : s) : + ∥x∥ = ∥(x:E)∥ := +rfl + /-- A submodule of a normed group is also a normed group, with the restriction of the norm. See note [implicit instance arguments]. -/ diff --git a/src/measure_theory/ae_eq_fun.lean b/src/measure_theory/ae_eq_fun.lean index 8919e40957246..cfb6b9e09869d 100644 --- a/src/measure_theory/ae_eq_fun.lean +++ b/src/measure_theory/ae_eq_fun.lean @@ -126,6 +126,9 @@ end @[ext] lemma ext {f g : α →ₘ[μ] β} (h : f =ᵐ[μ] g) : f = g := by rwa [← f.mk_coe_fn, ← g.mk_coe_fn, mk_eq_mk] +lemma ext_iff {f g : α →ₘ[μ] β} : f = g ↔ f =ᵐ[μ] g := +⟨λ h, by rw h, λ h, ext h⟩ + lemma coe_fn_mk (f : α → β) (hf) : (mk f hf : α →ₘ[μ] β) =ᵐ[μ] f := begin apply (ae_measurable.ae_eq_mk _).symm.trans, diff --git a/src/measure_theory/bochner_integration.lean b/src/measure_theory/bochner_integration.lean index 09c144ba19e9c..e439b5ce071d3 100644 --- a/src/measure_theory/bochner_integration.lean +++ b/src/measure_theory/bochner_integration.lean @@ -1,10 +1,11 @@ /- Copyright (c) 2019 Zhouhang Zhou. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Zhouhang Zhou, Yury Kudryashov +Authors: Zhouhang Zhou, Yury Kudryashov, Sébastien Gouëzel -/ import measure_theory.simple_func_dense import analysis.normed_space.bounded_linear_maps +import measure_theory.l1_space import topology.sequences /-! @@ -88,14 +89,14 @@ functions : 1. First go to the `L¹` space. For example, if you see `ennreal.to_real (∫⁻ a, ennreal.of_real $ ∥f a∥)`, that is the norm of - `f` in `L¹` space. Rewrite using `l1.norm_of_fun_eq_lintegral_norm`. + `f` in `L¹` space. Rewrite using `L1.norm_of_fun_eq_lintegral_norm`. 2. Show that the set `{f ∈ L¹ | ∫ f = ∫⁻ f⁺ - ∫⁻ f⁻}` is closed in `L¹` using `is_closed_eq`. 3. Show that the property holds for all simple functions `s` in `L¹` space. Typically, you need to convert various notions to their `simple_func` counterpart, using lemmas - like `l1.integral_coe_eq_integral`. + like `L1.integral_coe_eq_integral`. 4. Since simple functions are dense in `L¹`, ``` @@ -110,7 +111,7 @@ Use `is_closed_property` or `dense_range.induction_on` for this argument. * `α →ₛ E` : simple functions (defined in `measure_theory/integration`) * `α →₁[μ] E` : functions in L1 space, i.e., equivalence classes of integrable functions (defined in - `measure_theory/l1_space`) + `measure_theory/lp_space`) * `α →₁ₛ[μ] E` : simple functions in L1 space, i.e., equivalence classes of integrable simple functions @@ -383,7 +384,7 @@ end integral end simple_func -namespace l1 +namespace L1 open ae_eq_fun @@ -394,20 +395,19 @@ variables variables (α E μ) --- We use `Type*` instead of `add_subgroup` because otherwise we loose dot notation. -/-- `l1.simple_func` is a subspace of L1 consisting of equivalence classes of an integrable simple +/-- `L1.simple_func` is a subspace of L1 consisting of equivalence classes of an integrable simple function. -/ -def simple_func : Type* := -↥({ carrier := {f : α →₁[μ] E | ∃ (s : α →ₛ E), (ae_eq_fun.mk s s.ae_measurable : α →ₘ[μ] E) = f}, +def simple_func : add_subgroup (Lp E 1 μ) := +{ carrier := {f : α →₁[μ] E | ∃ (s : α →ₛ E), (ae_eq_fun.mk s s.ae_measurable : α →ₘ[μ] E) = f}, zero_mem' := ⟨0, rfl⟩, - add_mem' := λ f g ⟨s, hs⟩ ⟨t, ht⟩, - ⟨s + t, by simp only [coe_add, ← hs, ← ht, mk_add_mk, ← simple_func.coe_add]⟩, - neg_mem' := λ f ⟨s, hs⟩, ⟨-s, by simp only [coe_neg, ← hs, neg_mk, ← simple_func.coe_neg]⟩ } : - add_subgroup (α →₁[μ] E)) + add_mem' := λ f g ⟨s, hs⟩ ⟨t, ht⟩, ⟨s + t, + by simp only [←hs, ←ht, mk_add_mk, add_subgroup.coe_add, mk_eq_mk, simple_func.coe_add]⟩, + neg_mem' := λ f ⟨s, hs⟩, ⟨-s, + by simp only [←hs, neg_mk, simple_func.coe_neg, mk_eq_mk, add_subgroup.coe_neg]⟩ } variables {α E μ} -notation α ` →₁ₛ[`:25 μ `] ` E := measure_theory.l1.simple_func α E μ +notation α ` →₁ₛ[`:25 μ `] ` E := measure_theory.L1.simple_func α E μ namespace simple_func @@ -428,24 +428,15 @@ subtype.ext_iff.symm @[norm_cast] protected lemma eq_iff' {f g : α →₁ₛ[μ] E} : (f : α →ₘ[μ] E) = g ↔ f = g := iff.intro (simple_func.eq') (congr_arg _) -/-- L1 simple functions forms a `emetric_space`, with the emetric being inherited from L1 space, - i.e., `edist f g = ∫⁻ a, edist (f a) (g a)`. - Not declared as an instance as `α →₁ₛ[μ] β` will only be useful in the construction of the Bochner - integral. -/ -protected def emetric_space : emetric_space (α →₁ₛ[μ] E) := subtype.emetric_space - -/-- L1 simple functions forms a `metric_space`, with the metric being inherited from L1 space, +/-- L1 simple functions forms a `normed_group`, with the metric being inherited from L1 space, i.e., `dist f g = ennreal.to_real (∫⁻ a, edist (f a) (g a)`). Not declared as an instance as `α →₁ₛ[μ] β` will only be useful in the construction of the Bochner integral. -/ -protected def metric_space : metric_space (α →₁ₛ[μ] E) := subtype.metric_space +protected def normed_group : normed_group (α →₁ₛ[μ] E) := by apply_instance -local attribute [instance] simple_func.metric_space simple_func.emetric_space +local attribute [instance] simple_func.normed_group /-- Functions `α →₁ₛ[μ] E` form an additive commutative group. -/ -local attribute [instance, priority 10000] -protected def add_comm_group : add_comm_group (α →₁ₛ[μ] E) := add_subgroup.to_add_comm_group _ - instance : inhabited (α →₁ₛ[μ] E) := ⟨0⟩ @[simp, norm_cast] @@ -460,21 +451,7 @@ lemma coe_sub (f g : α →₁ₛ[μ] E) : ((f - g : α →₁ₛ[μ] E) : α @[simp] lemma edist_eq (f g : α →₁ₛ[μ] E) : edist f g = edist (f : α →₁[μ] E) (g : α →₁[μ] E) := rfl @[simp] lemma dist_eq (f g : α →₁ₛ[μ] E) : dist f g = dist (f : α →₁[μ] E) (g : α →₁[μ] E) := rfl -/-- The norm on `α →₁ₛ[μ] E` is inherited from L1 space. That is, `∥f∥ = ∫⁻ a, edist (f a) 0`. - Not declared as an instance as `α →₁ₛ[μ] E` will only be useful in the construction of the Bochner - integral. -/ -protected def has_norm : has_norm (α →₁ₛ[μ] E) := ⟨λf, ∥(f : α →₁[μ] E)∥⟩ - -local attribute [instance] simple_func.has_norm - lemma norm_eq (f : α →₁ₛ[μ] E) : ∥f∥ = ∥(f : α →₁[μ] E)∥ := rfl -lemma norm_eq' (f : α →₁ₛ[μ] E) : ∥f∥ = ennreal.to_real (edist (f : α →ₘ[μ] E) 0) := rfl - -/-- Not declared as an instance as `α →₁ₛ[μ] E` will only be useful in the construction of the -Bochner integral. -/ -protected def normed_group : normed_group (α →₁ₛ[μ] E) := -normed_group.of_add_dist (λ x, rfl) $ by - { intros, simp only [dist_eq, coe_add, l1.dist_eq, l1.coe_add], rw edist_add_right } variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 E] @@ -484,7 +461,9 @@ protected def has_scalar : has_scalar 𝕜 (α →₁ₛ[μ] E) := ⟨λk f, ⟨ begin rcases f with ⟨f, ⟨s, hs⟩⟩, use k • s, - rw [coe_smul, subtype.coe_mk, ← hs], refl + apply eq.trans (smul_mk k s s.ae_measurable).symm _, + rw hs, + refl, end ⟩⟩ local attribute [instance, priority 10000] simple_func.has_scalar @@ -513,105 +492,110 @@ end instances local attribute [instance] simple_func.normed_group simple_func.normed_space -section of_simple_func +section to_L1 /-- Construct the equivalence class `[f]` of an integrable simple function `f`. -/ -@[reducible] def of_simple_func (f : α →ₛ E) (hf : integrable f μ) : (α →₁ₛ[μ] E) := -⟨l1.of_fun f hf, ⟨f, rfl⟩⟩ +@[reducible] def to_L1 (f : α →ₛ E) (hf : integrable f μ) : (α →₁ₛ[μ] E) := +⟨hf.to_L1 f, ⟨f, rfl⟩⟩ -lemma of_simple_func_eq_of_fun (f : α →ₛ E) (hf : integrable f μ) : - (of_simple_func f hf : α →₁[μ] E) = l1.of_fun f hf := rfl +lemma to_L1_eq_to_L1 (f : α →ₛ E) (hf : integrable f μ) : + (to_L1 f hf : α →₁[μ] E) = hf.to_L1 f := rfl -lemma of_simple_func_eq_mk (f : α →ₛ E) (hf : integrable f μ) : - (of_simple_func f hf : α →ₘ[μ] E) = ae_eq_fun.mk f f.ae_measurable := rfl +lemma to_L1_eq_mk (f : α →ₛ E) (hf : integrable f μ) : + (to_L1 f hf : α →ₘ[μ] E) = ae_eq_fun.mk f f.ae_measurable := rfl -lemma of_simple_func_zero : of_simple_func (0 : α →ₛ E) (integrable_zero α E μ) = 0 := rfl +lemma to_L1_zero : to_L1 (0 : α →ₛ E) (integrable_zero α E μ) = 0 := rfl -lemma of_simple_func_add (f g : α →ₛ E) (hf : integrable f μ) (hg : integrable g μ) : - of_simple_func (f + g) (hf.add hg) = of_simple_func f hf + of_simple_func g hg := rfl +lemma to_L1_add (f g : α →ₛ E) (hf : integrable f μ) (hg : integrable g μ) : + to_L1 (f + g) (hf.add hg) = to_L1 f hf + to_L1 g hg := rfl -lemma of_simple_func_neg (f : α →ₛ E) (hf : integrable f μ) : - of_simple_func (-f) hf.neg = -of_simple_func f hf := rfl +lemma to_L1_neg (f : α →ₛ E) (hf : integrable f μ) : + to_L1 (-f) hf.neg = -to_L1 f hf := rfl -lemma of_simple_func_sub (f g : α →ₛ E) (hf : integrable f μ) (hg : integrable g μ) : - of_simple_func (f - g) (hf.sub hg) = of_simple_func f hf - of_simple_func g hg := -by { simp only [sub_eq_add_neg, ← of_simple_func_neg, ← of_simple_func_add], refl } +lemma to_L1_sub (f g : α →ₛ E) (hf : integrable f μ) (hg : integrable g μ) : + to_L1 (f - g) (hf.sub hg) = to_L1 f hf - to_L1 g hg := +by { simp only [sub_eq_add_neg, ← to_L1_neg, ← to_L1_add], refl } variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 E] -lemma of_simple_func_smul (f : α →ₛ E) (hf : integrable f μ) (c : 𝕜) : - of_simple_func (c • f) (hf.smul c) = c • of_simple_func f hf := rfl +lemma to_L1_smul (f : α →ₛ E) (hf : integrable f μ) (c : 𝕜) : + to_L1 (c • f) (hf.smul c) = c • to_L1 f hf := rfl -lemma norm_of_simple_func (f : α →ₛ E) (hf : integrable f μ) : - ∥of_simple_func f hf∥ = ennreal.to_real (∫⁻ a, edist (f a) 0 ∂μ) := -rfl +lemma norm_to_L1 (f : α →ₛ E) (hf : integrable f μ) : + ∥to_L1 f hf∥ = ennreal.to_real (∫⁻ a, edist (f a) 0 ∂μ) := +by simp [to_L1, integrable.norm_to_L1] -end of_simple_func +end to_L1 section to_simple_func -/-- Find a representative of a `l1.simple_func`. -/ +/-- Find a representative of a `L1.simple_func`. -/ def to_simple_func (f : α →₁ₛ[μ] E) : α →ₛ E := classical.some f.2 -/-- `f.to_simple_func` is measurable. -/ -protected lemma measurable (f : α →₁ₛ[μ] E) : measurable f.to_simple_func := -f.to_simple_func.measurable +/-- `(to_simple_func f)` is measurable. -/ +protected lemma measurable (f : α →₁ₛ[μ] E) : measurable (to_simple_func f) := +(to_simple_func f).measurable -protected lemma ae_measurable (f : α →₁ₛ[μ] E) : ae_measurable f.to_simple_func μ := -f.measurable.ae_measurable +protected lemma ae_measurable (f : α →₁ₛ[μ] E) : ae_measurable (to_simple_func f) μ := +(simple_func.measurable f).ae_measurable -/-- `f.to_simple_func` is integrable. -/ -protected lemma integrable (f : α →₁ₛ[μ] E) : integrable f.to_simple_func μ := -let h := classical.some_spec f.2 in (integrable_mk f.ae_measurable).1 $ h.symm ▸ (f : α →₁[μ] E).2 +/-- `to_simple_func f` is integrable. -/ +protected lemma integrable (f : α →₁ₛ[μ] E) : integrable (to_simple_func f) μ := +begin + apply (integrable_mk (simple_func.ae_measurable f)).1, + convert integrable_coe_fn f.val, + exact classical.some_spec f.2 +end -lemma of_simple_func_to_simple_func (f : α →₁ₛ[μ] E) : - of_simple_func (f.to_simple_func) f.integrable = f := +lemma to_L1_to_simple_func (f : α →₁ₛ[μ] E) : + to_L1 (to_simple_func f) (simple_func.integrable f) = f := by { rw ← simple_func.eq_iff', exact classical.some_spec f.2 } -lemma to_simple_func_of_simple_func (f : α →ₛ E) (hfi : integrable f μ) : - (of_simple_func f hfi).to_simple_func =ᵐ[μ] f := -by { rw ← mk_eq_mk, exact classical.some_spec (of_simple_func f hfi).2 } +lemma to_simple_func_to_L1 (f : α →ₛ E) (hfi : integrable f μ) : + to_simple_func (to_L1 f hfi) =ᵐ[μ] f := +by { rw ← mk_eq_mk, exact classical.some_spec (to_L1 f hfi).2 } -lemma to_simple_func_eq_to_fun (f : α →₁ₛ[μ] E) : f.to_simple_func =ᵐ[μ] f := +lemma to_simple_func_eq_to_fun (f : α →₁ₛ[μ] E) : to_simple_func f =ᵐ[μ] f := begin - rw [← of_fun_eq_of_fun f.to_simple_func f f.integrable (f : α →₁[μ] E).integrable, ← l1.eq_iff], - simp only [of_fun_eq_mk, ← coe_coe, mk_to_fun], - exact classical.some_spec f.coe_prop + simp_rw [← integrable.to_L1_eq_to_L1_iff (to_simple_func f) f (simple_func.integrable f) + (integrable_coe_fn ↑f), subtype.ext_iff], + convert classical.some_spec f.coe_prop, + exact integrable.to_L1_coe_fn _ _, end -variables (α E) -lemma zero_to_simple_func : (0 : α →₁ₛ[μ] E).to_simple_func =ᵐ[μ] 0 := +variables (E μ) +lemma zero_to_simple_func : to_simple_func (0 : α →₁ₛ[μ] E) =ᵐ[μ] 0 := begin - filter_upwards [to_simple_func_eq_to_fun (0 : α →₁ₛ[μ] E), l1.zero_to_fun α E], + filter_upwards [to_simple_func_eq_to_fun (0 : α →₁ₛ[μ] E), Lp.coe_fn_zero E 1 μ], assume a h₁ h₂, rwa h₁, end -variables {α E} +variables {E μ} lemma add_to_simple_func (f g : α →₁ₛ[μ] E) : - (f + g).to_simple_func =ᵐ[μ] f.to_simple_func + g.to_simple_func := + to_simple_func (f + g) =ᵐ[μ] to_simple_func f + to_simple_func g := begin filter_upwards [to_simple_func_eq_to_fun (f + g), to_simple_func_eq_to_fun f, - to_simple_func_eq_to_fun g, l1.add_to_fun (f : α →₁[μ] E) g], + to_simple_func_eq_to_fun g, Lp.coe_fn_add (f : α →₁[μ] E) g], assume a, simp only [← coe_coe, coe_add, pi.add_apply], iterate 4 { assume h, rw h } end -lemma neg_to_simple_func (f : α →₁ₛ[μ] E) : (-f).to_simple_func =ᵐ[μ] - f.to_simple_func := +lemma neg_to_simple_func (f : α →₁ₛ[μ] E) : to_simple_func (-f) =ᵐ[μ] - to_simple_func f := begin filter_upwards [to_simple_func_eq_to_fun (-f), to_simple_func_eq_to_fun f, - l1.neg_to_fun (f : α →₁[μ] E)], + Lp.coe_fn_neg (f : α →₁[μ] E)], assume a, simp only [pi.neg_apply, coe_neg, ← coe_coe], repeat { assume h, rw h } end lemma sub_to_simple_func (f g : α →₁ₛ[μ] E) : - (f - g).to_simple_func =ᵐ[μ] f.to_simple_func - g.to_simple_func := + to_simple_func (f - g) =ᵐ[μ] to_simple_func f - to_simple_func g := begin filter_upwards [to_simple_func_eq_to_fun (f - g), to_simple_func_eq_to_fun f, - to_simple_func_eq_to_fun g, l1.sub_to_fun (f : α →₁[μ] E) g], + to_simple_func_eq_to_fun g, Lp.coe_fn_sub (f : α →₁[μ] E) g], assume a, simp only [coe_sub, pi.sub_apply, ← coe_coe], repeat { assume h, rw h } @@ -620,44 +604,44 @@ end variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 E] lemma smul_to_simple_func (k : 𝕜) (f : α →₁ₛ[μ] E) : - (k • f).to_simple_func =ᵐ[μ] k • f.to_simple_func := + to_simple_func (k • f) =ᵐ[μ] k • to_simple_func f := begin filter_upwards [to_simple_func_eq_to_fun (k • f), to_simple_func_eq_to_fun f, - l1.smul_to_fun k (f : α →₁[μ] E)], + Lp.coe_fn_smul k (f : α →₁[μ] E)], assume a, simp only [pi.smul_apply, coe_smul, ← coe_coe], repeat { assume h, rw h } end lemma lintegral_edist_to_simple_func_lt_top (f g : α →₁ₛ[μ] E) : - ∫⁻ (x : α), edist ((to_simple_func f) x) ((to_simple_func g) x) ∂μ < ∞ := + ∫⁻ (x : α), edist (to_simple_func f x) (to_simple_func g x) ∂μ < ∞ := begin rw lintegral_rw₂ (to_simple_func_eq_to_fun f) (to_simple_func_eq_to_fun g), - exact lintegral_edist_to_fun_lt_top _ _ + exact lintegral_edist_lt_top (integrable_coe_fn _) (integrable_coe_fn _) end lemma dist_to_simple_func (f g : α →₁ₛ[μ] E) : dist f g = - ennreal.to_real (∫⁻ x, edist (f.to_simple_func x) (g.to_simple_func x) ∂μ) := + ennreal.to_real (∫⁻ x, edist (to_simple_func f x) (to_simple_func g x) ∂μ) := begin - rw [dist_eq, l1.dist_to_fun, ennreal.to_real_eq_to_real], + rw [dist_eq, L1.dist_def, ennreal.to_real_eq_to_real], { rw lintegral_rw₂, repeat { exact ae_eq_symm (to_simple_func_eq_to_fun _) } }, - { exact l1.lintegral_edist_to_fun_lt_top _ _ }, + { exact lintegral_edist_lt_top (integrable_coe_fn _) (integrable_coe_fn _) }, { exact lintegral_edist_to_simple_func_lt_top _ _ } end lemma norm_to_simple_func (f : α →₁ₛ[μ] E) : ∥f∥ = ennreal.to_real (∫⁻ (a : α), nnnorm ((to_simple_func f) a) ∂μ) := calc ∥f∥ = - ennreal.to_real (∫⁻x, edist (f.to_simple_func x) ((0 : α →₁ₛ[μ] E).to_simple_func x) ∂μ) : + ennreal.to_real (∫⁻x, edist ((to_simple_func f) x) (to_simple_func (0 : α →₁ₛ[μ] E) x) ∂μ) : begin rw [← dist_zero_right, dist_to_simple_func] end -... = ennreal.to_real (∫⁻ (x : α), (coe ∘ nnnorm) (f.to_simple_func x) ∂μ) : +... = ennreal.to_real (∫⁻ (x : α), (coe ∘ nnnorm) ((to_simple_func f) x) ∂μ) : begin rw lintegral_nnnorm_eq_lintegral_edist, have : ∫⁻ x, edist ((to_simple_func f) x) ((to_simple_func (0 : α →₁ₛ[μ] E)) x) ∂μ = ∫⁻ x, edist ((to_simple_func f) x) 0 ∂μ, - { refine lintegral_congr_ae ((zero_to_simple_func α E).mono (λ a h, _)), + { refine lintegral_congr_ae ((zero_to_simple_func E μ).mono (λ a h, _)), rw [h, pi.zero_apply] }, rw [ennreal.to_real_eq_to_real], { exact this }, @@ -665,20 +649,17 @@ begin { rw ← this, exact lintegral_edist_to_simple_func_lt_top _ _ } end -lemma norm_eq_integral (f : α →₁ₛ[μ] E) : ∥f∥ = (f.to_simple_func.map norm).integral μ := --- calc ∥f∥ = ennreal.to_real (∫⁻ (x : α), (coe ∘ nnnorm) (f.to_simple_func x) ∂μ) : --- by { rw norm_to_simple_func } --- ... = (f.to_simple_func.map norm).integral μ : +lemma norm_eq_integral (f : α →₁ₛ[μ] E) : ∥f∥ = ((to_simple_func f).map norm).integral μ := begin rw [norm_to_simple_func, simple_func.integral_eq_lintegral], { simp only [simple_func.map_apply, of_real_norm_eq_coe_nnnorm] }, - { exact f.integrable.norm }, + { exact (simple_func.integrable f).norm }, { exact eventually_of_forall (λ x, norm_nonneg _) } end end to_simple_func -section coe_to_l1 +section coe_to_L1 protected lemma uniform_continuous : uniform_continuous (coe : (α →₁ₛ[μ] E) → (α →₁[μ] E)) := uniform_continuous_comap @@ -692,16 +673,13 @@ simple_func.uniform_embedding.to_uniform_inducing protected lemma dense_embedding : dense_embedding (coe : (α →₁ₛ[μ] E) → (α →₁[μ] E)) := begin apply simple_func.uniform_embedding.dense_embedding, - rintros ⟨f, hfi⟩, - have A : ae_eq_fun.mk f f.ae_measurable = f := mk_coe_fn _, + assume f, rw mem_closure_iff_seq_limit, - have hfi' := integrable_coe_fn.2 hfi, - refine ⟨λ n, ↑(of_simple_func (simple_func.approx_on f f.measurable univ 0 trivial n) - (simple_func.integrable_approx_on_univ f.measurable hfi' n)), λ n, mem_range_self _, _⟩, - simp only [tendsto_iff_edist_tendsto_0, of_fun_eq_mk, subtype.coe_mk, edist_eq], - dsimp, - conv in (edist _ _) { congr, skip, rw ← A }, - simpa only [edist_mk_mk] using simple_func.tendsto_approx_on_univ_l1_edist f.measurable hfi' + have hfi' : integrable f μ := integrable_coe_fn f, + refine ⟨λ n, ↑(to_L1 (simple_func.approx_on f (Lp.measurable f) univ 0 trivial n) + (simple_func.integrable_approx_on_univ (Lp.measurable f) hfi' n)), λ n, mem_range_self _, _⟩, + convert simple_func.tendsto_approx_on_univ_L1 (Lp.measurable f) hfi', + rw integrable.to_L1_coe_fn end protected lemma dense_inducing : dense_inducing (coe : (α →₁ₛ[μ] E) → (α →₁[μ] E)) := @@ -715,24 +693,24 @@ variables (𝕜 : Type*) [normed_field 𝕜] [normed_space 𝕜 E] variables (α E) /-- The uniform and dense embedding of L1 simple functions into L1 functions. -/ -def coe_to_l1 : (α →₁ₛ[μ] E) →L[𝕜] (α →₁[μ] E) := +def coe_to_L1 : (α →₁ₛ[μ] E) →L[𝕜] (α →₁[μ] E) := { to_fun := (coe : (α →₁ₛ[μ] E) → (α →₁[μ] E)), map_add' := λf g, rfl, map_smul' := λk f, rfl, - cont := l1.simple_func.uniform_continuous.continuous, } + cont := L1.simple_func.uniform_continuous.continuous, } variables {α E 𝕜} -end coe_to_l1 +end coe_to_L1 section pos_part /-- Positive part of a simple function in L1 space. -/ -def pos_part (f : α →₁ₛ[μ] ℝ) : α →₁ₛ[μ] ℝ := ⟨l1.pos_part (f : α →₁[μ] ℝ), +def pos_part (f : α →₁ₛ[μ] ℝ) : α →₁ₛ[μ] ℝ := ⟨Lp.pos_part (f : α →₁[μ] ℝ), begin rcases f with ⟨f, s, hsf⟩, use s.pos_part, - simp only [subtype.coe_mk, l1.coe_pos_part, ← hsf, ae_eq_fun.pos_part_mk, simple_func.pos_part, + simp only [subtype.coe_mk, Lp.coe_pos_part, ← hsf, ae_eq_fun.pos_part_mk, simple_func.pos_part, simple_func.coe_map] end ⟩ @@ -740,10 +718,10 @@ end ⟩ def neg_part (f : α →₁ₛ[μ] ℝ) : α →₁ₛ[μ] ℝ := pos_part (-f) @[norm_cast] -lemma coe_pos_part (f : α →₁ₛ[μ] ℝ) : (f.pos_part : α →₁[μ] ℝ) = (f : α →₁[μ] ℝ).pos_part := rfl +lemma coe_pos_part (f : α →₁ₛ[μ] ℝ) : (pos_part f : α →₁[μ] ℝ) = Lp.pos_part (f : α →₁[μ] ℝ) := rfl @[norm_cast] -lemma coe_neg_part (f : α →₁ₛ[μ] ℝ) : (f.neg_part : α →₁[μ] ℝ) = (f : α →₁[μ] ℝ).neg_part := rfl +lemma coe_neg_part (f : α →₁ₛ[μ] ℝ) : (neg_part f : α →₁[μ] ℝ) = Lp.neg_part (f : α →₁[μ] ℝ) := rfl end pos_part @@ -752,47 +730,50 @@ section simple_func_integral variables [normed_space ℝ E] -/-- The Bochner integral over simple functions in l1 space. -/ -def integral (f : α →₁ₛ[μ] E) : E := (f.to_simple_func).integral μ +/-- The Bochner integral over simple functions in L1 space. -/ +def integral (f : α →₁ₛ[μ] E) : E := ((to_simple_func f)).integral μ -lemma integral_eq_integral (f : α →₁ₛ[μ] E) : integral f = (f.to_simple_func).integral μ := rfl +lemma integral_eq_integral (f : α →₁ₛ[μ] E) : integral f = ((to_simple_func f)).integral μ := rfl -lemma integral_eq_lintegral {f : α →₁ₛ[μ] ℝ} (h_pos : 0 ≤ᵐ[μ] f.to_simple_func) : - integral f = ennreal.to_real (∫⁻ a, ennreal.of_real (f.to_simple_func a) ∂μ) := -by rw [integral, simple_func.integral_eq_lintegral f.integrable h_pos] +lemma integral_eq_lintegral {f : α →₁ₛ[μ] ℝ} (h_pos : 0 ≤ᵐ[μ] (to_simple_func f)) : + integral f = ennreal.to_real (∫⁻ a, ennreal.of_real ((to_simple_func f) a) ∂μ) := +by rw [integral, simple_func.integral_eq_lintegral (simple_func.integrable f) h_pos] -lemma integral_congr {f g : α →₁ₛ[μ] E} (h : f.to_simple_func =ᵐ[μ] g.to_simple_func) : +lemma integral_congr {f g : α →₁ₛ[μ] E} (h : to_simple_func f =ᵐ[μ] to_simple_func g) : integral f = integral g := -simple_func.integral_congr f.integrable h +simple_func.integral_congr (simple_func.integrable f) h lemma integral_add (f g : α →₁ₛ[μ] E) : integral (f + g) = integral f + integral g := begin simp only [integral], - rw ← simple_func.integral_add f.integrable g.integrable, - apply measure_theory.simple_func.integral_congr (f + g).integrable, + rw ← simple_func.integral_add (simple_func.integrable f) (simple_func.integrable g), + apply measure_theory.simple_func.integral_congr (simple_func.integrable (f + g)), apply add_to_simple_func end lemma integral_smul (r : ℝ) (f : α →₁ₛ[μ] E) : integral (r • f) = r • integral f := begin simp only [integral], - rw ← simple_func.integral_smul _ f.integrable, - apply measure_theory.simple_func.integral_congr (r • f).integrable, + rw ← simple_func.integral_smul _ (simple_func.integrable f), + apply measure_theory.simple_func.integral_congr (simple_func.integrable (r • f)), apply smul_to_simple_func end -lemma norm_integral_le_norm (f : α →₁ₛ[μ] E) : ∥ integral f ∥ ≤ ∥f∥ := +lemma norm_integral_le_norm (f : α →₁ₛ[μ] E) : ∥integral f∥ ≤ ∥f∥ := begin rw [integral, norm_eq_integral], - exact f.to_simple_func.norm_integral_le_integral_norm f.integrable + exact (to_simple_func f).norm_integral_le_integral_norm (simple_func.integrable f) end -/-- The Bochner integral over simple functions in l1 space as a continuous linear map. -/ +variables (α E μ) +/-- The Bochner integral over simple functions in L1 space as a continuous linear map. -/ def integral_clm : (α →₁ₛ[μ] E) →L[ℝ] E := linear_map.mk_continuous ⟨integral, integral_add, integral_smul⟩ 1 (λf, le_trans (norm_integral_le_norm _) $ by rw one_mul) -local notation `Integral` := @integral_clm α E _ _ _ _ _ μ _ +variables {α E μ} + +local notation `Integral` := integral_clm α E μ open continuous_linear_map @@ -802,11 +783,11 @@ linear_map.mk_continuous_norm_le _ (zero_le_one) _ section pos_part lemma pos_part_to_simple_func (f : α →₁ₛ[μ] ℝ) : - f.pos_part.to_simple_func =ᵐ[μ] f.to_simple_func.pos_part := + to_simple_func (pos_part f) =ᵐ[μ] (to_simple_func f).pos_part := begin - have eq : ∀ a, f.to_simple_func.pos_part a = max (f.to_simple_func a) 0 := λa, rfl, - have ae_eq : ∀ᵐ a ∂μ, f.pos_part.to_simple_func a = max (f.to_simple_func a) 0, - { filter_upwards [to_simple_func_eq_to_fun f.pos_part, pos_part_to_fun (f : α →₁[μ] ℝ), + have eq : ∀ a, (to_simple_func f).pos_part a = max ((to_simple_func f) a) 0 := λa, rfl, + have ae_eq : ∀ᵐ a ∂μ, to_simple_func (pos_part f) a = max ((to_simple_func f) a) 0, + { filter_upwards [to_simple_func_eq_to_fun (pos_part f), Lp.coe_fn_pos_part (f : α →₁[μ] ℝ), to_simple_func_eq_to_fun f], assume a h₁ h₂ h₃, rw [h₁, ← coe_coe, coe_pos_part, h₂, coe_coe, ← h₃] }, @@ -815,7 +796,7 @@ begin end lemma neg_part_to_simple_func (f : α →₁ₛ[μ] ℝ) : - f.neg_part.to_simple_func =ᵐ[μ] f.to_simple_func.neg_part := + to_simple_func (neg_part f) =ᵐ[μ] (to_simple_func f).neg_part := begin rw [simple_func.neg_part, measure_theory.simple_func.neg_part], filter_upwards [pos_part_to_simple_func (-f), neg_to_simple_func f], @@ -826,38 +807,39 @@ begin refl end -lemma integral_eq_norm_pos_part_sub (f : α →₁ₛ[μ] ℝ) : f.integral = ∥f.pos_part∥ - ∥f.neg_part∥ := +lemma integral_eq_norm_pos_part_sub (f : α →₁ₛ[μ] ℝ) : + integral f = ∥pos_part f∥ - ∥neg_part f∥ := begin -- Convert things in `L¹` to their `simple_func` counterpart - have ae_eq₁ : f.to_simple_func.pos_part =ᵐ[μ] (f.pos_part).to_simple_func.map norm, + have ae_eq₁ : (to_simple_func f).pos_part =ᵐ[μ] (to_simple_func (pos_part f)).map norm, { filter_upwards [pos_part_to_simple_func f], assume a h, rw [simple_func.map_apply, h], conv_lhs { rw [← simple_func.pos_part_map_norm, simple_func.map_apply] } }, -- Convert things in `L¹` to their `simple_func` counterpart - have ae_eq₂ : f.to_simple_func.neg_part =ᵐ[μ] (f.neg_part).to_simple_func.map norm, + have ae_eq₂ : (to_simple_func f).neg_part =ᵐ[μ] (to_simple_func (neg_part f)).map norm, { filter_upwards [neg_part_to_simple_func f], assume a h, rw [simple_func.map_apply, h], conv_lhs { rw [← simple_func.neg_part_map_norm, simple_func.map_apply] } }, -- Convert things in `L¹` to their `simple_func` counterpart - have ae_eq : ∀ᵐ a ∂μ, f.to_simple_func.pos_part a - f.to_simple_func.neg_part a = - (f.pos_part).to_simple_func.map norm a - (f.neg_part).to_simple_func.map norm a, + have ae_eq : ∀ᵐ a ∂μ, (to_simple_func f).pos_part a - (to_simple_func f).neg_part a = + (to_simple_func (pos_part f)).map norm a - (to_simple_func (neg_part f)).map norm a, { filter_upwards [ae_eq₁, ae_eq₂], assume a h₁ h₂, rw [h₁, h₂] }, rw [integral, norm_eq_integral, norm_eq_integral, ← simple_func.integral_sub], - { show f.to_simple_func.integral μ = - ((f.pos_part.to_simple_func).map norm - f.neg_part.to_simple_func.map norm).integral μ, - apply measure_theory.simple_func.integral_congr f.integrable, + { show (to_simple_func f).integral μ = + ((to_simple_func (pos_part f)).map norm - (to_simple_func (neg_part f)).map norm).integral μ, + apply measure_theory.simple_func.integral_congr (simple_func.integrable f), filter_upwards [ae_eq₁, ae_eq₂], assume a h₁ h₂, show _ = _ - _, rw [← h₁, ← h₂], - have := f.to_simple_func.pos_part_sub_neg_part, + have := (to_simple_func f).pos_part_sub_neg_part, conv_lhs {rw ← this}, refl }, - { exact f.integrable.max_zero.congr ae_eq₁ }, - { exact f.integrable.neg.max_zero.congr ae_eq₂ } + { exact (simple_func.integrable f).max_zero.congr ae_eq₁ }, + { exact (simple_func.integrable f).neg.max_zero.congr ae_eq₂ } end end pos_part @@ -867,29 +849,32 @@ end simple_func_integral end simple_func open simple_func +local notation `Integral` := @integral_clm α E _ _ _ _ _ μ _ + variables [normed_space ℝ E] [normed_space ℝ F] [complete_space E] -section integration_in_l1 +section integration_in_L1 -local notation `to_l1` := coe_to_l1 α E ℝ +local notation `to_L1` := coe_to_L1 α E ℝ local attribute [instance] simple_func.normed_group simple_func.normed_space open continuous_linear_map -/-- The Bochner integral in l1 space as a continuous linear map. -/ +/-- The Bochner integral in L1 space as a continuous linear map. -/ def integral_clm : (α →₁[μ] E) →L[ℝ] E := - integral_clm.extend to_l1 simple_func.dense_range simple_func.uniform_inducing +(integral_clm α E μ).extend + to_L1 simple_func.dense_range simple_func.uniform_inducing -/-- The Bochner integral in l1 space -/ +/-- The Bochner integral in L1 space -/ def integral (f : α →₁[μ] E) : E := integral_clm f lemma integral_eq (f : α →₁[μ] E) : integral f = integral_clm f := rfl -@[norm_cast] lemma simple_func.integral_l1_eq_integral (f : α →₁ₛ[μ] E) : - integral (f : α →₁[μ] E) = f.integral := +@[norm_cast] lemma simple_func.integral_L1_eq_integral (f : α →₁ₛ[μ] E) : + integral (f : α →₁[μ] E) = (simple_func.integral f) := uniformly_extend_of_ind simple_func.uniform_inducing simple_func.dense_range - simple_func.integral_clm.uniform_continuous _ + (simple_func.integral_clm α E μ).uniform_continuous _ variables (α E) @[simp] lemma integral_zero : integral (0 : α →₁[μ] E) = 0 := @@ -924,20 +909,23 @@ calc ∥integral f∥ = ∥Integral f∥ : rfl ... = ∥f∥ : one_mul _ @[continuity] -lemma continuous_integral : continuous (λ (f : α →₁[μ] E), f.integral) := -by simp [l1.integral, l1.integral_clm.continuous] +lemma continuous_integral : continuous (λ (f : α →₁[μ] E), integral f) := +by simp [L1.integral, L1.integral_clm.continuous] section pos_part -lemma integral_eq_norm_pos_part_sub (f : α →₁[μ] ℝ) : integral f = ∥pos_part f∥ - ∥neg_part f∥ := +local attribute [instance] fact_one_le_one_ennreal + +lemma integral_eq_norm_pos_part_sub (f : α →₁[μ] ℝ) : + integral f = ∥Lp.pos_part f∥ - ∥Lp.neg_part f∥ := begin -- Use `is_closed_property` and `is_closed_eq` refine @is_closed_property _ _ _ (coe : (α →₁ₛ[μ] ℝ) → (α →₁[μ] ℝ)) - (λ f : α →₁[μ] ℝ, integral f = ∥pos_part f∥ - ∥neg_part f∥) - l1.simple_func.dense_range (is_closed_eq _ _) _ f, + (λ f : α →₁[μ] ℝ, integral f = ∥Lp.pos_part f∥ - ∥Lp.neg_part f∥) + L1.simple_func.dense_range (is_closed_eq _ _) _ f, { exact cont _ }, - { refine continuous.sub (continuous_norm.comp l1.continuous_pos_part) - (continuous_norm.comp l1.continuous_neg_part) }, + { refine continuous.sub (continuous_norm.comp Lp.continuous_pos_part) + (continuous_norm.comp Lp.continuous_neg_part) }, -- Show that the property holds for all simple functions in the `L¹` space. { assume s, norm_cast, @@ -947,9 +935,9 @@ end end pos_part -end integration_in_l1 +end integration_in_L1 -end l1 +end L1 variables [normed_group E] [second_countable_topology E] [normed_space ℝ E] [complete_space E] [measurable_space E] [borel_space E] @@ -958,7 +946,7 @@ variables [normed_group E] [second_countable_topology E] [normed_space ℝ E] [c /-- The Bochner integral -/ def integral (μ : measure α) (f : α → E) : E := -if hf : integrable f μ then (l1.of_fun f hf).integral else 0 +if hf : integrable f μ then L1.integral (hf.to_L1 f) else 0 /-! In the notation for integrals, an expression like `∫ x, g ∥x∥ ∂μ` will not be parsed correctly, and needs parentheses. We do not set the binding power of `r` to `0`, because then @@ -975,11 +963,11 @@ open continuous_linear_map measure_theory.simple_func variables {f g : α → E} {μ : measure α} lemma integral_eq (f : α → E) (hf : integrable f μ) : - ∫ a, f a ∂μ = (l1.of_fun f hf).integral := + ∫ a, f a ∂μ = L1.integral (hf.to_L1 f) := dif_pos hf -lemma l1.integral_eq_integral (f : α →₁[μ] E) : f.integral = ∫ a, f a ∂μ := -by rw [integral_eq, l1.of_fun_to_fun] +lemma L1.integral_eq_integral (f : α →₁[μ] E) : L1.integral f = ∫ a, f a ∂μ := +by rw [integral_eq _ (L1.integrable_coe_fn f), integrable.to_L1_coe_fn] lemma integral_undef (h : ¬ integrable f μ) : ∫ a, f a ∂μ = 0 := dif_neg h @@ -990,7 +978,7 @@ integral_undef $ not_and_of_not_left _ h variables (α E) lemma integral_zero : ∫ a : α, (0:E) ∂μ = 0 := -by rw [integral_eq, l1.of_fun_zero, l1.integral_zero] +by { rw [integral_eq _ (integrable_zero α E μ)], exact L1.integral_zero _ _ } @[simp] lemma integral_zero' : integral μ (0 : α → E) = 0 := integral_zero α E @@ -999,8 +987,11 @@ variables {α E} lemma integral_add (hf : integrable f μ) (hg : integrable g μ) : ∫ a, f a + g a ∂μ = ∫ a, f a ∂μ + ∫ a, g a ∂μ := -by { rw [integral_eq, integral_eq f hf, integral_eq g hg, ← l1.integral_add, ← l1.of_fun_add], - refl } +begin + rw [integral_eq, integral_eq f hf, integral_eq g hg, ← L1.integral_add], + { refl }, + { exact hf.add hg } +end lemma integral_add' (hf : integrable f μ) (hg : integrable g μ) : ∫ a, (f + g) a ∂μ = ∫ a, f a ∂μ + ∫ a, g a ∂μ := @@ -1009,7 +1000,7 @@ integral_add hf hg lemma integral_neg (f : α → E) : ∫ a, -f a ∂μ = - ∫ a, f a ∂μ := begin by_cases hf : integrable f μ, - { rw [integral_eq f hf, integral_eq (λa, - f a) hf.neg, ← l1.integral_neg, ← l1.of_fun_neg], + { rw [integral_eq f hf, integral_eq (λa, - f a) hf.neg, ← L1.integral_neg], refl }, { rw [integral_undef hf, integral_undef, neg_zero], rwa [← integrable_neg_iff] at hf } end @@ -1028,7 +1019,7 @@ integral_sub hf hg lemma integral_smul (r : ℝ) (f : α → E) : ∫ a, r • (f a) ∂μ = r • ∫ a, f a ∂μ := begin by_cases hf : integrable f μ, - { rw [integral_eq f hf, integral_eq (λa, r • (f a)), l1.of_fun_smul, l1.integral_smul] }, + { rw [integral_eq f hf, integral_eq (λa, r • (f a)), integrable.to_L1_smul, L1.integral_smul] }, { by_cases hr : r = 0, { simp only [hr, measure_theory.integral_zero, zero_smul] }, have hf' : ¬ integrable (λ x, r • f x) μ, @@ -1049,24 +1040,25 @@ lemma integral_congr_ae (h : f =ᵐ[μ] g) : ∫ a, f a ∂μ = ∫ a, g a ∂μ begin by_cases hfi : integrable f μ, { have hgi : integrable g μ := hfi.congr h, - rw [integral_eq f hfi, integral_eq g hgi, (l1.of_fun_eq_of_fun f g hfi hgi).2 h] }, + rw [integral_eq f hfi, integral_eq g hgi, (integrable.to_L1_eq_to_L1_iff f g hfi hgi).2 h] }, { have hgi : ¬ integrable g μ, { rw integrable_congr h at hfi, exact hfi }, rw [integral_undef hfi, integral_undef hgi] }, end -@[simp] lemma l1.integral_of_fun_eq_integral {f : α → E} (hf : integrable f μ) : - ∫ a, (l1.of_fun f hf) a ∂μ = ∫ a, f a ∂μ := -integral_congr_ae (l1.to_fun_of_fun f hf) +@[simp] lemma L1.integral_of_fun_eq_integral {f : α → E} (hf : integrable f μ) : + ∫ a, (hf.to_L1 f) a ∂μ = ∫ a, f a ∂μ := +integral_congr_ae $ by simp [integrable.coe_fn_to_L1] @[continuity] lemma continuous_integral : continuous (λ (f : α →₁[μ] E), ∫ a, f a ∂μ) := -by { simp only [← l1.integral_eq_integral], exact l1.continuous_integral } +by { simp only [← L1.integral_eq_integral], exact L1.continuous_integral } lemma norm_integral_le_lintegral_norm (f : α → E) : ∥∫ a, f a ∂μ∥ ≤ ennreal.to_real (∫⁻ a, (ennreal.of_real ∥f a∥) ∂μ) := begin by_cases hf : integrable f μ, - { rw [integral_eq f hf, ← l1.norm_of_fun_eq_lintegral_norm f hf], exact l1.norm_integral_le _ }, + { rw [integral_eq f hf, ← integrable.norm_to_L1_eq_lintegral_norm f hf], + exact L1.norm_integral_le _ }, { rw [integral_undef hf, norm_zero], exact to_real_nonneg } end @@ -1102,7 +1094,7 @@ lemma integrable.tendsto_set_integral_nhds_zero {ι} {f : α → E} hf.2.tendsto_set_integral_nhds_zero hs /-- If `F i → f` in `L1`, then `∫ x, F i x ∂μ → ∫ x, f x∂μ`. -/ -lemma tendsto_integral_of_l1 {ι} (f : α → E) (hfi : integrable f μ) +lemma tendsto_integral_of_L1 {ι} (f : α → E) (hfi : integrable f μ) {F : ι → α → E} {l : filter ι} (hFi : ∀ᶠ i in l, integrable (F i) μ) (hF : tendsto (λ i, ∫⁻ x, edist (F i x) (f x) ∂μ) l (𝓝 0)) : tendsto (λ i, ∫ x, F i x ∂μ) l (𝓝 $ ∫ x, f x ∂μ) := @@ -1184,33 +1176,36 @@ lemma integral_eq_lintegral_max_sub_lintegral_min {f : α → ℝ} (hf : integra ∫ a, f a ∂μ = ennreal.to_real (∫⁻ a, (ennreal.of_real $ max (f a) 0) ∂μ) - ennreal.to_real (∫⁻ a, (ennreal.of_real $ - min (f a) 0) ∂μ) := -let f₁ : α →₁[μ] ℝ := l1.of_fun f hf in +let f₁ := hf.to_L1 f in -- Go to the `L¹` space -have eq₁ : ennreal.to_real (∫⁻ a, (ennreal.of_real $ max (f a) 0) ∂μ) = ∥l1.pos_part f₁∥ := +have eq₁ : ennreal.to_real (∫⁻ a, (ennreal.of_real $ max (f a) 0) ∂μ) = ∥Lp.pos_part f₁∥ := begin - rw l1.norm_eq_norm_to_fun, + rw L1.norm_def, congr' 1, apply lintegral_congr_ae, - filter_upwards [l1.pos_part_to_fun f₁, l1.to_fun_of_fun f hf], + filter_upwards [Lp.coe_fn_pos_part f₁, hf.coe_fn_to_L1], assume a h₁ h₂, - rw [h₁, h₂, real.norm_eq_abs, abs_of_nonneg], - exact le_max_right _ _ + rw [h₁, h₂, ennreal.of_real, nnnorm], + congr' 1, + apply nnreal.eq, + simp [real.norm_of_nonneg, le_max_right, nnreal.coe_of_real] end, -- Go to the `L¹` space -have eq₂ : ennreal.to_real (∫⁻ a, (ennreal.of_real $ -min (f a) 0) ∂μ) = ∥l1.neg_part f₁∥ := +have eq₂ : ennreal.to_real (∫⁻ a, (ennreal.of_real $ -min (f a) 0) ∂μ) = ∥Lp.neg_part f₁∥ := begin - rw l1.norm_eq_norm_to_fun, + rw L1.norm_def, congr' 1, apply lintegral_congr_ae, - filter_upwards [l1.neg_part_to_fun_eq_min f₁, l1.to_fun_of_fun f hf], + filter_upwards [Lp.coe_fn_neg_part f₁, hf.coe_fn_to_L1], assume a h₁ h₂, - rw [h₁, h₂, real.norm_eq_abs, abs_of_nonneg], - rw [neg_nonneg], - exact min_le_right _ _ + rw [h₁, h₂, ennreal.of_real, nnnorm], + congr' 1, + apply nnreal.eq, + simp [real.norm_of_nonneg, min_le_right, nnreal.coe_of_real, neg_nonneg], end, begin rw [eq₁, eq₂, integral, dif_pos], - exact l1.integral_eq_norm_pos_part_sub _ + exact L1.integral_eq_norm_pos_part_sub _ end lemma integral_eq_lintegral_of_nonneg_ae {f : α → ℝ} (hf : 0 ≤ᵐ[μ] f) (hfm : ae_measurable f μ) : @@ -1303,17 +1298,21 @@ section normed_group variables {H : Type*} [normed_group H] [second_countable_topology H] [measurable_space H] [borel_space H] -lemma l1.norm_eq_integral_norm (f : α →₁[μ] H) : ∥f∥ = ∫ a, ∥f a∥ ∂μ := -by rw [l1.norm_eq_norm_to_fun, - integral_eq_lintegral_of_nonneg_ae (eventually_of_forall $ by simp [norm_nonneg]) - (continuous_norm.measurable.comp_ae_measurable f.ae_measurable)] +lemma L1.norm_eq_integral_norm (f : α →₁[μ] H) : ∥f∥ = ∫ a, ∥f a∥ ∂μ := +begin + simp only [snorm, snorm', ennreal.one_to_real, ennreal.rpow_one, Lp.norm_def, + if_false, ennreal.one_ne_top, one_ne_zero, _root_.div_one], + rw integral_eq_lintegral_of_nonneg_ae (eventually_of_forall (by simp [norm_nonneg])) + (continuous_norm.measurable.comp_ae_measurable (Lp.ae_measurable f)), + simp [of_real_norm_eq_coe_nnnorm] +end -lemma l1.norm_of_fun_eq_integral_norm {f : α → H} (hf : integrable f μ) : - ∥ l1.of_fun f hf ∥ = ∫ a, ∥f a∥ ∂μ := +lemma L1.norm_of_fun_eq_integral_norm {f : α → H} (hf : integrable f μ) : + ∥hf.to_L1 f∥ = ∫ a, ∥f a∥ ∂μ := begin - rw l1.norm_eq_integral_norm, + rw L1.norm_eq_integral_norm, refine integral_congr_ae _, - apply (l1.to_fun_of_fun f hf).mono, + apply hf.coe_fn_to_L1.mono, intros a ha, simp [ha] end @@ -1371,9 +1370,9 @@ end lemma simple_func.integral_eq_integral (f : α →ₛ E) (hfi : integrable f μ) : f.integral μ = ∫ x, f x ∂μ := begin - rw [integral_eq f hfi, ← l1.simple_func.of_simple_func_eq_of_fun, - l1.simple_func.integral_l1_eq_integral, l1.simple_func.integral_eq_integral], - exact simple_func.integral_congr hfi (l1.simple_func.to_simple_func_of_simple_func _ _).symm + rw [integral_eq f hfi, ← L1.simple_func.to_L1_eq_to_L1, + L1.simple_func.integral_L1_eq_integral, L1.simple_func.integral_eq_integral], + exact simple_func.integral_congr hfi (L1.simple_func.to_simple_func_to_L1 _ _).symm end @[simp] lemma integral_const (c : E) : ∫ x : α, c ∂μ = (μ univ).to_real • c := @@ -1409,9 +1408,9 @@ lemma tendsto_integral_approx_on_univ_of_measurable begin have : tendsto (λ n, ∫ x, simple_func.approx_on f fmeas univ 0 trivial n x ∂μ) at_top (𝓝 $ ∫ x, f x ∂μ) := - tendsto_integral_of_l1 _ hf + tendsto_integral_of_L1 _ hf (eventually_of_forall $ simple_func.integrable_approx_on_univ fmeas hf) - (simple_func.tendsto_approx_on_univ_l1_edist fmeas hf), + (simple_func.tendsto_approx_on_univ_L1_edist fmeas hf), simpa only [simple_func.integral_eq_integral, simple_func.integrable_approx_on_univ fmeas hf] end @@ -1539,9 +1538,9 @@ end properties mk_simp_attribute integral_simps "Simp set for integral rules." -attribute [integral_simps] integral_neg integral_smul l1.integral_add l1.integral_sub - l1.integral_smul l1.integral_neg +attribute [integral_simps] integral_neg integral_smul L1.integral_add L1.integral_sub + L1.integral_smul L1.integral_neg -attribute [irreducible] integral l1.integral +attribute [irreducible] integral L1.integral end measure_theory diff --git a/src/measure_theory/l1_space.lean b/src/measure_theory/l1_space.lean index bb0f966f2bd95..8a264b2af7998 100644 --- a/src/measure_theory/l1_space.lean +++ b/src/measure_theory/l1_space.lean @@ -3,7 +3,8 @@ Copyright (c) 2019 Zhouhang Zhou. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Zhouhang Zhou -/ -import measure_theory.ae_eq_fun_metric +import measure_theory.lp_space + /-! # Integrable functions and `L¹` space @@ -11,13 +12,15 @@ import measure_theory.ae_eq_fun_metric In the first part of this file, the predicate `integrable` is defined and basic properties of integrable functions are proved. -In the second part, the space `L¹` of equivalence classes of integrable functions under the relation -of being almost everywhere equal is defined as a subspace of the space `L⁰`. See the file -`src/measure_theory/ae_eq_fun.lean` for information on `L⁰` space. +Such a predicate is already available under the name `mem_ℒp 1`. We give a direct definition which +is easier to use, and show that it is equivalent to `mem_ℒp 1` + +In the second part, we establish an API between `integrable` and the space `L¹` of equivalence +classes of integrable functions, already defined as a special case of `L^p` spaces for `p = 1`. ## Notation -* `α →₁ β` is the type of `L¹` space, where `α` is a `measure_space` and `β` is a `normed_group` +* `α →₁[μ] β` is the type of `L¹` space, where `α` is a `measure_space` and `β` is a `normed_group` with a `second_countable_topology`. `f : α →ₘ β` is a "function" in `L¹`. In comments, `[f]` is also used to denote an `L¹` function. @@ -31,21 +34,8 @@ of being almost everywhere equal is defined as a subspace of the space `L⁰`. S * If `β` is moreover a `measurable_space` then `f` is called `integrable` if `f` is `measurable` and `has_finite_integral f` holds. -* The space `L¹` is defined as a subspace of `L⁰` : - An `ae_eq_fun` `[f] : α →ₘ β` is in the space `L¹` if `edist [f] 0 < ∞`, which means - `(∫⁻ a, edist (f a) 0) < ∞` if we expand the definition of `edist` in `L⁰`. - -## Main statements - -`L¹`, as a subspace, inherits most of the structures of `L⁰`. - ## Implementation notes -Maybe `integrable f` should be mean `(∫⁻ a, edist (f a) 0) < ∞`, so that `integrable` and -`ae_eq_fun.integrable` are more aligned. But in the end one can use the lemma -`lintegral_nnnorm_eq_lintegral_edist : (∫⁻ a, nnnorm (f a)) = (∫⁻ a, edist (f a) 0)` to switch the -two forms. - To prove something for an arbitrary integrable function, a useful theorem is `integrable.induction` in the file `set_integral`. @@ -516,6 +506,16 @@ lemma integrable.prod_mk [opens_measurable_space β] [opens_measurable_space γ] calc max ∥f x∥ ∥g x∥ ≤ ∥f x∥ + ∥g x∥ : max_le_add_of_nonneg (norm_nonneg _) (norm_nonneg _) ... ≤ ∥(∥f x∥ + ∥g x∥)∥ : le_abs_self _⟩ +lemma mem_ℒp_one_iff_integrable {f : α → β} : mem_ℒp f 1 μ ↔ integrable f μ := +by simp_rw [integrable, has_finite_integral, mem_ℒp, + snorm_eq_snorm' one_ne_zero ennreal.one_ne_top, ennreal.one_to_real, snorm', one_div_one, + ennreal.rpow_one] + +lemma mem_ℒp.integrable [borel_space β] {q : ℝ≥0∞} (hq1 : 1 ≤ q) {f : α → β} [finite_measure μ] + (hfq : mem_ℒp f q μ) : integrable f μ := +mem_ℒp_one_iff_integrable.mp (hfq.mem_ℒp_of_exponent_le hq1) + + section pos_part /-! ### Lemmas used for defining the positive part of a `L¹` function -/ @@ -563,7 +563,6 @@ end end normed_space_over_complete_field -variables [second_countable_topology β] /-! ### The predicate `integrable` on measurable functions modulo a.e.-equality -/ @@ -571,27 +570,38 @@ namespace ae_eq_fun section -variable [opens_measurable_space β] - -/-- A class of almost everywhere equal functions is `integrable` if it has a finite distance to - the origin. It means the same thing as the predicate `integrable` over functions. -/ -def integrable (f : α →ₘ[μ] β) : Prop := f ∈ ball (0 : α →ₘ[μ] β) ∞ +/-- A class of almost everywhere equal functions is `integrable` if its function representative +is integrable. -/ +def integrable (f : α →ₘ[μ] β) : Prop := integrable f μ lemma integrable_mk {f : α → β} (hf : ae_measurable f μ ) : (integrable (mk f hf : α →ₘ[μ] β)) ↔ measure_theory.integrable f μ := -by simp [integrable, zero_def, edist_mk_mk', measure_theory.integrable, nndist_eq_nnnorm, - has_finite_integral, hf] +begin + simp [integrable], + apply integrable_congr, + exact coe_fn_mk f hf +end lemma integrable_coe_fn {f : α →ₘ[μ] β} : (measure_theory.integrable f μ) ↔ integrable f := by rw [← integrable_mk, mk_coe_fn] -lemma integrable_zero : integrable (0 : α →ₘ[μ] β) := mem_ball_self coe_lt_top +lemma integrable_zero : integrable (0 : α →ₘ[μ] β) := +(integrable_zero α β μ).congr (coe_fn_mk _ _).symm end section -variable [borel_space β] +variables [borel_space β] + +lemma integrable.neg {f : α →ₘ[μ] β} : integrable f → integrable (-f) := +induction_on f $ λ f hfm hfi, (integrable_mk _).2 ((integrable_mk hfm).1 hfi).neg + +section +variable [second_countable_topology β] + +lemma integrable_iff_mem_L1 {f : α →ₘ[μ] β} : integrable f ↔ f ∈ (α →₁[μ] β) := +by rw [← integrable_coe_fn, ← mem_ℒp_one_iff_integrable, Lp.mem_Lp_iff_mem_ℒp] lemma integrable.add {f g : α →ₘ[μ] β} : integrable f → integrable g → integrable (f + g) := begin @@ -600,17 +610,11 @@ begin exact hfi.add hgi end -lemma integrable.neg {f : α →ₘ[μ] β} : integrable f → integrable (-f) := -induction_on f $ λ f hfm hfi, (integrable_mk _).2 ((integrable_mk hfm).1 hfi).neg - lemma integrable.sub {f g : α →ₘ[μ] β} (hf : integrable f) (hg : integrable g) : integrable (f - g) := hf.add hg.neg -protected lemma is_add_subgroup : is_add_subgroup (ball (0 : α →ₘ[μ] β) ∞) := -{ zero_mem := integrable_zero, - add_mem := λ _ _, integrable.add, - neg_mem := λ _, integrable.neg } +end section normed_space variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 β] @@ -624,220 +628,53 @@ end end ae_eq_fun -/-! ### The `L¹` space of functions -/ - -variables (α β) -/-- The space of equivalence classes of integrable (and measurable) functions, where two integrable - functions are equivalent if they agree almost everywhere, i.e., they differ on a set of measure - `0`. -/ -def l1 [opens_measurable_space β] (μ : measure α) : Type* := -{f : α →ₘ[μ] β // f.integrable} - -notation α ` →₁[`:25 μ `] ` β := l1 α β μ - -variables {α β} - -namespace l1 -open ae_eq_fun -local attribute [instance] ae_eq_fun.is_add_subgroup - -section - -variable [opens_measurable_space β] - -instance : has_coe (α →₁[μ] β) (α →ₘ[μ] β) := coe_subtype -instance : has_coe_to_fun (α →₁[μ] β) := ⟨λ f, α → β, λ f, ⇑(f : α →ₘ[μ] β)⟩ - -@[simp, norm_cast] lemma coe_coe (f : α →₁[μ] β) : ⇑(f : α →ₘ[μ] β) = f := rfl - -protected lemma eq {f g : α →₁[μ] β} : (f : α →ₘ[μ] β) = (g : α →ₘ[μ] β) → f = g := subtype.eq -@[norm_cast] protected lemma eq_iff {f g : α →₁[μ] β} : (f : α →ₘ[μ] β) = (g : α →ₘ[μ] β) ↔ f = g := -iff.intro (l1.eq) (congr_arg coe) - -/- TODO : order structure of l1-/ - -/-- `L¹` space forms a `emetric_space`, with the emetric being inherited from almost everywhere - functions, i.e., `edist f g = ∫⁻ a, edist (f a) (g a)`. -/ -instance : emetric_space (α →₁[μ] β) := subtype.emetric_space - -/-- `L¹` space forms a `metric_space`, with the metric being inherited from almost everywhere - functions, i.e., `edist f g = ennreal.to_real (∫⁻ a, edist (f a) (g a))`. -/ -instance : metric_space (α →₁[μ] β) := metric_space_emetric_ball 0 ∞ - -end - -variable [borel_space β] - -instance : add_comm_group (α →₁[μ] β) := subtype.add_comm_group - -instance : inhabited (α →₁[μ] β) := ⟨0⟩ - -@[simp, norm_cast] lemma coe_zero : ((0 : α →₁[μ] β) : α →ₘ[μ] β) = 0 := rfl -@[simp, norm_cast] -lemma coe_add (f g : α →₁[μ] β) : ((f + g : α →₁[μ] β) : α →ₘ[μ] β) = f + g := rfl -@[simp, norm_cast] lemma coe_neg (f : α →₁[μ] β) : ((-f : α →₁[μ] β) : α →ₘ[μ] β) = -f := rfl -@[simp, norm_cast] -lemma coe_sub (f g : α →₁[μ] β) : ((f - g : α →₁[μ] β) : α →ₘ[μ] β) = f - g := rfl - -@[simp] lemma edist_eq (f g : α →₁[μ] β) : edist f g = edist (f : α →ₘ[μ] β) (g : α →ₘ[μ] β) := rfl - -lemma dist_eq (f g : α →₁[μ] β) : - dist f g = ennreal.to_real (edist (f : α →ₘ[μ] β) (g : α →ₘ[μ] β)) := -rfl - -/-- The norm on `L¹` space is defined to be `∥f∥ = ∫⁻ a, edist (f a) 0`. -/ -instance : has_norm (α →₁[μ] β) := ⟨λ f, dist f 0⟩ - -lemma norm_eq (f : α →₁[μ] β) : ∥f∥ = ennreal.to_real (edist (f : α →ₘ[μ] β) 0) := rfl - -instance : normed_group (α →₁[μ] β) := normed_group.of_add_dist (λ x, rfl) $ by -{ intros, simp only [dist_eq, coe_add], rw edist_add_right } - -section normed_space - -variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 β] - -instance : has_scalar 𝕜 (α →₁[μ] β) := ⟨λ x f, ⟨x • (f : α →ₘ[μ] β), ae_eq_fun.integrable.smul f.2⟩⟩ - -@[simp, norm_cast] lemma coe_smul (c : 𝕜) (f : α →₁[μ] β) : - ((c • f : α →₁[μ] β) : α →ₘ[μ] β) = c • (f : α →ₘ[μ] β) := rfl - -instance : semimodule 𝕜 (α →₁[μ] β) := -{ one_smul := λf, l1.eq (by { simp only [coe_smul], exact one_smul _ _ }), - mul_smul := λx y f, l1.eq (by { simp only [coe_smul], exact mul_smul _ _ _ }), - smul_add := λx f g, l1.eq (by { simp only [coe_smul, coe_add], exact smul_add _ _ _ }), - smul_zero := λx, l1.eq (by { simp only [coe_zero, coe_smul], exact smul_zero _ }), - add_smul := λx y f, l1.eq (by { simp only [coe_smul], exact add_smul _ _ _ }), - zero_smul := λf, l1.eq (by { simp only [coe_smul], exact zero_smul _ _ }) } +namespace L1 +variables [second_countable_topology β] [borel_space β] -instance : normed_space 𝕜 (α →₁[μ] β) := -⟨ begin - rintros x ⟨f, hf⟩, - show ennreal.to_real (edist (x • f) 0) ≤ ∥x∥ * ennreal.to_real (edist f 0), - rw [edist_smul, to_real_of_real_mul], - exact norm_nonneg _ - end ⟩ +lemma integrable_coe_fn (f : α →₁[μ] β) : + integrable f μ := +by { rw ← mem_ℒp_one_iff_integrable, exact Lp.mem_ℒp f } -end normed_space - -section of_fun - -/-- Construct the equivalence class `[f]` of an integrable function `f`. -/ -def of_fun (f : α → β) (hf : integrable f μ) : (α →₁[μ] β) := -⟨mk f hf.ae_measurable, by { rw integrable_mk, exact hf }⟩ - -@[simp] lemma of_fun_eq_mk (f : α → β) (hf : integrable f μ) : - (of_fun f hf : α →ₘ[μ] β) = mk f hf.ae_measurable := -rfl - -lemma of_fun_eq_of_fun (f g : α → β) (hf : integrable f μ) (hg : integrable g μ) : - of_fun f hf = of_fun g hg ↔ f =ᵐ[μ] g := -by { rw ← l1.eq_iff, simp only [of_fun_eq_mk, mk_eq_mk] } - -lemma of_fun_zero : of_fun (λ _, (0 : β)) (integrable_zero α β μ) = 0 := rfl - -lemma of_fun_add (f g : α → β) (hf : integrable f μ) (hg : integrable g μ) : - of_fun (f + g) (hf.add hg) = of_fun f hf + of_fun g hg := -rfl - -lemma of_fun_neg (f : α → β) (hf : integrable f μ) : - of_fun (- f) (integrable.neg hf) = - of_fun f hf := rfl - -lemma of_fun_sub (f g : α → β) (hf : integrable f μ) (hg : integrable g μ) : - of_fun (f - g) (hf.sub hg) = of_fun f hf - of_fun g hg := -by simp only [sub_eq_add_neg, of_fun_add _ _ hf hg.neg, of_fun_neg] - -lemma norm_of_fun (f : α → β) (hf : integrable f μ) : - ∥ of_fun f hf ∥ = ennreal.to_real (∫⁻ a, edist (f a) 0 ∂μ) := -rfl - -lemma norm_of_fun_eq_lintegral_norm (f : α → β) (hf : integrable f μ) : - ∥ of_fun f hf ∥ = ennreal.to_real (∫⁻ a, (ennreal.of_real ∥f a∥) ∂μ) := -by { rw [norm_of_fun, lintegral_norm_eq_lintegral_edist] } - -variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 β] - -lemma of_fun_smul (f : α → β) (hf : integrable f μ) (k : 𝕜) : - of_fun (λa, k • f a) (hf.smul k) = k • of_fun f hf := rfl - -end of_fun - -section to_fun - -protected lemma measurable (f : α →₁[μ] β) : measurable f := f.1.measurable - -protected lemma ae_measurable (f : α →₁[μ] β) : ae_measurable f μ := f.1.ae_measurable - -lemma measurable_norm (f : α →₁[μ] β) : measurable (λ a, ∥f a∥) := -f.measurable.norm - -protected lemma integrable (f : α →₁[μ] β) : integrable ⇑f μ := -integrable_coe_fn.2 f.2 - -protected lemma has_finite_integral (f : α →₁[μ] β) : has_finite_integral ⇑f μ := -f.integrable.has_finite_integral - -lemma integrable_norm (f : α →₁[μ] β) : integrable (λ a, ∥f a∥) μ := -(integrable_norm_iff f.ae_measurable).mpr f.integrable - -lemma of_fun_to_fun (f : α →₁[μ] β) : of_fun f f.integrable = f := -subtype.ext (f : α →ₘ[μ] β).mk_coe_fn - -lemma mk_to_fun (f : α →₁[μ] β) : (mk f f.ae_measurable : α →ₘ[μ] β) = f := -by { rw ← of_fun_eq_mk, rw l1.eq_iff, exact of_fun_to_fun f } - -lemma to_fun_of_fun (f : α → β) (hf : integrable f μ) : ⇑(of_fun f hf : α →₁[μ] β) =ᵐ[μ] f := -coe_fn_mk f hf.ae_measurable - -variables (α β) -lemma zero_to_fun : ⇑(0 : α →₁[μ] β) =ᵐ[μ] 0 := ae_eq_fun.coe_fn_zero -variables {α β} - -lemma add_to_fun (f g : α →₁[μ] β) : ⇑(f + g) =ᵐ[μ] f + g := -ae_eq_fun.coe_fn_add _ _ - -lemma neg_to_fun (f : α →₁[μ] β) : ⇑(-f) =ᵐ[μ] -⇑f := ae_eq_fun.coe_fn_neg _ - -lemma sub_to_fun (f g : α →₁[μ] β) : ⇑(f - g) =ᵐ[μ] ⇑f - ⇑g := -ae_eq_fun.coe_fn_sub _ _ - -lemma dist_to_fun (f g : α →₁[μ] β) : dist f g = ennreal.to_real (∫⁻ x, edist (f x) (g x) ∂μ) := -by { simp only [← coe_coe, dist_eq, edist_eq_coe] } - -lemma norm_eq_nnnorm_to_fun (f : α →₁[μ] β) : ∥f∥ = ennreal.to_real (∫⁻ a, nnnorm (f a) ∂μ) := -by { rw [← coe_coe, lintegral_nnnorm_eq_lintegral_edist, ← edist_zero_eq_coe], refl } +lemma has_finite_integral_coe_fn (f : α →₁[μ] β) : + has_finite_integral f μ := +(integrable_coe_fn f).has_finite_integral -lemma norm_eq_norm_to_fun (f : α →₁[μ] β) : - ∥f∥ = ennreal.to_real (∫⁻ a, (ennreal.of_real ∥f a∥) ∂μ) := -by { rw norm_eq_nnnorm_to_fun, congr, funext, rw of_real_norm_eq_coe_nnnorm } +lemma measurable_coe_fn (f : α →₁[μ] β) : + measurable f := Lp.measurable f -lemma lintegral_edist_to_fun_lt_top (f g : α →₁[μ] β) : (∫⁻ a, edist (f a) (g a) ∂μ) < ∞ := -lintegral_edist_lt_top f.integrable g.integrable +lemma ae_measurable_coe_fn (f : α →₁[μ] β) : + ae_measurable f μ := Lp.ae_measurable f -variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 β] +lemma edist_def (f g : α →₁[μ] β) : + edist f g = ∫⁻ a, edist (f a) (g a) ∂μ := +by { simp [Lp.edist_def, snorm, snorm'], simp [edist_eq_coe_nnnorm_sub] } -lemma smul_to_fun (c : 𝕜) (f : α →₁[μ] β) : ⇑(c • f) =ᵐ[μ] c • f := -ae_eq_fun.coe_fn_smul _ _ +lemma dist_def (f g : α →₁[μ] β) : + dist f g = (∫⁻ a, edist (f a) (g a) ∂μ).to_real := +by { simp [Lp.dist_def, snorm, snorm'], simp [edist_eq_coe_nnnorm_sub] } -lemma norm_eq_lintegral (f : α →₁[μ] β) : ∥f∥ = (∫⁻ x, (nnnorm (f x) : ℝ≥0∞) ∂μ).to_real := -by simp [l1.norm_eq, ae_eq_fun.edist_zero_eq_coe, ← edist_eq_coe_nnnorm] +lemma norm_def (f : α →₁[μ] β) : + ∥f∥ = (∫⁻ a, nnnorm (f a) ∂μ).to_real := +by { simp [Lp.norm_def, snorm, snorm'] } /-- Computing the norm of a difference between two L¹-functions. Note that this is not a - special case of `norm_eq_lintegral` since `(f - g) x` and `f x - g x` are not equal + special case of `norm_def` since `(f - g) x` and `f x - g x` are not equal (but only a.e.-equal). -/ lemma norm_sub_eq_lintegral (f g : α →₁[μ] β) : ∥f - g∥ = (∫⁻ x, (nnnorm (f x - g x) : ℝ≥0∞) ∂μ).to_real := begin - simp_rw [l1.norm_eq, ae_eq_fun.edist_zero_eq_coe, ← edist_eq_coe_nnnorm], + rw [norm_def], + congr' 1, rw lintegral_congr_ae, - refine (ae_eq_fun.coe_fn_sub (f : α →ₘ[μ] β) g).mp _, - apply eventually_of_forall, intros x hx, simp [hx] + filter_upwards [Lp.coe_fn_sub f g], + assume a ha, + simp only [ha, pi.sub_apply], end lemma of_real_norm_eq_lintegral (f : α →₁[μ] β) : ennreal.of_real ∥f∥ = ∫⁻ x, (nnnorm (f x) : ℝ≥0∞) ∂μ := -by { rw [norm_eq_lintegral, ennreal.of_real_to_real], rw [← ennreal.lt_top_iff_ne_top], - exact f.has_finite_integral } +by { rw [norm_def, ennreal.of_real_to_real], rw [← ennreal.lt_top_iff_ne_top], + exact has_finite_integral_coe_fn f } /-- Computing the norm of a difference between two L¹-functions. Note that this is not a special case of `of_real_norm_eq_lintegral` since `(f - g) x` and `f x - g x` are not equal @@ -847,78 +684,70 @@ lemma of_real_norm_sub_eq_lintegral (f g : α →₁[μ] β) : begin simp_rw [of_real_norm_eq_lintegral, ← edist_eq_coe_nnnorm], apply lintegral_congr_ae, - refine (ae_eq_fun.coe_fn_sub (f : α →ₘ[μ] β) g).mp _, - apply eventually_of_forall, intros x hx, simp only [l1.coe_coe, pi.sub_apply] at hx, - simp_rw [← hx, ← l1.coe_sub, l1.coe_coe] + filter_upwards [Lp.coe_fn_sub f g], + assume a ha, + simp only [ha, pi.sub_apply], end -end to_fun +end L1 -section pos_part +namespace integrable -/-- Positive part of a function in `L¹` space. -/ -def pos_part (f : α →₁[μ] ℝ) : α →₁[μ] ℝ := -⟨ae_eq_fun.pos_part f, - begin - rw [← ae_eq_fun.integrable_coe_fn], - exact f.integrable.max_zero.congr (coe_fn_pos_part _).symm, - end ⟩ +variables [second_countable_topology β] [borel_space β] -/-- Negative part of a function in `L¹` space. -/ -def neg_part (f : α →₁[μ] ℝ) : α →₁[μ] ℝ := pos_part (-f) +/-- Construct the equivalence class `[f]` of an integrable function `f`, as a member of the +space `L1 β 1 μ`. -/ +def to_L1 (f : α → β) (hf : integrable f μ) : α →₁[μ] β := +(mem_ℒp_one_iff_integrable.2 hf).to_Lp f -@[norm_cast] -lemma coe_pos_part (f : α →₁[μ] ℝ) : (f.pos_part : α →ₘ[μ] ℝ) = (f : α →ₘ[μ] ℝ).pos_part := rfl +@[simp] lemma to_L1_coe_fn (f : α →₁[μ] β) (hf : integrable f μ) : hf.to_L1 f = f := +by simp [integrable.to_L1] -lemma pos_part_to_fun (f : α →₁[μ] ℝ) : ⇑(pos_part f) =ᵐ[μ] λ a, max (f a) 0 := -ae_eq_fun.coe_fn_pos_part _ +lemma coe_fn_to_L1 {f : α → β} (hf : integrable f μ) : hf.to_L1 f =ᵐ[μ] f := +ae_eq_fun.coe_fn_mk _ _ -lemma neg_part_to_fun_eq_max (f : α →₁[μ] ℝ) : ∀ᵐ a ∂μ, neg_part f a = max (- f a) 0 := -begin - rw neg_part, - filter_upwards [pos_part_to_fun (-f), neg_to_fun f], - assume a h₁ h₂, - rw [h₁, h₂, pi.neg_apply] -end +@[simp] lemma to_L1_zero (h : integrable (0 : α → β) μ) : h.to_L1 0 = 0 := rfl -lemma neg_part_to_fun_eq_min (f : α →₁[μ] ℝ) : ∀ᵐ a ∂μ, neg_part f a = - min (f a) 0 := -(neg_part_to_fun_eq_max f).mono $ assume a h, -by rw [h, ← max_neg_neg, neg_zero] +@[simp] lemma to_L1_eq_mk (f : α → β) (hf : integrable f μ) : + (hf.to_L1 f : α →ₘ[μ] β) = ae_eq_fun.mk f hf.ae_measurable := +rfl -lemma norm_le_norm_of_ae_le {f g : α →₁[μ] β} (h : ∀ᵐ a ∂μ, ∥f a∥ ≤ ∥g a∥) : ∥f∥ ≤ ∥g∥ := -begin - simp only [l1.norm_eq_norm_to_fun], - rw to_real_le_to_real, - { apply lintegral_mono_ae, - exact h.mono (λ a h, of_real_le_of_real h) }, - { rw [← lt_top_iff_ne_top, ← has_finite_integral_iff_norm], exact f.has_finite_integral }, - { rw [← lt_top_iff_ne_top, ← has_finite_integral_iff_norm], exact g.has_finite_integral } -end +@[simp] lemma to_L1_eq_to_L1_iff (f g : α → β) (hf : integrable f μ) (hg : integrable g μ) : + to_L1 f hf = to_L1 g hg ↔ f =ᵐ[μ] g := +mem_ℒp.to_Lp_eq_to_Lp_iff _ _ -lemma continuous_pos_part : continuous $ λf : α →₁[μ] ℝ, pos_part f := -begin - simp only [metric.continuous_iff], - assume g ε hε, - use ε, use hε, - simp only [dist_eq_norm], - assume f hfg, - refine lt_of_le_of_lt (norm_le_norm_of_ae_le _) hfg, - filter_upwards [l1.sub_to_fun f g, l1.sub_to_fun (pos_part f) (pos_part g), - pos_part_to_fun f, pos_part_to_fun g], - assume a h₁ h₂ h₃ h₄, - simp only [real.norm_eq_abs, h₁, h₂, h₃, h₄, pi.sub_apply], - exact abs_max_sub_max_le_abs _ _ _ -end +lemma to_L1_add (f g : α → β) (hf : integrable f μ) (hg : integrable g μ) : + to_L1 (f + g) (hf.add hg) = to_L1 f hf + to_L1 g hg := rfl -lemma continuous_neg_part : continuous $ λf : α →₁[μ] ℝ, neg_part f := -have eq : (λf : α →₁[μ] ℝ, neg_part f) = (λf : α →₁[μ] ℝ, pos_part (-f)) := rfl, -by { rw eq, exact continuous_pos_part.comp continuous_neg } +lemma to_L1_neg (f : α → β) (hf : integrable f μ) : + to_L1 (- f) (integrable.neg hf) = - to_L1 f hf := rfl -end pos_part +lemma to_L1_sub (f g : α → β) (hf : integrable f μ) (hg : integrable g μ) : + to_L1 (f - g) (hf.sub hg) = to_L1 f hf - to_L1 g hg := +by simp only [sub_eq_add_neg, to_L1_add _ _ hf hg.neg, to_L1_neg] + +lemma norm_to_L1 (f : α → β) (hf : integrable f μ) : + ∥hf.to_L1 f∥ = ennreal.to_real (∫⁻ a, edist (f a) 0 ∂μ) := +by { simp [to_L1, snorm, snorm'], simp [edist_eq_coe_nnnorm] } + +lemma norm_to_L1_eq_lintegral_norm (f : α → β) (hf : integrable f μ) : + ∥hf.to_L1 f∥ = ennreal.to_real (∫⁻ a, (ennreal.of_real ∥f a∥) ∂μ) := +by { rw [norm_to_L1, lintegral_norm_eq_lintegral_edist] } + +@[simp] lemma edist_to_L1_to_L1 (f g : α → β) (hf : integrable f μ) (hg : integrable g μ) : + edist (hf.to_L1 f) (hg.to_L1 g) = ∫⁻ a, edist (f a) (g a) ∂μ := +by { simp [integrable.to_L1, snorm, snorm'], simp [edist_eq_coe_nnnorm_sub] } + +@[simp] lemma edist_to_L1_zero (f : α → β) (hf : integrable f μ) : + edist (hf.to_L1 f) 0 = ∫⁻ a, edist (f a) 0 ∂μ := +by { simp [integrable.to_L1, snorm, snorm'], simp [edist_eq_coe_nnnorm] } + +variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 β] -/- TODO: l1 is a complete space -/ +lemma to_L1_smul (f : α → β) (hf : integrable f μ) (k : 𝕜) : + to_L1 (λa, k • f a) (hf.smul k) = k • to_L1 f hf := rfl -end l1 +end integrable end measure_theory open measure_theory diff --git a/src/measure_theory/prod.lean b/src/measure_theory/prod.lean index 771d8baa4194e..0ac2730268a03 100644 --- a/src/measure_theory/prod.lean +++ b/src/measure_theory/prod.lean @@ -843,18 +843,19 @@ lemma continuous_integral_integral : continuous (λ (f : α × β →₁[μ.prod ν] E), ∫ x, ∫ y, f (x, y) ∂ν ∂μ) := begin rw [continuous_iff_continuous_at], intro g, - refine tendsto_integral_of_l1 _ g.integrable.integral_prod_left - (eventually_of_forall $ λ h, h.integrable.integral_prod_left) _, + refine tendsto_integral_of_L1 _ (L1.integrable_coe_fn g).integral_prod_left + (eventually_of_forall $ λ h, (L1.integrable_coe_fn h).integral_prod_left) _, simp_rw [edist_eq_coe_nnnorm_sub, - ← lintegral_fn_integral_sub (λ x, (nnnorm x : ℝ≥0∞)) (l1.integrable _) g.integrable], + ← lintegral_fn_integral_sub (λ x, (nnnorm x : ℝ≥0∞)) (L1.integrable_coe_fn _) + (L1.integrable_coe_fn g)], refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds _ (λ i, zero_le _) _, { exact λ i, ∫⁻ x, ∫⁻ y, nnnorm (i (x, y) - g (x, y)) ∂ν ∂μ }, swap, { exact λ i, lintegral_mono (λ x, ennnorm_integral_le_lintegral_ennnorm _) }, show tendsto (λ (i : α × β →₁[μ.prod ν] E), ∫⁻ x, ∫⁻ (y : β), nnnorm (i (x, y) - g (x, y)) ∂ν ∂μ) (𝓝 g) (𝓝 0), have : ∀ (i : α × β →₁[μ.prod ν] E), measurable (λ z, (nnnorm (i z - g z) : ℝ≥0∞)) := - λ i, (i.measurable.sub g.measurable).ennnorm, - simp_rw [← lintegral_prod_of_measurable _ (this _), ← l1.of_real_norm_sub_eq_lintegral, + λ i, ((Lp.measurable i).sub (Lp.measurable g)).ennnorm, + simp_rw [← lintegral_prod_of_measurable _ (this _), ← L1.of_real_norm_sub_eq_lintegral, ← of_real_zero], refine (continuous_of_real.tendsto 0).comp _, rw [← tendsto_iff_norm_tendsto_zero], exact tendsto_id diff --git a/src/measure_theory/set_integral.lean b/src/measure_theory/set_integral.lean index 5c95b0d32cb01..ed79a414feeca 100644 --- a/src/measure_theory/set_integral.lean +++ b/src/measure_theory/set_integral.lean @@ -360,11 +360,12 @@ begin rw [simple_func.coe_add, integrable_add hfg f.measurable g.measurable] at int_fg, refine h_sum hfg int_fg.1 int_fg.2 (hf int_fg.1) (hg int_fg.2) } }, have : ∀ (f : α →₁ₛ[μ] E), P f, - { intro f, exact h_ae f.to_simple_func_eq_to_fun f.integrable - (this f.to_simple_func f.integrable) }, + { intro f, + exact h_ae (L1.simple_func.to_simple_func_eq_to_fun f) (L1.simple_func.integrable f) + (this (L1.simple_func.to_simple_func f) (L1.simple_func.integrable f)) }, have : ∀ (f : α →₁[μ] E), P f := - λ f, l1.simple_func.dense_range.induction_on f h_closed this, - exact λ f hf, h_ae (l1.to_fun_of_fun f hf) (l1.integrable _) (this (l1.of_fun f hf)) + λ f, L1.simple_func.dense_range.induction_on f h_closed this, + exact λ f hf, h_ae hf.coe_fn_to_L1 (L1.integrable_coe_fn _) (this (hf.to_L1 f)), end variables [complete_space E] [normed_space ℝ E] @@ -652,29 +653,19 @@ section /-! ### Continuous linear maps composed with integration The goal of this section is to prove that integration commutes with continuous linear maps. -The first step is to prove that, given a function `φ : α → E` which is measurable and integrable, -and a continuous linear map `L : E →L[ℝ] F`, the function `λ a, L(φ a)` is also measurable -and integrable. Note we cannot write this as `L ∘ φ` since the type of `L` is not an actual -function type. - -The next step is translate this to `l1`, replacing the function `φ` by a term with type -`α →₁[μ] E` (an equivalence class of integrable functions). -The corresponding "composition" is `L.comp_l1 φ : α →₁[μ] F`. This is then upgraded to -a linear map `L.comp_l1ₗ : (α →₁[μ] E) →ₗ[ℝ] (α →₁[μ] F)` and a continuous linear map -`L.comp_l1L : (α →₁[μ] E) →L[ℝ] (α →₁[μ] F)`. - -Then we can prove the commutation result using continuity of all relevant operations -and the result on simple functions. +This holds for simple functions. The general result follows from the continuity of all involved +operations on the space `L¹`. Note that composition by a continuous linear map on `L¹` is not just +the composition, as we are dealing with classes of functions, but it has already been defined +as `continuous_linear_map.comp_Lp`. We take advantage of this construction here. -/ variables {μ : measure α} [normed_space ℝ E] variables [normed_group F] [normed_space ℝ F] +variables {p : ennreal} -namespace continuous_linear_map +local attribute [instance] fact_one_le_one_ennreal -lemma norm_comp_l1_apply_le [opens_measurable_space E] [second_countable_topology E] (φ : α →₁[μ] E) - (L : E →L[ℝ] F) : ∀ᵐ a ∂μ, ∥L (φ a)∥ ≤ ∥L∥ * ∥φ a∥ := -eventually_of_forall (λ a, L.le_op_norm (φ a)) +namespace continuous_linear_map variables [measurable_space F] [borel_space F] @@ -683,72 +674,18 @@ lemma integrable_comp [opens_measurable_space E] {φ : α → E} (L : E →L[ℝ ((integrable.norm φ_int).const_mul ∥L∥).mono' (L.measurable.comp_ae_measurable φ_int.ae_measurable) (eventually_of_forall $ λ a, L.le_op_norm (φ a)) -variables [borel_space E] [second_countable_topology E] - -/-- Composing `φ : α →₁[μ] E` with `L : E →L[ℝ] F`. -/ -def comp_l1 [second_countable_topology F] (L : E →L[ℝ] F) (φ : α →₁[μ] E) : α →₁[μ] F := -l1.of_fun (λ a, L (φ a)) (L.integrable_comp φ.integrable) - -lemma comp_l1_apply [second_countable_topology F] (L : E →L[ℝ] F) (φ : α →₁[μ] E) : - ∀ᵐ a ∂μ, (L.comp_l1 φ) a = L (φ a) := -l1.to_fun_of_fun _ _ - -lemma integrable_comp_l1 (L : E →L[ℝ] F) (φ : α →₁[μ] E) : integrable (λ a, L (φ a)) μ := -L.integrable_comp φ.integrable - -lemma measurable_comp_l1 (L : E →L[ℝ] F) (φ : α →₁[μ] E) : - measurable (λ a, L (φ a)) := L.measurable.comp φ.measurable - -variables [second_countable_topology F] - -lemma integral_comp_l1 [complete_space F] (L : E →L[ℝ] F) (φ : α →₁[μ] E) : - ∫ a, (L.comp_l1 φ) a ∂μ = ∫ a, L (φ a) ∂μ := -by simp [comp_l1] - -/-- Composing `φ : α →₁[μ] E` with `L : E →L[ℝ] F`, seen as a `ℝ`-linear map on `α →₁[μ] E`. -/ -def comp_l1ₗ (L : E →L[ℝ] F) : (α →₁[μ] E) →ₗ[ℝ] (α →₁[μ] F) := -{ to_fun := λ φ, L.comp_l1 φ, - map_add' := begin - intros f g, - dsimp [comp_l1], - rw [← l1.of_fun_add, l1.of_fun_eq_of_fun], - apply (l1.add_to_fun f g).mono, - intros a ha, - simp only [ha, pi.add_apply, L.map_add] - end, - map_smul' := begin - intros c f, - dsimp [comp_l1], - rw [← l1.of_fun_smul, l1.of_fun_eq_of_fun], - apply (l1.smul_to_fun c f).mono, - intros a ha, - simp only [ha, pi.smul_apply, continuous_linear_map.map_smul] - end } - -lemma norm_comp_l1_le (φ : α →₁[μ] E) (L : E →L[ℝ] F) : ∥L.comp_l1 φ∥ ≤ ∥L∥*∥φ∥ := -begin - erw l1.norm_of_fun_eq_integral_norm, - calc - ∫ a, ∥L (φ a)∥ ∂μ ≤ ∫ a, ∥L∥ *∥φ a∥ ∂μ : integral_mono_ae (L.integrable_comp_l1 φ).norm - (φ.integrable_norm.const_mul $ ∥L∥) (L.norm_comp_l1_apply_le φ) - ... = ∥L∥ * ∥φ∥ : by rw [integral_mul_left, φ.norm_eq_integral_norm] -end - -/-- Composing `φ : α →₁[μ] E` with `L : E →L[ℝ] F`, seen as a continuous `ℝ`-linear map on -`α →₁[μ] E`. -/ -def comp_l1L (L : E →L[ℝ] F) : (α →₁[μ] E) →L[ℝ] (α →₁[μ] F) := -linear_map.mk_continuous L.comp_l1ₗ (∥L∥) (λ φ, L.norm_comp_l1_le φ) - -lemma norm_compl1L_le (L : E →L[ℝ] F) : ∥(L.comp_l1L : (α →₁[μ] E) →L[ℝ] (α →₁[μ] F))∥ ≤ ∥L∥ := -op_norm_le_bound _ (norm_nonneg _) (λ φ, L.norm_comp_l1_le φ) +variables [second_countable_topology F] [complete_space F] +[borel_space E] [second_countable_topology E] -variables [complete_space F] +lemma integral_comp_Lp (L : E →L[ℝ] F) (φ : Lp E p μ) : + ∫ a, (L.comp_Lp φ) a ∂μ = ∫ a, L (φ a) ∂μ := +integral_congr_ae $ coe_fn_comp_Lp _ _ -lemma continuous_integral_comp_l1 (L : E →L[ℝ] F) : +lemma continuous_integral_comp_L1 (L : E →L[ℝ] F) : continuous (λ (φ : α →₁[μ] E), ∫ (a : α), L (φ a) ∂μ) := begin - rw ← funext L.integral_comp_l1, - exact continuous_integral.comp L.comp_l1L.continuous + rw ← funext L.integral_comp_Lp, + exact continuous_integral.comp (L.comp_LpL 1 μ).continuous end variables [complete_space E] @@ -765,7 +702,7 @@ begin { intros f g H f_int g_int hf hg, simp [L.map_add, integral_add f_int g_int, integral_add (L.integrable_comp f_int) (L.integrable_comp g_int), hf, hg] }, - { exact is_closed_eq L.continuous_integral_comp_l1 (L.continuous.comp continuous_integral) }, + { exact is_closed_eq L.continuous_integral_comp_L1 (L.continuous.comp continuous_integral) }, { intros f g hfg f_int hf, convert hf using 1 ; clear hf, { exact integral_congr_ae (hfg.fun_comp L).symm }, @@ -773,8 +710,8 @@ begin all_goals { assumption } end -lemma integral_comp_l1_comm (L : E →L[ℝ] F) (φ : α →₁[μ] E) : ∫ a, L (φ a) ∂μ = L (∫ a, φ a ∂μ) := -L.integral_comp_comm φ.integrable +lemma integral_comp_L1_comm (L : E →L[ℝ] F) (φ : α →₁[μ] E) : ∫ a, L (φ a) ∂μ = L (∫ a, φ a ∂μ) := +L.integral_comp_comm (L1.integrable_coe_fn φ) end continuous_linear_map diff --git a/src/measure_theory/simple_func_dense.lean b/src/measure_theory/simple_func_dense.lean index 1246834daa222..925a212ee86e0 100644 --- a/src/measure_theory/simple_func_dense.lean +++ b/src/measure_theory/simple_func_dense.lean @@ -168,7 +168,7 @@ begin exact_mod_cast this, end -lemma tendsto_approx_on_l1_edist [opens_measurable_space E] +lemma tendsto_approx_on_L1_edist [opens_measurable_space E] {f : β → E} (hf : measurable f) {s : set E} {y₀ : E} (h₀ : y₀ ∈ s) [separable_space s] {μ : measure β} (hμ : ∀ᵐ x ∂μ, f x ∈ closure s) (hi : has_finite_integral (λ x, f x - y₀) μ) : tendsto (λ n, ∫⁻ x, edist (approx_on f hf s y₀ h₀ n x) (f x) ∂μ) at_top (𝓝 0) := @@ -207,21 +207,21 @@ begin add_lt_top.2 ⟨hi, hi⟩ end -lemma tendsto_approx_on_univ_l1_edist [opens_measurable_space E] [second_countable_topology E] +lemma tendsto_approx_on_univ_L1_edist [opens_measurable_space E] [second_countable_topology E] {f : β → E} {μ : measure β} (fmeas : measurable f) (hf : integrable f μ) : tendsto (λ n, ∫⁻ x, edist (approx_on f fmeas univ 0 trivial n x) (f x) ∂μ) at_top (𝓝 0) := -tendsto_approx_on_l1_edist fmeas trivial (by simp) (by simpa using hf.2) +tendsto_approx_on_L1_edist fmeas trivial (by simp) (by simpa using hf.2) lemma integrable_approx_on_univ [borel_space E] [second_countable_topology E] {f : β → E} {μ : measure β} (fmeas : measurable f) (hf : integrable f μ) (n : ℕ) : integrable (approx_on f fmeas univ 0 trivial n) μ := integrable_approx_on fmeas hf _ (integrable_zero _ _ _) n -lemma tendsto_approx_on_univ_l1 [borel_space E] [second_countable_topology E] +lemma tendsto_approx_on_univ_L1 [borel_space E] [second_countable_topology E] {f : β → E} {μ : measure β} (fmeas : measurable f) (hf : integrable f μ) : - tendsto (λ n, l1.of_fun (approx_on f fmeas univ 0 trivial n) - (integrable_approx_on_univ fmeas hf n)) at_top (𝓝 $ l1.of_fun f hf) := -tendsto_iff_edist_tendsto_0.2 $ tendsto_approx_on_univ_l1_edist fmeas hf + tendsto (λ n, integrable.to_L1 (approx_on f fmeas univ 0 trivial n) + (integrable_approx_on_univ fmeas hf n)) at_top (𝓝 $ hf.to_L1 f) := +tendsto_iff_edist_tendsto_0.2 $ by simpa using tendsto_approx_on_univ_L1_edist fmeas hf end simple_func diff --git a/src/order/galois_connection.lean b/src/order/galois_connection.lean index a2e3d64cd68a6..8927c76e47835 100644 --- a/src/order/galois_connection.lean +++ b/src/order/galois_connection.lean @@ -30,7 +30,7 @@ An example of this is the Galois insertion is in group thery. If `G` is a topolo then there is a Galois insertion between the set of subsets of `G`, `set G`, and the set of subgroups of `G`, `subgroup G`. The left adjoint is `subgroup.closure`, taking the `subgroup` generated by a `set`, The right adjoint is the coercion from `subgroup G` to -`set G`, taking the underlying set of an subgroup. +`set G`, taking the underlying set of a subgroup. Naively lifting a lattice structure along this Galois insertion would mean that the definition of `inf` on subgroups would be `subgroup.closure (↑S ∩ ↑T)`. This is an undesirable definition