All declarations

The 3,077 exported lemmas, theorems and definitions of both packages, in alphabetical order. Section-local Let definitions, Local declarations, instances and canonical structures are listed on their module pages only.

ABCDEFGHIJKLMNOPQRSTUVWXY

A49

• A_sym SKGap/Poincare.v
• abel_ge0 matrix/von_neumann.v
• abel_ge0_sum0 matrix/von_neumann.v
• add_clause RandomSAT/Model.v
• add_clause0 RandomSAT/Model.v
• add_clause_mono RandomSAT/Model.v
• add_clause_sub RandomSAT/Model.v
• add_clauseC RandomSAT/Model.v
• add_gauss_ball_le fourier/small_ball.v
• ae_integrable_tuple_set probability/efron_stein.v
• aext RandomSAT/Forcing.v
• aext0 RandomSAT/Forcing.v
• affine_half SKGap/TwoSpin.v
• affine_half' SKGap/TwoSpin.v
• affine_pos SKGap/TwoSpin.v
• affine_preimage_itv_neg comparison/normal_linear.v
• affine_preimage_itv_pos comparison/normal_linear.v
• alive RandomSAT/Model.v
• alive0 RandomSAT/Model.v
• alive_ge0 RandomSAT/Model.v
• alive_le1 RandomSAT/Model.v
• alive_mono RandomSAT/Model.v
• alive_restrict_le RandomSAT/Pivotal.v
• alive_sqr RandomSAT/Model.v
• all_take_tnth RandomSAT/Model.v
• allnet random_matrix/restricted_isometry.v
• almost_orthogonal_card_le matrix/tensor_packing.v
• almost_orthogonal_sum_le matrix/tensor_packing.v
• alpha random_matrix/restricted_isometry.v
• alpha_ge0 random_matrix/restricted_isometry.v
• atail RandomSAT/Forcing.v
• atail_ext RandomSAT/Forcing.v
• atomless_product_null probability/atoms.v
• atoms probability/atoms.v
• atoms_countable probability/atoms.v
• aux_bil_minmax comparison/escape.v
• aux_cov comparison/escape.v
• aux_mx comparison/escape.v
• aux_mxE comparison/escape.v
• auxg_cov comparison/cgmt.v
• auxg_mx comparison/cgmt.v
• auxg_mxE comparison/cgmt.v
• auxgT_cov comparison/cgmt.v
• auxgT_mx comparison/cgmt.v
• auxgT_mxE comparison/cgmt.v
• auxT_bilT_minmax comparison/escape.v
• auxT_cov comparison/escape.v
• auxT_mx comparison/escape.v
• auxT_mxE comparison/escape.v

B67

• bad_event random_matrix/restricted_isometry.v
• bad_event_le random_matrix/restricted_isometry.v
• ball_le_add_gauss fourier/small_ball.v
• ball_le_cf_rV fourier/charfun_rV.v
• barrier_lindeberg_concentration convex/barrier_lindeberg.v
• barrier_lindeberg_mean convex/barrier_lindeberg.v
• barrier_lindeberg_variance convex/barrier_lindeberg.v
• barrier_removal convex/barrier_removal.v
• barrier_removal_compare convex/barrier_removal.v
• bernoulli_tail probability/countable_mixture.v
• bernstein probability/subgaussian.v
• bernstein random_matrix/wigner.v
• bernstein_basis random_matrix/wigner.v
• bernstein_basis_ge0 random_matrix/wigner.v
• bernstein_lipschitz random_matrix/wigner.v
• bernstein_mean random_matrix/wigner.v
• bernstein_polyE random_matrix/wigner.v
• bernstein_shift random_matrix/wigner.v
• bernstein_sum probability/subgaussian.v
• bernstein_sum1 random_matrix/wigner.v
• bernstein_upper probability/subgaussian.v
• bernstein_var random_matrix/wigner.v
• bessel_mxdot matrix/tensor_packing.v
• big_tuple_distr probability/mixture.v
• bigmax0_contraction1 probability/symmetrization.v
• bigmax0_ge0 probability/symmetrization.v
• bigmax0_pM probability/symmetrization.v
• bigsetU_mem random_matrix/restricted_isometry.v
• bij_tuple_cons probability/finite_mean.v
• bil_aux_max comparison/escape.v
• bil_cov comparison/escape.v
• bil_mx comparison/escape.v
• bil_mxE comparison/escape.v
• bilg_mx comparison/cgmt.v
• bilg_mxE comparison/cgmt.v
• bilin_form_mx convex/self_concordant.v
• bilT_cov comparison/escape.v
• bilT_mx comparison/escape.v
• bilT_mxE comparison/escape.v
• bin_ge_internal RandomSAT/Replacement.v
• bin_le_expR matrix/nets.v
• binom_mean RandomSAT/Forcing.v
• binom_mean_cst RandomSAT/Forcing.v
• binom_mean_id RandomSAT/Forcing.v
• binom_mean_sum RandomSAT/Forcing.v
• binom_mean_trials RandomSAT/Forcing.v
• binom_mean_trials_le RandomSAT/Forcing.v
• binom_meanB RandomSAT/Forcing.v
• binom_meanD RandomSAT/Forcing.v
• binom_meanN RandomSAT/Forcing.v
• binom_meanZ RandomSAT/Forcing.v
• binom_rep_sum_le RandomSAT/Forcing.v
• block_ge_of_double RandomSAT/Replacement.v
• block_set_i SKGap/TwoSpin.v
• block_set_j SKGap/TwoSpin.v
• block_val_i SKGap/TwoSpin.v
• block_val_j SKGap/TwoSpin.v
• bool_diff_sqr RandomSAT/Pivotal.v
• bounded_C3 PerceptronSignDefinitions.v
• bounded_integrable probability/lindeberg.v
• brascamp_lieb comparison/brascamp_lieb_lebesgue.v
• brascamp_lieb_ge0 fourier/small_ball.v
• bregman_div convex/self_concordant.v
• bregman_div_add convex/self_concordant.v
• bsum SKGap/TwoSpin.v
• bsum_plaw SKGap/TwoSpin.v
• budget matrix/nets.v

C386

• cabsent RandomSAT/Model.v
• card_as_sum RandomSAT/Forcing.v
• card_clause RandomSAT/Model.v
• card_clause0 RandomSAT/Model.v
• card_clause0S RandomSAT/Model.v
• card_clause_gt0 RandomSAT/Model.v
• card_clauseSS RandomSAT/Model.v
• card_kills RandomSAT/Replacement.v
• card_large_le matrix/tensor_packing.v
• card_le_cover matrix/tensor_packing.v
• card_set_ord probability/hanson_wright.v
• card_small_sets random_matrix/restricted_isometry.v
• card_supp0 random_matrix/restricted_isometry.v
• card_support RandomSAT/Model.v
• card_support_clause RandomSAT/Replacement.v
• card_support_prepend RandomSAT/Model.v
• cauchy_schwarz probability/efron_stein.v
• ccount random_matrix/restricted_isometry.v
• ccount_ge1 random_matrix/restricted_isometry.v
• ccount_le random_matrix/restricted_isometry.v
• centered_chi2 comparison/chi_square.v
• centered_chi2N comparison/chi_square.v
• cf fourier/charfun.v
• cf_affine fourier/charfun.v
• cf_im fourier/charfun.v
• cf_im0 fourier/charfun.v
• cf_im_image fourier/charfun.v
• cf_im_le1 fourier/charfun.v
• cf_im_normal fourier/charfun.v
• cf_im_normal01 fourier/charfun.v
• cf_image fourier/charfun.v
• cf_imN fourier/charfun.v
• cf_iterated fourier/charfun.v
• cf_norm fourier/charfun.v
• cf_norm0 fourier/charfun.v
• cf_norm_affine fourier/charfun.v
• cf_norm_ge0 fourier/charfun.v
• cf_norm_le1 fourier/charfun.v
• cf_norm_normal fourier/charfun.v
• cf_norm_prod fourier/charfun.v
• cf_norm_sqr_sym fourier/esseen.v
• cf_norm_sym fourier/charfun.v
• cf_norm_tuple_prod fourier/charfun.v
• cf_normal fourier/charfun.v
• cf_normE fourier/charfun.v
• cf_normN fourier/charfun.v
• cf_prod fourier/charfun.v
• cf_prod_integral fourier/charfun.v
• cf_re fourier/charfun.v
• cf_re0 fourier/charfun.v
• cf_re_image fourier/charfun.v
• cf_re_le1 fourier/charfun.v
• cf_re_normal fourier/charfun.v
• cf_re_normal01 fourier/charfun.v
• cf_re_sum_sym fourier/gauss_factor.v
• cf_reN fourier/charfun.v
• cf_rV fourier/charfun_rV.v
• cf_rV_add fourier/charfun_rV.v
• cf_rV_density fourier/inversion.v
• cf_rV_density_ge0 fourier/inversion.v
• cf_rV_density_le fourier/inversion.v
• cf_rV_density_reg fourier/inversion.v
• cf_rV_density_reg0 fourier/inversion.v
• cf_rV_density_regE fourier/inversion.v
• cf_rV_gauss fourier/charfun_rV.v
• cf_rV_im fourier/charfun_rV.v
• cf_rV_im_le1 fourier/charfun_rV.v
• cf_rV_image fourier/charfun_rV.v
• cf_rV_inv_prob fourier/inversion.v
• cf_rV_inv_prob0 fourier/inversion.v
• cf_rV_inv_prob_dominates fourier/inversion.v
• cf_rV_inv_prob_ge0 fourier/inversion.v
• cf_rV_inv_prob_setT fourier/inversion.v
• cf_rV_inv_prob_sigma fourier/inversion.v
• cf_rV_inversion fourier/inversion.v
• cf_rV_kernel fourier/inversion.v
• cf_rV_kernel_le fourier/inversion.v
• cf_rV_law fourier/charfun_rV.v
• cf_rV_norm fourier/charfun_rV.v
• cf_rV_norm_add fourier/charfun_rV.v
• cf_rV_norm_frame fourier/small_ball.v
• cf_rV_norm_gauss fourier/charfun_rV.v
• cf_rV_norm_ge0 fourier/charfun_rV.v
• cf_rV_norm_image fourier/charfun_rV.v
• cf_rV_norm_le1 fourier/charfun_rV.v
• cf_rV_norm_tuple_prod fourier/charfun_rV.v
• cf_rV_re fourier/charfun_rV.v
• cf_rV_re_le1 fourier/charfun_rV.v
• cf_rV_regularization fourier/charfun_rV.v
• cf_rV_regularization_le fourier/charfun_rV.v
• cf_rV_regularized_le fourier/small_ball.v
• cf_rV_tuple_prod fourier/charfun_rV.v
• cf_sym fourier/charfun.v
• cf_sym_law fourier/gauss_factor.v
• cf_tuple_prod fourier/charfun.v
• cf_tuple_prod_integral fourier/charfun.v
• cgmt_aux comparison/cgmt.v
• cgmt_aux_cone_ge comparison/cone_escape.v
• cgmt_aux_cone_zero comparison/cone_escape.v
• cgmt_aux_cone_zero_lt comparison/cone_escape.v
• cgmt_aux_ge comparison/cgmt.v
• cgmt_aux_ge0 comparison/cgmt.v
• cgmt_aux_le comparison/cgmt.v
• cgmt_aux_lipschitz comparison/cgmt.v
• cgmt_aux_mean_zero comparison/cgmt.v
• cgmt_aux_tail comparison/cgmt.v
• cgmt_aux_tr_cone_ge comparison/cone_escape.v
• cgmt_aux_tr_cone_zero comparison/cone_escape.v
• cgmt_aux_tr_set comparison/cgmt.v
• cgmt_auxNl comparison/cgmt.v
• cgmt_escape_tail comparison/cgmt.v
• cgmt_lower comparison/cgmt.v
• cgmt_tail comparison/cgmt.v
• cgmt_upper comparison/cgmt.v
• cgmt_zero_tail comparison/cgmt.v
• char_poly_conj_diag matrix/psd_part.v
• cjoin RandomSAT/Model.v
• cjoin_bij RandomSAT/Model.v
• cjoin_surj RandomSAT/Model.v
• cjoinK RandomSAT/Model.v
• clamp matrix/condition_cone.v
• clamp01_lipschitz probability/small_ball_method.v
• clamp_itv matrix/condition_cone.v
• clause SatVarianceDefinitions.v
• clause_avg RandomSAT/Pivotal.v
• clause_avg_cst RandomSAT/Pivotal.v
• clause_avg_short_survival RandomSAT/Forcing.v
• clause_avg_subr RandomSAT/Forcing.v
• clause_avg_tuple_avg RandomSAT/Forcing.v
• clause_sat SatVarianceDefinitions.v
• clip comparison/gauss_concentration.v
• clip3_bound random_matrix/wigner.v
• clip_abs comparison/gauss_concentration.v
• clip_admissible probability/clip_profile.v
• clip_admissible_ae probability/clip_profile.v
• clip_admissible_ae_integrable probability/clip_profile.v
• clip_admissible_ae_sub probability/clip_profile.v
• clip_admissible_bounded probability/clip_profile.v
• clip_admissible_le probability/clip_profile.v
• clip_ae_admissible probability/clip_profile.v
• clip_ae_eq probability/clip_profile.v
• clip_ae_le probability/clip_profile.v
• clip_ae_objective probability/clip_profile.v
• clip_bound comparison/gauss_concentration.v
• clip_comp_lipschitz random_matrix/wigner.v
• clip_dual probability/clip_profile.v
• clip_dual_ge probability/clip_profile.v
• clip_dual_le probability/clip_profile.v
• clip_dual_lower probability/clip_profile.v
• clip_dual_opt probability/clip_profile.v
• clip_dual_profile probability/clip_profile.v
• clip_dual_window probability/clip_profile.v
• clip_energy probability/variational.v
• clip_energy_C probability/variational.v
• clip_energy_ge0 probability/variational.v
• clip_energy_shift probability/clip_profile.v
• clip_energy_shift_ge0 probability/clip_profile.v
• clip_energy_shift_min probability/clip_profile.v
• clip_energy_shiftE probability/clip_profile.v
• clip_energy_taylor probability/variational.v
• clip_energyE probability/variational.v
• clip_first_order probability/clip_profile.v
• clip_id comparison/gauss_concentration.v
• clip_integrable_bounded probability/clip_profile.v
• clip_integrable_id_bounded probability/clip_profile.v
• clip_integrable_mul probability/clip_profile.v
• clip_integrable_res_mul probability/clip_profile.v
• clip_integrable_res_sq probability/clip_profile.v
• clip_integrable_sq probability/clip_profile.v
• clip_lipschitz comparison/gauss_concentration.v
• clip_objective probability/clip_profile.v
• clip_objective_add probability/clip_profile.v
• clip_objective_ae_eq probability/clip_profile.v
• clip_objective_ae_set probability/clip_profile.v
• clip_objective_profile probability/clip_profile.v
• clip_objective_radial probability/clip_profile.v
• clip_objectiveE probability/clip_profile.v
• clip_optimal probability/clip_profile.v
• clip_pow_err random_matrix/goe.v
• clip_pow_lipschitz random_matrix/goe.v
• clip_profile probability/clip_profile.v
• clip_profile_admissible probability/clip_profile.v
• clip_profile_bounded probability/clip_profile.v
• clip_profile_bounds probability/clip_profile.v
• clip_profile_closest probability/clip_profile.v
• clip_profile_ct probability/clip_profile.v
• clip_profile_mean probability/clip_profile.v
• clip_profileE probability/clip_profile.v
• clip_res_sqE probability/clip_profile.v
• clip_residual_profile probability/clip_profile.v
• clip_residualE probability/clip_profile.v
• clip_value probability/variational.v
• clip_value_ae probability/clip_profile.v
• clip_value_attained probability/variational.v
• clip_value_ge probability/variational.v
• clip_value_le probability/variational.v
• clip_value_nincr probability/variational.v
• clip_xupper_integrable probability/clip_profile.v
• clip_xupperE probability/clip_profile.v
• closed_bounded_compact_cV comparison/cgmt.v
• closed_tr_set comparison/cgmt.v
• closed_vspace convex/minimizers.v
• cmixture probability/countable_mixture.v
• cmixture_tail probability/countable_mixture.v
• cmixture_tail_series probability/countable_mixture.v
• cmixture_tail_small probability/countable_mixture.v
• cmixture_tail_w probability/countable_mixture.v
• cmixture_tail_weights probability/countable_mixture.v
• cmixture_tailE probability/countable_mixture.v
• cmixture_weights probability/countable_mixture.v
• cmixture_weights_esum probability/countable_mixture.v
• cmixtureE probability/countable_mixture.v
• cmod fourier/charfun.v
• cmod1 fourier/charfun.v
• cmod_ge0 fourier/charfun.v
• cmod_ge_dot fourier/charfun.v
• cmod_prod fourier/charfun.v
• cmodM fourier/charfun.v
• cmul fourier/charfun.v
• cmul1z fourier/charfun.v
• cmul_real_big fourier/gauss_factor.v
• cmulA fourier/charfun.v
• cmulC fourier/charfun.v
• cmulE fourier/charfun.v
• coef_adj matrix/nuclear.v
• coef_map matrix/nuclear.v
• colmax matrix/covering.v
• colmax_col matrix/covering.v
• colmax_ge0 matrix/covering.v
• colmax_le matrix/covering.v
• colmax_le_frobenius matrix/covering.v
• colmax_le_opnorm matrix/covering.v
• colmax_lipschitz matrix/covering.v
• colmaxD matrix/covering.v
• colmaxN matrix/covering.v
• colmaxZ matrix/covering.v
• colsum_mx matrix/covering.v
• colsum_mx_col matrix/covering.v
• compact_unit_sphere matrix/real_spectral.v
• conc_fun fourier/esseen.v
• conc_fun_add fourier/esseen.v
• conc_fun_cover fourier/esseen.v
• conc_fun_ge0 fourier/esseen.v
• conc_fun_le fourier/esseen.v
• conc_fun_le1 fourier/esseen.v
• conc_fun_sum fourier/esseen.v
• conc_fun_sym_law fourier/gauss_factor.v
• conc_fun_truncated fourier/gauss_factor.v
• conc_fun_truncated_exists fourier/gauss_factor.v
• conc_fun_truncated_level fourier/gauss_factor.v
• conc_fun_truncated_level_exists fourier/gauss_factor.v
• conc_fun_ub fourier/esseen.v
• conc_fun_ubE fourier/esseen.v
• cond_clip matrix/condition_cone.v
• cond_clip_cone matrix/condition_cone.v
• cond_clip_energy matrix/condition_cone.v
• cond_cone matrix/condition_cone.v
• cond_cone0 matrix/condition_cone.v
• cond_cone1 matrix/condition_cone.v
• cond_cone_convex matrix/condition_cone.v
• cond_cone_dist matrix/condition_cone.v
• cond_cone_quad matrix/condition_cone.v
• cond_cone_slice matrix/condition_cone.v
• cond_cone_vec matrix/condition_cone.v
• cond_cone_vec0 matrix/condition_cone.v
• cond_cone_vec_closed matrix/condition_cone.v
• cond_cone_vec_convex matrix/condition_cone.v
• cond_cone_vec_slice matrix/condition_cone.v
• cond_cone_vecZ matrix/condition_cone.v
• cond_coneP matrix/condition_cone.v
• cond_coneZ matrix/condition_cone.v
• cond_dist matrix/condition_cone.v
• cond_dist_ge matrix/condition_cone.v
• cond_dist_ge0 matrix/condition_cone.v
• cond_dist_itv matrix/condition_cone.v
• cond_dist_le matrix/condition_cone.v
• cond_distZ matrix/condition_cone.v
• cond_energy matrix/condition_cone.v
• cond_energy_ge0 matrix/condition_cone.v
• cond_energy_le matrix/condition_cone.v
• cond_energy_mono matrix/condition_cone.v
• cond_energyZ matrix/condition_cone.v
• cond_slice matrix/condition_cone.v
• cond_slice1 matrix/condition_cone.v
• cond_slice_form matrix/condition_cone.v
• cond_slice_frobenius matrix/condition_cone.v
• cond_slice_spec matrix/condition_cone.v
• cond_slice_t matrix/condition_cone.v
• cond_slice_vec matrix/condition_cone.v
• cond_slice_vec_closed matrix/condition_cone.v
• cond_slice_vec_convex matrix/condition_cone.v
• cond_slice_vec_frobenius matrix/condition_cone.v
• cond_support matrix/condition_cone.v
• cond_support_ge0 matrix/condition_cone.v
• cond_support_proj matrix/condition_cone.v
• cond_support_sqr matrix/condition_cone.v
• cond_support_sym matrix/condition_cone.v
• cond_support_vec matrix/condition_cone.v
• cond_supportZ matrix/condition_cone.v
• cone_escape_lower_tail comparison/cone_escape.v
• cone_escape_zero_tail comparison/cone_escape.v
• cone_proj_support convex/moreau.v
• cone_projP convex/moreau.v
• cone_sup comparison/cone_escape.v
• cone_sup_attained comparison/cone_escape.v
• cone_sup_dot comparison/cone_escape.v
• cone_sup_ge0 comparison/cone_escape.v
• cone_sup_le comparison/cone_escape.v
• cone_sup_le_norm comparison/cone_escape.v
• cone_sup_lipschitz comparison/cone_escape.v
• cone_sup_proj comparison/cone_escape.v
• cone_sup_tr_setE comparison/cone_escape.v
• cone_sup_ub comparison/cone_escape.v
• conf_ok random_matrix/restricted_isometry.v
• conf_size random_matrix/restricted_isometry.v
• congruence_diag convex/logdet_barrier.v
• conj_equivariant random_matrix/goe_rotation.v
• conj_mx random_matrix/goe_rotation.v
• conj_mx_orthogonal random_matrix/goe_rotation.v
• conj_mxE random_matrix/goe_rotation.v
• continuity_under_integral_at gaussian/parameter_integral.v
• continuous_cf_im fourier/charfun.v
• continuous_cf_norm fourier/charfun.v
• continuous_cf_re fourier/charfun.v
• continuous_cf_rV_density fourier/inversion.v
• continuous_cf_rV_im fourier/charfun_rV.v
• continuous_cf_rV_norm fourier/charfun_rV.v
• continuous_cf_rV_re fourier/charfun_rV.v
• continuous_clip random_matrix/wigner.v
• continuous_dist2 convex/moreau.v
• continuous_expR_coord comparison/slepian.v
• continuous_form matrix/real_spectral.v
• continuous_frobenius_mulmx comparison/cgmt.v
• continuous_gauss_smooth_partial comparison/gauss_smoothing.v
• continuous_goe_stat random_matrix/wigner.v
• continuous_gp comparison/gordon.v
• continuous_gq comparison/gordon.v
• continuous_gsum comparison/gordon.v
• continuous_gtot comparison/gordon.v
• continuous_ls_reduced convex/minimizers.v
• continuous_lse_D2 comparison/slepian.v
• continuous_measurable_mx gaussian/measurable_matrix.v
• continuous_mehler comparison/ornstein_uhlenbeck.v
• continuous_mehler_d1 comparison/ornstein_uhlenbeck.v
• continuous_mehler_d2 comparison/ornstein_uhlenbeck.v
• continuous_mehler_r comparison/ornstein_uhlenbeck.v
• continuous_mehler_x comparison/ornstein_uhlenbeck.v
• continuous_minmax comparison/gordon.v
• continuous_mulmxl gaussian/measurable_matrix.v
• continuous_mulmxr gaussian/measurable_matrix.v
• continuous_mxdot matrix/real_spectral.v
• continuous_mxdot_line comparison/brascamp_lieb.v
• continuous_mxdotl convex/feature_moments.v
• continuous_mxdotv matrix/condition_cone.v
• continuous_mxentry random_matrix/goe.v
• continuous_mxP gaussian/measurable_matrix.v
• continuous_partials_linear gaussian/partial_derivative.v
• continuous_rmax comparison/slepian.v
• continuous_semicircle_pdf probability/semicircle_law.v
• continuous_smm_D comparison/gordon.v
• continuous_smm_D2 comparison/gordon.v
• continuous_softmax comparison/slepian.v
• continuous_sum gaussian/gauss_ibp.v
• continuous_trmx comparison/cgmt.v
• continuous_vec_mx comparison/gordon.v
• contraction probability/symmetrization.v
• contraction_bigmax0 probability/symmetrization.v
• contraction_trmx fourier/small_ball.v
• convex_ls_reduced convex/minimizers.v
• convex_tr_set comparison/cgmt.v
• countable_atomless_null probability/atoms.v
• cpresent RandomSAT/Model.v
• cross_event random_matrix/restricted_isometry.v
• cross_tail random_matrix/restricted_isometry.v
• csplit RandomSAT/Model.v
• csplit_absent RandomSAT/Forcing.v
• csplit_present RandomSAT/Forcing.v
• csplitK RandomSAT/Model.v
• cube_const SKGap/Ising.v
• cube_le_quart convex/ls_insertion.v
• cubic_le_sinh SKGap/Ising.v
• cvg_cf_rV_density_reg fourier/inversion.v
• cvg_nat_eps random_matrix/wigner.v
• cvg_seqP gaussian/parameter_integral.v
• cvg_sum_seq random_matrix/wigner.v
• cvgn_poly_normal_pdf01 gaussian/gauss_ibp.v

