Documentation
PFR
Search
Google site search
return to top
source
Imports
Init
PFR.ApproxHomPFR
PFR.BoundingMutual
PFR.Endgame
PFR.EntropyPFR
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.GroupQuot
PFR.ForMathlib.MeasureReal
PFR.ForMathlib.Pair
PFR.ForMathlib.ProbabilityMeasureProdCont
PFR.ForMathlib.Uniform
PFR.ForMathlib.ZModModule
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.Mathlib.Algebra.AddTorsor
PFR.Mathlib.Probability.ConditionalProbability
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.LinearAlgebra.AffineSpace.AffineSubspace
PFR.Mathlib.LinearAlgebra.Basis.VectorSpace
PFR.Mathlib.LinearAlgebra.Dimension.Finrank
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.FourVariables
PFR.Mathlib.Probability.Independence.Kernel
PFR.Mathlib.Probability.Independence.ThreeVariables
PFR.Mathlib.Probability.Kernel.Composition
PFR.Mathlib.Probability.Kernel.Disintegration
PFR.Mathlib.SetTheory.Cardinal.Finite
PFR.Mathlib.Analysis.SpecialFunctions.Log.Basic
PFR.Mathlib.Data.Set.Pointwise.SMul
Imported by