PFR.lean

import PFR.ApproxHomPFR
import PFR.BoundingMutual
import PFR.Endgame
import PFR.EntropyPFR
import PFR.Examples
import PFR.Fibring
import PFR.FirstEstimate
import PFR.ForMathlib.AffineSpaceDim
import PFR.ForMathlib.ConditionalIndependence
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.FiniteRange.ConditionalProbability
import PFR.ForMathlib.FiniteRange.Defs
import PFR.ForMathlib.FiniteRange.IdentDistrib
import PFR.ForMathlib.FourVariables
import PFR.ForMathlib.Pair
import PFR.ForMathlib.ThreeVariables
import PFR.ForMathlib.Uniform
import PFR.HomPFR
import PFR.HundredPercent
import PFR.ImprovedPFR
import PFR.Kullback
import PFR.Main
import PFR.Mathlib.Algebra.BigOperators.Fin
import PFR.Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
import PFR.Mathlib.Analysis.SpecialFunctions.NegMulLog
import PFR.Mathlib.Data.Fin.Basic
import PFR.Mathlib.Data.Set.Basic
import PFR.Mathlib.Data.Set.Card
import PFR.Mathlib.Data.Set.Insert
import PFR.Mathlib.LinearAlgebra.Basis.VectorSpace
import PFR.Mathlib.LinearAlgebra.Dimension.Finrank
import PFR.Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
import PFR.Mathlib.MeasureTheory.Constructions.Pi
import PFR.Mathlib.MeasureTheory.Group.Arithmetic
import PFR.Mathlib.MeasureTheory.Integral.Bochner.Set
import PFR.Mathlib.MeasureTheory.Integral.Lebesgue.Basic
import PFR.Mathlib.MeasureTheory.Integral.Lebesgue.Countable
import PFR.Mathlib.MeasureTheory.MeasurableSpace.Basic
import PFR.Mathlib.MeasureTheory.Measure.Dirac
import PFR.Mathlib.MeasureTheory.Measure.MeasureSpace
import PFR.Mathlib.MeasureTheory.Measure.MeasureSpaceDef
import PFR.Mathlib.MeasureTheory.Measure.ProbabilityMeasure
import PFR.Mathlib.MeasureTheory.Measure.Prod
import PFR.Mathlib.MeasureTheory.Measure.Real
import PFR.Mathlib.MeasureTheory.Measure.Typeclasses.Probability
import PFR.Mathlib.Order.Interval.Finset.Fin
import PFR.Mathlib.Probability.ConditionalProbability
import PFR.Mathlib.Probability.IdentDistrib
import PFR.Mathlib.Probability.Independence.Basic
import PFR.Mathlib.Probability.Independence.Kernel.IndepFun
import PFR.Mathlib.Probability.Kernel.Composition.Comp
import PFR.Mathlib.Probability.Kernel.Disintegration
import PFR.Mathlib.Probability.UniformOn
import PFR.MoreRuzsaDist
import PFR.MultiTauFunctional
import PFR.RhoFunctional
import PFR.SecondEstimate
import PFR.Tactic.RPowSimp
import PFR.TauFunctional
import PFR.TorsionEndgame
import PFR.WeakPFR