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.FourVariables
PFR.ForMathlib.Pair
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.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.Algebra.BigOperators.Fin
PFR.Mathlib.Analysis.Convex.StdSimplex
PFR.Mathlib.Analysis.SpecialFunctions.NegMulLog
PFR.Mathlib.Data.Fin.Basic
PFR.Mathlib.Data.Set.Basic
PFR.Mathlib.Data.Set.Card
PFR.Mathlib.Data.Set.Insert
PFR.Mathlib.LinearAlgebra.Basis.VectorSpace
PFR.Mathlib.LinearAlgebra.Dimension.Finrank
PFR.Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
PFR.Mathlib.MeasureTheory.Constructions.Pi
PFR.Mathlib.MeasureTheory.Group.Arithmetic
PFR.Mathlib.MeasureTheory.MeasurableSpace.Basic
PFR.Mathlib.MeasureTheory.Measure.Dirac
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.Probability.Independence.Basic
PFR.Mathlib.Probability.Independence.Kernel
PFR.Mathlib.Probability.Kernel.Disintegration
PFR.Mathlib.MeasureTheory.Integral.Bochner.Set
PFR.Mathlib.MeasureTheory.Integral.Lebesgue.Basic
PFR.Mathlib.MeasureTheory.Integral.Lebesgue.Countable
PFR.Mathlib.MeasureTheory.Measure.Typeclasses.Probability
PFR.Mathlib.Order.Interval.Finset.Fin
PFR.Mathlib.Probability.Kernel.Composition.Comp
PFR.Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Imported by