Documentation
FormalSLT
Search
return to top
source
Imports
Init
FormalSLT.AlgorithmicStability
FormalSLT.ERM
FormalSLT.GhostSample
FormalSLT.GlivenkoCantelli
FormalSLT.PACBayes
FormalSLT.Risk
FormalSLT.Sequential
FormalSLT.StochasticDynamics
FormalSLT.UniformConvergence
FormalSLT.VC
FormalSLT.AnytimeValid.ForwardPredictableMeanBesselProcess
FormalSLT.AnytimeValid.PredictableVarianceProxy
FormalSLT.Azuma.BoundedDiffMartingale
FormalSLT.Azuma.BoundedDifferences
FormalSLT.Azuma.BoundedDiffsAzumaInput
FormalSLT.Azuma.BoundedIncrementBound
FormalSLT.Azuma.ExposureIncrementCondMGF
FormalSLT.Azuma.ExposureIncrementHoeffding
FormalSLT.Azuma.ExposureMartingale
FormalSLT.Azuma.GenGapTail
FormalSLT.Azuma.HasBoundedDifferences
FormalSLT.Azuma.SharpMcDiarmid
FormalSLT.Concentration.HeterogeneousMcDiarmid
FormalSLT.Concentration.NamedTails
FormalSLT.Concentration.SharpMcDiarmid
FormalSLT.Covering.ContinuousDudley
FormalSLT.Covering.ContinuousDudleyCovering
FormalSLT.Covering.ContinuousDudleyUnitInterval
FormalSLT.Covering.ContinuousDudleyUnitIntervalCovering
FormalSLT.Covering.DudleyChaining
FormalSLT.Covering.DudleyChainingSum
FormalSLT.Covering.DudleyEntropyIntegral
FormalSLT.Covering.DudleySumToIntegral
FormalSLT.Covering.DudleyToRademacher
FormalSLT.Covering.FiniteDiscreteDudley
FormalSLT.Covering.FiniteSubGaussianChaining
FormalSLT.Covering.GuardedContinuousDudley
FormalSLT.Covering.GuardedDudleyIntegral
FormalSLT.Covering.MeasureDudley
FormalSLT.Covering.Rademacher
FormalSLT.Covering.TotalBoundedDudley
FormalSLT.Covering.TotalBoundedDudleyCovering
FormalSLT.Covering.TotalBoundedDudleyMinimalCapstone
FormalSLT.Covering.TotalBoundedDudleyMinimalShift
FormalSLT.Covering.TotalBoundedDudleySelectedCapstone
FormalSLT.Covering.TotalBoundedMinimalCovering
FormalSLT.Covering.TwoPointDudley
FormalSLT.Covering.TwoPointDudleyIntegral
FormalSLT.Covering.UnitIntervalDudley
FormalSLT.LinearAlgebra.CommonInequalities
FormalSLT.OnlineToPAC.CesaBianchi
FormalSLT.OnlineToPAC.IIDConcentration
FormalSLT.OnlineToPAC.RegretConversion
FormalSLT.PACBayes.ForwardPredictableMeanBesselPACBayes
FormalSLT.Probability.BernsteinMGF
FormalSLT.Probability.BorelCantelli
FormalSLT.Probability.Concentration
FormalSLT.Probability.FiniteExpectation
FormalSLT.Probability.FiniteUnionBound
FormalSLT.Probability.IIDConcentration
FormalSLT.Probability.KolmogorovAxioms
FormalSLT.Probability.LawOfLargeNumbers
FormalSLT.Probability.Martingale
FormalSLT.Probability.MeasureConvergence
FormalSLT.Probability.Moments
FormalSLT.Probability.SubGaussianFiniteMax
FormalSLT.Rademacher.Contraction
FormalSLT.Rademacher.Decoupling
FormalSLT.Rademacher.ERMGeneralization
FormalSLT.Rademacher.FiniteClassHighProb
FormalSLT.Rademacher.FiniteSample
FormalSLT.Rademacher.FiniteSampleSymmetrization
FormalSLT.Rademacher.HighProbRademacher
FormalSLT.Rademacher.HighProbability
FormalSLT.Rademacher.LinearPredictor
FormalSLT.Rademacher.LinearPredictorRademacher
FormalSLT.Rademacher.Localized
FormalSLT.Rademacher.Massart
FormalSLT.Rademacher.MetricEntropyGeneralization
FormalSLT.Rademacher.MetricEntropyHighProbability
FormalSLT.Rademacher.ProbabilityBridge
FormalSLT.Rademacher.RademacherBoundedDifferences
FormalSLT.Rademacher.RademacherContraction
FormalSLT.Rademacher.RademacherSymmetrization
FormalSLT.Rademacher.Symmetrization
FormalSLT.Rademacher.UniformDeviation
FormalSLT.Stability.BousquetElisseeff
FormalSLT.Stability.RKHSRegularisedERM
FormalSLT.Statistics.AsymptoticStatistics
FormalSLT.Statistics.Bernoulli
FormalSLT.Statistics.ClassicalEstimation
FormalSLT.Statistics.CramerRao
FormalSLT.Statistics.ExponentialFamily
FormalSLT.Statistics.FisherInformation
FormalSLT.Statistics.SampleStatistics
FormalSLT.StochasticDynamics.EmpiricalStationaryCatalog
FormalSLT.StochasticDynamics.StationaryPoissonContraction
FormalSLT.StochasticDynamics.StationaryPoissonDepthSelection
FormalSLT.StochasticDynamics.StationaryPoissonPACBayes
FormalSLT.StochasticDynamics.TrajectoryEmpiricalBernsteinPACBayes
FormalSLT.StochasticDynamics.TrajectoryEmpiricalBernsteinPACBayesCountable
FormalSLT.Test.PACBayesBernsteinTest
FormalSLT.Test.SharpMcDiarmidTest
FormalSLT.TestTimeMeta.AnytimeVillePopulationDecomposition
FormalSLT.TestTimeMeta.Assumptions
FormalSLT.TestTimeMeta.BernsteinPopulationDecomposition
FormalSLT.TestTimeMeta.BernsteinPopulationDecompositionReal
FormalSLT.TestTimeMeta.CompositionLemmas
FormalSLT.TestTimeMeta.Flagship
FormalSLT.TestTimeMeta.FlagshipAnytimeValid
FormalSLT.TestTimeMeta.FlagshipComposition
FormalSLT.TestTimeMeta.FlagshipFiveComponentAssembly
FormalSLT.TestTimeMeta.FlagshipFourComponentAssembly
FormalSLT.TestTimeMeta.FlagshipSimultaneousAssembly
FormalSLT.TestTimeMeta.MainTheorem
FormalSLT.TestTimeMeta.McAllesterPopulationDecomposition
FormalSLT.TestTimeMeta.OnlinePopulationDecomposition
FormalSLT.TestTimeMeta.PrefixKernelPopulationDecomposition
FormalSLT.Concentration.SubGamma.BennettBound
FormalSLT.Concentration.SubGamma.BoundedExpIntegrable
FormalSLT.Concentration.SubGamma.CondExpProduct
FormalSLT.Concentration.SubGamma.CondJensen
FormalSLT.Concentration.SubGamma.CondMarkov
FormalSLT.Concentration.SubGamma.CondVarianceFromSquare
FormalSLT.Concentration.SubGamma.Extractor
Imported by