D51

• decr_le matrix/von_neumann.v
• del_mean RandomSAT/Forcing.v
• del_mean0 RandomSAT/Forcing.v
• del_mean_binom RandomSAT/Forcing.v
• del_meanS RandomSAT/Forcing.v
• del_ok RandomSAT/Forcing.v
• delay RandomSAT/Pivotal.v
• delay_cons RandomSAT/Pivotal.v
• delay_cons_sqr RandomSAT/Pivotal.v
• delay_cross RandomSAT/Pivotal.v
• deleted RandomSAT/Forcing.v
• deleted_cons RandomSAT/Forcing.v
• delta_mxvec_index random_matrix/goe_entries.v
• delta_shiftE comparison/slepian.v
• dense_seq_rV probability/small_ball_method.v
• density_law probability/density_law.v
• density_law_dominates probability/density_law.v
• density_law_prob probability/density_law.v
• density_lawE probability/density_law.v
• density_prob probability/density_law.v
• density_prob_ae probability/density_law.v
• density_prob_default probability/density_law.v
• density_prob_dominates probability/density_law.v
• density_probE probability/density_law.v
• derive2_ge0_tangent convex/self_concordant.v
• derive_ge0_le convex/self_concordant.v
• derive_le0_le convex/self_concordant.v
• derive_le_cmp probability/rademacher_lindeberg.v
• det_congruence convex/logdet_barrier.v
• diag_mx_commute_map matrix/psd_splitting.v
• diag_part_le random_matrix/restricted_isometry.v
• diag_sqr_le random_matrix/goe_rotation.v
• diag_var random_matrix/goe_rotation.v
• diag_var_ge0 random_matrix/goe_rotation.v
• diag_varE random_matrix/goe_rotation.v
• diff_partials gaussian/partial_derivative.v
• diff_rV_sum gaussian/gauss_interpolation.v
• differentiable_partials gaussian/partial_derivative.v
• dim_sym_traceless convex/logdet_barrier.v
• discriminant_le probability/variational.v
• disj random_matrix/restricted_isometry.v
• disj_supported random_matrix/restricted_isometry.v
• distribution_mixture probability/mixture.v
• div_le4 SKGap/TwoSpin.v
• doubled_law probability/symmetrization.v
• doubled_law_left probability/symmetrization.v
• doubled_law_right probability/symmetrization.v
• doubly_stochastic_le matrix/von_neumann.v
• doubly_stochastic_le_mx matrix/von_neumann.v
• dual_ball_covering matrix/covering.v
• dual_sudakov comparison/sudakov.v

E86

• effective_rank_spec matrix/effective_rank.v
• EFin_Rintegral_bounded probability/lindeberg.v
• efron_stein probability/efron_stein.v
• efron_stein_fourth probability/efron_stein.v
• efron_stein_integrable probability/efron_stein.v
• efron_stein_omission probability/efron_stein_omission.v
• efron_stein_omission_bounded probability/efron_stein_omission.v
• efron_stein_pair probability/efron_stein.v
• efron_stein_resample probability/efron_stein.v
• eigenvalue_le_lambda_max matrix/lambda_max.v
• emp_diracs probability/variational.v
• emp_weight_ge0 probability/variational.v
• empirical probability/variational.v
• empirical_fun probability/variational.v
• empirical_fun_neq0 probability/variational.v
• empirical_fun_sqr probability/variational.v
• empirical_setT probability/variational.v
• empirical_variational_attained probability/variational.v
• empirical_variational_le probability/variational.v
• empiricalE probability/variational.v
• energy_bound_aux SKGap/TwoSpin.v
• entry_le_mx_norm matrix/real_spectral.v
• entry_le_opnorm probability/hanson_wright.v
• entry_mul_bound gaussian/gauss.v
• eq_binom_mean RandomSAT/Forcing.v
• eq_density_law probability/density_law.v
• eq_density_prob probability/density_law.v
• eq_tuple_prod probability/tuple_rows.v
• eq_unif_mean probability/finite_mean.v
• eq_unif_var probability/finite_mean.v
• era_del_ok RandomSAT/Forcing.v
• era_mean RandomSAT/Forcing.v
• era_mean0 RandomSAT/Forcing.v
• era_mean_replacement RandomSAT/Forcing.v
• era_meanS RandomSAT/Forcing.v
• era_ok RandomSAT/Forcing.v
• era_ok_sat RandomSAT/Forcing.v
• erased RandomSAT/Forcing.v
• erased_cons RandomSAT/Forcing.v
• erased_sub RandomSAT/Forcing.v
• escape_inf comparison/escape.v
• escape_inf_ge comparison/escape.v
• escape_inf_ge0 comparison/escape.v
• escape_inf_le comparison/escape.v
• escape_inf_lip comparison/cgmt.v
• escape_inf_lipschitz comparison/escape.v
• escape_inf_minimax comparison/cgmt.v
• escape_inf_norm comparison/escape.v
• escape_inf_tr_set comparison/cgmt.v
• escape_proj_lipschitz comparison/escape.v
• esseen fourier/esseen.v
• esseen0 fourier/esseen.v
• esum_fin probability/countable_mixture.v
• esum_tuple_distr probability/countable_mixture.v
• esum_tuple_prod probability/countable_mixture.v
• esumZl probability/countable_mixture.v
• ex_sym_spectral matrix/real_spectral.v
• exists_ordS RandomSAT/Forcing.v
• expectation_le_ln_mgf matrix/random_opnorm.v
• expectation_mixture probability/mixture.v
• expectation_sqr_le probability/moments.v
• expectation_tuple_prod0 probability/lindeberg.v
• expectation_tuple_prodS probability/lindeberg.v
• expectation_tuple_prodS' probability/lindeberg.v
• expR1_le4 random_matrix/matrix_series.v
• expR_avg_le probability/hanson_wright.v
• expR_bigmax_le matrix/random_opnorm.v
• expR_cosh_ge comparison/gauss_concentration.v
• expR_le_one_sub probability/total_variation.v
• expR_le_quad probability/subgaussian.v
• expR_lnN_half comparison/ornstein_uhlenbeck.v
• expR_mean_le probability/subgaussian.v
• expR_mul1B_le1 probability/subgaussian.v
• expR_sinh_ge comparison/gauss_concentration.v
• expR_spin SKGap/Ising.v
• expR_third_le probability/subgaussian.v
• exprB_le random_matrix/goe.v
• exprn1D_le gaussian/gauss.v
• exprn1S_le gaussian/gauss.v
• exprn_cross_le random_matrix/matrix_series.v
• exprn_expRN_le random_matrix/goe_entries.v
• exprn_le1D random_matrix/goe.v
• exprn_le_expR gaussian/normal_integral.v
• exprn_le_expR probability/subgaussian.v
• exprn_le_fact_expR random_matrix/goe.v
• expRN_lt1 comparison/ornstein_uhlenbeck.v

F81

• fam_mx comparison/escape.v
• fam_mxE comparison/escape.v
• fejer fourier/esseen.v
• fejer0 fourier/esseen.v
• fejer_ge fourier/esseen.v
• fejer_ge0 fourier/esseen.v
• fejerE fourier/esseen.v
• ffun_cons probability/rademacher_lindeberg.v
• ffun_cons_bij probability/rademacher_lindeberg.v
• first_min probability/measurable_minimizer.v
• first_min_in probability/measurable_minimizer.v
• first_min_le probability/measurable_minimizer.v
• first_min_val probability/measurable_minimizer.v
• forced RandomSAT/Replacement.v
• forced0 RandomSAT/Replacement.v
• forced_coord_mean RandomSAT/Forcing.v
• forced_frac RandomSAT/Forcing.v
• forced_frac_head RandomSAT/Forcing.v
• forced_frozen RandomSAT/Replacement.v
• forced_rename RandomSAT/Forcing.v
• form_le_opnorm convex/feature_moments.v
• form_unit_ball_le matrix/nets.v
• frame_mulmx fourier/small_ball.v
• frame_mxdot fourier/small_ball.v
• frame_trace fourier/small_ball.v
• frobenius matrix/euclidean.v
• frobenius0 matrix/euclidean.v
• frobenius_col_sqr matrix/nets.v
• frobenius_colE matrix/euclidean.v
• frobenius_compress_le matrix/psd_splitting.v
• frobenius_entry matrix/euclidean.v
• frobenius_eq0 matrix/euclidean.v
• frobenius_ge0 matrix/euclidean.v
• frobenius_goe_coef_diag random_matrix/goe_entries.v
• frobenius_goe_mx random_matrix/goe.v
• frobenius_gt0 matrix/euclidean.v
• frobenius_hsub_add comparison/cgmt.v
• frobenius_hsub_sqr comparison/cgmt.v
• frobenius_isometry_le matrix/tensor_packing.v
• frobenius_le_mx_norm comparison/gauss_smoothing.v
• frobenius_le_mx_norm matrix/real_spectral.v
• frobenius_le_nuclear matrix/nuclear.v
• frobenius_le_opnorm matrix/nuclear.v
• frobenius_lsubmx_le comparison/cgmt.v
• frobenius_mulmx matrix/euclidean.v
• frobenius_mulmx_mx_opnorm matrix/opnorm.v
• frobenius_mulmx_opnorm matrix/opnorm.v
• frobenius_mxcoef_le matrix/tensor_packing.v
• frobenius_mxcoef_sqr matrix/tensor_packing.v
• frobenius_mxvec convex/logdet_barrier.v
• frobenius_orthogonalmxl matrix/euclidean.v
• frobenius_orthogonalmxr matrix/euclidean.v
• frobenius_outer matrix/tensor_packing.v
• frobenius_proj_le comparison/escape.v
• frobenius_psd_part_shift matrix/psd_part.v
• frobenius_rowE matrix/euclidean.v
• frobenius_rowperp_compress_le matrix/tensor_packing.v
• frobenius_rowperp_le matrix/tensor_packing.v
• frobenius_rowproj matrix/tensor_packing.v
• frobenius_rsubmx_le comparison/cgmt.v
• frobenius_sk_coupling_le SKGap/Disorder.v
• frobenius_sqr matrix/euclidean.v
• frobenius_sqr_le_nuclear matrix/nuclear.v
• frobenius_sqr_sym matrix/psd_splitting.v
• frobenius_sum_le matrix/tensor_packing.v
• frobenius_sum_near matrix/tensor_packing.v
• frobenius_sum_psd_le matrix/psd_splitting.v
• frobenius_tensor matrix/tensor_packing.v
• frobenius_trmx matrix/euclidean.v
• frobenius_trmx_isometry matrix/tensor_packing.v
• frobenius_vec_mx comparison/escape.v
• frobenius_vec_mx convex/logdet_barrier.v
• frobenius_whitening_mx matrix/whitening.v
• frobeniusB matrix/euclidean.v
• frobeniusD matrix/euclidean.v
• frobeniusN matrix/euclidean.v
• frobeniusZ matrix/euclidean.v
• frozen RandomSAT/Replacement.v
• frozen_kills RandomSAT/Replacement.v
• ftail RandomSAT/Model.v
• ftail_prepend RandomSAT/Model.v

G290

