PFR/ForMathlib/Entropy/Kernel/Group.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma measureEntropy_inv line 25 source

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

   Statement uses: MeasurableSpace, MeasurableSingletonClass, Group, Countable, MeasureTheory.Measure, Eq, Real, ProbabilityTheory.measureEntropy, MeasureTheory.Measure.map, Inv.inv

   Proof uses: ProbabilityTheory.measureEntropy_map_of_injective, MeasurableInv.measurable_inv, inv_injective

   11 instances, coercions and auxiliary constants left out.

2. lemma measureEntropy_div_comm line 29 source

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

   Statement uses: MeasurableSpace, MeasurableSingletonClass, Group, Countable, MeasureTheory.Measure, Prod, Eq, Real, ProbabilityTheory.measureEntropy, MeasureTheory.Measure.map, HDiv.hDiv, Prod.fst, Prod.snd

   Proof uses: Eq.mpr, Inv.inv, id, congrArg, Eq.symm, measureEntropy_inv, Function.comp, MeasureTheory.Measure.map_map, MeasurableInv.measurable_inv, MeasurableDiv₂.measurable_div, Eq.rec, Eq.refl, funext, of_eq_true, Eq.trans, True, congrFun', inv_div, eq_self

   18 instances, coercions and auxiliary constants left out.

   Tactic trace: 3 steps

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

3. lemma ProbabilityTheory.Kernel.entropy_inv line 38 source

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

   Statement uses: MeasurableSpace, MeasurableSingletonClass, Group, Countable, ProbabilityTheory.Kernel, MeasureTheory.Measure, Eq, Real, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.map, Inv.inv

   Proof uses: ProbabilityTheory.Kernel.entropy_map_of_injective, inv_injective, MeasurableInv.measurable_inv

   11 instances, coercions and auxiliary constants left out.

4. lemma ProbabilityTheory.Kernel.entropy_div_comm line 42 source

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

   Statement uses: MeasurableSpace, MeasurableSingletonClass, Group, Countable, ProbabilityTheory.Kernel, Prod, MeasureTheory.Measure, Eq, Real, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.map, HDiv.hDiv, Prod.fst, Prod.snd

   Proof uses: Eq.mpr, Inv.inv, id, congrArg, Eq.symm, ProbabilityTheory.Kernel.entropy_inv, Function.comp, ProbabilityTheory.Kernel.map_map, Measurable.fun_div, Measurable.fst, measurable_id', Measurable.snd, Measurable.fun_inv, Eq.rec, Eq.refl, funext, of_eq_true, Eq.trans, True, congrFun' and 2 more

   18 instances, coercions and auxiliary constants left out.

   Tactic trace: 5 steps

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

5. lemma ProbabilityTheory.Kernel.entropy_snd_sub_mutualInfo_le_entropy_map_mul line 52 source

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

   Statement uses: MeasurableSpace, MeasurableSingletonClass, Group, Countable, ProbabilityTheory.Kernel, Prod, ProbabilityTheory.IsZeroOrMarkovKernel, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, ProbabilityTheory.FiniteSupport, ProbabilityTheory.Kernel.AEFiniteKernelSupport, LE.le, Real, HSub.hSub, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.snd, ProbabilityTheory.Kernel.mutualInfo, ProbabilityTheory.Kernel.map, HMul.hMul, Prod.fst and 1 more

   Proof uses: ProbabilityTheory.Kernel.entropy_snd_sub_mutualInfo_le_entropy_map_of_injective, mul_right_injective

   21 instances, coercions and auxiliary constants left out.

6. lemma ProbabilityTheory.Kernel.entropy_snd_sub_mutualInfo_le_entropy_map_mul' line 59 source

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

   Statement uses: MeasurableSpace, MeasurableSingletonClass, Group, Countable, ProbabilityTheory.Kernel, Prod, ProbabilityTheory.IsZeroOrMarkovKernel, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, ProbabilityTheory.FiniteSupport, ProbabilityTheory.Kernel.AEFiniteKernelSupport, LE.le, Real, HSub.hSub, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.snd, ProbabilityTheory.Kernel.mutualInfo, ProbabilityTheory.Kernel.map, HMul.hMul, Prod.snd and 1 more

   Proof uses: ProbabilityTheory.Kernel.entropy_snd_sub_mutualInfo_le_entropy_map_of_injective, mul_left_injective

   21 instances, coercions and auxiliary constants left out.

