Documentation
LeanPool
.
PFR
.
Imports
Search
return to top
source
Imports
Init
LeanPool.PFR
LeanPool.PFR.ApproxHomPFR
LeanPool.PFR.BoundingMutual
LeanPool.PFR.Endgame
LeanPool.PFR.EntropyPFR
LeanPool.PFR.Fibring
LeanPool.PFR.FirstEstimate
LeanPool.PFR.HomPFR
LeanPool.PFR.HundredPercent
LeanPool.PFR.ImprovedPFR
LeanPool.PFR.Kullback
LeanPool.PFR.Main
LeanPool.PFR.MoreRuzsaDist
LeanPool.PFR.MultiTauFunctional
LeanPool.PFR.RhoFunctional
LeanPool.PFR.SecondEstimate
LeanPool.PFR.Solution
LeanPool.PFR.TauFunctional
LeanPool.PFR.TorsionEndgame
LeanPool.PFR.WeakPFR
LeanPool.PFR.AddCombi.BSG
LeanPool.PFR.ForMathlib.AffineSpaceDim
LeanPool.PFR.ForMathlib.FourVariables
LeanPool.PFR.ForMathlib.ThreeVariables
LeanPool.PFR.ForMathlib.Entropy.Group
LeanPool.PFR.ForMathlib.Entropy.RuzsaDist
LeanPool.PFR.ForMathlib.Entropy.RuzsaSetDist
LeanPool.PFR.ForMathlib.FiniteRange.IdentDistrib
LeanPool.PFR.AddCombi.Convolution.Finite.Defs
LeanPool.PFR.AddCombi.Convolution.Finite.Order
LeanPool.PFR.ForMathlib.Entropy.Kernel.Group
LeanPool.PFR.ForMathlib.Entropy.Kernel.RuzsaDist
LeanPool.PFR.Mathlib.Algebra.BigOperators.Fin
LeanPool.PFR.Mathlib.Data.Fin.Basic
LeanPool.PFR.Mathlib.Data.Finset.Basic
LeanPool.PFR.Mathlib.LinearAlgebra.Basis.VectorSpace
LeanPool.PFR.Mathlib.LinearAlgebra.Dimension.Finrank
LeanPool.PFR.Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
LeanPool.PFR.Mathlib.LinearAlgebra.Quotient.Basic
LeanPool.PFR.Mathlib.MeasureTheory.Group.Arithmetic
LeanPool.PFR.Mathlib.MeasureTheory.Measure.ProbabilityMeasure
LeanPool.PFR.AddCombi.Mathlib.Algebra.GroupWithZero.Indicator
LeanPool.PFR.AddCombi.Mathlib.Algebra.Notation.Indicator
LeanPool.PFR.AddCombi.Mathlib.Algebra.Star.Pi
LeanPool.PFR.AddCombi.Mathlib.Combinatorics.Additive.Energy
LeanPool.PFR.AddCombi.Mathlib.Data.Finset.Density
LeanPool.PFR.Mathlib.Order.Interval.Finset.Defs
LeanPool.PFR.Mathlib.Order.Interval.Finset.Fin
LeanPool.PFR.AddCombi.Mathlib.Algebra.Order.GroupWithZero.Indicator
LeanPool.PFR.AddCombi.Mathlib.Algebra.Order.Ring.NNRat
LeanPool.PFR.Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Imported by