From f3b0295a1c7cbf7ac182e1bcb07e92cdb92101e3 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Sun, 7 Feb 2021 21:13:03 +0000 Subject: [PATCH] =?UTF-8?q?chore(measure=5Ftheory):=20use=20`=E2=88=9E`=20?= =?UTF-8?q?notation=20for=20`(=E2=8A=A4=20:=20=E2=84=9D=E2=89=A50=E2=88=9E?= =?UTF-8?q?)`=20(#6080)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/measure_theory/bochner_integration.lean | 26 +++---- src/measure_theory/borel_space.lean | 18 ++--- src/measure_theory/content.lean | 6 +- src/measure_theory/decomposition.lean | 10 +-- src/measure_theory/haar_measure.lean | 8 +- src/measure_theory/integration.lean | 70 ++++++++--------- src/measure_theory/l1_space.lean | 50 ++++++------ src/measure_theory/lp_space.lean | 80 ++++++++++---------- src/measure_theory/measure_space.lean | 84 ++++++++++----------- src/measure_theory/outer_measure.lean | 10 +-- src/measure_theory/prod.lean | 8 +- src/measure_theory/prod_group.lean | 2 +- src/measure_theory/set_integral.lean | 18 ++--- src/measure_theory/simple_func_dense.lean | 4 +- 14 files changed, 197 insertions(+), 197 deletions(-) diff --git a/src/measure_theory/bochner_integration.lean b/src/measure_theory/bochner_integration.lean index efaba24ee2750..9aca36028cb19 100644 --- a/src/measure_theory/bochner_integration.lean +++ b/src/measure_theory/bochner_integration.lean @@ -191,9 +191,9 @@ variables {μ : measure α} finite volume support. -/ lemma integrable_iff_fin_meas_supp {f : α →ₛ E} {μ : measure α} : integrable f μ ↔ f.fin_meas_supp μ := -calc integrable f μ ↔ ∫⁻ x, f.map (coe ∘ nnnorm : E → ℝ≥0∞) x ∂μ < ⊤ : +calc integrable f μ ↔ ∫⁻ x, f.map (coe ∘ nnnorm : E → ℝ≥0∞) x ∂μ < ∞ : and_iff_right f.ae_measurable -... ↔ (f.map (coe ∘ nnnorm : E → ℝ≥0∞)).lintegral μ < ⊤ : by rw lintegral_eq_lintegral +... ↔ (f.map (coe ∘ nnnorm : E → ℝ≥0∞)).lintegral μ < ∞ : by rw lintegral_eq_lintegral ... ↔ (f.map (coe ∘ nnnorm : E → ℝ≥0∞)).fin_meas_supp μ : iff.symm $ fin_meas_supp.iff_lintegral_lt_top $ eventually_of_forall $ λ x, coe_lt_top ... ↔ _ : fin_meas_supp.map_iff $ λ b, coe_eq_zero.trans nnnorm_eq_zero @@ -256,7 +256,7 @@ end `α →ₛ ℝ≥0∞`. But since `ℝ≥0∞` is not a `normed_space`, we need some form of coercion. See `integral_eq_lintegral` for a simpler version. -/ lemma integral_eq_lintegral' {f : α →ₛ E} {g : E → ℝ≥0∞} (hf : integrable f μ) (hg0 : g 0 = 0) - (hgt : ∀b, g b < ⊤): + (hgt : ∀b, g b < ∞): (f.map (ennreal.to_real ∘ g)).integral μ = ennreal.to_real (∫⁻ a, g (f a) ∂μ) := begin have hf' : f.fin_meas_supp μ := integrable_iff_fin_meas_supp.1 hf, @@ -630,7 +630,7 @@ begin 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 _ _ @@ -1255,7 +1255,7 @@ begin rw [← lt_top_iff_ne_top], convert hfi.has_finite_integral, ext1 x, rw [real.nnnorm_coe_eq_self] end -lemma integral_to_real {f : α → ℝ≥0∞} (hfm : ae_measurable f μ) (hf : ∀ᵐ x ∂μ, f x < ⊤) : +lemma integral_to_real {f : α → ℝ≥0∞} (hfm : ae_measurable f μ) (hf : ∀ᵐ x ∂μ, f x < ∞) : ∫ a, (f a).to_real ∂μ = (∫⁻ a, f a ∂μ).to_real := begin rw [integral_eq_lintegral_of_nonneg_ae _ hfm.to_real], @@ -1378,7 +1378,7 @@ end @[simp] lemma integral_const (c : E) : ∫ x : α, c ∂μ = (μ univ).to_real • c := begin - by_cases hμ : μ univ < ⊤, + by_cases hμ : μ univ < ∞, { haveI : finite_measure μ := ⟨hμ⟩, calc ∫ x : α, c ∂μ = (simple_func.const α c).integral μ : ((simple_func.const α c).integral_eq_integral (integrable_const _)).symm @@ -1449,7 +1449,7 @@ end norm_le_zero_iff.1 $ le_trans (norm_integral_le_lintegral_norm f) $ by simp private lemma integral_smul_measure_aux {f : α → E} {c : ℝ≥0∞} - (h0 : 0 < c) (hc : c < ⊤) (fmeas : measurable f) (hfi : integrable f μ) : + (h0 : 0 < c) (hc : c < ∞) (fmeas : measurable f) (hfi : integrable f μ) : ∫ x, f x ∂(c • μ) = c.to_real • ∫ x, f x ∂μ := begin refine tendsto_nhds_unique _ @@ -1469,26 +1469,26 @@ begin by_cases hfm : ae_measurable f μ, swap, { have : ¬ (ae_measurable f (c • μ)), by simpa [ne_of_gt h0] using hfm, simp [integral_non_ae_measurable, hfm, this] }, - -- `c = ⊤` - rcases (le_top : c ≤ ⊤).eq_or_lt with rfl|hc, + -- `c = ∞` + rcases (le_top : c ≤ ∞).eq_or_lt with rfl|hc, { rw [ennreal.top_to_real, zero_smul], by_cases hf : f =ᵐ[μ] 0, - { have : f =ᵐ[⊤ • μ] 0 := ae_smul_measure hf ⊤, + { have : f =ᵐ[∞ • μ] 0 := ae_smul_measure hf ∞, exact integral_eq_zero_of_ae this }, { apply integral_undef, - rw [integrable, has_finite_integral, iff_true_intro (hfm.smul_measure ⊤), true_and, + rw [integrable, has_finite_integral, iff_true_intro (hfm.smul_measure ∞), true_and, lintegral_smul_measure, top_mul, if_neg], { apply lt_irrefl }, { rw [lintegral_eq_zero_iff' hfm.ennnorm], refine λ h, hf (h.mono $ λ x, _), simp } } }, - -- `f` is not integrable and `0 < c < ⊤` + -- `f` is not integrable and `0 < c < ∞` by_cases hfi : integrable f μ, swap, { rw [integral_undef hfi, smul_zero], refine integral_undef (mt (λ h, _) hfi), convert h.smul_measure (ennreal.inv_lt_top.2 h0), rw [smul_smul, ennreal.inv_mul_cancel (ne_of_gt h0) (ne_of_lt hc), one_smul] }, - -- Main case: `0 < c < ⊤`, `f` is almost everywhere measurable and integrable + -- Main case: `0 < c < ∞`, `f` is almost everywhere measurable and integrable let g := hfm.mk f, calc ∫ x, f x ∂(c • μ) = ∫ x, g x ∂(c • μ) : integral_congr_ae $ ae_smul_measure hfm.ae_eq_mk c ... = c.to_real • ∫ x, g x ∂μ : diff --git a/src/measure_theory/borel_space.lean b/src/measure_theory/borel_space.lean index 4c48d07d31441..30d82fcd1998b 100644 --- a/src/measure_theory/borel_space.lean +++ b/src/measure_theory/borel_space.lean @@ -1089,7 +1089,7 @@ lemma measurable.ennreal_of_real {f : α → ℝ} (hf : measurable f) : ennreal.continuous_of_real.measurable.comp hf /-- The set of finite `ℝ≥0∞` numbers is `measurable_equiv` to `ℝ≥0`. -/ -def measurable_equiv.ennreal_equiv_nnreal : {r : ℝ≥0∞ | r ≠ ⊤} ≃ᵐ ℝ≥0 := +def measurable_equiv.ennreal_equiv_nnreal : {r : ℝ≥0∞ | r ≠ ∞} ≃ᵐ ℝ≥0 := ennreal.ne_top_homeomorph_nnreal.to_measurable_equiv namespace ennreal @@ -1099,20 +1099,20 @@ measurable_id.ennreal_coe lemma measurable_of_measurable_nnreal {f : ℝ≥0∞ → α} (h : measurable (λ p : ℝ≥0, f p)) : measurable f := -measurable_of_measurable_on_compl_singleton ⊤ +measurable_of_measurable_on_compl_singleton ∞ (measurable_equiv.ennreal_equiv_nnreal.symm.measurable_coe_iff.1 h) /-- `ℝ≥0∞` is `measurable_equiv` to `ℝ≥0 ⊕ unit`. -/ def ennreal_equiv_sum : ℝ≥0∞ ≃ᵐ ℝ≥0 ⊕ unit := { measurable_to_fun := measurable_of_measurable_nnreal measurable_inl, - measurable_inv_fun := measurable_sum measurable_coe (@measurable_const ℝ≥0∞ unit _ _ ⊤), + measurable_inv_fun := measurable_sum measurable_coe (@measurable_const ℝ≥0∞ unit _ _ ∞), .. equiv.option_equiv_sum_punit ℝ≥0 } open function (uncurry) lemma measurable_of_measurable_nnreal_prod [measurable_space β] [measurable_space γ] {f : ℝ≥0∞ × β → γ} (H₁ : measurable (λ p : ℝ≥0 × β, f (p.1, p.2))) - (H₂ : measurable (λ x, f (⊤, x))) : + (H₂ : measurable (λ x, f (∞, x))) : measurable f := let e : ℝ≥0∞ × β ≃ᵐ ℝ≥0 × β ⊕ unit × β := (ennreal_equiv_sum.prod_congr (measurable_equiv.refl β)).trans @@ -1121,7 +1121,7 @@ e.symm.measurable_coe_iff.1 $ measurable_sum H₁ (H₂.comp measurable_id.snd) lemma measurable_of_measurable_nnreal_nnreal [measurable_space β] {f : ℝ≥0∞ × ℝ≥0∞ → β} (h₁ : measurable (λ p : ℝ≥0 × ℝ≥0, f (p.1, p.2))) - (h₂ : measurable (λ r : ℝ≥0, f (⊤, r))) (h₃ : measurable (λ r : ℝ≥0, f (r, ⊤))) : + (h₂ : measurable (λ r : ℝ≥0, f (∞, r))) (h₃ : measurable (λ r : ℝ≥0, f (r, ∞))) : measurable f := measurable_of_measurable_nnreal_prod (measurable_swap_iff.1 $ measurable_of_measurable_nnreal_prod (h₁.comp measurable_swap) h₃) @@ -1386,7 +1386,7 @@ variables [topological_space α] {μ : measure α} - it is outer regular: `μ(A) = inf { μ(U) | A ⊆ U open }` for `A` measurable; - it is inner regular: `μ(U) = sup { μ(K) | K ⊆ U compact }` for `U` open. -/ structure regular (μ : measure α) : Prop := -(lt_top_of_is_compact : ∀ {{K : set α}}, is_compact K → μ K < ⊤) +(lt_top_of_is_compact : ∀ {{K : set α}}, is_compact K → μ K < ∞) (outer_regular : ∀ {{A : set α}}, measurable_set A → (⨅ (U : set α) (h : is_open U) (h2 : A ⊆ U), μ U) ≤ μ A) (inner_regular : ∀ {{U : set α}}, is_open U → @@ -1429,7 +1429,7 @@ begin rw [map_apply hf hK.measurable_set] } end -protected lemma smul (hμ : μ.regular) {x : ℝ≥0∞} (hx : x < ⊤) : +protected lemma smul (hμ : μ.regular) {x : ℝ≥0∞} (hx : x < ∞) : (x • μ).regular := begin split, @@ -1460,11 +1460,11 @@ end measure_theory lemma is_compact.measure_lt_top_of_nhds_within [topological_space α] {s : set α} {μ : measure α} (h : is_compact s) (hμ : ∀ x ∈ s, μ.finite_at_filter (𝓝[s] x)) : - μ s < ⊤ := + μ s < ∞ := is_compact.induction_on h (by simp) (λ s t hst ht, (measure_mono hst).trans_lt ht) (λ s t hs ht, (measure_union_le s t).trans_lt (ennreal.add_lt_top.2 ⟨hs, ht⟩)) hμ lemma is_compact.measure_lt_top [topological_space α] {s : set α} {μ : measure α} [locally_finite_measure μ] (h : is_compact s) : - μ s < ⊤ := + μ s < ∞ := h.measure_lt_top_of_nhds_within $ λ x hx, μ.finite_at_nhds_within _ _ diff --git a/src/measure_theory/content.lean b/src/measure_theory/content.lean index d4e9a25c2f862..c8b10ba736532 100644 --- a/src/measure_theory/content.lean +++ b/src/measure_theory/content.lean @@ -84,7 +84,7 @@ lemma inner_content_mono {μ : compacts G → ℝ≥0∞} ⦃U V : set G⦄ (hU supr_le_supr $ λ K, supr_le_supr_const $ λ hK, subset.trans hK h2 lemma inner_content_exists_compact {μ : compacts G → ℝ≥0∞} {U : opens G} - (hU : inner_content μ U < ⊤) {ε : ℝ≥0} (hε : 0 < ε) : + (hU : inner_content μ U < ∞) {ε : ℝ≥0} (hε : 0 < ε) : ∃ K : compacts G, K.1 ⊆ U ∧ inner_content μ U ≤ μ K + ε := begin have h'ε := ennreal.zero_lt_coe_iff.2 hε, @@ -208,7 +208,7 @@ lemma of_content_interior_compacts (h3 : ∀ (K₁ K₂ : compacts G), K₁.1 le_trans (le_of_eq $ of_content_opens h2 (opens.interior K.1)) (inner_content_le h3 _ _ interior_subset) -lemma of_content_exists_compact {U : opens G} (hU : of_content μ h1 U < ⊤) {ε : ℝ≥0} +lemma of_content_exists_compact {U : opens G} (hU : of_content μ h1 U < ∞) {ε : ℝ≥0} (hε : 0 < ε) : ∃ K : compacts G, K.1 ⊆ U ∧ of_content μ h1 U ≤ of_content μ h1 K.1 + ε := begin rw [of_content_opens h2] at hU ⊢, @@ -216,7 +216,7 @@ begin exact ⟨K, h1K, le_trans h2K $ add_le_add_right (le_of_content_compacts h2 K) _⟩, end -lemma of_content_exists_open {A : set G} (hA : of_content μ h1 A < ⊤) {ε : ℝ≥0} (hε : 0 < ε) : +lemma of_content_exists_open {A : set G} (hA : of_content μ h1 A < ∞) {ε : ℝ≥0} (hε : 0 < ε) : ∃ U : opens G, A ⊆ U ∧ of_content μ h1 U ≤ of_content μ h1 A + ε := begin rcases induced_outer_measure_exists_set _ _ inner_content_mono hA hε with ⟨U, hU, h2U, h3U⟩, diff --git a/src/measure_theory/decomposition.lean b/src/measure_theory/decomposition.lean index 8e15c7eb3e4c2..1a3078fc64cd2 100644 --- a/src/measure_theory/decomposition.lean +++ b/src/measure_theory/decomposition.lean @@ -23,7 +23,7 @@ private lemma aux {m : ℕ} {γ d : ℝ} (h : γ - (1 / 2) ^ m < d) : γ - 2 * (1 / 2) ^ m + (1 / 2) ^ m ≤ d := by linarith -lemma hahn_decomposition (hμ : μ univ < ⊤) (hν : ν univ < ⊤) : +lemma hahn_decomposition (hμ : μ univ < ∞) (hν : ν univ < ∞) : ∃s, measurable_set s ∧ (∀t, measurable_set t → t ⊆ s → ν t ≤ μ t) ∧ (∀t, measurable_set t → t ⊆ sᶜ → μ t ≤ ν t) := @@ -32,8 +32,8 @@ begin let c : set ℝ := d '' {s | measurable_set s }, let γ : ℝ := Sup c, - have hμ : ∀s, μ s < ⊤ := assume s, lt_of_le_of_lt (measure_mono $ subset_univ _) hμ, - have hν : ∀s, ν s < ⊤ := assume s, lt_of_le_of_lt (measure_mono $ subset_univ _) hν, + have hμ : ∀s, μ s < ∞ := assume s, lt_of_le_of_lt (measure_mono $ subset_univ _) hμ, + have hν : ∀s, ν s < ∞ := assume s, lt_of_le_of_lt (measure_mono $ subset_univ _) hν, have to_nnreal_μ : ∀s, ((μ s).to_nnreal : ℝ≥0∞) = μ s := (assume s, ennreal.coe_to_nnreal $ ne_top_of_lt $ hμ _), have to_nnreal_ν : ∀s, ((ν s).to_nnreal : ℝ≥0∞) = ν s := @@ -56,7 +56,7 @@ begin { assume s hs hm, refine tendsto.sub _ _; refine (nnreal.tendsto_coe.2 $ - (ennreal.tendsto_to_nnreal $ @ne_top_of_lt _ _ _ ⊤ _).comp $ tendsto_measure_Union hs hm), + (ennreal.tendsto_to_nnreal $ @ne_top_of_lt _ _ _ ∞ _).comp $ tendsto_measure_Union hs hm), exact hμ _, exact hν _ }, @@ -65,7 +65,7 @@ begin { assume s hs hm, refine tendsto.sub _ _; refine (nnreal.tendsto_coe.2 $ - (ennreal.tendsto_to_nnreal $ @ne_top_of_lt _ _ _ ⊤ _).comp $ tendsto_measure_Inter hs hm _), + (ennreal.tendsto_to_nnreal $ @ne_top_of_lt _ _ _ ∞ _).comp $ tendsto_measure_Inter hs hm _), exact hμ _, exact ⟨0, hμ _⟩, exact hν _, diff --git a/src/measure_theory/haar_measure.lean b/src/measure_theory/haar_measure.lean index 7170642554d93..bd7f3b69d77ad 100644 --- a/src/measure_theory/haar_measure.lean +++ b/src/measure_theory/haar_measure.lean @@ -470,12 +470,12 @@ lemma haar_outer_measure_le_echaar {K₀ : positive_compacts G} {U : set G} (hU (outer_measure.of_content_le echaar_sup_le echaar_mono ⟨U, hU⟩ K h : _) lemma haar_outer_measure_exists_open {K₀ : positive_compacts G} {A : set G} - (hA : haar_outer_measure K₀ A < ⊤) {ε : ℝ≥0} (hε : 0 < ε) : + (hA : haar_outer_measure K₀ A < ∞) {ε : ℝ≥0} (hε : 0 < ε) : ∃ U : opens G, A ⊆ U ∧ haar_outer_measure K₀ U ≤ haar_outer_measure K₀ A + ε := outer_measure.of_content_exists_open echaar_sup_le hA hε lemma haar_outer_measure_exists_compact {K₀ : positive_compacts G} {U : opens G} - (hU : haar_outer_measure K₀ U < ⊤) {ε : ℝ≥0} (hε : 0 < ε) : + (hU : haar_outer_measure K₀ U < ∞) {ε : ℝ≥0} (hε : 0 < ε) : ∃ K : compacts G, K.1 ⊆ U ∧ haar_outer_measure K₀ U ≤ haar_outer_measure K₀ K.1 + ε := outer_measure.of_content_exists_compact echaar_sup_le hU hε @@ -502,7 +502,7 @@ lemma haar_outer_measure_self_pos {K₀ : positive_compacts G} : ((haar_outer_measure K₀).mono interior_subset) lemma haar_outer_measure_lt_top_of_is_compact [locally_compact_space G] {K₀ : positive_compacts G} - {K : set G} (hK : is_compact K) : haar_outer_measure K₀ K < ⊤ := + {K : set G} (hK : is_compact K) : haar_outer_measure K₀ K < ∞ := begin rcases exists_compact_superset hK with ⟨F, h1F, h2F⟩, refine ((haar_outer_measure K₀).mono h2F).trans_lt _, @@ -612,7 +612,7 @@ begin end theorem regular_of_left_invariant (hμ : is_mul_left_invariant μ) {K} (hK : is_compact K) - (h2K : (interior K).nonempty) (hμK : μ K < ⊤) : regular μ := + (h2K : (interior K).nonempty) (hμK : μ K < ∞) : regular μ := begin rw [haar_measure_unique hμ ⟨K, hK, h2K⟩], exact regular.smul regular_haar_measure hμK diff --git a/src/measure_theory/integration.lean b/src/measure_theory/integration.lean index f545d35236412..e00a120f39def 100644 --- a/src/measure_theory/integration.lean +++ b/src/measure_theory/integration.lean @@ -717,11 +717,11 @@ protected def fin_meas_supp (f : α →ₛ β) (μ : measure α) : Prop := f =ᶠ[μ.cofinite] 0 lemma fin_meas_supp_iff_support {f : α →ₛ β} {μ : measure α} : - f.fin_meas_supp μ ↔ μ (support f) < ⊤ := + f.fin_meas_supp μ ↔ μ (support f) < ∞ := iff.rfl lemma fin_meas_supp_iff {f : α →ₛ β} {μ : measure α} : - f.fin_meas_supp μ ↔ ∀ y ≠ 0, μ (f ⁻¹' {y}) < ⊤ := + f.fin_meas_supp μ ↔ ∀ y ≠ 0, μ (f ⁻¹' {y}) < ∞ := begin split, { refine λ h y hy, lt_of_le_of_lt (measure_mono _) h, @@ -735,7 +735,7 @@ end namespace fin_meas_supp lemma meas_preimage_singleton_ne_zero {f : α →ₛ β} (h : f.fin_meas_supp μ) {y : β} (hy : y ≠ 0) : - μ (f ⁻¹' {y}) < ⊤ := + μ (f ⁻¹' {y}) < ∞ := fin_meas_supp_iff.1 h y hy protected lemma map {f : α →ₛ β} {g : β → γ} (hf : f.fin_meas_supp μ) (hg : g 0 = 0) : @@ -771,11 +771,11 @@ protected lemma mul {β} [monoid_with_zero β] {f g : α →ₛ β} (hf : f.fin_ (f * g).fin_meas_supp μ := by { rw [mul_eq_map₂], exact hf.map₂ hg (zero_mul 0) } -lemma lintegral_lt_top {f : α →ₛ ℝ≥0∞} (hm : f.fin_meas_supp μ) (hf : ∀ᵐ a ∂μ, f a < ⊤) : - f.lintegral μ < ⊤ := +lemma lintegral_lt_top {f : α →ₛ ℝ≥0∞} (hm : f.fin_meas_supp μ) (hf : ∀ᵐ a ∂μ, f a < ∞) : + f.lintegral μ < ∞ := begin refine sum_lt_top (λ a ha, _), - rcases eq_or_lt_of_le (le_top : a ≤ ⊤) with rfl|ha, + rcases eq_or_lt_of_le (le_top : a ≤ ∞) with rfl|ha, { simp only [ae_iff, lt_top_iff_ne_top, ne.def, not_not] at hf, simp [set.preimage, hf] }, { by_cases ha0 : a = 0, @@ -783,13 +783,13 @@ begin { exact mul_lt_top ha (fin_meas_supp_iff.1 hm _ ha0) } } end -lemma of_lintegral_lt_top {f : α →ₛ ℝ≥0∞} (h : f.lintegral μ < ⊤) : f.fin_meas_supp μ := +lemma of_lintegral_lt_top {f : α →ₛ ℝ≥0∞} (h : f.lintegral μ < ∞) : f.fin_meas_supp μ := begin refine fin_meas_supp_iff.2 (λ b hb, _), rw [lintegral, sum_lt_top_iff] at h, by_cases b_mem : b ∈ f.range, { rw ennreal.lt_top_iff_ne_top, - have h : ¬ _ = ⊤ := ennreal.lt_top_iff_ne_top.1 (h b b_mem), + have h : ¬ _ = ∞ := ennreal.lt_top_iff_ne_top.1 (h b b_mem), simp only [mul_eq_top, not_or_distrib, not_and_distrib] at h, rcases h with ⟨h, h'⟩, refine or.elim h (λh, by contradiction) (λh, h) }, @@ -798,8 +798,8 @@ begin exact with_top.zero_lt_top } end -lemma iff_lintegral_lt_top {f : α →ₛ ℝ≥0∞} (hf : ∀ᵐ a ∂μ, f a < ⊤) : - f.fin_meas_supp μ ↔ f.lintegral μ < ⊤ := +lemma iff_lintegral_lt_top {f : α →ₛ ℝ≥0∞} (hf : ∀ᵐ a ∂μ, f a < ∞) : + f.fin_meas_supp μ ↔ f.lintegral μ < ∞ := ⟨λ h, h.lintegral_lt_top hf, λ h, of_lintegral_lt_top h⟩ end fin_meas_supp @@ -907,17 +907,17 @@ begin refine le_antisymm (bsupr_le $ assume φ hφ, _) (supr_le_supr2 $ λ φ, ⟨φ.map (coe : ℝ≥0 → ℝ≥0∞), le_refl _⟩), - by_cases h : ∀ᵐ a ∂μ, φ a ≠ ⊤, + by_cases h : ∀ᵐ a ∂μ, φ a ≠ ∞, { let ψ := φ.map ennreal.to_nnreal, replace h : ψ.map (coe : ℝ≥0 → ℝ≥0∞) =ᵐ[μ] φ := h.mono (λ a, ennreal.coe_to_nnreal), have : ∀ x, ↑(ψ x) ≤ f x := λ x, le_trans ennreal.coe_to_nnreal_le_self (hφ x), exact le_supr_of_le (φ.map ennreal.to_nnreal) (le_supr_of_le this (ge_of_eq $ lintegral_congr h)) }, - { have h_meas : μ (φ ⁻¹' {⊤}) ≠ 0, from mt measure_zero_iff_ae_nmem.1 h, + { have h_meas : μ (φ ⁻¹' {∞}) ≠ 0, from mt measure_zero_iff_ae_nmem.1 h, refine le_trans le_top (ge_of_eq $ (supr_eq_top _).2 $ λ b hb, _), - obtain ⟨n, hn⟩ : ∃ n : ℕ, b < n * μ (φ ⁻¹' {⊤}), from exists_nat_mul_gt h_meas (ne_of_lt hb), - use (const α (n : ℝ≥0)).restrict (φ ⁻¹' {⊤}), + obtain ⟨n, hn⟩ : ∃ n : ℕ, b < n * μ (φ ⁻¹' {∞}), from exists_nat_mul_gt h_meas (ne_of_lt hb), + use (const α (n : ℝ≥0)).restrict (φ ⁻¹' {∞}), simp only [lt_supr_iff, exists_prop, coe_restrict, φ.measurable_set_preimage, coe_const, ennreal.coe_indicator, map_coe_ennreal_restrict, map_const, ennreal.coe_nat, restrict_const_lintegral], @@ -926,7 +926,7 @@ begin simp only [hx, le_top] } end -lemma exists_simple_func_forall_lintegral_sub_lt_of_pos {f : α → ℝ≥0∞} (h : ∫⁻ x, f x ∂μ < ⊤) +lemma exists_simple_func_forall_lintegral_sub_lt_of_pos {f : α → ℝ≥0∞} (h : ∫⁻ x, f x ∂μ < ∞) {ε : ℝ≥0∞} (hε : 0 < ε) : ∃ φ : α →ₛ ℝ≥0, (∀ x, ↑(φ x) ≤ f x) ∧ ∀ ψ : α →ₛ ℝ≥0, (∀ x, ↑(ψ x) ≤ f x) → (map coe (ψ - φ)).lintegral μ < ε := @@ -937,7 +937,7 @@ begin simp_rw [lt_supr_iff, supr_lt_iff, supr_le_iff] at this, rcases this with ⟨φ, hle : ∀ x, ↑(φ x) ≤ f x, b, hbφ, hb⟩, refine ⟨φ, hle, λ ψ hψ, _⟩, - have : (map coe φ).lintegral μ < ⊤, from (le_bsupr φ hle).trans_lt h, + have : (map coe φ).lintegral μ < ∞, from (le_bsupr φ hle).trans_lt h, rw [← add_lt_add_iff_left this, ← add_lintegral, ← map_add @ennreal.coe_add], refine (hb _ (λ x, le_trans _ (max_le (hle x) (hψ x)))).trans_lt hbφ, norm_cast, @@ -1106,7 +1106,7 @@ end /-- If `f` has finite integral, then `∫⁻ x in s, f x ∂μ` is absolutely continuous in `s`: it tends to zero as `μ s` tends to zero. This lemma states states this fact in terms of `ε` and `δ`. -/ -lemma exists_pos_set_lintegral_lt_of_measure_lt {f : α → ℝ≥0∞} (h : ∫⁻ x, f x ∂μ < ⊤) +lemma exists_pos_set_lintegral_lt_of_measure_lt {f : α → ℝ≥0∞} (h : ∫⁻ x, f x ∂μ < ∞) {ε : ℝ≥0∞} (hε : 0 < ε) : ∃ δ > 0, ∀ s, μ s < δ → ∫⁻ x in s, f x ∂μ < ε := begin @@ -1139,7 +1139,7 @@ end /-- If `f` has finite integral, then `∫⁻ x in s, f x ∂μ` is absolutely continuous in `s`: it tends to zero as `μ s` tends to zero. -/ -lemma tendsto_set_lintegral_zero {ι} {f : α → ℝ≥0∞} (h : ∫⁻ x, f x ∂μ < ⊤) +lemma tendsto_set_lintegral_zero {ι} {f : α → ℝ≥0∞} (h : ∫⁻ x, f x ∂μ < ∞) {l : filter ι} {s : ι → set α} (hl : tendsto (μ ∘ s) l (𝓝 0)) : tendsto (λ i, ∫⁻ x in s i, f x ∂μ) l (𝓝 0) := begin @@ -1265,7 +1265,7 @@ begin exact canonically_ordered_semiring.mul_le_mul (le_refl _) (hs x) end -lemma lintegral_const_mul' (r : ℝ≥0∞) (f : α → ℝ≥0∞) (hr : r ≠ ⊤) : +lemma lintegral_const_mul' (r : ℝ≥0∞) (f : α → ℝ≥0∞) (hr : r ≠ ∞) : (∫⁻ a, r * f a ∂μ) = r * (∫⁻ a, f a ∂μ) := begin by_cases h : r = 0, @@ -1291,7 +1291,7 @@ lemma lintegral_mul_const_le (r : ℝ≥0∞) (f : α → ℝ≥0∞) : ∫⁻ a, f a ∂μ * r ≤ ∫⁻ a, f a * r ∂μ := by simp_rw [mul_comm, lintegral_const_mul_le r f] -lemma lintegral_mul_const' (r : ℝ≥0∞) (f : α → ℝ≥0∞) (hr : r ≠ ⊤): +lemma lintegral_mul_const' (r : ℝ≥0∞) (f : α → ℝ≥0∞) (hr : r ≠ ∞): ∫⁻ a, f a * r ∂μ = ∫⁻ a, f a ∂μ * r := by simp_rw [mul_comm, lintegral_const_mul' r f hr] @@ -1340,7 +1340,7 @@ begin end lemma meas_ge_le_lintegral_div {f : α → ℝ≥0∞} (hf : measurable f) {ε : ℝ≥0∞} - (hε : ε ≠ 0) (hε' : ε ≠ ⊤) : + (hε : ε ≠ 0) (hε' : ε ≠ ∞) : μ {x | ε ≤ f x} ≤ (∫⁻ a, f a ∂μ) / ε := (ennreal.le_div_iff_mul_le (or.inl hε) (or.inl hε')).2 $ by { rw [mul_comm], exact mul_meas_ge_le_lintegral hf ε } @@ -1404,7 +1404,7 @@ calc by simp only [lintegral_congr_ae (g_eq_f.mono $ λ a ha, ha _)] lemma lintegral_sub {f g : α → ℝ≥0∞} (hf : measurable f) (hg : measurable g) - (hg_fin : ∫⁻ a, g a ∂μ < ⊤) (h_le : g ≤ᵐ[μ] f) : + (hg_fin : ∫⁻ a, g a ∂μ < ∞) (h_le : g ≤ᵐ[μ] f) : ∫⁻ a, f a - g a ∂μ = ∫⁻ a, f a ∂μ - ∫⁻ a, g a ∂μ := begin rw [← ennreal.add_left_inj hg_fin, @@ -1417,7 +1417,7 @@ end /-- Monotone convergence theorem for nonincreasing sequences of functions -/ lemma lintegral_infi_ae {f : ℕ → α → ℝ≥0∞} (h_meas : ∀n, measurable (f n)) - (h_mono : ∀n:ℕ, f n.succ ≤ᵐ[μ] f n) (h_fin : ∫⁻ a, f 0 a ∂μ < ⊤) : + (h_mono : ∀n:ℕ, f n.succ ≤ᵐ[μ] f n) (h_fin : ∫⁻ a, f 0 a ∂μ < ∞) : ∫⁻ a, ⨅n, f n a ∂μ = ⨅n, ∫⁻ a, f n a ∂μ := have fn_le_f0 : ∫⁻ a, ⨅n, f n a ∂μ ≤ ∫⁻ a, f 0 a ∂μ, from lintegral_mono (assume a, infi_le_of_le 0 (le_refl _)), @@ -1429,7 +1429,7 @@ calc (lintegral_sub (h_meas 0) (measurable_infi h_meas) (calc (∫⁻ a, ⨅n, f n a ∂μ) ≤ ∫⁻ a, f 0 a ∂μ : lintegral_mono (assume a, infi_le _ _) - ... < ⊤ : h_fin ) + ... < ∞ : h_fin ) (ae_of_all _ $ assume a, infi_le _ _)).symm ... = ∫⁻ a, ⨆n, f 0 a - f n a ∂μ : congr rfl (funext (assume a, ennreal.sub_infi)) ... = ⨆n, ∫⁻ a, f 0 a - f n a ∂μ : @@ -1446,14 +1446,14 @@ calc congr rfl (funext $ assume n, lintegral_sub (h_meas _) (h_meas _) (calc ∫⁻ a, f n a ∂μ ≤ ∫⁻ a, f 0 a ∂μ : lintegral_mono_ae $ h_mono n - ... < ⊤ : h_fin) + ... < ∞ : h_fin) (h_mono n)) ... = ∫⁻ a, f 0 a ∂μ - ⨅n, ∫⁻ a, f n a ∂μ : ennreal.sub_infi.symm /-- Monotone convergence theorem for nonincreasing sequences of functions -/ lemma lintegral_infi {f : ℕ → α → ℝ≥0∞} (h_meas : ∀n, measurable (f n)) - (h_mono : ∀ ⦃m n⦄, m ≤ n → f n ≤ f m) (h_fin : ∫⁻ a, f 0 a ∂μ < ⊤) : + (h_mono : ∀ ⦃m n⦄, m ≤ n → f n ≤ f m) (h_fin : ∫⁻ a, f 0 a ∂μ < ∞) : ∫⁻ a, ⨅n, f n a ∂μ = ⨅n, ∫⁻ a, f n a ∂μ := lintegral_infi_ae h_meas (λ n, ae_of_all _ $ h_mono $ le_of_lt n.lt_succ_self) h_fin @@ -1477,7 +1477,7 @@ lemma lintegral_liminf_le {f : ℕ → α → ℝ≥0∞} (h_meas : ∀n, measur lintegral_liminf_le' (λ n, (h_meas n).ae_measurable) lemma limsup_lintegral_le {f : ℕ → α → ℝ≥0∞} {g : α → ℝ≥0∞} - (hf_meas : ∀ n, measurable (f n)) (h_bound : ∀n, f n ≤ᵐ[μ] g) (h_fin : ∫⁻ a, g a ∂μ < ⊤) : + (hf_meas : ∀ n, measurable (f n)) (h_bound : ∀n, f n ≤ᵐ[μ] g) (h_fin : ∫⁻ a, g a ∂μ < ∞) : limsup at_top (λn, ∫⁻ a, f n a ∂μ) ≤ ∫⁻ a, limsup at_top (λn, f n a) ∂μ := calc limsup at_top (λn, ∫⁻ a, f n a ∂μ) = ⨅n:ℕ, ⨆i≥n, ∫⁻ a, f i a ∂μ : @@ -1500,7 +1500,7 @@ calc lemma tendsto_lintegral_of_dominated_convergence {F : ℕ → α → ℝ≥0∞} {f : α → ℝ≥0∞} (bound : α → ℝ≥0∞) (hF_meas : ∀n, measurable (F n)) (h_bound : ∀n, F n ≤ᵐ[μ] bound) - (h_fin : ∫⁻ a, bound a ∂μ < ⊤) + (h_fin : ∫⁻ a, bound a ∂μ < ∞) (h_lim : ∀ᵐ a ∂μ, tendsto (λ n, F n a) at_top (𝓝 (f a))) : tendsto (λn, ∫⁻ a, F n a ∂μ) at_top (𝓝 (∫⁻ a, f a ∂μ)) := tendsto_of_le_liminf_of_limsup_le @@ -1516,7 +1516,7 @@ measurable. -/ lemma tendsto_lintegral_of_dominated_convergence' {F : ℕ → α → ℝ≥0∞} {f : α → ℝ≥0∞} (bound : α → ℝ≥0∞) (hF_meas : ∀n, ae_measurable (F n) μ) (h_bound : ∀n, F n ≤ᵐ[μ] bound) - (h_fin : ∫⁻ a, bound a ∂μ < ⊤) + (h_fin : ∫⁻ a, bound a ∂μ < ∞) (h_lim : ∀ᵐ a ∂μ, tendsto (λ n, F n a) at_top (𝓝 (f a))) : tendsto (λn, ∫⁻ a, F n a ∂μ) at_top (𝓝 (∫⁻ a, f a ∂μ)) := begin @@ -1543,7 +1543,7 @@ lemma tendsto_lintegral_filter_of_dominated_convergence {ι} {l : filter ι} (hl_cb : l.is_countably_generated) (hF_meas : ∀ᶠ n in l, measurable (F n)) (h_bound : ∀ᶠ n in l, ∀ᵐ a ∂μ, F n a ≤ bound a) - (h_fin : ∫⁻ a, bound a ∂μ < ⊤) + (h_fin : ∫⁻ a, bound a ∂μ < ∞) (h_lim : ∀ᵐ a ∂μ, tendsto (λ n, F n a) l (𝓝 (f a))) : tendsto (λn, ∫⁻ a, F n a ∂μ) l (𝓝 $ ∫⁻ a, f a ∂μ) := begin @@ -1675,14 +1675,14 @@ begin exact funext (λ a, lintegral_dirac a f), end -lemma ae_lt_top {f : α → ℝ≥0∞} (hf : measurable f) (h2f : ∫⁻ x, f x ∂μ < ⊤) : - ∀ᵐ x ∂μ, f x < ⊤ := +lemma ae_lt_top {f : α → ℝ≥0∞} (hf : measurable f) (h2f : ∫⁻ x, f x ∂μ < ∞) : + ∀ᵐ x ∂μ, f x < ∞ := begin simp_rw [ae_iff, ennreal.not_lt_top], by_contra h, rw [← not_le] at h2f, apply h2f, - have : (f ⁻¹' {⊤}).indicator ⊤ ≤ f, - { intro x, by_cases hx : x ∈ f ⁻¹' {⊤}; [simpa [hx], simp [hx]] }, + have : (f ⁻¹' {∞}).indicator ⊤ ≤ f, + { intro x, by_cases hx : x ∈ f ⁻¹' {∞}; [simpa [hx], simp [hx]] }, convert lintegral_mono this, - rw [lintegral_indicator _ (hf (measurable_set_singleton ⊤))], simp [ennreal.top_mul, preimage, h] + rw [lintegral_indicator _ (hf (measurable_set_singleton ∞))], simp [ennreal.top_mul, preimage, h] end /-- Given a measure `μ : measure α` and a function `f : α → ℝ≥0∞`, `μ.with_density f` is the diff --git a/src/measure_theory/l1_space.lean b/src/measure_theory/l1_space.lean index df8a2ffc0d2fb..bb0f966f2bd95 100644 --- a/src/measure_theory/l1_space.lean +++ b/src/measure_theory/l1_space.lean @@ -26,14 +26,14 @@ of being almost everywhere equal is defined as a subspace of the space `L⁰`. S ## Main definitions * Let `f : α → β` be a function, where `α` is a `measure_space` and `β` a `normed_group`. - Then `has_finite_integral f` means `(∫⁻ a, nnnorm (f a)) < ⊤`. + Then `has_finite_integral f` means `(∫⁻ a, nnnorm (f a)) < ∞`. * 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⁰`. + 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 @@ -41,7 +41,7 @@ of being almost everywhere equal is defined as a subspace of the space `L⁰`. S ## Implementation notes -Maybe `integrable f` should be mean `(∫⁻ a, edist (f a) 0) < ⊤`, so that `integrable` and +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. @@ -103,18 +103,18 @@ by simp only [pi.neg_apply, nnnorm_neg] /-- `has_finite_integral f μ` means that the integral `∫⁻ a, ∥f a∥ ∂μ` is finite. `has_finite_integral f` means `has_finite_integral f volume`. -/ def has_finite_integral (f : α → β) (μ : measure α . volume_tac) : Prop := -∫⁻ a, nnnorm (f a) ∂μ < ⊤ +∫⁻ a, nnnorm (f a) ∂μ < ∞ lemma has_finite_integral_iff_norm (f : α → β) : - has_finite_integral f μ ↔ ∫⁻ a, (ennreal.of_real ∥f a∥) ∂μ < ⊤ := + has_finite_integral f μ ↔ ∫⁻ a, (ennreal.of_real ∥f a∥) ∂μ < ∞ := by simp only [has_finite_integral, of_real_norm_eq_coe_nnnorm] lemma has_finite_integral_iff_edist (f : α → β) : - has_finite_integral f μ ↔ ∫⁻ a, edist (f a) 0 ∂μ < ⊤ := + has_finite_integral f μ ↔ ∫⁻ a, edist (f a) 0 ∂μ < ∞ := by simp only [has_finite_integral_iff_norm, edist_dist, dist_zero_right] lemma has_finite_integral_iff_of_real {f : α → ℝ} (h : 0 ≤ᵐ[μ] f) : - has_finite_integral f μ ↔ ∫⁻ a, ennreal.of_real (f a) ∂μ < ⊤ := + has_finite_integral f μ ↔ ∫⁻ a, ennreal.of_real (f a) ∂μ < ∞ := have lintegral_eq : ∫⁻ a, (ennreal.of_real ∥f a∥) ∂μ = ∫⁻ a, ennreal.of_real (f a) ∂μ := begin refine lintegral_congr_ae (h.mono $ λ a h, _), @@ -128,7 +128,7 @@ begin simp only [has_finite_integral_iff_norm] at *, calc ∫⁻ a, (ennreal.of_real ∥f a∥) ∂μ ≤ ∫⁻ (a : α), (ennreal.of_real ∥g a∥) ∂μ : lintegral_mono_ae (h.mono $ assume a h, of_real_le_of_real h) - ... < ⊤ : hg + ... < ∞ : hg end lemma has_finite_integral.mono' {f : α → β} {g : α → ℝ} (hg : has_finite_integral g μ) @@ -153,7 +153,7 @@ lemma has_finite_integral_congr {f g : α → β} (h : f =ᵐ[μ] g) : has_finite_integral_congr' $ h.fun_comp norm lemma has_finite_integral_const_iff {c : β} : - has_finite_integral (λ x : α, c) μ ↔ c = 0 ∨ μ univ < ⊤ := + has_finite_integral (λ x : α, c) μ ↔ c = 0 ∨ μ univ < ∞ := begin simp only [has_finite_integral, lintegral_const], by_cases hc : c = 0, @@ -196,7 +196,7 @@ h.mono_measure $ measure.le_add_left $ le_refl _ ⟨λ h, ⟨h.left_of_add_measure, h.right_of_add_measure⟩, λ h, h.1.add_measure h.2⟩ lemma has_finite_integral.smul_measure {f : α → β} (h : has_finite_integral f μ) {c : ℝ≥0∞} - (hc : c < ⊤) : has_finite_integral f (c • μ) := + (hc : c < ∞) : has_finite_integral f (c • μ) := begin simp only [has_finite_integral, lintegral_smul_measure] at *, exact mul_lt_top hc h @@ -258,12 +258,12 @@ lemma has_finite_integral_of_dominated_convergence {F : ℕ → α → β} {f : (h_lim : ∀ᵐ a ∂μ, tendsto (λ n, F n a) at_top (𝓝 (f a))) : has_finite_integral f μ := /- `∥F n a∥ ≤ bound a` and `∥F n a∥ --> ∥f a∥` implies `∥f a∥ ≤ bound a`, - and so `∫ ∥f∥ ≤ ∫ bound < ⊤` since `bound` is has_finite_integral -/ + and so `∫ ∥f∥ ≤ ∫ bound < ∞` since `bound` is has_finite_integral -/ begin rw has_finite_integral_iff_norm, calc ∫⁻ a, (ennreal.of_real ∥f a∥) ∂μ ≤ ∫⁻ a, ennreal.of_real (bound a) ∂μ : lintegral_mono_ae $ all_ae_of_real_f_le_bound h_bound h_lim - ... < ⊤ : + ... < ∞ : begin rw ← has_finite_integral_iff_of_real, { exact bound_has_finite_integral }, @@ -317,7 +317,7 @@ begin { rw has_finite_integral_iff_of_real at bound_has_finite_integral, { calc ∫⁻ a, b a ∂μ = 2 * ∫⁻ a, ennreal.of_real (bound a) ∂μ : by { rw lintegral_const_mul', exact coe_ne_top } - ... < ⊤ : mul_lt_top (coe_lt_top) bound_has_finite_integral }, + ... < ∞ : mul_lt_top (coe_lt_top) bound_has_finite_integral }, filter_upwards [h_bound 0] λ a h, le_trans (norm_nonneg _) h }, -- Show `∥f a - F n a∥ --> 0` { exact h } @@ -349,7 +349,7 @@ begin calc ∫⁻ (a : α), nnnorm (c • f a) ∂μ = ∫⁻ (a : α), (nnnorm c) * nnnorm (f a) ∂μ : by simp only [nnnorm_smul, ennreal.coe_mul] - ... < ⊤ : + ... < ∞ : begin rw lintegral_const_mul', exacts [mul_lt_top coe_lt_top hfi, coe_ne_top] @@ -411,7 +411,7 @@ lemma integrable_congr {f g : α → β} (h : f =ᵐ[μ] g) : integrable f μ ↔ integrable g μ := ⟨λ hf, hf.congr h, λ hg, hg.congr h.symm⟩ -lemma integrable_const_iff {c : β} : integrable (λ x : α, c) μ ↔ c = 0 ∨ μ univ < ⊤ := +lemma integrable_const_iff {c : β} : integrable (λ x : α, c) μ ↔ c = 0 ∨ μ univ < ∞ := begin have : ae_measurable (λ (x : α), c) μ := measurable_const.ae_measurable, rw [integrable, and_iff_right this, has_finite_integral_const_iff] @@ -438,7 +438,7 @@ h.mono_measure $ measure.le_add_left $ le_refl _ integrable f (μ + ν) ↔ integrable f μ ∧ integrable f ν := ⟨λ h, ⟨h.left_of_add_measure, h.right_of_add_measure⟩, λ h, h.1.add_measure h.2⟩ -lemma integrable.smul_measure {f : α → β} (h : integrable f μ) {c : ℝ≥0∞} (hc : c < ⊤) : +lemma integrable.smul_measure {f : α → β} (h : integrable f μ) {c : ℝ≥0∞} (hc : c < ∞) : integrable f (c • μ) := ⟨h.ae_measurable.smul_measure c, h.has_finite_integral.smul_measure hc⟩ @@ -449,7 +449,7 @@ by simp [integrable, hg, hg.comp_measurable hf, has_finite_integral, lintegral_m lemma lintegral_edist_lt_top [second_countable_topology β] [opens_measurable_space β] {f g : α → β} (hf : integrable f μ) (hg : integrable g μ) : - ∫⁻ a, edist (f a) (g a) ∂μ < ⊤ := + ∫⁻ a, edist (f a) (g a) ∂μ < ∞ := lt_of_le_of_lt (lintegral_edist_triangle hf.ae_measurable hg.ae_measurable (measurable_const.ae_measurable : ae_measurable (λa, (0 : β)) μ)) @@ -467,7 +467,7 @@ lemma integrable.add' [opens_measurable_space β] {f g : α → β} (hf : integr calc ∫⁻ a, nnnorm (f a + g a) ∂μ ≤ ∫⁻ a, nnnorm (f a) + nnnorm (g a) ∂μ : lintegral_mono (λ a, by exact_mod_cast nnnorm_add_le _ _) ... = _ : lintegral_nnnorm_add hf.ae_measurable hg.ae_measurable -... < ⊤ : add_lt_top.2 ⟨hf.has_finite_integral, hg.has_finite_integral⟩ +... < ∞ : add_lt_top.2 ⟨hf.has_finite_integral, hg.has_finite_integral⟩ lemma integrable.add [borel_space β] [second_countable_topology β] {f g : α → β} (hf : integrable f μ) (hg : integrable g μ) : integrable (f + g) μ := @@ -494,7 +494,7 @@ calc ∫⁻ a, nnnorm (f a - g a) ∂μ ≤ ∫⁻ a, nnnorm (f a) + nnnorm (-g lintegral_mono (assume a, by { simp only [sub_eq_add_neg], exact_mod_cast nnnorm_add_le _ _ } ) ... = _ : by { simp only [nnnorm_neg], exact lintegral_nnnorm_add hf.ae_measurable hg.ae_measurable } -... < ⊤ : add_lt_top.2 ⟨hf.has_finite_integral, hg.has_finite_integral⟩ +... < ∞ : add_lt_top.2 ⟨hf.has_finite_integral, hg.has_finite_integral⟩ lemma integrable.sub [borel_space β] [second_countable_topology β] {f g : α → β} (hf : integrable f μ) (hg : integrable g μ) : integrable (f - g) μ := @@ -557,7 +557,7 @@ begin simp_rw [integrable, ae_measurable_smul_const hc, and.congr_right_iff, has_finite_integral, nnnorm_smul, ennreal.coe_mul], intro hf, rw [lintegral_mul_const' _ _ ennreal.coe_ne_top, ennreal.mul_lt_top_iff], - have : ∀ x : ℝ≥0∞, x = 0 → x < ⊤ := by simp, + have : ∀ x : ℝ≥0∞, x = 0 → x < ∞ := by simp, simp [hc, or_iff_left_of_imp (this _)] end end normed_space_over_complete_field @@ -575,7 +575,7 @@ 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 : α →ₘ[μ] β) ⊤ +def integrable (f : α →ₘ[μ] β) : Prop := f ∈ ball (0 : α →ₘ[μ] β) ∞ lemma integrable_mk {f : α → β} (hf : ae_measurable f μ ) : (integrable (mk f hf : α →ₘ[μ] β)) ↔ measure_theory.integrable f μ := @@ -607,7 +607,7 @@ lemma integrable.sub {f g : α →ₘ[μ] β} (hf : integrable f) (hg : integrab integrable (f - g) := hf.add hg.neg -protected lemma is_add_subgroup : is_add_subgroup (ball (0 : α →ₘ[μ] β) ⊤) := +protected lemma is_add_subgroup : is_add_subgroup (ball (0 : α →ₘ[μ] β) ∞) := { zero_mem := integrable_zero, add_mem := λ _ _, integrable.add, neg_mem := λ _, integrable.neg } @@ -662,7 +662,7 @@ 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 ⊤ +instance : metric_space (α →₁[μ] β) := metric_space_emetric_ball 0 ∞ end @@ -811,7 +811,7 @@ 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 lintegral_edist_to_fun_lt_top (f g : α →₁[μ] β) : (∫⁻ a, edist (f a) (g a) ∂μ) < ⊤ := +lemma lintegral_edist_to_fun_lt_top (f g : α →₁[μ] β) : (∫⁻ a, edist (f a) (g a) ∂μ) < ∞ := lintegral_edist_lt_top f.integrable g.integrable variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 β] diff --git a/src/measure_theory/lp_space.lean b/src/measure_theory/lp_space.lean index f7322f0b524af..01476db4c1c85 100644 --- a/src/measure_theory/lp_space.lean +++ b/src/measure_theory/lp_space.lean @@ -60,17 +60,17 @@ def snorm_ess_sup (f : α → F) (μ : measure α) := ess_sup (λ x, (nnnorm (f /-- `ℒp` seminorm, equal to `0` for `p=0`, to `(∫ ∥f a∥^p ∂μ) ^ (1/p)` for `0 < p < ∞` and to `ess_sup ∥f∥ μ` for `p = ∞`. -/ def snorm (f : α → F) (q : ℝ≥0∞) (μ : measure α) : ℝ≥0∞ := -if q = 0 then 0 else (if q = ⊤ then snorm_ess_sup f μ else snorm' f (ennreal.to_real q) μ) +if q = 0 then 0 else (if q = ∞ then snorm_ess_sup f μ else snorm' f (ennreal.to_real q) μ) -lemma snorm_eq_snorm' (hq_ne_zero : q ≠ 0) (hq_ne_top : q ≠ ⊤) {f : α → F} : +lemma snorm_eq_snorm' (hq_ne_zero : q ≠ 0) (hq_ne_top : q ≠ ∞) {f : α → F} : snorm f q μ = snorm' f (ennreal.to_real q) μ := by simp [snorm, hq_ne_zero, hq_ne_top] -@[simp] lemma snorm_exponent_top {f : α → F} : snorm f ⊤ μ = snorm_ess_sup f μ := by simp [snorm] +@[simp] lemma snorm_exponent_top {f : α → F} : snorm f ∞ μ = snorm_ess_sup f μ := by simp [snorm] /-- The property that `f:α→E` is ae_measurable and `(∫ ∥f a∥^p ∂μ)^(1/p)` is finite -/ def mem_ℒp (f : α → E) (p : ℝ≥0∞) (μ : measure α) : Prop := -ae_measurable f μ ∧ snorm f p μ < ⊤ +ae_measurable f μ ∧ snorm f p μ < ∞ lemma lintegral_rpow_nnnorm_eq_rpow_snorm' {f : α → F} (hp0_lt : 0 < p) : ∫⁻ a, (nnnorm (f a)) ^ p ∂μ = (snorm' f p μ) ^ p := @@ -88,13 +88,13 @@ by simp_rw [integrable, has_finite_integral, mem_ℒp, section top -lemma mem_ℒp.snorm_lt_top {f : α → E} (hfp : mem_ℒp f q μ) : snorm f q μ < ⊤ := hfp.2 +lemma mem_ℒp.snorm_lt_top {f : α → E} (hfp : mem_ℒp f q μ) : snorm f q μ < ∞ := hfp.2 -lemma mem_ℒp.snorm_ne_top {f : α → E} (hfp : mem_ℒp f q μ) : snorm f q μ ≠ ⊤ := ne_of_lt (hfp.2) +lemma mem_ℒp.snorm_ne_top {f : α → E} (hfp : mem_ℒp f q μ) : snorm f q μ ≠ ∞ := ne_of_lt (hfp.2) lemma lintegral_rpow_nnnorm_lt_top_of_snorm'_lt_top {f : α → F} (hp0_lt : 0 < p) - (hfp : snorm' f p μ < ⊤) : - ∫⁻ a, (nnnorm (f a)) ^ p ∂μ < ⊤ := + (hfp : snorm' f p μ < ∞) : + ∫⁻ a, (nnnorm (f a)) ^ p ∂μ < ∞ := begin rw lintegral_rpow_nnnorm_eq_rpow_snorm' hp0_lt, exact ennreal.rpow_lt_top_of_nonneg (le_of_lt hp0_lt) (ne_of_lt hfp), @@ -133,7 +133,7 @@ end begin by_cases h0 : q = 0, { simp [h0], }, - by_cases h_top : q = ⊤, + by_cases h_top : q = ∞, { simp only [h_top, snorm_exponent_top, snorm_ess_sup_zero], }, rw ←ne.def at h0, simp [snorm_eq_snorm' h0 h_top, @@ -148,7 +148,7 @@ by simp [snorm', hp_pos] lemma snorm'_measure_zero_of_exponent_zero {f : α → F} : snorm' f 0 0 = 1 := by simp [snorm'] -lemma snorm'_measure_zero_of_neg {f : α → F} (hp_neg : p < 0) : snorm' f p 0 = ⊤ := +lemma snorm'_measure_zero_of_neg {f : α → F} (hp_neg : p < 0) : snorm' f p 0 = ∞ := by simp [snorm', hp_neg] @[simp] lemma snorm_ess_sup_measure_zero {f : α → F} : snorm_ess_sup f 0 = 0 := @@ -158,7 +158,7 @@ by simp [snorm_ess_sup] begin by_cases h0 : q = 0, { simp [h0], }, - by_cases h_top : q = ⊤, + by_cases h_top : q = ∞, { simp [h_top], }, rw ←ne.def at h0, simp [snorm_eq_snorm' h0 h_top, snorm', @@ -205,13 +205,13 @@ by simp [snorm'_const c hp_pos, measure_univ] lemma snorm_const (c : F) (h0 : q ≠ 0) (hμ : μ ≠ 0) : snorm (λ x : α , c) q μ = (nnnorm c : ℝ≥0∞) * (μ set.univ) ^ (1/(ennreal.to_real q)) := begin - by_cases h_top : q = ⊤, + by_cases h_top : q = ∞, { simp [h_top, snorm_ess_sup_const c hμ], }, simp [snorm_eq_snorm' h0 h_top, snorm'_const, ennreal.to_real_pos_iff.mpr ⟨lt_of_le_of_ne (zero_le _) h0.symm, h_top⟩], end -lemma snorm_const' (c : F) (h0 : q ≠ 0) (h_top: q ≠ ⊤) : +lemma snorm_const' (c : F) (h0 : q ≠ 0) (h_top: q ≠ ∞) : snorm (λ x : α , c) q μ = (nnnorm c : ℝ≥0∞) * (μ set.univ) ^ (1/(ennreal.to_real q)) := begin simp [snorm_eq_snorm' h0 h_top, snorm'_const, @@ -248,7 +248,7 @@ lemma snorm_congr_ae {f g : α → F} (hfg : f =ᵐ[μ] g) : snorm f q μ = snor begin by_cases h0 : q = 0, { simp [h0], }, - by_cases h_top : q = ⊤, + by_cases h_top : q = ∞, { rw [h_top, snorm_exponent_top], exact snorm_ess_sup_congr_ae hfg, }, repeat { rw snorm_eq_snorm' h0 h_top, }, @@ -316,7 +316,7 @@ end lemma snorm_eq_zero_iff {f : α → E} (hf : ae_measurable f μ) (h0 : q ≠ 0) : snorm f q μ = 0 ↔ f =ᵐ[μ] 0 := begin - by_cases h_top : q = ⊤, + by_cases h_top : q = ∞, { rw [h_top, snorm_exponent_top, snorm_ess_sup_eq_zero_iff], }, rw snorm_eq_snorm' h0 h_top, exact snorm'_eq_zero_iff @@ -331,7 +331,7 @@ end opens_measurable_space begin by_cases h0 : q = 0, { simp [h0], }, - by_cases h_top : q = ⊤, + by_cases h_top : q = ∞, { simp [h_top, snorm_ess_sup], }, simp [snorm_eq_snorm' h0 h_top], end @@ -403,8 +403,8 @@ begin by_cases hp0 : p = 0, { simp [hp0], }, rw ←ne.def at hp0, - by_cases hq_top : q = ⊤, - { by_cases hp_top : p = ⊤, + by_cases hq_top : q = ∞, + { by_cases hp_top : p = ∞, { rw [hq_top, hp_top], exact le_refl _, }, { have hp_pos : 0 < p.to_real, @@ -412,7 +412,7 @@ begin rw [snorm_eq_snorm' hp0 hp_top, hq_top, snorm_exponent_top], refine le_trans (snorm'_le_snorm_ess_sup_mul_rpow_measure_univ hp_pos) (le_of_eq _), simp [measure_univ], }, }, - { have hp_top : p ≠ ⊤, + { have hp_top : p ≠ ∞, { by_contra hp_eq_top, push_neg at hp_eq_top, refine hq_top _, @@ -431,8 +431,8 @@ begin end lemma snorm'_lt_top_of_snorm'_lt_top_of_exponent_le {p q : ℝ} [finite_measure μ] {f : α → E} - (hf : ae_measurable f μ) (hfq_lt_top : snorm' f q μ < ⊤) (hp_nonneg : 0 ≤ p) (hpq : p ≤ q) : - snorm' f p μ < ⊤ := + (hf : ae_measurable f μ) (hfq_lt_top : snorm' f q μ < ∞) (hp_nonneg : 0 ≤ p) (hpq : p ≤ q) : + snorm' f p μ < ∞ := begin cases le_or_lt p 0 with hp_nonpos hp_pos, { rw le_antisymm hp_nonpos hp_nonneg, @@ -441,7 +441,7 @@ begin calc snorm' f p μ ≤ snorm' f q μ * (μ set.univ) ^ (1/p - 1/q) : snorm'_le_snorm'_mul_rpow_measure_univ hp_pos hpq hf - ... < ⊤ : + ... < ∞ : begin rw ennreal.mul_lt_top_iff, refine or.inl ⟨hfq_lt_top, ennreal.rpow_lt_top_of_nonneg _ (measure_ne_top μ set.univ)⟩, @@ -458,14 +458,14 @@ begin { rwa [hp0, mem_ℒp_zero_iff_ae_measurable], }, rw ←ne.def at hp0, refine ⟨hfq_m, _⟩, - by_cases hp_top : p = ⊤, - { have hq_top : q = ⊤, + by_cases hp_top : p = ∞, + { have hq_top : q = ∞, by rwa [hp_top, top_le_iff] at hpq, rw [hp_top], rwa hq_top at hfq_lt_top, }, have hp_pos : 0 < p.to_real, from ennreal.to_real_pos_iff.mpr ⟨lt_of_le_of_ne (zero_le _) hp0.symm, hp_top⟩, - by_cases hq_top : q = ⊤, + by_cases hq_top : q = ∞, { rw snorm_eq_snorm' hp0 hp_top, rw [hq_top, snorm_exponent_top] at hfq_lt_top, refine lt_of_le_of_lt (snorm'_le_snorm_ess_sup_mul_rpow_measure_univ hp_pos) _, @@ -514,7 +514,7 @@ lemma snorm_add_le {f g : α → E} (hf : ae_measurable f μ) (hg : ae_measurabl begin by_cases hq0 : q = 0, { simp [hq0], }, - by_cases hq_top : q = ⊤, + by_cases hq_top : q = ∞, { simp [hq_top, snorm_ess_sup_add_le], }, have hq1_real : 1 ≤ q.to_real, by rwa [←ennreal.one_to_real, ennreal.to_real_le_to_real ennreal.one_ne_top hq_top], @@ -524,12 +524,12 @@ end lemma snorm_add_lt_top_of_one_le {f g : α → E} (hf : mem_ℒp f q μ) (hg : mem_ℒp g q μ) (hq1 : 1 ≤ q) : - snorm (f + g) q μ < ⊤ := + snorm (f + g) q μ < ∞ := lt_of_le_of_lt (snorm_add_le hf.1 hg.1 hq1) (ennreal.add_lt_top.mpr ⟨hf.2, hg.2⟩) lemma snorm'_add_lt_top_of_le_one {f g : α → E} (hf : ae_measurable f μ) (hg : ae_measurable g μ) - (hf_snorm : snorm' f p μ < ⊤) (hg_snorm : snorm' g p μ < ⊤) (hp_pos : 0 < p) (hp1 : p ≤ 1) : - snorm' (f + g) p μ < ⊤ := + (hf_snorm : snorm' f p μ < ∞) (hg_snorm : snorm' g p μ < ∞) (hp_pos : 0 < p) (hp1 : p ≤ 1) : + snorm' (f + g) p μ < ∞ := calc (∫⁻ a, ↑(nnnorm ((f + g) a)) ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ a, (((λ a, (nnnorm (f a) : ℝ≥0∞)) + (λ a, (nnnorm (g a) : ℝ≥0∞))) a) ^ p ∂μ) ^ (1 / p) : @@ -543,7 +543,7 @@ begin refine @ennreal.rpow_le_rpow _ _ (1/p) (lintegral_mono (λ a, _)) (by simp [hp_pos.le]), exact ennreal.rpow_add_le_add_rpow _ _ hp_pos hp1, end -... < ⊤ : +... < ∞ : begin refine @ennreal.rpow_lt_top_of_nonneg _ (1/p) (by simp [hp_pos.le]) _, rw [lintegral_add' hf.nnnorm.ennreal_coe.ennreal_rpow_const @@ -554,14 +554,14 @@ begin end lemma snorm_add_lt_top {f g : α → E} (hf : mem_ℒp f q μ) (hg : mem_ℒp g q μ) : - snorm (f + g) q μ < ⊤ := + snorm (f + g) q μ < ∞ := begin by_cases h0 : q = 0, { simp [h0], }, rw ←ne.def at h0, cases le_total 1 q with hq1 hq1, { exact snorm_add_lt_top_of_one_le hf hg hq1, }, - have hq_top : q ≠ ⊤, from (lt_of_le_of_lt hq1 ennreal.coe_lt_top).ne, + have hq_top : q ≠ ∞, from (lt_of_le_of_lt hq1 ennreal.coe_lt_top).ne, have hq_pos : 0 < q.to_real, { rw [←ennreal.zero_to_real, @ennreal.to_real_lt_to_real 0 q ennreal.coe_ne_top hq_top], exact ((zero_le q).lt_of_ne h0.symm), }, @@ -616,7 +616,7 @@ lemma snorm_const_smul {f : α → F} (c : 𝕜) : begin by_cases h0 : q = 0, { simp [h0], }, - by_cases h_top : q = ⊤, + by_cases h_top : q = ∞, { simp [h_top, snorm_ess_sup_const_smul], }, repeat { rw snorm_eq_snorm' h0 h_top, }, rw ←ne.def at h0, @@ -646,7 +646,7 @@ end ℒp /-! ### Lp space -The space of equivalence classes of measurable functions for which `snorm f p μ < ⊤`. +The space of equivalence classes of measurable functions for which `snorm f p μ < ∞`. -/ @[simp] lemma snorm_ae_eq_fun {α E : Type*} [measurable_space α] {μ : measure α} @@ -656,14 +656,14 @@ snorm_congr_ae (ae_eq_fun.coe_fn_mk _ _) lemma mem_ℒp.snorm_mk_lt_top {α E : Type*} [measurable_space α] {μ : measure α} [measurable_space E] [normed_group E] {p : ℝ≥0∞} {f : α → E} (hfp : mem_ℒp f p μ) : - snorm (ae_eq_fun.mk f hfp.1) p μ < ⊤ := + snorm (ae_eq_fun.mk f hfp.1) p μ < ∞ := by simp [hfp.2] /-- Lp space -/ def Lp {α} (E : Type*) [measurable_space α] [measurable_space E] [normed_group E] [borel_space E] [topological_space.second_countable_topology E] (p : ℝ≥0∞) (μ : measure α) : add_subgroup (α →ₘ[μ] E) := -{ carrier := {f | snorm f p μ < ⊤}, +{ carrier := {f | snorm f p μ < ∞}, zero_mem' := by simp [snorm_congr_ae ae_eq_fun.coe_fn_zero, snorm_zero], add_mem' := λ f g hf hg, by simp [snorm_congr_ae (ae_eq_fun.coe_fn_add _ _), snorm_add_lt_top ⟨f.ae_measurable, hf⟩ ⟨g.ae_measurable, hg⟩], @@ -686,17 +686,17 @@ namespace Lp variables {α E F : Type*} [measurable_space α] {μ : measure α} [measurable_space E] [normed_group E] [borel_space E] [topological_space.second_countable_topology E] {p : ℝ≥0∞} -lemma mem_Lp_iff_snorm_lt_top {f : α →ₘ[μ] E} : f ∈ Lp E p μ ↔ snorm f p μ < ⊤ := iff.refl _ +lemma mem_Lp_iff_snorm_lt_top {f : α →ₘ[μ] E} : f ∈ Lp E p μ ↔ snorm f p μ < ∞ := iff.refl _ lemma antimono [finite_measure μ] {p q : ℝ≥0∞} (hpq : p ≤ q) : Lp E q μ ≤ Lp E p μ := λ f hf, (mem_ℒp.mem_ℒp_of_exponent_le ⟨f.ae_measurable, hf⟩ hpq).2 -lemma coe_fn_mk {f : α →ₘ[μ] E} (hf : snorm f p μ < ⊤) : ⇑(⟨f, hf⟩ : Lp E p μ) =ᵐ[μ] f := +lemma coe_fn_mk {f : α →ₘ[μ] E} (hf : snorm f p μ < ∞) : ⇑(⟨f, hf⟩ : Lp E p μ) =ᵐ[μ] f := by simp only [coe_fn_coe_base, subtype.coe_mk] -lemma snorm_lt_top (f : Lp E p μ) : snorm f p μ < ⊤ := f.prop +lemma snorm_lt_top (f : Lp E p μ) : snorm f p μ < ∞ := f.prop -lemma snorm_ne_top (f : Lp E p μ) : snorm f p μ ≠ ⊤ := (snorm_lt_top f).ne +lemma snorm_ne_top (f : Lp E p μ) : snorm f p μ ≠ ∞ := (snorm_lt_top f).ne lemma measurable (f : Lp E p μ) : measurable f := f.val.measurable diff --git a/src/measure_theory/measure_space.lean b/src/measure_theory/measure_space.lean index 342dcc63641d9..62aed236ec8f0 100644 --- a/src/measure_theory/measure_space.lean +++ b/src/measure_theory/measure_space.lean @@ -28,10 +28,10 @@ Measures on `α` form a complete lattice, and are closed under scalar multiplica We introduce the following typeclasses for measures: * `probability_measure μ`: `μ univ = 1`; -* `finite_measure μ`: `μ univ < ⊤`; +* `finite_measure μ`: `μ univ < ∞`; * `sigma_finite μ`: there exists a countable collection of measurable sets that cover `univ` where `μ` is finite; -* `locally_finite_measure μ` : `∀ x, ∃ s ∈ 𝓝 x, μ s < ⊤`; +* `locally_finite_measure μ` : `∀ x, ∃ s ∈ 𝓝 x, μ s < ∞`; * `has_no_atoms μ` : `∀ x, μ {x} = 0`; possibly should be redefined as `∀ s, 0 < μ s → ∃ t ⊆ s, 0 < μ t ∧ μ t < μ s`. @@ -194,7 +194,7 @@ lemma measure_mono (h : s₁ ⊆ s₂) : μ s₁ ≤ μ s₂ := μ.mono h lemma measure_mono_null (h : s₁ ⊆ s₂) (h₂ : μ s₂ = 0) : μ s₁ = 0 := nonpos_iff_eq_zero.1 $ h₂ ▸ measure_mono h -lemma measure_mono_top (h : s₁ ⊆ s₂) (h₁ : μ s₁ = ⊤) : μ s₂ = ⊤ := +lemma measure_mono_top (h : s₁ ⊆ s₂) (h₁ : μ s₁ = ∞) : μ s₂ = ∞ := top_unique $ h₁ ▸ measure_mono h lemma exists_measurable_superset (μ : measure α) (s : set α) : @@ -242,7 +242,7 @@ begin end lemma measure_bUnion_lt_top {s : set β} {f : β → set α} (hs : finite s) - (hfin : ∀ i ∈ s, μ (f i) < ⊤) : μ (⋃ i ∈ s, f i) < ⊤ := + (hfin : ∀ i ∈ s, μ (f i) < ∞) : μ (⋃ i ∈ s, f i) < ∞ := begin convert (measure_bUnion_finset_le hs.to_finset f).trans_lt _, { ext, rw [finite.mem_to_finset] }, @@ -410,14 +410,14 @@ by simp only [← measure_bUnion_finset (pairwise_on_disjoint_fiber _ _) hf, finset.set_bUnion_preimage_singleton] lemma measure_diff (h : s₂ ⊆ s₁) (h₁ : measurable_set s₁) (h₂ : measurable_set s₂) - (h_fin : μ s₂ < ⊤) : + (h_fin : μ s₂ < ∞) : μ (s₁ \ s₂) = μ s₁ - μ s₂ := begin refine (ennreal.add_sub_self' h_fin).symm.trans _, rw [← measure_union disjoint_diff h₂ (h₁.diff h₂), union_diff_cancel h] end -lemma measure_compl (h₁ : measurable_set s) (h_fin : μ s < ⊤) : μ (sᶜ) = μ univ - μ s := +lemma measure_compl (h₁ : measurable_set s) (h_fin : μ s < ∞) : μ (sᶜ) = μ univ - μ s := by { rw compl_eq_univ_diff, exact measure_diff (subset_univ s) measurable_set.univ h₁ h_fin } lemma sum_measure_le_measure_univ {s : finset ι} {t : ι → set α} (h : ∀ i ∈ s, measurable_set (t i)) @@ -492,7 +492,7 @@ end sets is the infimum of the measures. -/ lemma measure_Inter_eq_infi [encodable ι] {s : ι → set α} (h : ∀ i, measurable_set (s i)) (hd : directed (⊇) s) - (hfin : ∃ i, μ (s i) < ⊤) : + (hfin : ∃ i, μ (s i) < ∞) : μ (⋂ i, s i) = (⨅ i, μ (s i)) := begin rcases hfin with ⟨k, hk⟩, @@ -536,7 +536,7 @@ end /-- Continuity from above: the measure of the intersection of a decreasing sequence of measurable sets is the limit of the measures. -/ lemma tendsto_measure_Inter {s : ℕ → set α} - (hs : ∀ n, measurable_set (s n)) (hm : ∀ ⦃n m⦄, n ≤ m → s m ⊆ s n) (hf : ∃ i, μ (s i) < ⊤) : + (hs : ∀ n, measurable_set (s n)) (hm : ∀ ⦃n m⦄, n ≤ m → s m ⊆ s n) (hf : ∃ i, μ (s i) < ∞) : tendsto (μ ∘ s) at_top (𝓝 (μ (⋂ n, s n))) := begin rw measure_Inter_eq_infi hs (directed_of_sup hm) hf, @@ -546,7 +546,7 @@ end /-- One direction of the Borel-Cantelli lemma: if (sᵢ) is a sequence of measurable sets such that ∑ μ sᵢ exists, then the limit superior of the sᵢ is a null set. -/ lemma measure_limsup_eq_zero {s : ℕ → set α} (hs : ∀ i, measurable_set (s i)) - (hs' : ∑' i, μ (s i) ≠ ⊤) : μ (limsup at_top s) = 0 := + (hs' : ∑' i, μ (s i) ≠ ∞) : μ (limsup at_top s) = 0 := begin rw limsup_eq_infi_supr_of_nat', -- We will show that both `μ (⨅ n, ⨆ i, s (i + n))` and `0` are the limit of `μ (⊔ i, s (i + n))` @@ -1116,7 +1116,7 @@ alias ext_iff_of_sUnion_eq_univ ↔ _ measure_theory.measure.ext_of_sUnion_eq_un lemma ext_of_generate_from_of_cover {S T : set (set α)} (h_gen : ‹_› = generate_from S) (hc : countable T) (h_inter : is_pi_system S) - (hm : ∀ t ∈ T, measurable_set t) (hU : ⋃₀ T = univ) (htop : ∀ t ∈ T, μ t < ⊤) + (hm : ∀ t ∈ T, measurable_set t) (hU : ⋃₀ T = univ) (htop : ∀ t ∈ T, μ t < ∞) (ST_eq : ∀ (t ∈ T) (s ∈ S), μ (s ∩ t) = ν (s ∩ t)) (T_eq : ∀ t ∈ T, μ t = ν t) : μ = ν := begin @@ -1143,7 +1143,7 @@ end lemma ext_of_generate_from_of_cover_subset {S T : set (set α)} (h_gen : ‹_› = generate_from S) (h_inter : is_pi_system S) - (h_sub : T ⊆ S) (hc : countable T) (hU : ⋃₀ T = univ) (htop : ∀ s ∈ T, μ s < ⊤) + (h_sub : T ⊆ S) (hc : countable T) (hU : ⋃₀ T = univ) (htop : ∀ s ∈ T, μ s < ∞) (h_eq : ∀ s ∈ S, μ s = ν s) : μ = ν := begin @@ -1160,7 +1160,7 @@ end `finite_spanning_sets_in.ext` is a reformulation of this lemma. -/ lemma ext_of_generate_from_of_Union (C : set (set α)) (B : ℕ → set α) (hA : ‹_› = generate_from C) (hC : is_pi_system C) (h1B : (⋃ i, B i) = univ) - (h2B : ∀ i, B i ∈ C) (hμB : ∀ i, μ (B i) < ⊤) (h_eq : ∀ s ∈ C, μ s = ν s) : μ = ν := + (h2B : ∀ i, B i ∈ C) (hμB : ∀ i, μ (B i) < ∞) (h_eq : ∀ s ∈ C, μ s = ν s) : μ = ν := begin refine ext_of_generate_from_of_cover_subset hA hC _ (countable_range B) h1B _ h_eq, { rintro _ ⟨i, rfl⟩, apply h2B }, @@ -1264,7 +1264,7 @@ lemma count_apply_finite [measurable_singleton_class α] (s : set α) (hs : fini by rw [← count_apply_finset, finite.coe_to_finset] /-- `count` measure evaluates to infinity at infinite sets. -/ -lemma count_apply_infinite (hs : s.infinite) : count s = ⊤ := +lemma count_apply_infinite (hs : s.infinite) : count s = ∞ := begin refine top_unique (le_of_tendsto' ennreal.tendsto_nat_nhds_top $ λ n, _), rcases hs.exists_subset_card_eq n with ⟨t, ht, rfl⟩, @@ -1274,7 +1274,7 @@ begin ... ≤ count s : measure_mono ht end -@[simp] lemma count_apply_eq_top [measurable_singleton_class α] : count s = ⊤ ↔ s.infinite := +@[simp] lemma count_apply_eq_top [measurable_singleton_class α] : count s = ∞ ↔ s.infinite := begin by_cases hs : s.finite, { simp [set.infinite, hs, count_apply_finite] }, @@ -1282,8 +1282,8 @@ begin simp [hs, count_apply_infinite] } end -@[simp] lemma count_apply_lt_top [measurable_singleton_class α] : count s < ⊤ ↔ s.finite := -calc count s < ⊤ ↔ count s ≠ ⊤ : lt_top_iff_ne_top +@[simp] lemma count_apply_lt_top [measurable_singleton_class α] : count s < ∞ ↔ s.finite := +calc count s < ∞ ↔ count s ≠ ∞ : lt_top_iff_ne_top ... ↔ ¬s.infinite : not_congr count_apply_eq_top ... ↔ s.finite : not_not @@ -1316,19 +1316,19 @@ alias absolutely_continuous_of_eq ← eq.absolutely_continuous /-- The filter of sets `s` such that `sᶜ` has finite measure. -/ def cofinite (μ : measure α) : filter α := -{ sets := {s | μ sᶜ < ⊤}, +{ sets := {s | μ sᶜ < ∞}, univ_sets := by simp, inter_sets := λ s t hs ht, by { simp only [compl_inter, mem_set_of_eq], calc μ (sᶜ ∪ tᶜ) ≤ μ sᶜ + μ tᶜ : measure_union_le _ _ - ... < ⊤ : ennreal.add_lt_top.2 ⟨hs, ht⟩ }, + ... < ∞ : ennreal.add_lt_top.2 ⟨hs, ht⟩ }, sets_of_superset := λ s t hs hst, lt_of_le_of_lt (measure_mono $ compl_subset_compl.2 hst) hs } -lemma mem_cofinite : s ∈ μ.cofinite ↔ μ sᶜ < ⊤ := iff.rfl +lemma mem_cofinite : s ∈ μ.cofinite ↔ μ sᶜ < ∞ := iff.rfl -lemma compl_mem_cofinite : sᶜ ∈ μ.cofinite ↔ μ s < ⊤ := +lemma compl_mem_cofinite : sᶜ ∈ μ.cofinite ↔ μ s < ∞ := by rw [mem_cofinite, compl_compl] -lemma eventually_cofinite {p : α → Prop} : (∀ᶠ x in μ.cofinite, p x) ↔ μ {x | ¬p x} < ⊤ := iff.rfl +lemma eventually_cofinite {p : α → Prop} : (∀ᶠ x in μ.cofinite, p x) ↔ μ {x | ¬p x} < ∞ := iff.rfl end measure open measure @@ -1412,7 +1412,7 @@ by simp only [ae_restrict_eq hs, exists_prop, mem_principal_sets, mem_inf_sets]; /-- A version of the Borel-Cantelli lemma: if `sᵢ` is a sequence of measurable sets such that `∑ μ sᵢ` exists, then for almost all `x`, `x` does not belong to almost all `sᵢ`. -/ lemma ae_eventually_not_mem {s : ℕ → set α} (hs : ∀ i, measurable_set (s i)) - (hs' : ∑' i, μ (s i) ≠ ⊤) : ∀ᵐ x ∂ μ, ∀ᶠ n in at_top, x ∉ s n := + (hs' : ∑' i, μ (s i) ≠ ∞) : ∀ᵐ x ∂ μ, ∀ᶠ n in at_top, x ∉ s n := begin refine measure_mono_null _ (measure_limsup_eq_zero hs hs'), rw ←set.le_eq_subset, @@ -1458,10 +1458,10 @@ class probability_measure (μ : measure α) : Prop := (measure_univ : μ univ = instance measure.dirac.probability_measure {x : α} : probability_measure (dirac x) := ⟨dirac_apply_of_mem $ mem_univ x⟩ -/-- A measure `μ` is called finite if `μ univ < ⊤`. -/ -class finite_measure (μ : measure α) : Prop := (measure_univ_lt_top : μ univ < ⊤) +/-- A measure `μ` is called finite if `μ univ < ∞`. -/ +class finite_measure (μ : measure α) : Prop := (measure_univ_lt_top : μ univ < ∞) -instance restrict.finite_measure (μ : measure α) [hs : fact (μ s < ⊤)] : +instance restrict.finite_measure (μ : measure α) [hs : fact (μ s < ∞)] : finite_measure (μ.restrict s) := ⟨by simp [hs.elim]⟩ @@ -1477,10 +1477,10 @@ export probability_measure (measure_univ) has_no_atoms (measure_singleton) attribute [simp] measure_singleton -lemma measure_lt_top (μ : measure α) [finite_measure μ] (s : set α) : μ s < ⊤ := +lemma measure_lt_top (μ : measure α) [finite_measure μ] (s : set α) : μ s < ∞ := (measure_mono (subset_univ s)).trans_lt finite_measure.measure_univ_lt_top -lemma measure_ne_top (μ : measure α) [finite_measure μ] (s : set α) : μ s ≠ ⊤ := +lemma measure_ne_top (μ : measure α) [finite_measure μ] (s : set α) : μ s ≠ ∞ := ne_of_lt (measure_lt_top μ s) /-- `le_of_add_le_add_left` is normally applicable to `ordered_cancel_add_comm_monoid`, @@ -1568,7 +1568,7 @@ namespace measure /-- A measure is called finite at filter `f` if it is finite at some set `s ∈ f`. Equivalently, it is eventually finite at `s` in `f.lift' powerset`. -/ -def finite_at_filter (μ : measure α) (f : filter α) : Prop := ∃ s ∈ f, μ s < ⊤ +def finite_at_filter (μ : measure α) (f : filter α) : Prop := ∃ s ∈ f, μ s < ∞ lemma finite_at_filter_of_finite (μ : measure α) [finite_measure μ] (f : filter α) : μ.finite_at_filter f := @@ -1576,7 +1576,7 @@ lemma finite_at_filter_of_finite (μ : measure α) [finite_measure μ] (f : filt lemma finite_at_filter.exists_mem_basis {μ : measure α} {f : filter α} (hμ : finite_at_filter μ f) {p : ι → Prop} {s : ι → set α} (hf : f.has_basis p s) : - ∃ i (hi : p i), μ (s i) < ⊤ := + ∃ i (hi : p i), μ (s i) < ∞ := (hf.exists_iff (λ s t hst ht, (measure_mono hst).trans_lt ht)).1 hμ lemma finite_at_bot (μ : measure α) : μ.finite_at_filter ⊥ := @@ -1591,14 +1591,14 @@ lemma finite_at_bot (μ : measure α) : μ.finite_at_filter ⊥ := structure finite_spanning_sets_in (μ : measure α) (C : set (set α)) := (set : ℕ → set α) (set_mem : ∀ i, set i ∈ C) -(finite : ∀ i, μ (set i) < ⊤) +(finite : ∀ i, μ (set i) < ∞) (spanning : (⋃ i, set i) = univ) end measure open measure /-- A measure `μ` is called σ-finite if there is a countable collection of sets - `{ A i | i ∈ ℕ }` such that `μ (A i) < ⊤` and `⋃ i, A i = s`. -/ + `{ A i | i ∈ ℕ }` such that `μ (A i) < ∞` and `⋃ i, A i = s`. -/ class sigma_finite (μ : measure α) : Prop := (out' : nonempty (μ.finite_spanning_sets_in {s | measurable_set s})) @@ -1630,7 +1630,7 @@ measurable_set.Union $ λ j, measurable_set.Union_Prop $ λ hij, μ.to_finite_spanning_sets_in.set_mem j lemma measure_spanning_sets_lt_top (μ : measure α) [sigma_finite μ] (i : ℕ) : - μ (spanning_sets μ i) < ⊤ := + μ (spanning_sets μ i) < ∞ := measure_bUnion_lt_top (finite_le_nat i) $ λ j _, μ.to_finite_spanning_sets_in.finite j lemma Union_spanning_sets (μ : measure α) [sigma_finite μ] : @@ -1680,10 +1680,10 @@ lemma sigma_finite_of_not_nonempty (μ : measure α) (hα : ¬ nonempty α) : si ⟨⟨⟨λ _, ∅, λ n, measurable_set.empty, λ n, by simp, by simp [eq_empty_of_not_nonempty hα univ]⟩⟩⟩ lemma sigma_finite_of_countable {S : set (set α)} (hc : countable S) - (hμ : ∀ s ∈ S, μ s < ⊤) (hU : ⋃₀ S = univ) : + (hμ : ∀ s ∈ S, μ s < ∞) (hU : ⋃₀ S = univ) : sigma_finite μ := begin - obtain ⟨s, hμ, hs⟩ : ∃ s : ℕ → set α, (∀ n, μ (s n) < ⊤) ∧ (⋃ n, s n) = univ, + obtain ⟨s, hμ, hs⟩ : ∃ s : ℕ → set α, (∀ n, μ (s n) < ∞) ∧ (⋃ n, s n) = univ, from (exists_seq_cover_iff_countable ⟨∅, by simp⟩).2 ⟨S, hc, hμ, hU⟩, refine ⟨⟨⟨λ n, to_measurable μ (s n), λ n, measurable_set_to_measurable _ _, by simpa, _⟩⟩⟩, exact eq_univ_of_subset (Union_subset_Union $ λ n, subset_to_measurable μ (s n)) hs @@ -1738,7 +1738,7 @@ lemma measure.finite_at_nhds [topological_space α] (μ : measure α) locally_finite_measure.finite_at_nhds x lemma measure.smul_finite {α : Type*} [measurable_space α] (μ : measure α) [finite_measure μ] - {c : ℝ≥0∞} (hc : c < ⊤) : + {c : ℝ≥0∞} (hc : c < ∞) : finite_measure (c • μ) := begin refine ⟨_⟩, @@ -1748,7 +1748,7 @@ end lemma measure.exists_is_open_measure_lt_top [topological_space α] (μ : measure α) [locally_finite_measure μ] (x : α) : - ∃ s : set α, x ∈ s ∧ is_open s ∧ μ s < ⊤ := + ∃ s : set α, x ∈ s ∧ is_open s ∧ μ s < ∞ := by simpa only [exists_prop, and.assoc] using (μ.finite_at_nhds x).exists_mem_basis (nhds_basis_opens x) @@ -1833,7 +1833,7 @@ protected lemma measure_mono (h : μ ≤ ν) : ν.finite_at_filter f → μ.fini ν.finite_at_filter g → μ.finite_at_filter f := λ h, (h.filter_mono hf).measure_mono hμ -protected lemma eventually (h : μ.finite_at_filter f) : ∀ᶠ s in f.lift' powerset, μ s < ⊤ := +protected lemma eventually (h : μ.finite_at_filter f) : ∀ᶠ s in f.lift' powerset, μ s < ∞ := (eventually_lift'_powerset' $ λ s t hst ht, (measure_mono hst).trans_lt ht).2 h lemma filter_sup : μ.finite_at_filter f → μ.finite_at_filter g → μ.finite_at_filter (f ⊔ g) := @@ -1847,7 +1847,7 @@ lemma finite_at_nhds_within [topological_space α] (μ : measure α) [locally_fi μ.finite_at_filter (𝓝[s] x) := (finite_at_nhds μ x).inf_of_left -@[simp] lemma finite_at_principal : μ.finite_at_filter (𝓟 s) ↔ μ s < ⊤ := +@[simp] lemma finite_at_principal : μ.finite_at_filter (𝓟 s) ↔ μ s < ∞ := ⟨λ ⟨t, ht, hμ⟩, (measure_mono ht).trans_lt hμ, λ h, ⟨s, mem_principal_self s, h⟩⟩ /-! ### Subtraction of measures -/ @@ -1857,7 +1857,7 @@ It is the equivalent of `(μ - ν) ⊔ 0` if `μ` and `ν` were signed measures. Compare with `ennreal.has_sub`. Specifically, note that if you have `α = {1,2}`, and `μ {1} = 2`, `μ {2} = 0`, and `ν {2} = 2`, `ν {1} = 0`, then `(μ - ν) {1, 2} = 2`. However, if `μ ≤ ν`, and -`ν univ ≠ ⊤`, then `(μ - ν) + ν = μ`. -/ +`ν univ ≠ ∞`, then `(μ - ν) + ν = μ`. -/ noncomputable instance has_sub {α : Type*} [measurable_space α] : has_sub (measure α) := ⟨λ μ ν, Inf {τ | μ ≤ τ + ν} ⟩ @@ -2387,11 +2387,11 @@ namespace is_compact variables [topological_space α] [measurable_space α] {μ : measure α} {s : set α} lemma finite_measure_of_nhds_within (hs : is_compact s) : - (∀ a ∈ s, μ.finite_at_filter (𝓝[s] a)) → μ s < ⊤ := + (∀ a ∈ s, μ.finite_at_filter (𝓝[s] a)) → μ s < ∞ := by simpa only [← measure.compl_mem_cofinite, measure.finite_at_filter] using hs.compl_mem_sets_of_nhds_within -lemma finite_measure [locally_finite_measure μ] (hs : is_compact s) : μ s < ⊤ := +lemma finite_measure [locally_finite_measure μ] (hs : is_compact s) : μ s < ∞ := hs.finite_measure_of_nhds_within $ λ a ha, μ.finite_at_nhds_within _ _ lemma measure_zero_of_nhds_within (hs : is_compact s) : @@ -2403,6 +2403,6 @@ end is_compact lemma metric.bounded.finite_measure [metric_space α] [proper_space α] [measurable_space α] {μ : measure α} [locally_finite_measure μ] {s : set α} (hs : metric.bounded s) : - μ s < ⊤ := + μ s < ∞ := (measure_mono subset_closure).trans_lt (metric.compact_iff_closed_bounded.2 ⟨is_closed_closure, metric.bounded_closure_of_bounded hs⟩).finite_measure diff --git a/src/measure_theory/outer_measure.lean b/src/measure_theory/outer_measure.lean index bba97b6f14bbd..c6a445a9f6d40 100644 --- a/src/measure_theory/outer_measure.lean +++ b/src/measure_theory/outer_measure.lean @@ -288,9 +288,9 @@ def restrict (s : set α) : outer_measure α →ₗ[ℝ≥0∞] outer_measure α restrict s m t = m (t ∩ s) := by simp [restrict] -theorem top_apply {s : set α} (h : s.nonempty) : (⊤ : outer_measure α) s = ⊤ := +theorem top_apply {s : set α} (h : s.nonempty) : (⊤ : outer_measure α) s = ∞ := let ⟨a, as⟩ := h in -top_unique $ le_trans (by simp [smul_dirac_apply, as]) (le_bsupr ((⊤ : ℝ≥0∞) • dirac a) trivial) +top_unique $ le_trans (by simp [smul_dirac_apply, as]) (le_bsupr (∞ • dirac a) trivial) end basic @@ -311,7 +311,7 @@ let μ := λs, ⨅{f : ℕ → set α} (h : s ⊆ ⋃i, f i), ∑'i, m (f i) in mono := assume s₁ s₂ hs, infi_le_infi $ assume f, infi_le_infi2 $ assume hb, ⟨subset.trans hs hb, le_refl _⟩, Union_nat := assume s, ennreal.le_of_forall_pos_le_add $ begin - assume ε hε (hb : ∑'i, μ (s i) < ⊤), + assume ε hε (hb : ∑'i, μ (s i) < ∞), rcases ennreal.exists_pos_sum_of_encodable (ennreal.coe_lt_coe.2 hε) ℕ with ⟨ε', hε', hl⟩, refine le_trans _ (add_le_add_left (le_of_lt hl) _), rw ← ennreal.tsum_add, @@ -775,7 +775,7 @@ begin end lemma induced_outer_measure_exists_set {s : set α} - (hs : induced_outer_measure m P0 m0 s < ⊤) {ε : ℝ≥0} (hε : 0 < ε) : + (hs : induced_outer_measure m P0 m0 s < ∞) {ε : ℝ≥0} (hε : 0 < ε) : ∃ (t : set α) (ht : P t), s ⊆ t ∧ induced_outer_measure m P0 m0 t ≤ induced_outer_measure m P0 m0 s + ε := begin @@ -912,7 +912,7 @@ lemma exists_measurable_superset_eq_trim (m : outer_measure α) (s : set α) : ∃ t, s ⊆ t ∧ measurable_set t ∧ m t = m.trim s := begin simp only [trim_eq_infi], set ms := ⨅ (t : set α) (st : s ⊆ t) (ht : measurable_set t), m t, - by_cases hs : ms = ⊤, + by_cases hs : ms = ∞, { simp only [hs], simp only [infi_eq_top] at hs, exact ⟨univ, subset_univ s, measurable_set.univ, hs _ (subset_univ s) measurable_set.univ⟩ }, diff --git a/src/measure_theory/prod.lean b/src/measure_theory/prod.lean index 116d4ffa3f75e..674ba25ccef5c 100644 --- a/src/measure_theory/prod.lean +++ b/src/measure_theory/prod.lean @@ -339,7 +339,7 @@ begin { rcases (exists_measurable_superset_of_null hs0) with ⟨s', hs', h2s', h3s'⟩, convert measure_mono (prod_mono hs' (subset_univ _)), simp_rw [hs0, prod_prod h2s' measurable_set.univ, h3s', zero_mul] }, - by_cases hti : ν t = ⊤, + by_cases hti : ν t = ∞, { convert le_top, simp_rw [hti, ennreal.mul_top, hs0, if_false] }, rw [measure_eq_infi' μ], simp_rw [ennreal.infi_mul hti], @@ -350,7 +350,7 @@ begin { rcases (exists_measurable_superset_of_null ht0) with ⟨t', ht', h2t', h3t'⟩, convert measure_mono (prod_mono (subset_univ _) ht'), simp_rw [ht0, prod_prod measurable_set.univ h2t', h3t', mul_zero] }, - by_cases hsi : μ s' = ⊤, + by_cases hsi : μ s' = ∞, { convert le_top, simp_rw [hsi, ennreal.top_mul, ht0, if_false] }, rw [measure_eq_infi' ν], simp_rw [ennreal.mul_infi hsi], @@ -361,11 +361,11 @@ begin end lemma ae_measure_lt_top {s : set (α × β)} (hs : measurable_set s) - (h2s : (μ.prod ν) s < ⊤) : ∀ᵐ x ∂μ, ν (prod.mk x ⁻¹' s) < ⊤ := + (h2s : (μ.prod ν) s < ∞) : ∀ᵐ x ∂μ, ν (prod.mk x ⁻¹' s) < ∞ := by { simp_rw [prod_apply hs] at h2s, refine ae_lt_top (measurable_measure_prod_mk_left hs) h2s } lemma integrable_measure_prod_mk_left {s : set (α × β)} - (hs : measurable_set s) (h2s : (μ.prod ν) s < ⊤) : + (hs : measurable_set s) (h2s : (μ.prod ν) s < ∞) : integrable (λ x, (ν (prod.mk x ⁻¹' s)).to_real) μ := begin refine ⟨(measurable_measure_prod_mk_left hs).to_real.ae_measurable, _⟩, diff --git a/src/measure_theory/prod_group.lean b/src/measure_theory/prod_group.lean index 788393c000ad3..8e95353cdb1ee 100644 --- a/src/measure_theory/prod_group.lean +++ b/src/measure_theory/prod_group.lean @@ -187,7 +187,7 @@ begin have : ∀ x y, E.indicator (λ (z : G), (1 : ℝ≥0∞)) (y * x) = ((λ z, z * x) ⁻¹' E).indicator (λ (b : G), 1) y, { intros x y, symmetry, convert indicator_comp_right (λ y, y * x), ext1 z, simp }, - have h3E : ∀ y, ν ((λ x, x * y) ⁻¹' E) ≠ ⊤ := + have h3E : ∀ y, ν ((λ x, x * y) ⁻¹' E) ≠ ∞ := λ y, ennreal.lt_top_iff_ne_top.mp (h2ν.lt_top_of_is_compact $ (homeomorph.mul_right _).compact_preimage.mpr hE), simp_rw [this, lintegral_mul_const _ (mE _), lintegral_indicator _ (measurable_mul_right _ Em), diff --git a/src/measure_theory/set_integral.lean b/src/measure_theory/set_integral.lean index d78b561096a40..5c95b0d32cb01 100644 --- a/src/measure_theory/set_integral.lean +++ b/src/measure_theory/set_integral.lean @@ -125,7 +125,7 @@ namespace measure_theory section normed_group lemma has_finite_integral_restrict_of_bounded [normed_group E] {f : α → E} {s : set α} - {μ : measure α} {C} (hs : μ s < ⊤) (hf : ∀ᵐ x ∂(μ.restrict s), ∥f x∥ ≤ C) : + {μ : measure α} {C} (hs : μ s < ∞) (hf : ∀ᵐ x ∂(μ.restrict s), ∥f x∥ ≤ C) : has_finite_integral f (μ.restrict s) := by haveI : finite_measure (μ.restrict s) := ⟨by rwa [measure.restrict_apply_univ]⟩; exact has_finite_integral_of_bounded hf @@ -149,7 +149,7 @@ by rw [integrable_on, measure.restrict_univ] lemma integrable_on_zero : integrable_on (λ _, (0:E)) s μ := integrable_zero _ _ _ -lemma integrable_on_const {C : E} : integrable_on (λ _, C) s μ ↔ C = 0 ∨ μ s < ⊤ := +lemma integrable_on_const {C : E} : integrable_on (λ _, C) s μ ↔ C = 0 ∨ μ s < ∞ := integrable_const_iff.trans $ by rw [measure.restrict_apply_univ] lemma integrable_on.mono (h : integrable_on f t ν) (hs : s ⊆ t) (hμ : μ ≤ ν) : @@ -336,7 +336,7 @@ of their images is a subset of `{0}`). -/ @[elab_as_eliminator] lemma integrable.induction (P : (α → E) → Prop) - (h_ind : ∀ (c : E) ⦃s⦄, measurable_set s → μ s < ⊤ → P (s.indicator (λ _, c))) + (h_ind : ∀ (c : E) ⦃s⦄, measurable_set s → μ s < ∞ → P (s.indicator (λ _, c))) (h_sum : ∀ ⦃f g : α → E⦄, set.univ ⊆ f ⁻¹' {0} ∪ g ⁻¹' {0} → integrable f μ → integrable g μ → P f → P g → P (f + g)) (h_closed : is_closed {f : α →₁[μ] E | P f} ) @@ -350,7 +350,7 @@ begin by_cases hc : c = 0, { subst hc, convert h_ind 0 measurable_set.empty (by simp) using 1, simp [const] }, apply h_ind c hs, - have : (nnnorm c : ℝ≥0∞) * μ s < ⊤, + have : (nnnorm c : ℝ≥0∞) * μ s < ∞, { have := @comp_indicator _ _ _ _ (λ x : E, (nnnorm x : ℝ≥0∞)) (const α c) s, dsimp only at this, have h' := h.has_finite_integral, @@ -428,7 +428,7 @@ begin exact measure.map_mono hg measure.restrict_le_self end -lemma norm_set_integral_le_of_norm_le_const_ae {C : ℝ} (hs : μ s < ⊤) +lemma norm_set_integral_le_of_norm_le_const_ae {C : ℝ} (hs : μ s < ∞) (hC : ∀ᵐ x ∂μ.restrict s, ∥f x∥ ≤ C) : ∥∫ x in s, f x ∂μ∥ ≤ C * (μ s).to_real := begin @@ -437,7 +437,7 @@ begin exact norm_integral_le_of_norm_le_const hC end -lemma norm_set_integral_le_of_norm_le_const_ae' {C : ℝ} (hs : μ s < ⊤) +lemma norm_set_integral_le_of_norm_le_const_ae' {C : ℝ} (hs : μ s < ∞) (hC : ∀ᵐ x ∂μ, x ∈ s → ∥f x∥ ≤ C) (hfm : ae_measurable f (μ.restrict s)) : ∥∫ x in s, f x ∂μ∥ ≤ C * (μ s).to_real := begin @@ -453,17 +453,17 @@ begin rwa h1 end -lemma norm_set_integral_le_of_norm_le_const_ae'' {C : ℝ} (hs : μ s < ⊤) (hsm : measurable_set s) +lemma norm_set_integral_le_of_norm_le_const_ae'' {C : ℝ} (hs : μ s < ∞) (hsm : measurable_set s) (hC : ∀ᵐ x ∂μ, x ∈ s → ∥f x∥ ≤ C) : ∥∫ x in s, f x ∂μ∥ ≤ C * (μ s).to_real := norm_set_integral_le_of_norm_le_const_ae hs $ by rwa [ae_restrict_eq hsm, eventually_inf_principal] -lemma norm_set_integral_le_of_norm_le_const {C : ℝ} (hs : μ s < ⊤) +lemma norm_set_integral_le_of_norm_le_const {C : ℝ} (hs : μ s < ∞) (hC : ∀ x ∈ s, ∥f x∥ ≤ C) (hfm : ae_measurable f (μ.restrict s)) : ∥∫ x in s, f x ∂μ∥ ≤ C * (μ s).to_real := norm_set_integral_le_of_norm_le_const_ae' hs (eventually_of_forall hC) hfm -lemma norm_set_integral_le_of_norm_le_const' {C : ℝ} (hs : μ s < ⊤) (hsm : measurable_set s) +lemma norm_set_integral_le_of_norm_le_const' {C : ℝ} (hs : μ s < ∞) (hsm : measurable_set s) (hC : ∀ x ∈ s, ∥f x∥ ≤ C) : ∥∫ x in s, f x ∂μ∥ ≤ C * (μ s).to_real := norm_set_integral_le_of_norm_le_const_ae'' hs hsm $ eventually_of_forall hC diff --git a/src/measure_theory/simple_func_dense.lean b/src/measure_theory/simple_func_dense.lean index 422d486327dc6..1246834daa222 100644 --- a/src/measure_theory/simple_func_dense.lean +++ b/src/measure_theory/simple_func_dense.lean @@ -29,7 +29,7 @@ both pointwise and in `L¹` norm, by a sequence of simple functions. -/ open set filter topological_space -open_locale classical topological_space +open_locale classical topological_space ennreal variables {α β ι E : Type*} namespace measure_theory @@ -203,7 +203,7 @@ begin measure_theory.lintegral_mono (λ x, edist_approx_on_y0_le fmeas h₀ x n) ... = ∫⁻ x, edist y₀ (f x) ∂μ + ∫⁻ x, edist y₀ (f x) ∂μ : measure_theory.lintegral_add this this - ... < ⊤ : + ... < ∞ : add_lt_top.2 ⟨hi, hi⟩ end