Map

How this project builds on itself. An arrow goes from a file to a file that uses something in it, so the foundations are on the left. These links come from names in the source code, not from kernel dependency facts; the separate Trust page says exactly what Lean checked. every declaration's own map, on its file page, shows the same thing one result at a time.

Files as a table

The same map data in a searchable keyboard- and screen-reader-friendly form.

Files and cross-file dependency counts
FileDeclarationsBuilds onUsed by
PFR/ApproxHomPFR.lean631
PFR/BoundingMutual.lean471
PFR/Endgame.lean2074
PFR/EntropyPFR.lean261
PFR/Fibring.lean845
PFR/FirstEstimate.lean944
PFR/ForMathlib/AffineSpaceDim.lean502
PFR/ForMathlib/ConditionalIndependence.lean945
PFR/ForMathlib/Entropy/Basic.lean97913
PFR/ForMathlib/Entropy/Group.lean2950
PFR/ForMathlib/Entropy/Kernel/Basic.lean3866
PFR/ForMathlib/Entropy/Kernel/Group.lean1551
PFR/ForMathlib/Entropy/Kernel/MutualInfo.lean2643
PFR/ForMathlib/Entropy/Kernel/RuzsaDist.lean1872
PFR/ForMathlib/Entropy/Measure.lean52410
PFR/ForMathlib/Entropy/RuzsaDist.lean671416
PFR/ForMathlib/Entropy/RuzsaSetDist.lean851
PFR/ForMathlib/FiniteRange/ConditionalProbability.lean111
PFR/ForMathlib/FiniteRange/Defs.lean20015
PFR/ForMathlib/FiniteRange/IdentDistrib.lean536
PFR/ForMathlib/FourVariables.lean2301
PFR/ForMathlib/Pair.lean204
PFR/ForMathlib/ThreeVariables.lean1110
PFR/ForMathlib/Uniform.lean23211
PFR/HomPFR.lean311
PFR/HundredPercent.lean744
PFR/ImprovedPFR.lean18141
PFR/Kullback.lean2131
PFR/Main.lean874
PFR/Mathlib/Algebra/BigOperators/Fin.lean101
PFR/Mathlib/Algebra/Group/Action/Pointwise/Set/Basic.lean200
PFR/Mathlib/Analysis/SpecialFunctions/NegMulLog.lean302
PFR/Mathlib/Data/Fin/Basic.lean302
PFR/Mathlib/Data/Finset/Basic.lean100
PFR/Mathlib/Data/Set/Basic.lean100
PFR/Mathlib/Data/Set/Card.lean201
PFR/Mathlib/Data/ZMod/Basic.lean102
PFR/Mathlib/LinearAlgebra/Basis/VectorSpace.lean100
PFR/Mathlib/LinearAlgebra/Dimension/Finrank.lean100
PFR/Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean201
PFR/Mathlib/LinearAlgebra/Quotient/Basic.lean100
PFR/Mathlib/MeasureTheory/Constructions/Pi.lean302
PFR/Mathlib/MeasureTheory/Group/Arithmetic.lean100
PFR/Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean202
PFR/Mathlib/MeasureTheory/Integral/Lebesgue/Countable.lean402
PFR/Mathlib/MeasureTheory/Measure/Dirac/Def.lean100
PFR/Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean101
PFR/Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean703
PFR/Mathlib/MeasureTheory/Measure/Prod.lean404
PFR/Mathlib/MeasureTheory/Measure/Real.lean614
PFR/Mathlib/MeasureTheory/Measure/Typeclasses/Probability.lean110
PFR/Mathlib/Order/Interval/Finset/Defs.lean100
PFR/Mathlib/Order/Interval/Finset/Fin.lean101
PFR/Mathlib/Probability/ConditionalProbability.lean205
PFR/Mathlib/Probability/IdentDistrib.lean25211
PFR/Mathlib/Probability/Independence/Basic.lean1919
PFR/Mathlib/Probability/Independence/Kernel/IndepFun.lean201
PFR/Mathlib/Probability/Kernel/Composition/Comp.lean2413
PFR/Mathlib/Probability/Kernel/Disintegration.lean6428
PFR/Mathlib/Probability/UniformOn.lean1214
PFR/MoreRuzsaDist.lean60153
PFR/MultiTauFunctional.lean1432
PFR/RhoFunctional.lean82173
PFR/SecondEstimate.lean342
PFR/Tactic/RPowSimp.lean3600
PFR/TauFunctional.lean1247
PFR/TorsionEndgame.lean25101
PFR/WeakPFR.lean25141
PFRPalomar/Solution.lean1060
PFRPalomar/Challenge.lean600