OAI/NumberTheory/GaussianMoat/ConditionalSampling.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.GaussianMoat.FinLaw.cHf_eq_of_fibers line 14
  2. theorem OAI.GaussianMoat.FinLaw.cHf_le_of_determined line 27
  3. theorem OAI.GaussianMoat.FinLaw.cHf_finset_subadd line 37
  4. theorem OAI.GaussianMoat.FinLaw.cHf_fintype_subadd line 73
  5. theorem OAI.GaussianMoat.FinLaw.prefixVar_swap line 86
  6. theorem OAI.GaussianMoat.FinLaw.ordered_remaining_exchange_cond line 97
  7. theorem OAI.GaussianMoat.FinLaw.prefix_conditional_block line 110
  8. theorem OAI.GaussianMoat.FinLaw.ordered_prefix_conditional_bound line 133
  9. theorem OAI.GaussianMoat.FinLaw.ordered_enrichment_accounting line 152
  10. lemma OAI.GaussianMoat.perm_expect_exchange line 234
  11. theorem OAI.GaussianMoat.perm_covariance_nonpos line 242
  12. theorem OAI.GaussianMoat.perm_sample_second_moment line 282
  13. theorem OAI.GaussianMoat.expect_lower_tail_le line 304
  14. theorem OAI.GaussianMoat.perm_sample_interval_tail line 318
  15. def OAI.GaussianMoat.FinLaw.uniform line 349
  16. theorem OAI.GaussianMoat.FinLaw.uniform_mass line 356
  17. theorem OAI.GaussianMoat.FinLaw.uniform_Hf_injective line 359
  18. theorem OAI.GaussianMoat.FinLaw.Hf_le_log_card_type line 369
  19. theorem OAI.GaussianMoat.FinLaw.Hf_le_log_card_set line 374
  20. theorem OAI.GaussianMoat.FinLaw.map_mix line 385
  21. theorem OAI.GaussianMoat.FinLaw.Hf_mix_ge line 396
  22. theorem OAI.GaussianMoat.FinLaw.Hf_prefix_le line 411
  23. theorem OAI.GaussianMoat.FinLaw.Hf_fintype_subadd line 416
  24. theorem OAI.GaussianMoat.FinLaw.Hf_prefix_le_sum line 431
  25. theorem OAI.GaussianMoat.FinLaw.fresh_entropy_from_prefix line 453