refactor: adopt Statlib's Bernoulli measure lemmas and Bernoulli kernel

LMLExplore/InformationTheory/KullbackLeibler/Bernoulli.lean

@@ -266,7 +266,7 @@ theorem klBer_eq_top_iff (hp : p ∈ Set.Icc 0 1) (hq : q ∈ Set.Icc 0 1) :
 /-- The binary relative entropy is finite when the second argument lies in `(0, 1)`. -/
 theorem klBer_ne_top (hq : q ∈ Set.Ioo 0 1) : klBer p q ≠ ∞ := by
   rw [klBer_def, Set.projIcc_of_mem _ (Set.Ioo_subset_Icc_self hq)]
-  exact klDiv_ne_top_iff.2 ⟨bernoulliMeasure_absolutelyContinuous
+  exact klDiv_ne_top_iff.2 ⟨bernoulliMeasure_absolutelyContinuous_of_imp
     (fun h ↦ absurd (congrArg Subtype.val h) hq.1.ne')
     (fun h ↦ absurd (congrArg Subtype.val h) hq.2.ne), integrable_bernoulliMeasure _ _ _ _⟩
 
@@ -395,7 +395,7 @@ theorem klBer_projIcc (p q : ℝ) :
 @[simp]
 theorem klBer_one_sub_one_sub (p q : ℝ) : klBer (1 - p) (1 - q) = klBer p q := by
   have h (r : I) : Ber((1 : ℝ), 0, σ r) = Ber((1 : ℝ), 0, r).map (1 - ·) := by
-    rw [map_bernoulliMeasure, bernoulliMeasure_symm]
+    rw [map_bernoulliMeasure, bernoulliMeasure_swap]
     simp
   rw [klBer_def, klBer_def, ← symm_projIcc, ← symm_projIcc, h, h]
   exact klDiv_map_measurableEmbedding _ _ (MeasurableEquiv.subLeft (1 : ℝ)).measurableEmbedding
@@ -753,15 +753,16 @@ theorem klBer_mul_add_mul_le {p' q' : ℝ} (hp : p ∈ Set.Icc 0 1) (hq : q ∈
     (hp' : p' ∈ Set.Icc 0 1) (hq' : q' ∈ Set.Icc 0 1) {a b : ℝ≥0} (hab : a + b = 1) :
     klBer (a * p + b * p') (a * q + b * q') ≤ a * klBer p q + b * klBer p' q' := by
   have hab' : (a : ℝ) + b = 1 := by exact_mod_cast hab
+  have hb : (b : ℝ) = 1 - a := by linarith
   have hmem {u v : ℝ} (hu : u ∈ Set.Icc (0 : ℝ) 1) (hv : v ∈ Set.Icc (0 : ℝ) 1) :
       (a : ℝ) * u + b * v ∈ Set.Icc (0 : ℝ) 1 := by
     simpa using convex_Icc (0 : ℝ) 1 hu hv a.2 b.2 hab'
   rw [klBer_of_mem_Icc hp hq, klBer_of_mem_Icc hp' hq',
     klBer_of_mem_Icc (hmem hp hp') (hmem hq hq'),
-    bernoulliMeasure_eq_smul_add_smul (r := ⟨_, hmem hp hp'⟩) (p := ⟨p, hp⟩) (q := ⟨p', hp'⟩)
-      hab rfl,
-    bernoulliMeasure_eq_smul_add_smul (r := ⟨_, hmem hq hq'⟩) (p := ⟨q, hq⟩) (q := ⟨q', hq'⟩)
-      hab rfl]
+    bernoulliMeasure_eq_smul_add_smul (c := ⟨_, hmem hp hp'⟩) (a := ⟨p, hp⟩) (b := ⟨p', hp'⟩)
+      (t := a) _ _ (hab ▸ le_self_add) (by simp [hb]),
+    bernoulliMeasure_eq_smul_add_smul (c := ⟨_, hmem hq hq'⟩) (a := ⟨q, hq⟩) (b := ⟨q', hq'⟩)
+      (t := a) _ _ (hab ▸ le_self_add) (by simp [hb]), tsub_eq_of_eq_add_rev hab.symm]
   exact klDiv_smul_add_smul_le _ _ _ _ a b
 
 /-- The binary relative entropy is jointly convex on `[0, 1] × [0, 1]`, as a function with values

LMLExplore/Probability/Distributions/Bernoulli.lean

@@ -6,19 +6,23 @@ Authors: LMLExplore contributors
 module
 
 public import Mathlib.Probability.Moments.SubGaussian
-public import Mathlib.Probability.Distributions.Bernoulli
 public import LMLExplore.Analysis.Convex.Integral
 public import LMLExplore.Topology.UnitInterval
-public import TauCeti.Probability.Distributions.Bernoulli.Measurability
+public import Statlib.ForMathlib.Probability.Distributions.Bernoulli
 
 /-!
-# Bernoulli laws: symmetry, absolute continuity, boundedness, sub-Gaussianity and mixtures
+# Bernoulli laws: absolute continuity, boundedness, sub-Gaussianity and mixtures
 
-Exchanging the two points of a Bernoulli law `Ber(x, y, p)` replaces `p` by `1 - p`, and for
-`x ≠ y`, `Ber(x, y, p) ≪ Ber(x, y, q)` exactly when `p` puts no mass on a point that `q` ignores.
-Being supported on two points, a Bernoulli law gives every real function exponential moments of all
-orders, and tilting it by `exp ∘ f` gives the Bernoulli law on the same two points whose odds are
-multiplied by `exp (f x - f y)`.
+This file complements Statlib's `Statlib.ForMathlib.Probability.Distributions.Bernoulli`, which
+provides the Lebesgue integral against a Bernoulli law `Ber(x, y, p)`, its symmetry
+`ProbabilityTheory.bernoulliMeasure_swap`, its mixtures
+`ProbabilityTheory.bernoulliMeasure_eq_smul_add_smul` and the Markov kernel
+`ProbabilityTheory.bernoulliKernel x y` from the unit interval.
+
+For `x ≠ y`, `Ber(x, y, p) ≪ Ber(x, y, q)` exactly when `p` puts no mass on a point that `q`
+ignores. Being supported on two points, a Bernoulli law gives every real function exponential
+moments of all orders, and tilting it by `exp ∘ f` gives the Bernoulli law on the same two points
+whose odds are multiplied by `exp (f x - f y)`.
 
 The real two-point law `Ber(x, y, p)` is supported on the interval between `x` and `y`, hence, by
 Hoeffding's lemma (`ProbabilityTheory.hasSubgaussianMGF_of_mem_Icc`), it is
@@ -35,16 +39,14 @@ means.
 ## Main definitions
 
 * `LMLExplore.bernoulliKernel`: the Markov kernel `x ↦ Ber(1, 0, x)` on `ℝ`, the parameter being
-  clamped to `[0, 1]`.
+  clamped to `[0, 1]`; it is `ProbabilityTheory.bernoulliKernel 1 0` precomposed with the clamp.
 
 ## Main statements
 
-* `ProbabilityTheory.bernoulliMeasure_symm`: `Ber(x, y, 1 - p) = Ber(y, x, p)`.
-* `ProbabilityTheory.bernoulliMeasure_eq_smul_add_smul`: for `a + b = 1`,
-  `Ber(x, y, a p + b q) = a Ber(x, y, p) + b Ber(x, y, q)`.
+* `ProbabilityTheory.bernoulliMeasure_absolutelyContinuous_of_imp`: if `q = 0 → p = 0` and
+  `q = 1 → p = 1`, then `Ber(x, y, p) ≪ Ber(x, y, q)`.
 * `ProbabilityTheory.bernoulliMeasure_absolutelyContinuous_iff`: for `x ≠ y`,
   `Ber(x, y, p) ≪ Ber(x, y, q)` if and only if `q = 0 → p = 0` and `q = 1 → p = 1`.
-* `ProbabilityTheory.lintegral_bernoulliMeasure`: `∫⁻ f ∂Ber(x, y, p) = p f(x) + (1 - p) f(y)`.
 * `ProbabilityTheory.integrableExpSet_bernoulliMeasure`: every real function has exponential
   moments of all orders under `Ber(x, y, p)`.
 * `ProbabilityTheory.tilted_bernoulliMeasure`: tilting `Ber(x, y, p)` by `exp ∘ f` gives
@@ -68,33 +70,11 @@ namespace ProbabilityTheory
 
 variable {X : Type*} [MeasurableSpace X] {x y : X} {p q : I}
 
-/-- Exchanging the two points of a Bernoulli law replaces its parameter `p` by `1 - p`. -/
-theorem bernoulliMeasure_symm (x y : X) (p : I) : Ber(x, y, σ p) = Ber(y, x, p) := by
-  rw [bernoulliMeasure_def, bernoulliMeasure_def, unitInterval.symm_symm, add_comm]
-
-/-- A mixture of two Bernoulli laws on the same two points is the Bernoulli law whose parameter is
-the same mixture of their parameters: if `r = a p + b q` with `a + b = 1`, then
-`Ber(x, y, r) = a Ber(x, y, p) + b Ber(x, y, q)`. -/
-theorem bernoulliMeasure_eq_smul_add_smul {r : I} {a b : ℝ≥0} (hab : a + b = 1)
-    (hr : (r : ℝ) = a * p + b * q) :
-    Ber(x, y, r) = (a : ℝ≥0∞) • Ber(x, y, p) + (b : ℝ≥0∞) • Ber(x, y, q) := by
-  have hab' : (a : ℝ) + b = 1 := by exact_mod_cast hab
-  have h₁ : unitInterval.toNNReal r =
-      a * unitInterval.toNNReal p + b * unitInterval.toNNReal q := by
-    ext
-    simp [hr]
-  have h₂ : unitInterval.toNNReal (σ r) =
-      a * unitInterval.toNNReal (σ p) + b * unitInterval.toNNReal (σ q) := by
-    ext
-    simp only [unitInterval.coe_toNNReal, unitInterval.coe_symm_eq, NNReal.coe_add,
-      NNReal.coe_mul, hr]
-    linear_combination -hab'
-  simp only [bernoulliMeasure_def, ← ENNReal.smul_def, h₁, h₂, smul_add, smul_smul, add_smul]
-  abel
-
 /-- A Bernoulli law is absolutely continuous with respect to the Bernoulli law on the same two
-points with parameter `q` whenever it puts no mass on a point that the second law ignores. -/
-theorem bernoulliMeasure_absolutelyContinuous (h0 : q = 0 → p = 0) (h1 : q = 1 → p = 1) :
+points with parameter `q` whenever it puts no mass on a point that the second law ignores. Unlike
+`ProbabilityTheory.bernoulliMeasure_absolutelyContinuous`, this needs neither `x ≠ y` nor
+`q ∉ {0, 1}`. -/
+theorem bernoulliMeasure_absolutelyContinuous_of_imp (h0 : q = 0 → p = 0) (h1 : q = 1 → p = 1) :
     Ber(x, y, p) ≪ Ber(x, y, q) := by
   classical
   refine Measure.AbsolutelyContinuous.mk fun s hs hνs ↦ ?_
@@ -114,15 +94,10 @@ and `p = 1` when `q = 1`. -/
 theorem bernoulliMeasure_absolutelyContinuous_iff [MeasurableSingletonClass X] (hxy : x ≠ y) :
     Ber(x, y, p) ≪ Ber(x, y, q) ↔ (q = 0 → p = 0) ∧ (q = 1 → p = 1) := by
   refine ⟨fun h ↦ ⟨fun hq ↦ ?_, fun hq ↦ ?_⟩,
-    fun h ↦ bernoulliMeasure_absolutelyContinuous h.1 h.2⟩
+    fun h ↦ bernoulliMeasure_absolutelyContinuous_of_imp h.1 h.2⟩
   · simpa [hxy.symm] using h (s := {x}) (by simp [hq, hxy.symm])
   · simpa [hxy, unitInterval.symm_eq_zero] using h (s := {y}) (by simp [hq, hxy])
 
-/-- The lower Lebesgue integral of `f` against `Ber(x, y, p)` is `p f(x) + (1 - p) f(y)`. -/
-lemma lintegral_bernoulliMeasure [MeasurableSingletonClass X] (x y : X) (p : I) (f : X → ℝ≥0∞) :
-    ∫⁻ z, f z ∂Ber(x, y, p) = ENNReal.ofReal p * f x + ENNReal.ofReal (1 - p) * f y := by
-  simp [bernoulliMeasure_def, ENNReal.smul_def, ENNReal.coe_nnreal_eq]
-
 /-- Every real function has exponential moments of all orders under a Bernoulli law. -/
 @[simp]
 lemma integrableExpSet_bernoulliMeasure [MeasurableSingletonClass X] (x y : X) (p : I)
@@ -175,54 +150,38 @@ lemma hasSubgaussianMGF_bernoulliMeasure (x y : ℝ) (p : I) :
     simp [max_sub_min_eq_abs']
   simpa only [id_eq, integral_bernoulliMeasure, smul_eq_mul, hc] using h
 
-/-- The Markov kernel `x ↦ Ber(1, 0, x)` on `ℝ`, sending `x` to the Bernoulli law of mean `x`. The
-parameter is clamped to `[0, 1]` by `Set.projIcc`, so that the kernel is defined on all of `ℝ`. -/
-noncomputable def bernoulliKernel : Kernel ℝ ℝ where
-  toFun x := Ber((1 : ℝ), 0, Set.projIcc 0 1 zero_le_one x)
-  measurable' :=
-    measurable_const.bernoulliMeasure measurable_const continuous_projIcc.measurable
+/-- The Markov kernel `x ↦ Ber(1, 0, x)` on `ℝ`, sending `x` to the Bernoulli law of mean `x`. It is
+the kernel `ProbabilityTheory.bernoulliKernel 1 0` on the unit interval, precomposed with the clamp
+`Set.projIcc 0 1`, so that it is defined on all of `ℝ`. -/
+noncomputable def bernoulliKernel : Kernel ℝ ℝ :=
+  (ProbabilityTheory.bernoulliKernel (1 : ℝ) 0).comap (Set.projIcc 0 1 zero_le_one)
+    continuous_projIcc.measurable
 
 @[simp]
 lemma bernoulliKernel_apply (x : ℝ) :
-    bernoulliKernel x = Ber((1 : ℝ), 0, Set.projIcc 0 1 zero_le_one x) :=
-  (rfl)
+    bernoulliKernel x = Ber((1 : ℝ), 0, Set.projIcc 0 1 zero_le_one x) := by
+  rw [bernoulliKernel, Kernel.comap_apply, ProbabilityTheory.bernoulliKernel_apply]
 
 instance : IsMarkovKernel bernoulliKernel :=
   ⟨fun x ↦ by rw [bernoulliKernel_apply]; infer_instance⟩
 
 /-- For a probability measure `ρ` on `ℝ` supported on `[0, 1]`, the mixture
 `bernoulliKernel ∘ₘ ρ` of the Bernoulli laws `Ber(1, 0, x)` over `x ∼ ρ` is the Bernoulli law of
-mean `∫ x ∂ρ`. -/
+mean `∫ x ∂ρ`. This is `ProbabilityTheory.bernoulliKernel_comp_eq_bernoulliMeasure` for the image
+of `ρ` under the clamp `Set.projIcc 0 1`. -/
 theorem bernoulliKernel_comp {ρ : Measure ℝ} [IsProbabilityMeasure ρ]
     (hρ : ∀ᵐ x ∂ρ, x ∈ Set.Icc 0 1) :
     bernoulliKernel ∘ₘ ρ = Ber((1 : ℝ), 0, Set.projIcc 0 1 zero_le_one ρ[id]) := by
-  set p : ℝ → I := Set.projIcc 0 1 zero_le_one
-  have hp : Measurable p := continuous_projIcc.measurable
-  have hpi : Integrable (fun x ↦ (p x : ℝ)) ρ :=
-    Integrable.of_mem_Icc 0 1 (by fun_prop) (.of_forall fun x ↦ (p x).2)
-  have hint : ∫ x, (p x : ℝ) ∂ρ = ρ[id] := by
+  have hp : Measurable (Set.projIcc (0 : ℝ) 1 zero_le_one) := continuous_projIcc.measurable
+  have hmem : ρ[id] ∈ Set.Icc (0 : ℝ) 1 := integral_id_mem_Icc_of_ae_mem_Icc hρ
+  -- The clamp fixes `ρ`-almost every point, so the image of `ρ` under it has mean `ρ[id]`.
+  have hmean : ((Set.projIcc 0 1 zero_le_one ρ[id] : I) : ℝ) =
+      ∫ q, (q : ℝ) ∂ρ.map (Set.projIcc 0 1 zero_le_one) := by
+    rw [Set.projIcc_of_mem _ hmem, integral_map hp.aemeasurable (by fun_prop)]
     refine integral_congr_ae ?_
     filter_upwards [hρ] with x hx
-    simp [p, Set.projIcc_of_mem _ hx]
-  have hmem : ρ[id] ∈ Set.Icc (0 : ℝ) 1 := integral_id_mem_Icc_of_ae_mem_Icc hρ
-  have hpm : p ρ[id] = ⟨ρ[id], hmem⟩ := Set.projIcc_of_mem _ hmem
-  -- The masses that the mixture puts on `1` and on `0` are the means of `x` and of `1 - x`.
-  have h₁ : ∫⁻ x, (unitInterval.toNNReal (p x) : ℝ≥0∞) ∂ρ =
-      unitInterval.toNNReal (p ρ[id]) := by
-    simp_rw [← ENNReal.ofReal_coe_nnreal, unitInterval.coe_toNNReal]
-    rw [← ofReal_integral_eq_lintegral_ofReal hpi (.of_forall fun x ↦ (p x).2.1), hint, hpm]
-  have h₂ : ∫⁻ x, (unitInterval.toNNReal (σ (p x)) : ℝ≥0∞) ∂ρ =
-      unitInterval.toNNReal (σ (p ρ[id])) := by
-    simp_rw [← ENNReal.ofReal_coe_nnreal, unitInterval.coe_toNNReal, unitInterval.coe_symm_eq]
-    rw [← ofReal_integral_eq_lintegral_ofReal (Integrable.of_mem_Icc 0 1 (by fun_prop)
-      (.of_forall fun x ↦ ⟨by simp [(p x).2.2], by simp [(p x).2.1]⟩))
-      (.of_forall fun x ↦ by simp [(p x).2.2]), integral_sub (integrable_const 1) hpi, hint, hpm]
-    simp
-  ext s hs
-  rw [Measure.bind_apply hs bernoulliKernel.aemeasurable]
-  simp only [bernoulliKernel_apply, bernoulliMeasure_def, add_apply, smul_apply, ENNReal.smul_def,
-    smul_eq_mul]
-  rw [lintegral_add_left (by fun_prop), lintegral_mul_const _ (by fun_prop),
-    lintegral_mul_const _ (by fun_prop), h₁, h₂]
+    simp [Set.projIcc_of_mem _ hx]
+  rw [bernoulliKernel, ← Kernel.comp_deterministic_eq_comap, ← Measure.comp_assoc,
+    Measure.deterministic_comp_eq_map, bernoulliKernel_comp_eq_bernoulliMeasure _ _ _ hmean]
 
 end LMLExplore