Bump mathlib

PFR.lean

@@ -6,6 +6,7 @@ import PFR.Fibring
 import PFR.FirstEstimate
 import PFR.ForMathlib.AffineSpaceDim
 import PFR.ForMathlib.CompactProb
+import PFR.ForMathlib.ConditionalIndependence
 import PFR.ForMathlib.Entropy.Basic
 import PFR.ForMathlib.Entropy.Group
 import PFR.ForMathlib.Entropy.Kernel.Basic
@@ -17,12 +18,12 @@ import PFR.ForMathlib.Entropy.RuzsaDist
 import PFR.ForMathlib.Entropy.RuzsaSetDist
 import PFR.ForMathlib.FiniteMeasureComponent
 import PFR.ForMathlib.FiniteMeasureProd
-import PFR.ForMathlib.FiniteRange
+import PFR.ForMathlib.FiniteRange.ConditionalProbability
+import PFR.ForMathlib.FiniteRange.Defs
 import PFR.ForMathlib.GroupQuot
 import PFR.ForMathlib.MeasureReal
 import PFR.ForMathlib.Pair
 import PFR.ForMathlib.ProbabilityMeasureProdCont
-import PFR.ForMathlib.SubmoduleQuotMeasurableSpace
 import PFR.ForMathlib.Uniform
 import PFR.ForMathlib.ZModModule
 import PFR.HomPFR
@@ -35,7 +36,6 @@ import PFR.Mathlib.Algebra.Module.Submodule.Ker
 import PFR.Mathlib.Algebra.Module.Submodule.Map
 import PFR.Mathlib.Algebra.Module.Submodule.Range
 import PFR.Mathlib.Analysis.SpecialFunctions.NegMulLog
-import PFR.Mathlib.Data.Finsupp.Fintype
 import PFR.Mathlib.Data.Set.Pointwise.Finite
 import PFR.Mathlib.Data.Set.Pointwise.SMul
 import PFR.Mathlib.Data.ZMod.Basic
@@ -46,14 +46,11 @@ import PFR.Mathlib.MeasureTheory.Constructions.Prod.Basic
 import PFR.Mathlib.MeasureTheory.Integral.Bochner
 import PFR.Mathlib.MeasureTheory.Integral.Lebesgue
 import PFR.Mathlib.MeasureTheory.Integral.SetIntegral
-import PFR.Mathlib.MeasureTheory.MeasurableSpace.Basic
 import PFR.Mathlib.MeasureTheory.Measure.NullMeasurable
 import PFR.Mathlib.MeasureTheory.Measure.ProbabilityMeasure
-import PFR.Mathlib.MeasureTheory.Measure.Typeclasses
 import PFR.Mathlib.Probability.ConditionalProbability
 import PFR.Mathlib.Probability.IdentDistrib
 import PFR.Mathlib.Probability.Independence.Basic
-import PFR.Mathlib.Probability.Independence.Conditional
 import PFR.Mathlib.Probability.Independence.FourVariables
 import PFR.Mathlib.Probability.Independence.Kernel
 import PFR.Mathlib.Probability.Kernel.Composition

PFR/Mathlib/Probability/Independence/Conditional.lean → PFR/ForMathlib/ConditionalIndependence.lean

@@ -1,7 +1,8 @@
-import PFR.ForMathlib.Pair
+import PFR.Mathlib.Probability.ConditionalProbability
 import PFR.Mathlib.Probability.IdentDistrib
+import PFR.ForMathlib.FiniteRange.ConditionalProbability
+import PFR.ForMathlib.Pair
 import PFR.Tactic.Finiteness
-import PFR.Mathlib.Probability.ConditionalProbability
 
 open MeasureTheory Measure Set
 open scoped ENNReal

PFR/ForMathlib/Entropy/Basic.lean

@@ -1,7 +1,6 @@
+import PFR.ForMathlib.ConditionalIndependence
 import PFR.ForMathlib.Entropy.Kernel.MutualInfo
-import PFR.ForMathlib.Entropy.Kernel.Basic
 import PFR.ForMathlib.Uniform
