chore(measure_theory/*): rename probability_measure and finite_measure (#8831)

Renamed to `is_probability_measure` and `is_finite_measure`, respectively.  Also, `locally_finite_measure` becomes `is_locally_finite_measure`. See
https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.238337.20Weak.20convergence

Author: hrmacbeth

counterexamples/phillips.lean

@@ -108,7 +108,7 @@ def bounded_integrable_functions [measurable_space α] (μ : measure α) :
 of all bounded functions on a type. This is a technical device, that we will extend through
 Hahn-Banach. -/
 def bounded_integrable_functions_integral_clm [measurable_space α]
-  (μ : measure α) [finite_measure μ] : bounded_integrable_functions μ →L[ℝ] ℝ :=
+  (μ : measure α) [is_finite_measure μ] : bounded_integrable_functions μ →L[ℝ] ℝ :=
 linear_map.mk_continuous
   { to_fun := λ f, ∫ x, f x ∂μ,
     map_add' := λ f g, integral_add f.2 g.2,
@@ -126,7 +126,7 @@ linear_map.mk_continuous
 /-- Given a measure, there exists a continuous linear form on the space of all bounded functions
 (not necessarily measurable) that coincides with the integral on bounded measurable functions. -/
 lemma exists_linear_extension_to_bounded_functions
-  [measurable_space α] (μ : measure α) [finite_measure μ] :
+  [measurable_space α] (μ : measure α) [is_finite_measure μ] :
   ∃ φ : (discrete_copy α →ᵇ ℝ) →L[ℝ] ℝ, ∀ (f : discrete_copy α →ᵇ ℝ),
     integrable f μ → φ f = ∫ x, f x ∂μ :=
 begin
@@ -137,11 +137,11 @@ end
 /-- An arbitrary extension of the integral to all bounded functions, as a continuous linear map.
 It is not at all canonical, and constructed using Hahn-Banach. -/
 def _root_.measure_theory.measure.extension_to_bounded_functions
-  [measurable_space α] (μ : measure α) [finite_measure μ] : (discrete_copy α →ᵇ ℝ) →L[ℝ] ℝ :=
+  [measurable_space α] (μ : measure α) [is_finite_measure μ] : (discrete_copy α →ᵇ ℝ) →L[ℝ] ℝ :=
 (exists_linear_extension_to_bounded_functions μ).some
 
-lemma extension_to_bounded_functions_apply [measurable_space α] (μ : measure α) [finite_measure μ]
-  (f : discrete_copy α →ᵇ ℝ) (hf : integrable f μ) :
+lemma extension_to_bounded_functions_apply [measurable_space α] (μ : measure α)
+  [is_finite_measure μ] (f : discrete_copy α →ᵇ ℝ) (hf : integrable f μ) :
   μ.extension_to_bounded_functions f = ∫ x, f x ∂μ :=
 (exists_linear_extension_to_bounded_functions μ).some_spec f hf
 
@@ -406,7 +406,7 @@ let f := (eval_clm ℝ x).to_bounded_additive_measure in calc
 ... = indicator ((univ \ f.discrete_support) ∩ (s \ {x})) 1 x : rfl
 ... = 0 : by simp
 
-lemma to_functions_to_measure [measurable_space α] (μ : measure α) [finite_measure μ]
+lemma to_functions_to_measure [measurable_space α] (μ : measure α) [is_finite_measure μ]
   (s : set α) (hs : measurable_set s) :
   μ.extension_to_bounded_functions.to_bounded_additive_measure s = (μ s).to_real :=
 begin
@@ -423,7 +423,7 @@ begin
 end
 
 lemma to_functions_to_measure_continuous_part [measurable_space α] [measurable_singleton_class α]
-  (μ : measure α) [finite_measure μ] [has_no_atoms μ]
+  (μ : measure α) [is_finite_measure μ] [has_no_atoms μ]
   (s : set α) (hs : measurable_set s) :
   μ.extension_to_bounded_functions.to_bounded_additive_measure.continuous_part s = (μ s).to_real :=
 begin

docs/undergrad.yaml

@@ -532,7 +532,7 @@ Measures and integral Calculus:
 # 11.
 Probability Theory:
   Definitions of a probability space:
-    probability measure: 'measure_theory.probability_measure'
+    probability measure: 'measure_theory.is_probability_measure'
     events:
     independent events: 'probability_theory.Indep_set'
     sigma-algebra: 'measurable_space'

src/analysis/convex/integral.lean

@@ -46,7 +46,7 @@ variables {α E : Type*} [measurable_space α] {μ : measure α}
   [topological_space.second_countable_topology E] [measurable_space E] [borel_space E]
 
 private lemma convex.smul_integral_mem_of_measurable
-  [finite_measure μ] {s : set E} (hs : convex s) (hsc : is_closed s)
+  [is_finite_measure μ] {s : set E} (hs : convex s) (hsc : is_closed s)
   (hμ : μ ≠ 0) {f : α → E} (hfs : ∀ᵐ x ∂μ, f x ∈ s) (hfi : integrable f μ) (hfm : measurable f) :
   (μ univ).to_real⁻¹ • ∫ x, f x ∂μ ∈ s :=
 begin
@@ -79,7 +79,7 @@ integrable function sending `μ`-a.e. points to `s`, then the average value of `
 `(μ univ).to_real⁻¹ • ∫ x, f x ∂μ ∈ s`. See also `convex.center_mass_mem` for a finite sum version
 of this lemma. -/
 lemma convex.smul_integral_mem
-  [finite_measure μ] {s : set E} (hs : convex s) (hsc : is_closed s)
+  [is_finite_measure μ] {s : set E} (hs : convex s) (hsc : is_closed s)
   (hμ : μ ≠ 0) {f : α → E} (hfs : ∀ᵐ x ∂μ, f x ∈ s) (hfi : integrable f μ) :
   (μ univ).to_real⁻¹ • ∫ x, f x ∂μ ∈ s :=
 begin
@@ -96,19 +96,19 @@ end
 /-- If `μ` is a probability measure on `α`, `s` is a convex closed set in `E`, and `f` is an
 integrable function sending `μ`-a.e. points to `s`, then the expected value of `f` belongs to `s`:
 `∫ x, f x ∂μ ∈ s`. See also `convex.sum_mem` for a finite sum version of this lemma. -/
-lemma convex.integral_mem [probability_measure μ] {s : set E} (hs : convex s) (hsc : is_closed s)
+lemma convex.integral_mem [is_probability_measure μ] {s : set E} (hs : convex s) (hsc : is_closed s)
   {f : α → E} (hf : ∀ᵐ x ∂μ, f x ∈ s) (hfi : integrable f μ) :
   ∫ x, f x ∂μ ∈ s :=
-by simpa [measure_univ] using hs.smul_integral_mem hsc (probability_measure.ne_zero μ) hf hfi
+by simpa [measure_univ] using hs.smul_integral_mem hsc (is_probability_measure.ne_zero μ) hf hfi
 
 /-- Jensen's inequality: if a function `g : E → ℝ` is convex and continuous on a convex closed set
 `s`, `μ` is a finite non-zero measure on `α`, and `f : α → E` is a function sending `μ`-a.e. points
 to `s`, then the value of `g` at the average value of `f` is less than or equal to the average value
 of `g ∘ f` provided that both `f` and `g ∘ f` are integrable. See also `convex.map_center_mass_le`
 for a finite sum version of this lemma. -/
-lemma convex_on.map_smul_integral_le [finite_measure μ] {s : set E} {g : E → ℝ} (hg : convex_on s g)
-  (hgc : continuous_on g s) (hsc : is_closed s) (hμ : μ ≠ 0) {f : α → E} (hfs : ∀ᵐ x ∂μ, f x ∈ s)
-  (hfi : integrable f μ) (hgi : integrable (g ∘ f) μ) :
+lemma convex_on.map_smul_integral_le [is_finite_measure μ] {s : set E} {g : E → ℝ}
+  (hg : convex_on s g) (hgc : continuous_on g s) (hsc : is_closed s) (hμ : μ ≠ 0) {f : α → E}
+  (hfs : ∀ᵐ x ∂μ, f x ∈ s) (hfi : integrable f μ) (hgi : integrable (g ∘ f) μ) :
   g ((μ univ).to_real⁻¹ • ∫ x, f x ∂μ) ≤ (μ univ).to_real⁻¹ • ∫ x, g (f x) ∂μ :=
 begin
   set t := {p : E × ℝ | p.1 ∈ s ∧ g p.1 ≤ p.2},
@@ -126,9 +126,9 @@ end
 `s`, then the value of `g` at the expected value of `f` is less than or equal to the expected value
 of `g ∘ f` provided that both `f` and `g ∘ f` are integrable. See also `convex.map_sum_le` for a
 finite sum version of this lemma. -/
-lemma convex_on.map_integral_le [probability_measure μ] {s : set E} {g : E → ℝ} (hg : convex_on s g)
-  (hgc : continuous_on g s) (hsc : is_closed s) {f : α → E} (hfs : ∀ᵐ x ∂μ, f x ∈ s)
-  (hfi : integrable f μ) (hgi : integrable (g ∘ f) μ) :
+lemma convex_on.map_integral_le [is_probability_measure μ] {s : set E} {g : E → ℝ}
+  (hg : convex_on s g) (hgc : continuous_on g s) (hsc : is_closed s) {f : α → E}
+  (hfs : ∀ᵐ x ∂μ, f x ∈ s) (hfi : integrable f μ) (hgi : integrable (g ∘ f) μ) :
   g (∫ x, f x ∂μ) ≤ ∫ x, g (f x) ∂μ :=
 by simpa [measure_univ]
-  using hg.map_smul_integral_le hgc hsc (probability_measure.ne_zero μ) hfs hfi hgi
+  using hg.map_smul_integral_le hgc hsc (is_probability_measure.ne_zero μ) hfs hfi hgi

src/analysis/fourier.lean

@@ -19,7 +19,7 @@ This file contains basic technical results for a development of Fourier series.
 ## Main definitions
 
 * `haar_circle`, Haar measure on the circle, normalized to have total measure `1`
-* instances `measure_space`, `probability_measure` for the circle with respect to this measure
+* instances `measure_space`, `is_probability_measure` for the circle with respect to this measure
 * for `n : ℤ`, `fourier n` is the monomial `λ z, z ^ n`, bundled as a continuous map from `circle`
   to `ℂ`
 * for `n : ℤ` and `p : ℝ≥0∞`, `fourier_Lp p n` is an abbreviation for the monomial `fourier n`
@@ -71,7 +71,7 @@ instance : borel_space circle := ⟨rfl⟩
 /-- Haar measure on the circle, normalized to have total measure 1. -/
 def haar_circle : measure circle := haar_measure positive_compacts_univ
 
-instance : probability_measure haar_circle := ⟨haar_measure_self⟩
+instance : is_probability_measure haar_circle := ⟨haar_measure_self⟩
 
 instance : measure_space circle :=
 { volume := haar_circle,
@@ -198,7 +198,7 @@ begin
   intros i j,
   rw continuous_map.inner_to_Lp haar_circle (fourier i) (fourier j),
   split_ifs,
-  { simp [h, probability_measure.measure_univ, ← fourier_neg, ← fourier_add, -fourier_to_fun] },
+  { simp [h, is_probability_measure.measure_univ, ← fourier_neg, ← fourier_add, -fourier_to_fun] },
   simp only [← fourier_add, ← fourier_neg, is_R_or_C.conj_to_complex],
   have hij : -i + j ≠ 0,
   { rw add_comm,

src/analysis/special_functions/integrals.lean

@@ -35,7 +35,7 @@ variables {a b : ℝ} (n : ℕ)
 
 namespace interval_integral
 open measure_theory
-variables {f : ℝ → ℝ} {μ ν : measure ℝ} [locally_finite_measure μ] (c d : ℝ)
+variables {f : ℝ → ℝ} {μ ν : measure ℝ} [is_locally_finite_measure μ] (c d : ℝ)
 
 /-! ### Interval integrability -/
 

src/dynamics/ergodic/conservative.lean

@@ -53,7 +53,8 @@ structure conservative (f : α → α) (μ : measure α . volume_tac)
 (exists_mem_image_mem : ∀ ⦃s⦄, measurable_set s → μ s ≠ 0 → ∃ (x ∈ s) (m ≠ 0), f^[m] x ∈ s)
 
 /-- A self-map preserving a finite measure is conservative. -/
-protected lemma measure_preserving.conservative [finite_measure μ] (h : measure_preserving f μ μ) :
+protected lemma measure_preserving.conservative [is_finite_measure μ]
+  (h : measure_preserving f μ μ) :
   conservative f μ :=
 ⟨h.quasi_measure_preserving, λ s hsm h0, h.exists_mem_image_mem hsm h0⟩
 

src/dynamics/ergodic/measure_preserving.lean

@@ -134,7 +134,7 @@ end
 `x ∈ s` comes back to `s` under iterations of `f`. Actually, a.e. point of `s` comes back to `s`
 infinitely many times, see `measure_theory.measure_preserving.conservative` and theorems about
 `measure_theory.conservative`. -/
-lemma exists_mem_image_mem [finite_measure μ] (hf : measure_preserving f μ μ)
+lemma exists_mem_image_mem [is_finite_measure μ] (hf : measure_preserving f μ μ)
   (hs : measurable_set s) (hs' : μ s ≠ 0) :
   ∃ (x ∈ s) (m ≠ 0), f^[m] x ∈ s :=
 begin

src/measure_theory/constructions/borel_space.lean

@@ -1088,7 +1088,7 @@ by simpa using is_pi_system_Ioo (coe : ℚ → ℝ)
 
 /-- The intervals `(-(n + 1), (n + 1))` form a finite spanning sets in the set of open intervals
 with rational endpoints for a locally finite measure `μ` on `ℝ`. -/
-def finite_spanning_sets_in_Ioo_rat (μ : measure ℝ) [locally_finite_measure μ] :
+def finite_spanning_sets_in_Ioo_rat (μ : measure ℝ) [is_locally_finite_measure μ] :
   μ.finite_spanning_sets_in (⋃ (a b : ℚ) (h : a < b), {Ioo a b}) :=
 { set := λ n, Ioo (-(n + 1)) (n + 1),
   set_mem := λ n,
@@ -1099,12 +1099,12 @@ def finite_spanning_sets_in_Ioo_rat (μ : measure ℝ) [locally_finite_measure 
     end,
   finite := λ n,
     calc μ (Ioo _ _) ≤ μ (Icc _ _) : μ.mono Ioo_subset_Icc_self
-                 ... < ∞           : is_compact_Icc.finite_measure,
+                 ... < ∞           : is_compact_Icc.is_finite_measure,
   spanning := Union_eq_univ_iff.2 $ λ x,
     ⟨⌊abs x⌋₊, neg_lt.1 ((neg_le_abs_self x).trans_lt (lt_nat_floor_add_one _)),
       (le_abs_self x).trans_lt (lt_nat_floor_add_one _)⟩ }
 
-lemma measure_ext_Ioo_rat {μ ν : measure ℝ} [locally_finite_measure μ]
+lemma measure_ext_Ioo_rat {μ ν : measure ℝ} [is_locally_finite_measure μ]
   (h : ∀ a b : ℚ, μ (Ioo a b) = ν (Ioo a b)) : μ = ν :=
 (finite_spanning_sets_in_Ioo_rat μ).ext borel_eq_generate_from_Ioo_rat is_pi_system_Ioo_rat $
   by { simp only [mem_Union, mem_singleton_iff], rintro _ ⟨a, b, -, rfl⟩, apply h }
@@ -1595,6 +1595,6 @@ is_compact.induction_on h (by simp) (λ s t hst ht, (measure_mono hst).trans_lt
   (λ 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) :
+  [is_locally_finite_measure μ] (h : is_compact s) :
   μ s < ∞ :=
 h.measure_lt_top_of_nhds_within $ λ x hx, μ.finite_at_nhds_within _ _

src/measure_theory/constructions/pi.lean

@@ -486,8 +486,8 @@ instance [h : nonempty ι] [∀ i, has_no_atoms (μ i)] : has_no_atoms (measure.
 h.elim $ λ i, pi_has_no_atoms i
 
 instance [Π i, topological_space (α i)] [∀ i, opens_measurable_space (α i)]
-  [∀ i, locally_finite_measure (μ i)] :
-  locally_finite_measure (measure.pi μ) :=
+  [∀ i, is_locally_finite_measure (μ i)] :
+  is_locally_finite_measure (measure.pi μ) :=
 begin
   refine ⟨λ x, _⟩,
   choose s hxs ho hμ using λ i, (μ i).exists_is_open_measure_lt_top (x i),

src/measure_theory/constructions/prod.lean

@@ -145,7 +145,7 @@ is_pi_system_measurable_set.prod is_pi_system_measurable_set
 
 /-- If `ν` is a finite measure, and `s ⊆ α × β` is measurable, then `x ↦ ν { y | (x, y) ∈ s }` is
   a measurable function. `measurable_measure_prod_mk_left` is strictly more general. -/
-lemma measurable_measure_prod_mk_left_finite [finite_measure ν] {s : set (α × β)}
+lemma measurable_measure_prod_mk_left_finite [is_finite_measure ν] {s : set (α × β)}
   (hs : measurable_set s) : measurable (λ x, ν (prod.mk x ⁻¹' s)) :=
 begin
   refine induction_on_inter generate_from_prod.symm is_pi_system_prod _ _ _ _ hs,