PaperFormalizer · Formalized papers
Formalized papers
Estimation of Treatment Effects in Extreme and Unobserved Data
Lean code
A standalone Lake project: the paper's Lean, the toolkit modules it imports, and
Check.lean
.
Check.lean
Papers/TbsExtremeEffects/All.lean
Papers/TbsExtremeEffects/Basic.lean
Papers/TbsExtremeEffects/Helpers/AdaptiveAngularRates.lean
Papers/TbsExtremeEffects/Helpers/AdaptiveEvents.lean
Papers/TbsExtremeEffects/Helpers/AdaptiveExponent.lean
Papers/TbsExtremeEffects/Helpers/AdaptiveIPWMean.lean
Papers/TbsExtremeEffects/Helpers/AdaptiveMean.lean
Papers/TbsExtremeEffects/Helpers/AdaptiveNuisance.lean
Papers/TbsExtremeEffects/Helpers/AdaptiveProduct.lean
Papers/TbsExtremeEffects/Helpers/AdaptiveScoreMean.lean
Papers/TbsExtremeEffects/Helpers/AdaptiveTailCounts.lean
Papers/TbsExtremeEffects/Helpers/AdaptiveTailRates.lean
Papers/TbsExtremeEffects/Helpers/Angular.lean
Papers/TbsExtremeEffects/Helpers/AngularConvergence.lean
Papers/TbsExtremeEffects/Helpers/AngularDual.lean
Papers/TbsExtremeEffects/Helpers/AngularFactor.lean
Papers/TbsExtremeEffects/Helpers/AngularRates.lean
Papers/TbsExtremeEffects/Helpers/ConditionalConsistency.lean
Papers/TbsExtremeEffects/Helpers/ConditionalMoments.lean
Papers/TbsExtremeEffects/Helpers/Count.lean
Papers/TbsExtremeEffects/Helpers/DRAssembly.lean
Papers/TbsExtremeEffects/Helpers/DRAugmentation.lean
Papers/TbsExtremeEffects/Helpers/DRConditionalMean.lean
Papers/TbsExtremeEffects/Helpers/DRMean.lean
Papers/TbsExtremeEffects/Helpers/DRScoreIntegrability.lean
Papers/TbsExtremeEffects/Helpers/EtaDR.lean
Papers/TbsExtremeEffects/Helpers/EtaIPW.lean
Papers/TbsExtremeEffects/Helpers/EvaluationPatternBounds.lean
Papers/TbsExtremeEffects/Helpers/EvaluationTailLaw.lean
Papers/TbsExtremeEffects/Helpers/EvaluationTrainingLaw.lean
Papers/TbsExtremeEffects/Helpers/ExponentError.lean
Papers/TbsExtremeEffects/Helpers/ExponentScore.lean
Papers/TbsExtremeEffects/Helpers/GeneralizedRegressionProjection.lean
Papers/TbsExtremeEffects/Helpers/Hill/Calibration.lean
Papers/TbsExtremeEffects/Helpers/Hill/CappedMoments.lean
Papers/TbsExtremeEffects/Helpers/Hill/Convolution.lean
Papers/TbsExtremeEffects/Helpers/Hill/DensityContinuity.lean
Papers/TbsExtremeEffects/Helpers/Hill/DensityPositivity.lean
Papers/TbsExtremeEffects/Helpers/Hill/Deviation.lean
Papers/TbsExtremeEffects/Helpers/Hill/Exponential.lean
Papers/TbsExtremeEffects/Helpers/Hill/ExponentialLaw.lean
Papers/TbsExtremeEffects/Helpers/Hill/IncrementLaw.lean
Papers/TbsExtremeEffects/Helpers/Hill/LargestSummand.lean
Papers/TbsExtremeEffects/Helpers/Hill/Maximal.lean
Papers/TbsExtremeEffects/Helpers/Hill/NominalDensity.lean
Papers/TbsExtremeEffects/Helpers/Hill/NominalMarginals.lean
Papers/TbsExtremeEffects/Helpers/Hill/NominalProductLaw.lean
Papers/TbsExtremeEffects/Helpers/Hill/NumericalBudget.lean
Papers/TbsExtremeEffects/Helpers/Hill/OracleBias.lean
Papers/TbsExtremeEffects/Helpers/Hill/OracleCutoff.lean
Papers/TbsExtremeEffects/Helpers/Hill/OracleEnvelope.lean
Papers/TbsExtremeEffects/Helpers/Hill/OracleRate.lean
Papers/TbsExtremeEffects/Helpers/Hill/OrderStatistics.lean
Papers/TbsExtremeEffects/Helpers/Hill/OrderedSpacings.lean
Papers/TbsExtremeEffects/Helpers/Hill/PartialMoments.lean
Papers/TbsExtremeEffects/Helpers/Hill/Partition.lean
Papers/TbsExtremeEffects/Helpers/Hill/QuantileConstruction.lean
Papers/TbsExtremeEffects/Helpers/Hill/QuantileContinuity.lean
Papers/TbsExtremeEffects/Helpers/Hill/QuantileDerivative.lean
Papers/TbsExtremeEffects/Helpers/Hill/QuantileLower.lean
Papers/TbsExtremeEffects/Helpers/Hill/RadialTail.lean
Papers/TbsExtremeEffects/Helpers/Hill/RemainderMoments.lean
Papers/TbsExtremeEffects/Helpers/Hill/Renyi.lean
Papers/TbsExtremeEffects/Helpers/Hill/Selection.lean
Papers/TbsExtremeEffects/Helpers/Hill/Slice.lean
Papers/TbsExtremeEffects/Helpers/Hill/SortedDensity.lean
Papers/TbsExtremeEffects/Helpers/Hill/SpacingAverage.lean
Papers/TbsExtremeEffects/Helpers/Hill/SpacingJacobian.lean
Papers/TbsExtremeEffects/Helpers/Hill/SpacingProcess.lean
Papers/TbsExtremeEffects/Helpers/Hill/SurvivalCoordinate.lean
Papers/TbsExtremeEffects/Helpers/Hill/SurvivalFromDensity.lean
Papers/TbsExtremeEffects/Helpers/Hill/SurvivalLaw.lean
Papers/TbsExtremeEffects/Helpers/Hill/TailCalibration.lean
Papers/TbsExtremeEffects/Helpers/Hill/TailDerivative.lean
Papers/TbsExtremeEffects/Helpers/Hill/TailRatio.lean
Papers/TbsExtremeEffects/Helpers/Hill/Threshold.lean
Papers/TbsExtremeEffects/Helpers/Hill/VonMises.lean
Papers/TbsExtremeEffects/Helpers/HillRate.lean
Papers/TbsExtremeEffects/Helpers/HomogeneityError.lean
Papers/TbsExtremeEffects/Helpers/IPWMean.lean
Papers/TbsExtremeEffects/Helpers/IPWOutcomeMean.lean
Papers/TbsExtremeEffects/Helpers/JointRectangles.lean
Papers/TbsExtremeEffects/Helpers/JointScoreMeans.lean
Papers/TbsExtremeEffects/Helpers/JointScoreSampling.lean
Papers/TbsExtremeEffects/Helpers/JointTailLaw.lean
Papers/TbsExtremeEffects/Helpers/JointWeakLimit.lean
Papers/TbsExtremeEffects/Helpers/LocalizedThresholdEnvelope.lean
Papers/TbsExtremeEffects/Helpers/OutcomeConditioning.lean
Papers/TbsExtremeEffects/Helpers/ParetoRadial.lean
Papers/TbsExtremeEffects/Helpers/Potter.lean
Papers/TbsExtremeEffects/Helpers/PotterTwo.lean
Papers/TbsExtremeEffects/Helpers/ProductAssembly.lean
Papers/TbsExtremeEffects/Helpers/ProductBounds.lean
Papers/TbsExtremeEffects/Helpers/ProductJointSampling.lean
Papers/TbsExtremeEffects/Helpers/ProductSimplification.lean
Papers/TbsExtremeEffects/Helpers/RateAssembly.lean
Papers/TbsExtremeEffects/Helpers/RegressionPositivity.lean
Papers/TbsExtremeEffects/Helpers/RegularVariation.lean
Papers/TbsExtremeEffects/Helpers/RelabelledIID.lean
Papers/TbsExtremeEffects/Helpers/ScoreEnergy.lean
Papers/TbsExtremeEffects/Helpers/ScoreIntegrability.lean
Papers/TbsExtremeEffects/Helpers/ScoreMeasurability.lean
Papers/TbsExtremeEffects/Helpers/ScoreMoments.lean
Papers/TbsExtremeEffects/Helpers/ScoreSampling.lean
Papers/TbsExtremeEffects/Helpers/Split.lean
Papers/TbsExtremeEffects/Helpers/SplitIndependence.lean
Papers/TbsExtremeEffects/Helpers/TailConditionalMean.lean
Papers/TbsExtremeEffects/Helpers/TailIntegrals.lean
Papers/TbsExtremeEffects/Helpers/TailInterpolation.lean
Papers/TbsExtremeEffects/Helpers/TailRegressionProjection.lean
Papers/TbsExtremeEffects/Helpers/TailRegressionSections.lean
Papers/TbsExtremeEffects/Helpers/TailSurvival.lean
Papers/TbsExtremeEffects/Helpers/TailTreatment.lean
Papers/TbsExtremeEffects/Helpers/ThresholdBand.lean
Papers/TbsExtremeEffects/Helpers/ThresholdCountable.lean
Papers/TbsExtremeEffects/Helpers/ThresholdGhost.lean
Papers/TbsExtremeEffects/Helpers/ThresholdLocalization.lean
Papers/TbsExtremeEffects/Helpers/ThresholdMaximalEvents.lean
Papers/TbsExtremeEffects/Helpers/ThresholdPrefixes.lean
Papers/TbsExtremeEffects/Helpers/ThresholdSampling.lean
Papers/TbsExtremeEffects/Helpers/ThresholdSignedMoments.lean
Papers/TbsExtremeEffects/Helpers/TrainingScore.lean
Papers/TbsExtremeEffects/Helpers/TrainingThresholdGhost.lean
Papers/TbsExtremeEffects/Helpers/TruncatedJointLimit.lean
Papers/TbsExtremeEffects/Helpers/UnweightedRegressionProjection.lean
Papers/TbsExtremeEffects/Helpers/WeightedContrast.lean
Papers/TbsExtremeEffects/Helpers/WeightedRegressionProjection.lean
Papers/TbsExtremeEffects/Helpers.lean
Papers/TbsExtremeEffects/Setup/Algorithm.lean
Papers/TbsExtremeEffects/Setup/Model.lean
Papers/TbsExtremeEffects/Setup/TailModel.lean
Papers/TbsExtremeEffects/TCorRate.lean
Papers/TbsExtremeEffects/TCorRateIpw.lean
Papers/TbsExtremeEffects/TId.lean
Papers/TbsExtremeEffects/TRate.lean
Papers/TbsExtremeEffects.lean
Papers.lean
README.md
Toolkit/Foundations/Probability/Concentration/ChernoffBounds.lean
Toolkit/Foundations/Probability/Concentration/ExponentialSupermartingale.lean
Toolkit/Foundations/Probability/Conditioning/ConditionalIntegrability.lean
Toolkit/Foundations/Probability/Conditioning/ConditioningOnEvent.lean
Toolkit/Foundations/Probability/Conditioning/JoinFactorization.lean
Toolkit/Foundations/Probability/Distributions/DescendingOrderStatistics.lean
Toolkit/Foundations/Probability/Distributions/DescendingSortMeasure.lean
Toolkit/Foundations/Probability/Distributions/ExponentialOrderedDensity.lean
Toolkit/Foundations/Probability/Distributions/ExponentialSpacings.lean
Toolkit/Foundations/Probability/Distributions/NormalizedSpacingMap.lean
Toolkit/Foundations/Probability/Distributions/SurvivalTransform.lean
Toolkit/Foundations/Probability/Independence/Conditioning.lean
Toolkit/Foundations/Probability/Independence/ProductConditioning.lean
Toolkit.lean
built-against.json
lakefile.toml
lean-toolchain
vendor/StatLean/LICENSE
vendor/StatLean/LICENSES/formal-learning-theory-kernel-Apache-2.0.txt
vendor/StatLean/StatLean/AsymptoticStatistics/Asymptotics/Discharge/LeastFavorable.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Asymptotics/Discharge/LeastFavorableVec.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Asymptotics/Discharge/OneStep.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Asymptotics/Discharge/OneStepVec.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Asymptotics/Discharge/WeightedScoreEmpiricalLinearization.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Asymptotics/Discharge/ZEstimator.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Asymptotics/Discharge/ZEstimatorBiasExpansion.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Asymptotics/Discharge/ZEstimatorBiasExpansionVec.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Asymptotics/Discharge/ZEstimatorBiasResidual.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Asymptotics/Discharge/ZEstimatorBiasResidualExplicit.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Asymptotics/Discharge/ZEstimatorBiasResidualVdVFaithful.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Asymptotics/Discharge/ZEstimatorBiasResidualVec.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Asymptotics/Discharge/ZEstimatorEmpiricalReplacement.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Asymptotics/Discharge/ZEstimatorModelShift.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Asymptotics/Discharge/ZEstimatorVec.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Asymptotics/Discharge/ZEstimatorVecNative.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Asymptotics/LAN/BayesLanLimit/PosteriorWeights.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Asymptotics/LeastFavorable.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Asymptotics/LeastFavorableVec.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Asymptotics/OneStep.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Asymptotics/OneStepVec.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Asymptotics/ZEstimator.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Asymptotics/ZEstimatorVec.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ClassicalZEstimator/AsymptoticNormality.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ClassicalZEstimator/ExistenceAndNormality.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ClassicalZEstimator/GradientLocalMax.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ClassicalZEstimator/NonlinearWitness.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ClassicalZEstimator/RootExistence.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ClassicalZEstimator/TaylorDomination.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ClassicalZEstimator/Witness.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Consistency/OneDimContinuousConsistency.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Consistency/OneDimMonotoneConsistency.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Consistency/UniformConsistency.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Consistency/WaldCompactAvoidance.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Consistency/WaldConsistency.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Core/BoundedLinearFunctional.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Core/CandidateIF.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Core/EIF.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Core/EIFVec.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Core/EfficiencyOperational.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Core/EfficiencyOperationalVec.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Core/Hilbert.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Core/LinearFunctional.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Core/MassMethod.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Core/NondominatedEfficiencyOperational.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Core/NondominatedPathwise.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Core/NondominatedQMDPath.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Core/NondominatedQMDProductComparison.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Core/NondominatedTangent.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Core/Pathwise.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Core/PathwiseVec.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Core/QMDPath.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Core/TangentAbstract.lean
vendor/StatLean/StatLean/AsymptoticStatistics/DQM/Defs.lean
vendor/StatLean/StatLean/AsymptoticStatistics/DQM/LogDensity.lean
vendor/StatLean/StatLean/AsymptoticStatistics/DQM/LogDensityPopulationTaylor.lean
vendor/StatLean/StatLean/AsymptoticStatistics/DQM/MovingDirection.lean
vendor/StatLean/StatLean/AsymptoticStatistics/DQM/ParameterSubset.lean
vendor/StatLean/StatLean/AsymptoticStatistics/DQM/Properties.lean
vendor/StatLean/StatLean/AsymptoticStatistics/DQM/SqrtDensityRatio.lean
vendor/StatLean/StatLean/AsymptoticStatistics/DQM/ZeroDensity.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Efficiency/ConvexLinearEfficiency.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Efficiency/HajekLeCamConvolution.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Efficiency/LocalAsymptoticMinimax.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Efficiency/LowerBoundForExperiments.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/AbstractDonsker/BracketingDonsker.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/AbstractDonsker/BrownianBridge.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/AbstractDonsker/Carrier.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/AbstractDonsker/Characterization.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/AbstractDonsker/DonskerProcessData.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/AbstractDonsker/EquicontTightness.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/AbstractDonsker/FiniteCarrier.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/AbstractDonsker/GPNet.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/AbstractDonsker/GPProcess.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/AbstractDonsker/JointInfluenceBridge.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/AbstractDonsker/JointInfluenceCoordinates.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/AbstractDonsker/JointInfluenceGaussianExtension.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/AbstractDonsker/NecessityTightness.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/AbstractDonsker/PBridgeTight.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/AbstractDonsker/SufficiencyDiscretization.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/Bracketing.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/BracketingBounded.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/BracketingMaximalGeneral.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/ChainingAssembly.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/ChangingClassCore.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/ChangingClassFiniteGaussian.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/ChangingClassMarginal.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/ChangingClassOuterCLT.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/ChangingClassUniform.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/ChangingClassUniformAEC.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/ChangingClassUniformPartitionAEC.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/ChangingClassUniformProcess.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/ChangingClassUniformRadius.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/ChangingLindeberg.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/Donsker.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/DonskerBracketing.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/EmpiricalDistribution.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/EmpiricalMeasure.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/EmpiricalProcess.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/EmpiricalSquareRadius.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/EquicontinuityChaining.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/FunctionClass.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/GlivenkoCantelli.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/GoodnessOfFit.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/HalfLineBracketing.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/HalfLineBridgeTransport.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/HalfLineIndicators.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/HalfLineQuantile.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/IIDChebyshev.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/IIDFiniteRestriction.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/InfiniteDimZEstimator.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/LinearizationEquicontinuity.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/LinearizationModulus.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/LipschitzShellModulus.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/LocalizedClass.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/LocalizedEmpiricalRadiusAsymptotics.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/LocalizedEmpiricalSquareRadius.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/LocalizedPointwiseDense.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/LocalizedRelativeRadius.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/Maximal.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/MaximalBernstein.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/MaximalBoundedChaining.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/MaximalFullChaining.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/MaximalOrlicz.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/NestedPartition.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/OuterPeeling.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/OuterProbAsymptotics.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/ParameterEstimation.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/ParameterEstimationProcess.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/ParametricClassDonsker.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/PointwiseDense.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/RandomFunctions.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/SupMeasurability.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/TriangularLindeberg.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/UniformCovering.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/UniformCoveringBook.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/UniformCoveringBookDifference.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/UniformCoveringBookMaximal.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/UniformCoveringExtraction.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/UniformCoveringMeasurability.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/UniformCoveringOuterMaximal.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/UniformCoveringRademacher.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/UniformCoveringRademacherContraction.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/UniformCoveringRademacherFiniteChaining.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/UniformCoveringSymmetrization.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/UniformEntropyBracketingTransfer.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/UniformEntropyChaining.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/UniformEntropyGaussianBridge.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/UniformEntropyLimitAssembly.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/UniformEntropyLimitTheorems.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/UniformEntropyMaximal.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/UniformEntropyStructural.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/UniformEntropySymmetrization.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/UniformRandomFunctions.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/VCClass.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/VCSharpCoveringTransfer.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/VCSharpFiniteCovering.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/VCSharpPacking.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/VCUniformEntropy.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/VCUniformEntropyAssembly.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/ZEstimatorNormality.lean
vendor/StatLean/StatLean/AsymptoticStatistics/EmpiricalProcess/ZEstimatorNuisance.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Examples/EmpiricalDistribution/Model.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Examples/MARMean/EIF.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Examples/MARMean/Model.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Examples/MARMean/Tangent.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Examples/Regression/EIF.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Examples/Regression/Model.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Examples/ScoreOperatorDenseRange.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Examples/SymmetricLocation/EIF.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Examples/SymmetricLocation/Model.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Examples/Template.md
vendor/StatLean/StatLean/AsymptoticStatistics/Experiment/EquivariantInLaw.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Experiment/FiniteRiskCompactification.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Experiment/GaussianShift.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Experiment/GaussianShiftConvolution.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Experiment/GaussianShiftMinimax.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Experiment/KernelRealization.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Experiment/LeCamRepresentation.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Experiment/RandomizedStatistic.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/AnalyticSetCapacitability.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/Anderson.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/AntitoneDiagonal.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/AntitoneLintegral.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/BivariateMGFUniqueness.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/BowlShaped.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/Brunn1D.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/CharFnConvolution.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/ChoquetCapacity/Analytic.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/ChoquetCapacity/Basic.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/CondExpCauchySchwarz.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/CondExpCompProd.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/CondExpL2.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/ConditionalQMD.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/Contiguity.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/ContiguityIntegralComparison.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/CramerWoldAux.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/CramerWoldEuclidean.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/CramerWoldWeakConverges.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/DeltaMethod.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/DiagonalSubseqLimSupFinset.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/DifferentiableInProbability.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/EmpiricalAverage.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/FiniteProductLikelihood.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/GaussianMGF.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/GaussianRealTV.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/GaussianShift.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/GaussianTiltRigidity.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/GaussianVarCharFn.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/GaussianVarianceMono.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/HellingerIntegralBound.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/HellingerProduct.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/IIdJointLaw.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/IdentityTheoremMulti.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/IidOneSidedLLN.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/IidWLLN.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/InProbability.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/IndepWeakLimit.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/IntegrableTail.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/JointMGF.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/L2.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/L2Asymptotics.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/L2Tail.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/LevyMpassVec.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/LogTaylor.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/LogTaylorIntegral.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/LpDominatedConvergence.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/Markov.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/MarkovKernelProhorov.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/MassMethodUtilities.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/MatrixInProbability.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/MeanVarConvergence.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/MeasurableCountableRange.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/MeasurableSelection.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/MeasurableSelectionRandomFunctions.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/MultivariateCLT.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/MultivariateComplexMGF.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/MultivariateComplexMGFCoeff.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/MultivariateGaussianConv.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/MultivariateGaussianDensity.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/MultivariateGaussianSmul.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/MultivariateGaussianWeakLimit.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/OneSidedExpectation.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/OuterIntegration/OuterExpectation.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/PairwiseQMDAnalytic.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/PiGaussian.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/PiWithDensity.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/PortmanteauLscBridge.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/PosDefCoercivity.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/PrekopaLeindler.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/Probability/GaussianChaining.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/Probability/GaussianL2Closure.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/Probability/GaussianMaximal.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/Probability/IsonormalProcess.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/Probability/Rademacher.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/Probability/RademacherClippedSquare.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/Probability/RademacherContraction.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/Probability/SubgaussianGaussian.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/Prohorov.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/QMDAnalytic.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/RandomRadiusEntropy.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/RnDerivSqrt.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/SecondOrderCalculus.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/SetConvergence.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/SigmaFiniteTrimComap.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/Slutsky.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/SlutskyFrechetShift.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/SlutskyVec.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/SplitProductMoments.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/SqrtLogIntegral.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/SqrtLogProduct.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/SubsequenceLimit.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/TendstoInMeasureAlgebra.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/UpperSemicontinuousEnvelope.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/VarianceOfConvolution.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/VaryingSetSupremum.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/WeakConvergence/Outer.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/WeakConvergence/OuterFiniteProduct.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/WeakConvergence/OuterMapping.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/WeakConvergence/OuterProcessMapping.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/WeakConvergence/OuterSlutsky.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/WeakConvergence/OuterTightness.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/WeakConvergence/TightCoordinateUniqueness.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ForMathlib/WellSeparatedMaximum.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LocalAsymptoticNormality/AsymptoticRepresentation.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LocalAsymptoticNormality/LANExpansion.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LocalAsymptoticNormality/LocalContiguity.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LocalAsymptoticNormality/MovingLAN.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LocalAsymptoticNormality/MovingProductLikelihood.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/AndersonBayes.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/BasisFromProjSeq.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/BayesRiskLeCamClosure.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/BayesRiskLowerBound.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/BowlShapedUCApprox.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/Convolution.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/ConvolutionUnbounded.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/ConvolutionUnboundedVec.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/ConvolutionVec.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/FinDimSubmodel.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/GaussianConeBayes.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/GaussianConeMinimax.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/GaussianConePrior.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/GaussianConeQuantization.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/GaussianShiftMinimax.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/LAM.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/LAMCanonicalAlign.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/LAMLinearFromCone.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/LAMSemiparametricBridge.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/LAMSemiparametricCone.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/LAMSemiparametricUnbounded.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/LAMUnboundedBridge.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/LAMUnboundedRecenter.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/LeCamThirdAndCharFn.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/NondominatedFiniteExperimentMinimax.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/NondominatedOperationalEfficiencyAnalytic.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/OperationalEfficiencyCharacterization.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/OperationalEfficiencyCharacterizationNondominated.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/OperationalEfficiencyCharacterizationVecNondominated.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/ParametricBridge.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/ProjSeqToEif.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/RegularEstimator.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/RegularEstimatorDerivations.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/RegularEstimatorNarrow.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/RegularEstimatorNarrowCommonDom.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/RegularEstimatorNarrowLinear.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/RegularEstimatorNarrowReverse.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/RegularEstimatorNarrowReverseUncond.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/RegularEstimatorVec.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/RegularEstimatorVecReverse.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/ScoreOperatorRegularityObstruction.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/SubconvexApprox.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/T6_FinDimLAN/Abstract1DLAN.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/T6_FinDimLAN/CLTinf.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/T6_FinDimLAN/JointLAN.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/T6_FinDimLAN/LANexpansion.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/T6_FinDimLAN/NondominatedQMDLAN.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/T6_FinDimLAN/NondominatedQMDLeCamThird.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/T6_FinDimLAN/QMDPath1DLAN.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/T6_FinDimLAN/QMDScoreLAN.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/T6_FinDimLAN/Synthesis.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/T7_AndersonClosure/JointLRWeakConverges.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/T7_AndersonClosure/LRFactorization.lean
vendor/StatLean/StatLean/AsymptoticStatistics/LowerBounds/UnboundedSubmodelQMDPath.lean
vendor/StatLean/StatLean/AsymptoticStatistics/MEstimator/Argmax.lean
vendor/StatLean/StatLean/AsymptoticStatistics/MEstimator/ArgmaxContinuous.lean
vendor/StatLean/StatLean/AsymptoticStatistics/MEstimator/ArgmaxLocalization.lean
vendor/StatLean/StatLean/AsymptoticStatistics/MEstimator/AsymptoticNormality.lean
vendor/StatLean/StatLean/AsymptoticStatistics/MEstimator/DifferentiabilityInProbability.lean
vendor/StatLean/StatLean/AsymptoticStatistics/MEstimator/MEstimatorNormality.lean
vendor/StatLean/StatLean/AsymptoticStatistics/MEstimator/MetricRate.lean
vendor/StatLean/StatLean/AsymptoticStatistics/MEstimator/NuisanceRate.lean
vendor/StatLean/StatLean/AsymptoticStatistics/MEstimator/Rate.lean
vendor/StatLean/StatLean/AsymptoticStatistics/MaximumLikelihood/AsymptoticNormality.lean
vendor/StatLean/StatLean/AsymptoticStatistics/MaximumLikelihood/AsymptoticNormalityOn.lean
vendor/StatLean/StatLean/AsymptoticStatistics/MaximumLikelihood/Consistency.lean
vendor/StatLean/StatLean/AsymptoticStatistics/MaximumLikelihood/FisherAdapters.lean
vendor/StatLean/StatLean/AsymptoticStatistics/MaximumLikelihood/Likelihood.lean
vendor/StatLean/StatLean/AsymptoticStatistics/MaximumLikelihood/ParameterSubset.lean
vendor/StatLean/StatLean/AsymptoticStatistics/MaximumLikelihood/ProductComparisons.lean
vendor/StatLean/StatLean/AsymptoticStatistics/MomentEstimator/MethodOfMoments.lean
vendor/StatLean/StatLean/AsymptoticStatistics/OneStepEstimator/AsymptoticExpansion.lean
vendor/StatLean/StatLean/AsymptoticStatistics/OneStepEstimator/Discretization.lean
vendor/StatLean/StatLean/AsymptoticStatistics/OneStepEstimator/Linearization.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Operators/CAR.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Operators/CARScores.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Operators/CoarsenedQMD.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Operators/CoarsenedQMDLimit.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Operators/CoarseningScoreIdentification.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Operators/CompleteCaseIPW.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Operators/InformationLoss.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Operators/ScoreOperator.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ParametricFamily/BartlettIdentity.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ParametricFamily/CARScore.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ParametricFamily/Defs.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ParametricFamily/FisherInformation.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ParametricFamily/KullbackLeibler.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ParametricFamily/ParameterSubset.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ParametricFamily/RegularEstimator.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ParametricFamily/Score.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ParametricFamily/ScoreCLT.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ParametricFamily/SqrtDensityRatio.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ParametricFamily/SubmodelDQM.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ParametricFamily/SubmodelFromScores.lean
vendor/StatLean/StatLean/AsymptoticStatistics/ParametricFamily/UnboundedSubmodel.lean
vendor/StatLean/StatLean/AsymptoticStatistics/Probability/ScoreCLT.lean
vendor/StatLean/StatLean/AsymptoticStatistics/StrictModel/EfficientScore.lean
vendor/StatLean/StatLean/AsymptoticStatistics/StrictModel/EfficientScoreChosenPathsVec.lean
vendor/StatLean/StatLean/AsymptoticStatistics/StrictModel/EfficientScoreVec.lean
vendor/StatLean/StatLean/AsymptoticStatistics/StrictModel/MatrixBartlett.lean
vendor/StatLean/StatLean/AsymptoticStatistics/StrictModel/MatrixInfluenceEIF.lean
vendor/StatLean/StatLean/AsymptoticStatistics.lean
vendor/StatLean/StatLean/Bayesian/BayesEstimators/ArgminConsistency.lean
vendor/StatLean/StatLean/Bayesian/BayesEstimators/Defs.lean
vendor/StatLean/StatLean/Bayesian/BayesEstimators/PointEstimatorLimits.lean
vendor/StatLean/StatLean/Bayesian/BayesEstimators/PosteriorTails.lean
vendor/StatLean/StatLean/Bayesian/BayesEstimators/UniformApproximation.lean
vendor/StatLean/StatLean/Bayesian/BernsteinVonMises/Basic.lean
vendor/StatLean/StatLean/Bayesian/BernsteinVonMises/Defs.lean
vendor/StatLean/StatLean/Bayesian/BernsteinVonMises/EfficientCentering.lean
vendor/StatLean/StatLean/Bayesian/BernsteinVonMises/ExponentialTests.lean
vendor/StatLean/StatLean/Bayesian/BernsteinVonMises/LocalApproximation.lean
vendor/StatLean/StatLean/Bayesian/BernsteinVonMises/MixtureContiguity.lean
vendor/StatLean/StatLean/Bayesian/BernsteinVonMises/PosteriorConcentration.lean
vendor/StatLean/StatLean/Bayesian/BernsteinVonMises/PosteriorNormality.lean
vendor/StatLean/StatLean/Bayesian/BernsteinVonMises/PriorSmallBall.lean
vendor/StatLean/StatLean/Bayesian/BernsteinVonMises/ScoreTest.lean
vendor/StatLean/StatLean/Bayesian/BernsteinVonMises/TestBoost.lean
vendor/StatLean/StatLean/Bayesian/Cond/Defs.lean
vendor/StatLean/StatLean/Bayesian/Cond/FinitePartition.lean
vendor/StatLean/StatLean/Bayesian/Cond/Odds.lean
vendor/StatLean/StatLean/Bayesian/Conjugacy/BetaBernoulli.lean
vendor/StatLean/StatLean/Bayesian/Conjugacy/BetaBinomial.lean
vendor/StatLean/StatLean/Bayesian/Conjugacy/Criterion.lean
vendor/StatLean/StatLean/Bayesian/Conjugacy/Defs.lean
vendor/StatLean/StatLean/Bayesian/Conjugacy/DirichletMultinomial.lean
vendor/StatLean/StatLean/Bayesian/Conjugacy/ExpFamily.lean
vendor/StatLean/StatLean/Bayesian/Conjugacy/GammaPoisson.lean
vendor/StatLean/StatLean/Bayesian/Conjugacy/NormalNormal.lean
vendor/StatLean/StatLean/Bayesian/Decision/BayesEstimator.lean
vendor/StatLean/StatLean/Bayesian/Decision/Defs.lean
vendor/StatLean/StatLean/Bayesian/Decision/Minimax.lean
vendor/StatLean/StatLean/Bayesian/Decision/SquaredLoss.lean
vendor/StatLean/StatLean/Bayesian/Decision/ZeroOneLoss.lean
vendor/StatLean/StatLean/Bayesian/DirichletLaplace/CompressEngine.lean
vendor/StatLean/StatLean/Bayesian/DirichletLaplace/CoordinateSplit.lean
vendor/StatLean/StatLean/Bayesian/DirichletLaplace/CoveringNets.lean
vendor/StatLean/StatLean/Bayesian/DirichletLaplace/Defs.lean
vendor/StatLean/StatLean/Bayesian/DirichletLaplace/DenominatorLowerBound.lean
vendor/StatLean/StatLean/Bayesian/DirichletLaplace/DensityBounds.lean
vendor/StatLean/StatLean/Bayesian/DirichletLaplace/GaussianTests.lean
vendor/StatLean/StatLean/Bayesian/DirichletLaplace/MarginalDensity.lean
vendor/StatLean/StatLean/Bayesian/DirichletLaplace/NormalMeansModel.lean
vendor/StatLean/StatLean/Bayesian/DirichletLaplace/PosteriorCompressibility.lean
vendor/StatLean/StatLean/Bayesian/DirichletLaplace/PosteriorContraction.lean
vendor/StatLean/StatLean/Bayesian/DirichletLaplace/PriorDensityBounds.lean
vendor/StatLean/StatLean/Bayesian/DirichletLaplace/PriorMassRatio.lean
vendor/StatLean/StatLean/Bayesian/DirichletLaplace/PriorSmallBall.lean
vendor/StatLean/StatLean/Bayesian/DirichletLaplace/ShellDecomposition.lean
vendor/StatLean/StatLean/Bayesian/DirichletLaplace/TestingBound.lean
vendor/StatLean/StatLean/Bayesian/Dominated/Defs.lean
vendor/StatLean/StatLean/Bayesian/Dominated/PosteriorDensity.lean
vendor/StatLean/StatLean/Bayesian/Dominated/PosteriorLintegral.lean
vendor/StatLean/StatLean/Bayesian/Dominated/PredictiveDensity.lean
vendor/StatLean/StatLean/Bayesian/DoobConsistency/Accessible.lean
vendor/StatLean/StatLean/Bayesian/DoobConsistency/Basic.lean
vendor/StatLean/StatLean/Bayesian/DoobConsistency/Defs.lean
vendor/StatLean/StatLean/Bayesian/DoobConsistency/PosteriorConsistency.lean
vendor/StatLean/StatLean/Bayesian/DoobConsistency/PosteriorMartingale.lean
vendor/StatLean/StatLean/Bayesian/EmpiricalBayes/Compound.lean
vendor/StatLean/StatLean/Bayesian/EmpiricalBayes/Defs.lean
vendor/StatLean/StatLean/Bayesian/EmpiricalBayes/LocalFDR.lean
vendor/StatLean/StatLean/Bayesian/EmpiricalBayes/NPMLE.lean
vendor/StatLean/StatLean/Bayesian/EmpiricalBayes/Parametric.lean
vendor/StatLean/StatLean/Bayesian/EmpiricalBayes/Robbins.lean
vendor/StatLean/StatLean/Bayesian/EmpiricalBayes/Tweedie.lean
vendor/StatLean/StatLean/Bayesian/Experiment/Basic.lean
vendor/StatLean/StatLean/Bayesian/Experiment/Defs.lean
vendor/StatLean/StatLean/Bayesian/ForMathlib/BindWithDensity.lean
vendor/StatLean/StatLean/Bayesian/ForMathlib/DirichletDist.lean
vendor/StatLean/StatLean/Bayesian/ForMathlib/ExpOfRealCalc.lean
vendor/StatLean/StatLean/Bayesian/ForMathlib/GammaBounds.lean
vendor/StatLean/StatLean/Bayesian/ForMathlib/GaussianDeriv.lean
vendor/StatLean/StatLean/Bayesian/ForMathlib/GaussianShift.lean
vendor/StatLean/StatLean/Bayesian/ForMathlib/GaussianTV.lean
vendor/StatLean/StatLean/Bayesian/ForMathlib/IIDKernel.lean
vendor/StatLean/StatLean/Bayesian/ForMathlib/IIDSeqKernel.lean
vendor/StatLean/StatLean/Bayesian/ForMathlib/KernelMixture.lean
vendor/StatLean/StatLean/Bayesian/ForMathlib/LaplaceDist.lean
vendor/StatLean/StatLean/Bayesian/ForMathlib/MultinomialDist.lean
vendor/StatLean/StatLean/Bayesian/ForMathlib/PiKernel.lean
vendor/StatLean/StatLean/Bayesian/ForMathlib/PiLintegralFintype.lean
vendor/StatLean/StatLean/Bayesian/ForMathlib/PiWithDensity.lean
vendor/StatLean/StatLean/Bayesian/ForMathlib/TVDist.lean
vendor/StatLean/StatLean/Bayesian/GeneralizedBayes/Basic.lean
vendor/StatLean/StatLean/Bayesian/GeneralizedBayes/Defs.lean
vendor/StatLean/StatLean/Bayesian/GeneralizedBayes/FlatNormal.lean
vendor/StatLean/StatLean/Bayesian/Hierarchical/Decomposition.lean
vendor/StatLean/StatLean/Bayesian/Hierarchical/Defs.lean
vendor/StatLean/StatLean/Bayesian/Hierarchical/Exchangeable.lean
vendor/StatLean/StatLean/Bayesian/Hierarchical/Gibbs.lean
vendor/StatLean/StatLean/Bayesian/Hierarchical/NormalHier.lean
vendor/StatLean/StatLean/Bayesian/Hierarchical/Shrinkage.lean
vendor/StatLean/StatLean/Bayesian/Hierarchical/Tower.lean
vendor/StatLean/StatLean/Bayesian/MCMC/Defs.lean
vendor/StatLean/StatLean/Bayesian/MCMC/Gibbs.lean
vendor/StatLean/StatLean/Bayesian/MCMC/MetropolisHastings.lean
vendor/StatLean/StatLean/Bayesian/MCMC/RaoBlackwell.lean
vendor/StatLean/StatLean/Bayesian/ModelChoice/Basic.lean
vendor/StatLean/StatLean/Bayesian/ModelChoice/CredibleSet.lean
vendor/StatLean/StatLean/Bayesian/ModelChoice/Defs.lean
vendor/StatLean/StatLean/Bayesian/ModelChoice/Testing.lean
vendor/StatLean/StatLean/Bayesian/Sufficiency/Defs.lean
vendor/StatLean/StatLean/Bayesian/Sufficiency/Factorization.lean
vendor/StatLean/StatLean/Bayesian/Updating/Defs.lean
vendor/StatLean/StatLean/Bayesian/Updating/IID.lean
vendor/StatLean/StatLean/Bayesian/Updating/Predictive.lean
vendor/StatLean/StatLean/Bayesian/Updating/Sequential.lean
vendor/StatLean/StatLean/Bayesian.lean
vendor/StatLean/StatLean/CausalInference/Core/FiniteDefs.lean
vendor/StatLean/StatLean/CausalInference/Core/FinitePopulation.lean
vendor/StatLean/StatLean/CausalInference/Core/PopulationDefs.lean
vendor/StatLean/StatLean/CausalInference/ForMathlib/CondAlgebra.lean
vendor/StatLean/StatLean/CausalInference/IV/ComplianceTypes.lean
vendor/StatLean/StatLean/CausalInference/IV/Defs.lean
vendor/StatLean/StatLean/CausalInference/IV/InstrumentalInequalities.lean
vendor/StatLean/StatLean/CausalInference/IV/LATE.lean
vendor/StatLean/StatLean/CausalInference/IV/LinearIV.lean
vendor/StatLean/StatLean/CausalInference/Observational/AIPW.lean
vendor/StatLean/StatLean/CausalInference/Observational/ATT.lean
vendor/StatLean/StatLean/CausalInference/Observational/IPW.lean
vendor/StatLean/StatLean/CausalInference/Observational/Ignorability.lean
vendor/StatLean/StatLean/CausalInference/Observational/Matching.lean
vendor/StatLean/StatLean/CausalInference/Observational/PropensityScore.lean
vendor/StatLean/StatLean/CausalInference/Observational/SelectionBias.lean
vendor/StatLean/StatLean/CausalInference/Observational/Standardization.lean
vendor/StatLean/StatLean/CausalInference/Observational/Subclassification.lean
vendor/StatLean/StatLean/CausalInference/Observational/Trimming.lean
vendor/StatLean/StatLean/CausalInference/Randomized/CompleteRandomization.lean
vendor/StatLean/StatLean/CausalInference/Randomized/DifferenceInMeans.lean
vendor/StatLean/StatLean/CausalInference/Randomized/Fisher.lean
vendor/StatLean/StatLean/CausalInference/Randomized/MatchedPairs.lean
vendor/StatLean/StatLean/CausalInference/Randomized/Neyman.lean
vendor/StatLean/StatLean/CausalInference/Randomized/RegressionAdjustment.lean
vendor/StatLean/StatLean/CausalInference/Randomized/Stratified.lean
vendor/StatLean/StatLean/CausalInference/Randomized/SuperPopulationBridge.lean
vendor/StatLean/StatLean/CausalInference/Randomized/VarianceEstimator.lean
vendor/StatLean/StatLean/CausalInference/Sensitivity/EValue.lean
vendor/StatLean/StatLean/CausalInference/Sensitivity/ManskiBounds.lean
vendor/StatLean/StatLean/CausalInference/Sensitivity/Rosenbaum.lean
vendor/StatLean/StatLean/CausalInference.lean
vendor/StatLean/StatLean/ComputationalStatistics/Core/Defs.lean
vendor/StatLean/StatLean/ComputationalStatistics/Core/EmpiricalMeasure.lean
vendor/StatLean/StatLean/ComputationalStatistics/ForMathlib/PiMarginal.lean
vendor/StatLean/StatLean/ComputationalStatistics/ForMathlib/PiMoments.lean
vendor/StatLean/StatLean/ComputationalStatistics/MonteCarlo/Estimation.lean
vendor/StatLean/StatLean/ComputationalStatistics/MonteCarlo/ImportanceSampling.lean
vendor/StatLean/StatLean/ComputationalStatistics/MonteCarlo/RejectionSampling.lean
vendor/StatLean/StatLean/ComputationalStatistics/Partitioning/Holdout.lean
vendor/StatLean/StatLean/ComputationalStatistics/Partitioning/KFold.lean
vendor/StatLean/StatLean/ComputationalStatistics/Resampling/BootstrapMoments.lean
vendor/StatLean/StatLean/ComputationalStatistics/Resampling/CategoricalCounts.lean
vendor/StatLean/StatLean/ComputationalStatistics/Resampling/Jackknife.lean
vendor/StatLean/StatLean/ComputationalStatistics/Resampling/JackknifeBias.lean
vendor/StatLean/StatLean/ComputationalStatistics/Resampling/MultinomialMoments.lean
vendor/StatLean/StatLean/ComputationalStatistics/Resampling/ParticleResampling.lean
vendor/StatLean/StatLean/ComputationalStatistics.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Bernstein/Bernstein.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Bernstein/Defs.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Bernstein/MGFBound.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Chaining/CountableSupLift.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Chaining/DiscreteDudley.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Chaining/DiscreteDudleySup.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Chaining/Dudley.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Chaining/DudleyConsumers.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Chaining/DudleySup.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Chaining/DudleyTail.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Chaining/DudleyTailSup.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Chaining/DyadicNets.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Chaining/EntropyIntegrand.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Chaining/EntropySum.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Chaining/FinsetMaximal.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Chaining/GammaTwo.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Chaining/GenericChaining.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Chaining/GenericChainingSup.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Chaining/PsiTwoMaximal.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Chaining/SeparableProcess.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Chaining/SubGaussianIncrements.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Chaining/SubsetChaining.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Chaining/TailToExpectation.lean
vendor/StatLean/StatLean/ConcentrationInequalities/ClassicalLimits.lean
vendor/StatLean/StatLean/ConcentrationInequalities/EmpiricalProcess/Defs.lean
vendor/StatLean/StatLean/ConcentrationInequalities/EmpiricalProcess/LipschitzApprox.lean
vendor/StatLean/StatLean/ConcentrationInequalities/EmpiricalProcess/LipschitzCovering.lean
vendor/StatLean/StatLean/ConcentrationInequalities/EmpiricalProcess/LipschitzDense.lean
vendor/StatLean/StatLean/ConcentrationInequalities/EmpiricalProcess/LipschitzLLN.lean
vendor/StatLean/StatLean/ConcentrationInequalities/EmpiricalProcess/LipschitzNet.lean
vendor/StatLean/StatLean/ConcentrationInequalities/EmpiricalProcess/SubGaussianIncrements.lean
vendor/StatLean/StatLean/ConcentrationInequalities/ForMathlib/BinomialSumBound.lean
vendor/StatLean/StatLean/ConcentrationInequalities/ForMathlib/ExpTaylorBounds.lean
vendor/StatLean/StatLean/ConcentrationInequalities/ForMathlib/GaussianAbsMoment.lean
vendor/StatLean/StatLean/ConcentrationInequalities/ForMathlib/IndepTransport.lean
vendor/StatLean/StatLean/ConcentrationInequalities/ForMathlib/SupRatApprox.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Maximal/CoveringBall.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Maximal/CoveringNumbers.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Maximal/FiniteMaximal.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Maximal/L2Maximal.lean
vendor/StatLean/StatLean/ConcentrationInequalities/McDiarmid/CondHoeffding.lean
vendor/StatLean/StatLean/ConcentrationInequalities/McDiarmid/DoobDecomposition.lean
vendor/StatLean/StatLean/ConcentrationInequalities/McDiarmid/McDiarmid.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Orlicz/Attainment.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Orlicz/Basic.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Orlicz/Bernstein.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Orlicz/Defs.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Orlicz/Equivalence.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Orlicz/Generators.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Orlicz/NormFromMoments.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Orlicz/Product.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Orlicz/SubExponentialMGF.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Orlicz/SubExponentialTail.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Orlicz/SubGaussianMGF.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Orlicz/SubGaussianMoments.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Orlicz/SubGaussianTail.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Orlicz/SumNorm.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Orlicz/TailToNorm.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Orlicz/Triangle.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Orlicz/VectorNorm.lean
vendor/StatLean/StatLean/ConcentrationInequalities/SubExponential/Defs.lean
vendor/StatLean/StatLean/ConcentrationInequalities/SubExponential/SampleMean.lean
vendor/StatLean/StatLean/ConcentrationInequalities/SubExponential/TailBounds.lean
vendor/StatLean/StatLean/ConcentrationInequalities/SubGaussian/Bounded.lean
vendor/StatLean/StatLean/ConcentrationInequalities/SubGaussian/Chernoff.lean
vendor/StatLean/StatLean/ConcentrationInequalities/SubGaussian/Defs.lean
vendor/StatLean/StatLean/ConcentrationInequalities/SubGaussian/Hoeffding.lean
vendor/StatLean/StatLean/ConcentrationInequalities/SubGaussian/TailBounds.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Symmetrization/Contraction.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Symmetrization/Empirical.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Symmetrization/Gaussian.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Symmetrization/GaussianMax.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Symmetrization/GaussianVector.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Symmetrization/NormAddMeanZero.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Symmetrization/Rademacher.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Symmetrization/SignFlip.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Symmetrization/SymmetricLaw.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Symmetrization/Symmetrization.lean
vendor/StatLean/StatLean/ConcentrationInequalities/Symmetrization/SymmetrizationIndep.lean
vendor/StatLean/StatLean/ConcentrationInequalities/VC/CoveringByVC.lean
vendor/StatLean/StatLean/ConcentrationInequalities/VC/Defs.lean
vendor/StatLean/StatLean/ConcentrationInequalities/VC/DimensionReduction.lean
vendor/StatLean/StatLean/ConcentrationInequalities/VC/EntropyIntegral.lean
vendor/StatLean/StatLean/ConcentrationInequalities/VC/Examples.lean
vendor/StatLean/StatLean/ConcentrationInequalities/VC/Generalization.lean
vendor/StatLean/StatLean/ConcentrationInequalities/VC/GlivenkoCantelli.lean
vendor/StatLean/StatLean/ConcentrationInequalities/VC/HalfSpaces.lean
vendor/StatLean/StatLean/ConcentrationInequalities/VC/LawOfLargeNumbers.lean
vendor/StatLean/StatLean/ConcentrationInequalities/VC/LawOfLargeNumbersCountable.lean
vendor/StatLean/StatLean/ConcentrationInequalities/VC/SauerShelah.lean
vendor/StatLean/StatLean/ConcentrationInequalities.lean
vendor/StatLean/StatLean/ExperimentalDesign/Analysis/OneWayANOVA.lean
vendor/StatLean/StatLean/ExperimentalDesign/Core/Contrast.lean
vendor/StatLean/StatLean/ExperimentalDesign/Core/Design.lean
vendor/StatLean/StatLean/ExperimentalDesign/Core/FinitePopulation.lean
vendor/StatLean/StatLean/ExperimentalDesign/Core/Stratification.lean
vendor/StatLean/StatLean/ExperimentalDesign/Factorial/TwoLevel.lean
vendor/StatLean/StatLean/ExperimentalDesign/ForMathlib/PMFExpectation.lean
vendor/StatLean/StatLean/ExperimentalDesign/Randomization/Blocked.lean
vendor/StatLean/StatLean/ExperimentalDesign/Randomization/CompleteRandomization.lean
vendor/StatLean/StatLean/ExperimentalDesign/Randomization/SamplingEquivalence.lean
vendor/StatLean/StatLean/ExperimentalDesign/Stratified/ProductDesign.lean
vendor/StatLean/StatLean/ExperimentalDesign/Stratified/StratifiedEstimator.lean
vendor/StatLean/StatLean/ExperimentalDesign/SurveySampling/HorvitzThompson.lean
vendor/StatLean/StatLean/ExperimentalDesign/SurveySampling/InclusionProbability.lean
vendor/StatLean/StatLean/ExperimentalDesign/SurveySampling/SimpleRandomSampling.lean
vendor/StatLean/StatLean/ExperimentalDesign.lean
vendor/StatLean/StatLean/HighDimensionalStatistics/CompressedSensing/BasisPursuit.lean
vendor/StatLean/StatLean/HighDimensionalStatistics/CompressedSensing/ConeTheorem.lean
vendor/StatLean/StatLean/HighDimensionalStatistics/CompressedSensing/Defs.lean
vendor/StatLean/StatLean/HighDimensionalStatistics/CompressedSensing/GaussianChiSquared.lean
vendor/StatLean/StatLean/HighDimensionalStatistics/CompressedSensing/RIPRecovery.lean
vendor/StatLean/StatLean/HighDimensionalStatistics/CompressedSensing/RandomRIP.lean
vendor/StatLean/StatLean/HighDimensionalStatistics/ForMathlib/GramMatrix.lean
vendor/StatLean/StatLean/HighDimensionalStatistics/ForMathlib/PsiTaylor.lean
vendor/StatLean/StatLean/HighDimensionalStatistics/ForMathlib/SupportSubmatrix.lean
vendor/StatLean/StatLean/HighDimensionalStatistics/ForMathlib/TopK.lean
vendor/StatLean/StatLean/HighDimensionalStatistics/ForMathlib/VecNorms.lean
vendor/StatLean/StatLean/HighDimensionalStatistics/Lasso/Defs.lean
vendor/StatLean/StatLean/HighDimensionalStatistics/Lasso/DeterministicRate.lean
vendor/StatLean/StatLean/HighDimensionalStatistics/Lasso/RandomNoise.lean
vendor/StatLean/StatLean/HighDimensionalStatistics/Lasso/SupportRecovery/Defs.lean
vendor/StatLean/StatLean/HighDimensionalStatistics/Lasso/SupportRecovery/DeterministicGuarantee.lean
vendor/StatLean/StatLean/HighDimensionalStatistics/Lasso/SupportRecovery/DualCertificate.lean
vendor/StatLean/StatLean/HighDimensionalStatistics/Lasso/SupportRecovery/SubGaussianNoise.lean
vendor/StatLean/StatLean/HighDimensionalStatistics/Lasso/SupportRecovery/Subgradient.lean
vendor/StatLean/StatLean/HighDimensionalStatistics/LinearModel/Defs.lean
vendor/StatLean/StatLean/HighDimensionalStatistics/MEstimator/Bound.lean
vendor/StatLean/StatLean/HighDimensionalStatistics/MEstimator/Defs.lean
vendor/StatLean/StatLean/HighDimensionalStatistics/MEstimator/Deviation.lean
vendor/StatLean/StatLean/HighDimensionalStatistics/MEstimator/DualBound.lean
vendor/StatLean/StatLean/HighDimensionalStatistics/MEstimator/GLMCorollaries.lean
vendor/StatLean/StatLean/HighDimensionalStatistics/MEstimator/GLMDefs.lean
vendor/StatLean/StatLean/HighDimensionalStatistics/MEstimator/GoodEvent.lean
vendor/StatLean/StatLean/HighDimensionalStatistics/MEstimator/L1Decomposable.lean
vendor/StatLean/StatLean/HighDimensionalStatistics/MEstimator/ScoreSubGaussian.lean
vendor/StatLean/StatLean/HighDimensionalStatistics/MEstimator/SubspaceLip.lean
vendor/StatLean/StatLean/HighDimensionalStatistics/OLS/MSEExpectation.lean
vendor/StatLean/StatLean/HighDimensionalStatistics/OLS/MSEHighProb.lean
vendor/StatLean/StatLean/HighDimensionalStatistics.lean
vendor/StatLean/StatLean/HypothesisTesting/Bootstrap/Consistency.lean
vendor/StatLean/StatLean/HypothesisTesting/Bootstrap/Defs.lean
vendor/StatLean/StatLean/HypothesisTesting/Bootstrap/Edgeworth.lean
vendor/StatLean/StatLean/HypothesisTesting/Bootstrap/Multivariate.lean
vendor/StatLean/StatLean/HypothesisTesting/Bootstrap/NonparametricMean.lean
vendor/StatLean/StatLean/HypothesisTesting/Bootstrap/ParametricLocal.lean
vendor/StatLean/StatLean/HypothesisTesting/Bootstrap/Testing.lean
vendor/StatLean/StatLean/HypothesisTesting/ForMathlib/BerryEsseen.lean
vendor/StatLean/StatLean/HypothesisTesting/ForMathlib/BivariateEdgeworth.lean
vendor/StatLean/StatLean/HypothesisTesting/ForMathlib/CombinatorialCLT.lean
vendor/StatLean/StatLean/HypothesisTesting/ForMathlib/CondDistribTilt.lean
vendor/StatLean/StatLean/HypothesisTesting/ForMathlib/CriticalFunction.lean
vendor/StatLean/StatLean/HypothesisTesting/ForMathlib/DKWUniform.lean
vendor/StatLean/StatLean/HypothesisTesting/ForMathlib/EsseenSmoothing.lean
vendor/StatLean/StatLean/HypothesisTesting/ForMathlib/GaussianShell.lean
vendor/StatLean/StatLean/HypothesisTesting/ForMathlib/GroupAverageMeasure.lean
vendor/StatLean/StatLean/HypothesisTesting/ForMathlib/HypergeometricMoments.lean
vendor/StatLean/StatLean/HypothesisTesting/ForMathlib/LindebergCLT.lean
vendor/StatLean/StatLean/HypothesisTesting/ForMathlib/MultivariateBerryEsseen.lean
vendor/StatLean/StatLean/HypothesisTesting/ForMathlib/NoncentralChiSquared.lean
vendor/StatLean/StatLean/HypothesisTesting/ForMathlib/PermutationMarginals.lean
vendor/StatLean/StatLean/HypothesisTesting/ForMathlib/PolyaUniformCDF.lean
vendor/StatLean/StatLean/HypothesisTesting/ForMathlib/QuantileFunction.lean
vendor/StatLean/StatLean/HypothesisTesting/ForMathlib/SteinMethod.lean
vendor/StatLean/StatLean/HypothesisTesting/ForMathlib/TestsWeakCompact.lean
vendor/StatLean/StatLean/HypothesisTesting/ForMathlib/UniformRiemannLebesgue.lean
vendor/StatLean/StatLean/HypothesisTesting/GoodnessOfFit/AsymptoticMaximin.lean
vendor/StatLean/StatLean/HypothesisTesting/GoodnessOfFit/ChiSquaredMaximin.lean
vendor/StatLean/StatLean/HypothesisTesting/GoodnessOfFit/ChiSquaredMultinomial.lean
vendor/StatLean/StatLean/HypothesisTesting/GoodnessOfFit/KSConsistency.lean
vendor/StatLean/StatLean/HypothesisTesting/GoodnessOfFit/KSLocalPower.lean
vendor/StatLean/StatLean/HypothesisTesting/GoodnessOfFit/SmoothTest.lean
vendor/StatLean/StatLean/HypothesisTesting/GoodnessOfFit/SmoothTestLargeK.lean
vendor/StatLean/StatLean/HypothesisTesting/Invariance/Admissibility.lean
vendor/StatLean/StatLean/HypothesisTesting/Invariance/AlmostInvariance.lean
vendor/StatLean/StatLean/HypothesisTesting/Invariance/BayesAdmissible.lean
vendor/StatLean/StatLean/HypothesisTesting/Invariance/Defs.lean
vendor/StatLean/StatLean/HypothesisTesting/Invariance/EquivariantConfidence.lean
vendor/StatLean/StatLean/HypothesisTesting/Invariance/MaximalInvariant.lean
vendor/StatLean/StatLean/HypothesisTesting/Invariance/SufficiencyReduction.lean
vendor/StatLean/StatLean/HypothesisTesting/Invariance/SymmetryIdentity.lean
vendor/StatLean/StatLean/HypothesisTesting/Invariance/UMPInvariantFinite.lean
vendor/StatLean/StatLean/HypothesisTesting/Invariance/UnbiasednessCoincidence.lean
vendor/StatLean/StatLean/HypothesisTesting/LikelihoodMethods/EstimatorUnderAlternatives.lean
vendor/StatLean/StatLean/HypothesisTesting/LikelihoodMethods/ScoreUnderAlternatives.lean
vendor/StatLean/StatLean/HypothesisTesting/LikelihoodMethods/TrinityChiSquared.lean
vendor/StatLean/StatLean/HypothesisTesting/LikelihoodMethods/UniformLAN.lean
vendor/StatLean/StatLean/HypothesisTesting/MLR/ConfidenceBounds.lean
vendor/StatLean/StatLean/HypothesisTesting/MLR/Defs.lean
vendor/StatLean/StatLean/HypothesisTesting/MLR/OneSided.lean
vendor/StatLean/StatLean/HypothesisTesting/MLR/StochasticDominance.lean
vendor/StatLean/StatLean/HypothesisTesting/MLR/TwoSided.lean
vendor/StatLean/StatLean/HypothesisTesting/NeymanPearson/Generalized.lean
vendor/StatLean/StatLean/HypothesisTesting/NeymanPearson/LeastFavorable.lean
vendor/StatLean/StatLean/HypothesisTesting/NeymanPearson/Lemma.lean
vendor/StatLean/StatLean/HypothesisTesting/Randomization/Asymptotics.lean
vendor/StatLean/StatLean/HypothesisTesting/Randomization/Defs.lean
vendor/StatLean/StatLean/HypothesisTesting/Randomization/ExactLevel.lean
vendor/StatLean/StatLean/HypothesisTesting/Randomization/MultivariateQuadratic.lean
vendor/StatLean/StatLean/HypothesisTesting/Randomization/OrbitConditional.lean
vendor/StatLean/StatLean/HypothesisTesting/Randomization/PairCLT.lean
vendor/StatLean/StatLean/HypothesisTesting/Randomization/SignChange.lean
vendor/StatLean/StatLean/HypothesisTesting/Randomization/SlutskyRandomization.lean
vendor/StatLean/StatLean/HypothesisTesting/Randomization/Studentized.lean
vendor/StatLean/StatLean/HypothesisTesting/Randomization/TwoSamplePermutation.lean
vendor/StatLean/StatLean/HypothesisTesting/Tests/Confidence.lean
vendor/StatLean/StatLean/HypothesisTesting/Tests/Defs.lean
vendor/StatLean/StatLean/HypothesisTesting/Tests/PValue.lean
vendor/StatLean/StatLean/HypothesisTesting/Unbiased/ConditionalExpFamily.lean
vendor/StatLean/StatLean/HypothesisTesting/Unbiased/MultiparamUMPU.lean
vendor/StatLean/StatLean/HypothesisTesting/Unbiased/OneParamTwoSided.lean
vendor/StatLean/StatLean/HypothesisTesting/Unbiased/PowerContinuity.lean
vendor/StatLean/StatLean/HypothesisTesting/Unbiased/SimilarityCompleteness.lean
vendor/StatLean/StatLean/HypothesisTesting.lean
vendor/StatLean/StatLean/Minimaxity/Defs.lean
vendor/StatLean/StatLean/Minimaxity/EstimationToTesting.lean
vendor/StatLean/StatLean/Minimaxity/Examples/DensityEstimation.lean
vendor/StatLean/StatLean/Minimaxity/Examples/GaussianLocation.lean
vendor/StatLean/StatLean/Minimaxity/Examples/LinearRegression.lean
vendor/StatLean/StatLean/Minimaxity/Examples/LipschitzDensity.lean
vendor/StatLean/StatLean/Minimaxity/Examples/PCA.lean
vendor/StatLean/StatLean/Minimaxity/Examples/Sobolev.lean
vendor/StatLean/StatLean/Minimaxity/Examples/SparseLinearRegression.lean
vendor/StatLean/StatLean/Minimaxity/Examples/UniformLocation.lean
vendor/StatLean/StatLean/Minimaxity/Fano/FanoLowerBound.lean
vendor/StatLean/StatLean/Minimaxity/Fano/LocalPacking.lean
vendor/StatLean/StatLean/Minimaxity/Fano/MutualInformation.lean
vendor/StatLean/StatLean/Minimaxity/Fano/YangBarron.lean
vendor/StatLean/StatLean/Minimaxity/ForMathlib/Entropy.lean
vendor/StatLean/StatLean/Minimaxity/ForMathlib/GaussianKL.lean
vendor/StatLean/StatLean/Minimaxity/ForMathlib/GaussianKLMulti.lean
vendor/StatLean/StatLean/Minimaxity/ForMathlib/GaussianMaxEntropy.lean
vendor/StatLean/StatLean/Minimaxity/ForMathlib/HellingerDivergence.lean
vendor/StatLean/StatLean/Minimaxity/ForMathlib/KLDataProcessing.lean
vendor/StatLean/StatLean/Minimaxity/ForMathlib/KLDivergence.lean
vendor/StatLean/StatLean/Minimaxity/ForMathlib/LeCamInequality.lean
vendor/StatLean/StatLean/Minimaxity/ForMathlib/Packing/HammingPacking.lean
vendor/StatLean/StatLean/Minimaxity/ForMathlib/Packing/SobolevEntropy.lean
vendor/StatLean/StatLean/Minimaxity/ForMathlib/Packing/SparsePacking.lean
vendor/StatLean/StatLean/Minimaxity/ForMathlib/Packing/SpherePacking.lean
vendor/StatLean/StatLean/Minimaxity/ForMathlib/PinskerInequality.lean
vendor/StatLean/StatLean/Minimaxity/ForMathlib/TotalVariation.lean
vendor/StatLean/StatLean/Minimaxity/LeCam/ConvexHull.lean
vendor/StatLean/StatLean/Minimaxity/LeCam/Functional.lean
vendor/StatLean/StatLean/Minimaxity/LeCam/TwoPoint.lean
vendor/StatLean/StatLean/Minimaxity.lean
vendor/StatLean/StatLean/MultipleTesting/BHDependence.lean
vendor/StatLean/StatLean/MultipleTesting/BHMartingale.lean
vendor/StatLean/StatLean/MultipleTesting/BenjaminiHochberg.lean
vendor/StatLean/StatLean/MultipleTesting/ChiSquaredTest/Distribution.lean
vendor/StatLean/StatLean/MultipleTesting/Conformal/Coverage.lean
vendor/StatLean/StatLean/MultipleTesting/EValues/Conversion.lean
vendor/StatLean/StatLean/MultipleTesting/EValues/Defs.lean
vendor/StatLean/StatLean/MultipleTesting/EmpiricalBayes/BayesRisk.lean
vendor/StatLean/StatLean/MultipleTesting/FDP/Defs.lean
vendor/StatLean/StatLean/MultipleTesting/ForMathlib/BinomialRatio.lean
vendor/StatLean/StatLean/MultipleTesting/ForMathlib/ChiSquared.lean
vendor/StatLean/StatLean/MultipleTesting/ForMathlib/EmpiricalCDF.lean
vendor/StatLean/StatLean/MultipleTesting/ForMathlib/EmpiricalProcessSup.lean
vendor/StatLean/StatLean/MultipleTesting/ForMathlib/GammaMoments.lean
vendor/StatLean/StatLean/MultipleTesting/ForMathlib/GaussianMoments.lean
vendor/StatLean/StatLean/MultipleTesting/ForMathlib/GaussianSquareMGF.lean
vendor/StatLean/StatLean/MultipleTesting/ForMathlib/OptionalStopping.lean
vendor/StatLean/StatLean/MultipleTesting/ForMathlib/OrderStatistics.lean
vendor/StatLean/StatLean/MultipleTesting/ForMathlib/RankUniform.lean
vendor/StatLean/StatLean/MultipleTesting/ForMathlib/SymmetricCondExp.lean
vendor/StatLean/StatLean/MultipleTesting/GoodnessOfFit/KolmogorovSmirnov.lean
vendor/StatLean/StatLean/MultipleTesting/HolmBonferroni.lean
vendor/StatLean/StatLean/MultipleTesting/Knockoff/Defs.lean
vendor/StatLean/StatLean/MultipleTesting/Knockoff/FdpBound.lean
vendor/StatLean/StatLean/MultipleTesting/Knockoff/Initial.lean
vendor/StatLean/StatLean/MultipleTesting/Knockoff/Procedure.lean
vendor/StatLean/StatLean/MultipleTesting/Knockoff/Supermartingale.lean
vendor/StatLean/StatLean/MultipleTesting/Knockoff.lean
vendor/StatLean/StatLean/MultipleTesting/PValues/Defs.lean
vendor/StatLean/StatLean/MultipleTesting.lean
vendor/StatLean/StatLean/NonparametricStatistics/ForMathlib/GaussianExpSq.lean
vendor/StatLean/StatLean/NonparametricStatistics/ForMathlib/MaxExpSquare.lean
vendor/StatLean/StatLean/NonparametricStatistics/ForMathlib/MinkowskiIntegral.lean
vendor/StatLean/StatLean/NonparametricStatistics/ForMathlib/TailSumRpow.lean
vendor/StatLean/StatLean/NonparametricStatistics/ForMathlib/TaylorIntegralRemainder.lean
vendor/StatLean/StatLean/NonparametricStatistics/ForMathlib/TaylorLagrangeTwoSided.lean
vendor/StatLean/StatLean/NonparametricStatistics/ForMathlib/TranslationL2.lean
vendor/StatLean/StatLean/NonparametricStatistics/ForMathlib/TrigDiscreteSums.lean
vendor/StatLean/StatLean/NonparametricStatistics/KernelDensity/AuxiliaryKernel.lean
vendor/StatLean/StatLean/NonparametricStatistics/KernelDensity/Bias.lean
vendor/StatLean/StatLean/NonparametricStatistics/KernelDensity/Defs.lean
vendor/StatLean/StatLean/NonparametricStatistics/KernelDensity/ExactMISE.lean
vendor/StatLean/StatLean/NonparametricStatistics/KernelDensity/IntegratedBias.lean
vendor/StatLean/StatLean/NonparametricStatistics/KernelDensity/IntegratedVariance.lean
vendor/StatLean/StatLean/NonparametricStatistics/KernelDensity/LawTransfer.lean
vendor/StatLean/StatLean/NonparametricStatistics/KernelDensity/MISEBias.lean
vendor/StatLean/StatLean/NonparametricStatistics/KernelDensity/MISEVariance.lean
vendor/StatLean/StatLean/NonparametricStatistics/KernelDensity/PointwiseRate.lean
vendor/StatLean/StatLean/NonparametricStatistics/KernelDensity/UniformDensityBound.lean
vendor/StatLean/StatLean/NonparametricStatistics/KernelDensity/Variance.lean
vendor/StatLean/StatLean/NonparametricStatistics/LocalPolynomial/Defs.lean
vendor/StatLean/StatLean/NonparametricStatistics/LocalPolynomial/L2Risk.lean
vendor/StatLean/StatLean/NonparametricStatistics/LocalPolynomial/PointwiseRisk.lean
vendor/StatLean/StatLean/NonparametricStatistics/LocalPolynomial/Quadratic.lean
vendor/StatLean/StatLean/NonparametricStatistics/LocalPolynomial/Reproduction.lean
vendor/StatLean/StatLean/NonparametricStatistics/LocalPolynomial/SupNorm/Increments.lean
vendor/StatLean/StatLean/NonparametricStatistics/LocalPolynomial/SupNorm/StochasticTerm.lean
vendor/StatLean/StatLean/NonparametricStatistics/LocalPolynomial/SupNorm/SupNormRate.lean
vendor/StatLean/StatLean/NonparametricStatistics/LocalPolynomial/WeightBounds.lean
vendor/StatLean/StatLean/NonparametricStatistics/Projection/Aliasing.lean
vendor/StatLean/StatLean/NonparametricStatistics/Projection/CoefficientRisk.lean
vendor/StatLean/StatLean/NonparametricStatistics/Projection/Defs.lean
vendor/StatLean/StatLean/NonparametricStatistics/Projection/DiscreteOrthogonality.lean
vendor/StatLean/StatLean/NonparametricStatistics/Projection/MISEDecomposition.lean
vendor/StatLean/StatLean/NonparametricStatistics/Projection/SobolevRate.lean
vendor/StatLean/StatLean/NonparametricStatistics/Projection/TrigOrthogonality.lean
vendor/StatLean/StatLean/NonparametricStatistics/RKHS/Basic.lean
vendor/StatLean/StatLean/NonparametricStatistics/RKHS/Continuity.lean
vendor/StatLean/StatLean/NonparametricStatistics/RKHS/FeatureMap.lean
vendor/StatLean/StatLean/NonparametricStatistics/RKHS/InnerKernel.lean
vendor/StatLean/StatLean/NonparametricStatistics/RKHS/IntegralOperator.lean
vendor/StatLean/StatLean/NonparametricStatistics/RKHS/KernelFunction.lean
vendor/StatLean/StatLean/NonparametricStatistics/RKHS/MaxMargin.lean
vendor/StatLean/StatLean/NonparametricStatistics/RKHS/Mercer/Basic.lean
vendor/StatLean/StatLean/NonparametricStatistics/RKHS/Mercer/Compact.lean
vendor/StatLean/StatLean/NonparametricStatistics/RKHS/Mercer/Defs.lean
vendor/StatLean/StatLean/NonparametricStatistics/RKHS/Mercer/OperatorLemmas.lean
vendor/StatLean/StatLean/NonparametricStatistics/RKHS/Mercer/SquareRoot.lean
vendor/StatLean/StatLean/NonparametricStatistics/RKHS/Mercer/Theorem.lean
vendor/StatLean/StatLean/NonparametricStatistics/RKHS/MinKernel.lean
vendor/StatLean/StatLean/NonparametricStatistics/RKHS/Moore.lean
vendor/StatLean/StatLean/NonparametricStatistics/RKHS/OrthonormalExpansion.lean
vendor/StatLean/StatLean/NonparametricStatistics/RKHS/Papadakis.lean
vendor/StatLean/StatLean/NonparametricStatistics/RKHS/ParsevalFrame.lean
vendor/StatLean/StatLean/NonparametricStatistics/RKHS/RangeSpace.lean
vendor/StatLean/StatLean/NonparametricStatistics/RKHS/RankOne.lean
vendor/StatLean/StatLean/NonparametricStatistics/RKHS/Representer.lean
vendor/StatLean/StatLean/NonparametricStatistics/RKHS/Separation.lean
vendor/StatLean/StatLean/NonparametricStatistics/RKHS/Sobolev.lean
vendor/StatLean/StatLean/NonparametricStatistics/RKHS/Subspace.lean
vendor/StatLean/StatLean/NonparametricStatistics/RKHS/Uniqueness.lean
vendor/StatLean/StatLean/NonparametricStatistics/RKHS.lean
vendor/StatLean/StatLean/NonparametricStatistics/Regression/Defs.lean
vendor/StatLean/StatLean/NonparametricStatistics/Regression/NWKernelRepresentation.lean
vendor/StatLean/StatLean/NonparametricStatistics/SmoothnessClasses/Defs.lean
vendor/StatLean/StatLean/NonparametricStatistics/SmoothnessClasses/HolderTaylor.lean
vendor/StatLean/StatLean/NonparametricStatistics/SmoothnessClasses/NikolskiTaylor.lean
vendor/StatLean/StatLean/NonparametricStatistics.lean
vendor/StatLean/StatLean/Optimization/AcceleratedGradient.lean
vendor/StatLean/StatLean/Optimization/AcceleratedProximal.lean
vendor/StatLean/StatLean/Optimization/Convex/Defs.lean
vendor/StatLean/StatLean/Optimization/Convex/Subgradient.lean
vendor/StatLean/StatLean/Optimization/ForMathlib/FirstOrderConvex.lean
vendor/StatLean/StatLean/Optimization/ForMathlib/GradientCalc.lean
vendor/StatLean/StatLean/Optimization/FrankWolfe.lean
vendor/StatLean/StatLean/Optimization/GradientDescent.lean
vendor/StatLean/StatLean/Optimization/LocalGlobal.lean
vendor/StatLean/StatLean/Optimization/Prox/Defs.lean
vendor/StatLean/StatLean/Optimization/Prox/Pillar.lean
vendor/StatLean/StatLean/Optimization/ProximalGradient.lean
vendor/StatLean/StatLean/Optimization/Smoothness/CoCoercive.lean
vendor/StatLean/StatLean/Optimization/Smoothness/Defs.lean
vendor/StatLean/StatLean/Optimization.lean
vendor/StatLean/StatLean/PointEstimation/Completeness/Basu.lean
vendor/StatLean/StatLean/PointEstimation/Completeness/Defs.lean
vendor/StatLean/StatLean/PointEstimation/Completeness/ExpFamily.lean
vendor/StatLean/StatLean/PointEstimation/Equivariance/ConditionalRiskEngine.lean
vendor/StatLean/StatLean/PointEstimation/Equivariance/Defs.lean
vendor/StatLean/StatLean/PointEstimation/Equivariance/General.lean
vendor/StatLean/StatLean/PointEstimation/Equivariance/LocationExamples.lean
vendor/StatLean/StatLean/PointEstimation/Equivariance/LocationMRE.lean
vendor/StatLean/StatLean/PointEstimation/Equivariance/LocationStructure.lean
vendor/StatLean/StatLean/PointEstimation/Equivariance/NoGroup.lean
vendor/StatLean/StatLean/PointEstimation/Equivariance/Pitman.lean
vendor/StatLean/StatLean/PointEstimation/Equivariance/RiskUnbiased.lean
vendor/StatLean/StatLean/PointEstimation/Equivariance/ScaleMRE.lean
vendor/StatLean/StatLean/PointEstimation/Equivariance/ScaleStructure.lean
vendor/StatLean/StatLean/PointEstimation/ExponentialFamily/Basic.lean
vendor/StatLean/StatLean/PointEstimation/ExponentialFamily/Defs.lean
vendor/StatLean/StatLean/PointEstimation/ExponentialFamily/MGF.lean
vendor/StatLean/StatLean/PointEstimation/ExponentialFamily/MinimalSufficient.lean
vendor/StatLean/StatLean/PointEstimation/ExponentialFamily/NaturalStatistic.lean
vendor/StatLean/StatLean/PointEstimation/ExponentialFamily/Smoothness.lean
vendor/StatLean/StatLean/PointEstimation/ExponentialFamily/SteinIdentity.lean
vendor/StatLean/StatLean/PointEstimation/ForMathlib/CondDistribDensity.lean
vendor/StatLean/StatLean/PointEstimation/ForMathlib/CondExpWithDensity.lean
vendor/StatLean/StatLean/PointEstimation/ForMathlib/ConvexMinimizers.lean
vendor/StatLean/StatLean/PointEstimation/ForMathlib/HalmosSavage.lean
vendor/StatLean/StatLean/PointEstimation/ForMathlib/IntegrationByPartsReal.lean
vendor/StatLean/StatLean/PointEstimation/ForMathlib/MGFUniqueness.lean
vendor/StatLean/StatLean/PointEstimation/ForMathlib/MGFUniquenessPi.lean
vendor/StatLean/StatLean/PointEstimation/ForMathlib/MeasurableArgmin.lean
vendor/StatLean/StatLean/PointEstimation/InformationInequality/Additivity.lean
vendor/StatLean/StatLean/PointEstimation/InformationInequality/Attainment.lean
vendor/StatLean/StatLean/PointEstimation/InformationInequality/Basic.lean
vendor/StatLean/StatLean/PointEstimation/InformationInequality/CramerRao.lean
vendor/StatLean/StatLean/PointEstimation/InformationInequality/Defs.lean
vendor/StatLean/StatLean/PointEstimation/InformationInequality/DensityRegularity.lean
vendor/StatLean/StatLean/PointEstimation/InformationInequality/ExpFamilyInfo.lean
vendor/StatLean/StatLean/PointEstimation/InformationInequality/Multiparameter.lean
vendor/StatLean/StatLean/PointEstimation/LinearModel/Canonical.lean
vendor/StatLean/StatLean/PointEstimation/LinearModel/Defs.lean
vendor/StatLean/StatLean/PointEstimation/LinearModel/Equivariant.lean
vendor/StatLean/StatLean/PointEstimation/LinearModel/GaussMarkov.lean
vendor/StatLean/StatLean/PointEstimation/LinearModel/LeastSquares.lean
vendor/StatLean/StatLean/PointEstimation/LinearModel/RandomDesign.lean
vendor/StatLean/StatLean/PointEstimation/Model/Defs.lean
vendor/StatLean/StatLean/PointEstimation/Sufficiency/Basic.lean
vendor/StatLean/StatLean/PointEstimation/Sufficiency/BayesianBridge.lean
vendor/StatLean/StatLean/PointEstimation/Sufficiency/Defs.lean
vendor/StatLean/StatLean/PointEstimation/Sufficiency/Factorization.lean
vendor/StatLean/StatLean/PointEstimation/Sufficiency/HalmosSavageCriterion.lean
vendor/StatLean/StatLean/PointEstimation/Sufficiency/Minimal.lean
vendor/StatLean/StatLean/PointEstimation/Sufficiency/RegularConditional.lean
vendor/StatLean/StatLean/PointEstimation/Sufficiency/RiskEquality.lean
vendor/StatLean/StatLean/PointEstimation/UMVU/Basic.lean
vendor/StatLean/StatLean/PointEstimation/UMVU/CovarianceCriterion.lean
vendor/StatLean/StatLean/PointEstimation/UMVU/Defs.lean
vendor/StatLean/StatLean/PointEstimation/UMVU/LehmannScheffe.lean
vendor/StatLean/StatLean/PointEstimation/UMVU/RaoBlackwell.lean
vendor/StatLean/StatLean/PointEstimation.lean
vendor/StatLean/StatLean/RobustStatistics/Core/Bias.lean
vendor/StatLean/StatLean/RobustStatistics/Core/BreakdownPoint.lean
vendor/StatLean/StatLean/RobustStatistics/Core/Contamination.lean
vendor/StatLean/StatLean/RobustStatistics/Core/Equivariance.lean
vendor/StatLean/StatLean/RobustStatistics/Core/InfluenceFunction.lean
vendor/StatLean/StatLean/RobustStatistics/ForMathlib/OrderStatPerturb.lean
vendor/StatLean/StatLean/RobustStatistics/HeavyTails/Catoni.lean
vendor/StatLean/StatLean/RobustStatistics/HeavyTails/DeviationLowerBound.lean
vendor/StatLean/StatLean/RobustStatistics/HeavyTails/EmpiricalMeanBaseline.lean
vendor/StatLean/StatLean/RobustStatistics/HeavyTails/MedianOfMeans.lean
vendor/StatLean/StatLean/RobustStatistics/HeavyTails/TrimmedMean.lean
vendor/StatLean/StatLean/RobustStatistics/LocationScale/Huber.lean
vendor/StatLean/StatLean/RobustStatistics/LocationScale/MAD.lean
vendor/StatLean/StatLean/RobustStatistics/LocationScale/MLocation.lean
vendor/StatLean/StatLean/RobustStatistics/LocationScale/Mean.lean
vendor/StatLean/StatLean/RobustStatistics/LocationScale/Median.lean
vendor/StatLean/StatLean/RobustStatistics/LocationScale/MedianBreakdown.lean
vendor/StatLean/StatLean/RobustStatistics/LocationScale/TrimmedMean.lean
vendor/StatLean/StatLean/RobustStatistics/MEstimation/AsymptoticBreakdown.lean
vendor/StatLean/StatLean/RobustStatistics/MEstimation/Asymptotics.lean
vendor/StatLean/StatLean/RobustStatistics/MEstimation/Influence.lean
vendor/StatLean/StatLean/RobustStatistics/MEstimation/MLocationFunctional.lean
vendor/StatLean/StatLean/RobustStatistics/MaxBias/MaxBiasLocation.lean
vendor/StatLean/StatLean/RobustStatistics/MaxBias/MedianMinimaxBias.lean
vendor/StatLean/StatLean/RobustStatistics/Multivariate/AffineEquivariance.lean
vendor/StatLean/StatLean/RobustStatistics/Multivariate/BallMoM.lean
vendor/StatLean/StatLean/RobustStatistics/Regression/MRegression.lean
vendor/StatLean/StatLean/RobustStatistics/Scale/DispersionBreakdown.lean
vendor/StatLean/StatLean/RobustStatistics/Scale/MScale.lean
vendor/StatLean/StatLean/RobustStatistics.lean
vendor/StatLean/StatLean/StatisticalLearning/Core/Defs.lean
vendor/StatLean/StatLean/StatisticalLearning/Core/ERM.lean
vendor/StatLean/StatLean/StatisticalLearning/Core/SampleLaw.lean
vendor/StatLean/StatLean/StatisticalLearning/FiniteClass/AgnosticPAC.lean
vendor/StatLean/StatLean/StatisticalLearning/FiniteClass/RealizablePAC.lean
vendor/StatLean/StatLean/StatisticalLearning/FiniteClass/UniformConvergence.lean
vendor/StatLean/StatLean/StatisticalLearning/PACBayes/ChangeOfMeasure.lean
vendor/StatLean/StatLean/StatisticalLearning/PACBayes/Defs.lean
vendor/StatLean/StatLean/StatisticalLearning/PACBayes/Generalization.lean
vendor/StatLean/StatLean/StatisticalLearning/Rademacher/Contraction.lean
vendor/StatLean/StatLean/StatisticalLearning/Rademacher/Defs.lean
vendor/StatLean/StatLean/StatisticalLearning/Rademacher/Generalization.lean
vendor/StatLean/StatLean/StatisticalLearning/Rademacher/Structural.lean
vendor/StatLean/StatLean/StatisticalLearning/Rademacher/Symmetrization.lean
vendor/StatLean/StatLean/StatisticalLearning/Stability/Defs.lean
vendor/StatLean/StatLean/StatisticalLearning/Stability/Generalization.lean
vendor/StatLean/StatLean/StatisticalLearning/Stability/RegularizedERM.lean
vendor/StatLean/StatLean/StatisticalLearning/Stability/ReplaceOne.lean
vendor/StatLean/StatLean/StatisticalLearning/VC/AgnosticPAC.lean
vendor/StatLean/StatLean/StatisticalLearning/VC/Bridge.lean
vendor/StatLean/StatLean/StatisticalLearning.lean
vendor/StatLean/StatLean/StatisticalModels/Adapters/Bayes.lean
vendor/StatLean/StatLean/StatisticalModels/Adapters/DecisionRisk.lean
vendor/StatLean/StatLean/StatisticalModels/Adapters/ParametricFamily.lean
vendor/StatLean/StatLean/StatisticalModels/Adapters/Sufficiency.lean
vendor/StatLean/StatLean/StatisticalModels/Calculus/Compose.lean
vendor/StatLean/StatLean/StatisticalModels/Calculus/Defs.lean
vendor/StatLean/StatLean/StatisticalModels/Calculus/Marginal.lean
vendor/StatLean/StatLean/StatisticalModels/Coarsening/Attenuation.lean
vendor/StatLean/StatLean/StatisticalModels/Coarsening/Basic.lean
vendor/StatLean/StatLean/StatisticalModels/Coarsening/CARBridge.lean
vendor/StatLean/StatLean/StatisticalModels/Coarsening/Defs.lean
vendor/StatLean/StatLean/StatisticalModels/Coarsening/IPW.lean
vendor/StatLean/StatLean/StatisticalModels/Coarsening/Ignorability.lean
vendor/StatLean/StatLean/StatisticalModels/Constraint/Defs.lean
vendor/StatLean/StatLean/StatisticalModels/Examples/BernoulliIID.lean
vendor/StatLean/StatLean/StatisticalModels/Examples/LocationCensoring.lean
vendor/StatLean/StatLean/StatisticalModels/FactorModels/Bridge.lean
vendor/StatLean/StatLean/StatisticalModels/FactorModels/Communality.lean
vendor/StatLean/StatLean/StatisticalModels/FactorModels/Defs.lean
vendor/StatLean/StatLean/StatisticalModels/FactorModels/FactorScores.lean
vendor/StatLean/StatLean/StatisticalModels/FactorModels/Gaussian.lean
vendor/StatLean/StatLean/StatisticalModels/FactorModels/Identifiability.lean
vendor/StatLean/StatLean/StatisticalModels/FactorModels/Likelihood.lean
vendor/StatLean/StatLean/StatisticalModels/FactorModels/LocalIndep.lean
vendor/StatLean/StatLean/StatisticalModels/FactorModels/Moments.lean
vendor/StatLean/StatLean/StatisticalModels/FactorModels/Rotation.lean
vendor/StatLean/StatLean/StatisticalModels/ForMathlib/CovarianceMatrix.lean
vendor/StatLean/StatLean/StatisticalModels/Gaussian/Affine.lean
vendor/StatLean/StatLean/StatisticalModels/Gaussian/BlockIndex.lean
vendor/StatLean/StatLean/StatisticalModels/Gaussian/Conditioning.lean
vendor/StatLean/StatLean/StatisticalModels/Gaussian/FinCorridor.lean
vendor/StatLean/StatLean/StatisticalModels/Gaussian/Marginal.lean
vendor/StatLean/StatLean/StatisticalModels/GraphicalModels/Core/CondIndep.lean
vendor/StatLean/StatLean/StatisticalModels/GraphicalModels/Core/Coordinates.lean
vendor/StatLean/StatLean/StatisticalModels/GraphicalModels/Core/Semigraphoid.lean
vendor/StatLean/StatLean/StatisticalModels/GraphicalModels/Core/Separation.lean
vendor/StatLean/StatLean/StatisticalModels/GraphicalModels/Directed/DAG.lean
vendor/StatLean/StatLean/StatisticalModels/GraphicalModels/Directed/DSeparation.lean
vendor/StatLean/StatLean/StatisticalModels/GraphicalModels/Directed/Factorization.lean
vendor/StatLean/StatLean/StatisticalModels/GraphicalModels/Directed/Markov.lean
vendor/StatLean/StatLean/StatisticalModels/GraphicalModels/Directed/Moralization.lean
vendor/StatLean/StatLean/StatisticalModels/GraphicalModels/Discrete/CondIndep.lean
vendor/StatLean/StatLean/StatisticalModels/GraphicalModels/Discrete/Factorization.lean
vendor/StatLean/StatLean/StatisticalModels/GraphicalModels/Examples/Chain.lean
vendor/StatLean/StatLean/StatisticalModels/GraphicalModels/Gaussian/Model.lean
vendor/StatLean/StatLean/StatisticalModels/GraphicalModels/Gaussian/PartialCorrelation.lean
vendor/StatLean/StatLean/StatisticalModels/GraphicalModels/Gaussian/Precision.lean
vendor/StatLean/StatLean/StatisticalModels/GraphicalModels/Gaussian/Regression.lean
vendor/StatLean/StatLean/StatisticalModels/GraphicalModels/Undirected/Markov.lean
vendor/StatLean/StatLean/StatisticalModels/Identifiability/Defs.lean
vendor/StatLean/StatLean/StatisticalModels/Identifiability/Transfer.lean
vendor/StatLean/StatLean/StatisticalModels/Longitudinal/Defs.lean
vendor/StatLean/StatLean/StatisticalModels/Longitudinal/GEE.lean
vendor/StatLean/StatLean/StatisticalModels/Longitudinal/Godambe.lean
vendor/StatLean/StatLean/StatisticalModels/Longitudinal/Sandwich.lean
vendor/StatLean/StatLean/StatisticalModels/MixedEffects/BLUP.lean
vendor/StatLean/StatLean/StatisticalModels/MixedEffects/Defs.lean
vendor/StatLean/StatLean/StatisticalModels/MixedEffects/Henderson.lean
vendor/StatLean/StatLean/StatisticalModels/MixedEffects/Marginal.lean
vendor/StatLean/StatLean/StatisticalModels/Model/Defs.lean
vendor/StatLean/StatLean/StatisticalModels/Model/KernelAgreement.lean
vendor/StatLean/StatLean/StatisticalModels/Survival/Censoring.lean
vendor/StatLean/StatLean/StatisticalModels/Survival/CompetingRisks.lean
vendor/StatLean/StatLean/StatisticalModels/Survival/Cox/Basic.lean
vendor/StatLean/StatLean/StatisticalModels/Survival/Cox/Defs.lean
vendor/StatLean/StatLean/StatisticalModels/Survival/Cox/Identifiability.lean
vendor/StatLean/StatLean/StatisticalModels/Survival/Cox/PartialLikelihood.lean
vendor/StatLean/StatLean/StatisticalModels/Survival/CumulativeHazard.lean
vendor/StatLean/StatLean/StatisticalModels/Survival/Defs.lean
vendor/StatLean/StatLean/StatisticalModels/Survival/HazardBridges.lean
vendor/StatLean/StatLean/StatisticalModels/Survival/KaplanMeier.lean
vendor/StatLean/StatLean/StatisticalModels/Survival/Survival.lean
vendor/StatLean/StatLean/StatisticalModels.lean
vendor/StatLean/StatLean/TimeSeries/ARMA/Consistency.lean
vendor/StatLean/StatLean/TimeSeries/ARMA/Diagnostics.lean
vendor/StatLean/StatLean/TimeSeries/ARMA/Likelihood.lean
vendor/StatLean/StatLean/TimeSeries/ARMA/MLEAsymptotics.lean
vendor/StatLean/StatLean/TimeSeries/ARMA/OrderSelection.lean
vendor/StatLean/StatLean/TimeSeries/ARMA/Prediction.lean
vendor/StatLean/StatLean/TimeSeries/ARMA/ScoreAnalysis.lean
vendor/StatLean/StatLean/TimeSeries/ForMathlib/Ergodic/Birkhoff.lean
vendor/StatLean/StatLean/TimeSeries/ForMathlib/Fourier/FejerKernel.lean
vendor/StatLean/StatLean/TimeSeries/ForMathlib/Fourier/HerglotzBochner.lean
vendor/StatLean/StatLean/TimeSeries/ForMathlib/Fourier/MeasureFourierCoeff.lean
vendor/StatLean/StatLean/TimeSeries/ForMathlib/Markov/Chain.lean
vendor/StatLean/StatLean/TimeSeries/ForMathlib/Markov/GeometricErgodicity.lean
vendor/StatLean/StatLean/TimeSeries/ForMathlib/Markov/HarrisTheorem.lean
vendor/StatLean/StatLean/TimeSeries/ForMathlib/Markov/IFSMinorization.lean
vendor/StatLean/StatLean/TimeSeries/ForMathlib/Markov/TwoSidedChain.lean
vendor/StatLean/StatLean/TimeSeries/ForMathlib/PosSemidefSequence.lean
vendor/StatLean/StatLean/TimeSeries/ForMathlib/Probability/MartingaleCLT/BrownCLT.lean
vendor/StatLean/StatLean/TimeSeries/ForMathlib/Probability/MartingaleCLT/CondCharFun.lean
vendor/StatLean/StatLean/TimeSeries/ForMathlib/Probability/MartingaleCLT/Defs.lean
vendor/StatLean/StatLean/TimeSeries/ForMathlib/Probability/TriangularCLT.lean
vendor/StatLean/StatLean/TimeSeries/GARCH/ARCHBasic.lean
vendor/StatLean/StatLean/TimeSeries/GARCH/ARCHTest.lean
vendor/StatLean/StatLean/TimeSeries/GARCH/Estimation.lean
vendor/StatLean/StatLean/TimeSeries/GARCH/GARCHBasic.lean
vendor/StatLean/StatLean/TimeSeries/GARCH/StochasticVolatility.lean
vendor/StatLean/StatLean/TimeSeries/Mixing/Defs.lean
vendor/StatLean/StatLean/TimeSeries/Mixing/Inequalities.lean
vendor/StatLean/StatLean/TimeSeries/Mixing/KernelRegressionCLT.lean
vendor/StatLean/StatLean/TimeSeries/Mixing/LimitTheorems.lean
vendor/StatLean/StatLean/TimeSeries/Mixing/MarkovBridge.lean
vendor/StatLean/StatLean/TimeSeries/Mixing/Relations.lean
vendor/StatLean/StatLean/TimeSeries/Models/Defs.lean
vendor/StatLean/StatLean/TimeSeries/Models/Linear.lean
vendor/StatLean/StatLean/TimeSeries/Models/WhiteNoise.lean
vendor/StatLean/StatLean/TimeSeries/Process/Autocovariance.lean
vendor/StatLean/StatLean/TimeSeries/Process/Defs.lean
vendor/StatLean/StatLean/TimeSeries/Process/LinearProcess.lean
vendor/StatLean/StatLean/TimeSeries/Process/PartialAutocorrelation.lean
vendor/StatLean/StatLean/TimeSeries/Process/SampleACF.lean
vendor/StatLean/StatLean/TimeSeries/Process/SecondOrder.lean
vendor/StatLean/StatLean/TimeSeries/Process/Stationary.lean
vendor/StatLean/StatLean/TimeSeries/Spectral/ARMASpectral.lean
vendor/StatLean/StatLean/TimeSeries/Spectral/DFT.lean
vendor/StatLean/StatLean/TimeSeries/Spectral/LinearFilter.lean
vendor/StatLean/StatLean/TimeSeries/Spectral/Periodogram.lean
vendor/StatLean/StatLean/TimeSeries/Spectral/PeriodogramAsymptotics.lean
vendor/StatLean/StatLean/TimeSeries/Spectral/SpectralDensity.lean
vendor/StatLean/StatLean/TimeSeries/Spectral/SpectralMeasure.lean
vendor/StatLean/StatLean/TimeSeries/Stationarity/ARCH.lean
vendor/StatLean/StatLean/TimeSeries/Stationarity/ARMAExistence.lean
vendor/StatLean/StatLean/TimeSeries/Stationarity/Gaussian.lean
vendor/StatLean/StatLean/TimeSeries/Threshold/Estimation.lean
vendor/StatLean/StatLean/TimeSeries/Threshold/LinearityTest.lean
vendor/StatLean/StatLean/TimeSeries/Threshold/TAR.lean
vendor/StatLean/StatLean/TimeSeries.lean
vendor/StatLean/StatLean.lean
vendor/StatLean/UPSTREAM.md
vendor/StatLean/lake-manifest.json
vendor/StatLean/lakefile.toml
vendor/StatLean/lean-toolchain
vendor/StatLean/port/build_cache.sh
vendor/StatLean/port/convert_modules.py
vendor/StatLean/port/scan_names.py