remove unnecessary MeasureTheory.

LorenzoLuccioli · Aug 29, 2024 · 63c3a31 · 63c3a31
1 parent d31bab1
commit 63c3a31
Show file tree

Hide file tree

Showing 5 changed files with 5 additions and 7 deletions.
diff --git a/TestingLowerBounds/FDiv/CondFDiv.lean b/TestingLowerBounds/FDiv/CondFDiv.lean
@@ -207,8 +207,7 @@ lemma condFDiv_zero_left [IsFiniteMeasure μ] [IsFiniteKernel η] :
       EReal.coe_ennreal_ne_bot, EReal.coe_ne_top, EReal.coe_ennreal_pos, Measure.measure_univ_pos,
       EReal.coe_pos, EReal.coe_ennreal_eq_top_iff, measure_ne_top, or_self, not_false_eq_true]
   · simp_rw [EReal.toReal_mul, EReal.toReal_coe, EReal.toReal_coe_ennreal]
-    apply MeasureTheory.Integrable.const_mul
-    exact Kernel.IsFiniteKernel.integrable μ η .univ
+    exact (Kernel.IsFiniteKernel.integrable μ η .univ).const_mul _
 
 lemma condFDiv_zero_left' [IsProbabilityMeasure μ] [IsMarkovKernel η] :
     condFDiv f 0 η μ = f 0 := by

diff --git a/TestingLowerBounds/ForMathlib/RadonNikodym.lean b/TestingLowerBounds/ForMathlib/RadonNikodym.lean
@@ -103,7 +103,7 @@ lemma Measure.mutuallySingular_of_mutuallySingular_compProd {μ ν ξ : Measure
   have hs := h.measurableSet_nullSet
   have hμ_zero:= h.measure_nullSet
   have hν_zero := h.measure_compl_nullSet
-  rw [Measure.compProd_apply, MeasureTheory.lintegral_eq_zero_iff'] at hμ_zero hν_zero
+  rw [Measure.compProd_apply, lintegral_eq_zero_iff'] at hμ_zero hν_zero
   rotate_left
   · exact measurable_kernel_prod_mk_left hs.compl |>.aemeasurable
   · exact measurable_kernel_prod_mk_left hs |>.aemeasurable

diff --git a/TestingLowerBounds/ForMathlib/RnDeriv.lean b/TestingLowerBounds/ForMathlib/RnDeriv.lean
@@ -106,7 +106,7 @@ lemma rnDeriv_eq_div' {ξ : Measure α} [SigmaFinite μ] [SigmaFinite ν] [Sigma
 
 lemma rnDeriv_eq_zero_ae_of_zero_measure (ν : Measure α) {s : Set α} (hs : MeasurableSet s)
     (hμ : μ s = 0) : ∀ᵐ x ∂ν, x ∈ s → (μ.rnDeriv ν) x = 0 := by
-  rw [← MeasureTheory.setLIntegral_eq_zero_iff hs (μ.measurable_rnDeriv ν)]
+  rw [← setLIntegral_eq_zero_iff hs (μ.measurable_rnDeriv ν)]
   exact le_antisymm (hμ ▸ Measure.setLIntegral_rnDeriv_le s) (zero_le _)
 
 --PRed, see #15540

diff --git a/TestingLowerBounds/MeasureCompProd.lean b/TestingLowerBounds/MeasureCompProd.lean
@@ -40,7 +40,7 @@ variable {α β γ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β
 Defined using `MeasureTheory.Measure.bind` -/
 --scoped[ProbabilityTheory] infixl:100 " ∘ₘ " => fun μ κ ↦ MeasureTheory.Measure.bind κ μ
 
-scoped[ProbabilityTheory] notation3 κ " ∘ₘ " μ:100 => MeasureTheory.Measure.bind μ κ
+scoped[ProbabilityTheory] notation3 κ " ∘ₘ " μ:100 => Measure.bind μ κ
 
 lemma Measure.map_comp (μ : Measure α) (κ : Kernel α β) {f : β → γ} (hf : Measurable f) :
     (κ ∘ₘ μ).map f = (κ.map f hf) ∘ₘ μ := by

diff --git a/TestingLowerBounds/Testing/Binary.lean b/TestingLowerBounds/Testing/Binary.lean
@@ -622,8 +622,7 @@ lemma bayesBinaryRisk_eq_lintegral_ennnorm (μ ν : Measure 𝒳) [IsFiniteMeasu
     toReal_bayesBinaryRisk_eq_integral_abs, ENNReal.ofReal_mul (inv_nonneg.mpr zero_le_two),
     ENNReal.ofReal_inv_of_pos zero_lt_two, ENNReal.ofReal_ofNat,
     ENNReal.ofReal_sub _ (by positivity), ENNReal.ofReal_toReal (measure_ne_top _ _),
-    MeasureTheory.ofReal_integral_eq_lintegral_ofReal _
-    (Filter.eventually_of_forall fun _ ↦ by positivity)]
+    ofReal_integral_eq_lintegral_ofReal _ (Filter.eventually_of_forall fun _ ↦ by positivity)]
   swap
   · refine ⟨Measurable.aestronglyMeasurable (by fun_prop), ?_⟩
     simp_rw [HasFiniteIntegral, Real.nnnorm_abs]