Gogopex/pfr
healthyIndexed1905theorem-like declarations
Sorries left0%0 markers in 0 declarations
Blueprint27 nodes to go
211 of 238 proved27 ready
| Theorem | Status | Owner | Module | Last run |
|---|---|---|---|---|
| absolutelyContinuous_add_of_indep | Checked | unowned | PFR/Kullback.lean | |
| abs_sub_entropy_le_rdist | Checked | unowned | PFR/ForMathlib/Entropy/Kernel/RuzsaDist.lean | |
| add | Checked | unowned | PFR/ForMathlib/FiniteRange/Defs.lean | |
| add | Checked | unowned | PFR/Mathlib/Probability/IdentDistrib.lean | |
| add' | Checked | unowned | PFR/ForMathlib/FiniteRange/Defs.lean | |
| add_singleton' | Checked | unowned | PFR/Mathlib/Algebra/Group/Action/Pointwise/Set/Basic.lean | |
| ae_eq | Checked | unowned | PFR/Mathlib/Probability/Independence/Basic.lean | |
| ae_eq_condKernel_of_compProd_eq | Checked | unowned | PFR/Mathlib/Probability/Kernel/Disintegration.lean | |
| ae_eq_mk | Checked | unowned | PFR/Mathlib/Probability/Kernel/Disintegration.lean | |
| aefiniteKernelSupport | Checked | unowned | PFR/Mathlib/Probability/Kernel/Disintegration.lean | |
| aefiniteKernelSupport_condDistrib | Checked | unowned | PFR/ForMathlib/Entropy/Kernel/Basic.lean | |
| aefiniteKernelSupport_iff | Checked | unowned | PFR/Mathlib/Probability/Kernel/Disintegration.lean | |
| aefiniteKernelSupport_of_cond | Checked | unowned | PFR/Mathlib/Probability/Kernel/Disintegration.lean | |
| aefiniteKernelSupport_zero | Checked | unowned | PFR/Mathlib/Probability/Kernel/Disintegration.lean | |
| ae_mem | Checked | unowned | PFR/ForMathlib/Uniform.lean | |
| ae_of_ae_compProd | Checked | unowned | PFR/Mathlib/Probability/Kernel/Disintegration.lean | |
| ae_of_compProd_eq_zero | Checked | unowned | PFR/Mathlib/Probability/Kernel/Disintegration.lean | |
| app_ent_PFR | Checked | unowned | PFR/WeakPFR.lean | |
| app_ent_PFR' | Checked | unowned | PFR/WeakPFR.lean | |
| apply_two_last | Checked | unowned | PFR/ForMathlib/FourVariables.lean | |
| approx_hom_pfr | Checked | unowned | PFR/ApproxHomPFR.lean | |
| approx_hom_pfr' | Checked | unowned | PFR/ApproxHomPFR.lean | |
| atom_pf | Checked | unowned | PFR/Tactic/RPowSimp.lean | |
| atom_pf' | Checked | unowned | PFR/Tactic/RPowSimp.lean | |
| atom_pow_pf | Checked | unowned | PFR/Tactic/RPowSimp.lean | |
| atom_pow_pf' | Checked | unowned | PFR/Tactic/RPowSimp.lean | |
| averaged_construct_good | Checked | unowned | PFR/ImprovedPFR.lean | |
| averaged_final | Checked | unowned | PFR/ImprovedPFR.lean | |
| bddAbove_card_inter_add | Checked | unowned | PFR/RhoFunctional.lean | |
| bddBelow_rhoMinusSet | Checked | unowned | PFR/RhoFunctional.lean | |
| better_PFR_conjecture | Checked | unowned | PFR/RhoFunctional.lean | |
| better_PFR_conjecture' | Checked | unowned | PFR/RhoFunctional.lean | |
| better_PFR_conjecture_aux | Checked | unowned | PFR/RhoFunctional.lean | |
| better_PFR_conjecture_aux0 | Checked | unowned | PFR/RhoFunctional.lean | |
| card_congr | Checked | unowned | PFR/WeakPFR.lean | |
| cardinal_le_aleph0_of_finiteDimensional | Checked | unowned | PFR/Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean | |
| card_of_dual | Checked | unowned | PFR/ApproxHomPFR.lean | |
| card_of_dual_constrained | Checked | unowned | PFR/ApproxHomPFR.lean | |
| card_of_slice | Checked | unowned | PFR/ApproxHomPFR.lean | |
| cast_bijective | Checked | unowned | PFR/Mathlib/Data/Fin/Basic.lean | |
| cast_surjective | Checked | unowned | PFR/Mathlib/Data/Fin/Basic.lean | |
| chain_rule | Checked | unowned | PFR/ForMathlib/Entropy/Kernel/Basic.lean | |
| chain_rule | Checked | unowned | PFR/ForMathlib/Entropy/Basic.lean | |
| chain_rule' | Checked | unowned | PFR/ForMathlib/Entropy/Basic.lean | |
| chain_rule' | Checked | unowned | PFR/ForMathlib/Entropy/Kernel/Basic.lean | |
| chain_rule'' | Checked | unowned | PFR/ForMathlib/Entropy/Basic.lean | |
| comap | Checked | unowned | PFR/Mathlib/Probability/Kernel/Disintegration.lean | |
| comap_equiv | Checked | unowned | PFR/Mathlib/Probability/Kernel/Disintegration.lean | |
| comap_equiv | Checked | unowned | PFR/ForMathlib/Entropy/Kernel/Basic.lean | |
| comap_real_apply | Checked | unowned | PFR/Mathlib/MeasureTheory/Measure/Real.lean | |
| comp | Checked | unowned | PFR/ForMathlib/Uniform.lean | |
| comparison_of_ruzsa_distances | Checked | unowned | PFR/ForMathlib/Entropy/RuzsaDist.lean | |
| comp_left | Checked | unowned | PFR/Mathlib/Probability/IdentDistrib.lean | |
| compProd | Checked | unowned | PFR/ForMathlib/Entropy/Kernel/MutualInfo.lean | |
| compProd | Checked | unowned | PFR/Mathlib/Probability/Kernel/Disintegration.lean | |
| compProd | Checked | unowned | PFR/Mathlib/Probability/Kernel/Disintegration.lean | |
| compProd_apply_singleton | Checked | unowned | PFR/Mathlib/Probability/Kernel/Disintegration.lean | |
| compProd_assoc' | Checked | unowned | PFR/ForMathlib/Entropy/Kernel/MutualInfo.lean | |
| compProd_compProd | Checked | unowned | PFR/ForMathlib/Entropy/Kernel/MutualInfo.lean | |
| compProd_compProd' | Checked | unowned | PFR/ForMathlib/Entropy/Kernel/MutualInfo.lean | |
| compProd_compProd'' | Checked | unowned | PFR/ForMathlib/Entropy/Kernel/MutualInfo.lean | |
| compProd_congr_ae | Checked | unowned | PFR/Mathlib/Probability/Kernel/Disintegration.lean | |
| compProd_swapLeft_prodMkLeft | Checked | unowned | PFR/Mathlib/Probability/Kernel/Disintegration.lean | |
| comp_right | Checked | unowned | PFR/Mathlib/Probability/IdentDistrib.lean | |
| comp_right | Checked | unowned | PFR/ForMathlib/ConditionalIndependence.lean | |
| comp_right | Checked | unowned | PFR/Mathlib/Probability/Independence/Basic.lean | |
| conclusion_transfers | Checked | unowned | PFR/WeakPFR.lean | |
| cond | Checked | unowned | PFR/Mathlib/Probability/IdentDistrib.lean | |
| cond | Checked | unowned | PFR/ForMathlib/ConditionalIndependence.lean | |
| cond_c_eq_integral | Checked | unowned | PFR/Endgame.lean | |
| cond_chain_rule | Checked | unowned | PFR/ForMathlib/Entropy/Basic.lean | |
| cond_chain_rule' | Checked | unowned | PFR/ForMathlib/Entropy/Basic.lean | |
| cond_construct_good | Checked | unowned | PFR/Endgame.lean | |
| condDistrib_ae_eq | Checked | unowned | PFR/Mathlib/Probability/Kernel/Disintegration.lean | |
| condDistrib_apply | Checked | unowned | PFR/Mathlib/Probability/Kernel/Disintegration.lean | |
| condDistrib_apply' | Checked | unowned | PFR/Mathlib/Probability/Kernel/Disintegration.lean | |
| condDistrib_const_unit | Checked | unowned | PFR/Mathlib/Probability/Kernel/Disintegration.lean | |
| condDistrib_eq_prod_of_indepFun | Checked | unowned | PFR/Mathlib/Probability/Kernel/Disintegration.lean | |
| condDistrib_fst_ae_eq | Checked | unowned | PFR/Mathlib/Probability/Kernel/Disintegration.lean | |
| condDistrib_fst_of_ne_zero | Checked | unowned | PFR/Mathlib/Probability/Kernel/Disintegration.lean | |
| condDistrib_snd_ae_eq | Checked | unowned | PFR/Mathlib/Probability/Kernel/Disintegration.lean | |
| condDistrib_snd_of_ne_zero | Checked | unowned | PFR/Mathlib/Probability/Kernel/Disintegration.lean | |
| condDistrib_unit_right | Checked | unowned | PFR/Mathlib/Probability/Kernel/Disintegration.lean | |
| condEntropy_add_left | Checked | unowned | PFR/ForMathlib/Entropy/Group.lean | |
| condEntropy_add_right | Checked | unowned | PFR/ForMathlib/Entropy/Group.lean | |
| condEntropy_comm | Checked | unowned | PFR/ForMathlib/Entropy/Basic.lean | |
| condEntropy_comp_ge | Checked | unowned | PFR/ForMathlib/Entropy/Basic.lean | |
| condEntropy_comp_of_injective | Checked | unowned | PFR/ForMathlib/Entropy/Basic.lean | |
| condEntropy_comp_self | Checked | unowned | PFR/ForMathlib/Entropy/Basic.lean | |
| condEntropy_def | Checked | unowned | PFR/ForMathlib/Entropy/Basic.lean | |
| condEntropy_div_left | Checked | unowned | PFR/ForMathlib/Entropy/Group.lean | |
| condEntropy_div_right | Checked | unowned | PFR/ForMathlib/Entropy/Group.lean | |
| condEntropy_eq | Checked | unowned | PFR/ForMathlib/Entropy/Basic.lean | |
| condEntropy_eq_entropy | Checked | unowned | PFR/ForMathlib/Entropy/Basic.lean | |
| condEntropy_eq_kernel_entropy | Checked | unowned | PFR/ForMathlib/Entropy/Basic.lean | |
| condEntropy_eq_sum | Checked | unowned | PFR/ForMathlib/Entropy/Basic.lean | |
| condEntropy_eq_sum_fintype | Checked | unowned | PFR/ForMathlib/Entropy/Basic.lean | |
| condEntropy_eq_sum_prod | Checked | unowned | PFR/ForMathlib/Entropy/Basic.lean | |
| condEntropy_eq_sum_sum | Checked | unowned | PFR/ForMathlib/Entropy/Basic.lean | |
| condEntropy_eq_sum_sum_fintype | Checked | unowned | PFR/ForMathlib/Entropy/Basic.lean | |
| condEntropy_eq_zero | Checked | unowned | PFR/ForMathlib/Entropy/Basic.lean | |
| cond_entropy_indep | Checked | unowned | PFR/MoreRuzsaDist.lean | |
| condEntropy_le_entropy | Checked | unowned | PFR/ForMathlib/Entropy/Basic.lean | |
| condEntropy_le_log_card | Checked | unowned | PFR/ForMathlib/Entropy/Basic.lean | |
| condEntropy_mul_left | Checked | unowned | PFR/ForMathlib/Entropy/Group.lean | |
| condEntropy_mul_right | Checked | unowned | PFR/ForMathlib/Entropy/Group.lean | |
| condEntropy_nonneg | Checked | unowned | PFR/ForMathlib/Entropy/Basic.lean | |
| condEntropy_of_injective | Checked | unowned | PFR/ForMathlib/Entropy/Basic.lean | |
| condEntropy_of_injective' | Checked | unowned | PFR/ForMathlib/Entropy/Basic.lean | |
| condEntropy_prod_eq_of_indepFun | Checked | unowned | PFR/ForMathlib/Entropy/Basic.lean | |
| condEntropy_prod_eq_sum | Checked | unowned | PFR/ForMathlib/Entropy/Basic.lean | |
| condEntropy_sub_left | Checked | unowned | PFR/ForMathlib/Entropy/Group.lean | |
| condEntropy_sub_right | Checked | unowned | PFR/ForMathlib/Entropy/Group.lean | |
| condEntropy_two_eq_kernel_entropy | Checked | unowned | PFR/ForMathlib/Entropy/Basic.lean | |
| condEntropy_zero_measure | Checked | unowned | PFR/ForMathlib/Entropy/Basic.lean | |
| condIndep_copies | Checked | unowned | PFR/ForMathlib/ConditionalIndependence.lean | |
| condIndep_copies' | Checked | unowned | PFR/ForMathlib/ConditionalIndependence.lean | |
| condIndepFun_iff | Checked | unowned | PFR/ForMathlib/ConditionalIndependence.lean | |
| cond_isProbabilityMeasure_of_real | Checked | unowned | PFR/Mathlib/Probability/ConditionalProbability.lean | |
| condKernel_apply | Checked | unowned | PFR/Mathlib/Probability/Kernel/Disintegration.lean | |
| condKernel_apply' | Checked | unowned | PFR/Mathlib/Probability/Kernel/Disintegration.lean | |
| condKernel_compProd_ae_eq | Checked | unowned | PFR/Mathlib/Probability/Kernel/Disintegration.lean | |
| condKernel_compProd_apply | Checked | unowned | PFR/Mathlib/Probability/Kernel/Disintegration.lean | |
| condKernel_compProd_apply' | Checked | unowned | PFR/Mathlib/Probability/Kernel/Disintegration.lean | |
| condKernel_condDistrib_ae_eq | Checked | unowned | PFR/Mathlib/Probability/Kernel/Disintegration.lean | |
| condKernel_map_prodMk_left | Checked | unowned | PFR/Mathlib/Probability/Kernel/Disintegration.lean | |
| condKernel_prod_ae_eq | Checked | unowned | PFR/Mathlib/Probability/Kernel/Disintegration.lean | |
| condKLDiv_eq | Checked | unowned | PFR/Kullback.lean | |
| condKLDiv_nonneg | Checked | unowned | PFR/Kullback.lean | |
| cond_left | Checked | unowned | PFR/ForMathlib/ConditionalIndependence.lean | |
| cond_multiDist_chainRule | Checked | unowned | PFR/MoreRuzsaDist.lean | |
| condMultiDist_eq | Checked | unowned | PFR/MoreRuzsaDist.lean | |
| condMultiDist_eq' | Checked | unowned | PFR/MoreRuzsaDist.lean | |
| condMultiDist_nonneg | Checked | unowned | PFR/MoreRuzsaDist.lean | |
| condMultiDist_of_cast | Checked | unowned | PFR/BoundingMutual.lean | |
| condMultiDist_of_const | Checked | unowned | PFR/MoreRuzsaDist.lean | |
| condMultiDist_of_hom | Checked | unowned | PFR/MoreRuzsaDist.lean | |
| condMultiDist_of_inj | Checked | unowned | PFR/MoreRuzsaDist.lean | |
| condMutual_comp_comp_le | Checked | unowned | PFR/ForMathlib/Entropy/Basic.lean | |
| condMutualInfo_comm | Checked | unowned | PFR/ForMathlib/Entropy/Basic.lean | |
| condMutualInfo_def | Checked | unowned | PFR/ForMathlib/Entropy/Basic.lean | |
| condMutualInfo_eq | Checked | unowned | PFR/ForMathlib/Entropy/Basic.lean | |
| condMutualInfo_eq' | Checked | unowned | PFR/ForMathlib/Entropy/Basic.lean | |
| condMutualInfo_eq_integral_mutualInfo | Checked | unowned | PFR/ForMathlib/Entropy/Basic.lean | |
| condMutualInfo_eq_kernel_mutualInfo | Checked | unowned | PFR/ForMathlib/Entropy/Basic.lean | |
| condMutualInfo_eq_sum | Checked | unowned | PFR/ForMathlib/Entropy/Basic.lean | |
| condMutualInfo_eq_sum' | Checked | unowned | PFR/ForMathlib/Entropy/Basic.lean | |
| condMutualInfo_eq_zero | Checked | unowned | PFR/ForMathlib/Entropy/Basic.lean | |
| condMutualInfo_nonneg | Checked | unowned | PFR/ForMathlib/Entropy/Basic.lean | |
| condMutualInfo_of_inj | Checked | unowned | PFR/ForMathlib/Entropy/Basic.lean | |
| condMutualInfo_of_inj' | Checked | unowned | PFR/ForMathlib/Entropy/Basic.lean | |
| condMutualInfo_of_inj_map | Checked | unowned | PFR/ForMathlib/Entropy/Basic.lean | |
| condMutualInfo_zero_measure | Checked | unowned | PFR/ForMathlib/Entropy/Basic.lean | |
| cond_real_apply | Checked | unowned | PFR/Mathlib/Probability/ConditionalProbability.lean | |
| condRho_eq | Checked | unowned | PFR/RhoFunctional.lean | |
| condRho_eq_of_identDistrib | Checked | unowned | PFR/RhoFunctional.lean | |
| condRho_le | Checked | unowned | PFR/RhoFunctional.lean | |
| condRho_le_condRuzsaDist_of_phiMinimizes | Checked | unowned | PFR/RhoFunctional.lean | |
| condRhoMinus_le | Checked | unowned | PFR/RhoFunctional.lean | |
| condRho_of_injective | Checked | unowned | PFR/RhoFunctional.lean | |
| condRho_of_sum_le | Checked | unowned | PFR/RhoFunctional.lean | |
| condRho_of_translate | Checked | unowned | PFR/RhoFunctional.lean | |
| condRhoPlus_le | Checked | unowned | PFR/RhoFunctional.lean | |
| condRho_prod_eq_of_indepFun | Checked | unowned | PFR/RhoFunctional.lean | |
| condRho_prod_eq_sum | Checked | unowned | PFR/RhoFunctional.lean | |
| condRho_prod_le | Checked | unowned | PFR/RhoFunctional.lean | |
| condRho_sum_le | Checked | unowned | PFR/RhoFunctional.lean | |
| condRho_sum_le' | Checked | unowned | PFR/RhoFunctional.lean | |
| cond_right | Checked | unowned | PFR/ForMathlib/ConditionalIndependence.lean | |
| condRuszaDist_prod_eq_of_indepFun | Checked | unowned | PFR/ForMathlib/Entropy/RuzsaDist.lean | |
| condRuszaDist_zero_left | Checked | unowned | PFR/ForMathlib/Entropy/RuzsaDist.lean | |
| condRuszaDist_zero_right | Checked | unowned | PFR/ForMathlib/Entropy/RuzsaDist.lean | |
| condRuzsaDistance_ge_of_min | Checked | unowned | PFR/TauFunctional.lean | |
| condRuzsaDist_comp_right | Checked | unowned | PFR/ForMathlib/Entropy/RuzsaDist.lean | |
| condRuzsaDist'_def | Checked | unowned | PFR/ForMathlib/Entropy/RuzsaDist.lean | |
| condRuzsaDist_def | Checked | unowned | PFR/ForMathlib/Entropy/RuzsaDist.lean | |
| condRuzsaDist_diff_le | Checked | unowned | PFR/ForMathlib/Entropy/RuzsaDist.lean | |
| condRuzsaDist_diff_le' | Checked | unowned | PFR/ForMathlib/Entropy/RuzsaDist.lean | |
| condRuzsaDist_diff_le'' | Checked | unowned | PFR/ForMathlib/Entropy/RuzsaDist.lean | |
| condRuzsaDist_diff_le''' | Checked | unowned | PFR/ForMathlib/Entropy/RuzsaDist.lean | |
| condRuzsaDist_diff_ofsum_le | Checked | unowned | PFR/ForMathlib/Entropy/RuzsaDist.lean | |
| condRuzsaDist'_eq_integral | Checked | unowned | PFR/ForMathlib/Entropy/RuzsaDist.lean | |
| condRuzsaDist'_eq_sum | Checked | unowned | PFR/ForMathlib/Entropy/RuzsaDist.lean | |
| condRuzsaDist'_eq_sum' | Checked | unowned | PFR/ForMathlib/Entropy/RuzsaDist.lean | |
| condRuzsaDist_eq_sum | Checked | unowned | PFR/ForMathlib/Entropy/RuzsaDist.lean | |
| condRuzsaDist_eq_sum' | Checked | unowned | PFR/ForMathlib/Entropy/RuzsaDist.lean | |
| condRuzsaDist_le | Checked | unowned | PFR/ForMathlib/Entropy/RuzsaDist.lean | |
| condRuzsaDist_le' | Checked | unowned | PFR/ForMathlib/Entropy/RuzsaDist.lean | |
| condRuzsaDist_le'_prod | Checked | unowned | PFR/ForMathlib/Entropy/RuzsaDist.lean | |
| condRuzsaDist_nonneg | Checked | unowned | PFR/ForMathlib/Entropy/RuzsaDist.lean | |
| condRuzsaDist_of_const | Checked | unowned | PFR/ForMathlib/Entropy/RuzsaDist.lean | |
| condRuzsaDist'_of_copy | Checked | unowned | PFR/ForMathlib/Entropy/RuzsaDist.lean | |
| condRuzsaDist_of_copy | Checked | unowned | PFR/ForMathlib/Entropy/RuzsaDist.lean | |
| condRuzsaDist'_of_indep | Checked | unowned | PFR/ForMathlib/Entropy/RuzsaDist.lean | |
| condRuzsaDist_of_indep | Checked | unowned | PFR/ForMathlib/Entropy/RuzsaDist.lean | |
| condRuzsaDist'_of_inj_map | Checked | unowned | PFR/ForMathlib/Entropy/RuzsaDist.lean | |
| condRuzsaDist'_of_inj_map' | Checked | unowned | PFR/ForMathlib/Entropy/RuzsaDist.lean | |
| condRuzsaDist_of_inj_map | Checked | unowned | PFR/ForMathlib/Entropy/RuzsaDist.lean | |
| condRuzsaDist_of_sums_ge | Checked | unowned | PFR/FirstEstimate.lean | |
| condRuzsaDist'_prod_eq_sum | Checked | unowned | PFR/ForMathlib/Entropy/RuzsaDist.lean |
No theorems match the active view.
Showing the highest-priority 200 proofs for fast server render.