Less rules

Author: gaetanserre

RandomDo/ForMathlib/Probability/Distributions/Bernoulli.lean

@@ -22,17 +22,11 @@ namespace ProbabilityTheory
 
 variable {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y]
 
-lemma bernoulliMeasure_bind (x y : X) (p : I) {g : X → Measure Y} (hg : Measurable g) :
-    Ber(x, y, p).bind g = (toNNReal p : ℝ≥0∞) • g x + (toNNReal (σ p) : ℝ≥0∞) • g y := by
-  rw [bernoulliMeasure_def, bind_add hg.aemeasurable, bind_smul, bind_smul, dirac_bind hg,
-    dirac_bind hg]
-  rfl
-
 /-- Binding a Bernoulli distribution on a space whose points are measurable: the continuation needs
 no measurability, and the two weights are real numbers, so that `simp` can use it and `norm_num`
 can compute with the result. -/
 @[simp]
-lemma bernoulliMeasure_bind' [MeasurableSingletonClass X] (x y : X) (p : I) (g : X → Measure Y) :
+lemma bernoulliMeasure_bind [MeasurableSingletonClass X] (x y : X) (p : I) (g : X → Measure Y) :
     Ber(x, y, p).bind g = ENNReal.ofReal p • g x + ENNReal.ofReal (1 - p) • g y := by
   have h (q : I) : ((toNNReal q : NNReal) : ℝ≥0∞) = ENNReal.ofReal q := by
     rw [ENNReal.ofReal, Real.toNNReal_of_nonneg q.2.1]

RandomDo/Monad/While.lean

@@ -8,7 +8,6 @@ module
 public import RandomDo.Monad.Instances
 public import RandomDo.Tactic.IsMarkov.Defs
 import RandomDo.Monad.Notation
-public import Mathlib.Probability.Distributions.Bernoulli
 
 /-!
 # `while` loops
@@ -151,7 +150,8 @@ private lemma loopRun_succ (f : σ → Measure (ForInStep σ)) (n : ℕ) (b : σ
     loopRun f (n + 1) b = (f b).bind fun t ↦
       ForInStep.casesOn (motive := fun _ ↦ Measure σ) t (fun _ ↦ 0) (loopRun f n) := rfl
 
-private lemma measurable_casesOn {γ : Type*} [MeasurableSpace γ] {d y : σ → γ}
+/-- A case analysis on the outcome of a step is measurable as soon as its two branches are. -/
+lemma measurable_casesOn {γ : Type*} [MeasurableSpace γ] {d y : σ → γ}
     (hd : Measurable d) (hy : Measurable y) :
     Measurable fun t : ForInStep σ ↦ ForInStep.casesOn (motive := fun _ ↦ γ) t d y :=
   fun _ hs ↦ ⟨hy hs, hd hs⟩

RandomDo/Tactic/IsMarkov/ForInStep.lean

@@ -22,8 +22,7 @@ largest one making both `ForInStep.yield` and `ForInStep.done` measurable.
 ## Main results
 * `measurable_yield`, `measurable_run`, `measurable_isDone`: the maps relating `ForInStep β` to `β`
   and to `Bool` are measurable.
-* The points of `ForInStep β` are measurable as soon as those of `β` are, and `ForInStep.yield` is a
-  measurable embedding.
+* The points of `ForInStep β` are measurable as soon as those of `β` are.
 * `measurable_CasesOn`: a case analysis on a `ForInStep`, measurable in each of its two branches, is
   measurable.
 * `IsMarkov.forInStepCasesOn`: the same statement for the Markov property.
@@ -65,17 +64,6 @@ instance [MeasurableSingletonClass β] : MeasurableSingletonClass (ForInStep β)
     -- A singleton's preimages under `yield` and `done` are a singleton and the empty set.
     constructor <;> cases t <;> change MeasurableSet (_ ⁻¹' _) <;> simp [Set.preimage]
 
-lemma measurableEmbedding_yield : MeasurableEmbedding (ForInStep.yield : β → ForInStep β) where
-  injective _ _ h := ForInStep.yield.inj h
-  measurable := measurable_yield
-  measurableSet_image' S hS := by
-    refine ⟨?_, ?_⟩
-    · change MeasurableSet (ForInStep.yield ⁻¹' _)
-      rwa [Set.preimage_image_eq _ fun _ _ h ↦ ForInStep.yield.inj h]
-    · change MeasurableSet (ForInStep.done ⁻¹' _)
-      convert MeasurableSet.empty (α := β)
-      ext; simp
-
 instance [Countable β] : Countable (ForInStep β) :=
   Function.Injective.countable (f := fun t : ForInStep β ↦ (t.isDone, t.run)) <| by
     rintro (_ | _) (_ | _) h <;> simp_all