LeanMachineLearning exposition🔗

Auto-generated exposition for LeanMachineLearning.

Browse the chapters and modules below for each file's declarations, with their statements and documentation. The Graph page shows the dependencies between declarations, and each declaration's details page shows its own dependency graph together with the statements of the declarations it depends on, so that the assumptions behind a result can be checked without leaving the page.

Project overview.

Reader guides

• Overview explains the repository scope and mathematical target.

• Dependency Graph provides the interactive dependency view.

For Mathlib (6 definitions, 133 lemmas, 7 theorems)

• ForMathlib.MeasureTheory.Constructions.Polish.StandardBorel (0 definitions, 1 lemmas, 0 theorems)

• ForMathlib.MeasureTheory.Measurable (0 definitions, 5 lemmas, 0 theorems)

• ForMathlib.MeasureTheory.Measure.AbsolutelyContinuous (0 definitions, 1 lemmas, 0 theorems)

• ForMathlib.MeasureTheory.OuterMeasure.Basic (0 definitions, 1 lemmas, 0 theorems)

• ForMathlib.MeasureTheory.Order.Lattice (0 definitions, 0 lemmas, 1 theorems)

• ForMathlib.MeasureTheory.Order.MeasurableArg (4 definitions, 7 lemmas, 6 theorems)

• ForMathlib.Probability.HasCondDistrib (0 definitions, 11 lemmas, 0 theorems)

• ForMathlib.Probability.Independence.CondDistrib (1 definitions, 36 lemmas, 0 theorems)

• ForMathlib.Probability.Kernel.KernelSub (0 definitions, 15 lemmas, 0 theorems)

• ForMathlib.Probability.Independence.CondIndepFun (0 definitions, 10 lemmas, 0 theorems)

• ForMathlib.Probability.Independence.IndepFun (0 definitions, 8 lemmas, 0 theorems)

• ForMathlib.Probability.Independence.IndepInfinitePi (0 definitions, 2 lemmas, 0 theorems)

• ForMathlib.Probability.Integrable (0 definitions, 1 lemmas, 0 theorems)

• ForMathlib.Probability.Kernel.Basic (0 definitions, 1 lemmas, 0 theorems)

• ForMathlib.Probability.Kernel.Composition.MapComap (0 definitions, 4 lemmas, 0 theorems)

• ForMathlib.Probability.Kernel.Composition.MeasureCompProd (0 definitions, 1 lemmas, 0 theorems)

• ForMathlib.Probability.Kernel.IonescuTulcea.Traj (1 definitions, 11 lemmas, 0 theorems)

• ForMathlib.Probability.Moments.SubGaussian (0 definitions, 9 lemmas, 0 theorems)

• ForMathlib.Probability.WithDensity (0 definitions, 9 lemmas, 0 theorems)

Online (31 definitions, 195 lemmas, 3 theorems)

• Online.Bandit.Algorithms.ETC (2 definitions, 15 lemmas, 1 theorems)

• Online.Bandit.SumRewards (0 definitions, 32 lemmas, 0 theorems)

• Online.Bandit.ArrayProbSpace (9 definitions, 68 lemmas, 0 theorems)

• Online.Bandit.BayesRegret (4 definitions, 13 lemmas, 0 theorems)

• Online.Bandit.Regret (3 definitions, 15 lemmas, 0 theorems)

• Online.Bandit.Algorithms.Regret.BayesRegretTS (2 definitions, 12 lemmas, 1 theorems)

• Online.Bandit.Algorithms.TS (3 definitions, 3 lemmas, 0 theorems)

• Online.Bandit.Algorithms.UCB (5 definitions, 26 lemmas, 1 theorems)

• Online.Bandit.RewardByCountMeasure (3 definitions, 11 lemmas, 0 theorems)

Sequential Learning (51 definitions, 271 lemmas, 1 theorems)

• SequentialLearning.FiniteActions (8 definitions, 95 lemmas, 0 theorems)

• SequentialLearning.Algorithm (11 definitions, 31 lemmas, 0 theorems)

• SequentialLearning.StationaryEnv (4 definitions, 22 lemmas, 0 theorems)

• SequentialLearning.BayesStationaryEnv (4 definitions, 13 lemmas, 0 theorems)

• SequentialLearning.IonescuTulceaSpace (7 definitions, 41 lemmas, 1 theorems)

• SequentialLearning.Algorithms.RoundRobin (2 definitions, 10 lemmas, 0 theorems)

• SequentialLearning.Deterministic (8 definitions, 31 lemmas, 0 theorems)

• SequentialLearning.AlgorithmDensityBayes (0 definitions, 3 lemmas, 0 theorems)

• SequentialLearning.AlgorithmDensity (3 definitions, 3 lemmas, 0 theorems)

• SequentialLearning.Algorithms.Uniform (1 definitions, 1 lemmas, 0 theorems)

• SequentialLearning.Algorithms.RandomSampling (1 definitions, 4 lemmas, 0 theorems)

• SequentialLearning.EvaluationEnv (2 definitions, 17 lemmas, 0 theorems)