chore(measure_theory/measurable_space_def): make measurable_space arguments implicit (#13832)

Author: eric-wieser

src/measure_theory/measurable_space.lean

@@ -484,11 +484,11 @@ m₁.comap prod.fst ⊔ m₂.comap prod.snd
 instance {α β} [m₁ : measurable_space α] [m₂ : measurable_space β] : measurable_space (α × β) :=
 m₁.prod m₂
 
-@[measurability] lemma measurable_fst [measurable_space α] [measurable_space β] :
+@[measurability] lemma measurable_fst {ma : measurable_space α} {mb : measurable_space β} :
   measurable (prod.fst : α × β → α) :=
 measurable.of_comap_le le_sup_left
 
-@[measurability] lemma measurable_snd [measurable_space α] [measurable_space β] :
+@[measurability] lemma measurable_snd {ma : measurable_space α} {mb : measurable_space β} :
   measurable (prod.snd : α × β → β) :=
 measurable.of_comap_le le_sup_right
 
@@ -561,8 +561,8 @@ lemma measurable_set_prod_of_nonempty {s : set α} {t : set β} (h : (s ×ˢ t :
 begin
   rcases h with ⟨⟨x, y⟩, hx, hy⟩,
   refine ⟨λ hst, _, λ h, h.1.prod h.2⟩,
-  have : measurable_set ((λ x, (x, y)) ⁻¹' s ×ˢ t) := measurable_id.prod_mk measurable_const hst,
-  have : measurable_set (prod.mk x ⁻¹' s ×ˢ t) := measurable_const.prod_mk measurable_id hst,
+  have : measurable_set ((λ x, (x, y)) ⁻¹' s ×ˢ t) := measurable_prod_mk_right hst,
+  have : measurable_set (prod.mk x ⁻¹' s ×ˢ t) := measurable_prod_mk_left hst,
   simp * at *
 end
 

src/measure_theory/measurable_space_def.lean

@@ -413,21 +413,21 @@ def measurable [measurable_space α] [measurable_space β] (f : α → β) : Pro
 
 localized "notation `measurable[` m `]` := @measurable _ _ m _" in measure_theory
 
-variables [measurable_space α] [measurable_space β] [measurable_space γ]
+lemma measurable_id {ma : measurable_space α} : measurable (@id α) := λ t, id
 
-lemma measurable_id : measurable (@id α) := λ t, id
+lemma measurable_id' {ma : measurable_space α} : measurable (λ a : α, a) := measurable_id
 
-lemma measurable_id' : measurable (λ a : α, a) := measurable_id
-
-lemma measurable.comp {α β γ} {mα : measurable_space α} {mβ : measurable_space β}
+lemma measurable.comp {mα : measurable_space α} {mβ : measurable_space β}
   {mγ : measurable_space γ} {g : β → γ} {f : α → β} (hg : measurable g) (hf : measurable f) :
   measurable (g ∘ f) :=
 λ t ht, hf (hg ht)
 
-@[simp] lemma measurable_const {a : α} : measurable (λ b : β, a) :=
+@[simp] lemma measurable_const {ma : measurable_space α} {mb : measurable_space β} {a : α} :
+  measurable (λ b : β, a) :=
 assume s hs, measurable_set.const (a ∈ s)
 
-lemma measurable.le {α} {m m0 : measurable_space α} (hm : m ≤ m0) {f : α → β}
+lemma measurable.le {α} {m m0 : measurable_space α} {mb : measurable_space β} (hm : m ≤ m0)
+  {f : α → β}
   (hf : measurable[m] f) : measurable[m0] f :=
 λ s hs, hm _ (hf hs)
 

src/probability/stopping.lean

@@ -267,7 +267,7 @@ begin
   intro i,
   have : u i = (λ p : set.Iic i × α, u p.1 p.2) ∘ (λ x, (⟨i, set.mem_Iic.mpr le_rfl⟩, x)) := rfl,
   rw this,
-  exact (h i).comp_measurable ((@measurable_const _ _ _ (f i) _).prod_mk (@measurable_id _ (f i))),
+  exact (h i).comp_measurable measurable_prod_mk_left,
 end
 
 protected lemma comp {t : ι → α → ι} [topological_space ι] [borel_space ι] [metrizable_space ι]
@@ -280,7 +280,7 @@ begin
     = (λ p : ↥(set.Iic i) × α, u (p.fst : ι) p.snd) ∘ (λ p : ↥(set.Iic i) × α,
       (⟨t (p.fst : ι) p.snd, set.mem_Iic.mpr ((ht_le _ _).trans p.fst.prop)⟩, p.snd)) := rfl,
   rw this,
-  exact (h i).comp_measurable ((ht i).measurable.subtype_mk.prod_mk (@measurable_snd _ _ _ (f i))),
+  exact (h i).comp_measurable ((ht i).measurable.subtype_mk.prod_mk measurable_snd),
 end
 
 section arithmetic
@@ -715,7 +715,7 @@ begin
     rw h_set_eq,
     suffices h_meas : @measurable _ _ (m_set s) (f i) (λ x : s, (x : set.Iic i × α).snd),
       from h_meas (f.mono (min_le_left _ _) _ (hτ.measurable_set_le (min i j))),
-    exact (@measurable_snd _ _ _ (f i)).comp (@measurable_subtype_coe _ m_prod _), },
+    exact measurable_snd.comp (@measurable_subtype_coe _ m_prod _), },
   { suffices h_min_eq_left : (λ x : sᶜ, min ↑((x : set.Iic i × α).fst) (τ (x : set.Iic i × α).snd))
       = λ x : sᶜ, ↑((x : set.Iic i × α).fst),
     { rw [set.restrict, h_min_eq_left],
@@ -798,10 +798,9 @@ begin
   { suffices h_meas : measurable[measurable_space.prod _ (f i)]
         (λ a : ↥(set.Iic i) × α, (a.fst : ℕ)),
       from h_meas (measurable_set_singleton j),
-    exact (@measurable_fst _ α _ (f i)).subtype_coe, },
+    exact measurable_fst.subtype_coe, },
   { have h_le : j ≤ i, from finset.mem_range_succ_iff.mp hj,
-    exact (strongly_measurable.mono (h j) (f.mono h_le)).comp_measurable
-      (@measurable_snd _ α _ (f i)), },
+    exact (strongly_measurable.mono (h j) (f.mono h_le)).comp_measurable measurable_snd, },
   { exact strongly_measurable_const, },
 end