perf(MeasureTheory,Probability): expand slow measurabilty calls (#13770)

Manually expand slow `measurability` calls in various files: see individual commit messages for details.

From the benchmarking run, this seems to net -160*10⁹ instructions.
The `RadonNikodym` and `SignedMeasure` files each speed up by more than half (33 -> 18 billion resp. 100 -> 40 billion instructions). `Group/Convolution` is galvanised, 55 -> 8 billion instructions. The independence files become 10 billion instructions faster.

Author: grunweg

Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean

@@ -156,6 +156,7 @@ theorem integrable_rpow_neg_one_add_norm_sq {r : ℝ} (hnr : (finrank ℝ E : 
   refine ((integrable_one_add_norm hnr).const_mul <| (2 : ℝ) ^ (r / 2)).mono'
     ?_ (eventually_of_forall fun x => ?_)
   · -- Note: `measurability` proves this, but very slowly.
+    -- TODO(#13864): reinstate faster automation, e.g. by making `fun_prop` work here
     exact measurable_norm.pow_const 2 |>.const_add 1 |>.pow_const (-r / 2) |>.aestronglyMeasurable
   refine (abs_of_pos ?_).trans_le (rpow_neg_one_add_norm_sq_le x hr)
   positivity

Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean

@@ -428,7 +428,9 @@ theorem withDensityᵥ_rnDeriv_eq (s : SignedMeasure α) (μ : Measure α) [Sigm
       refine IntegrableOn.restrict ?_ MeasurableSet.univ
       refine ⟨?_, hasFiniteIntegral_toReal_of_lintegral_ne_top ?_⟩
       · apply Measurable.aestronglyMeasurable
-        measurability
+        -- NB. `measurability` proves this, but is quite slow
+        -- TODO(#13864): reinstate faster automation, e.g. by making `fun_prop` work here
+        apply (Measure.measurable_rnDeriv _ μ).ennreal_toNNReal.coe_nnreal_real
       · rw [set_lintegral_univ]
         exact (lintegral_rnDeriv_lt_top _ _).ne
   · exact equivMeasure.right_inv μ

Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean

@@ -189,13 +189,21 @@ variable {s t : SignedMeasure α}
 @[measurability]
 theorem measurable_rnDeriv (s : SignedMeasure α) (μ : Measure α) : Measurable (rnDeriv s μ) := by
   rw [rnDeriv_def]
-  measurability
+  -- Note. `measurabilty` proves this, but is very slow
+  apply Measurable.add
+  · exact ((Measure.measurable_rnDeriv _ μ).ennreal_toNNReal).coe_nnreal_real
+  · rw [measurable_neg_iff]
+    exact (Measure.measurable_rnDeriv _ μ).ennreal_toNNReal.coe_nnreal_real
+
 #align measure_theory.signed_measure.measurable_rn_deriv MeasureTheory.SignedMeasure.measurable_rnDeriv
 
 theorem integrable_rnDeriv (s : SignedMeasure α) (μ : Measure α) : Integrable (rnDeriv s μ) μ := by
   refine Integrable.sub ?_ ?_ <;>
     · constructor
-      · apply Measurable.aestronglyMeasurable; measurability
+      · -- NB: `measurability` proves this, but is very slow
+        -- TODO(#13864): reinstate faster automation, e.g. by making `fun_prop` work here
+        exact (((Measure.measurable_rnDeriv _ μ
+          ).ennreal_toNNReal).coe_nnreal_real).aestronglyMeasurable
       exact hasFiniteIntegral_toReal_of_lintegral_ne_top (lintegral_rnDeriv_lt_top _ μ).ne
 #align measure_theory.signed_measure.integrable_rn_deriv MeasureTheory.SignedMeasure.integrable_rnDeriv
 
@@ -306,10 +314,15 @@ private theorem eq_singularPart' (t : SignedMeasure α) {f : α → ℝ} (hf : M
   rw [singularPart, ← t.toSignedMeasure_toJordanDecomposition,
     JordanDecomposition.toSignedMeasure]
   congr
-  · have hfpos : Measurable fun x => ENNReal.ofReal (f x) := by measurability
+  -- NB: `measurability` proves this `have`, but is slow.
+  -- TODO(#13864): reinstate faster automation, e.g. by making `fun_prop` work here
+  · have hfpos : Measurable fun x => ENNReal.ofReal (f x) := hf.real_toNNReal.coe_nnreal_ennreal
     refine eq_singularPart hfpos htμ.1 ?_
     rw [toJordanDecomposition_eq_of_eq_add_withDensity hf hfi htμ' hadd]
-  · have hfneg : Measurable fun x => ENNReal.ofReal (-f x) := by measurability
+  · have hfneg : Measurable fun x => ENNReal.ofReal (-f x) :=
+      -- NB: `measurability` proves this, but is slow.
+      -- TODO(#13864): reinstate faster automation, e.g. by making `fun_prop` work here
+      (measurable_neg_iff.mpr hf).real_toNNReal.coe_nnreal_ennreal
     refine eq_singularPart hfneg htμ.2 ?_
     rw [toJordanDecomposition_eq_of_eq_add_withDensity hf hfi htμ' hadd]
 

Mathlib/MeasureTheory/Group/Convolution.lean

@@ -43,7 +43,10 @@ theorem dirac_one_mconv [MeasurableMul₂ M] (μ : Measure M) [SFinite μ] :
   unfold mconv
   rw [MeasureTheory.Measure.dirac_prod, map_map]
   · simp only [Function.comp_def, one_mul, map_id']
-  all_goals { measurability }
+  · -- NB. `measurability` proves this, but is slow
+    -- TODO(#13864): reinstate faster automation, e.g. by making `fun_prop` work here
+    exact Measurable.mul measurable_fst measurable_snd
+  measurability
 
 /-- Convolution of a measure μ with the dirac measure at 1 returns μ. -/
 @[to_additive (attr := simp)]
@@ -52,7 +55,14 @@ theorem mconv_dirac_one [MeasurableMul₂ M]
   unfold mconv
   rw [MeasureTheory.Measure.prod_dirac, map_map]
   · simp only [Function.comp_def, mul_one, map_id']
-  all_goals { measurability }
+  · -- NB. `measurability` proves this, but is slow
+    -- TODO(#13864): reinstate faster automation, e.g. by making `fun_prop` work here
+    exact Measurable.mul measurable_fst measurable_snd
+  -- NB. `measurability` proves this, but is slow
+  -- TODO(#13864): reinstate faster automation, e.g. by making `fun_prop` work here
+  apply Measurable.prod
+  · apply measurable_id'
+  · exact measurable_const
 
 /-- Convolution of the zero measure with a measure μ returns the zero measure. -/
 @[to_additive (attr := simp) conv_zero]
@@ -71,14 +81,18 @@ theorem mconv_add [MeasurableMul₂ M] (μ : Measure M) (ν : Measure M) (ρ : M
     [SFinite ν] [SFinite ρ] : μ ∗ (ν + ρ) = μ ∗ ν + μ ∗ ρ := by
   unfold mconv
   rw [prod_add, map_add]
-  measurability
+  -- NB. `measurability` proves this, but is pretty slow
+  -- TODO(#13864): reinstate faster automation, e.g. by making `fun_prop` work here
+  exact Measurable.mul measurable_fst measurable_snd
 
 @[to_additive add_conv]
 theorem add_mconv [MeasurableMul₂ M] (μ : Measure M) (ν : Measure M) (ρ : Measure M) [SFinite μ]
     [SFinite ν] [SFinite ρ] : (μ + ν) ∗ ρ = μ ∗ ρ + ν ∗ ρ := by
   unfold mconv
   rw [add_prod, map_add]
-  measurability
+  -- NB. `measurability` proves this, but is pretty slow
+  -- TODO(#13864): reinstate faster automation, e.g. by making `fun_prop` work here
+  exact Measurable.mul measurable_fst measurable_snd
 
 /-- To get commutativity, we need the underlying multiplication to be commutative. -/
 @[to_additive conv_comm]
@@ -87,7 +101,10 @@ theorem mconv_comm {M : Type*} [CommMonoid M] [MeasurableSpace M] [MeasurableMul
   unfold mconv
   rw [← prod_swap, map_map]
   · simp [Function.comp_def, mul_comm]
-  all_goals { measurability }
+  · -- NB. `measurability` proves this, but is pretty slow
+    -- TODO(#13864): reinstate faster automation, e.g. by making `fun_prop` work here
+    exact Measurable.mul measurable_fst measurable_snd
+  measurability
 
 /-- Convolution of SFinite maps is SFinite. -/
 @[to_additive sfinite_conv_of_sfinite]
@@ -107,7 +124,10 @@ instance probabilitymeasure_of_probabilitymeasures_mconv (μ : Measure M) (ν :
     [MeasurableMul₂ M] [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] :
     IsProbabilityMeasure (μ ∗ ν) := by
   apply MeasureTheory.isProbabilityMeasure_map
-  measurability
+  -- NB. `measurability` proves this, but is really slow
+  -- TODO(#13864): reinstate faster automation, e.g. by making `fun_prop` work here
+  exact AEMeasurable.mul (measurable_fst.comp_aemeasurable' aemeasurable_id')
+    (measurable_snd.comp_aemeasurable' aemeasurable_id')
 
 end Measure
 

Mathlib/Probability/Independence/Basic.lean

@@ -710,7 +710,13 @@ lemma iIndepFun.indepFun_prod_mk_prod_mk (h_indep : iIndepFun m f μ) (hf : ∀
   classical
   let g (i j : ι) (v : Π x : ({i, j} : Finset ι), β x) : β i × β j :=
     ⟨v ⟨i, mem_insert_self _ _⟩, v ⟨j, mem_insert_of_mem <| mem_singleton_self _⟩⟩
-  have hg (i j : ι) : Measurable (g i j) := by measurability
+  have hg (i j : ι) : Measurable (g i j) := by
+    -- NB: `measurability proves this, but is slow
+    -- TODO(#13864): reinstate faster automation, e.g. by making `fun_prop` work here
+    simp only [ne_eq, g]
+    apply Measurable.prod
+    · exact measurable_pi_apply _
+    · exact measurable_pi_apply _
   exact (h_indep.indepFun_finset {i, j} {k, l} (by aesop) hf).comp (hg i j) (hg k l)
 
 end iIndepFun

Mathlib/Probability/Independence/Conditional.lean

@@ -731,7 +731,13 @@ lemma iCondIndepFun.condIndepFun_prod_mk_prod_mk (h_indep : iCondIndepFun m' hm'
   classical
   let g (i j : ι) (v : Π x : ({i, j} : Finset ι), β x) : β i × β j :=
     ⟨v ⟨i, mem_insert_self _ _⟩, v ⟨j, mem_insert_of_mem <| mem_singleton_self _⟩⟩
-  have hg (i j : ι) : Measurable (g i j) := by measurability
+  have hg (i j : ι) : Measurable (g i j) := by
+    -- NB: `measurability proves this, but is slow
+    -- TODO(#13864): reinstate faster automation, e.g. by making `fun_prop` work here
+    simp only [ne_eq, g]
+    apply Measurable.prod
+    · exact measurable_pi_apply _
+    · exact measurable_pi_apply _
   exact (h_indep.indepFun_finset {i, j} {k, l} (by aesop) hf).comp (hg i j) (hg k l)
 
 end iCondIndepFun

Mathlib/Probability/Independence/Kernel.lean

@@ -963,7 +963,13 @@ lemma iIndepFun.indepFun_prod_mk_prod_mk [IsMarkovKernel κ] (hf_indep : iIndepF
   classical
   let g (i j : ι) (v : Π x : ({i, j} : Finset ι), β x) : β i × β j :=
     ⟨v ⟨i, mem_insert_self _ _⟩, v ⟨j, mem_insert_of_mem <| mem_singleton_self _⟩⟩
-  have hg (i j : ι) : Measurable (g i j) := by measurability
+  have hg (i j : ι) : Measurable (g i j) := by
+    -- NB: `measurability proves this, but is slow
+    -- TODO(#13864): reinstate faster automation, e.g. by making `fun_prop` work here
+    simp only [ne_eq, g]
+    apply Measurable.prod
+    · exact measurable_pi_apply _
+    · exact measurable_pi_apply _
   exact (hf_indep.indepFun_finset {i, j} {k, l} (by aesop) hf_meas).comp (hg i j) (hg k l)
 
 end iIndepFun