• g_ge1 RandomSAT/Forcing.v
• gap_from_bounds SKGap/Poincare.v
• gauss gaussian/gauss.v
• gauss2_ibp_snd comparison/gauss_concentration.v
• gauss2_rotation comparison/gauss_rotation.v
• gauss_box gaussian/gauss.v
• gauss_brascamp_lieb comparison/brascamp_lieb_lebesgue.v
• gauss_brascamp_lieb_bounded comparison/brascamp_lieb.v
• gauss_brascamp_lieb_ge0 comparison/brascamp_lieb_lebesgue.v
• gauss_centered_chi2_abs_tail comparison/chi_square.v
• gauss_centered_chi2_lower_tail comparison/chi_square.v
• gauss_centered_chi2_upper_tail comparison/chi_square.v
• gauss_chaos_mgf probability/hanson_wright.v
• gauss_col_perm gaussian/gauss.v
• gauss_comparison gaussian/gauss_interpolation.v
• gauss_comparison_partial gaussian/gauss_interpolation.v
• gauss_concentration comparison/gauss_concentration.v
• gauss_concentration_abs_tail comparison/gauss_concentration.v
• gauss_concentration_lower_tail comparison/gauss_concentration.v
• gauss_concentration_smooth comparison/gauss_concentration.v
• gauss_concentration_smooth_ge0 comparison/gauss_concentration.v
• gauss_concentration_upper_tail comparison/gauss_concentration.v
• gauss_coord gaussian/gauss.v
• gauss_coord_moments convex/gauss_feature.v
• gauss_cov gaussian/gauss_moments.v
• gauss_diag_moments convex/gauss_feature.v
• gauss_factor_center_exists fourier/gauss_factor.v
• gauss_factor_center_le fourier/gauss_factor.v
• gauss_factor_const fourier/gauss_factor.v
• gauss_factor_const_gt0 fourier/gauss_factor.v
• gauss_factor_exists fourier/gauss_factor.v
• gauss_factor_le fourier/gauss_factor.v
• gauss_factor_scaled_le fourier/gauss_factor.v
• gauss_frobenius_ge fourier/charfun_rV.v
• gauss_frobenius_mean random_matrix/goe.v
• gauss_frobenius_mean_le comparison/escape.v
• gauss_herbst_ineq comparison/gauss_concentration.v
• gauss_ibp gaussian/gauss_ibp.v
• gauss_ibp0 gaussian/gauss_ibp.v
• gauss_ibp2 gaussian/gauss_ibp.v
• gauss_ibp_gradient gaussian/gauss_interpolation.v
• gauss_ibp_line gaussian/gauss_ibp.v
• gauss_ibp_mulmx gaussian/gauss_interpolation.v
• gauss_ibp_polyfun random_matrix/goe.v
• gauss_ibp_unit comparison/brascamp_lieb.v
• gauss_integrable4 convex/gauss_feature.v
• gauss_interpolation gaussian/gauss_interpolation.v
• gauss_law_double_smooth comparison/gauss_law.v
• gauss_law_lipschitz comparison/gauss_law.v
• gauss_law_smooth comparison/gauss_law.v
• gauss_lebesgue_rV gaussian/lebesgue_rV.v
• gauss_lsubmx gaussian/gauss.v
• gauss_markov random_matrix/goe_rotation.v
• gauss_max_lower comparison/sudakov.v
• gauss_mean gaussian/gauss_moments.v
• gauss_min_singular_mean comparison/escape.v
• gauss_mulmx_cov gaussian/gauss_moments.v
• gauss_mulmx_law comparison/gauss_law.v
• gauss_mx_series_ibp random_matrix/matrix_series.v
• gauss_mx_series_ibp_coord random_matrix/matrix_series.v
• gauss_mx_series_moment random_matrix/matrix_series.v
• gauss_mx_series_opnorm random_matrix/matrix_series.v
• gauss_mx_series_opnorm_log random_matrix/matrix_series.v
• gauss_mx_series_opnorm_moment random_matrix/matrix_series.v
• gauss_mx_series_trace_le random_matrix/matrix_series.v
• gauss_mx_series_trace_rec random_matrix/matrix_series.v
• gauss_mx_series_trace_sqr random_matrix/matrix_series.v
• gauss_mxdot comparison/gauss_linear.v
• gauss_mxdot_abs_tail comparison/gauss_linear.v
• gauss_mxdot_moments convex/gauss_feature.v
• gauss_mxdot_upper_tail comparison/gauss_linear.v
• gauss_opnorm_mean comparison/escape.v
• gauss_opnorm_mean_sqrt comparison/escape.v
• gauss_opnorm_tail comparison/escape.v
• gauss_orthogonal_law comparison/gauss_law.v
• gauss_pdf gaussian/lebesgue_rV.v
• gauss_pdf_cons gaussian/lebesgue_rV.v
• gauss_pdf_ge0 gaussian/lebesgue_rV.v
• gauss_pdf_gt0 gaussian/lebesgue_rV.v
• gauss_pdf_scale fourier/charfun_rV.v
• gauss_poincare_lipschitz comparison/gauss_concentration.v
• gauss_pressure PerceptronSignDefinitions.v
• gauss_proj_mean_ge comparison/escape.v
• gauss_proj_singular_tail comparison/escape.v
• gauss_quad_moments convex/gauss_feature.v
• gauss_regular_feature convex/gauss_feature.v
• gauss_row_mx gaussian/gauss.v
• gauss_rsubmx gaussian/gauss.v
• gauss_shift_sym comparison/sudakov.v
• gauss_smooth comparison/gauss_smoothing.v
• gauss_smooth_bounded comparison/gauss_smoothing.v
• gauss_smooth_close comparison/gauss_smoothing.v
• gauss_smooth_derive comparison/gauss_smoothing.v
• gauss_smooth_differentiable comparison/gauss_smoothing.v
• gauss_smooth_grad comparison/gauss_smoothing.v
• gauss_smooth_lipschitz comparison/gauss_smoothing.v
• gauss_smooth_partial comparison/gauss_smoothing.v
• gauss_smooth_partial_bounded comparison/gauss_law.v
• gauss_smooth_partial_lipschitz comparison/gauss_law.v
• gauss_smooth_partial_stein comparison/gauss_law.v
• gauss_sqr_mulmx comparison/escape.v
• gauss_tail_expR random_matrix/goe.v
• gauss_trmx comparison/gauss_matrix_law.v
• gauss_tuple_mx comparison/gauss_matrix_law.v
• gauss_unique gaussian/gauss.v
• gauss_weight_conc_fun fourier/gauss_factor.v
• gaussS gaussian/gauss.v
• ge0_integral_avg probability/hanson_wright.v
• ge0_integral_cf_rV_inv_prob fourier/inversion.v
• ge0_integral_cmixture probability/countable_mixture.v
• ge0_integral_density_law probability/density_law.v
• ge0_integral_density_prob probability/density_law.v
• ge0_integral_empirical probability/variational.v
• ge0_integral_gauss2_cons comparison/gauss_rotation.v
• ge0_integral_gauss2_rotation comparison/gauss_rotation.v
• ge0_integral_gauss_affine fourier/charfun_rV.v
• ge0_integral_gauss_cons gaussian/gauss.v
• ge0_integral_gauss_coord gaussian/gauss.v
• ge0_integral_gauss_lincomb comparison/gauss_rotation.v
• ge0_integral_gauss_mulmx comparison/gauss_law.v
• ge0_integral_gauss_mxdot comparison/gauss_linear.v
• ge0_integral_gauss_opp comparison/escape.v
• ge0_integral_gauss_pdf gaussian/lebesgue_rV.v
• ge0_integral_gauss_prod gaussian/gauss.v
• ge0_integral_gauss_shift comparison/gauss_shift.v
• ge0_integral_image probability/tuple_rows.v
• ge0_integral_lebesgue_affine comparison/normal_linear.v
• ge0_integral_lebesgue_rV_col_perm gaussian/lebesgue_rV.v
• ge0_integral_lebesgue_rV_cons gaussian/lebesgue_rV.v
• ge0_integral_lebesgue_rV_gauss gaussian/lebesgue_rV.v
• ge0_integral_lebesgue_rV_image gaussian/lebesgue_rV.v
• ge0_integral_lebesgue_rV_prod gaussian/lebesgue_rV.v
• ge0_integral_lebesgue_rV_row_mx gaussian/lebesgue_rV.v
• ge0_integral_lebesgue_rV_scale gaussian/lebesgue_rV.v
• ge0_integral_lebesgue_rV_shift gaussian/lebesgue_rV.v
• ge0_integral_mixture probability/mixture.v
• ge0_integral_normal2 comparison/gauss_rotation.v
• ge0_integral_normal2_rotation comparison/gauss_rotation.v
• ge0_integral_normal_prob gaussian/normal_integral.v
• ge0_integral_normal_shift comparison/gauss_shift.v
• ge0_integral_oppr2 comparison/gauss_rotation.v
• ge0_integral_rademacher_mean probability/symmetrization.v
• ge0_integral_rotation2 comparison/gauss_rotation.v
• ge0_integral_semicircle_prob probability/semicircle_law.v
• ge0_integral_semicircle_scale probability/semicircle_law.v
• ge0_integral_shear1 comparison/gauss_rotation.v
• ge0_integral_shear2 comparison/gauss_rotation.v
• ge0_integral_swap probability/symmetrization.v
• ge0_integral_tuple_left probability/symmetrization.v
• ge0_integral_tuple_map probability/tuple_rows.v
• ge0_integral_tuple_prod_cat probability/tuple_rows.v
• ge0_integral_tuple_prod_coord probability/efron_stein.v
• ge0_integral_tuple_prod_coordM probability/efron_stein.v
• ge0_integral_tuple_prod_merge probability/conditioning.v
• ge0_integral_tuple_prod_prod probability/tuple_rows.v
• ge0_integral_tuple_prod_set probability/efron_stein.v
• ge0_integral_tuple_prod_tnth convex/barrier_lindeberg.v
• ge0_integral_tuple_prodS probability/tuple_rows.v
• ge0_integral_tuple_right probability/symmetrization.v
• ge0_integral_tuple_rows probability/tuple_rows.v
• geom_sum_le RandomSAT/Pivotal.v
• gibbs_mass_gt0 probability/log_partition.v
• gibbs_mean probability/log_partition.v
• gibbs_mean_le probability/log_partition.v
• goe_clip random_matrix/goe.v
• goe_clip_bound random_matrix/goe.v
• goe_clip_cvg random_matrix/wigner.v
• goe_clip_err random_matrix/goe.v
• goe_clip_err2 random_matrix/goe.v
• goe_clip_err2_small random_matrix/goe.v
• goe_clip_lipschitz random_matrix/goe.v
• goe_coef random_matrix/goe_entries.v
• goe_conj_integral random_matrix/goe_rotation.v
• goe_diag_var_identity random_matrix/goe_rotation.v
• goe_diag_var_identityS random_matrix/goe_rotation.v
• goe_diag_var_tail random_matrix/goe_rotation.v
• goe_edge_exponent random_matrix/goe_edge.v
• goe_edge_statement GoeEdgeStatement.v
• goe_edge_theorem GoeEdgeTheorem.v
• goe_equiv_diag random_matrix/goe_rotation.v
• goe_equiv_diag2 random_matrix/goe_rotation.v
• goe_equiv_form random_matrix/goe_rotation.v
• goe_equiv_formR random_matrix/goe_rotation.v
• goe_equiv_pair random_matrix/goe_rotation.v
• goe_equiv_pair2 random_matrix/goe_rotation.v
• goe_form_cov random_matrix/goe_edge.v
• goe_form_incr_var random_matrix/goe_edge.v
• goe_form_max_mean random_matrix/goe_edge.v
• goe_form_mx random_matrix/goe_edge.v
• goe_form_mxE random_matrix/goe_edge.v
• goe_lambda_max_lipschitz random_matrix/goe_edge.v
• goe_lambda_max_mean random_matrix/goe_edge.v
• goe_lambda_max_tail random_matrix/goe_edge.v
• goe_lambda_maxN_lipschitz random_matrix/goe_edge.v
• goe_lambda_maxN_mean random_matrix/goe_edge.v
• goe_lambda_maxN_tail random_matrix/goe_edge.v
• goe_lin_cov random_matrix/goe_edge.v
• goe_lin_mx random_matrix/goe_edge.v
• goe_moment_cvg random_matrix/wigner.v
• goe_mx random_matrix/goe.v
• goe_mx_conj random_matrix/goe_rotation.v
• goe_mx_delta random_matrix/goe.v
• goe_mx_diag_max_tail random_matrix/goe_entries.v
• goe_mx_diag_tail random_matrix/goe_entries.v
• goe_mx_form random_matrix/goe_edge.v
• goe_mx_mxdot random_matrix/goe_entries.v
• goe_mx_offdiag_max_tail random_matrix/goe_entries.v
• goe_mx_offdiag_tail random_matrix/goe_entries.v
• goe_mx_row_max_tail random_matrix/goe_entries.v
• goe_mx_row_tail random_matrix/goe_entries.v
• goe_mx_sym random_matrix/goe.v
• goe_mx_symmetric random_matrix/goe.v
• goe_mxB random_matrix/goe.v
• goe_mxD random_matrix/goe.v
• goe_mxE random_matrix/goe.v
• goe_mxN random_matrix/goe_edge.v
• goe_mxZ random_matrix/goe.v
• goe_opnorm_edge_tail random_matrix/goe_edge.v
• goe_opnorm_lipschitz random_matrix/goe.v
• goe_opnorm_mean random_matrix/goe.v
• goe_opnorm_mgf random_matrix/goe.v
• goe_opnorm_tail_small random_matrix/goe.v
• goe_schwinger_dyson random_matrix/goe.v
• goe_stat random_matrix/wigner.v
• goe_stat_clip_mean_cvg random_matrix/wigner.v
• goe_stat_conc random_matrix/wigner.v
• goe_stat_lipschitz random_matrix/wigner.v
• goe_stat_near random_matrix/wigner.v
• goe_stat_poly_clip random_matrix/wigner.v
• goe_tr random_matrix/goe.v
• goe_tr_cov_cvg random_matrix/wigner.v
• goe_tr_sd random_matrix/goe.v
• goe_tr_var random_matrix/goe.v
• goe_tr_var_small random_matrix/goe.v
• goe_trE random_matrix/goe.v
• gordon comparison/gordon.v
• gordon_cov comparison/gordon.v
• gordon_escape comparison/escape.v
• gordon_escape_tail comparison/escape.v
• gordon_gamma comparison/cgmt.v
• gordon_minmax comparison/escape.v
• gordon_projection comparison/escape.v
• gordon_projection_tail comparison/escape.v
• gp comparison/gordon.v
• gp_ge0 comparison/gordon.v
• gp_le1 comparison/gordon.v
• gp_sum comparison/gordon.v
• gq comparison/gordon.v
• gq_ge0 comparison/gordon.v
• gq_le1 comparison/gordon.v
• gq_sum comparison/gordon.v
• gram_form matrix/tensor_packing.v
• gram_form_ge0 matrix/tensor_packing.v
• gram_off random_matrix/restricted_isometry.v
• gram_off0l random_matrix/restricted_isometry.v
• gram_off_ball random_matrix/restricted_isometry.v
• gram_off_decouple random_matrix/restricted_isometry.v
• gram_off_disj random_matrix/restricted_isometry.v
• gram_off_rip random_matrix/restricted_isometry.v
• gram_off_rip2 random_matrix/restricted_isometry.v
• gram_off_suml random_matrix/restricted_isometry.v
• gram_off_sumr random_matrix/restricted_isometry.v
• gram_off_tri random_matrix/restricted_isometry.v
• gram_offC random_matrix/restricted_isometry.v
• gram_offDl random_matrix/restricted_isometry.v
• gram_offDr random_matrix/restricted_isometry.v
• gram_offE random_matrix/restricted_isometry.v
• gram_offZl random_matrix/restricted_isometry.v
• gram_sym matrix/tensor_packing.v
• gram_trace matrix/tensor_packing.v
• gram_trace_on matrix/tensor_packing.v
• grid_code matrix/nets.v
• grid_code_dist matrix/nets.v
• grid_code_mem matrix/nets.v
• grid_code_near matrix/nets.v
• grid_codes matrix/nets.v
• grid_net matrix/nets.v
• grid_point matrix/nets.v
• grid_point_code matrix/nets.v
• gsum comparison/gordon.v
• gsum_gt0 comparison/gordon.v
• gtot comparison/gordon.v
• gtot_gt0 comparison/gordon.v
• gwidth_fun comparison/escape.v
• gwidth_ge comparison/escape.v
• gwidth_le comparison/escape.v
• gwidth_lipschitz comparison/escape.v
• gwidth_norm comparison/escape.v
• gwidth_range_sphere comparison/escape.v
• gwidth_sphere comparison/escape.v

H42

• half_diff SKGapDefinitions.v
• half_diff_form SKGap/Poincare.v
• half_diff_set SKGap/Ising.v
• hanson_wright probability/hanson_wright.v
• hanson_wright_mgf probability/hanson_wright.v
• hanson_wright_subexponential probability/hanson_wright.v
• hanson_wright_upper probability/hanson_wright.v
• has_sup_rip random_matrix/restricted_isometry.v
• head_forced RandomSAT/Forcing.v
• head_forced_ind RandomSAT/Forcing.v
• head_forced_mean_le RandomSAT/Forcing.v
• head_forced_reduction RandomSAT/Forcing.v
• Hk random_matrix/restricted_isometry.v
• Hk_ge0 random_matrix/restricted_isometry.v
• Hk_rev random_matrix/restricted_isometry.v
• Hk_step random_matrix/restricted_isometry.v
• Hk_sum random_matrix/restricted_isometry.v
• hoffman_wielandt matrix/von_neumann.v
• householder matrix/real_spectral.v
• householder0 matrix/real_spectral.v
• householder_orthogonal matrix/real_spectral.v
• householder_swap matrix/real_spectral.v
• householder_sym matrix/real_spectral.v
• householder_tr matrix/real_spectral.v
• householderK matrix/real_spectral.v
• householderN matrix/real_spectral.v
• hw_center probability/hanson_wright.v
• hw_decoupled probability/hanson_wright.v
• hw_decoupled_mgf probability/hanson_wright.v
• hw_diag probability/hanson_wright.v
• hw_diag_mgf probability/hanson_wright.v
• hw_mask probability/hanson_wright.v
• hw_mask_diag probability/hanson_wright.v
• hw_offdiag probability/hanson_wright.v
• hw_offdiag_mgf probability/hanson_wright.v
• hw_quad probability/hanson_wright.v
• hw_quad0 probability/hanson_wright.v
• hw_quad_split probability/hanson_wright.v
• hw_quadN probability/hanson_wright.v
• hw_sqmean probability/hanson_wright.v
• hybrid convex/barrier_lindeberg.v
• hybrid_regular convex/barrier_lindeberg.v

I346