-import PFR.Mathlib.Probability.Independence.Conditional
 
 /-!
 # Entropy and conditional entropy
@@ -218,7 +217,7 @@ lemma entropy_eq_log_card {X : Ω → S} [Fintype S] [MeasurableSingletonClass S
 lemma prob_ge_exp_neg_entropy [MeasurableSingletonClass S] (X : Ω → S) (μ : Measure Ω)
     [IsProbabilityMeasure μ] (hX : Measurable X) [hX': FiniteRange X] :
     ∃ s : S, μ.map X {s} ≥ (μ Set.univ) * (rexp (- H[X ; μ])).toNNReal := by
-  have : Nonempty Ω := nonempty_of_isProbabilityMeasure μ
+  have : Nonempty Ω := μ.nonempty_of_neZero
   have : Nonempty S := Nonempty.map X (by infer_instance)
   let μS := μ.map X
   let μs s := μS {s}
@@ -551,7 +550,7 @@ lemma chain_rule' (μ : Measure Ω) [IsZeroOrProbabilityMeasure μ]
     H[⟨X, Y⟩ ; μ] = H[X ; μ] + H[Y | X ; μ] := by
   rcases eq_zero_or_isProbabilityMeasure μ with rfl | hμ
   · simp
-  have : Nonempty T := Nonempty.map Y (nonempty_of_isProbabilityMeasure μ)
+  have : Nonempty T := Nonempty.map Y (μ.nonempty_of_neZero)
   rw [entropy_eq_kernel_entropy, Kernel.chain_rule]
   simp_rw [← Kernel.map_const _ (hX.prod_mk hY), Kernel.fst_map_prod _ hY, Kernel.map_const _ hX,
     Kernel.map_const _ (hX.prod_mk hY)]
@@ -623,8 +622,8 @@ lemma cond_chain_rule' (μ : Measure Ω) [IsZeroOrProbabilityMeasure μ]
     H[⟨X, Y⟩ | Z ; μ] = H[X | Z ; μ] + H[Y | ⟨X, Z⟩ ; μ] := by
   rcases eq_zero_or_isProbabilityMeasure μ with rfl | hμ
   · simp
-  have : Nonempty S := Nonempty.map X (nonempty_of_isProbabilityMeasure μ)
-  have : Nonempty T := Nonempty.map Y (nonempty_of_isProbabilityMeasure μ)
+  have : Nonempty S := Nonempty.map X (μ.nonempty_of_neZero)
+  have : Nonempty T := Nonempty.map Y (μ.nonempty_of_neZero)
   rw [condEntropy_eq_kernel_entropy (hX.prod_mk hY) hZ, Kernel.chain_rule]
   · congr 1
     · rw [condEntropy_eq_kernel_entropy hX hZ]
@@ -905,8 +904,8 @@ lemma condMutualInfo_eq [Countable U]
     I[X : Y | Z ; μ] = H[X | Z ; μ] + H[Y | Z; μ] - H[⟨X, Y⟩ | Z ; μ] := by
   rcases eq_zero_or_isProbabilityMeasure μ with rfl | hμ
   · simp
-  have : Nonempty S := Nonempty.map X (nonempty_of_isProbabilityMeasure μ)
-  have : Nonempty T := Nonempty.map Y (nonempty_of_isProbabilityMeasure μ)
+  have : Nonempty S := Nonempty.map X (μ.nonempty_of_neZero)
+  have : Nonempty T := Nonempty.map Y (μ.nonempty_of_neZero)
   rw [condMutualInfo_eq_kernel_mutualInfo hX hY hZ, Kernel.mutualInfo,
     Kernel.entropy_congr (condDistrib_fst_ae_eq hX hY hZ _),
     Kernel.entropy_congr (condDistrib_snd_ae_eq hX hY hZ _),
@@ -1025,8 +1024,8 @@ lemma entropy_submodular (hX : Measurable X) (hY : Measurable Y) (hZ : Measurabl
     H[X | ⟨Y, Z⟩ ; μ] ≤ H[X | Z ; μ] := by
   rcases eq_zero_or_isProbabilityMeasure μ with rfl | hμ
   · simp
-  have : Nonempty S := Nonempty.map X (nonempty_of_isProbabilityMeasure μ)
-  have : Nonempty T := Nonempty.map Y (nonempty_of_isProbabilityMeasure μ)
+  have : Nonempty S := Nonempty.map X (μ.nonempty_of_neZero)
+  have : Nonempty T := Nonempty.map Y (μ.nonempty_of_neZero)
   rw [condEntropy_eq_kernel_entropy hX hZ, condEntropy_two_eq_kernel_entropy hX hY hZ]
   refine (Kernel.entropy_condKernel_le_entropy_snd ?_).trans_eq ?_
   · apply Kernel.aefiniteKernelSupport_condDistrib

PFR/ForMathlib/Entropy/Kernel/Basic.lean

@@ -230,8 +230,8 @@ lemma entropy_compProd_aux [MeasurableSingletonClass S] [MeasurableSingletonClas
   intro t ht
   rw [← mul_add]
   congr
-  rcases (local_support_of_finiteKernelSupport hκ A) with ⟨B, hB⟩
-  rcases (local_support_of_finiteKernelSupport hη (A ×ˢ B)) with ⟨C, hC⟩
+  obtain ⟨B, hB⟩ := local_support_of_finiteKernelSupport hκ A
+  obtain ⟨C, hC⟩ := local_support_of_finiteKernelSupport hη (A ×ˢ B)
   rw [integral_eq_setIntegral (hB t ht)]
   have hκη : ((κ ⊗ₖ η) t) (B ×ˢ C : Finset (S × U))ᶜ = 0 := by
     rw [ProbabilityTheory.Kernel.compProd_apply, lintegral_eq_setLIntegral (hB t ht),
@@ -252,16 +252,12 @@ lemma entropy_compProd_aux [MeasurableSingletonClass S] [MeasurableSingletonClas
   intro s hs
   simp
   have hts : (t, s) ∈ A ×ˢ B := by simp [ht, hs]
-  have hη': (comap η (Prod.mk t) measurable_prod_mk_left) s Cᶜ = 0 := by
-    rw [Kernel.comap_apply]
-    exact hC (t, s) hts
-  rw [measureEntropy_def_finite' hη']
+  rw [measureEntropy_def_finite' (hC (t, s) hts)]
   simp
   have : negMulLog ((κ t).real {s}) = ∑ u in C, negMulLog ((κ t).real {s}) *
       ((comap η (Prod.mk t) measurable_prod_mk_left) s).real {u} := by
     rw [← Finset.mul_sum]
     simp
-    rw [Kernel.comap_apply]
     suffices (η (t, s)).real ↑C = (η (t, s)).real Set.univ by simp [this]
     have := hC (t, s) hts
     rw [← measureReal_eq_zero_iff] at this
@@ -325,18 +321,14 @@ lemma entropy_compProd_deterministic [Countable S] [MeasurableSingletonClass S]
     Hk[κ ⊗ₖ (deterministic f .of_discrete), μ] = Hk[κ, μ] := by
   simp [entropy_compProd hκ ((FiniteKernelSupport.deterministic f).aefiniteKernelSupport _)]
 
-lemma nonempty_of_isMarkovKernel
-    {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] (κ : Kernel α β) [IsMarkovKernel κ]
-    [Nonempty α] : Nonempty β := by
-  inhabit α
-  let ν : Measure β := κ default
-  have : IsProbabilityMeasure ν := IsMarkovKernel.isProbabilityMeasure default
-  exact nonempty_of_isProbabilityMeasure ν
+lemma nonempty_of_isMarkovKernel {α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
+    (κ : Kernel α β) [IsMarkovKernel κ] [Nonempty α] : Nonempty β :=
+  (κ <| Classical.arbitrary _).nonempty_of_neZero
 
 lemma nonempty_of_isProbabilityMeasure_of_isMarkovKernel
     {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] (μ : Measure α) [IsProbabilityMeasure μ]
     (κ : Kernel α β) [IsMarkovKernel κ] : Nonempty β := by
-  have : Nonempty α := nonempty_of_isProbabilityMeasure μ
+  have : Nonempty α := μ.nonempty_of_neZero
   exact nonempty_of_isMarkovKernel κ
 
 lemma chain_rule [Countable S] [MeasurableSingletonClass S] [Countable T]

PFR/ForMathlib/Entropy/Kernel/MutualInfo.lean

@@ -287,7 +287,7 @@ lemma entropy_submodular_compProd {ξ : Kernel T S} [IsZeroOrMarkovKernel ξ]
   rcases eq_zero_or_isMarkovKernel ξ with rfl | hξ'
   · simp
   have : Nonempty S := nonempty_of_isProbabilityMeasure_of_isMarkovKernel μ ξ
-  have : Nonempty T := nonempty_of_isProbabilityMeasure μ
+  have : Nonempty T := μ.nonempty_of_neZero
   rcases eq_zero_or_isMarkovKernel κ with rfl | hκ'
   · simp
   have : Nonempty U := nonempty_of_isMarkovKernel κ
@@ -325,7 +325,7 @@ lemma entropy_compProd_triple_add_entropy_le {ξ : Kernel T S} [IsZeroOrMarkovKe
   rcases eq_zero_or_isMarkovKernel ξ with rfl | hξ'
   · simp
   have : Nonempty S := nonempty_of_isProbabilityMeasure_of_isMarkovKernel μ ξ
-  have : Nonempty T := nonempty_of_isProbabilityMeasure μ
+  have : Nonempty T := μ.nonempty_of_neZero
   have : Nonempty U := nonempty_of_isMarkovKernel κ
   have : Nonempty V := nonempty_of_isMarkovKernel η
   rw [chain_rule,

PFR/ForMathlib/Entropy/Measure.lean

@@ -1,7 +1,7 @@
 import Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
 import Mathlib.MeasureTheory.Integral.Bochner
 import Mathlib.Tactic.Positivity.Finset
-import PFR.ForMathlib.FiniteRange
+import PFR.ForMathlib.FiniteRange.Defs
 import PFR.ForMathlib.MeasureReal
 import PFR.Mathlib.MeasureTheory.Constructions.Prod.Basic
 import PFR.Tactic.Finiteness

PFR/ForMathlib/FiniteRange/ConditionalProbability.lean

@@ -0,0 +1,26 @@
+import Mathlib.Probability.ConditionalProbability
+import PFR.ForMathlib.FiniteRange.Defs
+
+open MeasureTheory Set
+
+namespace ProbabilityTheory
+variable {Ω α : Type*} {m : MeasurableSpace Ω} (μ : Measure Ω)
+ [MeasurableSpace α] [MeasurableSingletonClass α]
+
+-- TODO: Replace `sum_meas_smul_cond_fiber` once `FiniteRange` is in Mathlib.
+/-- The **law of total probability** for a random variable taking finitely many values: a measure
+`μ` can be expressed as a linear combination of its conditional measures `μ[|X ← x]` on fibers of a
+random variable `X` valued in a fintype. -/
+lemma sum_meas_smul_cond_fiber' {X : Ω → α} (hX : Measurable X) [finX : FiniteRange X]
+    (μ : Measure Ω) [IsFiniteMeasure μ] :
+    ∑ x ∈ finX.toFinset, μ (X ⁻¹' {x}) • μ[|X ← x] = μ := by
+  ext E hE
+  calc
+    _ = ∑ x ∈ finX.toFinset, μ (X ⁻¹' {x} ∩ E) := by
+      simp only [Measure.coe_finset_sum, Measure.coe_smul, Finset.sum_apply,
+        Pi.smul_apply, smul_eq_mul]
+      simp_rw [mul_comm (μ _), cond_mul_eq_inter _ (hX (.singleton _))]
+    _ = _ := by
+      have : ⋃ x ∈ finX.toFinset, X ⁻¹' {x} ∩ E = E := by ext _; simp
+      rw [← measure_biUnion_finset _ fun _ _ ↦ (hX (.singleton _)).inter hE, this]
+      aesop (add simp [PairwiseDisjoint, Set.Pairwise, Function.onFun, disjoint_left])

PFR/ForMathlib/GroupQuot.lean

@@ -1,6 +1,5 @@
 import Mathlib.LinearAlgebra.Dimension.Free
 import PFR.ForMathlib.ZModModule
-import PFR.Mathlib.Data.Finsupp.Fintype
 import PFR.Mathlib.RingTheory.Finiteness
 
 /-!

PFR/ForMathlib/Uniform.lean

@@ -1,7 +1,7 @@
 import Mathlib.Probability.IdentDistrib
 import Mathlib.Probability.ConditionalProbability
 import PFR.ForMathlib.MeasureReal
-import PFR.ForMathlib.FiniteRange
+import PFR.ForMathlib.FiniteRange.Defs
 
 open Function MeasureTheory Set
 open scoped ENNReal

PFR/Kullback.lean

@@ -1,4 +1,4 @@
-import PFR.ForMathlib.FiniteRange
+import PFR.ForMathlib.FiniteRange.Defs
 import Mathlib.Probability.IdentDistrib
 import PFR.ForMathlib.Entropy.Basic
 

PFR/Mathlib/Analysis/SpecialFunctions/NegMulLog.lean

@@ -19,31 +19,6 @@ open scoped ENNReal NNReal Topology
 namespace Real
 variable {ι : Type*} {s : Finset ι} {w : ι → ℝ} {p : ι → ℝ}
 
-/-- Jensen's inequality for the entropy function. -/
-lemma sum_negMulLog_le (h₀ : ∀ i ∈ s, 0 ≤ w i) (h₁ : ∑ i in s, w i = 1) (hmem : ∀ i ∈ s, 0 ≤ p i) :
-    ∑ i in s, w i * negMulLog (p i) ≤ negMulLog (∑ i in s, w i * p i) :=
-  concaveOn_negMulLog.le_map_sum h₀ h₁ hmem
-
-/-- The strict Jensen inequality for the entropy function. -/
-lemma sum_negMulLog_lt (h₀ : ∀ i ∈ s, 0 < w i) (h₁ : ∑ i in s, w i = 1) (hmem : ∀ i ∈ s, 0 ≤ p i)
-    (hp : ∃ j ∈ s, ∃ k ∈ s, p j ≠ p k) :
-    ∑ i in s, w i * negMulLog (p i) < negMulLog (∑ i in s, w i * p i) :=
-  strictConcaveOn_negMulLog.lt_map_sum h₀ h₁ hmem hp
-
-/-- The equality case of Jensen's inequality for the entropy function. -/
-lemma sum_negMulLog_eq_iff (h₀ : ∀ i ∈ s, 0 < w i) (h₁ : ∑ i in s, w i = 1)
-    (hmem : ∀ i ∈ s, 0 ≤ p i) :
-    ∑ i in s, w i * negMulLog (p i) = negMulLog (∑ i in s, w i * p i) ↔
-      ∀ j ∈ s, p j = ∑ i in s, w i * p i :=
-  eq_comm.trans $ strictConcaveOn_negMulLog.map_sum_eq_iff h₀ h₁ hmem
-
-/-- The equality case of Jensen's inequality for the entropy function. -/
-lemma sum_negMulLog_eq_iff' (h₀ : ∀ i ∈ s, 0 ≤ w i) (h₁ : ∑ i in s, w i = 1)
-    (hmem : ∀ i ∈ s, 0 ≤ p i) :
-    ∑ i in s, w i * negMulLog (p i) = negMulLog (∑ i in s, w i * p i) ↔
-      ∀ j ∈ s, w j ≠ 0 → p j = ∑ i in s, w i * p i :=
-  eq_comm.trans $ strictConcaveOn_negMulLog.map_sum_eq_iff' h₀ h₁ hmem
-
 /-- If $S$ is a finite set, and $a_s,b_s$ are non-negative for $s\in S$, then
   $$\sum_{s\in S} a_s \log\frac{a_s}{b_s}\ge \left(\sum_{s\in S}a_s\right)\log\frac{\sum_{s\in S} a_s}{\sum_{s\in S} b_s},$$
   with the convention $0\log\frac{0}{b}=0$ for any $b\ge 0$ and $0\log\frac{a}{0}=\infty$ for any $a>0$. -/