Documentation
PFR
Search
return to top
source
Imports
Init
PFR.ApproxHomPFR
PFR.BoundingMutual
PFR.Endgame
PFR.EntropyPFR
PFR.Examples
PFR.Fibring
PFR.FirstEstimate
PFR.HomPFR
PFR.HundredPercent
PFR.ImprovedPFR
PFR.Kullback
PFR.Main
PFR.MoreRuzsaDist
PFR.MultiTauFunctional
PFR.RhoFunctional
PFR.SecondEstimate
PFR.TauFunctional
PFR.TorsionEndgame
PFR.WeakPFR
PFR.ForMathlib.AffineSpaceDim
PFR.ForMathlib.CompactProb
PFR.ForMathlib.ConditionalIndependence
PFR.ForMathlib.FiniteMeasureComponent
PFR.ForMathlib.FiniteMeasureProd
PFR.ForMathlib.FourVariables
PFR.ForMathlib.Pair
PFR.ForMathlib.ProbabilityMeasureProdCont
PFR.ForMathlib.ThreeVariables
PFR.ForMathlib.Uniform
PFR.Tactic.RPowSimp
PFR.ForMathlib.Entropy.Basic
PFR.ForMathlib.Entropy.Group
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.MeasureReal.Defs
PFR.ForMathlib.MeasureReal.Indep
PFR.ForMathlib.MeasureReal.UniformOn
PFR.Mathlib.Probability.IdentDistrib
PFR.Mathlib.Probability.UniformOn
PFR.ForMathlib.Entropy.Kernel.Basic
PFR.ForMathlib.Entropy.Kernel.Group
PFR.ForMathlib.Entropy.Kernel.MutualInfo
PFR.ForMathlib.Entropy.Kernel.RuzsaDist
PFR.Mathlib.Analysis.SpecialFunctions.NegMulLog
PFR.Mathlib.Data.Prod.Basic
PFR.Mathlib.LinearAlgebra.Basis.VectorSpace
PFR.Mathlib.LinearAlgebra.Dimension.Finrank
PFR.Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
PFR.Mathlib.MeasureTheory.Constructions.Pi
PFR.Mathlib.MeasureTheory.Integral.Lebesgue
PFR.Mathlib.MeasureTheory.Integral.SetIntegral
PFR.Mathlib.MeasureTheory.Measure.Prod
PFR.Mathlib.Probability.Independence.Basic
PFR.Mathlib.Probability.Independence.Kernel
PFR.Mathlib.Probability.Kernel.Disintegration
PFR.Mathlib.Probability.Kernel.Composition.Comp
PFR.Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Imported by