PFR/BoundingMutual.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma multiDist_of_cast line 16 source

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Nat, Eq, Fin, MeasureTheory.MeasureSpace, MeasureTheory.IsFiniteMeasure, MeasureTheory.MeasureSpace.volume, MeasurableFinGroup, Real, multiDist, Fin.cast

   Proof uses: id, HSub, Eq.rec, HSub.hSub, Eq.refl, ProbabilityTheory.entropy, Finset.sum, Finset.univ, MeasureTheory.Measure.pi, MeasureTheory.Measure.map, ProbabilityTheory.IdentDistrib.entropy_congr, ProbabilityTheory.IdentDistrib.mk, Measurable.aemeasurable, Finset.measurable_sum, Prod, Membership.mem, Finset, measurable_pi_apply, Function.comp, Eq.symm and 25 more

   36 instances, coercions and auxiliary constants left out.

   Tactic trace: 22 steps

   Open to load the checked before-and-after goal states.

2. lemma ProbabilityTheory.iIndepFun.sum_elim For Mathlib? line 39 source

   Source documentation

   For Mathlib?

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: MeasurableSpace, MeasureTheory.Measure, ProbabilityTheory.iIndepFun, ProbabilityTheory.IndepFun, Sum, Sum.elim

   Proof uses: Eq.mpr, Finset, Set, Membership.mem, MeasurableSet, MeasurableSpace.comap, Eq, ENNReal, Set.iInter, Finset.prod, id, congrArg, propext, ProbabilityTheory.iIndepFun_iff, Finset.disjSum, Finset.toLeft, Finset.toRight, Finset.toLeft_disjSum_toRight, Eq.symm, HMul.hMul and 47 more

   37 instances, coercions and auxiliary constants left out.

   Tactic trace: 38 steps

   Open to load the checked before-and-after goal states.

   lemma ProbabilityTheory.iIndepFun.sum_elim {Ω I J G : Type*} [MeasurableSpace Ω] [MeasurableSpace G]
       (μ : Measure Ω) {f : I → Ω → G} {g : J → Ω → G} (hf_indep : iIndepFun f μ)
       (hg_indep : iIndepFun g μ) (hindep : IndepFun (fun ω x ↦ f x ω) (fun ω y ↦ g y ω) μ) :
       iIndepFun (Sum.elim f g) μ := by
   …

3. lemma condMultiDist_of_cast line 77 source

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Nat, Eq, Fin, MeasureTheory.MeasureSpace, MeasurableFinGroup, Fintype, Real, condMultiDist, Fin.cast

   Proof uses: id, Eq.symm, Function.Bijective, And.intro, Function.Injective, Function.Surjective, funext, congrFun, Exists.intro, Function.comp, of_eq_true, eq_self, Eq.mpr, Finset.sum, Finset.univ, HMul.hMul, Finset.prod, MeasureTheory.Measure.real, MeasureTheory.MeasureSpace.volume, Set.preimage and 25 more

   19 instances, coercions and auxiliary constants left out.

   Tactic trace: 25 steps

   Open to load the checked before-and-after goal states.

4. lemma mutual_information_le Documented declaration: mutual_information_le line 107 source

   Source documentation

   Suppose that $X_{i, j}$, $1 \leq i, j \leq m$, are jointly independent $G$-valued random variables, such that for each $j = 1,\dots,m$, the random variables $(X_{i, j})_{i = 1}^m$ coincide in distribution with some permutation of $X_{[m]}$. Write $$ {\mathcal I} := \bbI[ \bigl(\sum_{i=1}^m X_{i, j}\bigr)_{j =1}^{m} : \bigl(\sum_{j=1}^m X_{i, j}\bigr)_{i = 1}^m \; \big| \; \sum_{i=1}^m \sum_{j = 1}^m X_{i, j} ]. $$ Then ${\mathcal I} \leq 4 m^2 \eta k.$

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: MeasurableFinGroup, MeasureTheory.MeasureSpace, multiRefPackage, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Fin, multiRefPackage.m, Measurable, ProbabilityTheory.iIndepFun, multiTauMinimizes, Prod, Prod.mk, Exists, Equiv, ProbabilityTheory.IdentDistrib, LE.le, Real, ProbabilityTheory.condMutualInfo, Finset.sum, Finset.univ and 6 more

   Proof uses: GE.ge, multiRefPackage.hm, NeZero, Eq.mpr, Ne, id, Eq, congrArg, propext, neZero_iff, LT.lt, multiRefPackage.hη, rfl, Fin.mk, Decidable.byContradiction, Not, HSub.hSub, Finset.Ici, condMultiDist, Finset.Iio and 353 more

   346 instances, coercions and auxiliary constants left out.

   Tactic trace: 443 steps (first 200 of 443)

   Open to load the checked before-and-after goal states.

   lemma mutual_information_le {G Ωₒ : Type u} [MeasurableFinGroup G] [MeasureSpace Ωₒ]
       {p : multiRefPackage G Ωₒ} {Ω : Type u} [hΩ : MeasureSpace Ω] [IsProbabilityMeasure hΩ.volume]
       {X : Fin p.m → Ω → G} (hX : ∀ i, Measurable (X i)) (h_indep : iIndepFun X)
       (h_min : multiTauMinimizes p (fun _ ↦ Ω) (fun _ ↦ hΩ) X) {Ω' : Type u} [hΩ' : MeasureSpace Ω']
       [IsProbabilityMeasure hΩ'.volume]
       {X' : Fin p.m × Fin p.m → Ω' → G} (hX' : ∀ i j, Measurable (X' (i, j)))
       (h_indep' : iIndepFun X')
       (hperm : ∀ j, ∃ e : Fin p.m ≃ Fin p.m, IdentDistrib (fun ω ↦ (fun i ↦ X' (i, j) ω))
         (fun ω ↦ (fun i ↦ X (e i) ω))) :
       I[ fun ω ↦ ( fun j ↦ ∑ i, X' (i, j) ω) : fun ω ↦ ( fun i ↦ ∑ j, X' (i, j) ω) |
     fun ω ↦ ∑ i, ∑ j, X' (i, j) ω ] ≤ p.m * (4*p.m+1) * p.η * D[ X; (fun _ ↦ hΩ)] := by
   …

   Mentions: MeasurableFinGroup, multiRefPackage, multiTauMinimizes