• in_set_toggle probability/hanson_wright.v
• incr_var comparison/slepian.v
• incr_var_bil_aux comparison/escape.v
• incr_var_bilT_auxT comparison/escape.v
• incr_var_gamma comparison/cgmt.v
• indic_tuple_box probability/density_law.v
• infsup comparison/cgmt.v
• infsup_bound comparison/cgmt.v
• infsup_compare comparison/cgmt.v
• infsup_le comparison/cgmt.v
• infsup_lipschitz comparison/cgmt.v
• infsup_net comparison/cgmt.v
• ins_alpha convex/ls_insertion.v
• ins_alphaE convex/ls_insertion.v
• ins_c convex/ls_insertion.v
• ins_c0 convex/ls_insertion.v
• ins_c0_bounds convex/ls_insertion.v
• ins_c_linear convex/ls_insertion.v
• ins_cost convex/ls_insertion.v
• ins_cost_bounds convex/ls_insertion.v
• ins_cost_lower convex/ls_insertion.v
• ins_cost_quadratic convex/ls_insertion.v
• ins_cost_set convex/ls_insertion.v
• ins_cost_upper convex/ls_insertion.v
• ins_D2B_ge0 convex/ls_insertion.v
• ins_dir convex/ls_insertion.v
• ins_ell convex/ls_insertion.v
• ins_ell_ge0 convex/ls_insertion.v
• ins_ell_quadratic convex/ls_insertion.v
• ins_form_le convex/ls_insertion.v
• ins_h convex/ls_insertion.v
• ins_h_linear convex/ls_insertion.v
• ins_hessian convex/ls_insertion.v
• ins_hessian_pd convex/ls_insertion.v
• ins_hessianE convex/ls_insertion.v
• ins_hform convex/ls_insertion.v
• ins_hform_ge convex/ls_insertion.v
• ins_hform_linearl convex/ls_insertion.v
• ins_hform_ridge convex/ls_insertion.v
• ins_hformC convex/ls_insertion.v
• ins_hV convex/ls_insertion.v
• ins_inv_sym convex/ls_insertion.v
• ins_l_var convex/barrier_lindeberg.v
• ins_n_gt0 convex/ls_insertion.v
• ins_norm_h convex/ls_insertion.v
• ins_nR_gt0 convex/ls_insertion.v
• ins_objective convex/ls_insertion.v
• ins_r convex/ls_insertion.v
• ins_rem convex/ls_insertion.v
• ins_rem_le convex/ls_insertion.v
• ins_ridge_ge convex/ls_insertion.v
• ins_s_eq convex/ls_insertion.v
• ins_s_ge0 convex/ls_insertion.v
• ins_size_le convex/ls_insertion.v
• ins_sqrt_ge6 convex/ls_insertion.v
• ins_T convex/ls_insertion.v
• ins_T_bounds convex/ls_insertion.v
• ins_T_frobenius convex/ls_insertion.v
• ins_T_sym convex/ls_insertion.v
• ins_taylor convex/ls_insertion.v
• ins_v convex/ls_insertion.v
• ins_v_bound convex/ls_insertion.v
• insertion_compare convex/barrier_lindeberg.v
• int_P4 convex/barrier_lindeberg.v
• int_Phi convex/barrier_lindeberg.v
• int_Phi_set convex/barrier_lindeberg.v
• integrable_cf_rV_kernel fourier/inversion.v
• integrable_cf_rV_norm fourier/inversion.v
• integrable_cos_comp fourier/charfun.v
• integrable_cos_mul fourier/charfun.v
• integrable_cst_prob convex/feature_moments.v
• integrable_density_law probability/density_law.v
• integrable_density_prob probability/density_law.v
• integrable_empirical probability/variational.v
• integrable_escape_inf comparison/escape.v
• integrable_gauss2_fst comparison/gauss_concentration.v
• integrable_gauss2_rotation comparison/gauss_rotation.v
• integrable_gauss2_snd comparison/gauss_concentration.v
• integrable_gauss_bounded comparison/gauss_smoothing.v
• integrable_gauss_concentration comparison/gauss_concentration.v
• integrable_gauss_cons gaussian/gauss.v
• integrable_gauss_coord gaussian/gauss.v
• integrable_gauss_entry gaussian/gauss_interpolation.v
• integrable_gauss_expR_abs_coord comparison/gauss_smoothing.v
• integrable_gauss_frobenius comparison/gauss_smoothing.v
• integrable_gauss_lipschitz comparison/gauss_concentration.v
• integrable_gauss_lse comparison/slepian.v
• integrable_gauss_minmax comparison/gordon.v
• integrable_gauss_mxdot comparison/gauss_linear.v
• integrable_gauss_opnorm comparison/escape.v
• integrable_gauss_opp comparison/escape.v
• integrable_gauss_pdf gaussian/lebesgue_rV.v
• integrable_gauss_poly gaussian/gauss.v
• integrable_gauss_rmax comparison/slepian.v
• integrable_gauss_shift comparison/gauss_shift.v
• integrable_gauss_smm comparison/gordon.v
• integrable_gauss_weight fourier/gauss_factor.v
• integrable_goe_lambda_max random_matrix/goe_edge.v
• integrable_goe_lambda_maxN random_matrix/goe_edge.v
• integrable_goe_opnorm random_matrix/goe.v
• integrable_goe_opnorm_expR random_matrix/goe.v
• integrable_gwidth comparison/escape.v
• integrable_idR probability/variational.v
• integrable_image gaussian/gauss.v
• integrable_infsupX comparison/cgmt.v
• integrable_infsupY comparison/cgmt.v
• integrable_lebesgue_rV_cons gaussian/lebesgue_rV.v
• integrable_lebesgue_rV_image gaussian/lebesgue_rV.v
• integrable_lebesgue_rV_scale gaussian/lebesgue_rV.v
• integrable_lebesgue_rV_shift gaussian/lebesgue_rV.v
• integrable_minmax_sph comparison/escape.v
• integrable_mixture probability/mixture.v
• integrable_mul_sqr probability/variational.v
• integrable_nondecreasing_set_cvg_integral gaussian/gauss_ibp.v
• integrable_normal_affine probability/rademacher_lindeberg.v
• integrable_normal_bounded comparison/ornstein_uhlenbeck.v
• integrable_normal_expR comparison/normal_mgf.v
• integrable_normal_expR_abs comparison/gauss_smoothing.v
• integrable_normal_expR_sqr comparison/chi_square.v
• integrable_normal_exprn gaussian/normal_integral.v
• integrable_normal_poly gaussian/normal_integral.v
• integrable_normal_prob gaussian/normal_integral.v
• integrable_normal_sqr probability/rademacher_lindeberg.v
• integrable_of_sqr probability/variational.v
• integrable_polyfun random_matrix/goe.v
• integrable_pow4 probability/small_ball_method.v
• integrable_prob_bounded comparison/gauss_concentration.v
• integrable_quad_bound probability/variational.v
• integrable_Rsum comparison/brascamp_lieb.v
• integrable_semicircle_continuous probability/semicircle_law.v
• integrable_semicircle_pdf probability/semicircle_law.v
• integrable_semicircle_pdfM probability/semicircle_law.v
• integrable_semicircle_poly random_matrix/wigner.v
• integrable_semicircle_prob probability/semicircle_law.v
• integrable_sin_comp fourier/charfun.v
• integrable_sin_mul fourier/charfun.v
• integrable_sqr_Lfun2 probability/moments.v
• integrable_subexponential probability/subgaussian.v
• integrable_subexponential_expR probability/subgaussian.v
• integrable_subgaussian_expR probability/subgaussian.v
• integrable_subgaussian_exprn probability/subgaussian.v
• integrable_sym probability/variational.v
• integrable_tuple_map probability/tuple_rows.v
• integrable_tuple_prod_set_pair probability/efron_stein.v
• integrable_tuple_prod_tnth convex/barrier_lindeberg.v
• integrable_tuple_prodS probability/tuple_rows.v
• integrable_upper1 probability/clip_profile.v
• integrable_upper1_reflect probability/clip_profile.v
• integrable_upper_pow probability/variational.v
• integrableR_sum convex/feature_moments.v
• integrableRB convex/feature_moments.v
• integrableRD convex/feature_moments.v
• integrableRZl convex/feature_moments.v
• integrableRZr convex/feature_moments.v
• integral_add_gauss fourier/inversion.v
• integral_affine_pow4_le probability/small_ball_method.v
• integral_affine_sqr probability/small_ball_method.v
• integral_cf_rV_density fourier/inversion.v
• integral_cf_rV_density_gauss fourier/inversion.v
• integral_cf_rV_kernel_gauss fourier/inversion.v
• integral_cmixture probability/countable_mixture.v
• integral_density_law probability/density_law.v
• integral_density_law_prob probability/density_law.v
• integral_density_prob probability/density_law.v
• integral_distribution_measurable probability/efron_stein.v
• integral_gauss2_fst comparison/gauss_concentration.v
• integral_gauss2_prod comparison/gauss_concentration.v
• integral_gauss2_rotation comparison/gauss_rotation.v
• integral_gauss2_snd comparison/gauss_concentration.v
• integral_gauss_col_perm gaussian/gauss.v
• integral_gauss_cons gaussian/gauss.v
• integral_gauss_cons21 gaussian/gauss_ibp.v
• integral_gauss_coord gaussian/gauss.v
• integral_gauss_expR_centered_chi2 comparison/chi_square.v
• integral_gauss_expR_centered_chi2_le comparison/chi_square.v
• integral_gauss_expR_dot probability/hanson_wright.v
• integral_gauss_expR_mxdot comparison/gauss_linear.v
• integral_gauss_half_le fourier/esseen.v
• integral_gauss_lsubmx gaussian/gauss.v
• integral_gauss_mulmx comparison/gauss_law.v
• integral_gauss_mxdot comparison/gauss_linear.v
• integral_gauss_mxdot_self fourier/charfun_rV.v
• integral_gauss_opp comparison/escape.v
• integral_gauss_orthogonal comparison/gauss_law.v
• integral_gauss_pdf gaussian/lebesgue_rV.v
• integral_gauss_pdf_inv_prob fourier/inversion.v
• integral_gauss_rsubmx gaussian/gauss.v
• integral_gauss_shift comparison/gauss_shift.v
• integral_image gaussian/gauss.v
• integral_lebesgue_rV_col_perm gaussian/lebesgue_rV.v
• integral_lebesgue_rV_cons gaussian/lebesgue_rV.v
• integral_lebesgue_rV_image gaussian/lebesgue_rV.v
• integral_lebesgue_rV_row_mx gaussian/lebesgue_rV.v
• integral_lebesgue_rV_scale gaussian/lebesgue_rV.v
• integral_lebesgue_rV_shift gaussian/lebesgue_rV.v
• integral_mehler comparison/ornstein_uhlenbeck.v
• integral_minmax_aux comparison/escape.v
• integral_mixture probability/mixture.v
• integral_normal_expR comparison/normal_mgf.v
• integral_normal_expR_sqr comparison/chi_square.v
• integral_normal_expR_sqrB1 comparison/chi_square.v
• integral_normal_expR_sqrB1_le comparison/chi_square.v
• integral_normal_prob gaussian/normal_integral.v
• integral_resample_tuple_set probability/efron_stein.v
• integral_rmax_aux comparison/escape.v
• integral_semicircle_pdf probability/semicircle_law.v
• integral_semicircle_pdf_support probability/semicircle_law.v
• integral_semicircle_prob probability/semicircle_law.v
• integral_tuple_map probability/tuple_rows.v
• integral_tuple_prod_coord probability/efron_stein.v
• integral_tuple_prod_coordM probability/efron_stein.v
• integral_tuple_prod_free convex/barrier_lindeberg.v
• integral_tuple_prod_set probability/efron_stein.v
• integral_tuple_prodS probability/tuple_rows.v
• integral_tuple_rows probability/tuple_rows.v
• integrated_head_forcing RandomSAT/Forcing.v
• inv_diff_le convex/barrier_lindeberg.v
• invmx_orthogonal matrix/euclidean.v
• is_derive_affine comparison/slepian.v
• is_derive_affine_comp comparison/gauss_law.v
• is_derive_comp_dir comparison/brascamp_lieb.v
• is_derive_continuous probability/rademacher_lindeberg.v
• is_derive_cos_mul fourier/charfun.v
• is_derive_cos_mulr fourier/charfun.v
• is_derive_cubic comparison/ornstein_uhlenbeck.v
• is_derive_cubicE comparison/ornstein_uhlenbeck.v
• is_derive_expR_coord comparison/slepian.v
• is_derive_expRN comparison/gauss_concentration.v
• is_derive_expRN' SKGap/Ising.v
• is_derive_fsum probability/log_partition.v
• is_derive_gibbs_mass probability/log_partition.v
• is_derive_gibbs_mean probability/log_partition.v
• is_derive_gibbs_sum probability/log_partition.v
• is_derive_goe_pow random_matrix/goe.v
• is_derive_gsum comparison/gordon.v
• is_derive_gsumV comparison/gordon.v
• is_derive_gtot comparison/gordon.v
• is_derive_lift comparison/slepian.v
• is_derive_line convex/self_concordant.v
• is_derive_line_inv convex/self_concordant.v
• is_derive_log_partition probability/log_partition.v
• is_derive_lse comparison/slepian.v
• is_derive_lse_sum comparison/slepian.v
• is_derive_mehler comparison/ornstein_uhlenbeck.v
• is_derive_mehler_d1 comparison/ornstein_uhlenbeck.v
• is_derive_mehler_d2 comparison/ornstein_uhlenbeck.v
• is_derive_mehler_r comparison/ornstein_uhlenbeck.v
• is_derive_mull fourier/charfun.v
• is_derive_mulmxl gaussian/gauss_interpolation.v
• is_derive_mulr fourier/charfun.v
• is_derive_mxdot comparison/brascamp_lieb.v
• is_derive_mxdot_comp comparison/brascamp_lieb.v
• is_derive_mxentry random_matrix/goe.v
• is_derive_mxpow random_matrix/goe.v
• is_derive_normal_kernel comparison/ornstein_uhlenbeck.v
• is_derive_normal_pdf01 gaussian/gauss_ibp.v
• is_derive_omega_line convex/self_concordant.v
• is_derive_omega_line1 convex/self_concordant.v
• is_derive_omega_star_line convex/self_concordant.v
• is_derive_omega_star_line1 convex/self_concordant.v
• is_derive_ou comparison/ornstein_uhlenbeck.v
• is_derive_ou_d1 comparison/ornstein_uhlenbeck.v
• is_derive_ou_t comparison/ornstein_uhlenbeck.v
• is_derive_Rintegral comparison/gauss_smoothing.v
• is_derive_rV_comp gaussian/gauss_interpolation.v
• is_derive_sc_omega convex/self_concordant.v
• is_derive_sc_omega_star convex/self_concordant.v
• is_derive_scalel gaussian/gauss_interpolation.v
• is_derive_series_pow random_matrix/matrix_series.v
• is_derive_sin_mul fourier/charfun.v
• is_derive_sin_mulr fourier/charfun.v
• is_derive_smm comparison/gordon.v
• is_derive_smm_D comparison/gordon.v
• is_derive_softmax comparison/slepian.v
• is_derive_transfer gaussian/gauss_ibp.v
• is_net matrix/nets.v
• is_net_le matrix/nets.v
• is_net_sub matrix/nets.v
• ising_cexp SKGap/Ising.v
• ising_cexp_set SKGap/Ising.v
• ising_cond_mean SKGapDefinitions.v
• ising_cond_mean_lt1 SKGap/Ising.v
• ising_cond_mean_set SKGap/Ising.v
• ising_cond_var SKGapDefinitions.v
• ising_cond_var_ge0 SKGap/Ising.v
• ising_cond_var_le1 SKGap/Ising.v
• ising_cond_var_set SKGap/Ising.v
• ising_cov SKGapDefinitions.v
• ising_cov_form SKGap/Poincare.v
• ising_cov_from_gap SKGap/Poincare.v
• ising_cov_sym SKGap/Poincare.v
• ising_dirichlet SKGapDefinitions.v
• ising_dirichlet_eq0 SKGap/Ising.v
• ising_dirichlet_form SKGap/Poincare.v
• ising_dirichlet_ge0 SKGap/Ising.v
• ising_dirichletE SKGap/Ising.v
• ising_dproj SKGap/Ising.v
• ising_dproj_adj SKGap/Ising.v
• ising_dproj_eq SKGap/Ising.v
• ising_dproj_eq0 SKGap/Ising.v
• ising_energy SKGap/Ising.v
• ising_gap_from_square SKGap/Spectral.v
• ising_gen SKGap/Ising.v
• ising_gen_dot SKGap/Spectral.v
• ising_gen_form SKGap/Spectral.v
• ising_gen_ge0 SKGap/Spectral.v
• ising_gen_ker SKGap/Spectral.v
• ising_gen_lin SKGap/Spectral.v
• ising_gen_sq_expand SKGap/Poincare.v
• ising_gen_sq_ge SKGap/Poincare.v
• ising_gen_sym SKGap/Spectral.v
• ising_mass SKGapDefinitions.v
• ising_mass_gt0 SKGap/Ising.v
• ising_mass_sum SKGap/Ising.v
• ising_mean SKGapDefinitions.v
• ising_mean_block SKGap/TwoSpin.v
• ising_mean_cst SKGap/Ising.v
• ising_mean_eq0 SKGap/Ising.v
• ising_mean_ext SKGap/Ising.v
• ising_mean_ge0 SKGap/Ising.v
• ising_mean_le SKGap/Ising.v
• ising_mean_pair SKGap/Ising.v
• ising_mean_pair_eq SKGap/Ising.v
• ising_mean_sum SKGap/Ising.v
• ising_meanB SKGap/Ising.v
• ising_meanD SKGap/Ising.v
• ising_meanE SKGap/Ising.v
• ising_meanN SKGap/Ising.v
• ising_meanZ SKGap/Ising.v
• ising_pair_den SKGap/Ising.v
• ising_pair_val SKGap/Ising.v
• ising_two_spin SKGap/TwoSpin.v
• ising_two_spin_block SKGap/TwoSpin.v
• ising_var SKGapDefinitions.v
• ising_var_alt SKGap/Poincare.v
• ising_var_ge0 SKGap/Poincare.v
• ising_weight SKGapDefinitions.v
• ising_weight_block SKGap/Ising.v
• ising_weight_gt0 SKGap/Ising.v
• ising_Z_gt0 SKGap/Ising.v
• itv_dist matrix/condition_cone.v
• itv_dist_clamp matrix/condition_cone.v
• itv_dist_ge0 matrix/condition_cone.v
• itv_dist_le matrix/condition_cone.v
• itv_dist_lipschitz matrix/condition_cone.v
• itv_dist_shift matrix/condition_cone.v

J3

• jensen_max_norm probability/symmetrization.v
• jordan_cos fourier/esseen.v
• jordan_sin fourier/esseen.v

K16

• kfrac RandomSAT/Replacement.v
• kfrac0 RandomSAT/Replacement.v
• kfrac_ge0 RandomSAT/Replacement.v
• kfrac_le_half_pow RandomSAT/Replacement.v
• kfrac_le_pow RandomSAT/Replacement.v
• kfrac_small RandomSAT/Replacement.v
• kfrac_succ RandomSAT/Replacement.v
• kfrac_succ_lower RandomSAT/Replacement.v
• kill RandomSAT/Pivotal.v
• kill0 RandomSAT/Pivotal.v
• kill_ge0 RandomSAT/Pivotal.v
• kill_le1 RandomSAT/Pivotal.v
• kill_replacement RandomSAT/Replacement.v
• killE RandomSAT/Pivotal.v
• killE_forced RandomSAT/Replacement.v
• kills_frozen RandomSAT/Replacement.v

L188

• L_cst0 probability/finite_gap.v
• L_sum probability/finite_gap.v
• label_coupling probability/countable_mixture.v
• label_esum1 probability/countable_mixture.v
• label_esum_le probability/countable_mixture.v
• labels_le probability/countable_mixture.v
• lambda_max matrix/lambda_max.v
• lambda_max_attained matrix/lambda_max.v
• lambda_max_dim0 matrix/lambda_max.v
• lambda_max_eigenvector matrix/lambda_max.v
• lambda_max_form matrix/lambda_max.v
• lambda_max_has_sup matrix/lambda_max.v
• lambda_max_le matrix/lambda_max.v
• lambda_max_lipschitz matrix/lambda_max.v
• lambda_max_lipschitz_frobenius matrix/lambda_max.v
• lambda_max_net_le random_matrix/goe_edge.v
• lambda_max_opnorm matrix/lambda_max.v
• lambda_max_set_neq0 matrix/lambda_max.v
• lambda_max_ub matrix/lambda_max.v
• lambda_max_ubound matrix/lambda_max.v
• lambda_maxD matrix/lambda_max.v
• large_projection_card matrix/tensor_packing.v
• large_projection_cluster_card matrix/tensor_packing.v
• le0_small convex/moreau.v
• le1_sqr convex/feature_moments.v
• le_amgm convex/barrier_lindeberg.v
• le_conc_fun fourier/esseen.v
• le_expR34 probability/subgaussian.v
• le_infsup comparison/cgmt.v
• le_minmax comparison/gordon.v
• le_rmax comparison/slepian.v
• le_smm comparison/gordon.v
• le_weighted_sqr convex/barrier_lindeberg.v
• lebesgue_measure_affine comparison/normal_linear.v
• lebesgue_rV gaussian/lebesgue_rV.v
• lebesgue_rV_ball_le gaussian/lebesgue_rV.v
• lebesgue_rV_ball_scale fourier/charfun_rV.v
• lebesgue_rV_box gaussian/lebesgue_rV.v
• lebesgue_rV_col_perm gaussian/lebesgue_rV.v
• lebesgue_rV_cons gaussian/lebesgue_rV.v
• lebesgue_rV_gauss_integral gaussian/lebesgue_rV.v
• lebesgue_rV_preimage gaussian/lebesgue_rV.v
• lebesgue_rV_rec gaussian/lebesgue_rV.v
• lebesgue_rV_row_mx gaussian/lebesgue_rV.v
• lebesgue_rV_scale gaussian/lebesgue_rV.v
• lebesgue_rV_shift gaussian/lebesgue_rV.v
• lebesgue_rV_unique gaussian/lebesgue_rV.v
• lebesgue_rVS gaussian/lebesgue_rV.v
• lee_prod fourier/small_ball.v
• lee_prod_ge0 probability/subgaussian.v
• leq_ffact_expn matrix/nets.v
• ler_binom_mean RandomSAT/Forcing.v
• ler_clause_avg RandomSAT/Pivotal.v
• ler_frobeniusB matrix/euclidean.v
• ler_max_norm probability/symmetrization.v
• ler_mxdot matrix/euclidean.v
• ler_rademacher_mean probability/symmetrization.v
• ler_tuple_avg RandomSAT/Pivotal.v
• ler_tuple_avg_cst RandomSAT/Forcing.v
• ler_unif_mean probability/finite_mean.v
• level random_matrix/restricted_isometry.v
• level_alpha random_matrix/restricted_isometry.v
• level_cover random_matrix/restricted_isometry.v
• level_size random_matrix/restricted_isometry.v
• level_sum random_matrix/restricted_isometry.v
• level_supp random_matrix/restricted_isometry.v
• level_uniq random_matrix/restricted_isometry.v
• Lfun1_mixture probability/mixture.v
• Lfun2_mixture probability/mixture.v
• Lfun2_sqr probability/moments.v
• Lfun4_sqr probability/moments.v
• life RandomSAT/Model.v
• life0 RandomSAT/Model.v
• life_ge0 RandomSAT/Model.v
• life_le RandomSAT/Model.v
• life_mean RandomSAT/Pivotal.v
• life_mean_ge0 RandomSAT/Pivotal.v
• life_mean_sum RandomSAT/Pivotal.v
• life_meanS RandomSAT/Pivotal.v
• life_mono RandomSAT/Model.v
• life_sum RandomSAT/Model.v
• life_var RandomSAT/Pivotal.v
• life_var_le_occ RandomSAT/Pivotal.v
• life_var_succ_le RandomSAT/Pivotal.v
• lin_expand SKGap/Ising.v
• lin_form_vec convex/self_concordant.v
• lindeberg_replacement probability/lindeberg.v
• lindeberg_telescope convex/barrier_lindeberg.v
• line_derive3 convex/self_concordant.v
• lipschitz_add_gauss fourier/inversion.v
• lipschitz_frobenius_bound comparison/gauss_concentration.v
• lipschitz_frobenius_continuous comparison/gauss_smoothing.v
• lipschitz_frobenius_grad comparison/gauss_smoothing.v
• lipschitz_frobenius_mulmx comparison/gauss_law.v
• lipschitz_pos comparison/gauss_law.v
• lipschitz_pos_agree comparison/gauss_law.v
• lipschitz_pos_setT comparison/gauss_law.v
• ln2_le1 random_matrix/restricted_isometry.v
• ln2D_ge random_matrix/matrix_series.v
• ln_ge_half_sub_inv comparison/chi_square.v
• ln_ge_sub_half_sqr comparison/chi_square.v
• ln_le_sub1 random_matrix/restricted_isometry.v
• ln_le_subr1 matrix/tensor_packing.v
• ln_prod convex/logdet_barrier.v
• ln_sub_ge convex/logdet_barrier.v
• ln_subgamma comparison/chi_square.v
• lnb2_le random_matrix/restricted_isometry.v
• lnX_le random_matrix/restricted_isometry.v
• log_partition_derive3 probability/log_partition.v
• logdet2_sc_barrier convex/logdet_barrier.v
• logdet_barrier convex/logdet_barrier.v
• logdet_barrier2 convex/logdet_barrier.v
• logdet_barrier2_ge0 convex/logdet_barrier.v
• logdet_barrier2_one convex/logdet_barrier.v
• logdet_barrier_ge0 convex/logdet_barrier.v
• logdet_barrier_one convex/logdet_barrier.v
• logdet_line convex/logdet_barrier.v
• logdet_sc_barrier convex/logdet_barrier.v
• logsum convex/logdet_barrier.v
• logsum1 convex/logdet_barrier.v
• logsum2 convex/logdet_barrier.v
• logsum2_ge0 convex/logdet_barrier.v
• logsum3 convex/logdet_barrier.v
• logsum_blowup convex/logdet_barrier.v
• logsum_bp convex/logdet_barrier.v
• logsum_derive convex/logdet_barrier.v
• logsum_sc convex/logdet_barrier.v
• logsum_sc_barrier convex/logdet_barrier.v
• loo_compare convex/barrier_lindeberg.v
• loo_variance convex/barrier_lindeberg.v
• Lp random_matrix/restricted_isometry.v
• Lp_ge1 random_matrix/restricted_isometry.v
• ls_A0 convex/minimizers.v
• ls_barrier_minimizer convex/minimizers.v
• ls_barrier_objective convex/least_squares.v
• ls_barrier_value convex/least_squares.v
• ls_barrier_value_empty convex/least_squares.v
• ls_barrier_value_ge0 convex/least_squares.v
• ls_barrier_value_le convex/least_squares.v
• ls_barrier_value_mono convex/least_squares.v
• ls_barrier_valueE convex/barrier_lindeberg.v
• ls_bopt convex/minimizers.v
• ls_bopt_linear convex/minimizers.v
• ls_bopt_tuple_set probability/measurable_minimizer.v
• ls_first_order convex/minimizers.v
• ls_grad convex/minimizers.v
• ls_loss convex/least_squares.v
• ls_min probability/measurable_minimizer.v
• ls_min_exists probability/measurable_minimizer.v
• ls_min_growth probability/measurable_minimizer.v
• ls_min_in probability/measurable_minimizer.v
• ls_min_le probability/measurable_minimizer.v
• ls_min_tuple_set probability/measurable_minimizer.v
• ls_min_unique probability/measurable_minimizer.v
• ls_minP probability/measurable_minimizer.v
• ls_objective convex/least_squares.v
• ls_objective_convex convex/barrier_removal.v
• ls_objective_ge0 convex/least_squares.v
• ls_reduced probability/measurable_minimizer.v
• ls_reduced_le probability/measurable_minimizer.v
• ls_reduced_tuple_set probability/measurable_minimizer.v
• ls_ref_scale convex/barrier_lindeberg.v
• ls_ridge convex/least_squares.v
• ls_ridge_bopt convex/minimizers.v
• ls_ridge_coercive convex/minimizers.v
• ls_ridge_expand convex/minimizers.v
• ls_ridge_ge0 convex/minimizers.v
• ls_ridge_ge0' convex/barrier_lindeberg.v
• ls_taylor convex/minimizers.v
• ls_value convex/least_squares.v
• ls_value_barrierE convex/least_squares.v
• ls_value_ge0 convex/least_squares.v
• ls_value_le convex/least_squares.v
• ls_value_mono convex/least_squares.v
• lse comparison/slepian.v
• lse_D2 comparison/slepian.v
• lse_D2E comparison/slepian.v
• lse_DE comparison/slepian.v
• lse_differentiable comparison/slepian.v
• lse_hessian comparison/slepian.v
• lse_le_rmax comparison/slepian.v
• lse_norm comparison/slepian.v
• lse_sum_gt0 comparison/slepian.v
• lsize random_matrix/restricted_isometry.v
• lvl_lo random_matrix/restricted_isometry.v
• lvl_lo_ge0 random_matrix/restricted_isometry.v
• Lz random_matrix/restricted_isometry.v
• Lz_ge9 random_matrix/restricted_isometry.v

