230 proof lines with ≥ 11 declarations, reconstructed as dependency
graphs over the atomic Lean corpus — no files were moved. Click a row to open the
diagram; inside it, click any node to open that .lean file in VS Code.
Node colour: theorem axiom def lemma structure/class
| Decls | Kind | Proof narrative | Root source |
|---|---|---|---|
| 176 | theorem | matrix_bernstein_rect | Statlib/HighDim/Concentration/MatrixBernstein.lean:4216 |
| 146 | theorem | matrix_bernstein | Statlib/HighDim/Concentration/MatrixBernstein.lean:4078 |
| 130 | theorem | wedin_sin_theta | Statlib/HighDim/MatrixAnalysis/WedinSinTheta.lean:3225 |
| 115 | theorem | gaussian_lipschitz_concentration | Statlib/StatFoundation/RandomVariable/Gaussian/LipschitzConcentration.lean:606 |
| 112 | theorem | subgaussian_design_l1RSE_from_final_tau_eps_cover_budget | Statlib/HighDim/Regression/L1RSEFromCovariance.lean:229 |
| 107 | theorem | standardGaussian_logSobolev_lipschitz_euclidean | Statlib/StatFoundation/RandomVariable/Gaussian/LogSobolev.lean:35887 |
| 91 | theorem | subgaussian_design_l1RSE_from_sparse_ball_oracle_final_rate | Statlib/HighDim/Regression/L1RSEFromCovariance.lean:294 |
| 83 | theorem | unit_cube_bspline_high_order_holder_smooth_uniform_sieve_approximation_rate | Statlib/Nonparametric/Approximation/Spline.lean:2361 |
| 81 | theorem | subgaussian_l1_shell_centered_quadratic_deviation_tail_named_event_from_sparse_ball_oracle_certificate | Statlib/HighDim/CovarianceMatrix/L1QuadraticProcess/RadiusFluctuation.lean:4747 |
| 76 | theorem | offdiag_hanson_wright_tail_high_of_const_decoupling_norm_bernstein_absorb | Statlib/HighDim/Concentration/HansonWright.lean:3615 |
| 76 | theorem | subgaussian_design_l1RSE_from_sparse_oracle_final_rate | Statlib/HighDim/Regression/L1RSEFromCovariance.lean:690 |
| 75 | theorem | subgaussian_l1_shell_localized_centered_quadratic_deviation_tail_from_sparse_ball_oracle_certificate | Statlib/HighDim/CovarianceMatrix/L1QuadraticProcess/RadiusFluctuation.lean:4650 |
| 71 | theorem | subgaussian_design_l1RSE_from_entrywise_coordinate_rate_profile | Statlib/HighDim/Regression/L1RSEFromCovariance.lean:598 |
| 70 | theorem | tendsto_measure_debiasedLasso_standardWaldCI_coverage_lyapunov_real | Statlib/HighDim/Regression/DebiasingLasso.lean:2705 |
| 70 | theorem | exists_reluNetworkClass_holderSmoothBall_unitCube_uniform_parameter_count | Statlib/Nonparametric/Approximation/NeuralNetworkAlgebra.lean:13468 |
| 69 | theorem | pca_eigvec_perturbation | Statlib/HighDim/SpectralPerturbation/PCA.lean:32 |
| 68 | theorem | offdiag_hanson_wright_tail_high_of_decoupling_norm_bernstein_absorb | Statlib/HighDim/Concentration/HansonWright.lean:3570 |
| 68 | theorem | tendsto_measure_debiasedLasso_standardWaldCI_coverage_iidScoreSum_real | Statlib/HighDim/Regression/DebiasingLasso.lean:2599 |
| 66 | theorem | offdiag_hanson_wright_tail_high_norm_bernstein_of_const_decoupling | Statlib/HighDim/Concentration/HansonWright.lean:3251 |
| 66 | theorem | exists_reluNetworkClass_holderSmooth_unitCube_approximation | Statlib/Nonparametric/Approximation/NeuralNetworkAlgebra.lean:13339 |
| 65 | theorem | tendsto_measure_debiasedLasso_standardWaldCI_coverage_lindebergFeller_real | Statlib/HighDim/Regression/DebiasingLasso.lean:2517 |
| 64 | theorem | tendstoInDistribution_studentizedDebiasedLasso_coordinate_of_scoreVector_l1_rowApprox_and_se_real | Statlib/HighDim/Regression/DebiasingLasso.lean:371 |
| 63 | theorem | gaussian_quadratic_form_concentration | Statlib/HighDim/Concentration/GaussianQuadraticForm.lean:14 |
| 60 | theorem | exists_reluNetworkClass_holderSmooth_unitCube_approximation_from_exact_grid | Statlib/Nonparametric/Approximation/NeuralNetworkAlgebra.lean:10932 |
| 59 | lemma | decoupled_zeroDiag_quadratic_form_tail_high_norm_bernstein_absorb_of_exponents' | Statlib/HighDim/Concentration/HansonWright.lean:2697 |
| 59 | theorem | standardPi_logSobolev_smooth_finiteFisher | Statlib/StatFoundation/RandomVariable/Gaussian/LogSobolev.lean:11830 |
| 58 | theorem | frobenius_norm_sq_subgaussian_concentration | Statlib/HighDim/Concentration/FrobeniusNormSqConcentration.lean:21 |
| 58 | theorem | unit_cube_bspline_trace_zero_order_uniform_sieve_holder_approximation_rate | Statlib/Nonparametric/Approximation/Spline.lean:804 |
| 58 | theorem | unit_cube_bspline_trace_zero_order_uniform_sieve_holder_approximation_rate_explicit | Statlib/Nonparametric/Approximation/Spline.lean:859 |
| 56 | theorem | zeroDiag_centered_quadratic_form_tail_high_of_decoupling_norm_bernstein_absorb | Statlib/HighDim/Concentration/HansonWright.lean:3304 |
| 56 | theorem | hanson_wright_of_const_decoupling_norm_bernstein_absorb_of_exponents | Statlib/HighDim/Concentration/HansonWright.lean:4612 |
| 56 | theorem | tendstoInDistribution_debiasedLasso_scaledCenteredCoordinate_of_iid_scoreSum_and_l1_rowApprox_real | Statlib/HighDim/Regression/DebiasingLasso.lean:804 |
| 56 | theorem | tendstoInDistribution_debiasedLasso_scaledCenteredCoordinate_of_lyapunov_scoreArray_and_l1_rowApprox_real | Statlib/HighDim/Regression/DebiasingLasso.lean:938 |
| 56 | theorem | exists_reluNetworkClass_holderSmooth_axisAligned_tent_partition_approximation_on_domain_bound | Statlib/Nonparametric/Approximation/NeuralNetworkAlgebra.lean:8657 |
| 55 | theorem | subgaussian_l1_shell_centered_quadratic_deviation_tail_from_interval_endpoint_inputs | Statlib/HighDim/CovarianceMatrix/L1QuadraticProcess/RadiusFluctuation.lean:2923 |
| 55 | theorem | subgaussian_l1_shell_localized_centered_quadratic_deviation_tail_from_entrywise_l1_cover_certificate | Statlib/HighDim/CovarianceMatrix/L1QuadraticProcess/RadiusFluctuation.lean:4551 |
| 55 | theorem | tendstoInDistribution_debiasedLasso_scaledCenteredFiniteCoordinate_of_scoreVector_and_l1_rowApprox_real | Statlib/HighDim/Regression/DebiasingLasso.lean:323 |
| 54 | theorem | unit_cube_bspline_uniform_sieve_holder_approximation_rate | Statlib/Nonparametric/Approximation/Spline.lean:226 |
| 52 | theorem | subgaussian_l1_shell_localized_centered_quadratic_deviation_tail_from_rademacher_profile_certificate | Statlib/HighDim/CovarianceMatrix/L1QuadraticProcess/RadiusFluctuation.lean:4025 |
| 49 | theorem | tensor_product_positive_degree_bspline_holder_smooth_approximation_bound_of_projection_error | Statlib/Nonparametric/Approximation/Spline.lean:1395 |
| 48 | theorem | haar_wavelet_zero_order_uniform_sieve_holder_approximation_rate_of_projection_error | Statlib/Nonparametric/Approximation/Wavelet.lean:655 |
| 47 | theorem | tensor_product_linear_bspline_holder_smooth_approximation_bound_of_projection_error | Statlib/Nonparametric/Approximation/Spline.lean:1330 |
| 46 | theorem | tensor_product_positive_degree_bspline_holder_smooth_approximation_bound_of_projection_rate | Statlib/Nonparametric/Approximation/Spline.lean:1366 |
| 46 | theorem | tendstoInDistribution_studentizedScaledCenteredCoordinate_of_coordinatewise_remainder_isBigOInProbability_real | Statlib/StatFoundation/Convergence/AnalysisTools/AsymptoticLinear.lean:125 |
| 44 | theorem | subgaussian_l1_shell_localized_centered_quadratic_deviation_tail_from_entrywise_good_cover | Statlib/HighDim/CovarianceMatrix/L1QuadraticProcess.lean:7053 |
| 43 | theorem | subgaussian_rip_sample_complexity | Statlib/HighDim/Geometry/RIPConstruction.lean:1626 |
| 43 | theorem | trace_exp_add_log_simpleFunc_jensen_posDef | Statlib/HighDim/MatrixAnalysis/LiebTraceConcavity.lean:198 |
| 43 | theorem | exists_reluNetworkClass_holderSmooth_local_approx_on_centered_box_with_symbolic_budget | Statlib/Nonparametric/Approximation/NeuralNetworkAlgebra.lean:6250 |
| 43 | theorem | finite_holderSmooth_local_table_reluNetworkClass_active_cell_error_bound | Statlib/Nonparametric/Approximation/NeuralNetworkAlgebra.lean:8483 |
| 42 | theorem | rkhsBall_rademacher_complexity_dudley_le | Statlib/Nonparametric/Approximation/RKHS.lean:3126 |
| 41 | theorem | hanson_wright_tail_high_of_offdiag_tail | Statlib/HighDim/Concentration/HansonWright.lean:4127 |
| 41 | theorem | tensor_product_extended_bspline_holder_smooth_approximation_rate_of_projection_error | Statlib/Nonparametric/Approximation/Spline.lean:1582 |
| 39 | theorem | golden_thompson | Statlib/HighDim/MatrixAnalysis/GoldenThompson.lean:1018 |
| 39 | theorem | finite_axisAlignedBoxTentWeight_common_fixed_width_depth_rate_from_mul_gadget | Statlib/Nonparametric/Approximation/NeuralNetworkAlgebra.lean:19658 |
| 39 | theorem | dyadic_wavelet_high_order_holder_smooth_uniform_sieve_approximation_rate_of_projection_error | Statlib/Nonparametric/Approximation/Wavelet.lean:494 |
| 39 | theorem | mle_asymptotically_efficient | Statlib/StatFoundation/Statistics/Estimation/MultiParameter.lean:1331 |
| 38 | lemma | decoupledOffDiagQuadForm_prod_tail_le_markov_plus_good_ofReal | Statlib/HighDim/Concentration/HansonWright.lean:1086 |
| 38 | theorem | lrt_statistic_asymptotic_chisq1 | Statlib/HypothesisTesting/Asymptotic/ChiSquareAsymptotics.lean:1052 |
| 38 | theorem | exists_fullyConnectedReLUNet_holderSmooth_local_approx_on_centered_box_with_depth_bound | Statlib/Nonparametric/Approximation/NeuralNetworkAlgebra.lean:6168 |
| 38 | theorem | dyadic_wavelet_high_order_holder_smooth_uniform_sieve_approximation_rate_of_projection_certificate | Statlib/Nonparametric/Approximation/Wavelet.lean:456 |
| 36 | theorem | t_statistic_asymptotic_normal | Statlib/HypothesisTesting/Asymptotic/TTestAsymptotic.lean:45 |
| 35 | theorem | rank_constrained_denoising_frobenius_bound | Statlib/HighDim/MatrixRecovery/RankConstrainedDenoising.lean:2203 |
| 35 | theorem | exists_fullyConnectedReLUNet_holderSmooth_local_approx_on_centered_box | Statlib/Nonparametric/Approximation/NeuralNetworkAlgebra.lean:6096 |
| 34 | theorem | wald_statistic_asymptotic_chisq1 | Statlib/HypothesisTesting/Asymptotic/ChiSquareAsymptotics.lean:548 |
| 34 | theorem | tensor_product_spline_sieve_holder_smooth_approximation_exact_basis_count_of_projection_certificate | Statlib/Nonparametric/Approximation/Spline.lean:1130 |
| 34 | theorem | wavelet_sieve_holder_smooth_approximation_exact_basis_count_of_projection_certificate | Statlib/Nonparametric/Approximation/Wavelet.lean:277 |
| 33 | theorem | subgaussian_l1_shell_centered_quadratic_deviation_tail_named_event_from_coordinate_rate | Statlib/HighDim/CovarianceMatrix/L1QuadraticProcess/RadiusFluctuation.lean:4284 |
| 33 | theorem | linear_combination_clt_to_finiteLinearCombination | Statlib/StatFoundation/Convergence/CentralLimitTheorem/FiniteLinearCombination.lean:26 |
| 32 | lemma | decoupledOffDiagQuadForm_prod_tail_le_lintegral_frobenius | Statlib/HighDim/Concentration/HansonWright.lean:929 |
| 32 | theorem | finite_holderSmooth_local_table_reluNetworkClass_fixed_width_active_cell_error_and_domain_output_bound_from_mul_gadget | Statlib/Nonparametric/Approximation/NeuralNetworkAlgebra.lean:23672 |
| 32 | theorem | unitCubeBSplineTensorDual_exists_sub_reproduction_degreeSucc_localStability | Statlib/Nonparametric/Approximation/SplineFacts.lean:6263 |
| 31 | theorem | exists_fullyConnectedReLUNet_taylor_polynomial_approx_on_centered_box_with_depth_bound | Statlib/Nonparametric/Approximation/NeuralNetworkAlgebra.lean:6135 |
| 31 | theorem | unit_cube_haar_selector_positive_holder_uniform_sieve_approximation_rate | Statlib/Nonparametric/Approximation/Wavelet.lean:802 |
| 31 | theorem | tendsto_covarianceBilin_map_toLp_apply_of_forall_inProbabilityConvergence_of_isUniformIntegrableInLp_two_real | Statlib/StatFoundation/Convergence/AnalysisTools/IntegralConvergence.lean:2960 |
| 30 | lemma | decoupledOffDiagQuadForm_prod_tail_le_lintegral_spectral | Statlib/HighDim/Concentration/HansonWright.lean:888 |
| 30 | theorem | hard_sv_threshold_is_rank_constrained_minimizer | Statlib/HighDim/MatrixAnalysis/HardSvThreshold.lean:21 |
| 30 | theorem | tendsto_inner_covariance_matrix_toEuclideanCLM_of_forall_inProbabilityConvergence_of_isUniformIntegrableInLp_two_real | Statlib/StatFoundation/Convergence/AnalysisTools/IntegralConvergence.lean:2908 |
| 30 | theorem | mestimator_asymptotic_normal_of_linearization | Statlib/StatFoundation/Statistics/Estimation/AsymptoticLinear.lean:197 |
| 29 | theorem | exists_fullyConnectedReLUNet_finite_quadratic_polynomial_approx_on_box | Statlib/Nonparametric/Approximation/NeuralNetworkAlgebra.lean:1047 |
| 29 | theorem | tendsto_norm_covariance_matrix_toEuclideanCLM_of_forall_inProbabilityConvergence_of_isUniformIntegrableInLp_two_real | Statlib/StatFoundation/Convergence/AnalysisTools/IntegralConvergence.lean:2887 |
| 29 | theorem | multivariate_central_limit_theorem | Statlib/StatFoundation/Convergence/CentralLimitTheorem/Multivariate.lean:86 |
| 28 | theorem | mle_asymptotic_normal | Statlib/HypothesisTesting/Asymptotic/ChiSquareAsymptotics.lean:392 |
| 27 | theorem | exists_fullyConnectedReLUNet_quadratic_two_term_approx_on_box | Statlib/Nonparametric/Approximation/NeuralNetworkAlgebra.lean:883 |
| 27 | theorem | tendsto_norm_sub_covariance_matrix_toEuclideanCLM_zero_of_forall_inProbabilityConvergence_of_isUniformIntegrableInLp_two_real | Statlib/StatFoundation/Convergence/AnalysisTools/IntegralConvergence.lean:2862 |
| 27 | theorem | z_estimator_linearization_from_mvt | Statlib/StatFoundation/Statistics/Estimation/AsymptoticLinear.lean:309 |
| 26 | theorem | subgaussian_rip_tail_anisotropic | Statlib/HighDim/Geometry/SubGaussianRIPTailAnisotropic.lean:381 |
| 26 | theorem | unit_cube_selector_indicator_uniform_sieve_holder_approximation_grid_rate | Statlib/Nonparametric/Approximation/Holder.lean:744 |
| 26 | theorem | exists_reluNetworkClass_holderSmooth_unitCube_fixed_width_exact_grid_and_error_budget | Statlib/Nonparametric/Approximation/NeuralNetworkAlgebra.lean:20070 |
| 26 | theorem | exists_reluNetworkClass_holderSmooth_unitCube_fixed_width_exact_grid_explicit_depth_and_error_budget | Statlib/Nonparametric/Approximation/NeuralNetworkAlgebra.lean:22472 |
| 26 | theorem | tendsto_covarianceOperator_map_toLp_toWOT_of_forall_inProbabilityConvergence_of_isUniformIntegrableInLp_two_real | Statlib/StatFoundation/Convergence/AnalysisTools/IntegralConvergence.lean:2773 |
| 26 | theorem | tendsto_covariance_matrix_of_forall_inProbabilityConvergence_of_isUniformIntegrableInLp_two_real | Statlib/StatFoundation/Convergence/AnalysisTools/IntegralConvergence.lean:2818 |
| 26 | theorem | tendsto_covarianceBilin_map_toLp_basisFun_of_forall_inProbabilityConvergence_of_isUniformIntegrableInLp_two_real | Statlib/StatFoundation/Convergence/AnalysisTools/IntegralConvergence.lean:2934 |
| 25 | theorem | sample_cov_min_eig_lower | Statlib/HighDim/CovarianceMatrix/SampleCovEigenvalueLower.lean:21 |
| 25 | theorem | sample_cov_max_eig_upper | Statlib/HighDim/CovarianceMatrix/SampleCovEigenvalueUpper.lean:22 |
| 25 | theorem | exists_fullyConnectedReLUNet_product_of_depth_one_approximants_on_box | Statlib/Nonparametric/Approximation/NeuralNetworkAlgebra.lean:1144 |
| 25 | theorem | exists_reluNetworkClass_mul_fixed_width_depth_rate_on_box | Statlib/Nonparametric/Approximation/NeuralNetworkAlgebra.lean:15477 |
| 25 | theorem | exists_reluNetworkClass_finite_centered_monomial_polynomial_fixed_width_depth_rate_from_mul_gadget | Statlib/Nonparametric/Approximation/NeuralNetworkAlgebra.lean:23086 |
| 25 | theorem | unitCubeBSplineTensorDual_polynomialReproduction | Statlib/Nonparametric/Approximation/SplineFacts.lean:2551 |
| 25 | theorem | tendsto_cross_covariance_matrix_of_forall_inProbabilityConvergence_of_isUniformIntegrableInLp_two_real | Statlib/StatFoundation/Convergence/AnalysisTools/IntegralConvergence.lean:2593 |
| 25 | theorem | tendsto_inner_secondMoment_matrix_toEuclideanCLM_of_forall_inProbabilityConvergence_of_isUniformIntegrableInLp_two_real | Statlib/StatFoundation/Convergence/AnalysisTools/IntegralConvergence.lean:2700 |
| 25 | theorem | maxCoord_standardizedPartialSum_tendsto | Statlib/StatFoundation/Convergence/CentralLimitTheorem/MaxType.lean:241 |
| 25 | theorem | maxAbsCoord_standardizedPartialSum_tendsto | Statlib/StatFoundation/Convergence/CentralLimitTheorem/MaxType.lean:265 |
| 24 | theorem | fischer_inequality | Statlib/HighDim/MatrixAnalysis/Fischer.lean:13 |
| 24 | theorem | selector_indicator_uniform_sieve_holder_approximation_rate_of_cover | Statlib/Nonparametric/Approximation/Holder.lean:498 |
| 24 | theorem | tendsto_norm_secondMoment_matrix_toEuclideanCLM_of_forall_inProbabilityConvergence_of_isUniformIntegrableInLp_two_real | Statlib/StatFoundation/Convergence/AnalysisTools/IntegralConvergence.lean:2681 |
| 24 | theorem | tendsto_covarianceOperator_map_toLp_inner_of_forall_inProbabilityConvergence_of_isUniformIntegrableInLp_two_real | Statlib/StatFoundation/Convergence/AnalysisTools/IntegralConvergence.lean:2750 |
| 24 | theorem | multiplierBootstrap_conditional_clt | Statlib/StatFoundation/Convergence/Resampling/BootstrapInterface.lean:814 |
| 23 | theorem | subgaussian_l1_shell_localized_centered_quadratic_deviation_tail_from_cover_certificate | Statlib/HighDim/CovarianceMatrix/L1QuadraticProcess.lean:7259 |
| 23 | theorem | l1_shell_localized_centered_tail_from_process_metric_good_cover_certificate_absorbed | Statlib/HighDim/CovarianceMatrix/L1QuadraticProcess/RadiusFluctuation.lean:1740 |
| 23 | theorem | l1_shell_localized_centered_tail_from_shifted_process_metric_good_cover_certificate_absorbed | Statlib/HighDim/CovarianceMatrix/L1QuadraticProcess/RadiusFluctuation.lean:1821 |
| 23 | theorem | l1_shell_localized_centered_tail_from_shifted_process_metric_components_absorbed | Statlib/HighDim/CovarianceMatrix/L1QuadraticProcess/RadiusFluctuation.lean:1914 |
| 23 | theorem | fixed_design_lasso_oracle_of_l1RSE | Statlib/HighDim/Regression/LassoRSEOracle.lean:23 |
| 23 | theorem | exists_selector_indicator_sieve_holder_approximation_bound | Statlib/Nonparametric/Approximation/Holder.lean:352 |
| 23 | theorem | finite_axisAligned_tent_weighted_local_reluNetworkClass_global_error_bound | Statlib/Nonparametric/Approximation/NeuralNetworkAlgebra.lean:8203 |
| 22 | theorem | unitCubePositiveDegreeExtendedBSplineSystem_support_radius_degree_plus_two_div | Statlib/Nonparametric/Approximation/SplineFacts.lean:2164 |
| 22 | theorem | tendsto_norm_sub_secondMoment_matrix_toEuclideanCLM_zero_of_forall_inProbabilityConvergence_of_isUniformIntegrableInLp_two_real | Statlib/StatFoundation/Convergence/AnalysisTools/IntegralConvergence.lean:2657 |
| 22 | theorem | tendsto_covarianceOperator_map_toLp_basisFun_inner_of_forall_inProbabilityConvergence_of_isUniformIntegrableInLp_two_real | Statlib/StatFoundation/Convergence/AnalysisTools/IntegralConvergence.lean:2724 |
| 21 | lemma | isotropic_norm_concentration | Statlib/HighDim/CovarianceMatrix/Properties.lean:761 |
| 21 | theorem | svSoftThreshold_frobenius_non_expansive | Statlib/HighDim/MatrixAnalysis/SvSoftThreshold.lean:886 |
| 21 | theorem | standardizedPartialSumVec_tendstoInDistribution | Statlib/StatFoundation/Convergence/CentralLimitTheorem/MaxType.lean:224 |
| 21 | theorem | integral_hermite_normalized_mul_eq | Statlib/StatFoundation/RandomVariable/Gaussian/Hermite.lean:226 |
| 20 | theorem | l1_shell_localized_centered_deviation_tail_from_fixed_direction_cover_absorbed | Statlib/HighDim/CovarianceMatrix/L1QuadraticProcess.lean:3635 |
| 20 | theorem | tendsto_norm_integral_continuousLinearMap_sub_zero_of_inProbabilityConvergence_ui | Statlib/StatFoundation/Convergence/AnalysisTools/IntegralConvergence.lean:187 |
| 20 | theorem | momentConvergence_one_of_inProbabilityConvergence_of_isUniformIntegrable | Statlib/StatFoundation/Convergence/AnalysisTools/IntegralConvergence.lean:280 |
| 20 | theorem | tendsto_secondMoment_matrix_of_forall_inProbabilityConvergence_of_isUniformIntegrableInLp_two_real | Statlib/StatFoundation/Convergence/AnalysisTools/IntegralConvergence.lean:2618 |
| 20 | theorem | empirical_process_dudley_bound | Statlib/StatFoundation/EmpiricalProcess/DudleyRademacher.lean:1085 |
| 19 | theorem | offdiag_hanson_wright_tail_high_of_const_decoupling_norm_bernstein_absorb_of_exponents' | Statlib/HighDim/Concentration/HansonWright.lean:3746 |
| 19 | theorem | offdiag_hanson_wright_tail_high_of_const_decoupling_absorb | Statlib/HighDim/Concentration/HansonWright.lean:3852 |
| 19 | theorem | haar_wavelet_zero_order_holder_projection_rate_of_cell_selector | Statlib/Nonparametric/Approximation/Wavelet.lean:574 |
| 18 | lemma | diagQuadForm_centered_tail_bernstein_explicit | Statlib/HighDim/Concentration/HansonWright.lean:2247 |
| 18 | theorem | cov_trace_concentration | Statlib/HighDim/CovarianceMatrix/CovTraceConcentration.lean:37 |
| 18 | theorem | weyl_product_inequality | Statlib/HighDim/MatrixAnalysis/Weyl.lean:21 |
| 18 | theorem | exists_fullyConnectedReLUNet_unitInterval_square_approx | Statlib/Nonparametric/Approximation/NeuralNetworkAlgebra.lean:231 |
| 18 | theorem | holderSmoothBall_unitCube_epsilon_rate_from_M_rate | Statlib/Nonparametric/Approximation/NeuralNetworkAlgebra.lean:13633 |
| 18 | theorem | finite_axisAligned_tent_weighted_local_products_fixed_width_depth_sum_bound | Statlib/Nonparametric/Approximation/NeuralNetworkAlgebra.lean:19797 |
| 18 | theorem | tensor_product_extended_bspline_holder_smooth_projection_rate_of_projection_error | Statlib/Nonparametric/Approximation/Spline.lean:1474 |
| 18 | theorem | tendsto_norm_integral_sub_zero_of_inProbabilityConvergence_of_isUniformIntegrable | Statlib/StatFoundation/Convergence/AnalysisTools/IntegralConvergence.lean:84 |
| 18 | theorem | tendsto_integral_continuousLinearMap_of_inProbabilityConvergence_of_isUniformIntegrable | Statlib/StatFoundation/Convergence/AnalysisTools/IntegralConvergence.lean:170 |
| 18 | theorem | tendsto_pairwise_integral_mul_cross_of_forall_inProbabilityConvergence_of_isUniformIntegrableInLp_two_real | Statlib/StatFoundation/Convergence/AnalysisTools/IntegralConvergence.lean:2549 |
| 17 | theorem | offdiag_hanson_wright_tail_high_of_const_decoupling_and_decoupled_tail | Statlib/HighDim/Concentration/HansonWright.lean:3813 |
| 17 | lemma | l1_shell_bad_event_subset_large_coordinate_event_of_subgaussian_covariance | Statlib/HighDim/CovarianceMatrix/L1QuadraticProcess.lean:3239 |
| 17 | theorem | lasso_oracle_support_l2_of_uniformRE | Statlib/HighDim/Regression/LassoOracle.lean:1013 |
| 17 | theorem | lasso_oracle_l2_of_uniformRE | Statlib/HighDim/Regression/LassoOracle.lean:1028 |
| 17 | lemma | sampleSecondMoment_lower_to_SatisfiesUniformSupportRE | Statlib/HighDim/Regression/SampleCovarianceDesignBridge.lean:222 |
| 17 | lemma | sampleSecondMoment_cone_lower_to_SatisfiesSupportRE | Statlib/HighDim/Regression/SampleCovarianceDesignBridge.lean:256 |
| 17 | theorem | two_sample_t_confidence_interval | Statlib/HypothesisTesting/Inference/NormalTheoryConfidence.lean:262 |
| 17 | theorem | holderSmoothBall_unitCube_LW2_rate_from_fixed_width_M_rate | Statlib/Nonparametric/Approximation/NeuralNetworkAlgebra.lean:22519 |
| 17 | theorem | tensor_product_linear_bspline_holder_projection_rate_of_local_partition | Statlib/Nonparametric/Approximation/Spline.lean:1286 |
| 17 | theorem | tendsto_integral_of_inProbabilityConvergence_of_isUniformIntegrableInLp_two | Statlib/StatFoundation/Convergence/AnalysisTools/IntegralConvergence.lean:2483 |
| 17 | theorem | standardReal_ou_mehler_basic | Statlib/StatFoundation/RandomVariable/Gaussian/LogSobolev.lean:2089 |
| 16 | lemma | l1_shell_bad_event_subset_large_coordinate_centered_event_of_subgaussian_covariance | Statlib/HighDim/CovarianceMatrix/L1QuadraticProcess.lean:3312 |
| 16 | theorem | lasso_oracle_prediction_of_uniformRE | Statlib/HighDim/Regression/LassoOracle.lean:645 |
| 16 | theorem | lasso_oracle_l1_of_uniformRE | Statlib/HighDim/Regression/LassoOracle.lean:892 |
| 16 | theorem | one_sample_t_confidence_interval | Statlib/HypothesisTesting/Inference/NormalTheoryConfidence.lean:121 |
| 16 | theorem | holderSmoothBall_unitCube_LM2_rate_from_M_rate | Statlib/Nonparametric/Approximation/NeuralNetworkAlgebra.lean:19952 |
| 16 | theorem | holderSmoothBall_unitCube_fixed_width_M_rate_from_exact_grid | Statlib/Nonparametric/Approximation/NeuralNetworkAlgebra.lean:20119 |
| 16 | theorem | kernel_regression_risk_integrability_of_centered_sum_bias_and_design_l2 | Statlib/Nonparametric/KernelRegression/KernelRate.lean:1049 |
| 16 | theorem | tendsto_integral_of_inProbabilityConvergence_of_isUniformIntegrable | Statlib/StatFoundation/Convergence/AnalysisTools/IntegralConvergence.lean:68 |
| 16 | theorem | tendsto_norm_covariance_matrix_toEuclideanCLM_of_forall_inLpConvergence_two_real | Statlib/StatFoundation/Convergence/AnalysisTools/IntegralConvergence.lean:2365 |
| 16 | theorem | inProbabilityConvergence_add_of_isBigOInProbability_tendsto_zero_right | Statlib/StatFoundation/Convergence/AnalysisTools/StochasticOrder/ConvergenceBridges.lean:449 |
| 16 | theorem | integral_deriv_mul_hermite_normalized | Statlib/StatFoundation/RandomVariable/Gaussian/Hermite.lean:407 |
| 15 | theorem | dseparated_symm | Statlib/Causal/SCM/Theorems.lean:1505 |
| 15 | theorem | unitCubePositiveDegreeExtendedBSplineBasis_continuous | Statlib/Nonparametric/Approximation/SplineFacts.lean:2139 |
| 15 | theorem | cramer_wold_iff | Statlib/StatFoundation/Convergence/AnalysisTools/CramerWold.lean:332 |
| 15 | theorem | tendstoInDistribution_iff_forall_inner_real | Statlib/StatFoundation/Convergence/AnalysisTools/CramerWold.lean:390 |
| 15 | theorem | inProbabilityConvergence_add_of_isBigOInProbability_tendsto_zero_left | Statlib/StatFoundation/Convergence/AnalysisTools/StochasticOrder/ConvergenceBridges.lean:437 |
| 15 | theorem | isLittleOInProbability_mul_of_isBigOInProbability_tendsto_zero_left | Statlib/StatFoundation/Convergence/AnalysisTools/StochasticOrder/SlutskyProduct.lean:45 |
| 15 | theorem | isLittleOInProbability_mul_of_isBigOInProbability_tendsto_zero_right | Statlib/StatFoundation/Convergence/AnalysisTools/StochasticOrder/SlutskyProduct.lean:57 |
| 14 | theorem | gformula_marginal_non_ancestor | Statlib/Causal/SCM/Theorems.lean:696 |
| 14 | lemma | decoupledOffDiagQuadForm_prod_first_section_abs_tail_real | Statlib/HighDim/Concentration/HansonWright.lean:142 |
| 14 | lemma | l1_shell_scale_bad_measure_le_exp_card_tail_of_matrix_entrywise_good_cover_two_caps | Statlib/HighDim/CovarianceMatrix/L1QuadraticProcess/RadiusFluctuation.lean:1145 |
| 14 | theorem | rank1_top_singular_vector_recovery | Statlib/HighDim/MatrixRecovery/RankOneSpectralInitialization.lean:14 |
| 14 | theorem | lasso_oracle_support_l2_of_uniformSupportRE | Statlib/HighDim/Regression/LassoOracle.lean:950 |
| 14 | theorem | paired_t_test | Statlib/HypothesisTesting/Inference/NormalTheoryConfidence.lean:440 |
| 14 | theorem | kernel_smoother_classApproximationError_le_of_holder_bias_member | Statlib/Nonparametric/Approximation/Kernel.lean:223 |
| 14 | theorem | kernel_smoother_classApproximationError_le_of_holder_bias_rate | Statlib/Nonparametric/Approximation/Kernel.lean:265 |
| 14 | theorem | reluNetworkClass_classApproximationError_le_of_pointwise_candidate | Statlib/Nonparametric/Approximation/NeuralNetwork.lean:11 |
| 14 | theorem | reluNetworkClass_classApproximationError_le_of_exists_pointwise | Statlib/Nonparametric/Approximation/NeuralNetwork.lean:72 |
| 14 | theorem | inProbabilityConvergence_iff_isLittleOInProbability_sub | Statlib/StatFoundation/Convergence/AnalysisTools/StochasticOrder/ConvergenceBridges.lean:327 |
| 14 | theorem | inProbabilityConvergence_sub_of_isBigOInProbability_tendsto_zero_left | Statlib/StatFoundation/Convergence/AnalysisTools/StochasticOrder/ConvergenceBridges.lean:462 |
| 14 | theorem | inProbabilityConvergence_sub_of_isBigOInProbability_tendsto_zero_right | Statlib/StatFoundation/Convergence/AnalysisTools/StochasticOrder/ConvergenceBridges.lean:475 |
| 14 | theorem | isTightMeasureSet_range_map_of_isBigOInProbability_tendsto_zero_finiteDimensional | Statlib/StatFoundation/Convergence/AnalysisTools/Tightness.lean:416 |
| 14 | theorem | isTightMeasureSet_range_map_of_isLittleOInProbability_rate_isBigO_one_finiteDimensional | Statlib/StatFoundation/Convergence/AnalysisTools/Tightness.lean:488 |
| 14 | theorem | uniform_strong_law | Statlib/StatFoundation/Convergence/LawOfLargeNumbers/UniformStrongLaw.lean:408 |
| 14 | theorem | bootstrap_coverage_from_distance_and_anticonc | Statlib/StatFoundation/Convergence/Resampling/BootstrapInterface.lean:143 |
| 14 | theorem | mle_asymptotic_normal | Statlib/StatFoundation/Statistics/Estimation/MLE.lean:164 |
| 13 | theorem | induced_family_do_bridge | Statlib/Causal/SCM/Theorems.lean:465 |
| 13 | theorem | lasso_oracle_prediction_of_uniformSupportRE | Statlib/HighDim/Regression/LassoOracle.lean:613 |
| 13 | theorem | lasso_oracle_l1_of_uniformSupportRE | Statlib/HighDim/Regression/LassoOracle.lean:862 |
| 13 | theorem | variance_ratio_confidence_interval | Statlib/HypothesisTesting/NormalTheory/VarianceTest.lean:2617 |
| 13 | theorem | reluNetworkClass_classApproximationError_le_of_candidate_ise | Statlib/Nonparametric/Approximation/NeuralNetwork.lean:46 |
| 13 | theorem | rkhsBall_classApproximationError_le_of_exists_pointwise | Statlib/Nonparametric/Approximation/RKHS.lean:187 |
| 13 | theorem | exists_uniform_sieve_approximation_error_bound_of_pointwise_series_approximation | Statlib/Nonparametric/Approximation/Sieve.lean:360 |
| 13 | theorem | tensorProductPositiveDegreeBSplineBasis_nonneg | Statlib/Nonparametric/Approximation/SplineFacts.lean:1997 |
| 13 | theorem | inProbabilityConvergence_continuousLinearMap_of_isBigOInProbability_tendsto_zero | Statlib/StatFoundation/Convergence/AnalysisTools/StochasticOrder/ConvergenceBridges.lean:488 |
| 13 | theorem | inProbabilityConvergence_norm_of_isBigOInProbability_tendsto_zero | Statlib/StatFoundation/Convergence/AnalysisTools/StochasticOrder/ConvergenceBridges.lean:502 |
| 13 | theorem | isTightMeasureSet_range_map_of_isBigOInProbability_tendsto_zero_real | Statlib/StatFoundation/Convergence/AnalysisTools/Tightness.lean:393 |
| 13 | theorem | isTightMeasureSet_range_map_of_isBigOInProbability_tendsto_zero_proper | Statlib/StatFoundation/Convergence/AnalysisTools/Tightness.lean:403 |
| 13 | theorem | isTightMeasureSet_range_map_of_isLittleOInProbability_rate_isBigO_one_real | Statlib/StatFoundation/Convergence/AnalysisTools/Tightness.lean:465 |
| 13 | theorem | isTightMeasureSet_range_map_of_isLittleOInProbability_rate_isBigO_one_proper | Statlib/StatFoundation/Convergence/AnalysisTools/Tightness.lean:475 |
| 13 | theorem | hermite_span_dense_L2_standard | Statlib/StatFoundation/RandomVariable/Gaussian/Hermite.lean:684 |
| 12 | lemma | coord_mul_scaled_subexponential_exists_of_indep | Statlib/HighDim/Concentration/HansonWright.lean:1880 |
| 12 | theorem | hp_jensen_mul_log | Statlib/HighDim/MatrixAnalysis/HansenPedersenJensenMulLog.lean:1300 |
| 12 | theorem | variance_ratio_test_size | Statlib/HypothesisTesting/NormalTheory/VarianceTest.lean:2874 |
| 12 | theorem | selector_indicator_holder_class_approximation_error_le_rate | Statlib/Nonparametric/Approximation/Holder.lean:522 |
| 12 | theorem | rkhsBall_coveringNumber_le_of_domainCover | Statlib/Nonparametric/Approximation/RKHS.lean:419 |
| 12 | theorem | tensorProductPositiveDegreeExtendedBSplineBasis_ne_zero_imp_coord_scaled_mem_Ioo | Statlib/Nonparametric/Approximation/SplineFacts.lean:1198 |
| 12 | theorem | haarScalingWaveletSystem_isMeasurable | Statlib/Nonparametric/Approximation/WaveletFacts.lean:32 |
| 12 | theorem | kernel_centered_sum_integrability_of_summand_l2_and_variance_bound | Statlib/Nonparametric/KernelRegression/KernelRate.lean:571 |
| 12 | theorem | kernel_centered_mse_bound_of_uniform_design_interior_bounded | Statlib/Nonparametric/KernelRegression/KernelRate.lean:1235 |
| 12 | theorem | kernel_regression_bias_ise_bound | Statlib/Nonparametric/KernelRegression/KernelRate.lean:1434 |
| 12 | structure | KernelRegressionUniformInteriorWellposednessAssumptions | Statlib/Nonparametric/Vocabulary/KernelRegression.lean:247 |
| 12 | theorem | tendsto_covariance_matrix_of_forall_inLpConvergence_two_real | Statlib/StatFoundation/Convergence/AnalysisTools/IntegralConvergence.lean:2303 |
| 12 | theorem | tendstoInDistribution_sub_of_isBigOInProbability_tendsto_zero_right | Statlib/StatFoundation/Convergence/AnalysisTools/StochasticOrder/ConvergenceBridges.lean:655 |
| 11 | lemma | coord_sq_centered_mgf_bound | Statlib/HighDim/Concentration/HansonWright.lean:1931 |
| 11 | lemma | coord_sq_centered_scaled_mgf_bound_explicit | Statlib/HighDim/Concentration/HansonWright.lean:1972 |
| 11 | lemma | rip_cross_term_abs_le_half_delta_sum | Statlib/HighDim/Geometry/RIPConstruction.lean:223 |
| 11 | lemma | restrictByEquiv_subgaussian | Statlib/HighDim/Geometry/RIPConstruction.lean:453 |
| 11 | lemma | sampleSecondMoment_upper_to_column_bound | Statlib/HighDim/Regression/SampleCovarianceDesignBridge.lean:278 |
| 11 | theorem | t_test_consistent | Statlib/HypothesisTesting/Asymptotic/TTestAsymptotic.lean:542 |
| 11 | theorem | finite_grid_selector_indicator_local_reluNetworkClass_approximation_bound | Statlib/Nonparametric/Approximation/NeuralNetworkAlgebra.lean:6665 |
| 11 | theorem | finite_linear_span_class_approximation_error_le_of_pointwise_series_approximation | Statlib/Nonparametric/Approximation/Sieve.lean:209 |
| 11 | noncomputable def | realize | Statlib/Nonparametric/Vocabulary/NeuralNetwork.lean:192 |
| 11 | theorem | tendsto_norm_secondMoment_matrix_toEuclideanCLM_of_forall_inLpConvergence_two_real | Statlib/StatFoundation/Convergence/AnalysisTools/IntegralConvergence.lean:2064 |
| 11 | theorem | tendstoInDistribution_sub_of_isLittleOInProbability_rate_isBigO_one_right | Statlib/StatFoundation/Convergence/AnalysisTools/StochasticOrder/ConvergenceBridges.lean:745 |
| 11 | theorem | tendstoInDistribution_sub_of_isBigOInProbability_tendsto_zero_left | Statlib/StatFoundation/Convergence/AnalysisTools/StochasticOrder/ConvergenceBridges.lean:772 |
| 11 | theorem | isTightMeasureSet_range_map_of_isBigOInProbability_rate_isBigO_one_finiteDimensional | Statlib/StatFoundation/Convergence/AnalysisTools/Tightness.lean:452 |
| 11 | theorem | hasUniformlyAbsolutelyContinuousIntegral_of_inLpConvergence_one | Statlib/StatFoundation/Convergence/AnalysisTools/UniformIntegrability.lean:192 |
| 11 | theorem | subgaussian_prod_subexponential | Statlib/StatFoundation/RandomVariable/SubExponential/subgaussian_prod_subexponential.lean:27 |
| 11 | theorem | basu_indepFun | Statlib/StatFoundation/Statistics/Sufficiency/Basu.lean:50 |
