From 69e861e9fe786dac4b5131e0fac6737bd27d2358 Mon Sep 17 00:00:00 2001 From: Zhouhang Zhou Date: Thu, 12 Dec 2019 04:05:22 -0500 Subject: [PATCH] feat(measure_theory/bochner_integration): connecting the Bochner integral with the integral on `ennreal`-valued functions (#1790) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * shorter proof * feat(measure_theory/bochner_integration): connecting the Bochner integral with the integral on `ennreal` This PR proves that `∫ f = ∫ f⁺ - ∫ f⁻`, with the first integral sign being the Bochner integral of a real-valued function `f : α → ℝ`, and second and third integral sign being the integral on `ennreal`-valued functions. See `integral_eq_lintegral_max_sub_lintegral_min`. I feel that most of the basic properties of the Bochner integral are proved. Please let me know if you think something else is needed. * various things : * add guides for typeclass inference; * add `norm_cast` tags; * prove some corollaries; * add doc strings; * other fixes * Update bochner_integration.lean * add some doc strings * Fix doc strings * Update bochner_integration.lean * Update bochner_integration.lean * fix doc strings * Update bochner_integration.lean * Use dot notation * use dot notation * Update Meas.lean --- src/algebra/order_functions.lean | 23 + src/measure_theory/ae_eq_fun.lean | 84 ++-- src/measure_theory/bochner_integration.lean | 466 +++++++++++++++++--- src/measure_theory/borel_space.lean | 81 ++-- src/measure_theory/category/Meas.lean | 4 +- src/measure_theory/giry_monad.lean | 6 +- src/measure_theory/integration.lean | 8 +- src/measure_theory/l1_space.lean | 230 +++++++--- src/measure_theory/measurable_space.lean | 64 +-- src/measure_theory/simple_func_dense.lean | 6 +- 10 files changed, 740 insertions(+), 232 deletions(-) diff --git a/src/algebra/order_functions.lean b/src/algebra/order_functions.lean index edd0ba71ffd08..a844f88b89181 100644 --- a/src/algebra/order_functions.lean +++ b/src/algebra/order_functions.lean @@ -251,6 +251,29 @@ calc lemma max_le_add_of_nonneg {a b : α} (ha : a ≥ 0) (hb : b ≥ 0) : max a b ≤ a + b := max_le_iff.2 (by split; simpa) +lemma max_zero_sub_eq_self (a : α) : max a 0 - max (-a) 0 = a := +begin + rcases le_total a 0, + { rw [max_eq_right h, max_eq_left, zero_sub, neg_neg], { rwa [le_neg, neg_zero] } }, + { rw [max_eq_left, max_eq_right, sub_zero], { rwa [neg_le, neg_zero] }, exact h } +end + +lemma abs_max_sub_max_le_abs (a b c : α) : abs (max a c - max b c) ≤ abs (a - b) := +begin + simp only [max], + split_ifs, + { rw [sub_self, abs_zero], exact abs_nonneg _ }, + { calc abs (c - b) = - (c - b) : abs_of_neg (sub_neg_of_lt (lt_of_not_ge h_1)) + ... = b - c : neg_sub _ _ + ... ≤ b - a : by { rw sub_le_sub_iff_left, exact h } + ... = - (a - b) : by rw neg_sub + ... ≤ abs (a - b) : neg_le_abs_self _ }, + { calc abs (a - c) = a - c : abs_of_pos (sub_pos_of_lt (lt_of_not_ge h)) + ... ≤ a - b : by { rw sub_le_sub_iff_left, exact h_1 } + ... ≤ abs (a - b) : le_abs_self _ }, + { refl } +end + end decidable_linear_ordered_comm_group section decidable_linear_ordered_semiring diff --git a/src/measure_theory/ae_eq_fun.lean b/src/measure_theory/ae_eq_fun.lean index 8ba662dd192dc..79009cc4d1885 100644 --- a/src/measure_theory/ae_eq_fun.lean +++ b/src/measure_theory/ae_eq_fun.lean @@ -8,42 +8,42 @@ import measure_theory.integration /-! -# ALmost everywhere equal functions +# Almost everywhere equal functions Two measurable functions are treated as identical if they are almost everywhere equal. We form the set of equivalence classes under the relation of being almost everywhere equal, which is sometimes -known as the L0 space. +known as the `L⁰` space. -See `l1_space.lean` for L1 space. +See `l1_space.lean` for `L¹` space. ## Notation -* `α →ₘ β` is the type of L0 space, where `α` is a measure space and `β` is a measurable space. - `f : α →ₘ β` is a "function" in L0. In comments, `[f]` is also used to denote an L0 function. +* `α →ₘ β` is the type of `L⁰` space, where `α` is a measure space and `β` is a measurable space. + `f : α →ₘ β` is a "function" in `L⁰`. In comments, `[f]` is also used to denote an `L⁰` function. `ₘ` can be typed as `\_m`. Sometimes it is shown as a box if font is missing. ## Main statements -* The linear structure of L0 : - Addition and scalar multiplication are defined on L0 in the natural way, i.e., +* The linear structure of `L⁰` : + Addition and scalar multiplication are defined on `L⁰` in the natural way, i.e., `[f] + [g] := [f + g]`, `c • [f] := [c • f]`. So defined, `α →ₘ β` inherits the linear structure of `β`. For example, if `β` is a module, then `α →ₘ β` is a module over the same ring. See `mk_add_mk`, `neg_mk`, `mk_sub_mk`, `smul_mk`, `add_to_fun`, `neg_to_fun`, `sub_to_fun`, `smul_to_fun` -* The order structure of L0 : +* The order structure of `L⁰` : `≤` can be defined in a similar way: `[f] ≤ [g]` if `f a ≤ g a` for almost all `a` in domain. And `α →ₘ β` inherits the preorder and partial order of `β`. - TODO: Define `sup` and `inf` on L0 so that it forms a lattice. It seems that `β` must be a + TODO: Define `sup` and `inf` on `L⁰` so that it forms a lattice. It seems that `β` must be a linear order, since otherwise `f ⊔ g` may not be a measurable function. -* Emetric on L0 : - If `β` is an `emetric_space`, then L0 can be made into an `emetric_space`, where +* Emetric on `L⁰` : + If `β` is an `emetric_space`, then `L⁰` can be made into an `emetric_space`, where `edist [f] [g]` is defined to be `∫⁻ a, edist (f a) (g a)`. The integral used here is `lintegral : (α → ennreal) → ennreal`, which is defined in the file @@ -54,24 +54,22 @@ See `l1_space.lean` for L1 space. ## Implementation notes -`f.to_fun` : To find a representative of `f : α →ₘ β`, use `f.to_fun`. - For each operation `op` in L0, there is a lemma called `op_to_fun`, characterizing, +* `f.to_fun` : To find a representative of `f : α →ₘ β`, use `f.to_fun`. + For each operation `op` in `L⁰`, there is a lemma called `op_to_fun`, characterizing, say, `(f op g).to_fun`. - -`ae_eq_fun.mk` : To constructs an L0 function `α →ₘ β` from a measurable function `f : α → β`, +* `ae_eq_fun.mk` : To constructs an `L⁰` function `α →ₘ β` from a measurable function `f : α → β`, use `ae_eq_fun.mk` - -`comp` : Use `comp g f` to get `[g ∘ f]` from `g : β → γ` and `[f] : α →ₘ γ` - -`comp₂` : Use `comp₂ g f₁ f₂ to get `[λa, g (f₁ a) (f₂ a)]`. +* `comp` : Use `comp g f` to get `[g ∘ f]` from `g : β → γ` and `[f] : α →ₘ γ` +* `comp₂` : Use `comp₂ g f₁ f₂ to get `[λa, g (f₁ a) (f₂ a)]`. For example, `[f + g]` is `comp₂ (+)` ## Tags -function space, almost everywhere equal, L0, ae_eq_fun +function space, almost everywhere equal, `L⁰`, ae_eq_fun -/ + noncomputable theory open_locale classical @@ -162,7 +160,7 @@ def comp₂ {γ δ : Type*} [measurable_space γ] [measurable_space δ] (g : β → γ → δ) (hg : measurable (λp:β×γ, g p.1 p.2)) (f₁ : α →ₘ β) (f₂ : α →ₘ γ) : α →ₘ δ := begin refine quotient.lift_on₂ f₁ f₂ (λf₁ f₂, mk (λa, g (f₁.1 a) (f₂.1 a)) $ _) _, - { exact measurable.comp hg (measurable_prod_mk f₁.2 f₂.2) }, + { exact measurable.comp hg (measurable.prod_mk f₁.2 f₂.2) }, { rintros ⟨f₁, hf₁⟩ ⟨f₂, hf₂⟩ ⟨g₁, hg₁⟩ ⟨g₂, hg₂⟩ h₁ h₂, refine quotient.sound _, filter_upwards [h₁, h₂], @@ -172,13 +170,13 @@ end @[simp] lemma comp₂_mk_mk {γ δ : Type*} [measurable_space γ] [measurable_space δ] (g : β → γ → δ) (hg : measurable (λp:β×γ, g p.1 p.2)) (f₁ : α → β) (f₂ : α → γ) (hf₁ hf₂) : comp₂ g hg (mk f₁ hf₁) (mk f₂ hf₂) = - mk (λa, g (f₁ a) (f₂ a)) (measurable.comp hg (measurable_prod_mk hf₁ hf₂)) := + mk (λa, g (f₁ a) (f₂ a)) (measurable.comp hg (measurable.prod_mk hf₁ hf₂)) := rfl lemma comp₂_eq_mk_to_fun {γ δ : Type*} [measurable_space γ] [measurable_space δ] (g : β → γ → δ) (hg : measurable (λp:β×γ, g p.1 p.2)) (f₁ : α →ₘ β) (f₂ : α →ₘ γ) : comp₂ g hg f₁ f₂ = mk (λa, g (f₁.to_fun a) (f₂.to_fun a)) - (hg.comp (measurable_prod_mk f₁.measurable f₂.measurable)) := + (hg.comp (measurable.prod_mk f₁.measurable f₂.measurable)) := by conv_lhs { rw [self_eq_mk f₁, self_eq_mk f₂, comp₂_mk_mk] } lemma comp₂_to_fun {γ δ : Type*} [measurable_space γ] [measurable_space δ] @@ -199,8 +197,8 @@ end `(f a, g a)` for almost all `a` -/ def lift_rel {γ : Type*} [measurable_space γ] (r : β → γ → Prop) (f : α →ₘ β) (g : α →ₘ γ) : Prop := lift_pred (λp:β×γ, r p.1 p.2) - (comp₂ prod.mk (measurable_prod_mk - (measurable_fst measurable_id) (measurable_snd measurable_id)) f g) + (comp₂ prod.mk (measurable.prod_mk + (measurable.fst measurable_id) (measurable.snd measurable_id)) f g) lemma lift_rel_mk_mk {γ : Type*} [measurable_space γ] (r : β → γ → Prop) (f : α → β) (g : α → γ) (hf hg) : lift_rel r (mk f hf) (mk g hg) ↔ ∀ₘ a, r (f a) (g a) := @@ -236,7 +234,7 @@ instance [partial_order β] : partial_order (α →ₘ β) := end, .. ae_eq_fun.preorder } -/- TODO: Prove L0 space is a lattice if β is linear order. +/- TODO: Prove `L⁰` space is a lattice if β is linear order. What if β is only a lattice? -/ -- instance [linear_order β] : semilattice_sup (α →ₘ β) := @@ -266,12 +264,12 @@ variables {γ : Type*} [topological_space γ] [second_countable_topology γ] [add_monoid γ] [topological_add_monoid γ] protected def add : (α →ₘ γ) → (α →ₘ γ) → (α →ₘ γ) := -comp₂ (+) (measurable_add (measurable_fst measurable_id) (measurable_snd measurable_id)) +comp₂ (+) (measurable.add (measurable.fst measurable_id) (measurable.snd measurable_id)) instance : has_add (α →ₘ γ) := ⟨ae_eq_fun.add⟩ @[simp] lemma mk_add_mk (f g : α → γ) (hf hg) : - (mk f hf) + (mk g hg) = mk (f + g) (measurable_add hf hg) := rfl + (mk f hf) + (mk g hg) = mk (f + g) (measurable.add hf hg) := rfl lemma add_to_fun (f g : α →ₘ γ) : ∀ₘ a, (f + g).to_fun a = f.to_fun a + g.to_fun a := comp₂_to_fun _ _ _ _ @@ -300,11 +298,11 @@ section add_group variables {γ : Type*} [topological_space γ] [add_group γ] [topological_add_group γ] -protected def neg : (α →ₘ γ) → (α →ₘ γ) := comp has_neg.neg (measurable_neg measurable_id) +protected def neg : (α →ₘ γ) → (α →ₘ γ) := comp has_neg.neg (measurable.neg measurable_id) instance : has_neg (α →ₘ γ) := ⟨ae_eq_fun.neg⟩ -@[simp] lemma neg_mk (f : α → γ) (hf) : -(mk f hf) = mk (-f) (measurable_neg hf) := rfl +@[simp] lemma neg_mk (f : α → γ) (hf) : -(mk f hf) = mk (-f) (measurable.neg hf) := rfl lemma neg_to_fun (f : α →ₘ γ) : ∀ₘ a, (-f).to_fun a = - f.to_fun a := comp_to_fun _ _ _ @@ -316,7 +314,7 @@ instance : add_group (α →ₘ γ) := } @[simp] lemma mk_sub_mk (f g : α → γ) (hf hg) : - (mk f hf) - (mk g hg) = mk (λa, (f a) - (g a)) (measurable_sub hf hg) := rfl + (mk f hf) - (mk g hg) = mk (λa, (f a) - (g a)) (measurable.sub hf hg) := rfl lemma sub_to_fun (f g : α →ₘ γ) : ∀ₘ a, (f - g).to_fun a = f.to_fun a - g.to_fun a := begin @@ -403,8 +401,8 @@ instance : vector_space 𝕜 (α →ₘ γ) := { .. ae_eq_fun.semimodule } end vector_space -/- TODO : Prove that L0 is a complete space if the codomain is complete. -/ -/- TODO : Multiplicative structure of L0 if useful -/ +/- TODO : Prove that `L⁰` is a complete space if the codomain is complete. -/ +/- TODO : Multiplicative structure of `L⁰` if useful -/ open ennreal @@ -541,6 +539,26 @@ end end normed_space +section pos_part + +variables {γ : Type*} [topological_space γ] [decidable_linear_order γ] [ordered_topology γ] + [second_countable_topology γ] [has_zero γ] + +/-- Positive part of an `ae_eq_fun`. -/ +def pos_part (f : α →ₘ γ) : α →ₘ γ := +comp₂ max (measurable.max (measurable.fst measurable_id) (measurable.snd measurable_id)) f 0 + +lemma pos_part_to_fun (f : α →ₘ γ) : ∀ₘ a, (pos_part f).to_fun a = max (f.to_fun a) (0:γ) := +begin + filter_upwards [comp₂_to_fun max (measurable.max (measurable.fst measurable_id) + (measurable.snd measurable_id)) f 0, @ae_eq_fun.zero_to_fun α γ], + simp only [mem_set_of_eq], + assume a h₁ h₂, + rw [pos_part, h₁, h₂] +end + +end pos_part + end ae_eq_fun end measure_theory diff --git a/src/measure_theory/bochner_integration.lean b/src/measure_theory/bochner_integration.lean index 3f8e3553b155b..cab8809e69351 100644 --- a/src/measure_theory/bochner_integration.lean +++ b/src/measure_theory/bochner_integration.lean @@ -18,45 +18,99 @@ extending the integral on simple functions. The Bochner integral is defined following these steps: -Step 1: Define the integral on simple functions of the type `simple_func α β` (notation : `α →ₛ β`) +1. Define the integral on simple functions of the type `simple_func α β` (notation : `α →ₛ β`) where `β` is a real normed space. (See `simple_func.bintegral` and section `bintegral` for details. Also see `simple_func.integral` for the integral on simple functions of the type `simple_func α ennreal`.) -Step 2: Use `simple_func α β` to cut out the simple functions from L1 functions, and define integral +2. Use `simple_func α β` to cut out the simple functions from L1 functions, and define integral on these. The type of simple functions in L1 space is written as `α →₁ₛ β`. -Step 3: Show that the embedding of `α →₁ₛ β` into L1 is a dense and uniform one. +3. Show that the embedding of `α →₁ₛ β` into L1 is a dense and uniform one. -Step 4: Show that the integral defined on `α →₁ₛ β` is a continuous linear map. +4. Show that the integral defined on `α →₁ₛ β` is a continuous linear map. -Step 5: Define the Bochner integral on L1 functions by extending the integral on integrable simple +5. Define the Bochner integral on L1 functions by extending the integral on integrable simple functions `α →₁ₛ β` using `continuous_linear_map.extend`. Define the Bochner integral on functions as the Bochner integral of its equivalence class in L1 space. ## Main statements -`section bintegral` : basic properties of `simple_func.bintegral` proved. +1. Basic properties of the Bochner integral on functions of type `α → β`, where `α` is a measure + space and `β` is a real normed space. -`section instances` : `l1.simple_func` forms a `normed_space`. + * `integral_zero` : `∫ 0 = 0` + * `integral_add` : `∫ f + g = ∫ f + ∫ g` + * `integral_neg` : `∫ -f = - ∫ f` + * `integral_sub` : `∫ f - g = ∫ f - ∫ g` + * `integral_smul` : `∫ r • f = r • ∫ f` + * `integral_congr_ae` : `∀ₘ a, f a = g a → ∫ f = ∫ g` + * `norm_integral_le_integral_norm` : `∥∫ f∥ ≤ ∫ ∥f∥` -`section coe_to_l1` : `coe` from `l1.simple_func` to `l1` is a uniform and dense embedding. +2. Basic properties of the Bochner integral on functions of type `α → ℝ`, where `α` is a measure + space. -`section simple_func_integral` : basic properties of `l1.simple_func.integral` proved. + * `integral_nonneg_of_nonneg_ae` : `∀ₘ a, 0 ≤ f a → 0 ≤ ∫ f` + * `integral_nonpos_of_nonpos_ae` : `∀ₘ a, f a ≤ 0 → ∫ f ≤ 0` + * `integral_le_integral_of_le_ae` : `∀ₘ a, f a ≤ g a → ∫ f ≤ ∫ g` + +3. Propositions connecting the Bochner integral with the integral on `ennreal`-valued functions, + which is called `lintegral` and has the notation `∫⁻`. + + * `integral_eq_lintegral_max_sub_lintegral_min` : `∫ f = ∫⁻ f⁺ - ∫⁻ f⁻`, where `f⁺` is the positive + part of `f` and `f⁻` is the negative part of `f`. + * `integral_eq_lintegral_of_nonneg_ae` : `∀ₘ a, 0 ≤ f a → ∫ f = ∫⁻ f` + +4. `tendsto_integral_of_dominated_convergence` : the Lebesgue dominated convergence theorem + +## Notes + +Some tips on how to prove a proposition if the API for the Bochner integral is not enough so that +you need to unfold the definition of the Bochner integral and go back to simple functions. + +See `integral_eq_lintegral_max_sub_lintegral_min` for a complicated example, which proves that +`∫ f = ∫⁻ f⁺ - ∫⁻ f⁻`, with the first integral sign being the Bochner integral of a real-valued +function f : α → ℝ, and second and third integral sign being the integral on ennreal-valued +functions (called `lintegral`). The proof of `integral_eq_lintegral_max_sub_lintegral_min` is +scattered in sections with the name `pos_part`. + +Here are the usual steps of proving that a property `p`, say `∫ f = ∫⁻ f⁺ - ∫⁻ f⁻`, holds for all +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`. + +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`. + +4. Since simple functions are dense in `L¹`, +``` +univ = closure {s simple} + = closure {s simple | ∫ s = ∫⁻ s⁺ - ∫⁻ s⁻} : the property holds for all simple functions + ⊆ closure {f | ∫ f = ∫⁻ f⁺ - ∫⁻ f⁻} + = {f | ∫ f = ∫⁻ f⁺ - ∫⁻ f⁻} : closure of a closed set is itself +``` +Use `is_closed_property` or `dense_range.induction_on` for this argument. ## Notations -`α →ₛ β` : simple functions (defined in `measure_theory/integration`) -`α →₁ β` : functions in L1 space, i.e., equivalence classes of integrable functions (defined in - `measure_theory/l1_space`) -`α →₁ₛ β` : simple functions in L1 space, i.e., equivalence classes of integrable simple functions +* `α →ₛ β` : simple functions (defined in `measure_theory/integration`) +* `α →₁ β` : functions in L1 space, i.e., equivalence classes of integrable functions (defined in + `measure_theory/l1_space`) +* `α →₁ₛ β` : simple functions in L1 space, i.e., equivalence classes of integrable simple functions Note : `ₛ` is typed using `\_s`. Sometimes it shows as a box if font is missing. ## Tags -Bochner integral, simple function, function space +Bochner integral, simple function, function space, Lebesgue dominated convergence theorem -/ @@ -65,6 +119,53 @@ open_locale classical topological_space set_option class.instance_max_depth 100 +-- Typeclass inference has difficulty finding `has_scalar ℝ β` where `β` is a `normed_space` on `ℝ` +local attribute [instance, priority 10000] + mul_action.to_has_scalar distrib_mul_action.to_mul_action add_comm_group.to_add_comm_monoid + normed_group.to_add_comm_group normed_space.to_vector_space vector_space.to_module + module.to_semimodule + +namespace measure_theory + +universes u v w +variables {α : Type u} [measurable_space α] {β : Type v} [decidable_linear_order β] [has_zero β] + +local infixr ` →ₛ `:25 := simple_func + +namespace simple_func + +section pos_part + +/-- Positive part of a simple function. -/ +def pos_part (f : α →ₛ β) : α →ₛ β := f.map (λb, max b 0) + +/-- Negative part of a simple function. -/ +def neg_part [has_neg β] (f : α →ₛ β) : α →ₛ β := pos_part (-f) + +lemma pos_part_map_norm (f : α →ₛ ℝ) : (pos_part f).map norm = pos_part f := +begin + ext, + rw [map_apply, real.norm_eq_abs, abs_of_nonneg], + rw [pos_part, map_apply], + exact le_max_right _ _ +end + +lemma neg_part_map_norm (f : α →ₛ ℝ) : (neg_part f).map norm = neg_part f := +by { rw neg_part, exact pos_part_map_norm _ } + +lemma pos_part_sub_neg_part (f : α →ₛ ℝ) : f.pos_part - f.neg_part = f := +begin + simp only [pos_part, neg_part], + ext, + exact max_zero_sub_eq_self (f a) +end + +end pos_part + +end simple_func + +end measure_theory + namespace measure_theory open set lattice filter topological_space ennreal emetric @@ -248,6 +349,23 @@ begin end ... = bintegral f + bintegral g : rfl +lemma bintegral_neg {f : α →ₛ β} (hf : integrable f) : bintegral (-f) = - bintegral f := +calc bintegral (-f) = bintegral (f.map (has_neg.neg)) : rfl + ... = - bintegral f : + begin + rw [map_bintegral f _ hf neg_zero, bintegral, ← sum_neg_distrib], + refine finset.sum_congr rfl (λx h, smul_neg _ _), + end + +lemma bintegral_sub {f g : α →ₛ β} (hf : integrable f) (hg : integrable g) : + bintegral (f - g) = bintegral f - bintegral g := +begin + have : f - g = f + (-g) := rfl, + rw [this, bintegral_add hf _, bintegral_neg hg], + { refl }, + exact hg.neg +end + lemma bintegral_smul (r : ℝ) {f : α →ₛ β} (hf : integrable f) : bintegral (r • f) = r • bintegral f := calc bintegral (r • f) = sum f.range (λx, ennreal.to_real (volume (f ⁻¹' {x})) • r • x) : @@ -332,14 +450,14 @@ local attribute [instance] protected lemma is_add_subgroup : is_add_subgroup begin rintros f g ⟨s, hsi, hs⟩ ⟨t, hti, ht⟩, use s + t, split, - { exact integrable_add s.measurable t.measurable hsi hti }, + { exact integrable.add s.measurable t.measurable hsi hti }, { rw [coe_add, ← hs, ← ht], refl } end, neg_mem := begin rintros f ⟨s, hsi, hs⟩, use -s, split, - { exact integrable_neg hsi }, + { exact hsi.neg }, { rw [coe_neg, ← hs], refl } end } @@ -350,10 +468,10 @@ protected def add_comm_group : add_comm_group (α →₁ₛ β) := subtype.add_c local attribute [instance] simple_func.add_comm_group simple_func.metric_space simple_func.emetric_space -@[simp] lemma coe_zero : ((0 : α →₁ₛ β) : α →₁ β) = 0 := rfl -@[simp] lemma coe_add (f g : α →₁ₛ β) : ((f + g : α →₁ₛ β) : α →₁ β) = f + g := rfl -@[simp] lemma coe_neg (f : α →₁ₛ β) : ((-f : α →₁ₛ β) : α →₁ β) = -f := rfl -@[simp] lemma coe_sub (f g : α →₁ₛ β) : ((f - g : α →₁ₛ β) : α →₁ β) = f - g := rfl +@[simp, elim_cast] lemma coe_zero : ((0 : α →₁ₛ β) : α →₁ β) = 0 := rfl +@[simp, move_cast] lemma coe_add (f g : α →₁ₛ β) : ((f + g : α →₁ₛ β) : α →₁ β) = f + g := rfl +@[simp, move_cast] lemma coe_neg (f : α →₁ₛ β) : ((-f : α →₁ₛ β) : α →₁ β) = -f := rfl +@[simp, move_cast] lemma coe_sub (f g : α →₁ₛ β) : ((f - g : α →₁ₛ β) : α →₁ β) = f - g := rfl @[simp] lemma edist_eq (f g : α →₁ₛ β) : edist f g = edist (f : α →₁ β) (g : α →₁ β) := rfl @[simp] lemma dist_eq (f g : α →₁ₛ β) : dist f g = dist (f : α →₁ β) (g : α →₁ β) := rfl @@ -381,13 +499,14 @@ protected def has_scalar : has_scalar 𝕜 (α →₁ₛ β) := ⟨λk f, ⟨k begin rcases f with ⟨f, ⟨s, hsi, hs⟩⟩, use k • s, split, - { exact integrable_smul _ hsi }, + { exact integrable.smul _ hsi }, { rw [coe_smul, subtype.coe_mk, ← hs], refl } end ⟩⟩ -local attribute [instance] simple_func.has_scalar +local attribute [instance, priority 10000] simple_func.has_scalar -@[simp] lemma coe_smul (c : 𝕜) (f : α →₁ₛ β) : ((c • f : α →₁ₛ β) : α →₁ β) = c • (f : α →₁ β) := rfl +@[simp, move_cast] lemma coe_smul (c : 𝕜) (f : α →₁ₛ β) : + ((c • f : α →₁ₛ β) : α →₁ β) = c • (f : α →₁ β) := rfl /-- Not declared as an instance as `α →₁ₛ β` will only be useful in the construction of the bochner integral. -/ @@ -435,20 +554,20 @@ lemma of_simple_func_eq_mk (f : α →ₛ β) (hf : integrable f) : lemma of_simple_func_zero : of_simple_func (0 : α →ₛ β) integrable_zero = 0 := rfl lemma of_simple_func_add (f g : α →ₛ β) (hf hg) : - of_simple_func (f + g) (integrable_add f.measurable g.measurable hf hg) = of_simple_func f hf + + of_simple_func (f + g) (integrable.add f.measurable g.measurable hf hg) = of_simple_func f hf + of_simple_func g hg := rfl lemma of_simple_func_neg (f : α →ₛ β) (hf) : - of_simple_func (-f) (integrable_neg hf) = -of_simple_func f hf := rfl + of_simple_func (-f) (integrable.neg hf) = -of_simple_func f hf := rfl lemma of_simple_func_sub (f g : α →ₛ β) (hf hg) : - of_simple_func (f - g) (integrable_sub f.measurable g.measurable hf hg) = of_simple_func f hf - + of_simple_func (f - g) (integrable.sub f.measurable g.measurable hf hg) = of_simple_func f hf - of_simple_func g hg := rfl variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 β] lemma of_simple_func_smul (f : α →ₛ β) (hf) (c : 𝕜) : - of_simple_func (c • f) (integrable_smul _ hf) = c • of_simple_func f hf := rfl + of_simple_func (c • f) (integrable.smul _ hf) = c • of_simple_func f hf := rfl lemma norm_of_simple_func (f : α →ₛ β) (hf) : ∥of_simple_func f hf∥ = ennreal.to_real (∫⁻ a, edist (f a) 0) := rfl @@ -658,13 +777,41 @@ variables {α β 𝕜} end coe_to_l1 +section pos_part + +/-- Positive part of a simple function in L1 space. -/ +def pos_part (f : α →₁ₛ ℝ) : α →₁ₛ ℝ := ⟨l1.pos_part (f : α →₁ ℝ), +begin + rcases f with ⟨f, s, hsi, hsf⟩, + use s.pos_part, + split, + { exact integrable.max_zero hsi }, + { simp only [subtype.coe_mk], + rw [l1.coe_pos_part, ← hsf, ae_eq_fun.pos_part, ae_eq_fun.zero_def, comp₂_mk_mk, mk_eq_mk], + filter_upwards [], + simp only [mem_set_of_eq], + assume a, + refl } +end ⟩ + +/-- Negative part of a simple function in L1 space. -/ +def neg_part (f : α →₁ₛ ℝ) : α →₁ₛ ℝ := pos_part (-f) + +@[move_cast] lemma coe_pos_part (f : α →₁ₛ ℝ) : (f.pos_part : α →₁ ℝ) = (f : α →₁ ℝ).pos_part := rfl + +@[move_cast] lemma coe_neg_part (f : α →₁ₛ ℝ) : (f.neg_part : α →₁ ℝ) = (f : α →₁ ℝ).neg_part := rfl + +end pos_part + section simple_func_integral /-! Define the Bochner integral on `α →₁ₛ β` and prove basic properties of this integral. -/ variables [normed_space ℝ β] /-- The Bochner integral over simple functions in l1 space. -/ -def integral (f : α →₁ₛ β) : β := simple_func.bintegral (f.to_simple_func) +def integral (f : α →₁ₛ β) : β := (f.to_simple_func).bintegral + +lemma integral_eq_bintegral (f : α →₁ₛ β) : integral f = (f.to_simple_func).bintegral := rfl lemma integral_eq_lintegral {f : α →₁ₛ ℝ} (h_pos : ∀ₘ a, 0 ≤ f.to_simple_func a) : integral f = ennreal.to_real (∫⁻ a, ennreal.of_real (f.to_simple_func a)) := @@ -679,7 +826,7 @@ begin simp only [integral], rw ← simple_func.bintegral_add f.integrable g.integrable, apply simple_func.bintegral_congr (f + g).integrable, - { exact integrable_add f.measurable g.measurable f.integrable g.integrable }, + { exact integrable.add f.measurable g.measurable f.integrable g.integrable }, { apply add_to_simple_func }, end @@ -688,7 +835,7 @@ begin simp only [integral], rw ← simple_func.bintegral_smul _ f.integrable, apply simple_func.bintegral_congr (r • f).integrable, - { exact integrable_smul _ f.integrable }, + { exact integrable.smul _ f.integrable }, { apply smul_to_simple_func } end @@ -716,6 +863,83 @@ begin exact norm_integral_le_norm _ end +section pos_part + +lemma pos_part_to_simple_func (f : α →₁ₛ ℝ) : + ∀ₘ a, f.pos_part.to_simple_func a = f.to_simple_func.pos_part a := +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 : α →₁ ℝ), + to_simple_func_eq_to_fun f], + simp only [mem_set_of_eq], + assume a h₁ h₂ h₃, + rw [h₁, coe_pos_part, h₂, ← h₃] }, + filter_upwards [ae_eq], + simp only [mem_set_of_eq], + assume a h, + rw [h, eq] +end + +lemma neg_part_to_simple_func (f : α →₁ₛ ℝ) : + ∀ₘ a, f.neg_part.to_simple_func a = f.to_simple_func.neg_part a := +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], + simp only [mem_set_of_eq], + assume a h₁ h₂, + rw h₁, + show max _ _ = max _ _, + rw h₂, + refl +end + +lemma integral_eq_norm_pos_part_sub (f : α →₁ₛ ℝ) : f.integral = ∥f.pos_part∥ - ∥f.neg_part∥ := +begin + -- Convert things in `L¹` to their `simple_func` counterpart + have ae_eq₁ : ∀ₘ a, f.to_simple_func.pos_part a = (f.pos_part).to_simple_func.map norm a, + { filter_upwards [pos_part_to_simple_func f], + simp only [mem_set_of_eq], + 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₂ : ∀ₘ a, f.to_simple_func.neg_part a = (f.neg_part).to_simple_func.map norm a, + { filter_upwards [neg_part_to_simple_func f], + simp only [mem_set_of_eq], + 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, + { filter_upwards [ae_eq₁, ae_eq₂], + simp only [mem_set_of_eq], + assume a h₁ h₂, + rw [h₁, h₂] }, + rw [integral, norm_eq_bintegral, norm_eq_bintegral, ← simple_func.bintegral_sub], + { show f.to_simple_func.bintegral = + ((f.pos_part.to_simple_func).map norm - f.neg_part.to_simple_func.map norm).bintegral, + apply simple_func.bintegral_congr f.integrable, + { show integrable (f.pos_part.to_simple_func.map norm - f.neg_part.to_simple_func.map norm), + refine integrable_of_ae_eq _ _, + { exact (f.to_simple_func.pos_part - f.to_simple_func.neg_part) }, + { exact integrable.sub f.to_simple_func.pos_part.measurable f.to_simple_func.neg_part.measurable + (integrable.max_zero f.integrable) (integrable.max_zero f.integrable.neg) }, + exact ae_eq }, + filter_upwards [ae_eq₁, ae_eq₂], + simp only [mem_set_of_eq], + assume a h₁ h₂, show _ = _ - _, + rw [← h₁, ← h₂], + have := f.to_simple_func.pos_part_sub_neg_part, + conv_lhs {rw ← this}, + refl }, + { refine integrable_of_ae_eq (integrable.max_zero f.integrable) ae_eq₁ }, + { refine integrable_of_ae_eq (integrable.max_zero f.integrable.neg) ae_eq₂ } +end + +end pos_part + end simple_func_integral end simple_func @@ -740,6 +964,10 @@ def integral (f : α →₁ β) : β := (integral_clm).to_fun f lemma integral_eq (f : α →₁ β) : integral f = (integral_clm).to_fun f := rfl +@[elim_cast] lemma integral_coe_eq_integral (f : α →₁ₛ β) : + integral (f : α →₁ β) = f.integral := +by { refine uniformly_extend_of_ind _ _ _ _, exact simple_func.integral_clm.uniform_continuous } + variables (α β) @[simp] lemma integral_zero : integral (0 : α →₁ β) = 0 := map_zero integral_clm @@ -772,6 +1000,26 @@ calc ∥integral f∥ = ∥Integral f∥ : rfl ... ≤ 1 * ∥f∥ : mul_le_mul_of_nonneg_right norm_Integral_le_one $ norm_nonneg _ ... = ∥f∥ : one_mul _ +section pos_part + +lemma integral_eq_norm_pos_part_sub (f : α →₁ ℝ) : integral f = ∥pos_part f∥ - ∥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, + { exact cont _ }, + { refine continuous.sub (continuous_norm.comp l1.continuous_pos_part) + (continuous_norm.comp l1.continuous_neg_part) }, + -- Show that the property holds for all simple functions in the `L¹` space. + { assume s, + norm_cast, + rw [← simple_func.norm_eq, ← simple_func.norm_eq], + exact simple_func.integral_eq_norm_pos_part_sub _} +end + +end pos_part + end integration_in_l1 end l1 @@ -818,7 +1066,7 @@ begin { rw ← l1.integral_add, refl }, { exact ⟨hgm, hgi⟩ }, { exact ⟨hfm, hfi⟩ }, - { exact ⟨measurable_add hfm hgm, integrable_add hfm hgm hfi hgi⟩ } + { exact ⟨measurable.add hfm hgm, integrable.add hfm hgm hfi hgi⟩ } end lemma integral_neg (f : α → β) : integral (-f) = - integral f := @@ -828,7 +1076,7 @@ begin { repeat { rw dif_pos }, { rw ← l1.integral_neg, refl }, { exact ⟨hfm, hfi⟩ }, - { exact ⟨measurable_neg hfm, integrable_neg hfi⟩ } }, + { exact ⟨measurable.neg hfm, integrable.neg hfi⟩ } }, { repeat { rw dif_neg }, { rw neg_zero }, { rw not_and_distrib, exact or.inr hfi }, @@ -846,7 +1094,7 @@ begin { rw ← l1.integral_sub, refl }, { exact ⟨hgm, hgi⟩ }, { exact ⟨hfm, hfi⟩ }, - { exact ⟨measurable_sub hfm hgm, integrable_sub hfm hgm hfi hgi⟩ } + { exact ⟨measurable.sub hfm hgm, integrable.sub hfm hgm hfi hgi⟩ } end lemma integral_smul (r : ℝ) (f : α → β) : (∫ x, r • (f x)) = r • integral f := @@ -859,13 +1107,13 @@ begin { rw dif_pos, rw dif_pos, { rw ← l1.integral_smul, refl }, { exact ⟨hfm, hfi⟩ }, - { exact ⟨measurable_smul _ hfm, integrable_smul _ hfi⟩ } }, + { exact ⟨measurable_smul _ hfm, integrable.smul _ hfi⟩ } }, { repeat { rw dif_neg }, { rw smul_zero }, { rw not_and_distrib, exact or.inr hfi }, { rw not_and_distrib, have : (λx, r • (f x)) = r • f, { funext, simp only [pi.smul_apply] }, - rw [this, integrable_smul_iff r0], exact or.inr hfi } }, + rw [this, integrable.smul_iff r0], exact or.inr hfi } }, { repeat { rw dif_neg }, { rw smul_zero }, { rw not_and_distrib, exact or.inl hfm }, @@ -886,43 +1134,17 @@ begin rw [integral_eq_zero_of_non_integrable hfi, integral_eq_zero_of_non_integrable hgi] }, end -lemma of_real_norm_integral_le_lintegral_norm (f : α → β) : - ennreal.of_real ∥integral f∥ ≤ ∫⁻ a, ennreal.of_real ∥f a∥ := -begin - by_cases hfm : measurable f, - by_cases hfi : integrable f, - rotate, - { rw [integral_eq_zero_of_non_integrable hfi, _root_.norm_zero, of_real_zero], exact zero_le _ }, - { rw [integral_eq_zero_of_non_measurable hfm, _root_.norm_zero, of_real_zero], exact zero_le _ }, - rw [integral, dif_pos], - rotate, { exact ⟨hfm, hfi⟩ }, - calc ennreal.of_real ∥l1.integral (l1.of_fun f hfm hfi)∥ ≤ (ennreal.of_real ∥l1.of_fun f hfm hfi∥) : - of_real_le_of_real $ l1.norm_integral_le _ - ... = (ennreal.of_real $ ennreal.to_real $ ∫⁻ a, ennreal.of_real $ ∥(l1.of_fun f hfm hfi).to_fun a∥) : - by { rw l1.norm_eq_norm_to_fun } - ... = (ennreal.of_real $ ennreal.to_real $ ∫⁻ a, ennreal.of_real ∥f a∥) : - begin - congr' 2, - apply lintegral_congr_ae, - filter_upwards [l1.to_fun_of_fun f hfm hfi], - simp only [mem_set_of_eq], - assume a h, - rw h - end - ... = (∫⁻ a, ennreal.of_real ∥f a∥) : - by { rw of_real_to_real, rw ← lt_top_iff_ne_top, rwa ← integrable_iff_norm } -end - lemma norm_integral_le_lintegral_norm (f : α → β) : ∥integral f∥ ≤ ennreal.to_real (∫⁻ a, ennreal.of_real ∥f a∥) := begin + by_cases hfm : measurable f, by_cases hfi : integrable f, - rotate, - { rw [integral_eq_zero_of_non_integrable hfi, _root_.norm_zero], exact to_real_nonneg }, - have := (to_real_le_to_real _ _).2 (of_real_norm_integral_le_lintegral_norm f), - { rwa to_real_of_real (norm_nonneg _) at this }, - { exact of_real_ne_top }, - { rw ← lt_top_iff_ne_top, rwa ← integrable_iff_norm } + { rw [integral, ← l1.norm_of_fun_eq_lintegral_norm f hfm hfi, dif_pos], + exact l1.norm_integral_le _, exact ⟨hfm, hfi⟩ }, + { rw [integral_eq_zero_of_non_integrable hfi, _root_.norm_zero], + exact to_real_nonneg }, + { rw [integral_eq_zero_of_non_measurable hfm, _root_.norm_zero], + exact to_real_nonneg } end /-- Lebesgue dominated convergence theorem provides sufficient conditions under which almost @@ -960,6 +1182,114 @@ begin exact norm_integral_le_lintegral_norm _ } end +/-- The Bochner integral of a real-valued function `f : α → ℝ` is the difference between the + integral of the positive part of `f` and the integral of the negative part of `f`. -/ +lemma integral_eq_lintegral_max_sub_lintegral_min {f : α → ℝ} + (hfm : measurable f) (hfi : integrable f) : integral f = + 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 hfm hfi in +-- Go to the `L¹` space +have eq₁ : ennreal.to_real (∫⁻ a, ennreal.of_real $ max (f a) 0) = ∥l1.pos_part f₁∥ := +begin + rw l1.norm_eq_norm_to_fun, + congr' 1, + apply lintegral_congr_ae, + filter_upwards [l1.pos_part_to_fun f₁, l1.to_fun_of_fun f hfm hfi], + simp only [mem_set_of_eq], + assume a h₁ h₂, + rw [h₁, h₂, real.norm_eq_abs, abs_of_nonneg], + exact le_max_right _ _ +end, +-- Go to the `L¹` space +have eq₂ : ennreal.to_real (∫⁻ a, ennreal.of_real $ -min (f a) 0) = ∥l1.neg_part f₁∥ := +begin + rw l1.norm_eq_norm_to_fun, + congr' 1, + apply lintegral_congr_ae, + filter_upwards [l1.neg_part_to_fun_eq_min f₁, l1.to_fun_of_fun f hfm hfi], + simp only [mem_set_of_eq], + assume a h₁ h₂, + rw [h₁, h₂, real.norm_eq_abs, abs_of_nonneg], + rw [min_eq_neg_max_neg_neg, _root_.neg_neg, neg_zero], + exact le_max_right _ _ +end, +begin + rw [eq₁, eq₂, integral, dif_pos], + exact l1.integral_eq_norm_pos_part_sub _, + { exact ⟨hfm, hfi⟩ } +end + +lemma integral_eq_lintegral_of_nonneg_ae {f : α → ℝ} (hf : ∀ₘ a, 0 ≤ f a) (hfm : measurable f) : + integral f = ennreal.to_real (∫⁻ a, ennreal.of_real $ f a) := +begin + by_cases hfi : integrable f, + { rw integral_eq_lintegral_max_sub_lintegral_min hfm hfi, + have h_min : (∫⁻ a, ennreal.of_real (-min (f a) 0)) = 0, + { rw lintegral_eq_zero_iff, + { filter_upwards [hf], + simp only [mem_set_of_eq], + assume a h, + simp only [min_eq_right h, neg_zero, ennreal.of_real_zero] }, + { refine measurable_of_real.comp + ((measurable.neg measurable_id).comp $ measurable.min hfm measurable_const) } }, + have h_max : (∫⁻ a, ennreal.of_real (max (f a) 0)) = (∫⁻ a, ennreal.of_real $ f a), + { apply lintegral_congr_ae, + filter_upwards [hf], + simp only [mem_set_of_eq], + assume a h, + rw max_eq_left h }, + rw [h_min, h_max, zero_to_real, _root_.sub_zero] }, + { rw integral_eq_zero_of_non_integrable hfi, + rw [integrable_iff_norm, lt_top_iff_ne_top, ne.def, not_not] at hfi, + have : (∫⁻ (a : α), ennreal.of_real (f a)) = (∫⁻ a, ennreal.of_real ∥f a∥), + { apply lintegral_congr_ae, + filter_upwards [hf], + simp only [mem_set_of_eq], + assume a h, + rw [real.norm_eq_abs, abs_of_nonneg h] }, + rw [this, hfi], refl } +end + +lemma integral_nonneg_of_nonneg_ae {f : α → ℝ} (hf : ∀ₘ a, 0 ≤ f a) : 0 ≤ integral f := +begin + by_cases hfm : measurable f, + { rw integral_eq_lintegral_of_nonneg_ae hf hfm, exact to_real_nonneg }, + { rw integral_eq_zero_of_non_measurable hfm } +end + +lemma integral_nonpos_of_nonpos_ae {f : α → ℝ} (hf : ∀ₘ a, f a ≤ 0) : integral f ≤ 0 := +begin + have hf : ∀ₘ a, 0 ≤ (-f) a, + { filter_upwards [hf], simp only [mem_set_of_eq], assume a h, rwa [pi.neg_apply, neg_nonneg] }, + have : 0 ≤ integral (-f) := integral_nonneg_of_nonneg_ae hf, + rwa [integral_neg, neg_nonneg] at this, +end + +lemma integral_le_integral_of_le_ae {f g : α → ℝ} (hfm : measurable f) (hfi : integrable f) + (hgm : measurable g) (hgi : integrable g) (h : ∀ₘ a, f a ≤ g a) : integral f ≤ integral g := +le_of_sub_nonneg +begin + rw ← integral_sub hgm hgi hfm hfi, + apply integral_nonneg_of_nonneg_ae, + filter_upwards [h], + simp only [mem_set_of_eq], + assume a, + exact sub_nonneg_of_le +end + +lemma norm_integral_le_integral_norm (f : α → β) : ∥integral f∥ ≤ ∫ a, ∥f a∥ := +have le_ae : ∀ₘ (a : α), 0 ≤ ∥f a∥ := by filter_upwards [] λa, norm_nonneg _, +classical.by_cases +( λh : measurable f, + calc ∥integral f∥ ≤ ennreal.to_real (∫⁻ a, ennreal.of_real ∥f a∥) : norm_integral_le_lintegral_norm _ + ... = ∫ a, ∥f a∥ : (integral_eq_lintegral_of_nonneg_ae le_ae $ measurable_norm h).symm ) +( λh : ¬measurable f, + begin + rw [integral_eq_zero_of_non_measurable h, _root_.norm_zero], + exact integral_nonneg_of_nonneg_ae le_ae + end ) + end properties mk_simp_attribute integral_simps "Simp set for integral rules." diff --git a/src/measure_theory/borel_space.lean b/src/measure_theory/borel_space.lean index 7bf07beb283fd..3eef27f58cfee 100644 --- a/src/measure_theory/borel_space.lean +++ b/src/measure_theory/borel_space.lean @@ -23,7 +23,6 @@ open_locale classical universes u v w x y variables {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} {ι : Sort y} {s t u : set α} -namespace measure_theory open measurable_space topological_space @[instance, priority 900] def borel (α : Type u) [topological_space α] : measurable_space α := @@ -136,13 +135,13 @@ lemma is_measurable_interior : is_measurable (interior s) := is_measurable_of_is_open is_open_interior lemma is_measurable_ball [metric_space β] {x : β} {ε : ℝ} : is_measurable (metric.ball x ε) := -measure_theory.is_measurable_of_is_open metric.is_open_ball +is_measurable_of_is_open metric.is_open_ball lemma is_measurable_of_is_closed (h : is_closed s) : is_measurable s := is_measurable.compl_iff.1 $ is_measurable_of_is_open h lemma is_measurable_singleton [t1_space α] {x : α} : is_measurable ({x} : set α) := -measure_theory.is_measurable_of_is_closed is_closed_singleton +is_measurable_of_is_closed is_closed_singleton lemma is_measurable_closure : is_measurable (closure s) := is_measurable_of_is_closed is_closed_closure @@ -189,10 +188,10 @@ begin apply measurable.comp, { rw borel_prod, exact measurable_of_continuous h }, - { exact measurable_prod_mk hf hg } + { exact measurable.prod_mk hf hg } end -lemma measurable_add +lemma measurable.add [add_monoid α] [topological_add_monoid α] [second_countable_topology α] [measurable_space β] {f : β → α} {g : β → α} : measurable f → measurable g → measurable (λa, f a + g a) := measurable_of_continuous2 continuous_add @@ -202,9 +201,9 @@ lemma measurable_finset_sum {ι : Type*} {f : ι → β → α} (s : finset ι) (hf : ∀i, measurable (f i)) : measurable (λa, s.sum (λi, f i a)) := finset.induction_on s (by simpa using measurable_const) - (assume i s his ih, by simpa [his] using measurable_add (hf i) ih) + (assume i s his ih, by simpa [his] using measurable.add (hf i) ih) -lemma measurable_neg +lemma measurable.neg [add_group α] [topological_add_group α] [measurable_space β] {f : β → α} (hf : measurable f) : measurable (λa, - f a) := (measurable_of_continuous continuous_neg).comp hf @@ -215,24 +214,24 @@ lemma measurable_neg_iff iff.intro begin assume h, - have := measurable_neg h, + have := measurable.neg h, convert this, funext, simp only [pi.neg_apply, _root_.neg_neg] end -$ measurable_neg +$ measurable.neg -lemma measurable_sub +lemma measurable.sub [add_group α] [topological_add_group α] [second_countable_topology α] [measurable_space β] {f : β → α} {g : β → α} : measurable f → measurable g → measurable (λa, f a - g a) := measurable_of_continuous2 continuous_sub -lemma measurable_mul +lemma measurable.mul [monoid α] [topological_monoid α] [second_countable_topology α] [measurable_space β] {f : β → α} {g : β → α} : measurable f → measurable g → measurable (λa, f a * g a) := measurable_of_continuous2 continuous_mul -lemma measurable_le {α β} +lemma is_measurable_le {α β} [topological_space α] [partial_order α] [ordered_topology α] [second_countable_topology α] [measurable_space β] {f : β → α} {g : β → α} (hf : measurable f) (hg : measurable g) : is_measurable {a | f a ≤ g a} := @@ -241,9 +240,21 @@ have is_measurable {p : α × α | p.1 ≤ p.2}, show is_measurable {a | (f a, g a).1 ≤ (f a, g a).2}, begin refine measurable.preimage _ this, - exact measurable_prod_mk hf hg + exact measurable.prod_mk hf hg end +lemma measurable.max {α β} + [topological_space α] [decidable_linear_order α] [ordered_topology α] [second_countable_topology α] + [measurable_space β] {f : β → α} {g : β → α} (hf : measurable f) (hg : measurable g) : + measurable (λa, max (f a) (g a)) := +measurable.if (is_measurable_le hf hg) hg hf + +lemma measurable.min {α β} + [topological_space α] [decidable_linear_order α] [ordered_topology α] [second_countable_topology α] + [measurable_space β] {f : β → α} {g : β → α} (hf : measurable f) (hg : measurable g) : + measurable (λa, min (f a) (g a)) := +measurable.if (is_measurable_le hf hg) hf hg + -- generalize lemma measurable_coe_int_real : measurable (λa, a : ℤ → ℝ) := assume s (hs : is_measurable s), by trivial @@ -327,16 +338,14 @@ classical.by_cases end -end measure_theory - def homemorph.to_measurable_equiv [topological_space α] [topological_space β] (h : α ≃ₜ β) : measurable_equiv α β := { to_equiv := h.to_equiv, - measurable_to_fun := measure_theory.measurable_of_continuous h.continuous_to_fun, - measurable_inv_fun := measure_theory.measurable_of_continuous h.continuous_inv_fun } + measurable_to_fun := measurable_of_continuous h.continuous_to_fun, + measurable_inv_fun := measurable_of_continuous h.continuous_inv_fun } namespace real -open measure_theory measurable_space +open measurable_space lemma borel_eq_generate_from_Ioo_rat : borel ℝ = generate_from (⋃(a b : ℚ) (h : a < b), {Ioo a b}) := @@ -369,17 +378,17 @@ end end real namespace nnreal -open filter measure_theory +open filter -lemma measurable_add [measurable_space α] {f : α → nnreal} {g : α → nnreal} : +lemma measurable.add [measurable_space α] {f : α → nnreal} {g : α → nnreal} : measurable f → measurable g → measurable (λa, f a + g a) := measurable_of_continuous2 continuous_add -lemma measurable_sub [measurable_space α] {f g: α → nnreal} +lemma measurable.sub [measurable_space α] {f g: α → nnreal} (hf : measurable f) (hg : measurable g) : measurable (λ a, f a - g a) := measurable_of_continuous2 continuous_sub hf hg -lemma measurable_mul [measurable_space α] {f : α → nnreal} {g : α → nnreal} : +lemma measurable.mul [measurable_space α] {f : α → nnreal} {g : α → nnreal} : measurable f → measurable g → measurable (λa, f a * g a) := measurable_of_continuous2 continuous_mul @@ -389,7 +398,7 @@ measurable_of_continuous nnreal.continuous_of_real end nnreal namespace ennreal -open filter measure_theory +open filter lemma measurable_coe : measurable (coe : nnreal → ennreal) := measurable_of_continuous (continuous_coe.2 continuous_id) @@ -407,7 +416,7 @@ def ennreal_equiv_nnreal : measurable_equiv {r : ennreal | r < ⊤} nnreal := simp [continuous_at, nhds_subtype_eq_comap], refine tendsto.comp (tendsto_to_nnreal (ne_of_lt hr)) tendsto_comap end, - measurable_inv_fun := measurable_subtype_mk measurable_coe } + measurable_inv_fun := measurable.subtype_mk measurable_coe } lemma measurable_of_measurable_nnreal [measurable_space α] {f : ennreal → α} (h : measurable (λp:nnreal, f p)) : measurable f := @@ -449,21 +458,21 @@ begin { show measurable (λp:nnreal × nnreal, f p.1 p.2), exact h₁ }, { show measurable (λp:nnreal × unit, f p.1 ⊤), - exact h₃.comp (measurable_fst measurable_id) }, + exact h₃.comp (measurable.fst measurable_id) }, { show measurable ((λp:nnreal, f ⊤ p) ∘ (λp:unit × nnreal, p.2)), - exact h₂.comp (measurable_snd measurable_id) }, + exact h₂.comp (measurable.snd measurable_id) }, { show measurable (λp:unit × unit, f ⊤ ⊤), exact measurable_const } end, -this.comp (measurable_prod_mk hg hh) +this.comp (measurable.prod_mk hg hh) -lemma measurable_mul {α : Type*} [measurable_space α] {f g : α → ennreal} : +lemma measurable.mul {α : Type*} [measurable_space α] {f g : α → ennreal} : measurable f → measurable g → measurable (λa, f a * g a) := begin refine measurable_of_measurable_nnreal_nnreal (*) _ _ _, { simp only [ennreal.coe_mul.symm], exact measurable_coe.comp - (measurable_mul (measurable_fst measurable_id) (measurable_snd measurable_id)) }, + (measurable.mul (measurable.fst measurable_id) (measurable.snd measurable_id)) }, { simp [top_mul], exact measurable.if (is_measurable_of_is_closed $ is_closed_eq continuous_id continuous_const) @@ -476,24 +485,24 @@ begin measurable_const } end -lemma measurable_add {α : Type*} [measurable_space α] {f g : α → ennreal} : +lemma measurable.add {α : Type*} [measurable_space α] {f g : α → ennreal} : measurable f → measurable g → measurable (λa, f a + g a) := begin refine measurable_of_measurable_nnreal_nnreal (+) _ _ _, { simp only [ennreal.coe_add.symm], exact measurable_coe.comp - (measurable_add (measurable_fst measurable_id) (measurable_snd measurable_id)) }, + (measurable.add (measurable.fst measurable_id) (measurable.snd measurable_id)) }, { simp [measurable_const] }, { simp [measurable_const] } end -lemma measurable_sub {α : Type*} [measurable_space α] {f g : α → ennreal} : +lemma measurable.sub {α : Type*} [measurable_space α] {f g : α → ennreal} : measurable f → measurable g → measurable (λa, f a - g a) := begin refine measurable_of_measurable_nnreal_nnreal (has_sub.sub) _ _ _, { simp only [ennreal.coe_sub.symm], exact measurable_coe.comp - (nnreal.measurable_sub (measurable_fst measurable_id) (measurable_snd measurable_id)) }, + (nnreal.measurable.sub (measurable.fst measurable_id) (measurable.snd measurable_id)) }, { simp [measurable_const] }, { simp [measurable_const] } end @@ -548,7 +557,7 @@ end lemma measurable_dist {α : Type*} [metric_space α] [second_countable_topology α] [measurable_space β] {f g : β → α} (hf : measurable f) (hg : measurable g) : measurable (λ b, dist (f b) (g b)) := -measurable.comp measurable_dist' (measurable_prod_mk hf hg) +measurable.comp measurable_dist' (measurable.prod_mk hf hg) lemma measurable_nndist' {α : Type*} [metric_space α] [second_countable_topology α] : measurable (λp:α×α, nndist p.1 p.2) := @@ -561,7 +570,7 @@ end lemma measurable_nndist {α : Type*} [metric_space α] [second_countable_topology α] [measurable_space β] {f g : β → α} (hf : measurable f) (hg : measurable g) : measurable (λ b, nndist (f b) (g b)) := -measurable.comp measurable_nndist' (measurable_prod_mk hf hg) +measurable.comp measurable_nndist' (measurable.prod_mk hf hg) lemma measurable_edist' {α : Type*} [emetric_space α] [second_countable_topology α] : measurable (λp:α×α, edist p.1 p.2) := @@ -574,7 +583,7 @@ end lemma measurable_edist {α : Type*} [emetric_space α] [second_countable_topology α] [measurable_space β] {f g : β → α} (hf : measurable f) (hg : measurable g) : measurable (λ b, edist (f b) (g b)) := -measurable.comp measurable_edist' (measurable_prod_mk hf hg) +measurable.comp measurable_edist' (measurable.prod_mk hf hg) lemma measurable_norm' {α : Type*} [normed_group α] : measurable (norm : α → ℝ) := measurable_of_continuous continuous_norm diff --git a/src/measure_theory/category/Meas.lean b/src/measure_theory/category/Meas.lean index 6005896df73dd..9c9d5adbe3eb0 100644 --- a/src/measure_theory/category/Meas.lean +++ b/src/measure_theory/category/Meas.lean @@ -88,8 +88,8 @@ end Meas instance Top.has_forget_to_Meas : has_forget₂ Top.{u} Meas.{u} := bundled_hom.mk_has_forget₂ - @measure_theory.borel - (λ X Y f, ⟨f.1, measure_theory.measurable_of_continuous f.2⟩) + borel + (λ X Y f, ⟨f.1, measurable_of_continuous f.2⟩) (by intros; refl) /-- The Borel functor, the canonical embedding of topological spaces into measurable spaces. -/ diff --git a/src/measure_theory/giry_monad.lean b/src/measure_theory/giry_monad.lean index 036a08500d8fb..b37bcea79f011 100644 --- a/src/measure_theory/giry_monad.lean +++ b/src/measure_theory/giry_monad.lean @@ -82,7 +82,7 @@ measurable.supr $ assume n, dunfold simple_func.integral, refine measurable_finset_sum (simple_func.eapprox f n).range _, assume i, - refine ennreal.measurable_mul measurable_const _, + refine ennreal.measurable.mul measurable_const _, exact measurable_coe ((simple_func.eapprox f n).preimage_measurable _) end @@ -133,12 +133,12 @@ begin transitivity, apply lintegral_supr, { exact assume n, - measurable_finset_sum _ (assume r, ennreal.measurable_mul measurable_const (hf _ _)) }, + measurable_finset_sum _ (assume r, ennreal.measurable.mul measurable_const (hf _ _)) }, { exact hm }, congr, funext n, transitivity, apply lintegral_finset_sum, - { exact assume r, ennreal.measurable_mul measurable_const (hf _ _) }, + { exact assume r, ennreal.measurable.mul measurable_const (hf _ _) }, congr, funext r, apply lintegral_const_mul, exact hf _ _ }, diff --git a/src/measure_theory/integration.lean b/src/measure_theory/integration.lean index 7f16dda970841..0ea87f74d1349 100644 --- a/src/measure_theory/integration.lean +++ b/src/measure_theory/integration.lean @@ -779,7 +779,7 @@ begin refine inter_subset_inter (subset.refl _) _, assume x hx, exact le_trans hx (h_mono h x) }, have h_meas : ∀n, is_measurable {a : α | ⇑(map c rs) a ≤ f n a} := - assume n, measurable_le (simple_func.measurable _) (hf n), + assume n, is_measurable_le (simple_func.measurable _) (hf n), calc (r:ennreal) * integral (s.map c) = (rs.map c).range.sum (λr, r * volume ((rs.map c) ⁻¹' {r})) : by rw [← const_mul_integral, integral, eq_rs] ... ≤ (rs.map c).range.sum (λr, r * volume (⋃n, (rs.map c) ⁻¹' {r} ∩ {a | r ≤ f n a})) : @@ -851,7 +851,7 @@ calc (∫⁻ a, f a + g a) = begin rw [lintegral_supr], { congr, funext n, rw [← simple_func.add_integral, ← simple_func.lintegral_eq_integral], refl }, - { assume n, exact measurable_add (eapprox f n).measurable (eapprox g n).measurable }, + { assume n, exact measurable.add (eapprox f n).measurable (eapprox g n).measurable }, { assume i j h a, exact add_le_add' (monotone_eapprox _ h _) (monotone_eapprox _ h _) } end ... = (⨆n, (eapprox f n).integral) + (⨆n, (eapprox g n).integral) : @@ -1037,7 +1037,7 @@ lemma lintegral_sub {f g : α → ennreal} (hf : measurable f) (hg : measurable begin rw [← ennreal.add_right_inj hg_fin, ennreal.sub_add_cancel_of_le (lintegral_le_lintegral_ae h_le), - ← lintegral_add (ennreal.measurable_sub hf hg) hg], + ← lintegral_add (ennreal.measurable.sub hf hg) hg], show (∫⁻ (a : α), f a - g a + g a) = ∫⁻ (a : α), f a, apply lintegral_congr_ae, filter_upwards [h_le], simp only [add_comm, mem_set_of_eq], assume a ha, exact ennreal.add_sub_cancel_of_le ha @@ -1064,7 +1064,7 @@ calc ... = ∫⁻ a, ⨆n, f 0 a - f n a : congr rfl (funext (assume a, ennreal.sub_infi)) ... = ⨆n, ∫⁻ a, f 0 a - f n a : lintegral_supr_ae - (assume n, ennreal.measurable_sub (h_meas 0) (h_meas n)) + (assume n, ennreal.measurable.sub (h_meas 0) (h_meas n)) (assume n, by filter_upwards [h_mono n] assume a ha, ennreal.sub_le_sub (le_refl _) ha) ... = ⨆n, lintegral (f 0) - ∫⁻ a, f n a : diff --git a/src/measure_theory/l1_space.lean b/src/measure_theory/l1_space.lean index 9a995a63a24e6..d321d65770946 100644 --- a/src/measure_theory/l1_space.lean +++ b/src/measure_theory/l1_space.lean @@ -7,20 +7,20 @@ Authors: Zhouhang Zhou import measure_theory.ae_eq_fun /-! -# Integrable functions and L1 space +# Integrable functions and `L¹` space 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 L1 of equivalence classes of integrable functions under the relation -of being almost everywhere equal is defined as a subspace of the space L0. See the file -`src/measure_theory/ae_eq_fun.lean` for information on L0 space. +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. ## Notation -* `α →₁ β` is the type of L1 space, where `α` is a `measure_space` and `β` is a `normed_group` with - a `second_countable_topology`. `f : α →ₘ β` is a "function" in L1. In comments, `[f]` is also used - to denote an L1 function. +* `α →₁ β` 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. `₁` can be typed as `\1`. @@ -29,13 +29,13 @@ of being almost everywhere equal is defined as a subspace of the space L0. See t * Let `f : α → β` be a function, where `α` is a `measure_space` and `β` a `normed_group`. Then `f` is called `integrable` if `(∫⁻ a, nnnorm (f a)) < ⊤` holds. -* The space L1 is defined as a subspace of L0 : - An `ae_eq_fun` `[f] : α →ₘ β` is in the space L1 if `edist [f] 0 < ⊤`, which means - `(∫⁻ a, edist (f a) 0) < ⊤` if we expand the definition of `edist` in L0. +* 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 -L1, as a subspace, inherits most of the structures of L0. +`L¹`, as a subspace, inherits most of the structures of `L⁰`. ## Implementation notes @@ -60,7 +60,7 @@ open set lattice filter topological_space ennreal emetric universes u v w variables {α : Type u} [measure_space α] -variables {β : Type v} [normed_group β] +variables {β : Type v} [normed_group β] {γ : Type w} [normed_group γ] /-- A function is `integrable` if the integral of its pointwise norm is less than infinity. -/ def integrable (f : α → β) : Prop := (∫⁻ a, nnnorm (f a)) < ⊤ @@ -104,10 +104,23 @@ end lemma integrable_iff_of_ae_eq {f g : α → β} (h : ∀ₘ a, f a = g a) : integrable f ↔ integrable g := iff.intro (λhf, integrable_of_ae_eq hf h) (λhg, integrable_of_ae_eq hg (all_ae_eq_symm h)) +lemma integrable_of_le_ae {f : α → β} {g : α → γ} (h : ∀ₘ a, ∥f a∥ ≤ ∥g a∥) (hg : integrable g) : + integrable f := +begin + simp only [integrable_iff_norm] at *, + calc (∫⁻ a, ennreal.of_real ∥f a∥) ≤ (∫⁻ (a : α), ennreal.of_real ∥g a∥) : + lintegral_le_lintegral_ae (by { filter_upwards [h], assume a h, exact of_real_le_of_real h }) + ... < ⊤ : hg +end + lemma lintegral_nnnorm_eq_lintegral_edist (f : α → β) : (∫⁻ a, nnnorm (f a)) = ∫⁻ a, edist (f a) 0 := by { congr, funext, rw edist_eq_coe_nnnorm } +lemma lintegral_norm_eq_lintegral_edist (f : α → β) : + (∫⁻ a, ennreal.of_real ∥f a∥) = ∫⁻ a, edist (f a) 0 := +by { congr, funext, rw [of_real_norm_eq_coe_nnnorm, edist_eq_coe_nnnorm] } + lemma lintegral_edist_triangle [second_countable_topology β] {f g h : α → β} (hf : measurable f) (hg : measurable g) (hh : measurable h) : (∫⁻ a, edist (f a) (g a)) ≤ (∫⁻ a, edist (f a) (h a)) + ∫⁻ a, edist (g a) (h a) := @@ -132,11 +145,11 @@ lt_of_le_of_lt lemma integrable_zero : integrable (0 : α → β) := by { have := coe_lt_top, simpa [integrable] } -lemma lintegral_nnnorm_add {f g : α → β} (hf : measurable f) (hg : measurable g) : +lemma lintegral_nnnorm_add {f : α → β} {g : α → γ} (hf : measurable f) (hg : measurable g) : (∫⁻ a, nnnorm (f a) + nnnorm (g a)) = (∫⁻ a, nnnorm (f a)) + ∫⁻ a, nnnorm (g a) := lintegral_add (measurable_coe_nnnorm hf) (measurable_coe_nnnorm hg) -lemma integrable_add {f g : α → β} (hfm : measurable f) (hgm : measurable g) : +lemma integrable.add {f g : α → β} (hfm : measurable f) (hgm : measurable g) : integrable f → integrable g → integrable (f + g) := assume hfi hgi, calc @@ -151,7 +164,7 @@ lemma lintegral_nnnorm_neg {f : α → β} : (∫⁻ (a : α), ↑(nnnorm ((-f) a))) = ∫⁻ (a : α), ↑(nnnorm ((f) a)) := lintegral_congr_ae $ by { filter_upwards [], simp } -lemma integrable_neg {f : α → β} : integrable f → integrable (-f) := +lemma integrable.neg {f : α → β} : integrable f → integrable (-f) := assume hfi, calc _ = _ : lintegral_nnnorm_neg ... < ⊤ : hfi @@ -159,17 +172,17 @@ lemma integrable_neg_iff (f : α → β) : integrable (-f) ↔ integrable f := begin split, { assume h, - have := integrable_neg h, + have := integrable.neg h, rwa _root_.neg_neg at this }, - exact integrable_neg + exact integrable.neg end -lemma integrable_sub {f g : α → β} (hf : measurable f) (hg : measurable g) : +lemma integrable.sub {f g : α → β} (hf : measurable f) (hg : measurable g) : integrable f → integrable g → integrable (f - g) := λ hfi hgi, - by { rw sub_eq_add_neg, refine integrable_add hf (measurable_neg hg) hfi (integrable_neg hgi) } + by { rw sub_eq_add_neg, refine integrable.add hf (measurable.neg hg) hfi (integrable.neg hgi) } -lemma integrable_norm {f : α → β} (hfi : integrable f) : integrable (λa, ∥f a∥) := +lemma integrable.norm {f : α → β} (hfi : integrable f) : integrable (λa, ∥f a∥) := have eq : (λa, (nnnorm ∥f a∥ : ennreal)) = λa, (nnnorm (f a) : ennreal), by { funext, rw nnnorm_norm }, by { rwa [integrable, eq] } @@ -286,7 +299,7 @@ begin -- Using the dominated convergence theorem. refine tendsto_lintegral_of_dominated_convergence _ hb _ _, -- Show `λa, ∥f a - F n a∥` is measurable for all `n` - { exact λn, measurable.comp measurable_of_real (measurable_norm (measurable_sub (F_measurable n) + { exact λn, measurable.comp measurable_of_real (measurable_norm (measurable.sub (F_measurable n) f_measurable)) }, -- Show `2 * bound` is integrable { rw integrable_iff_of_real at bound_integrable, @@ -300,30 +313,65 @@ end end dominated_convergence +section pos_part +/-! Lemmas used for defining the positive part of a `L¹` function -/ + +lemma integrable.max_zero {f : α → ℝ} (hf : integrable f) : integrable (λa, max (f a) 0) := +begin + simp only [integrable_iff_norm] at *, + calc (∫⁻ a, ennreal.of_real ∥max (f a) 0∥) ≤ (∫⁻ (a : α), ennreal.of_real ∥f a∥) : + lintegral_le_lintegral _ _ + begin + assume a, + apply of_real_le_of_real, + simp only [real.norm_eq_abs], + calc abs (max (f a) 0) = max (f a) 0 : by { rw abs_of_nonneg, apply le_max_right } + ... ≤ abs (f a) : max_le (le_abs_self _) (abs_nonneg _) + end + ... < ⊤ : hf +end + +lemma integrable.min_zero {f : α → ℝ} (hf : integrable f) : integrable (λa, min (f a) 0) := +begin + have : (λa, min (f a) 0) = (λa, - max (-f a) 0), + { funext, rw [min_eq_neg_max_neg_neg, neg_zero] }, + rw this, + exact (integrable.max_zero hf.neg).neg, +end + +end pos_part + section normed_space variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 β] -lemma integrable_smul (c : 𝕜) {f : α → β} : integrable f → integrable (c • f) := +lemma integrable.smul (c : 𝕜) {f : α → β} : integrable f → integrable (c • f) := begin simp only [integrable], assume hfi, calc - (∫⁻ (a : α), nnnorm ((c • f) a)) = (∫⁻ (a : α), (nnnorm c) * nnnorm (f a)) : by - { apply lintegral_congr_ae, filter_upwards [], assume a, simp [nnnorm_smul] } + (∫⁻ (a : α), nnnorm ((c • f) a)) = (∫⁻ (a : α), (nnnorm c) * nnnorm (f a)) : + begin + apply lintegral_congr_ae, + filter_upwards [], + assume a, + simp only [nnnorm_smul, set.mem_set_of_eq, pi.smul_apply, ennreal.coe_mul] + end ... < ⊤ : begin rw lintegral_const_mul', apply mul_lt_top, - { simp }, { exact hfi }, { simp } + { exact coe_lt_top }, + { exact hfi }, + { simp only [ennreal.coe_ne_top, ne.def, not_false_iff] } end end -lemma integrable_smul_iff {c : 𝕜} (hc : c ≠ 0) (f : α → β) : integrable (c • f) ↔ integrable f := +lemma integrable.smul_iff {c : 𝕜} (hc : c ≠ 0) (f : α → β) : integrable (c • f) ↔ integrable f := begin split, { assume h, - have := integrable_smul c⁻¹ h, + have := integrable.smul c⁻¹ h, rwa [smul_smul, inv_mul_cancel hc, one_smul] at this }, - exact integrable_smul _ + exact integrable.smul _ end end normed_space @@ -347,29 +395,29 @@ local attribute [simp] integrable_mk lemma integrable_zero : integrable (0 : α →ₘ β) := mem_ball_self coe_lt_top -lemma integrable_add : ∀ {f g : α →ₘ β}, integrable f → integrable g → integrable (f + g) := +lemma integrable.add : ∀ {f g : α →ₘ β}, integrable f → integrable g → integrable (f + g) := begin rintros ⟨f, hf⟩ ⟨g, hg⟩, - have := measure_theory.integrable_add hf hg, + have := measure_theory.integrable.add hf hg, simpa [mem_ball, zero_def] end -lemma integrable_neg : ∀ {f : α →ₘ β}, integrable f → integrable (-f) := -by { rintros ⟨f, hf⟩, have := measure_theory.integrable_neg, simpa } +lemma integrable.neg : ∀ {f : α →ₘ β}, integrable f → integrable (-f) := +by { rintros ⟨f, hf⟩, have := measure_theory.integrable.neg, simpa } -lemma integrable_sub : ∀ {f g : α →ₘ β}, integrable f → integrable g → integrable (f - g) := -by { rintros ⟨f, hf⟩ ⟨g, hg⟩, have := measure_theory.integrable_sub hf hg, simpa [mem_ball, zero_def] } +lemma integrable.sub : ∀ {f g : α →ₘ β}, integrable f → integrable g → integrable (f - g) := +by { rintros ⟨f, hf⟩ ⟨g, hg⟩, have := measure_theory.integrable.sub hf hg, simpa [mem_ball, zero_def] } protected lemma is_add_subgroup : is_add_subgroup (ball (0 : α →ₘ β) ⊤) := { zero_mem := integrable_zero, - add_mem := λ _ _, integrable_add, - neg_mem := λ _, integrable_neg } + add_mem := λ _ _, integrable.add, + neg_mem := λ _, integrable.neg } section normed_space variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 β] -lemma integrable_smul : ∀ {c : 𝕜} {f : α →ₘ β}, integrable f → integrable (c • f) := -by { assume c, rintros ⟨f, hf⟩, simpa using integrable_smul _ } +lemma integrable.smul : ∀ {c : 𝕜} {f : α →ₘ β}, integrable f → integrable (c • f) := +by { assume c, rintros ⟨f, hf⟩, simpa using integrable.smul _ } end normed_space @@ -399,24 +447,24 @@ iff.intro (l1.eq) (congr_arg coe) /- TODO : order structure of l1-/ -/-- L1 space forms a `emetric_space`, with the emetric being inherited from almost everywhere +/-- `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 -/-- L1 space forms a `metric_space`, with the metric being inherited from almost everywhere +/-- `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 ⊤ instance : add_comm_group (α →₁ β) := subtype.add_comm_group -@[simp] lemma coe_zero : ((0 : α →₁ β) : α →ₘ β) = 0 := rfl -@[simp] lemma coe_add (f g : α →₁ β) : ((f + g : α →₁ β) : α →ₘ β) = f + g := rfl -@[simp] lemma coe_neg (f : α →₁ β) : ((-f : α →₁ β) : α →ₘ β) = -f := rfl -@[simp] lemma coe_sub (f g : α →₁ β) : ((f - g : α →₁ β) : α →ₘ β) = f - g := rfl +@[simp, elim_cast] lemma coe_zero : ((0 : α →₁ β) : α →ₘ β) = 0 := rfl +@[simp, move_cast] lemma coe_add (f g : α →₁ β) : ((f + g : α →₁ β) : α →ₘ β) = f + g := rfl +@[simp, move_cast] lemma coe_neg (f : α →₁ β) : ((-f : α →₁ β) : α →ₘ β) = -f := rfl +@[simp, move_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 L1 space is defined to be `∥f∥ = ∫⁻ a, edist (f a) 0`. -/ +/-- 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 @@ -428,9 +476,10 @@ section normed_space variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 β] -instance : has_scalar 𝕜 (α →₁ β) := ⟨λ x f, ⟨x • (f : α →ₘ β), ae_eq_fun.integrable_smul f.2⟩⟩ +instance : has_scalar 𝕜 (α →₁ β) := ⟨λ x f, ⟨x • (f : α →ₘ β), ae_eq_fun.integrable.smul f.2⟩⟩ -@[simp] lemma coe_smul (c : 𝕜) (f : α →₁ β) : ((c • f : α →₁ β) : α →ₘ β) = c • (f : α →ₘ β) := rfl +@[simp, move_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 _ _ }), @@ -469,26 +518,35 @@ by { rw ← l1.eq_iff, simp only [of_fun_eq_mk, mk_eq_mk] } lemma of_fun_zero : of_fun (0 : α → β) (@measurable_const _ _ _ _ (0:β)) integrable_zero = 0 := rfl lemma of_fun_add (f g : α → β) (hfm hfi hgm hgi) : - of_fun (f + g) (measurable_add hfm hgm) (integrable_add hfm hgm hfi hgi) + of_fun (f + g) (measurable.add hfm hgm) (integrable.add hfm hgm hfi hgi) = of_fun f hfm hfi + of_fun g hgm hgi := rfl lemma of_fun_neg (f : α → β) (hfm hfi) : - of_fun (-f) (measurable_neg hfm) (integrable_neg hfi) = - of_fun f hfm hfi := rfl + of_fun (-f) (measurable.neg hfm) (integrable.neg hfi) = - of_fun f hfm hfi := rfl + +lemma of_fun_sub (f g : α → β) (hfm hfi hgm hgi) : + of_fun (f - g) (measurable.sub hfm hgm) (integrable.sub hfm hgm hfi hgi) + = of_fun f hfm hfi - of_fun g hgm hgi := +rfl lemma norm_of_fun (f : α → β) (hfm hfi) : ∥of_fun f hfm hfi∥ = ennreal.to_real (∫⁻ a, edist (f a) 0) := rfl +lemma norm_of_fun_eq_lintegral_norm (f : α → β) (hfm hfi) : + ∥of_fun f hfm hfi∥ = 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 : α → β) (hfm hfi) (k : 𝕜) : - of_fun (k • f) (measurable_smul _ hfm) (integrable_smul _ hfi) = k • of_fun f hfm hfi := rfl + of_fun (k • f) (measurable_smul _ hfm) (integrable.smul _ hfi) = k • of_fun f hfm hfi := rfl end of_fun section to_fun -/-- Find a representative of a L1 function [f] -/ +/-- Find a representative of a `L¹` function [f] -/ @[reducible] protected def to_fun (f : α →₁ β) : α → β := (f : α →ₘ β).to_fun @@ -551,6 +609,76 @@ ae_eq_fun.smul_to_fun _ _ end to_fun +section pos_part + +/-- Positive part of a function in `L¹` space. -/ +def pos_part (f : α →₁ ℝ) : α →₁ ℝ := +⟨ ae_eq_fun.pos_part f, + begin + rw [ae_eq_fun.integrable_to_fun, integrable_iff_of_ae_eq (pos_part_to_fun _)], + exact integrable.max_zero f.integrable + end ⟩ + +/-- Negative part of a function in `L¹` space. -/ +def neg_part (f : α →₁ ℝ) : α →₁ ℝ := pos_part (-f) + +@[move_cast] lemma coe_pos_part (f : α →₁ ℝ) : (f.pos_part : α →ₘ ℝ) = (f : α →ₘ ℝ).pos_part := rfl + +lemma pos_part_to_fun (f : α →₁ ℝ) : ∀ₘ a, (pos_part f).to_fun a = max (f.to_fun a) 0 := +ae_eq_fun.pos_part_to_fun _ + +lemma neg_part_to_fun_eq_max (f : α →₁ ℝ) : ∀ₘ a, (neg_part f).to_fun a = max (- f.to_fun a) 0 := +begin + rw neg_part, + filter_upwards [pos_part_to_fun (-f), neg_to_fun f], + simp only [mem_set_of_eq], + assume a h₁ h₂, + rw [h₁, h₂] +end + +lemma neg_part_to_fun_eq_min (f : α →₁ ℝ) : ∀ₘ a, (neg_part f).to_fun a = - min (f.to_fun a) 0 := +begin + filter_upwards [neg_part_to_fun_eq_max f], + simp only [mem_set_of_eq], + assume a h, + rw [h, min_eq_neg_max_neg_neg, _root_.neg_neg, neg_zero], +end + +lemma norm_le_norm_of_ae_le {f g : α →₁ β} (h : ∀ₘ a, ∥f.to_fun a∥ ≤ ∥g.to_fun a∥) : ∥f∥ ≤ ∥g∥ := +begin + simp only [l1.norm_eq_norm_to_fun], + rw to_real_le_to_real, + { apply lintegral_le_lintegral_ae, + filter_upwards [h], + simp only [mem_set_of_eq], + assume a h, + exact of_real_le_of_real h }, + { rw [← lt_top_iff_ne_top, ← integrable_iff_norm], exact f.integrable }, + { rw [← lt_top_iff_ne_top, ← integrable_iff_norm], exact g.integrable } +end + +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], + simp only [mem_set_of_eq], + assume a h₁ h₂ h₃ h₄, + simp only [real.norm_eq_abs, h₁, h₂, h₃, h₄], + exact abs_max_sub_max_le_abs _ _ _ +end + +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 } + +end pos_part + /- TODO: l1 is a complete space -/ end l1 diff --git a/src/measure_theory/measurable_space.lean b/src/measure_theory/measurable_space.lean index 373184d20d342..16a69eee12763 100644 --- a/src/measure_theory/measurable_space.lean +++ b/src/measure_theory/measurable_space.lean @@ -440,11 +440,11 @@ section subtype instance {p : α → Prop} [m : measurable_space α] : measurable_space (subtype p) := m.comap subtype.val -lemma measurable_subtype_val [measurable_space α] [measurable_space β] {p : β → Prop} +lemma measurable.subtype_val [measurable_space α] [measurable_space β] {p : β → Prop} {f : α → subtype p} (hf : measurable f) : measurable (λa:α, (f a).val) := measurable.comp (measurable_space.comap_le_iff_le_map.mp (le_refl _)) hf -lemma measurable_subtype_mk [measurable_space α] [measurable_space β] {p : β → Prop} +lemma measurable.subtype_mk [measurable_space α] [measurable_space β] {p : β → Prop} {f : α → subtype p} (hf : measurable (λa, (f a).val)) : measurable f := measurable_space.comap_le_iff_le_map.mpr $ by rw [measurable_space.map_comp]; exact hf @@ -477,11 +477,11 @@ section prod instance [m₁ : measurable_space α] [m₂ : measurable_space β] : measurable_space (α × β) := m₁.comap prod.fst ⊔ m₂.comap prod.snd -lemma measurable_fst [measurable_space α] [measurable_space β] [measurable_space γ] +lemma measurable.fst [measurable_space α] [measurable_space β] [measurable_space γ] {f : α → β × γ} (hf : measurable f) : measurable (λa:α, (f a).1) := measurable.comp (measurable_space.comap_le_iff_le_map.mp le_sup_left) hf -lemma measurable_snd [measurable_space α] [measurable_space β] [measurable_space γ] +lemma measurable.snd [measurable_space α] [measurable_space β] [measurable_space γ] {f : α → β × γ} (hf : measurable f) : measurable (λa:α, (f a).2) := measurable.comp (measurable_space.comap_le_iff_le_map.mp le_sup_right) hf @@ -492,13 +492,13 @@ sup_le (by rw [measurable_space.comap_le_iff_le_map, measurable_space.map_comp]; exact hf₁) (by rw [measurable_space.comap_le_iff_le_map, measurable_space.map_comp]; exact hf₂) -lemma measurable_prod_mk [measurable_space α] [measurable_space β] [measurable_space γ] +lemma measurable.prod_mk [measurable_space α] [measurable_space β] [measurable_space γ] {f : α → β} {g : α → γ} (hf : measurable f) (hg : measurable g) : measurable (λa:α, (f a, g a)) := measurable.prod hf hg lemma is_measurable_set_prod [measurable_space α] [measurable_space β] {s : set α} {t : set β} (hs : is_measurable s) (ht : is_measurable t) : is_measurable (set.prod s t) := -is_measurable.inter (measurable_fst measurable_id _ hs) (measurable_snd measurable_id _ ht) +is_measurable.inter (measurable.fst measurable_id _ hs) (measurable.snd measurable_id _ ht) end prod @@ -628,17 +628,17 @@ def prod_congr [measurable_space α] [measurable_space β] [measurable_space γ] (ab : measurable_equiv α β) (cd : measurable_equiv γ δ) : measurable_equiv (α × γ) (β × δ) := { to_equiv := equiv.prod_congr ab.to_equiv cd.to_equiv, - measurable_to_fun := measurable_prod_mk - (ab.measurable_to_fun.comp (measurable_fst measurable_id)) - (cd.measurable_to_fun.comp (measurable_snd measurable_id)), - measurable_inv_fun := measurable_prod_mk - (ab.measurable_inv_fun.comp (measurable_fst measurable_id)) - (cd.measurable_inv_fun.comp (measurable_snd measurable_id)) } + measurable_to_fun := measurable.prod_mk + (ab.measurable_to_fun.comp (measurable.fst measurable_id)) + (cd.measurable_to_fun.comp (measurable.snd measurable_id)), + measurable_inv_fun := measurable.prod_mk + (ab.measurable_inv_fun.comp (measurable.fst measurable_id)) + (cd.measurable_inv_fun.comp (measurable.snd measurable_id)) } def prod_comm [measurable_space α] [measurable_space β] : measurable_equiv (α × β) (β × α) := { to_equiv := equiv.prod_comm α β, - measurable_to_fun := measurable_prod_mk (measurable_snd measurable_id) (measurable_fst measurable_id), - measurable_inv_fun := measurable_prod_mk (measurable_snd measurable_id) (measurable_fst measurable_id) } + measurable_to_fun := measurable.prod_mk (measurable.snd measurable_id) (measurable.fst measurable_id), + measurable_inv_fun := measurable.prod_mk (measurable.snd measurable_id) (measurable.fst measurable_id) } def sum_congr [measurable_space α] [measurable_space β] [measurable_space γ] [measurable_space δ] (ab : measurable_equiv α β) (cd : measurable_equiv γ δ) : @@ -658,22 +658,22 @@ def sum_congr [measurable_space α] [measurable_space β] [measurable_space γ] def set.prod [measurable_space α] [measurable_space β] (s : set α) (t : set β) : measurable_equiv (set.prod s t) (s × t) := { to_equiv := equiv.set.prod s t, - measurable_to_fun := measurable_prod_mk - (measurable_subtype_mk $ measurable_fst $ measurable_subtype_val $ measurable_id) - (measurable_subtype_mk $ measurable_snd $ measurable_subtype_val $ measurable_id), - measurable_inv_fun := measurable_subtype_mk $ measurable_prod_mk - (measurable_subtype_val $ measurable_fst $ measurable_id) - (measurable_subtype_val $ measurable_snd $ measurable_id) } + measurable_to_fun := measurable.prod_mk + (measurable.subtype_mk $ measurable.fst $ measurable.subtype_val $ measurable_id) + (measurable.subtype_mk $ measurable.snd $ measurable.subtype_val $ measurable_id), + measurable_inv_fun := measurable.subtype_mk $ measurable.prod_mk + (measurable.subtype_val $ measurable.fst $ measurable_id) + (measurable.subtype_val $ measurable.snd $ measurable_id) } def set.univ (α : Type*) [measurable_space α] : measurable_equiv (univ : set α) α := { to_equiv := equiv.set.univ α, - measurable_to_fun := measurable_subtype_val measurable_id, - measurable_inv_fun := measurable_subtype_mk measurable_id } + measurable_to_fun := measurable.subtype_val measurable_id, + measurable_inv_fun := measurable.subtype_mk measurable_id } def set.singleton [measurable_space α] (a:α) : measurable_equiv ({a} : set α) unit := { to_equiv := equiv.set.singleton a, measurable_to_fun := measurable_const, - measurable_inv_fun := measurable_subtype_mk $ show measurable (λu:unit, a), from + measurable_inv_fun := measurable.subtype_mk $ show measurable (λu:unit, a), from measurable_const } noncomputable def set.image [measurable_space α] [measurable_space β] @@ -684,8 +684,8 @@ noncomputable def set.image [measurable_space α] [measurable_space β] { to_equiv := equiv.set.image f s hf, measurable_to_fun := begin - have : measurable (λa:s, f a) := hfm.comp (measurable_subtype_val measurable_id), - refine measurable_subtype_mk _, + have : measurable (λa:s, f a) := hfm.comp (measurable.subtype_val measurable_id), + refine measurable.subtype_mk _, convert this, ext ⟨a, h⟩, refl end, @@ -698,7 +698,7 @@ noncomputable def set.image [measurable_space α] [measurable_space β] λa ha h, (classical.some_spec h).2, rw show {x:f '' s | ((equiv.set.image f s hf).inv_fun x).val ∈ u} = subtype.val ⁻¹' (f '' u), by ext ⟨b, a, hbs, rfl⟩; simp [equiv.set.image, equiv.set.image_of_inj_on, hf, this _ hbs], - exact (measurable_subtype_val measurable_id) (f '' u) (hfi u hu) + exact (measurable.subtype_val measurable_id) (f '' u) (hfi u hu) end } noncomputable def set.range [measurable_space α] [measurable_space β] @@ -724,7 +724,7 @@ def set.range_inl [measurable_space α] [measurable_space β] : rintros ⟨ab, a, rfl⟩, simp [set.range_inl._match_1] end, - measurable_inv_fun := measurable_subtype_mk measurable_inl } + measurable_inv_fun := measurable.subtype_mk measurable_inl } def set.range_inr [measurable_space α] [measurable_space β] : measurable_equiv (range sum.inr : set (α ⊕ β)) β := @@ -741,7 +741,7 @@ def set.range_inr [measurable_space α] [measurable_space β] : rintros ⟨ab, b, rfl⟩, simp [set.range_inr._match_1] end, - measurable_inv_fun := measurable_subtype_mk measurable_inr } + measurable_inv_fun := measurable.subtype_mk measurable_inr } def sum_prod_distrib (α β γ) [measurable_space α] [measurable_space β] [measurable_space γ] : measurable_equiv ((α ⊕ β) × γ) ((α × γ) ⊕ (β × γ)) := @@ -770,11 +770,11 @@ def sum_prod_distrib (α β γ) [measurable_space α] [measurable_space β] [mea measurable_inv_fun := begin refine measurable_sum _ _, - { convert measurable_prod_mk - (measurable_inl.comp (measurable_fst measurable_id)) (measurable_snd measurable_id), + { convert measurable.prod_mk + (measurable_inl.comp (measurable.fst measurable_id)) (measurable.snd measurable_id), ext ⟨a, c⟩; refl }, - { convert measurable_prod_mk - (measurable_inr.comp (measurable_fst measurable_id)) (measurable_snd measurable_id), + { convert measurable.prod_mk + (measurable_inr.comp (measurable.fst measurable_id)) (measurable.snd measurable_id), ext ⟨b, c⟩; refl } end } diff --git a/src/measure_theory/simple_func_dense.lean b/src/measure_theory/simple_func_dense.lean index 252ecdda84d68..ccf57c5012773 100644 --- a/src/measure_theory/simple_func_dense.lean +++ b/src/measure_theory/simple_func_dense.lean @@ -243,8 +243,8 @@ let G : ℕ → α → ennreal := λn x, nndist (F n x) (f x) in let g : α → ennreal := λx, nnnorm (f x) + nnnorm (f x) + nnnorm (f x) in have hF_meas : ∀ n, measurable (G n) := λ n, measurable.comp measurable_coe $ measurable_nndist (F n).measurable hfm, -have hg_meas : measurable g := measurable.comp measurable_coe $ measurable_add - (measurable_add (measurable_nnnorm hfm) (measurable_nnnorm hfm)) (measurable_nnnorm hfm), +have hg_meas : measurable g := measurable.comp measurable_coe $ measurable.add + (measurable.add (measurable_nnnorm hfm) (measurable_nnnorm hfm)) (measurable_nnnorm hfm), have h_bound : ∀ n, ∀ₘ x, G n x ≤ g x := λ n, all_ae_of_all $ λ x, coe_le_coe.2 $ calc nndist (F n x) (f x) ≤ nndist (F n x) 0 + nndist 0 (f x) : nndist_triangle _ _ _ @@ -254,7 +254,7 @@ have h_finite : lintegral g < ⊤ := calc (∫⁻ x, nnnorm (f x) + nnnorm (f x) + nnnorm (f x)) = (∫⁻ x, nnnorm (f x)) + (∫⁻ x, nnnorm (f x)) + (∫⁻ x, nnnorm (f x)) : - by rw [lintegral_add, lintegral_add]; simp only [measurable_coe_nnnorm hfm, measurable_add] + by rw [lintegral_add, lintegral_add]; simp only [measurable_coe_nnnorm hfm, measurable.add] ... < ⊤ : by { simp only [and_self, add_lt_top], exact hfi}, have h_lim : ∀ₘ x, tendsto (λ n, G n x) at_top (𝓝 0) := all_ae_of_all $ λ x, begin