OAI/Probability/SKRatio/Entropy/LogPartition.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKRatio.Planted.standardSample line 16
  2. lemma OAI.SKRatio.Planted.standardSample_continuous line 19
  3. lemma OAI.SKRatio.Planted.standardSample_preserving line 24
  4. lemma OAI.SKRatio.Planted.hamiltonian_difference_le line 41
  5. lemma OAI.SKRatio.Planted.log_partition_difference_le line 53
  6. lemma OAI.SKRatio.Planted.edge_card_bound line 73
  7. lemma OAI.SKRatio.Planted.standard_lipschitz_bound line 78
  8. lemma OAI.SKRatio.Planted.log_partition_standard_lipschitz line 96
  9. lemma OAI.SKRatio.Planted.log_partition_integrable line 117
  10. lemma OAI.SKRatio.Planted.log_partition_centered_L1 line 124
  11. lemma OAI.SKRatio.Planted.log_partition_mean_upper line 150
  12. lemma OAI.SKRatio.Planted.log_partition_mean_lower line 171
  13. lemma OAI.SKRatio.Planted.log_partition_annealed_L1 line 207
  14. lemma OAI.SKRatio.Planted.partition_lower_probability line 231
  15. lemma OAI.SKRatio.Planted.sqrt_nat_add_div_tendsto line 265
  16. lemma OAI.SKRatio.Planted.partition_lower_high_probability line 279