M367

• markov_ge0 probability/small_ball_method.v
• markov_lt convex/ridge_comparison.v
• matrix_series_statement MatrixSeriesStatement.v
• matrix_series_theorem MatrixSeriesTheorem.v
• matrix_small_ball matrix/covering.v
• max0_leD comparison/cgmt.v
• max_norm probability/symmetrization.v
• max_norm_ge0 probability/symmetrization.v
• max_normD probability/symmetrization.v
• max_normN probability/symmetrization.v
• maximal_separated_subset matrix/tensor_packing.v
• maxnorm random_matrix/restricted_isometry.v
• maxnorm_ge0 random_matrix/restricted_isometry.v
• maxr_dist comparison/gauss_law.v
• mean_value_coord gaussian/partial_derivative.v
• measurable_addmx gaussian/measurable_matrix.v
• measurable_affine comparison/normal_linear.v
• measurable_bad_event random_matrix/restricted_isometry.v
• measurable_ball_rV fourier/charfun_rV.v
• measurable_bigmax0 probability/symmetrization.v
• measurable_bigmax_seq matrix/random_opnorm.v
• measurable_centered_chi2 comparison/chi_square.v
• measurable_cf_rV_density fourier/inversion.v
• measurable_cf_rV_im fourier/charfun_rV.v
• measurable_cf_rV_kernel fourier/inversion.v
• measurable_cf_rV_norm fourier/charfun_rV.v
• measurable_cf_rV_re fourier/charfun_rV.v
• measurable_cgmt_aux comparison/cgmt.v
• measurable_clip_profile probability/clip_profile.v
• measurable_col_mx gaussian/measurable_matrix.v
• measurable_col_perm gaussian/measurable_matrix.v
• measurable_colsum_mx matrix/covering.v
• measurable_const_mx gaussian/measurable_matrix.v
• measurable_cos fourier/charfun.v
• measurable_cos_comp fourier/charfun.v
• measurable_cos_mul fourier/charfun.v
• measurable_cross_event random_matrix/restricted_isometry.v
• measurable_derive_rV gaussian/gauss_ibp.v
• measurable_dsubmx gaussian/measurable_matrix.v
• measurable_escape_inf comparison/cgmt.v
• measurable_escape_proj comparison/escape.v
• measurable_expR_sqr comparison/chi_square.v
• measurable_expR_sqr probability/subgaussian.v
• measurable_first_min probability/measurable_minimizer.v
• measurable_fun_mxP gaussian/measurable_matrix.v
• measurable_gauss2_rot comparison/gauss_rotation.v
• measurable_gauss_pdf gaussian/lebesgue_rV.v
• measurable_gauss_weight fourier/gauss_factor.v
• measurable_goe_diag_max random_matrix/goe_entries.v
• measurable_goe_entry random_matrix/goe_entries.v
• measurable_goe_entry_ge random_matrix/goe_entries.v
• measurable_goe_lambda_max random_matrix/goe_edge.v
• measurable_goe_lambda_maxN random_matrix/goe_edge.v
• measurable_goe_mx random_matrix/goe_rotation.v
• measurable_goe_offdiag_max random_matrix/goe_entries.v
• measurable_goe_opnorm_ge random_matrix/goe_entries.v
• measurable_goe_row_ge random_matrix/goe_entries.v
• measurable_goe_row_max random_matrix/goe_entries.v
• measurable_idR fourier/charfun.v
• measurable_inf_rel_open convex/barrier_lindeberg.v
• measurable_integral1 probability/efron_stein.v
• measurable_integral2 probability/efron_stein.v
• measurable_integral_tuple_set probability/efron_stein.v
• measurable_lipschitz_gt0 comparison/gauss_law.v
• measurable_lipschitz_pos comparison/gauss_law.v
• measurable_ls_barrier_value convex/barrier_lindeberg.v
• measurable_ls_bopt_min probability/measurable_minimizer.v
• measurable_ls_min probability/measurable_minimizer.v
• measurable_ls_reduced convex/barrier_lindeberg.v
• measurable_ls_reduced_at probability/measurable_minimizer.v
• measurable_ls_value convex/ridge_comparison.v
• measurable_lsubmx gaussian/measurable_matrix.v
• measurable_matrix gaussian/measurable_matrix.v
• measurable_max_norm probability/symmetrization.v
• measurable_mehler comparison/ornstein_uhlenbeck.v
• measurable_mehler_kernel comparison/ornstein_uhlenbeck.v
• measurable_merge_section probability/conditioning.v
• measurable_minimizer probability/measurable_minimizer.v
• measurable_mulmx gaussian/measurable_matrix.v
• measurable_mxbox gaussian/measurable_matrix.v
• measurable_mxboxes gaussian/measurable_matrix.v
• measurable_mxdot comparison/gauss_linear.v
• measurable_mxdot_comb random_matrix/restricted_isometry.v
• measurable_mxdot_fun probability/measurable_minimizer.v
• measurable_mxdot_ls_min probability/measurable_minimizer.v
• measurable_mxdot_tnth convex/barrier_lindeberg.v
• measurable_mxdotl comparison/gauss_shift.v
• measurable_mxdotl convex/feature_moments.v
• measurable_mxentry gaussian/measurable_matrix.v
• measurable_mxvec comparison/gauss_matrix_law.v
• measurable_norm2 convex/feature_moments.v
• measurable_opnorm probability/subgaussian_matrix.v
• measurable_oppmx gaussian/measurable_matrix.v
• measurable_partial_Rintegral probability/lindeberg.v
• measurable_perceptron_pressure Perceptron/Pressure.v
• measurable_quad convex/feature_moments.v
• measurable_rademacher_mean probability/symmetrization.v
• measurable_ramp probability/small_ball_method.v
• measurable_Rintegral1 fourier/esseen.v
• measurable_Rintegral2 fourier/esseen.v
• measurable_row_mx gaussian/measurable_matrix.v
• measurable_row_perm gaussian/measurable_matrix.v
• measurable_rowbox gaussian/measurable_matrix.v
• measurable_rsubmx gaussian/measurable_matrix.v
• measurable_rV_cons gaussian/gauss.v
• measurable_rV_scale gaussian/lebesgue_rV.v
• measurable_rV_shift gaussian/lebesgue_rV.v
• measurable_scalemx gaussian/measurable_matrix.v
• measurable_semicircle_pdf probability/semicircle_law.v
• measurable_series_opnorm random_matrix/matrix_series.v
• measurable_set_lt convex/ridge_comparison.v
• measurable_shift_density comparison/gauss_shift.v
• measurable_sin fourier/charfun.v
• measurable_sin_comp fourier/charfun.v
• measurable_sin_mul fourier/charfun.v
• measurable_sk_coupling_opnorm SKGap/Disorder.v
• measurable_small_ball_event probability/small_ball_method.v
• measurable_sum_pred convex/barrier_lindeberg.v
• measurable_sym_diff fourier/gauss_factor.v
• measurable_trmx gaussian/measurable_matrix.v
• measurable_tuple_ball_rV fourier/small_ball.v
• measurable_tuple_box probability/conditioning.v
• measurable_tuple_boxes probability/conditioning.v
• measurable_tuple_cat probability/tuple_rows.v
• measurable_tuple_cons probability/lindeberg.v
• measurable_tuple_cons_l probability/lindeberg.v
• measurable_tuple_cons_r probability/lindeberg.v
• measurable_tuple_left probability/symmetrization.v
• measurable_tuple_lincomb fourier/charfun.v
• measurable_tuple_map probability/tuple_rows.v
• measurable_tuple_merge probability/conditioning.v
• measurable_tuple_mx comparison/gauss_matrix_law.v
• measurable_tuple_mx_comb random_matrix/restricted_isometry.v
• measurable_tuple_pick probability/conditioning.v
• measurable_tuple_right probability/symmetrization.v
• measurable_tuple_rows probability/tuple_rows.v
• measurable_tuple_set probability/lindeberg.v
• measurable_tuple_set_integral probability/efron_stein.v
• measurable_tuple_set_pair probability/efron_stein.v
• measurable_tuple_sum fourier/gauss_factor.v
• measurable_tuple_sum_rV fourier/small_ball.v
• measurable_upper_pow probability/variational.v
• measurable_usubmx gaussian/measurable_matrix.v
• measurable_variance1 probability/efron_stein.v
• measurable_variance2 probability/efron_stein.v
• measurable_variance_tuple_set probability/efron_stein.v
• measurable_vec_mx comparison/gauss_matrix_law.v
• measure_bigcup_fin_le random_matrix/goe_entries.v
• measure_bigsetU_le random_matrix/restricted_isometry.v
• measure_ge_expR comparison/normal_mgf.v
• measure_lipschitz_unique comparison/gauss_law.v
• measure_matrix_display gaussian/measurable_matrix.v
• measure_mxbox_unique gaussian/measurable_matrix.v
• measure_rowbox_unique gaussian/measurable_matrix.v
• measure_tuple_box_unique probability/conditioning.v
• mehler comparison/ornstein_uhlenbeck.v
• mehler0 comparison/ornstein_uhlenbeck.v
• mehler1 comparison/ornstein_uhlenbeck.v
• mehler_bound comparison/ornstein_uhlenbeck.v
• mehler_contraction comparison/ornstein_uhlenbeck.v
• mehler_cvg1 comparison/ornstein_uhlenbeck.v
• mehler_cvg_L1 comparison/ornstein_uhlenbeck.v
• mehler_d1 comparison/ornstein_uhlenbeck.v
• mehler_d1_le comparison/ornstein_uhlenbeck.v
• mehler_d2 comparison/ornstein_uhlenbeck.v
• mehler_d2_le comparison/ornstein_uhlenbeck.v
• mehler_d3 comparison/ornstein_uhlenbeck.v
• mehler_dr comparison/ornstein_uhlenbeck.v
• mehler_dr_le comparison/ornstein_uhlenbeck.v
• mehler_dr_split comparison/ornstein_uhlenbeck.v
• mehler_ge comparison/ornstein_uhlenbeck.v
• mehler_generator comparison/ornstein_uhlenbeck.v
• mehler_kernel comparison/ornstein_uhlenbeck.v
• mehler_kernel_gt0 comparison/ornstein_uhlenbeck.v
• mehler_kernel_integral comparison/ornstein_uhlenbeck.v
• mehler_kernel_le comparison/ornstein_uhlenbeck.v
• mehler_kernel_mul_le comparison/ornstein_uhlenbeck.v
• mehler_le comparison/ornstein_uhlenbeck.v
• mem_allnet random_matrix/restricted_isometry.v
• mem_budget matrix/nets.v
• mem_restrict_rename RandomSAT/Forcing.v
• mem_sets_le random_matrix/restricted_isometry.v
• mem_sign_lists matrix/nets.v
• mem_wconf random_matrix/restricted_isometry.v
• mem_xconf random_matrix/restricted_isometry.v
• mesh random_matrix/restricted_isometry.v
• mesh_gt0 random_matrix/restricted_isometry.v
• mesh_sum random_matrix/restricted_isometry.v
• mgf_tail probability/subgaussian_matrix.v
• mgf_upper_tail probability/subgaussian_matrix.v
• min_le_lin RandomSAT/Variance.v
• minmax comparison/gordon.v
• minmax_add comparison/escape.v
• minmax_aux comparison/escape.v
• minmax_bil_le comparison/escape.v
• minmax_bil_sph_le comparison/escape.v
• minmax_le comparison/gordon.v
• minmax_leD comparison/gordon.v
• minmax_lipschitz comparison/gordon.v
• minmax_norm comparison/gordon.v
• minmax_sph comparison/escape.v
• minmax_sph_ge comparison/escape.v
• minmax_sph_le comparison/escape.v
• minmax_sph_lipschitz comparison/escape.v
• minmax_sph_range comparison/escape.v
• minr_dist comparison/gauss_law.v
• mixture probability/mixture.v
• mixture_cover probability/mixture.v
• mixture_regular_feature convex/feature_mixture.v
• mixture_regular_feature_dot convex/feature_mixture.v
• mixture_weights probability/mixture.v
• mixture_weights_ge0 probability/mixture.v
• mixture_weights_inhabited probability/mixture.v
• mixture_weights_prod probability/mixture.v
• mixture_weights_sum probability/mixture.v
• mixtureE probability/mixture.v
• moment4_int4 convex/feature_mixture.v
• moment4_int_lin convex/feature_mixture.v
• moment4_int_lin2 convex/feature_mixture.v
• moment4_int_norm4 convex/feature_mixture.v
• moment4_int_quad convex/feature_mixture.v
• moment4_integrable convex/feature_mixture.v
• moment4_Lfun1_lin convex/feature_mixture.v
• moment4_Lfun1_lin2 convex/feature_mixture.v
• moment4_Lfun2_quad convex/feature_mixture.v
• moment_root_le random_matrix/matrix_series.v
• moment_root_powR random_matrix/matrix_series.v
• monomials_bound SKGap/TwoSpin.v
• moreau convex/moreau.v
• moreau_norm convex/moreau.v
• mul_orthogonalmx matrix/euclidean.v
• mulmx_col_mx gaussian/gauss_interpolation.v
• mulmx_col_mxdot matrix/spectral_gap.v
• mulmx_delta_entry random_matrix/goe.v
• mulmx_delta_entry0 random_matrix/goe_rotation.v
• mulmx_outer_rV fourier/small_ball.v
• mx_norm_col_mx_le gaussian/measurable_matrix.v
• mx_norm_col_perm_le gaussian/measurable_matrix.v
• mx_norm_entry_le gaussian/measurable_matrix.v
• mx_norm_exprn_le gaussian/measurable_matrix.v
• mx_norm_frobenius comparison/cgmt.v
• mx_norm_le_frobenius matrix/real_spectral.v
• mx_norm_le_opnorm matrix/opnorm.v
• mx_norm_mulmx_le gaussian/measurable_matrix.v
• mx_polyfun random_matrix/goe.v
• mx_polyfun_cst random_matrix/goe.v
• mx_polyfun_exp random_matrix/goe.v
• mx_polyfun_goe random_matrix/goe.v
• mx_polyfun_mul random_matrix/goe.v
• mx_polyfun_mxpow_deriv random_matrix/goe.v
• mx_polyfun_series random_matrix/matrix_series.v
• mx_polyfun_sum random_matrix/goe.v
• mx_polyfunD random_matrix/goe.v
• mx_polyfunZ random_matrix/goe.v
• mxbox gaussian/measurable_matrix.v
• mxboxes gaussian/measurable_matrix.v
• mxboxI gaussian/measurable_matrix.v
• mxboxT gaussian/measurable_matrix.v
• mxcoef matrix/tensor_packing.v
• mxcoef_compress_near matrix/tensor_packing.v
• mxcoef_sum matrix/tensor_packing.v
• mxcoefB matrix/tensor_packing.v
• mxcoefD matrix/tensor_packing.v
• mxdot matrix/euclidean.v
• mxdot0l matrix/euclidean.v
• mxdot0r matrix/euclidean.v
• mxdot1l matrix/trace_projection.v
• mxdot_block0 matrix/psd_splitting.v
• mxdot_cauchy_schwarz matrix/euclidean.v
• mxdot_coef_map matrix/nuclear.v
• mxdot_col matrix/opnorm.v
• mxdot_col_mx random_matrix/matrix_series.v
• mxdot_colE matrix/euclidean.v
• mxdot_compress matrix/psd_splitting.v
• mxdot_conj random_matrix/goe_rotation.v
• mxdot_conjmx matrix/trace_projection.v
• mxdot_convex convex/barrier_removal.v
• mxdot_delta matrix/euclidean.v
• mxdot_delta_opnorm matrix/opnorm.v
• mxdot_deltal SKGap/Ising.v
• mxdot_diag matrix/euclidean.v
• mxdot_disj random_matrix/restricted_isometry.v
• mxdot_entry matrix/euclidean.v
• mxdot_eq0 matrix/euclidean.v
• mxdot_form_lipschitz probability/small_ball_method.v
• mxdot_form_outer probability/small_ball_method.v
• mxdot_ge0 matrix/euclidean.v
• mxdot_goe_coef_row random_matrix/goe_entries.v
• mxdot_gt0 matrix/euclidean.v
• mxdot_hw_mask probability/hanson_wright.v
• mxdot_le matrix/euclidean.v
• mxdot_le_mx_norm comparison/brascamp_lieb.v
• mxdot_le_nuclear matrix/nuclear.v
• mxdot_mulmx_le comparison/cgmt.v
• mxdot_mulmx_opnorm_le random_matrix/matrix_series.v
• mxdot_mulmx_sum matrix/spectral_gap.v
• mxdot_mulmx_sym matrix/real_spectral.v
• mxdot_mulmxl matrix/euclidean.v
• mxdot_mulmxr matrix/euclidean.v
• mxdot_mxvec convex/logdet_barrier.v
• mxdot_mxvec_mxvec random_matrix/goe_edge.v
• mxdot_net_bound matrix/nets.v
• mxdot_opnorm matrix/opnorm.v
• mxdot_orthogonalmxl matrix/euclidean.v
• mxdot_orthogonalmxr matrix/euclidean.v
• mxdot_outer matrix/euclidean.v
• mxdot_outer2 matrix/euclidean.v
• mxdot_proj comparison/escape.v
• mxdot_psd_ge0 matrix/psd_part.v
• mxdot_psd_le matrix/random_opnorm.v
• mxdot_psd_part_shift matrix/psd_part.v
• mxdot_quad_vec matrix/condition_cone.v
• mxdot_quadE convex/feature_moments.v
• mxdot_restr random_matrix/restricted_isometry.v
• mxdot_row_mx convex/ls_insertion.v
• mxdot_row_tail comparison/gauss_linear.v
• mxdot_rowE matrix/euclidean.v
• mxdot_rowproj_perp matrix/tensor_packing.v
• mxdot_rV_cons comparison/gauss_linear.v
• mxdot_self_le_norm convex/gauss_feature.v
• mxdot_spec matrix/von_neumann.v
• mxdot_spec_le matrix/psd_part.v
• mxdot_sqr_sum convex/feature_moments.v
• mxdot_sum_disj random_matrix/restricted_isometry.v
• mxdot_suml matrix/euclidean.v
• mxdot_sumr matrix/euclidean.v
• mxdot_sym_part matrix/random_opnorm.v
• mxdot_sym_tr matrix/psd_splitting.v
• mxdot_tensor matrix/tensor_packing.v
• mxdot_tensor_form matrix/tensor_packing.v
• mxdot_trace matrix/euclidean.v
• mxdot_trace_scalel matrix/trace_projection.v
• mxdot_trmx matrix/euclidean.v
• mxdot_trmx_form matrix/random_opnorm.v
• mxdot_tuple_mx random_matrix/restricted_isometry.v
• mxdot_unit_dim matrix/lambda_max.v
• mxdot_unit_le1 comparison/brascamp_lieb.v
• mxdot_vec_mx matrix/condition_cone.v
• mxdot_vec_mxl random_matrix/goe_edge.v
• mxdot_vec_mxr matrix/nuclear.v
• mxdot_wvec probability/finite_gap.v
• mxdotBl matrix/euclidean.v
• mxdotBr matrix/euclidean.v
• mxdotC matrix/euclidean.v
• mxdotDl matrix/euclidean.v
• mxdotDr matrix/euclidean.v
• mxdotNl matrix/euclidean.v
• mxdotNr matrix/euclidean.v
• mxdotZl matrix/euclidean.v
• mxdotZr matrix/euclidean.v
• mxpow_deriv random_matrix/goe.v
• mxpow_deriv_trace random_matrix/goe.v
• mxpow_derivD random_matrix/goe.v
• mxpow_derivS random_matrix/goe.v
• mxpow_derivZ random_matrix/goe.v
• mxtrace_ABAB_le matrix/real_spectral.v
• mxtrace_conj matrix/trace_projection.v
• mxtrace_diag_sandwich random_matrix/matrix_series.v
• mxtrace_divK matrix/trace_projection.v
• mxtrace_mul_psd_le random_matrix/matrix_series.v
• mxtrace_psd_ge0 matrix/psd_splitting.v
• mxtrace_sandwich_le random_matrix/matrix_series.v
• mxtrace_scale matrix/trace_projection.v
• mxtrace_sqr_le matrix/trace_projection.v
• mxtraceB matrix/trace_projection.v
• mxvec_index_eq comparison/gordon.v
• mxvec_index_val comparison/gordon.v

