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.Main
PFR.MoreRuzsaDist
PFR.MultiTauFunctional
PFR.RhoFunctional
PFR.SecondEstimate
PFR.TauFunctional
PFR.TorsionEndgame
PFR.WeakPFR
PFR.kullback
PFR.ForMathlib.CompactProb
PFR.ForMathlib.Elementary
PFR.ForMathlib.FiniteMeasureComponent
PFR.ForMathlib.FiniteMeasureProd
PFR.ForMathlib.FiniteRange
PFR.ForMathlib.Graph
PFR.ForMathlib.MeasureReal
PFR.ForMathlib.Pair
PFR.ForMathlib.ProbabilityMeasureProdCont
PFR.ForMathlib.Summable
PFR.ForMathlib.Uniform
PFR.Tactic.Finiteness
PFR.Tactic.RPowSimp
PFR.ForMathlib.Entropy.Basic
PFR.ForMathlib.Entropy.Group
PFR.ForMathlib.Entropy.Measure
PFR.ForMathlib.Entropy.RuzsaDist
PFR.ForMathlib.Entropy.RuzsaSetDist
PFR.Mathlib.GroupTheory.Torsion
PFR.Mathlib.Probability.ConditionalProbability
PFR.Mathlib.Probability.IdentDistrib
PFR.Tactic.Finiteness.Attr
PFR.ForMathlib.Entropy.Kernel.Basic
PFR.ForMathlib.Entropy.Kernel.Group
PFR.ForMathlib.Entropy.Kernel.MutualInfo
PFR.ForMathlib.Entropy.Kernel.RuzsaDist
PFR.Mathlib.Data.Fin.VecNotation
PFR.Mathlib.LinearAlgebra.Basis.VectorSpace
PFR.Mathlib.MeasureTheory.Constructions.Pi
PFR.Mathlib.MeasureTheory.Integral.Bochner
PFR.Mathlib.MeasureTheory.Integral.Lebesgue
PFR.Mathlib.MeasureTheory.Integral.SetIntegral
PFR.Mathlib.MeasureTheory.MeasurableSpace.Basic
PFR.Mathlib.MeasureTheory.Measure.MeasureSpace
PFR.Mathlib.MeasureTheory.Measure.NullMeasurable
PFR.Mathlib.MeasureTheory.Measure.ProbabilityMeasure
PFR.Mathlib.MeasureTheory.Measure.Typeclasses
PFR.Mathlib.Probability.Independence.Basic
PFR.Mathlib.Probability.Independence.Conditional
PFR.Mathlib.Probability.Independence.FourVariables
PFR.Mathlib.Probability.Independence.Kernel
PFR.Mathlib.Probability.Kernel.Composition
PFR.Mathlib.Probability.Kernel.Disintegration
PFR.Mathlib.Probability.Kernel.MeasureCompProd
PFR.Mathlib.SetTheory.Cardinal.Finite
PFR.Mathlib.Algebra.Group.Subgroup.Pointwise
PFR.Mathlib.Data.Set.Pointwise.SMul
PFR.Mathlib.MeasureTheory.Constructions.Prod.Basic
Imported by