OAI/NumberTheory/GaussianMoat/TimeLaw.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.GaussianMoat.TimeLaw line 12
  2. def OAI.GaussianMoat.endpointTime line 16
  3. def OAI.GaussianMoat.TimeLaw.step line 21
  4. lemma OAI.GaussianMoat.SplitSieve.pointEntropy_map line 26
  5. lemma OAI.GaussianMoat.SplitSieve.pointEntropy_joint_fst line 33
  6. lemma OAI.GaussianMoat.shifted_walk_injective line 40
  7. lemma OAI.GaussianMoat.walk_pair_displacement line 43
  8. theorem OAI.GaussianMoat.TimeLaw.step_enrichment line 51
  9. def OAI.GaussianMoat.FinLaw.prob line 104
  10. lemma OAI.GaussianMoat.FinLaw.prob_nonneg line 106
  11. lemma OAI.GaussianMoat.FinLaw.prob_le_one line 109
  12. lemma OAI.GaussianMoat.FinLaw.prob_mono line 113
  13. def OAI.GaussianMoat.FinLaw.iid line 121
  14. lemma OAI.GaussianMoat.FinLaw.iid_mass line 128
  15. lemma OAI.GaussianMoat.FinLaw.iid_product line 131
  16. lemma OAI.GaussianMoat.FinLaw.exp_neg_le_quadratic line 136
  17. lemma OAI.GaussianMoat.FinLaw.prob_le_exp_moment line 152
  18. lemma OAI.GaussianMoat.FinLaw.bernoulli_moment line 167
  19. theorem OAI.GaussianMoat.FinLaw.iid_lower_tail line 176
  20. lemma OAI.GaussianMoat.FinLaw.le_map_apply line 220
  21. def OAI.GaussianMoat.FinLaw.conditionOn line 226
  22. lemma OAI.GaussianMoat.FinLaw.conditionOn_weight line 239
  23. lemma OAI.GaussianMoat.FinLaw.disintegration line 256
  24. lemma OAI.GaussianMoat.FinLaw.conditionOn_mixture line 267
  25. lemma OAI.GaussianMoat.FinLaw.conditionOn_observation line 272
  26. lemma OAI.GaussianMoat.FinLaw.condH_eq_conditionOn line 278
  27. lemma OAI.GaussianMoat.FinLaw.prob_map line 284
  28. lemma OAI.GaussianMoat.FinLaw.prob_joint line 296
  29. lemma OAI.GaussianMoat.FinLaw.conditionOn_prob line 305
  30. lemma OAI.GaussianMoat.FinLaw.prob_le_expect_div line 309
  31. lemma OAI.GaussianMoat.FinLaw.prob_compl line 322
  32. lemma OAI.GaussianMoat.FinLaw.prob_inter_ge line 331
  33. lemma OAI.GaussianMoat.FinLaw.prob_exists_le_sum line 338
  34. lemma OAI.GaussianMoat.FinLaw.map_equiv_mass line 359
  35. lemma OAI.GaussianMoat.FinLaw.entropy_map_equiv line 368
  36. lemma OAI.GaussianMoat.FinLaw.iid_succ line 373
  37. lemma OAI.GaussianMoat.FinLaw.entropy_iid line 381
  38. lemma OAI.GaussianMoat.FinLaw.iid_split line 393
  39. lemma OAI.GaussianMoat.FinLaw.iid_map_eval line 413