7. lemma ProbabilityTheory.Kernel.entropy_fst_sub_mutualInfo_le_entropy_map_mul line 66 source

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

   Statement uses: MeasurableSpace, MeasurableSingletonClass, Group, Countable, ProbabilityTheory.Kernel, Prod, ProbabilityTheory.IsZeroOrMarkovKernel, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, ProbabilityTheory.FiniteSupport, ProbabilityTheory.Kernel.AEFiniteKernelSupport, LE.le, Real, HSub.hSub, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.fst, ProbabilityTheory.Kernel.mutualInfo, ProbabilityTheory.Kernel.map, HMul.hMul, Prod.fst and 1 more

   Proof uses: ProbabilityTheory.Kernel.snd, ProbabilityTheory.Kernel.swapRight, ProbabilityTheory.Kernel.entropy_snd_sub_mutualInfo_le_entropy_map_mul', ProbabilityTheory.Kernel.AEFiniteKernelSupport.swapRight, LE.le.trans_eq, Function.comp, Prod.swap, Eq.mp, congr, congrArg, congrFun', ProbabilityTheory.Kernel.snd_swapRight, ProbabilityTheory.Kernel.mutualInfo_swapRight, ProbabilityTheory.Kernel.map_swapRight, Eq, rfl, of_eq_true, Eq.trans, True, eq_self

   21 instances, coercions and auxiliary constants left out.

   Tactic trace: 5 steps

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

8. lemma ProbabilityTheory.Kernel.entropy_fst_sub_mutualInfo_le_entropy_map_mul' line 77 source

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

   Statement uses: MeasurableSpace, MeasurableSingletonClass, Group, Countable, ProbabilityTheory.Kernel, Prod, ProbabilityTheory.IsZeroOrMarkovKernel, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, ProbabilityTheory.FiniteSupport, ProbabilityTheory.Kernel.AEFiniteKernelSupport, LE.le, Real, HSub.hSub, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.fst, ProbabilityTheory.Kernel.mutualInfo, ProbabilityTheory.Kernel.map, HMul.hMul, Prod.snd and 1 more

   Proof uses: ProbabilityTheory.Kernel.snd, ProbabilityTheory.Kernel.swapRight, ProbabilityTheory.Kernel.entropy_snd_sub_mutualInfo_le_entropy_map_mul, ProbabilityTheory.Kernel.AEFiniteKernelSupport.swapRight, LE.le.trans_eq, Function.comp, Prod.swap, Eq.mp, congr, congrArg, congrFun', ProbabilityTheory.Kernel.snd_swapRight, ProbabilityTheory.Kernel.mutualInfo_swapRight, ProbabilityTheory.Kernel.map_swapRight, Eq, rfl, of_eq_true, Eq.trans, True, eq_self

   21 instances, coercions and auxiliary constants left out.

   Tactic trace: 5 steps

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

9. lemma ProbabilityTheory.Kernel.entropy_snd_sub_mutualInfo_le_entropy_map_div line 88 source

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

   Statement uses: MeasurableSpace, MeasurableSingletonClass, Group, Countable, ProbabilityTheory.Kernel, Prod, ProbabilityTheory.IsZeroOrMarkovKernel, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, ProbabilityTheory.FiniteSupport, ProbabilityTheory.Kernel.AEFiniteKernelSupport, LE.le, Real, HSub.hSub, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.snd, ProbabilityTheory.Kernel.mutualInfo, ProbabilityTheory.Kernel.map, HDiv.hDiv, Prod.fst and 1 more

   Proof uses: ProbabilityTheory.Kernel.entropy_snd_sub_mutualInfo_le_entropy_map_of_injective, div_right_injective

   11 instances, coercions and auxiliary constants left out.

10. lemma ProbabilityTheory.Kernel.entropy_fst_sub_mutualInfo_le_entropy_map_div line 95 source

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

    Statement uses: MeasurableSpace, MeasurableSingletonClass, Group, Countable, ProbabilityTheory.Kernel, Prod, ProbabilityTheory.IsZeroOrMarkovKernel, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, ProbabilityTheory.FiniteSupport, ProbabilityTheory.Kernel.AEFiniteKernelSupport, LE.le, Real, HSub.hSub, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.fst, ProbabilityTheory.Kernel.mutualInfo, ProbabilityTheory.Kernel.map, HDiv.hDiv, Prod.fst and 1 more

    Proof uses: ProbabilityTheory.Kernel.snd, ProbabilityTheory.Kernel.swapRight, ProbabilityTheory.Kernel.entropy_snd_sub_mutualInfo_le_entropy_map_div, ProbabilityTheory.Kernel.AEFiniteKernelSupport.swapRight, LE.le.trans_eq, Function.comp, Prod.swap, Eq.mp, congr, congrArg, congrFun', ProbabilityTheory.Kernel.snd_swapRight, ProbabilityTheory.Kernel.mutualInfo_swapRight, ProbabilityTheory.Kernel.map_swapRight, Eq, rfl, Eq.mpr, id, Eq.symm, ProbabilityTheory.Kernel.entropy_div_comm and 1 more

    15 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

