OAI/Probability/CriticalPercolation/Entropy/BinaryConfiguration.lean
10 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.CriticalPercolation.BinaryLaw.scheduleWeight_nonnegline 18 - lemma
OAI.CriticalPercolation.BinaryLaw.scheduleWeight_sumline 23 - theorem
OAI.CriticalPercolation.BinaryLaw.scheduleWeight_exponentialline 32 - lemma
OAI.CriticalPercolation.BinaryLaw.density_seed_le_rawProductline 50 - def
OAI.CriticalPercolation.BinaryLaw.constructionCostline 65 - lemma
OAI.CriticalPercolation.BinaryLaw.exp_constructionCostline 69 - theorem
OAI.CriticalPercolation.BinaryLaw.conditionedMass_density_leline 77 - lemma
OAI.CriticalPercolation.BinaryLaw.sum_configurationline 112 - lemma
OAI.CriticalPercolation.BinaryLaw.scheduleWeight_exponential_boolline 127 - theorem
OAI.CriticalPercolation.BinaryLaw.conditioned_configuration_entropyline 143