-- Formal Statistical Learning Theory in Lean 4
-- All results verified. No stub tactics. No custom axioms.
-- Axioms: [propext, Classical.choice, Quot.sound] only.

import FormalSLT.Risk
import FormalSLT.ERM
import FormalSLT.UniformConvergence
import FormalSLT.GlivenkoCantelli
import FormalSLT.GhostSample

import FormalSLT.Probability.Concentration
import FormalSLT.Probability.FiniteUnionBound
import FormalSLT.Probability.FiniteExpectation
import FormalSLT.Probability.BernsteinMGF
import FormalSLT.Probability.IIDConcentration
import FormalSLT.Probability.BorelCantelli
import FormalSLT.Probability.KolmogorovAxioms
import FormalSLT.Probability.LawOfLargeNumbers
import FormalSLT.Probability.Martingale
import FormalSLT.Probability.MeasureConvergence
import FormalSLT.Probability.Moments

import FormalSLT.LinearAlgebra.CommonInequalities

import FormalSLT.Concentration.SubGamma.BennettBound
import FormalSLT.Concentration.SubGamma.BoundedExpIntegrable
import FormalSLT.Concentration.SubGamma.CondExpProduct
import FormalSLT.Concentration.SubGamma.CondJensen
import FormalSLT.Concentration.SubGamma.CondMarkov
import FormalSLT.Concentration.SubGamma.CondVarianceFromSquare
import FormalSLT.Concentration.SubGamma.Extractor
import FormalSLT.Concentration.SharpMcDiarmid
import FormalSLT.Concentration.HeterogeneousMcDiarmid
import FormalSLT.Concentration.NamedTails
import FormalSLT.Sequential

import FormalSLT.Statistics.Bernoulli
import FormalSLT.Statistics.SampleStatistics
import FormalSLT.Statistics.ClassicalEstimation
import FormalSLT.Statistics.FisherInformation
import FormalSLT.Statistics.CramerRao
import FormalSLT.Statistics.ExponentialFamily
import FormalSLT.Statistics.AsymptoticStatistics

import FormalSLT.Rademacher.FiniteSample
import FormalSLT.Rademacher.FiniteSampleSymmetrization
import FormalSLT.Rademacher.ProbabilityBridge
import FormalSLT.Rademacher.Decoupling
import FormalSLT.Rademacher.RademacherBoundedDifferences
import FormalSLT.Rademacher.Symmetrization
import FormalSLT.Rademacher.Massart
import FormalSLT.Rademacher.HighProbability
import FormalSLT.Rademacher.FiniteClassHighProb
import FormalSLT.Rademacher.UniformDeviation
import FormalSLT.Rademacher.MetricEntropyGeneralization
import FormalSLT.Rademacher.MetricEntropyHighProbability
import FormalSLT.Rademacher.ERMGeneralization
import FormalSLT.Rademacher.Contraction
import FormalSLT.Rademacher.LinearPredictor
import FormalSLT.Rademacher.Localized
import FormalSLT.Rademacher.HighProbRademacher
import FormalSLT.Rademacher.LinearPredictorRademacher
import FormalSLT.Rademacher.RademacherContraction
import FormalSLT.Rademacher.RademacherSymmetrization

import FormalSLT.Azuma.ExposureMartingale
import FormalSLT.Azuma.BoundedDifferences
import FormalSLT.Azuma.BoundedDiffMartingale
import FormalSLT.Azuma.BoundedDiffsAzumaInput
import FormalSLT.Azuma.BoundedIncrementBound
import FormalSLT.Azuma.HasBoundedDifferences
import FormalSLT.Azuma.ExposureIncrementHoeffding
import FormalSLT.Azuma.ExposureIncrementCondMGF
import FormalSLT.Azuma.GenGapTail
import FormalSLT.Azuma.SharpMcDiarmid

import FormalSLT.VC

import FormalSLT.Covering.Rademacher
import FormalSLT.Covering.DudleyChaining
import FormalSLT.Covering.FiniteSubGaussianChaining
import FormalSLT.Probability.SubGaussianFiniteMax
import FormalSLT.Covering.DudleyChainingSum
import FormalSLT.Covering.DudleySumToIntegral
import FormalSLT.Covering.DudleyEntropyIntegral
import FormalSLT.Covering.TotalBoundedDudley
import FormalSLT.Covering.UnitIntervalDudley
import FormalSLT.Covering.TwoPointDudley
import FormalSLT.Covering.TwoPointDudleyIntegral
import FormalSLT.Covering.DudleyToRademacher
import FormalSLT.Covering.ContinuousDudley
import FormalSLT.Covering.ContinuousDudleyCovering
import FormalSLT.Covering.GuardedDudleyIntegral
import FormalSLT.Covering.GuardedContinuousDudley
import FormalSLT.Covering.TotalBoundedDudleyCovering
import FormalSLT.Covering.TotalBoundedMinimalCovering
import FormalSLT.Covering.TotalBoundedDudleySelectedCapstone
import FormalSLT.Covering.TotalBoundedDudleyMinimalCapstone
import FormalSLT.Covering.TotalBoundedDudleyMinimalShift
import FormalSLT.Covering.ContinuousDudleyUnitInterval
import FormalSLT.Covering.ContinuousDudleyUnitIntervalCovering
import FormalSLT.Covering.MeasureDudley
import FormalSLT.Covering.FiniteDiscreteDudley

import FormalSLT.AlgorithmicStability
import FormalSLT.Stability.BousquetElisseeff
import FormalSLT.Stability.RKHSRegularisedERM
import FormalSLT.PACBayes

import FormalSLT.OnlineToPAC.RegretConversion
import FormalSLT.OnlineToPAC.CesaBianchi
import FormalSLT.OnlineToPAC.IIDConcentration

import FormalSLT.Test.PACBayesBernsteinTest
import FormalSLT.Test.SharpMcDiarmidTest

import FormalSLT.TestTimeMeta.Assumptions
import FormalSLT.TestTimeMeta.CompositionLemmas
import FormalSLT.TestTimeMeta.MainTheorem
import FormalSLT.TestTimeMeta.Flagship
import FormalSLT.TestTimeMeta.FlagshipComposition
import FormalSLT.TestTimeMeta.OnlinePopulationDecomposition
import FormalSLT.TestTimeMeta.McAllesterPopulationDecomposition
import FormalSLT.TestTimeMeta.BernsteinPopulationDecomposition
import FormalSLT.TestTimeMeta.FlagshipSimultaneousAssembly
import FormalSLT.TestTimeMeta.BernsteinPopulationDecompositionReal
import FormalSLT.TestTimeMeta.AnytimeVillePopulationDecomposition
import FormalSLT.TestTimeMeta.FlagshipAnytimeValid
import FormalSLT.TestTimeMeta.FlagshipFourComponentAssembly
import FormalSLT.TestTimeMeta.PrefixKernelPopulationDecomposition
import FormalSLT.TestTimeMeta.FlagshipFiveComponentAssembly