pfr/PFR.lean at master · TFBloom/pfr · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
import PFR.ApproxHomPFR
import PFR.Endgame
import PFR.EntropyPFR
import PFR.Fibring
import PFR.FirstEstimate
import PFR.ForMathlib.CompactProb
import PFR.ForMathlib.Elementary
import PFR.ForMathlib.Entropy.Basic
import PFR.ForMathlib.Entropy.Group
import PFR.ForMathlib.Entropy.Kernel.Basic
import PFR.ForMathlib.Entropy.Kernel.Group
import PFR.ForMathlib.Entropy.Kernel.MutualInfo
import PFR.ForMathlib.Entropy.Kernel.RuzsaDist
import PFR.ForMathlib.Entropy.Measure
import PFR.ForMathlib.Entropy.RuzsaDist
import PFR.ForMathlib.FiniteMeasureComponent
import PFR.ForMathlib.FiniteMeasureProd
import PFR.ForMathlib.Graph
import PFR.ForMathlib.MeasureReal
import PFR.ForMathlib.Pair
import PFR.ForMathlib.ProbabilityMeasureProdCont
import PFR.ForMathlib.Uniform
import PFR.HomPFR
import PFR.HundredPercent
import PFR.ImprovedPFR
import PFR.Main
import PFR.Mathlib.Algebra.Group.Hom.Basic
import PFR.Mathlib.Algebra.Module.Submodule.Map
import PFR.Mathlib.Algebra.Order.Archimedean
import PFR.Mathlib.Analysis.Convex.Jensen
import PFR.Mathlib.Analysis.Convex.Topology
import PFR.Mathlib.Analysis.SpecialFunctions.NegMulLog
import PFR.Mathlib.Combinatorics.Additive.RuzsaCovering
import PFR.Mathlib.Data.Fin.Basic
import PFR.Mathlib.Data.Finset.Pointwise
import PFR.Mathlib.Data.Finset.Sigma
import PFR.Mathlib.Data.Fintype.Card
import PFR.Mathlib.Data.Fintype.Sigma
import PFR.Mathlib.Data.Set.Finite
import PFR.Mathlib.Data.Set.Image
import PFR.Mathlib.Data.Set.Pointwise.Basic
import PFR.Mathlib.Data.Set.Pointwise.Finite
import PFR.Mathlib.Data.Set.Sigma
import PFR.Mathlib.GroupTheory.Sylow
import PFR.Mathlib.Init.Core
import PFR.Mathlib.LinearAlgebra.Basis.VectorSpace
import PFR.Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
import PFR.Mathlib.MeasureTheory.Constructions.Pi
import PFR.Mathlib.MeasureTheory.Constructions.Prod.Basic
import PFR.Mathlib.MeasureTheory.Integral.Bochner
import PFR.Mathlib.MeasureTheory.Integral.Lebesgue
import PFR.Mathlib.MeasureTheory.MeasurableSpace.Basic
import PFR.Mathlib.MeasureTheory.Measure.Dirac
import PFR.Mathlib.MeasureTheory.Measure.MeasureSpace
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.Kernel
import PFR.Mathlib.Probability.Kernel.Disintegration
import PFR.Mathlib.Probability.Kernel.MeasureCompProd
import PFR.Mathlib.SetTheory.Cardinal.Finite
import PFR.Mathlib.Topology.Bases
import PFR.Mathlib.Topology.Clopen
import PFR.SecondEstimate
import PFR.Tactic.Finiteness
import PFR.Tactic.Finiteness.Attr
import PFR.Tactic.RPowSimp
import PFR.TauFunctional