PFR.lean
0 declarations, 0 contain sorry, 0 declared as axioms
This file declares nothing itself. It gathers the 73 imports below, so a file that imports it gets all of them.
Imports
- PFR.ApproxHomPFR
- PFR.BoundingMutual
- PFR.Endgame
- PFR.EntropyPFR
- PFR.Examples
- PFR.Fibring
- PFR.FirstEstimate
- PFR.ForMathlib.AffineSpaceDim
- PFR.ForMathlib.ConditionalIndependence
- PFR.ForMathlib.Entropy.Basic
- PFR.ForMathlib.Entropy.Group
- PFR.ForMathlib.Entropy.Kernel.Basic
- PFR.ForMathlib.Entropy.Kernel.Group
- PFR.ForMathlib.Entropy.Kernel.MutualInfo
- PFR.ForMathlib.Entropy.Kernel.RuzsaDist
- PFR.ForMathlib.Entropy.Measure
- PFR.ForMathlib.Entropy.RuzsaDist
- PFR.ForMathlib.Entropy.RuzsaSetDist
- PFR.ForMathlib.FiniteRange.ConditionalProbability
- PFR.ForMathlib.FiniteRange.Defs
- PFR.ForMathlib.FiniteRange.IdentDistrib
- PFR.ForMathlib.FourVariables
- PFR.ForMathlib.Pair
- PFR.ForMathlib.ThreeVariables
- PFR.ForMathlib.Uniform
- PFR.HomPFR
- PFR.HundredPercent
- PFR.ImprovedPFR
- PFR.Kullback
- PFR.Main
- PFR.Mathlib.Algebra.BigOperators.Fin
- PFR.Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
- PFR.Mathlib.Analysis.SpecialFunctions.NegMulLog
- PFR.Mathlib.Data.Fin.Basic
- PFR.Mathlib.Data.Finset.Basic
- PFR.Mathlib.Data.Set.Basic
- PFR.Mathlib.Data.Set.Card
- PFR.Mathlib.Data.Set.Insert
- PFR.Mathlib.Data.ZMod.Basic
- PFR.Mathlib.LinearAlgebra.Basis.VectorSpace
- PFR.Mathlib.LinearAlgebra.Dimension.Finrank
- PFR.Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
- PFR.Mathlib.LinearAlgebra.Quotient.Basic
- PFR.Mathlib.MeasureTheory.Constructions.Pi
- PFR.Mathlib.MeasureTheory.Group.Arithmetic
- PFR.Mathlib.MeasureTheory.Integral.Lebesgue.Basic
- PFR.Mathlib.MeasureTheory.Integral.Lebesgue.Countable
- PFR.Mathlib.MeasureTheory.MeasurableSpace.Basic
- PFR.Mathlib.MeasureTheory.MeasurableSpace.Constructions
- PFR.Mathlib.MeasureTheory.Measure.Dirac.Def
- PFR.Mathlib.MeasureTheory.Measure.MeasureSpace
- PFR.Mathlib.MeasureTheory.Measure.MeasureSpaceDef
- PFR.Mathlib.MeasureTheory.Measure.ProbabilityMeasure
- PFR.Mathlib.MeasureTheory.Measure.Prod
- PFR.Mathlib.MeasureTheory.Measure.Real
- PFR.Mathlib.MeasureTheory.Measure.Typeclasses.Probability
- PFR.Mathlib.Order.Interval.Finset.Defs
- PFR.Mathlib.Order.Interval.Finset.Fin
- PFR.Mathlib.Probability.ConditionalProbability
- PFR.Mathlib.Probability.IdentDistrib
- PFR.Mathlib.Probability.Independence.Basic
- PFR.Mathlib.Probability.Independence.Kernel.IndepFun
- PFR.Mathlib.Probability.Kernel.Composition.Comp
- PFR.Mathlib.Probability.Kernel.Disintegration
- PFR.Mathlib.Probability.UniformOn
- PFR.MoreRuzsaDist
- PFR.MultiTauFunctional
- PFR.RhoFunctional
- PFR.SecondEstimate
- PFR.Tactic.RPowSimp
- PFR.TauFunctional
- PFR.TorsionEndgame
- PFR.WeakPFR