PaperFormalizer · Formalized papers
Formalized papers
Partial Identification of Policy-Relevant Treatment Effects with Instrumental Variables via Optimal Transport
Lean code
A standalone Lake project: the paper's Lean, the toolkit modules it imports, and
Check.lean
.
Check.lean
Papers/TbsPrteOptimalTransport/All.lean
Papers/TbsPrteOptimalTransport/Basic.lean
Papers/TbsPrteOptimalTransport/Helpers/AdmissibleBandBoundary.lean
Papers/TbsPrteOptimalTransport/Helpers/AdmissibleFullDenominators.lean
Papers/TbsPrteOptimalTransport/Helpers/AttainingVersion.lean
Papers/TbsPrteOptimalTransport/Helpers/Attainment.lean
Papers/TbsPrteOptimalTransport/Helpers/BinaryBranchConvergence.lean
Papers/TbsPrteOptimalTransport/Helpers/BinaryBranches.lean
Papers/TbsPrteOptimalTransport/Helpers/BinaryRegressionAssembly.lean
Papers/TbsPrteOptimalTransport/Helpers/BinaryRegressionOrthogonality.lean
Papers/TbsPrteOptimalTransport/Helpers/BinaryScoreRemainder.lean
Papers/TbsPrteOptimalTransport/Helpers/BoundaryAtomFreedom.lean
Papers/TbsPrteOptimalTransport/Helpers/BoundaryLocalization.lean
Papers/TbsPrteOptimalTransport/Helpers/BoundaryMixture.lean
Papers/TbsPrteOptimalTransport/Helpers/BoundaryQuantileAssembly.lean
Papers/TbsPrteOptimalTransport/Helpers/BoundaryRateAssembly.lean
Papers/TbsPrteOptimalTransport/Helpers/Canonical.lean
Papers/TbsPrteOptimalTransport/Helpers/ConnectedBoundary.lean
Papers/TbsPrteOptimalTransport/Helpers/ConnectedIV.lean
Papers/TbsPrteOptimalTransport/Helpers/ConnectedReduction.lean
Papers/TbsPrteOptimalTransport/Helpers/ContinuousBandAdmissiblePropensity.lean
Papers/TbsPrteOptimalTransport/Helpers/ContinuousBandBoundaryMean.lean
Papers/TbsPrteOptimalTransport/Helpers/ContinuousBandCoreAssembly.lean
Papers/TbsPrteOptimalTransport/Helpers/ContinuousBandCorrection.lean
Papers/TbsPrteOptimalTransport/Helpers/ContinuousBandDirectionRegularity.lean
Papers/TbsPrteOptimalTransport/Helpers/ContinuousBandFinalDerivative.lean
Papers/TbsPrteOptimalTransport/Helpers/ContinuousBandIndicatorJoint.lean
Papers/TbsPrteOptimalTransport/Helpers/ContinuousBandJointBias.lean
Papers/TbsPrteOptimalTransport/Helpers/ContinuousBandJointDerivative.lean
Papers/TbsPrteOptimalTransport/Helpers/ContinuousBandOutcomeJoint.lean
Papers/TbsPrteOptimalTransport/Helpers/ContinuousBandPolicyAssembly.lean
Papers/TbsPrteOptimalTransport/Helpers/ContinuousBandPolicyRegressionAssembly.lean
Papers/TbsPrteOptimalTransport/Helpers/ContinuousBandPropensityBias.lean
Papers/TbsPrteOptimalTransport/Helpers/ContinuousBandPropensityPolicyAssembly.lean
Papers/TbsPrteOptimalTransport/Helpers/ContinuousBandQuantileRegressionAssembly.lean
Papers/TbsPrteOptimalTransport/Helpers/ContinuousBandRegressionAssembly.lean
Papers/TbsPrteOptimalTransport/Helpers/ContinuousBandRegressionBounds.lean
Papers/TbsPrteOptimalTransport/Helpers/ContinuousBoundaryResidualBounds.lean
Papers/TbsPrteOptimalTransport/Helpers/ContinuousDirectionRegularity.lean
Papers/TbsPrteOptimalTransport/Helpers/ContinuousFittedBoundaryWeights.lean
Papers/TbsPrteOptimalTransport/Helpers/ContinuousFrozenBandWeights.lean
Papers/TbsPrteOptimalTransport/Helpers/ContinuousFullAdmissibleDerivative.lean
Papers/TbsPrteOptimalTransport/Helpers/ContinuousFullBounds.lean
Papers/TbsPrteOptimalTransport/Helpers/ContinuousFullJointBias.lean
Papers/TbsPrteOptimalTransport/Helpers/ContinuousFullMeanOverlap.lean
Papers/TbsPrteOptimalTransport/Helpers/ContinuousFullProductJointBias.lean
Papers/TbsPrteOptimalTransport/Helpers/ContinuousLearners.lean
Papers/TbsPrteOptimalTransport/Helpers/ContinuousMovingPropensity.lean
Papers/TbsPrteOptimalTransport/Helpers/ContinuousPolicyBounds.lean
Papers/TbsPrteOptimalTransport/Helpers/ContinuousPooledJoint.lean
Papers/TbsPrteOptimalTransport/Helpers/ContinuousPropensityBounds.lean
Papers/TbsPrteOptimalTransport/Helpers/ContinuousQuantileOrdering.lean
Papers/TbsPrteOptimalTransport/Helpers/ContinuousTailAdmissibleDerivative.lean
Papers/TbsPrteOptimalTransport/Helpers/ContinuousTailPopulation.lean
Papers/TbsPrteOptimalTransport/Helpers/ContinuousTotalBandWeights.lean
Papers/TbsPrteOptimalTransport/Helpers/ContinuousTotalFullWeights.lean
Papers/TbsPrteOptimalTransport/Helpers/ContinuousTotalJointDerivative.lean
Papers/TbsPrteOptimalTransport/Helpers/CrossedBandBoundary.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLActivePolicyConvergence.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLBaselineResidualRates.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLBinaryBiasAssembly.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLBinaryBranchRates.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLBinaryComponentBridge.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLBinaryComponentDecoding.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLBinaryFiniteLabelClipping.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLBinaryLowerBoundNormality.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLBinaryOracleClipping.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLBinaryOracleConclusions.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLBinaryOracleMoments.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLBinaryOracleRemainder.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLBinaryPoolingBias.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLBinaryPopulationNormality.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLBinaryPopulationVariance.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLBinaryRearrangement.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLBinaryRearrangementAdmissibility.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLBinaryScoreBounds.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLBinaryTargetConclusions.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLBinaryTrainingVariance.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLBinaryVarianceConsistency.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLBoundaryResidualRates.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLBoundedFixedLabels.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLBoundedTrainingConclusions.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLBranchCoefficientBridge.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLBranchProductBridge.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLBranchResidualBridge.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLBranchWeightedConvergence.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLCanonicalRecoveryLabels.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLCenteredBandConvergence.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLChangingBandRegressions.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLChangingBandWeights.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLChangingIndicatorRegressions.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLChangingOutcomeBands.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLChangingOutcomeRegressions.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLChangingSelectedDenominators.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLConditionalFluctuation.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousBandBiasDecomposition.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousBandBiasTransfer.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousBandCoreConvergence.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousBandJointMean.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousBandProductBias.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousBandProductMean.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousBandProductRegression.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousBandPropensityRates.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousBandReferenceMean.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousBandRegressionHybrid.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousBandRegressionRates.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousBandShares.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousBandSmoothReduction.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousBandTreatment.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousBandTreatmentEvaluation.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousBoundaryProducts.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousCenteredFluctuation.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousComponentBridge.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousComponentDecoding.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousDenominatorBias.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousEncodedBand.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousEncodedFull.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousEncodedQuantile.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousEncodedTail.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousEvaluation.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousFirstBandBias.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousFullBiasAssembly.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousFullContrast.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousFullEvaluation.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousFullMean.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousFullProductBias.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousFullRates.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousFullResidual.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousHybridMean.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousJointBlock.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousJointMean.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousLabelTransport.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousLowerBoundNormality.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousOracleClipping.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousPolicyResidual.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousPoolingBias.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousPoolingRates.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousQuantileDenominatorBias.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousRegimeConvergence.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousRestoredBandBias.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousRieszCoordinates.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousRieszRates.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousScoreBounds.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousScoreConvergence.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousScoreLabels.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousSmoothPropensity.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousTailBias.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousTailConvergence.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousTailEvaluation.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousTargetConclusions.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousTotalBias.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousTreatmentResidual.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLContinuousWeightedFullResidual.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLCountableScoreLabels.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLCrossedBandBias.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLEnvelopeFactorization.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLErrorFiniteness.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLFiniteFullScoreConvergence.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLFiniteLabelClipping.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLFiniteLabelDecoding.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLFiniteLabelVariance.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLFittedFullProduct.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLFittedPolicyResidual.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLFittedRegularProduct.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLFittedSuccessResidual.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLFittedTail.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLFittedTreatmentResidual.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLFixedLabelPredictors.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLFractionalBiasBlocks.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLFractionalBranchRates.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLFractionalHingeBias.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLFractionalPolicyBias.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLFractionalProductBias.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLFractionalResidualConvergence.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLFractionalTreatmentConvergence.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLFullBlockRates.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLFullProductAssembly.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLFullScoreConvergence.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLGammaBandBlock.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLGammaBandMeans.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLGammaBandTreatment.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLGammaIndicatorContrast.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLGammaOutcomeBlock.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLGammaOutcomeContrast.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLGammaOutcomeConvergence.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLGammaPolicyResidual.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLIPWConvergence.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLIndependentScoreMoments.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLIndependentScoreVariance.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLIndicatorRates.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLIntegrableEvaluationLLN.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLMinusOutcomeConvergence.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLObservedQuantileBias.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLObservedRampBandBias.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLObservedResidualConvergence.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLOracleNormality.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLOracleRemainder.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLOracleSecondMoment.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLOracleTransfer.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLOutcomeBandConvergence.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLPairedPolicyBlock.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLPolicyResidualConvergence.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLPooledPolicyConvergence.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLPoolingRemainder.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLPopulationBiasAssembly.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLPopulationProductBias.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLPopulationScoreConvergence.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLProcedure.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLProcedureCore.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLQuantileBandConvergence.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLQuantileBandMeans.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLQuantileBiasRates.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLQuantileBoundaryBlock.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLQuantileBoundaryProducts.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLQuantilePolicyBlock.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLQuantileWeightedIndicator.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLRandomEvaluationLaw.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLRandomEvaluationMoments.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLRandomSplitEnumeration.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLRandomSplitLaw.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLRandomTrainingIndependence.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLRearrangedOracle.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLRearrangedVariance.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLRearrangementRegularity.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLReconstructedRegularity.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLRecoveryGraphMeasurability.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLRecoveryLabelDomains.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLRegimeVariance.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLRegularBiasAssembly.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLRegularHingeConvergence.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLRegularProductAssembly.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLRegularScoreConvergence.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLRemainderRates.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLRootNConsistency.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLScoreMeasurability.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLSelectedBandEnergy.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLSelectedChangingBands.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLStructuralZeroBranchRates.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLStructuralZeroFractionalRates.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLStructuralZeroHinge.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLTailAssembly.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLTailBaselineConvergence.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLTailScoreConvergence.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLTrainingFactorization.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLTrueBinaryOracle.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLWeightedBaselineCancellation.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLWeightedBoundaryResidual.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLWeightedHinge.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLWeightedPolicyConvergence.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLWeightedPooling.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLWeightedQuantileBias.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLWeightedQuantileIndicator.lean
Papers/TbsPrteOptimalTransport/Helpers/DMLWeightedRegularRegressionConvergence.lean
Papers/TbsPrteOptimalTransport/Helpers/DebiasedBandBoundary.lean
Papers/TbsPrteOptimalTransport/Helpers/DebiasedQuantileBoundary.lean
Papers/TbsPrteOptimalTransport/Helpers/DenominatorOrthogonality.lean
Papers/TbsPrteOptimalTransport/Helpers/DiscreteIV.lean
Papers/TbsPrteOptimalTransport/Helpers/DiscretePolicyAssembly.lean
Papers/TbsPrteOptimalTransport/Helpers/DiscretePolicyInterior.lean
Papers/TbsPrteOptimalTransport/Helpers/DiscretePolicyQuantile.lean
Papers/TbsPrteOptimalTransport/Helpers/DiscretePolicyTail.lean
Papers/TbsPrteOptimalTransport/Helpers/Disintegration.lean
Papers/TbsPrteOptimalTransport/Helpers/EssentialRanges.lean
Papers/TbsPrteOptimalTransport/Helpers/FeasibleDisintegration.lean
Papers/TbsPrteOptimalTransport/Helpers/FiniteRangeReduction.lean
Papers/TbsPrteOptimalTransport/Helpers/FirstStageTransfer.lean
Papers/TbsPrteOptimalTransport/Helpers/FittedBranchRegression.lean
Papers/TbsPrteOptimalTransport/Helpers/FractionalRegressionOrthogonality.lean
Papers/TbsPrteOptimalTransport/Helpers/FullRegressionOrthogonality.lean
Papers/TbsPrteOptimalTransport/Helpers/GapAttainment.lean
Papers/TbsPrteOptimalTransport/Helpers/GapBounds.lean
Papers/TbsPrteOptimalTransport/Helpers/GapKernelQuantile.lean
Papers/TbsPrteOptimalTransport/Helpers/GapQuantileMoments.lean
Papers/TbsPrteOptimalTransport/Helpers/HingePathEnvelopes.lean
Papers/TbsPrteOptimalTransport/Helpers/IPWRegressionRemainder.lean
Papers/TbsPrteOptimalTransport/Helpers/JBinaryBands.lean
Papers/TbsPrteOptimalTransport/Helpers/JQuantileBands.lean
Papers/TbsPrteOptimalTransport/Helpers/JointAttainment.lean
Papers/TbsPrteOptimalTransport/Helpers/JointFullRegressionWeights.lean
Papers/TbsPrteOptimalTransport/Helpers/JointPooledEnvelopes.lean
Papers/TbsPrteOptimalTransport/Helpers/JointPooledIntegration.lean
Papers/TbsPrteOptimalTransport/Helpers/JointPooledPopulation.lean
Papers/TbsPrteOptimalTransport/Helpers/JointPooledRemainder.lean
Papers/TbsPrteOptimalTransport/Helpers/JointRegularConditional.lean
Papers/TbsPrteOptimalTransport/Helpers/JointResidualEnvelopes.lean
Papers/TbsPrteOptimalTransport/Helpers/JointTailAdmissibility.lean
Papers/TbsPrteOptimalTransport/Helpers/JointTailConditional.lean
Papers/TbsPrteOptimalTransport/Helpers/JointTailIntegrability.lean
Papers/TbsPrteOptimalTransport/Helpers/JointTailIntegration.lean
Papers/TbsPrteOptimalTransport/Helpers/JointTailPopulation.lean
Papers/TbsPrteOptimalTransport/Helpers/JointTailRemainder.lean
Papers/TbsPrteOptimalTransport/Helpers/LIVPart.lean
Papers/TbsPrteOptimalTransport/Helpers/LearnerInterpolation.lean
Papers/TbsPrteOptimalTransport/Helpers/LevelGraphRecovery.lean
Papers/TbsPrteOptimalTransport/Helpers/LevelMarginalBaselineIdentification.lean
Papers/TbsPrteOptimalTransport/Helpers/LevelMarginalConcentration.lean
Papers/TbsPrteOptimalTransport/Helpers/LevelMarginalPolicyIdentification.lean
Papers/TbsPrteOptimalTransport/Helpers/LevelMarginalRates.lean
Papers/TbsPrteOptimalTransport/Helpers/LevelMarginalSeparation.lean
Papers/TbsPrteOptimalTransport/Helpers/LevelRecoveryProbability.lean
Papers/TbsPrteOptimalTransport/Helpers/LevelZeroRecovery.lean
Papers/TbsPrteOptimalTransport/Helpers/ObservationalCompatibility.lean
Papers/TbsPrteOptimalTransport/Helpers/ObservedBandBoundary.lean
Papers/TbsPrteOptimalTransport/Helpers/ObservedBoundaryTransfer.lean
Papers/TbsPrteOptimalTransport/Helpers/OrderedRanges.lean
Papers/TbsPrteOptimalTransport/Helpers/Orthogonality.lean
Papers/TbsPrteOptimalTransport/Helpers/PluginMeasurability.lean
Papers/TbsPrteOptimalTransport/Helpers/PluginPopulation.lean
Papers/TbsPrteOptimalTransport/Helpers/PluginPopulationRegularity.lean
Papers/TbsPrteOptimalTransport/Helpers/PluginRateAlgebra.lean
Papers/TbsPrteOptimalTransport/Helpers/PluginScoreMeasurability.lean
Papers/TbsPrteOptimalTransport/Helpers/PluginScoreTransport.lean
Papers/TbsPrteOptimalTransport/Helpers/PluginSplitMoment.lean
Papers/TbsPrteOptimalTransport/Helpers/PluginStability.lean
Papers/TbsPrteOptimalTransport/Helpers/PluginTraining.lean
Papers/TbsPrteOptimalTransport/Helpers/PolicyDerivativeMeasurability.lean
Papers/TbsPrteOptimalTransport/Helpers/PooledPolicyDirections.lean
Papers/TbsPrteOptimalTransport/Helpers/PooledPolicyOrthogonality.lean
Papers/TbsPrteOptimalTransport/Helpers/PooledTreated.lean
Papers/TbsPrteOptimalTransport/Helpers/PopulationAssignmentResidual.lean
Papers/TbsPrteOptimalTransport/Helpers/PopulationBinaryAdmissibility.lean
Papers/TbsPrteOptimalTransport/Helpers/PopulationBinaryComponents.lean
Papers/TbsPrteOptimalTransport/Helpers/PopulationBinaryDenominatorProducts.lean
Papers/TbsPrteOptimalTransport/Helpers/PopulationBinaryDenominators.lean
Papers/TbsPrteOptimalTransport/Helpers/PopulationBinaryMargins.lean
Papers/TbsPrteOptimalTransport/Helpers/PopulationBinaryMoments.lean
Papers/TbsPrteOptimalTransport/Helpers/PopulationBinaryRegularProducts.lean
Papers/TbsPrteOptimalTransport/Helpers/PopulationBinaryRegularity.lean
Papers/TbsPrteOptimalTransport/Helpers/PopulationBinaryScoreMean.lean
Papers/TbsPrteOptimalTransport/Helpers/PopulationBinaryTailOrthogonality.lean
Papers/TbsPrteOptimalTransport/Helpers/PopulationBinaryTarget.lean
Papers/TbsPrteOptimalTransport/Helpers/PopulationBinaryWeightAssembly.lean
Papers/TbsPrteOptimalTransport/Helpers/PopulationContinuousAdmissibility.lean
Papers/TbsPrteOptimalTransport/Helpers/PopulationContinuousBandAssembly.lean
Papers/TbsPrteOptimalTransport/Helpers/PopulationContinuousBandMean.lean
Papers/TbsPrteOptimalTransport/Helpers/PopulationContinuousBandSeparation.lean
Papers/TbsPrteOptimalTransport/Helpers/PopulationContinuousBandWeights.lean
Papers/TbsPrteOptimalTransport/Helpers/PopulationContinuousBoundaries.lean
Papers/TbsPrteOptimalTransport/Helpers/PopulationContinuousBoundaryRegularity.lean
Papers/TbsPrteOptimalTransport/Helpers/PopulationContinuousBounds.lean
Papers/TbsPrteOptimalTransport/Helpers/PopulationContinuousFullDenominators.lean
Papers/TbsPrteOptimalTransport/Helpers/PopulationContinuousFullMean.lean
Papers/TbsPrteOptimalTransport/Helpers/PopulationContinuousFullProducts.lean
Papers/TbsPrteOptimalTransport/Helpers/PopulationContinuousFullRanges.lean
Papers/TbsPrteOptimalTransport/Helpers/PopulationContinuousFullRegressions.lean
Papers/TbsPrteOptimalTransport/Helpers/PopulationContinuousRanges.lean
Papers/TbsPrteOptimalTransport/Helpers/PopulationContinuousResidual.lean
Papers/TbsPrteOptimalTransport/Helpers/PopulationContinuousTarget.lean
Papers/TbsPrteOptimalTransport/Helpers/PopulationContinuousTotalMean.lean
Papers/TbsPrteOptimalTransport/Helpers/PopulationDebiasedQuantileBoundary.lean
Papers/TbsPrteOptimalTransport/Helpers/PopulationFullJointDerivative.lean
Papers/TbsPrteOptimalTransport/Helpers/PopulationFullJointMean.lean
Papers/TbsPrteOptimalTransport/Helpers/PopulationInstrumentMoments.lean
Papers/TbsPrteOptimalTransport/Helpers/PopulationRegressionDirections.lean
Papers/TbsPrteOptimalTransport/Helpers/PopulationSuccessResidual.lean
Papers/TbsPrteOptimalTransport/Helpers/PopulationTreatmentResidual.lean
Papers/TbsPrteOptimalTransport/Helpers/PrimitivePluginTransfer.lean
Papers/TbsPrteOptimalTransport/Helpers/ProductScoreMoments.lean
Papers/TbsPrteOptimalTransport/Helpers/QuantileBandAssembly.lean
Papers/TbsPrteOptimalTransport/Helpers/QuantileGridTransfer.lean
Papers/TbsPrteOptimalTransport/Helpers/QuantileIndicatorConvergence.lean
Papers/TbsPrteOptimalTransport/Helpers/QuantilePolicyCancellation.lean
Papers/TbsPrteOptimalTransport/Helpers/QuantilePropensityCancellation.lean
Papers/TbsPrteOptimalTransport/Helpers/QuantileScoreRemainder.lean
Papers/TbsPrteOptimalTransport/Helpers/QuantileSorting.lean
Papers/TbsPrteOptimalTransport/Helpers/QuantileTotalAssembly.lean
Papers/TbsPrteOptimalTransport/Helpers/RandomizedRank.lean
Papers/TbsPrteOptimalTransport/Helpers/RangeRegularity.lean
Papers/TbsPrteOptimalTransport/Helpers/Ranges.lean
Papers/TbsPrteOptimalTransport/Helpers/RecoveryBaselineClasses.lean
Papers/TbsPrteOptimalTransport/Helpers/RecoveryBaselineCount.lean
Papers/TbsPrteOptimalTransport/Helpers/RecoveryBaselineIndexing.lean
Papers/TbsPrteOptimalTransport/Helpers/RecoveryBaselineOrder.lean
Papers/TbsPrteOptimalTransport/Helpers/RecoveryBaselineProjection.lean
Papers/TbsPrteOptimalTransport/Helpers/RecoveryComponentIndexing.lean
Papers/TbsPrteOptimalTransport/Helpers/RecoveryComponentValueOrder.lean
Papers/TbsPrteOptimalTransport/Helpers/RecoveryExactEvent.lean
Papers/TbsPrteOptimalTransport/Helpers/RecoveryInteriorComponents.lean
Papers/TbsPrteOptimalTransport/Helpers/RecoveryInteriorPolicyBins.lean
Papers/TbsPrteOptimalTransport/Helpers/RecoveryInteriorPolicyInclusion.lean
Papers/TbsPrteOptimalTransport/Helpers/RecoveryInteriorPolicyOrder.lean
Papers/TbsPrteOptimalTransport/Helpers/RecoveryInteriorPolicyProjection.lean
Papers/TbsPrteOptimalTransport/Helpers/RecoveryNonterminalBaselineComponents.lean
Papers/TbsPrteOptimalTransport/Helpers/RecoveryPolicyIndexing.lean
Papers/TbsPrteOptimalTransport/Helpers/RecoveryPolicyLabels.lean
Papers/TbsPrteOptimalTransport/Helpers/RecoveryTailExclusion.lean
Papers/TbsPrteOptimalTransport/Helpers/RecoveryTailPolicyBins.lean
Papers/TbsPrteOptimalTransport/Helpers/RecoveryTailPolicyIndexing.lean
Papers/TbsPrteOptimalTransport/Helpers/RecoveryZeroPolicyBins.lean
Papers/TbsPrteOptimalTransport/Helpers/RegionIntegration.lean
Papers/TbsPrteOptimalTransport/Helpers/RegionPartition.lean
Papers/TbsPrteOptimalTransport/Helpers/RegressionEndpointMargins.lean
Papers/TbsPrteOptimalTransport/Helpers/RegressionPathEnvelopes.lean
Papers/TbsPrteOptimalTransport/Helpers/RegressionTransfer.lean
Papers/TbsPrteOptimalTransport/Helpers/RegularComponentBias.lean
Papers/TbsPrteOptimalTransport/Helpers/RegularComponentRemainder.lean
Papers/TbsPrteOptimalTransport/Helpers/RegularPolicyMean.lean
Papers/TbsPrteOptimalTransport/Helpers/RegularProductBias.lean
Papers/TbsPrteOptimalTransport/Helpers/RegularProductOrthogonality.lean
Papers/TbsPrteOptimalTransport/Helpers/RegularRegressionMean.lean
Papers/TbsPrteOptimalTransport/Helpers/ScoreOrthogonality.lean
Papers/TbsPrteOptimalTransport/Helpers/Scores.lean
Papers/TbsPrteOptimalTransport/Helpers/ScoresBinary.lean
Papers/TbsPrteOptimalTransport/Helpers/SelectedConditionalLaw.lean
Papers/TbsPrteOptimalTransport/Helpers/SelectedGridIntegrability.lean
Papers/TbsPrteOptimalTransport/Helpers/SharpnessConstruction.lean
Papers/TbsPrteOptimalTransport/Helpers/SharpnessExogeneity.lean
Papers/TbsPrteOptimalTransport/Helpers/SharpnessIdentification.lean
Papers/TbsPrteOptimalTransport/Helpers/SharpnessModel.lean
Papers/TbsPrteOptimalTransport/Helpers/StructuralZeroBranches.lean
Papers/TbsPrteOptimalTransport/Helpers/StructuralZeroPopulation.lean
Papers/TbsPrteOptimalTransport/Helpers/TailAttainment.lean
Papers/TbsPrteOptimalTransport/Helpers/TailScoreOrthogonality.lean
Papers/TbsPrteOptimalTransport/Helpers/Transport.lean
Papers/TbsPrteOptimalTransport/Helpers/VarianceScoreComparison.lean
Papers/TbsPrteOptimalTransport/Helpers/WeightedBinaryRegression.lean
Papers/TbsPrteOptimalTransport/Helpers/WeightedFittedTreatment.lean
Papers/TbsPrteOptimalTransport/Helpers/WeightedPooledPopulation.lean
Papers/TbsPrteOptimalTransport/Helpers/WeightedQuantileBoundary.lean
Papers/TbsPrteOptimalTransport/Helpers.lean
Papers/TbsPrteOptimalTransport/T1dOt.lean
Papers/TbsPrteOptimalTransport/TContinuousLowerBound.lean
Papers/TbsPrteOptimalTransport/TContinuousPrimitiveRate.lean
Papers/TbsPrteOptimalTransport/TContinuousRate.lean
Papers/TbsPrteOptimalTransport/TContinuousReduction.lean
Papers/TbsPrteOptimalTransport/TCovariateLowerBound.lean
Papers/TbsPrteOptimalTransport/TDiscreteLowerBound.lean
Papers/TbsPrteOptimalTransport/TDiscreteReduction.lean
Papers/TbsPrteOptimalTransport/TDmlNormality.lean
Papers/TbsPrteOptimalTransport/TJSpecialization.lean
Papers/TbsPrteOptimalTransport/TSharpness.lean
Papers/TbsPrteOptimalTransport.lean
Papers.lean
README.md
Toolkit/Foundations/Analysis/Calculus/AbsolutelyContinuous.lean
Toolkit/Foundations/Probability/Conditioning/FiniteValuedConditionalExpectation.lean
Toolkit/Tricks/Probability/Moments/ClippedCouplings.lean
Toolkit/Tricks/Probability/Moments/ProductCouplingBounds.lean
Toolkit/Tricks/Probability/Moments/QuantileVersions.lean
Toolkit/Tricks/Probability/Moments/SymmetricClipping.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