N57

• nbase random_matrix/restricted_isometry.v
• nbase_ge1 random_matrix/restricted_isometry.v
• net random_matrix/restricted_isometry.v
• net_exists matrix/nets.v
• net_family comparison/escape.v
• net_log_le matrix/random_opnorm.v
• net_spec random_matrix/restricted_isometry.v
• netP random_matrix/restricted_isometry.v
• nonneg_part matrix/psd_splitting.v
• norm_concentration probability/subgaussian_matrix.v
• norm_vec_mx_le comparison/gordon.v
• normal2_rotation comparison/gauss_rotation.v
• normal_continuous_approx comparison/ornstein_uhlenbeck.v
• normal_ibp gaussian/gauss_ibp.v
• normal_mean gaussian/gauss_moments.v
• normal_moment_even gaussian/gauss_moments.v
• normal_moment_odd gaussian/gauss_moments.v
• normal_momentS gaussian/gauss_moments.v
• normal_pdf01_rotation comparison/gauss_rotation.v
• normal_pdf01_shift comparison/gauss_shift.v
• normal_pdf01E gaussian/gauss_ibp.v
• normal_pdf01N gaussian/gauss_ibp.v
• normal_pdf_affine comparison/normal_linear.v
• normal_pdf_conv comparison/normal_linear.v
• normal_pdf_expR comparison/normal_mgf.v
• normal_pdf_expR_sqr comparison/chi_square.v
• normal_pdf_mehler comparison/ornstein_uhlenbeck.v
• normal_pdf_normr comparison/gauss_linear.v
• normal_peak1V fourier/gauss_factor.v
• normal_prob_abs_tail comparison/normal_mgf.v
• normal_prob_affine comparison/normal_linear.v
• normal_prob_ge comparison/normal_mgf.v
• normal_prob_itv_ge comparison/sudakov.v
• normal_prob_le comparison/normal_mgf.v
• normal_prob_lincomb comparison/normal_linear.v
• normal_prob_lower_tail comparison/normal_mgf.v
• normal_prob_normr comparison/gauss_linear.v
• normal_prob_upper_tail comparison/normal_mgf.v
• normr_rademacher probability/symmetrization.v
• normr_Rintegral_gauss_le comparison/gauss_law.v
• normr_Rintegral_normal_le comparison/ornstein_uhlenbeck.v
• normr_Rintegral_normal_mul_le comparison/ornstein_uhlenbeck.v
• nrm_cov comparison/cgmt.v
• nrm_mx comparison/cgmt.v
• nuclear matrix/nuclear.v
• nuclear_eq0 matrix/nuclear.v
• nuclear_ge0 matrix/nuclear.v
• nuclear_has_sup matrix/nuclear.v
• nuclear_le matrix/nuclear.v
• nuclear_le_frobenius matrix/nuclear.v
• nuclear_outer matrix/nuclear.v
• nuclear_spectral matrix/nuclear.v
• nuclear_sym matrix/nuclear.v
• nuclear_ub matrix/nuclear.v
• nuclearD matrix/nuclear.v
• nuclearN matrix/nuclear.v
• nuclearZ matrix/nuclear.v

O72

• occ RandomSAT/Pivotal.v
• occ_ge0 RandomSAT/Pivotal.v
• occS RandomSAT/Pivotal.v
• offdiag_decouple probability/hanson_wright.v
• one_sub_le_expR probability/total_variation.v
• onem_sqr_gt0 comparison/ornstein_uhlenbeck.v
• open_measurable_mx gaussian/measurable_matrix.v
• opnorm matrix/opnorm.v
• opnorm0 matrix/opnorm.v
• opnorm_bilinearP matrix/opnorm.v
• opnorm_block_diag_le random_matrix/matrix_series.v
• opnorm_compress_gram matrix/tensor_packing.v
• opnorm_diag01 probability/hanson_wright.v
• opnorm_diag_mx_le random_matrix/goe_entries.v
• opnorm_exp_le_trace matrix/opnorm.v
• opnorm_exp_le_trace_even matrix/opnorm.v
• opnorm_ge0 matrix/opnorm.v
• opnorm_goe_mx random_matrix/goe.v
• opnorm_has_sup matrix/opnorm.v
• opnorm_hw_mask probability/hanson_wright.v
• opnorm_lambda_max matrix/lambda_max.v
• opnorm_le matrix/opnorm.v
• opnorm_le_form_exp matrix/opnorm.v
• opnorm_le_frobenius matrix/opnorm.v
• opnorm_le_sym_dilation random_matrix/matrix_series.v
• opnorm_le_trace_exp matrix/opnorm.v
• opnorm_leP matrix/opnorm.v
• opnorm_lipschitz comparison/escape.v
• opnorm_mulmx matrix/opnorm.v
• opnorm_net matrix/nets.v
• opnorm_net_bilinear matrix/nets.v
• opnorm_net_sphere matrix/nets.v
• opnorm_net_sym matrix/nets.v
• opnorm_orthogonalmxl matrix/opnorm.v
• opnorm_orthogonalmxr matrix/opnorm.v
• opnorm_row_sum matrix/spectral_gap.v
• opnorm_spectral matrix/opnorm.v
• opnorm_sqr_le convex/gauss_feature.v
• opnorm_sub_diag_le random_matrix/goe_entries.v
• opnorm_sum_subexponential matrix/random_opnorm.v
• opnorm_sym_part_net matrix/random_opnorm.v
• opnorm_symP matrix/opnorm.v
• opnorm_tail_mgf probability/subgaussian_matrix.v
• opnorm_trmx matrix/opnorm.v
• opnorm_ub matrix/opnorm.v
• opnormD matrix/opnorm.v
• opnormN matrix/opnorm.v
• opnormZ matrix/opnorm.v
• opp_ffun RandomSAT/Replacement.v
• ord_ext probability/hanson_wright.v
• ord_extE probability/hanson_wright.v
• orthogonal_block_mx matrix/euclidean.v
• orthogonal_sqr_col matrix/von_neumann.v
• orthogonal_sqr_row matrix/von_neumann.v
• orthogonalmx matrix/euclidean.v
• orthogonalmx1 matrix/euclidean.v
• orthogonalmx_key matrix/euclidean.v
• orthogonalmx_row_unit matrix/real_spectral.v
• orthogonalmx_unit matrix/euclidean.v
• orthogonalmxP matrix/euclidean.v
• orthogonalmxT matrix/euclidean.v
• orthonormal_entry_le1 convex/barrier_lindeberg.v
• orthoprojmx matrix/psd_splitting.v
• orthoprojmx0 matrix/psd_splitting.v
• orthoprojmx1 matrix/psd_splitting.v
• orthoprojmxB matrix/psd_splitting.v
• ou comparison/ornstein_uhlenbeck.v
• ou0 comparison/ornstein_uhlenbeck.v
• ou_cvg0 comparison/ornstein_uhlenbeck.v
• ou_cvg0_L1 comparison/ornstein_uhlenbeck.v
• ou_cvgy comparison/ornstein_uhlenbeck.v
• ouE comparison/ornstein_uhlenbeck.v

P147

• p_ge0 RandomSAT/Forcing.v
• p_le1 RandomSAT/Forcing.v
• pair_cross_mean SKGap/TwoSpin.v
• pair_factorization SKGap/TwoSpin.v
• pair_grad_bound SKGap/TwoSpin.v
• pair_quad_le SKGap/Poincare.v
• pair_signed_mean_lower SKGap/TwoSpin.v
• pair_two_spin SKGap/TwoSpin.v
• pairing_zero_sums comparison/gordon.v
• paley_zygmund probability/moments.v
• paley_zygmund_half probability/small_ball_method.v
• paley_zygmund_point probability/moments.v
• paley_zygmund_sqr probability/moments.v
• partials_diff_differentiable gaussian/partial_derivative.v
• partials_expansion gaussian/partial_derivative.v
• partials_linear gaussian/partial_derivative.v
• pcm SKGap/TwoSpin.v
• pcm_block_i SKGap/TwoSpin.v
• pcm_block_j SKGap/TwoSpin.v
• pcv SKGap/TwoSpin.v
• pcv_eq SKGap/TwoSpin.v
• pd_slice convex/logdet_barrier.v
• pd_slice2 convex/logdet_barrier.v
• pd_slice2_one convex/logdet_barrier.v
• pd_slice_one convex/logdet_barrier.v
• perceptron_pressure PerceptronSignDefinitions.v
• perceptron_pressure_derive3 Perceptron/Pressure.v
• perceptron_pressure_le Perceptron/Pressure.v
• perceptron_pressureE Perceptron/Pressure.v
• perceptron_sign_compare Perceptron/Pressure.v
• perceptron_sign_statement PerceptronSignStatement.v
• perceptron_sign_theorem PerceptronSignTheorem.v
• perm_mx_orthogonal matrix/euclidean.v
• perm_spec_seq matrix/von_neumann.v
• pg1 SKGap/TwoSpin.v
• pg2 SKGap/TwoSpin.v
• Phi_ge0 convex/barrier_lindeberg.v
• Phi_le convex/barrier_lindeberg.v
• Phi_meas convex/barrier_lindeberg.v
• pivot_sqr RandomSAT/Pivotal.v
• pivotal_local RandomSAT/Pivotal.v
• plaw SKGap/TwoSpin.v
• plaw_add SKGap/TwoSpin.v
• plaw_energy SKGap/TwoSpin.v
• plaw_energy_ge SKGap/TwoSpin.v
• plaw_energy_ge' SKGap/TwoSpin.v
• plaw_swap SKGap/TwoSpin.v
• pmean SKGap/TwoSpin.v
• pmean_add SKGap/TwoSpin.v
• pmean_const SKGap/TwoSpin.v
• pmean_le SKGap/TwoSpin.v
• pmean_scale SKGap/TwoSpin.v
• pmean_swap SKGap/TwoSpin.v
• polar convex/moreau.v
• polar0 convex/moreau.v
• polar_closed convex/moreau.v
• polar_convex convex/moreau.v
• poly_bound_ge0 gaussian/gauss.v
• poly_bound_le random_matrix/goe.v
• polyfun random_matrix/goe.v
• polyfun_bound2 random_matrix/goe.v
• polyfun_coord random_matrix/goe.v
• polyfun_cst random_matrix/goe.v
• polyfun_goe_clip random_matrix/goe.v
• polyfun_goe_stat_clip random_matrix/wigner.v
• polyfun_goe_tr random_matrix/goe.v
• polyfun_sum random_matrix/goe.v
• polyfun_trace random_matrix/goe.v
• polyfunB random_matrix/goe.v
• polyfunD random_matrix/goe.v
• polyfunM random_matrix/goe.v
• pos_row matrix/psd_part.v
• posdefmx convex/logdet_barrier.v
• posdefmx_congruence convex/logdet_barrier.v
• posdefmx_convex convex/logdet_barrier.v
• posdefmx_ge convex/logdet_barrier.v
• posdefmx_open convex/logdet_barrier.v
• posdefmx_scalar convex/logdet_barrier.v
• posdefmx_spectral convex/logdet_barrier.v
• posdefmx_unit convex/minimizers.v
• pow_le_norm SKGap/Poincare.v
• pow_one_sub_bounds probability/total_variation.v
• pow_one_sub_cvg probability/total_variation.v
• pow_one_sub_dist probability/total_variation.v
• poweR2 probability/efron_stein.v
• power_survival_bound RandomSAT/Replacement.v
• powR_sum fourier/small_ball.v
• pprefactor SKGap/TwoSpin.v
• pprefactor_bounds SKGap/TwoSpin.v
• prefix_sat SatVarianceDefinitions.v
• prefix_sat0 RandomSAT/Model.v
• prefix_sat_le RandomSAT/Model.v
• prefix_satE RandomSAT/Model.v
• prepend RandomSAT/Model.v
• prepend0 RandomSAT/Model.v
• prepend_ftail RandomSAT/Model.v
• prepend_lift RandomSAT/Model.v
• pressure_energy Perceptron/Pressure.v
• prob_density probability/density_law.v
• prob_density_tuple_prod probability/density_law.v
• prob_fine_itv probability/total_variation.v
• prob_fineB_le1 probability/total_variation.v
• probability_inhabited convex/barrier_lindeberg.v
• prod_gauss_le_cf_rV fourier/charfun_rV.v
• prod_mxvec comparison/gauss_matrix_law.v
• product_covering matrix/covering.v
• product_sections_null probability/atoms.v
• proj convex/moreau.v
• proj_eq convex/moreau.v
• proj_exists convex/moreau.v
• proj_nonexpansive convex/moreau.v
• proj_unique convex/moreau.v
• proj_variational convex/moreau.v
• projP convex/moreau.v
• proper_clause SatVarianceDefinitions.v
• proper_ftail RandomSAT/Model.v
• proper_ftail_None RandomSAT/Model.v
• proper_ftail_Some RandomSAT/Model.v
• proper_opp RandomSAT/Replacement.v
• proper_prepend RandomSAT/Model.v
• proper_rename RandomSAT/Forcing.v
• psd_conj matrix/psd_part.v
• psd_form_eq0 matrix/real_spectral.v
• psd_nearest matrix/psd_part.v
• psd_part matrix/psd_part.v
• psd_part_conj matrix/psd_part.v
• psd_part_moreau matrix/psd_part.v
• psd_part_nearest matrix/psd_part.v
• psd_part_nonexpansive matrix/psd_part.v
• psd_part_psd matrix/psd_part.v
• psd_partE matrix/psd_part.v
• psd_partZ matrix/psd_part.v
• psd_splitting matrix/psd_splitting.v
• psd_splitting_rel matrix/psd_splitting.v
• psd_splitting_statement PsdSplittingStatement.v
• psd_splitting_theorem PsdSplittingTheorem.v
• psd_square_gap matrix/spectral_gap.v
• psdmx matrix/psd_part.v
• psdmx0 matrix/psd_splitting.v
• psdmx_conj matrix/psd_splitting.v
• psdmx_exp_even random_matrix/matrix_series.v
• psdmx_sum matrix/psd_splitting.v
• psdmxD matrix/psd_splitting.v
• psi2_norm probability/subgaussian.v
• psign SKGap/TwoSpin.v
• psign_bound SKGap/TwoSpin.v
• psign_eq SKGap/TwoSpin.v

Q5

• quad_expand SKGap/Ising.v
• quad_expectation convex/feature_mixture.v
• quad_le_frobenius convex/feature_moments.v
• quad_response convex/minimizers.v
• quad_sqr_le convex/feature_moments.v

R183

