1. For Mathlib🔗

Modules in the For Mathlib slice are grouped from the first path component after the project root.

• ForMathlib.InformationTheory.KullbackLeibler.ChainRule 8 declarations

• ForMathlib.Probability.Kernel.Composition.Lemmas 1 declarations

• ForMathlib.Probability.Kernel.Composition.MapComap 5 declarations

• ForMathlib.InformationTheory.KullbackLeibler.CompProd 5 declarations

• ForMathlib.InformationTheory.KullbackLeibler.Convex 7 declarations

• ForMathlib.InformationTheory.KullbackLeibler.DataProcessing 1 declarations

• ForMathlib.InformationTheory.KullbackLeibler.MapSequence 2 declarations

• ForMathlib.InformationTheory.KullbackLeibler.Restrict 6 declarations

• ForMathlib.MeasureTheory.Measurable 5 declarations

• ForMathlib.MeasureTheory.MeasurableSpace.Embedding 19 declarations

• ForMathlib.MeasureTheory.Measure.AbsolutelyContinuous 1 declarations

• ForMathlib.MeasureTheory.OuterMeasure.Basic 1 declarations

• ForMathlib.MeasureTheory.Order.Lattice 1 declarations

• ForMathlib.MeasureTheory.Order.MeasurableArg 17 declarations

• ForMathlib.Order.Interval.Finset 1 declarations

• ForMathlib.Probability.ConditionalProbability 1 declarations

• ForMathlib.Probability.HasCondDistrib 26 declarations

• ForMathlib.Probability.Independence.CondDistrib 37 declarations

• ForMathlib.Probability.Kernel.KernelSub 15 declarations

• ForMathlib.Probability.HasLaw 5 declarations

• ForMathlib.Probability.Independence.CondIndepFun 10 declarations

• ForMathlib.Probability.Independence.IndepFun 16 declarations

• ForMathlib.Probability.Independence.IndepInfinitePi 3 declarations

• ForMathlib.Probability.Integrable 1 declarations

• ForMathlib.Probability.Kernel.Basic 1 declarations

• ForMathlib.Probability.Kernel.Composition.IntegralCompProd 2 declarations

• ForMathlib.Probability.Kernel.Composition.MeasureCompProd 1 declarations

• ForMathlib.Probability.Kernel.IonescuTulcea.Traj 16 declarations

• ForMathlib.Probability.Moments.SubExponential 107 declarations

• ForMathlib.Probability.Moments.SubGaussian 9 declarations

• ForMathlib.Probability.WithDensity 9 declarations

• ForMathlib.Topology.Instances.ENNReal.Lemmas 1 declarations

Module dependencies

Showing the 2 modules that depend on one another. The other 30 are independent of the rest of the chapter.