chore(measure_theory/*): rename probability_measure and `finite_mea…

…sure` (#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

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,

src/measure_theory/decomposition/jordan.lean

@@ -49,8 +49,8 @@ namespace measure_theory
 finite measures. -/
 @[ext] structure jordan_decomposition (α : Type*) [measurable_space α] :=
 (pos_part neg_part : measure α)
-[pos_part_finite : finite_measure pos_part]
-[neg_part_finite : finite_measure neg_part]
+[pos_part_finite : is_finite_measure pos_part]
+[neg_part_finite : is_finite_measure neg_part]
 (mutually_singular : pos_part ⊥ₘ neg_part)
 
 attribute [instance] jordan_decomposition.pos_part_finite
@@ -121,7 +121,7 @@ namespace signed_measure
 
 open measure vector_measure jordan_decomposition classical
 
-variables {s : signed_measure α} {μ ν : measure α} [finite_measure μ] [finite_measure ν]
+variables {s : signed_measure α} {μ ν : measure α} [is_finite_measure μ] [is_finite_measure ν]
 
 /-- Given a signed measure `s`, `s.to_jordan_decomposition` is the Jordan decomposition `j`,
 such that `s = j.to_signed_measure`. This property is known as the Jordan decomposition

src/measure_theory/decomposition/lebesgue.lean

@@ -122,17 +122,17 @@ begin
     exact measure.zero_le μ }
 end
 
-instance {μ ν : measure α} [finite_measure μ] :
-  finite_measure (singular_part μ ν) :=
-finite_measure_of_le μ $ singular_part_le μ ν
+instance {μ ν : measure α} [is_finite_measure μ] :
+  is_finite_measure (singular_part μ ν) :=
+is_finite_measure_of_le μ $ singular_part_le μ ν
 
 instance {μ ν : measure α} [sigma_finite μ] :
   sigma_finite (singular_part μ ν) :=
 sigma_finite_of_le μ $ singular_part_le μ ν
 
-instance {μ ν : measure α} [finite_measure μ] :
-  finite_measure (ν.with_density $ radon_nikodym_deriv μ ν) :=
-finite_measure_of_le μ $ with_density_radon_nikodym_deriv_le μ ν
+instance {μ ν : measure α} [is_finite_measure μ] :
+  is_finite_measure (ν.with_density $ radon_nikodym_deriv μ ν) :=
+is_finite_measure_of_le μ $ with_density_radon_nikodym_deriv_le μ ν
 
 instance {μ ν : measure α} [sigma_finite μ] :
   sigma_finite (ν.with_density $ radon_nikodym_deriv μ ν) :=
@@ -259,7 +259,7 @@ a measurable set `E`, such that `ν(E) > 0` and `E` is positive with respect to
 
 This lemma is useful for the Lebesgue decomposition theorem. -/
 lemma exists_positive_of_not_mutually_singular
-  (μ ν : measure α) [finite_measure μ] [finite_measure ν] (h : ¬ μ ⊥ₘ ν) :
+  (μ ν : measure α) [is_finite_measure μ] [is_finite_measure ν] (h : ¬ μ ⊥ₘ ν) :
   ∃ ε : ℝ≥0, 0 < ε ∧ ∃ E : set α, measurable_set E ∧ 0 < ν E ∧
   0 ≤[E] μ.to_signed_measure - (ε • ν).to_signed_measure :=
 begin
@@ -461,7 +461,7 @@ with respect to `ν` and `μ = ξ + ν.with_density f`.
 This is not an instance since this is also shown for the more general σ-finite measures with
 `measure_theory.measure.have_lebesgue_decomposition_of_sigma_finite`. -/
 theorem have_lebesgue_decomposition_of_finite_measure
-  {μ ν : measure α} [finite_measure μ] [finite_measure ν] :
+  {μ ν : measure α} [is_finite_measure μ] [is_finite_measure ν] :
   have_lebesgue_decomposition μ ν :=
 ⟨begin
   have h := @exists_seq_tendsto_Sup _ _ _ _ _ (measurable_le_eval ν μ)
@@ -500,8 +500,8 @@ theorem have_lebesgue_decomposition_of_finite_measure
     simp_rw [supr_apply],
     rw lintegral_supr (λ i, (supr_mem_measurable_le _ hf₁ i).1) (supr_monotone _),
     exact supr_le (λ i, (supr_mem_measurable_le _ hf₁ i).2 B hB) },
-  haveI : finite_measure (ν.with_density ξ),
-  { refine finite_measure_with_density _,
+  haveI : is_finite_measure (ν.with_density ξ),
+  { refine is_finite_measure_with_density _,
     have hle' := hle set.univ measurable_set.univ,
     rw [with_density_apply _ measurable_set.univ, measure.restrict_univ] at hle',
     exact lt_of_le_of_lt hle' (measure_lt_top _ _) },
@@ -575,7 +575,7 @@ end⟩
 local attribute [instance] have_lebesgue_decomposition_of_finite_measure
 
 instance {μ : measure α} {S : μ.finite_spanning_sets_in {s : set α | measurable_set s}} (n : ℕ) :
-  finite_measure (μ.restrict $ S.set n) :=
+  is_finite_measure (μ.restrict $ S.set n) :=
 ⟨by { rw [restrict_apply measurable_set.univ, set.univ_inter], exact S.finite _ }⟩
 
 /-- **The Lebesgue decomposition theorem**: Any pair of σ-finite measures `μ` and `ν`

src/measure_theory/decomposition/unsigned_hahn.lean

@@ -34,7 +34,7 @@ private lemma aux {m : ℕ} {γ d : ℝ} (h : γ - (1 / 2) ^ m < d) :
 by linarith
 
 /-- **Hahn decomposition theorem** -/
-lemma hahn_decomposition [finite_measure μ] [finite_measure ν] :
+lemma hahn_decomposition [is_finite_measure μ] [is_finite_measure ν] :
   ∃s, measurable_set s ∧
     (∀t, measurable_set t → t ⊆ s → ν t ≤ μ t) ∧
     (∀t, measurable_set t → t ⊆ sᶜ → μ t ≤ ν t) :=

src/measure_theory/function/ae_eq_of_integral.lean

@@ -154,7 +154,7 @@ section real
 
 section real_finite_measure
 
-variables [finite_measure μ] {f : α → ℝ}
+variables [is_finite_measure μ] {f : α → ℝ}
 
 /-- Don't use this lemma. Use `ae_nonneg_of_forall_set_integral_nonneg_of_finite_measure`. -/
 lemma ae_nonneg_of_forall_set_integral_nonneg_of_finite_measure_of_measurable (hfm : measurable f)

src/measure_theory/function/conditional_expectation.lean

@@ -464,7 +464,8 @@ lemma integrable_on_condexp_L2_of_measure_ne_top (hm : m ≤ m0) (hμs : μ s 
 integrable_on_Lp_of_measure_ne_top ((condexp_L2 𝕜 hm f) : α →₂[μ] E)
   fact_one_le_two_ennreal.elim hμs
 
-lemma integrable_condexp_L2_of_finite_measure (hm : m ≤ m0) [finite_measure μ] {f : α →₂[μ] E} :
+lemma integrable_condexp_L2_of_is_finite_measure (hm : m ≤ m0) [is_finite_measure μ]
+  {f : α →₂[μ] E} :
   integrable (condexp_L2 𝕜 hm f) μ :=
 integrable_on_univ.mp $ integrable_on_condexp_L2_of_measure_ne_top hm (measure_ne_top _ _) f
 
@@ -478,8 +479,8 @@ lemma norm_condexp_L2_le (hm : m ≤ m0) (f : α →₂[μ] E) : ∥condexp_L2 
 lemma snorm_condexp_L2_le (hm : m ≤ m0) (f : α →₂[μ] E) :
   snorm (condexp_L2 𝕜 hm f) 2 μ ≤ snorm f 2 μ :=
 begin
-  rw [Lp_meas_coe, ← ennreal.to_real_le_to_real (Lp.snorm_ne_top _) (Lp.snorm_ne_top _), ← norm_def,
-    ← norm_def, submodule.norm_coe],
+  rw [Lp_meas_coe, ← ennreal.to_real_le_to_real (Lp.snorm_ne_top _) (Lp.snorm_ne_top _),
+    ← norm_def, ← norm_def, submodule.norm_coe],
   exact norm_condexp_L2_le hm f,
 end