• rademacher probability/symmetrization.v
• rademacher_gauss_lindeberg probability/rademacher_lindeberg.v
• rademacher_gauss_step probability/rademacher_lindeberg.v
• rademacher_mean probability/symmetrization.v
• rademacher_mean_abs_sum probability/symmetrization.v
• rademacher_mean_cst probability/symmetrization.v
• rademacher_mean_flip probability/symmetrization.v
• rademacher_mean_ge0 probability/symmetrization.v
• rademacher_mean_neg probability/symmetrization.v
• rademacher_mean_pair probability/symmetrization.v
• rademacher_mean_prod probability/symmetrization.v
• rademacher_mean_sqr_sum probability/symmetrization.v
• rademacher_mean_sum probability/symmetrization.v
• rademacher_meanD probability/symmetrization.v
• rademacher_meanZ probability/symmetrization.v
• rademacher_sqr probability/symmetrization.v
• rademacherN probability/symmetrization.v
• ramp probability/small_ball_method.v
• ramp0 probability/small_ball_method.v
• ramp1 probability/small_ball_method.v
• ramp_ge0 probability/small_ball_method.v
• ramp_le1 probability/small_ball_method.v
• ramp_lipschitz probability/small_ball_method.v
• ramp_sqr probability/small_ball_method.v
• range_duality matrix/nuclear.v
• range_duality_sym matrix/nuclear.v
• range_sphere comparison/escape.v
• range_sphere0 comparison/escape.v
• rat_approx_rV probability/small_ball_method.v
• ratio_le RandomSAT/Replacement.v
• rayleigh_max matrix/real_spectral.v
• ref_moment_bound convex/barrier_lindeberg.v
• ref_objective_int convex/ridge_comparison.v
• ref_objective_mean convex/ridge_comparison.v
• ref_objectiveE convex/ridge_comparison.v
• ref_point convex/barrier_lindeberg.v
• reg_cov convex/feature_moments.v
• reg_ell_int convex/feature_moments.v
• reg_ell_mean convex/feature_moments.v
• reg_ell_var convex/feature_moments.v
• reg_int4 convex/feature_moments.v
• reg_int_ell2 convex/feature_moments.v
• reg_int_lin convex/feature_moments.v
• reg_int_lin2 convex/feature_moments.v
• reg_int_norm4 convex/feature_moments.v
• reg_int_quad convex/feature_moments.v
• reg_int_quad2 convex/feature_moments.v
• reg_int_resid2 convex/feature_moments.v
• reg_int_resid4 convex/feature_moments.v
• reg_int_sqr convex/feature_moments.v
• reg_integrable convex/feature_moments.v
• reg_lambda_gt0 convex/feature_moments.v
• reg_mean convex/feature_moments.v
• reg_moment4 convex/feature_moments.v
• reg_quad_mean convex/feature_moments.v
• reg_quad_var convex/feature_moments.v
• reg_resid2 convex/feature_moments.v
• reg_resid4 convex/feature_moments.v
• regular_feature convex/least_squares.v
• rel_open_convex convex/self_concordant.v
• rel_open_convex_closure convex/minimizers.v
• rel_open_convex_line convex/self_concordant.v
• rel_open_convex_pd_slice convex/logdet_barrier.v
• rel_open_convex_pd_slice2 convex/logdet_barrier.v
• rel_open_convex_segment convex/self_concordant.v
• rel_open_dense_seq probability/measurable_minimizer.v
• rename_asg RandomSAT/Forcing.v
• rename_asg_bij RandomSAT/Forcing.v
• rename_clause RandomSAT/Forcing.v
• rename_clause_bij RandomSAT/Forcing.v
• rename_ffun RandomSAT/Forcing.v
• rename_tuple RandomSAT/Forcing.v
• rename_tuple_bij RandomSAT/Forcing.v
• rep_diff RandomSAT/Forcing.v
• rep_diff_mono RandomSAT/Forcing.v
• rep_diff_sum_le RandomSAT/Forcing.v
• replacement_numeric RandomSAT/Replacement.v
• resample_sqr_le probability/efron_stein.v
• resample_sqr_sqr_le probability/efron_stein.v
• resid4_le convex/feature_moments.v
• restr random_matrix/restricted_isometry.v
• restr_supp random_matrix/restricted_isometry.v
• restrE random_matrix/restricted_isometry.v
• restrict RandomSAT/Model.v
• restrict_add_clause RandomSAT/Forcing.v
• restrict_mono RandomSAT/Model.v
• restrict_sub RandomSAT/Model.v
• restrictE RandomSAT/Model.v
• restricted_isometry random_matrix/restricted_isometry.v
• ridge_comparison convex/ridge_comparison.v
• Rintegral_bounded probability/lindeberg.v
• Rintegral_cf_re_gauss_weight fourier/gauss_factor.v
• Rintegral_cos2 probability/semicircle_law.v
• Rintegral_cos_sin fourier/charfun.v
• Rintegral_cov_le random_matrix/goe.v
• Rintegral_cst_prob convex/feature_moments.v
• Rintegral_EFin convex/feature_moments.v
• Rintegral_empirical probability/variational.v
• Rintegral_empirical_fun probability/variational.v
• Rintegral_empirical_ge0 probability/variational.v
• Rintegral_even fourier/esseen.v
• Rintegral_FTC fourier/esseen.v
• Rintegral_FTC_R probability/semicircle_law.v
• Rintegral_fubini fourier/esseen.v
• Rintegral_gauss_cons probability/rademacher_lindeberg.v
• Rintegral_gauss_weight fourier/gauss_factor.v
• Rintegral_id_sym probability/variational.v
• Rintegral_normal01 fourier/gauss_factor.v
• Rintegral_normal_abs3 probability/rademacher_lindeberg.v
• Rintegral_normal_ge comparison/ornstein_uhlenbeck.v
• Rintegral_normal_quadratic probability/rademacher_lindeberg.v
• Rintegral_polyfun_sum random_matrix/goe.v
• Rintegral_polyfunD random_matrix/goe.v
• Rintegral_polyfunZ random_matrix/goe.v
• Rintegral_prob_cst probability/variational.v
• Rintegral_prod_bounded fourier/charfun.v
• Rintegral_semicircle probability/semicircle_law.v
• Rintegral_sqr_le probability/variational.v
• Rintegral_sqr_le random_matrix/goe.v
• Rintegral_sqrt_disk probability/semicircle_law.v
• Rintegral_sum gaussian/gauss_interpolation.v
• Rintegral_sumr convex/feature_moments.v
• Rintegral_swap_bounded fourier/charfun_rV.v
• Rintegral_sym probability/variational.v
• Rintegral_tuple_map probability/tuple_rows.v
• Rintegral_tuple_prod0 probability/lindeberg.v
• Rintegral_tuple_prod_tnth convex/barrier_lindeberg.v
• Rintegral_tuple_prodS probability/lindeberg.v
• Rintegral_tuple_prodS' probability/lindeberg.v
• Rintegral_var_le random_matrix/goe.v
• RintegralN fourier/charfun.v
• rip_const random_matrix/restricted_isometry.v
• rip_const_ge0 random_matrix/restricted_isometry.v
• rip_const_le random_matrix/restricted_isometry.v
• rip_good random_matrix/restricted_isometry.v
• rip_T random_matrix/restricted_isometry.v
• rmax comparison/slepian.v
• rmax_addr comparison/escape.v
• rmax_aux comparison/escape.v
• rmax_eq comparison/slepian.v
• rmax_fam_width comparison/escape.v
• rmax_le comparison/slepian.v
• rmax_le_lse comparison/slepian.v
• rmax_leD comparison/gordon.v
• rmax_lipschitz comparison/slepian.v
• rmax_net_ge comparison/escape.v
• rmax_net_width comparison/escape.v
• rmax_norm comparison/slepian.v
• rmax_vec_add comparison/escape.v
• rmaxZ comparison/sudakov.v
• root_err RandomSAT/Variance.v
• root_ge1 RandomSAT/Variance.v
• root_gt0 RandomSAT/Variance.v
• root_pow RandomSAT/Variance.v
• root_small RandomSAT/Variance.v
• root_sqr RandomSAT/Variance.v
• row_index probability/tuple_rows.v
• row_index_subproof probability/tuple_rows.v
• row_tail comparison/gauss_linear.v
• rowboxE gaussian/measurable_matrix.v
• rowperp matrix/tensor_packing.v
• rowperpK matrix/tensor_packing.v
• rowperpT matrix/tensor_packing.v
• rowproj matrix/tensor_packing.v
• rowproj_perp matrix/tensor_packing.v
• rowprojK matrix/tensor_packing.v
• rowprojT matrix/tensor_packing.v
• rV_cons gaussian/gauss.v
• rV_cons0 gaussian/gauss.v
• rV_cons_lin comparison/gauss_rotation.v
• rV_cons_lincomb comparison/gauss_rotation.v
• rV_cons_line probability/rademacher_lindeberg.v
• rV_cons_line0 probability/rademacher_lindeberg.v
• rV_cons_norm_exprn_le gaussian/gauss_ibp.v
• rV_cons_row_tail comparison/gauss_shift.v
• rV_consD gaussian/gauss_ibp.v
• rV_consD2 comparison/gauss_shift.v
• rV_consS gaussian/gauss.v
• rV_prefix gaussian/partial_derivative.v
• rV_prefix0 gaussian/partial_derivative.v
• rV_prefix_norm gaussian/partial_derivative.v
• rV_prefixn gaussian/partial_derivative.v
• rV_prefixS gaussian/partial_derivative.v

S361

• sat_cabsent RandomSAT/Forcing.v
• sat_cap SatVarianceDefinitions.v
• sat_capped_var SatVarianceDefinitions.v
• sat_capped_varE RandomSAT/Variance.v
• sat_cpresent RandomSAT/Forcing.v
• sat_del_ok RandomSAT/Forcing.v
• sat_mean SatVarianceDefinitions.v
• sat_prefix_len SatVarianceDefinitions.v
• sat_prefix_lenE RandomSAT/Model.v
• sat_rename RandomSAT/Forcing.v
• sat_var SatVarianceDefinitions.v
• sat_variance_bound RandomSAT/Variance.v
• sat_variance_bound_explicit RandomSAT/Variance.v
• sat_variance_statement SatVarianceStatement.v
• sat_variance_theorem SatVarianceTheorem.v
• sball random_matrix/restricted_isometry.v
• Sbar_sqr_le convex/barrier_lindeberg.v
• sc_barrier convex/self_concordant.v
• sc_barrier_contraction convex/self_concordant.v
• sc_barrier_grad_le convex/self_concordant.v
• sc_bregman_ge convex/self_concordant.v
• sc_bregman_le convex/self_concordant.v
• sc_bregman_small convex/self_concordant.v
• sc_dikin convex/self_concordant.v
• sc_function convex/self_concordant.v
• sc_function_continuous convex/self_concordant.v
• sc_function_convex convex/self_concordant.v
• sc_hessian_line_ge convex/self_concordant.v
• sc_hessian_line_le convex/self_concordant.v
• sc_line_derive convex/self_concordant.v
• sc_line_taylor_le convex/self_concordant.v
• sc_minimizer convex/minimizers.v
• sc_norm convex/self_concordant.v
• sc_ode_ge convex/self_concordant.v
• sc_ode_inv convex/self_concordant.v
• sc_ode_le convex/self_concordant.v
• sc_omega convex/self_concordant.v
• sc_omega0 convex/self_concordant.v
• sc_omega_ge convex/self_concordant.v
• sc_omega_ge0 convex/self_concordant.v
• sc_omega_gt_half convex/self_concordant.v
• sc_omega_le convex/self_concordant.v
• sc_omega_star convex/self_concordant.v
• sc_omega_star0 convex/self_concordant.v
• sc_omega_star_taylor convex/self_concordant.v
• sc_omega_taylor convex/self_concordant.v
• sc_sublevel_closed convex/minimizers.v
• sc_taylor3 convex/self_concordant.v
• scale_ineq SKGap/TwoSpin.v
• scaled_bounds SKGap/Poincare.v
• second RandomSAT/Pivotal.v
• second0 RandomSAT/Pivotal.v
• second_ge0 RandomSAT/Pivotal.v
• second_le_occ RandomSAT/Pivotal.v
• secondS RandomSAT/Pivotal.v
• sections_charge_countable probability/atoms.v
• segner random_matrix/wigner.v
• select_rows matrix/tensor_packing.v
• select_rows_orth matrix/tensor_packing.v
• select_rows_proj matrix/tensor_packing.v
• semicircle_catalan random_matrix/wigner.v
• semicircle_clip random_matrix/wigner.v
• semicircle_integrable_eq probability/semicircle_law.v
• semicircle_integral_eq probability/semicircle_law.v
• semicircle_moment0 probability/semicircle_law.v
• semicircle_moment1 probability/semicircle_law.v
• semicircle_moment2 probability/semicircle_law.v
• semicircle_moment_odd probability/semicircle_law.v
• semicircle_momentS probability/semicircle_law.v
• semicircle_near random_matrix/wigner.v
• semicircle_pdf probability/semicircle_law.v
• semicircle_pdf_ge0 probability/semicircle_law.v
• semicircle_pdf_out probability/semicircle_law.v
• semicircle_pdf_scale probability/semicircle_law.v
• semicircle_pdfE probability/semicircle_law.v
• semicircle_pdfN probability/semicircle_law.v
• semicircle_poly random_matrix/wigner.v
• semicircle_prob probability/semicircle_law.v
• semicircle_prob_dominates probability/semicircle_law.v
• semicircle_prob_gt0 probability/semicircle_law.v
• semicircle_prob_sym probability/semicircle_law.v
• semicircle_restrict probability/semicircle_law.v
• separated comparison/sudakov.v
• separated_card_sudakov matrix/tensor_packing.v
• separated_net comparison/sudakov.v
• seq_index comparison/escape.v
• series_delta random_matrix/matrix_series.v
• series_lin random_matrix/matrix_series.v
• series_log_bound random_matrix/matrix_series.v
• series_opnorm_lipschitz random_matrix/matrix_series.v
• series_sym random_matrix/matrix_series.v
• set_toggle probability/hanson_wright.v
• set_toggleK probability/hanson_wright.v
• setI_closed_lipschitz_pos comparison/gauss_law.v
• setI_closed_mxboxes gaussian/measurable_matrix.v
• setI_closed_tuple_boxes probability/conditioning.v
• sets_le random_matrix/restricted_isometry.v
• short_survival RandomSAT/Forcing.v
• sign_flip probability/symmetrization.v
• sign_flipK probability/symmetrization.v
• sign_lists matrix/nets.v
• sign_neg probability/symmetrization.v
• sign_negK probability/symmetrization.v
• sign_pressure PerceptronSignDefinitions.v
• sign_pressureE Perceptron/Pressure.v
• sign_row probability/rademacher_lindeberg.v
• sign_row_cons probability/rademacher_lindeberg.v
• sinh_le_mul_cosh SKGap/Ising.v
• size_allnet random_matrix/restricted_isometry.v
• size_budget matrix/nets.v
• size_grid_codes matrix/nets.v
• size_net random_matrix/restricted_isometry.v
• size_sign_lists matrix/nets.v
• size_spec_seq matrix/von_neumann.v
• size_vlist random_matrix/restricted_isometry.v
• size_wconf random_matrix/restricted_isometry.v
• size_xconf random_matrix/restricted_isometry.v
• sk_cosh SKGap/Ising.v
• sk_cosh_den SKGap/Ising.v
• sk_cosh_gt0 SKGap/Ising.v
• sk_coupling SKGapDefinitions.v
• sk_coupling_diag SKGap/Poincare.v
• sk_coupling_opnorm_le SKGap/Disorder.v
• sk_coupling_row SKGap/Disorder.v
• sk_coupling_sym SKGap/Poincare.v
• sk_couplingB SKGap/Disorder.v
• sk_couplingE SKGap/Disorder.v
• sk_gap_deterministic SKGap/Poincare.v
• sk_gap_statement SKGapStatement.v
• sk_gap_theorem SKGapTheorem.v
• sk_gap_tol SKGap/Poincare.v
• sk_gap_tol_gt0 SKGap/Poincare.v
• sk_good_disorder SKGap/Disorder.v
• sk_good_disorder_measurable SKGap/Disorder.v
• sk_good_disorder_prob SKGap/Disorder.v
• sk_tanh SKGap/Ising.v
• sk_tanh0 SKGap/Ising.v
• sk_tanh2_mx SKGap/Poincare.v
• sk_tanh_cubic SKGap/Ising.v
• sk_tanh_diag SKGap/Poincare.v
• sk_tanh_ge0 SKGap/Ising.v
• sk_tanh_le SKGap/Ising.v
• sk_tanh_lt1 SKGap/Ising.v
• sk_tanh_mx SKGap/Poincare.v
• sk_tanh_norm_le SKGap/Ising.v
• sk_tanh_sub_le SKGap/Ising.v
• sk_tanhN SKGap/Ising.v
• slepian comparison/slepian.v
• slog_le random_matrix/restricted_isometry.v
• small_ball_event probability/small_ball_method.v
• small_ball_linear probability/small_ball_method.v
• small_ball_method probability/small_ball_method.v
• small_ball_of_cf_bound fourier/small_ball.v
• small_sets_le random_matrix/restricted_isometry.v
• smm comparison/gordon.v
• smm_D comparison/gordon.v
• smm_D2 comparison/gordon.v
• smm_D2_colsum comparison/gordon.v
• smm_D2_rowsum comparison/gordon.v
• smm_D2E comparison/gordon.v
• smm_D_differentiable comparison/gordon.v
• smm_D_ge0 comparison/gordon.v
• smm_D_le1 comparison/gordon.v
• smm_D_sum comparison/gordon.v
• smm_DE comparison/gordon.v
• smm_differentiable comparison/gordon.v
• smm_hessian_sign comparison/gordon.v
• smm_le comparison/gordon.v
• smm_lse comparison/gordon.v
• smm_norm comparison/gordon.v
• softmax comparison/slepian.v
• softmax_differentiable comparison/slepian.v
• softmax_ge0 comparison/slepian.v
• softmax_le1 comparison/slepian.v
• softmax_sum comparison/slepian.v
• sorted_spec_seq matrix/von_neumann.v
• sparse_ball random_matrix/restricted_isometry.v
• sparse_emb random_matrix/restricted_isometry.v
• sparse_emb_dot random_matrix/restricted_isometry.v
• sparse_emb_out random_matrix/restricted_isometry.v
• sparse_emb_proj random_matrix/restricted_isometry.v
• sparse_emb_val random_matrix/restricted_isometry.v
• sparse_embB random_matrix/restricted_isometry.v
• sparse_embE random_matrix/restricted_isometry.v
• sparse_isometry_dev random_matrix/restricted_isometry.v
• sparse_net random_matrix/restricted_isometry.v
• sparse_norm_bound random_matrix/restricted_isometry.v
• sparse_norm_subgaussian random_matrix/restricted_isometry.v
• sparse_proj random_matrix/restricted_isometry.v
• sparse_proj_dot random_matrix/restricted_isometry.v
• spec matrix/von_neumann.v
• spec_conj_diag matrix/psd_part.v
• spec_decomposition matrix/von_neumann.v
• spec_decr matrix/von_neumann.v
• spec_le_opnorm random_matrix/goe.v
• spec_lipschitz matrix/von_neumann.v
• spec_perm matrix/von_neumann.v
• spec_psd_ge0 matrix/psd_part.v
• spec_scale matrix/psd_part.v
• spec_seq matrix/von_neumann.v
• spec_shift_decomposition matrix/psd_part.v
• spec_stat_lipschitz matrix/von_neumann.v
• spectral_eigenvector matrix/real_spectral.v
• spectral_exp matrix/real_spectral.v
• spectral_form matrix/real_spectral.v
• spectral_form_abs matrix/real_spectral.v
• spectral_form_ge matrix/real_spectral.v
• spectral_form_le matrix/real_spectral.v
• spectral_mxdot matrix/real_spectral.v
• spectral_nonneg_proj matrix/psd_splitting.v
• spectral_psd matrix/real_spectral.v
• spectral_rowperp_coord matrix/tensor_packing.v
• spectral_rowperp_form_le matrix/tensor_packing.v
• spectral_trace matrix/real_spectral.v
• sphere_net random_matrix/restricted_isometry.v
• sphere_net_spec random_matrix/restricted_isometry.v
• sphere_netP random_matrix/restricted_isometry.v
• spin SKGapDefinitions.v
• spin_col PerceptronSignDefinitions.v
• spin_flip SKGap/Ising.v
• spin_flipK SKGap/Ising.v
• spin_form_sum SKGap/Poincare.v
• spin_mul SKGap/Ising.v
• spin_norm SKGap/Ising.v
• spin_set SKGapDefinitions.v
• spin_set_id SKGap/Ising.v
• spin_set_other SKGap/Ising.v
• spin_set_same SKGap/Ising.v
• spin_set_val SKGap/Ising.v
• spin_setC SKGap/Ising.v
• spin_setE SKGap/Ising.v
• spin_setK SKGap/Ising.v
• spin_sqr SKGap/Ising.v
• spin_vec SKGapDefinitions.v
• spin_vec_set2 SKGap/Ising.v
• spinF SKGap/TwoSpin.v
• spinT SKGap/TwoSpin.v
• sq_le_pow2 random_matrix/restricted_isometry.v
• sqnorm_dev random_matrix/restricted_isometry.v
• sqnorm_dev_ge0 random_matrix/restricted_isometry.v
• sqnorm_dev_ub random_matrix/restricted_isometry.v
• sqr_convex convex/barrier_removal.v
• sqr_dev_Lfun2 probability/efron_stein.v
• sqr_dev_variance probability/efron_stein.v
• sqr_fine_expectation_le probability/efron_stein.v
• sqr_le1 SKGap/TwoSpin.v
• sqr_le_abs SKGap/Poincare.v
• sqr_le_expR probability/subgaussian.v
• sqr_le_norm SKGap/TwoSpin.v
• sqrt_w_gt0 probability/finite_gap.v
• subexponential probability/subgaussian.v
• subexponential_center probability/subgaussian.v
• subexponential_max_sum matrix/random_opnorm.v
• subexponential_mgf probability/subgaussian.v
• subexponential_mixture probability/mixture.v
• subexponential_mul probability/subgaussian.v
• subexponential_of_mgf probability/hanson_wright.v
• subexponential_sqr probability/subgaussian.v
• subexponential_sum_mgf probability/subgaussian.v
• subexponential_tail probability/subgaussian.v
• subgaussian probability/subgaussian.v
• subgaussian_exprn_le probability/subgaussian.v
• subgaussian_lincomb probability/subgaussian.v
• subgaussian_mgf probability/subgaussian.v
• subgaussian_mgf_pointwise probability/subgaussian.v
• subgaussian_mixture probability/mixture.v
• subgaussian_moment probability/subgaussian.v
• subgaussian_of_mgf probability/subgaussian.v
• subgaussian_opnorm_tail probability/subgaussian_matrix.v
• subgaussian_sum probability/subgaussian.v
• subgaussian_sum_mgf probability/subgaussian.v
• subgaussian_tail probability/subgaussian.v
• subgaussian_unit_ge1 probability/subgaussian_matrix.v
• sudakov_fernique comparison/slepian.v
• sudakov_minoration comparison/sudakov.v
• sudakov_mx_series matrix/tensor_packing.v
• sum_abs_col_le matrix/nets.v
• sum_bin_hockey matrix/nets.v
• sum_cauchy_schwarz matrix/euclidean.v
• sum_combine SKGap/TwoSpin.v
• sum_empirical_fun probability/variational.v
• sum_enum_val probability/finite_gap.v
• sum_ffun_sel random_matrix/restricted_isometry.v
• sum_flip SKGap/Ising.v
• sum_geo_lin random_matrix/restricted_isometry.v
• sum_law fourier/gauss_factor.v
• sum_lawE fourier/gauss_factor.v
• sum_ltn_ord RandomSAT/Model.v
• sum_mxvec_index comparison/gordon.v
• sum_offdiag_recl matrix/psd_splitting.v
• sum_pair2 SKGap/Ising.v
• sum_parity random_matrix/wigner.v
• sum_pow2 random_matrix/restricted_isometry.v
• sum_pred_sqr_le convex/barrier_lindeberg.v
• sum_rademacher_flip probability/symmetrization.v
• sum_rademacher_neg probability/symmetrization.v
• sum_set_indicator probability/hanson_wright.v
• sum_shift_diff_le RandomSAT/Forcing.v
• sum_sign_rowS probability/rademacher_lindeberg.v
• sum_spec matrix/von_neumann.v
• sum_spec_exp matrix/von_neumann.v
• sum_spec_trace matrix/psd_part.v
• sum_weight_le matrix/von_neumann.v
• sup_row_bound comparison/cgmt.v
• sup_row_le comparison/cgmt.v
• sup_row_ub comparison/cgmt.v
• supp random_matrix/restricted_isometry.v
• supp_restr random_matrix/restricted_isometry.v
• supp_scale random_matrix/restricted_isometry.v
• support RandomSAT/Replacement.v
• supported random_matrix/restricted_isometry.v
• supported_card random_matrix/restricted_isometry.v
• supported_restr random_matrix/restricted_isometry.v
• supported_restrE random_matrix/restricted_isometry.v
• supported_sub random_matrix/restricted_isometry.v
• supported_sum random_matrix/restricted_isometry.v
• supportedB random_matrix/restricted_isometry.v
• supportedP random_matrix/restricted_isometry.v
• survival RandomSAT/Pivotal.v
• survival0_set RandomSAT/Pivotal.v
• survival_antitone RandomSAT/Forcing.v
• survival_ge0 RandomSAT/Pivotal.v
• survival_le RandomSAT/Forcing.v
• survival_le1 RandomSAT/Pivotal.v
• survival_le_geom RandomSAT/Pivotal.v
• survival_mono RandomSAT/Pivotal.v
• sym_cf_bound fourier/esseen.v
• sym_cf_bound_expR fourier/esseen.v
• sym_diff fourier/gauss_factor.v
• sym_dilation random_matrix/matrix_series.v
• sym_dilation_series random_matrix/matrix_series.v
• sym_dilation_sqr random_matrix/matrix_series.v
• sym_dilation_sym random_matrix/matrix_series.v
• sym_law fourier/gauss_factor.v
• sym_law_second_moment fourier/gauss_factor.v
• sym_law_second_moment_center fourier/gauss_factor.v
• sym_lawE fourier/gauss_factor.v
• sym_part matrix/random_opnorm.v
• sym_part_form matrix/random_opnorm.v
• sym_part_sym matrix/random_opnorm.v
• sym_second_moment fourier/esseen.v
• sym_second_moment_center fourier/esseen.v
• sym_small_ball fourier/esseen.v
• sym_spectral_diag matrix/real_spectral.v
• sym_spectral_diag_ge matrix/whitening.v
• sym_spectralE matrix/real_spectral.v
• sym_spectralmx matrix/real_spectral.v
• sym_spectralmx_orthogonal matrix/real_spectral.v
• sym_sphere_net comparison/escape.v
• sym_tail fourier/esseen.v
• sym_traceless convex/logdet_barrier.v
• sym_tracelessP convex/logdet_barrier.v
• symmetric_block_of_eigen matrix/real_spectral.v
• symmetric_eigenvector matrix/real_spectral.v
• symmetric_spectral matrix/real_spectral.v
• symmetricmx_conj matrix/real_spectral.v
• symmetricmxP matrix/real_spectral.v
• symmetrization probability/symmetrization.v
• symtr_lin convex/logdet_barrier.v
• symtr_map convex/logdet_barrier.v
• symtr_map_is_linear convex/logdet_barrier.v

