PFR.lean

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.Entropy.RuzsaSetDist
import PFR.ForMathlib.FiniteMeasureComponent
import PFR.ForMathlib.FiniteMeasureProd
import PFR.ForMathlib.FiniteRange
import PFR.ForMathlib.Graph
import PFR.ForMathlib.MeasureReal
import PFR.ForMathlib.Pair
import PFR.ForMathlib.ProbabilityMeasureProdCont
import PFR.ForMathlib.Summable
import PFR.ForMathlib.Uniform
import PFR.HomPFR
import PFR.HundredPercent
import PFR.ImprovedPFR
import PFR.Main
import PFR.Mathlib.Algebra.BigOperators.Basic
import PFR.Mathlib.Algebra.Group.Hom.Basic
import PFR.Mathlib.Algebra.GroupWithZero.Units.Lemmas
import PFR.Mathlib.Analysis.SpecialFunctions.NegMulLog
import PFR.Mathlib.Data.Fin.Basic
import PFR.Mathlib.Data.Finset.Sigma
import PFR.Mathlib.Data.Fintype.Card
import PFR.Mathlib.Data.Fintype.Lattice
import PFR.Mathlib.Data.Fintype.Sigma
import PFR.Mathlib.Data.Fin.VecNotation
import PFR.Mathlib.Data.Real.Ennreal
import PFR.Mathlib.Data.Set.Image
import PFR.Mathlib.Data.Set.Pointwise.SMul
import PFR.Mathlib.Data.Set.Sigma
import PFR.Mathlib.GroupTheory.Subgroup.Pointwise
import PFR.Mathlib.GroupTheory.Torsion
import PFR.Mathlib.LinearAlgebra.Basis.VectorSpace
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.Integral.SetIntegral
import PFR.Mathlib.MeasureTheory.Measure.NullMeasurable
import PFR.Mathlib.MeasureTheory.Measure.ProbabilityMeasure
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.Disintegration
import PFR.Mathlib.Probability.Kernel.MeasureCompProd
import PFR.Mathlib.SetTheory.Cardinal.Finite
import PFR.SecondEstimate
import PFR.Tactic.Finiteness
import PFR.Tactic.Finiteness.Attr
import PFR.Tactic.RPowSimp
import PFR.TauFunctional
import PFR.WeakPFR