11. lemma ProbabilityTheory.Kernel.max_entropy_sub_mutualInfo_le_entropy_mul line 107 source

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

    Statement uses: MeasurableSpace, MeasurableSingletonClass, Group, Countable, ProbabilityTheory.Kernel, Prod, ProbabilityTheory.IsZeroOrMarkovKernel, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, ProbabilityTheory.FiniteSupport, ProbabilityTheory.Kernel.AEFiniteKernelSupport, LE.le, Real, HSub.hSub, Max.max, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.fst, ProbabilityTheory.Kernel.snd, ProbabilityTheory.Kernel.mutualInfo, ProbabilityTheory.Kernel.map and 3 more

    Proof uses: Eq.mpr, id, Eq, congrArg, Eq.symm, max_sub_sub_right, And, propext, max_le_iff, And.intro, ProbabilityTheory.Kernel.entropy_fst_sub_mutualInfo_le_entropy_map_mul, ProbabilityTheory.Kernel.entropy_snd_sub_mutualInfo_le_entropy_map_mul

    36 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

12. lemma ProbabilityTheory.Kernel.max_entropy_sub_mutualInfo_le_entropy_mul' line 117 source

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

    Statement uses: MeasurableSpace, MeasurableSingletonClass, Group, Countable, ProbabilityTheory.Kernel, Prod, ProbabilityTheory.IsZeroOrMarkovKernel, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, ProbabilityTheory.FiniteSupport, ProbabilityTheory.Kernel.AEFiniteKernelSupport, LE.le, Real, HSub.hSub, Max.max, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.fst, ProbabilityTheory.Kernel.snd, ProbabilityTheory.Kernel.mutualInfo, ProbabilityTheory.Kernel.map and 3 more

    Proof uses: Eq.mpr, id, Eq, congrArg, Eq.symm, max_sub_sub_right, And, propext, max_le_iff, And.intro, ProbabilityTheory.Kernel.entropy_fst_sub_mutualInfo_le_entropy_map_mul', ProbabilityTheory.Kernel.entropy_snd_sub_mutualInfo_le_entropy_map_mul'

    36 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

13. lemma ProbabilityTheory.Kernel.max_entropy_sub_mutualInfo_le_entropy_div line 127 source

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

    Statement uses: MeasurableSpace, MeasurableSingletonClass, Group, Countable, ProbabilityTheory.Kernel, Prod, ProbabilityTheory.IsZeroOrMarkovKernel, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, ProbabilityTheory.FiniteSupport, ProbabilityTheory.Kernel.AEFiniteKernelSupport, LE.le, Real, HSub.hSub, Max.max, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.fst, ProbabilityTheory.Kernel.snd, ProbabilityTheory.Kernel.mutualInfo, ProbabilityTheory.Kernel.map and 3 more

    Proof uses: Eq.mpr, id, Eq, congrArg, Eq.symm, max_sub_sub_right, And, propext, max_le_iff, And.intro, ProbabilityTheory.Kernel.entropy_fst_sub_mutualInfo_le_entropy_map_div, ProbabilityTheory.Kernel.entropy_snd_sub_mutualInfo_le_entropy_map_div

    30 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

14. lemma ProbabilityTheory.Kernel.max_entropy_le_entropy_mul_prod line 137 source

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

    Statement uses: MeasurableSpace, MeasurableSingletonClass, Group, Countable, ProbabilityTheory.Kernel, ProbabilityTheory.IsMarkovKernel, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, ProbabilityTheory.FiniteSupport, ProbabilityTheory.Kernel.AEFiniteKernelSupport, LE.le, Real, Max.max, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.map, Prod, ProbabilityTheory.Kernel.prod, HMul.hMul, Prod.fst, Prod.snd

    Proof uses: Trans.trans, Eq, HSub.hSub, ProbabilityTheory.Kernel.mutualInfo, Eq.mpr, OfNat.ofNat, id, congrArg, ProbabilityTheory.Kernel.mutualInfo_prod, sub_zero, Eq.refl, ProbabilityTheory.Kernel.fst, ProbabilityTheory.Kernel.snd, eq_of_heq, LE, HEq, HEq.refl, Eq.symm, outParam, HSub and 9 more

    37 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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

15. lemma ProbabilityTheory.Kernel.max_entropy_le_entropy_div_prod line 151 source

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

    Statement uses: MeasurableSpace, MeasurableSingletonClass, Group, Countable, ProbabilityTheory.Kernel, ProbabilityTheory.IsMarkovKernel, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, ProbabilityTheory.FiniteSupport, ProbabilityTheory.Kernel.AEFiniteKernelSupport, LE.le, Real, Max.max, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.map, Prod, ProbabilityTheory.Kernel.prod, HDiv.hDiv, Prod.fst, Prod.snd

    Proof uses: Trans.trans, Eq, HSub.hSub, ProbabilityTheory.Kernel.mutualInfo, Eq.mpr, OfNat.ofNat, id, congrArg, ProbabilityTheory.Kernel.mutualInfo_prod, sub_zero, Eq.refl, ProbabilityTheory.Kernel.fst, ProbabilityTheory.Kernel.snd, eq_of_heq, LE, HEq, HEq.refl, Eq.symm, outParam, HSub and 9 more

    31 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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