T141

• taylor2_le probability/rademacher_lindeberg.v
• taylor_ndecr probability/variational.v
• taylor_nincr probability/variational.v
• tensor_packing matrix/tensor_packing.v
• tensor_packing_cluster matrix/tensor_packing.v
• tensor_packing_count matrix/tensor_packing.v
• tensor_packing_net matrix/tensor_packing.v
• tensor_packing_separated matrix/tensor_packing.v
• tensor_packing_statement TensorPackingStatement.v
• tensor_packing_theorem TensorPackingTheorem.v
• tight_frame_cauchy_schwarz comparison/brascamp_lieb.v
• tight_frame_mxdot comparison/brascamp_lieb.v
• tight_frame_mxdot_sqr comparison/brascamp_lieb.v
• tight_frame_sum comparison/brascamp_lieb.v
• tk random_matrix/restricted_isometry.v
• tk_exp random_matrix/restricted_isometry.v
• tk_gt0 random_matrix/restricted_isometry.v
• tk_sum random_matrix/restricted_isometry.v
• tnth_merge probability/conditioning.v
• tnth_sign_flip probability/symmetrization.v
• tnth_tuple_set convex/barrier_lindeberg.v
• tnth_tuple_set_neq convex/barrier_lindeberg.v
• tr_form2_linearl convex/logdet_barrier.v
• tr_form2_linearr convex/logdet_barrier.v
• tr_form_linear convex/logdet_barrier.v
• tr_set comparison/cgmt.v
• tr_set0 comparison/cone_escape.v
• tr_set_base comparison/cone_escape.v
• tr_set_bounded comparison/cgmt.v
• tr_set_cone comparison/cone_escape.v
• tr_set_neq0 comparison/cgmt.v
• tr_set_norm_ge comparison/cone_escape.v
• tr_set_sub comparison/cone_escape.v
• tr_setE comparison/cgmt.v
• trace_argmax matrix/trace_projection.v
• trace_argmax0 matrix/trace_projection.v
• trace_argmax_cone matrix/trace_projection.v
• trace_argmax_conj matrix/trace_projection.v
• trace_argmax_eq matrix/trace_projection.v
• trace_argmax_ge matrix/trace_projection.v
• trace_argmax_lipschitz matrix/trace_projection.v
• trace_argmax_norm matrix/trace_projection.v
• trace_argmax_unique matrix/trace_projection.v
• trace_argmaxP matrix/trace_projection.v
• trace_compress_gram matrix/tensor_packing.v
• trace_pen_ge matrix/trace_projection.v
• trace_psd_part_shift matrix/psd_part.v
• trace_quad matrix/trace_projection.v
• trace_quad_expand matrix/trace_projection.v
• trace_quad_ge0 matrix/psd_splitting.v
• trace_quad_sub_le matrix/psd_splitting.v
• trace_scale matrix/trace_projection.v
• trace_scale0 matrix/trace_projection.v
• trace_scale_adj matrix/trace_projection.v
• trace_scale_conj matrix/trace_projection.v
• trace_scale_id matrix/trace_projection.v
• trace_scaleB matrix/trace_projection.v
• trace_scaleD matrix/trace_projection.v
• trace_scaleK matrix/trace_projection.v
• trace_scaleN matrix/trace_projection.v
• trace_scaleZ matrix/trace_projection.v
• trace_sqr_le random_matrix/goe_rotation.v
• trmx_exp random_matrix/goe.v
• trmx_orthogonal matrix/euclidean.v
• trunc RandomSAT/Pivotal.v
• trunc_block RandomSAT/Variance.v
• trunc_ge0 RandomSAT/Pivotal.v
• trunc_le_forced RandomSAT/Variance.v
• ts_certificate SKGap/TwoSpin.v
• ts_coef SKGap/TwoSpin.v
• ts_coef_bound SKGap/TwoSpin.v
• ts_coef_remainder SKGap/TwoSpin.v
• ts_lead SKGap/TwoSpin.v
• ts_lead_ge SKGap/TwoSpin.v
• ts_lead_sign SKGap/TwoSpin.v
• ts_monomials SKGap/TwoSpin.v
• ts_rem SKGap/TwoSpin.v
• ts_rem_bound SKGap/TwoSpin.v
• tuple_avg RandomSAT/Pivotal.v
• tuple_avg0 RandomSAT/Pivotal.v
• tuple_avg_add RandomSAT/Forcing.v
• tuple_avgS RandomSAT/Pivotal.v
• tuple_box probability/conditioning.v
• tuple_boxE probability/conditioning.v
• tuple_boxes probability/conditioning.v
• tuple_cons probability/lindeberg.v
• tuple_left probability/symmetrization.v
• tuple_map probability/tuple_rows.v
• tuple_map_cons probability/tuple_rows.v
• tuple_merge probability/conditioning.v
• tuple_merge_dep_disj probability/conditioning.v
• tuple_merge_dep_sub probability/conditioning.v
• tuple_merge_id probability/conditioning.v
• tuple_mx comparison/gauss_matrix_law.v
• tuple_mx random_matrix/restricted_isometry.v
• tuple_mx_blocks random_matrix/restricted_isometry.v
• tuple_mx_dot_tail random_matrix/restricted_isometry.v
• tuple_mx_rip random_matrix/restricted_isometry.v
• tuple_mxE random_matrix/restricted_isometry.v
• tuple_pick probability/conditioning.v
• tuple_prod probability/lindeberg.v
• tuple_prod_ball_mulmx fourier/small_ball.v
• tuple_prod_box probability/conditioning.v
• tuple_prod_chain_le probability/conditioning.v
• tuple_prod_cmixture probability/countable_mixture.v
• tuple_prod_cond_le probability/conditioning.v
• tuple_prod_density probability/density_law.v
• tuple_prod_density_law probability/density_law.v
• tuple_prod_indep_big probability/conditioning.v
• tuple_prod_indepS probability/conditioning.v
• tuple_prod_map probability/tuple_rows.v
• tuple_prod_merge probability/conditioning.v
• tuple_prod_mixture probability/mixture.v
• tuple_prod_pick probability/conditioning.v
• tuple_prod_rows probability/tuple_rows.v
• tuple_prod_tv probability/total_variation.v
• tuple_right probability/symmetrization.v
• tuple_rows probability/tuple_rows.v
• tuple_rows_cat probability/tuple_rows.v
• tuple_set probability/lindeberg.v
• tuple_set_cons0 probability/lindeberg.v
• tuple_set_consS probability/lindeberg.v
• tuple_set_set probability/efron_stein.v
• tuple_submx random_matrix/restricted_isometry.v
• tuple_submx_mul random_matrix/restricted_isometry.v
• tuple_submx_net random_matrix/restricted_isometry.v
• tuple_submx_proj random_matrix/restricted_isometry.v
• tuple_sum fourier/gauss_factor.v
• tv_dist probability/total_variation.v
• tv_dist_eq0 probability/total_variation.v
• tv_dist_ge probability/total_variation.v
• tv_dist_ge0 probability/total_variation.v
• tv_dist_geE probability/total_variation.v
• tv_dist_le probability/total_variation.v
• tv_dist_le1 probability/total_variation.v
• tv_dist_triangle probability/total_variation.v
• tv_distC probability/total_variation.v
• tv_distE probability/total_variation.v
• tv_distxx probability/total_variation.v
• two_div_sqrt random_matrix/goe.v
• two_matrix_split matrix/psd_splitting.v

U98

• uk random_matrix/restricted_isometry.v
• uk_gt0 random_matrix/restricted_isometry.v
• unif_mean probability/finite_mean.v
• unif_mean_bij probability/finite_mean.v
• unif_mean_binom_mean RandomSAT/Forcing.v
• unif_mean_clause_split RandomSAT/Model.v
• unif_mean_comm probability/finite_mean.v
• unif_mean_cst probability/finite_mean.v
• unif_mean_ge probability/finite_mean.v
• unif_mean_ge0 probability/finite_mean.v
• unif_mean_indicator probability/finite_mean.v
• unif_mean_le probability/finite_mean.v
• unif_mean_pair probability/finite_mean.v
• unif_mean_sqr_dev probability/finite_mean.v
• unif_mean_sqr_le probability/finite_mean.v
• unif_mean_sum probability/finite_mean.v
• unif_mean_sum_type probability/finite_mean.v
• unif_mean_sumE probability/finite_mean.v
• unif_mean_tuple0 probability/finite_mean.v
• unif_mean_tuple_cons probability/finite_mean.v
• unif_mean_tuple_prod probability/finite_mean.v
• unif_meanB probability/finite_mean.v
• unif_meanD probability/finite_mean.v
• unif_meanN probability/finite_mean.v
• unif_meanZ probability/finite_mean.v
• unif_meanZr probability/finite_mean.v
• unif_var probability/finite_mean.v
• unif_var_addl probability/finite_mean.v
• unif_var_bij probability/finite_mean.v
• unif_var_ge0 probability/finite_mean.v
• unif_var_le probability/finite_mean.v
• unif_var_pair probability/finite_mean.v
• unif_var_tuple_cons probability/finite_mean.v
• unif_varE probability/finite_mean.v
• unit_ball matrix/nets.v
• unit_ball0 matrix/nets.v
• unit_ball_net matrix/nets.v
• unit_ball_quarter_net matrix/random_opnorm.v
• unit_dir comparison/cgmt.v
• unit_sphere matrix/nets.v
• unit_sphere_ball matrix/nets.v
• unit_sphere_net matrix/nets.v
• unvec comparison/escape.v
• unvecK comparison/escape.v
• upper random_matrix/restricted_isometry.v
• upper_admissible probability/variational.v
• upper_admissible_cst probability/variational.v
• upper_admissible_cutoff probability/variational.v
• upper_cutoff probability/variational.v
• upper_cutoff_cvg probability/variational.v
• upper_cutoff_dual probability/variational.v
• upper_cutoff_growth probability/variational.v
• upper_cutoff_le probability/variational.v
• upper_cutoff_lipschitz probability/variational.v
• upper_cutoff_stability probability/variational.v
• upper_cutoff_unique probability/variational.v
• upper_cutoffE probability/variational.v
• upper_energy probability/variational.v
• upper_energy_continuous probability/variational.v
• upper_energy_decr probability/variational.v
• upper_energy_ge probability/variational.v
• upper_energy_lipschitz probability/variational.v
• upper_energy_lt probability/variational.v
• upper_form_ge0 probability/variational.v
• upper_moment probability/variational.v
• upper_moment1_cutoff_gt0 probability/variational.v
• upper_moment1_ge probability/variational.v
• upper_moment1_gt0 probability/variational.v
• upper_moment1_le probability/variational.v
• upper_moment1_lipschitz probability/variational.v
• upper_moment1_reflect probability/clip_profile.v
• upper_moment1_sym probability/variational.v
• upper_moment2_eq0 probability/variational.v
• upper_moment2_lipschitz probability/variational.v
• upper_moment2_sym probability/variational.v
• upper_moment2_taylor probability/variational.v
• upper_moment_empirical_fun probability/variational.v
• upper_moment_ge0 probability/variational.v
• upper_part_diff probability/variational.v
• upper_part_sqr_diff probability/variational.v
• upper_part_sqr_taylor probability/variational.v
• upper_ratio probability/variational.v
• upper_ratio_cutoff probability/variational.v
• upper_ratio_ge0 probability/variational.v
• upper_ratio_le probability/variational.v
• upper_ratio_nondecr probability/variational.v
• upper_value probability/variational.v
• upper_value_cvg probability/variational.v
• upper_value_dual probability/variational.v
• upper_value_ge0 probability/variational.v
• upper_value_incr probability/variational.v
• upper_value_nondecr probability/variational.v
• upper_value_stability probability/variational.v
• upper_variational probability/variational.v
• upper_variational_attained probability/variational.v
• upper_variational_le probability/variational.v
• upper_variational_sym_le probability/variational.v
• upper_vlist random_matrix/restricted_isometry.v

V14

• variance_arith RandomSAT/Variance.v
• variance_distribution probability/efron_stein.v
• variance_le_sqr_dev probability/efron_stein.v
• variance_mixture probability/mixture.v
• variance_resample probability/efron_stein.v
• varianceT probability/efron_stein.v
• vector_small_ball fourier/small_ball.v
• vector_small_ball_fourier fourier/small_ball.v
• vector_small_ball_moments fourier/small_ball.v
• vector_small_ball_moments_level fourier/small_ball.v
• vector_small_ball_variance fourier/small_ball.v
• vlist random_matrix/restricted_isometry.v
• von_neumann_trace matrix/von_neumann.v
• vspace_orthonormal convex/minimizers.v

W25

• wbasis probability/finite_gap.v
• wconf random_matrix/restricted_isometry.v
• wdot probability/finite_gap.v
• wdot_basis probability/finite_gap.v
• wdot_ising SKGap/Spectral.v
• wdotC probability/finite_gap.v
• weierstrass_lipschitz random_matrix/wigner.v
• wfun probability/finite_gap.v
• wfun_sum probability/finite_gap.v
• wfunK probability/finite_gap.v
• wgap_from_square probability/finite_gap.v
• whitening_exists matrix/whitening.v
• whitening_mx matrix/whitening.v
• whitening_mxP matrix/whitening.v
• wigner random_matrix/wigner.v
• wigner_uniform random_matrix/wigner.v
• wigner_uniform_inf random_matrix/wigner.v
• wop_mx probability/finite_gap.v
• wop_mx_form probability/finite_gap.v
• wop_mx_mul probability/finite_gap.v
• wop_mx_sym probability/finite_gap.v
• wpoincare_from_square probability/finite_gap.v
• wvec probability/finite_gap.v
• wvec_eq0 probability/finite_gap.v
• wvecK probability/finite_gap.v

X1

• xconf random_matrix/restricted_isometry.v

Y1

• young_exprn random_matrix/matrix_series.v