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.Group.Subgroup.Pointwise
import PFR.Mathlib.Data.Fin.VecNotation
import PFR.Mathlib.Data.Set.Pointwise.SMul
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.MeasurableSpace.Basic
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.FourVariables
import PFR.Mathlib.Probability.Independence.Kernel
import PFR.Mathlib.Probability.Kernel.Composition
import PFR.Mathlib.Probability.Kernel.Disintegration
import PFR.Mathlib.Probability.Kernel.MeasureCompProd
import PFR.Mathlib.SetTheory.Cardinal.Finite
import PFR.MoreRuzsaDist
import PFR.MultiTauFunctional
import PFR.SecondEstimate
import PFR.Tactic.Finiteness
import PFR.Tactic.Finiteness.Attr
import PFR.Tactic.RPowSimp
import PFR.TauFunctional
import PFR.WeakPFR