OAI/Probability/Subsphere/Kernels/Precision.lean

GitHub source file

77 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SubsphereCurrent.borelPMF line 17
  2. lemma OAI.SubsphereCurrent.measurable_borelPMF line 22
  3. lemma OAI.SubsphereCurrent.borelPMF_ae_eq line 37
  4. def OAI.SubsphereCurrent.KernelLearner.borelVersion line 54
  5. lemma OAI.SubsphereCurrent.KernelLearner.borelVersion_rules line 61
  6. lemma OAI.SubsphereCurrent.KernelLearner.run_congr line 66
  7. lemma OAI.SubsphereCurrent.KernelLearner.borelVersion_success_ae line 85
  8. def OAI.SubsphereCurrent.finiteCDF line 114
  9. lemma OAI.SubsphereCurrent.finiteCDF_zero line 117
  10. lemma OAI.SubsphereCurrent.finiteCDF_succ line 120
  11. lemma OAI.SubsphereCurrent.finiteCDF_mono line 124
  12. lemma OAI.SubsphereCurrent.finiteCDF_total line 130
  13. lemma OAI.SubsphereCurrent.finiteCDF_interval_unique line 138
  14. lemma OAI.SubsphereCurrent.finiteCDF_interval_exists line 149
  15. def OAI.SubsphereCurrent.finiteSample line 165
  16. lemma OAI.SubsphereCurrent.finiteSample_eq_on_interval line 169
  17. lemma OAI.SubsphereCurrent.finiteSample_eq_iff line 176
  18. lemma OAI.SubsphereCurrent.measurable_finiteCDF line 197
  19. lemma OAI.SubsphereCurrent.measurable_finiteSample line 207
  20. def OAI.SubsphereCurrent.coinLaw line 223
  21. instance OAI.SubsphereCurrent.coinLaw_probability line 225
  22. lemma OAI.SubsphereCurrent.finiteSample_map line 229
  23. lemma OAI.SubsphereCurrent.lintegral_finiteSample line 260
  24. lemma OAI.SubsphereCurrent.pmf_map_equiv_apply line 271
  25. def OAI.SubsphereCurrent.samplePMF line 283
  26. lemma OAI.SubsphereCurrent.measurable_samplePMF line 287
  27. lemma OAI.SubsphereCurrent.lintegral_samplePMF line 295
  28. lemma OAI.SubsphereCurrent.samplePMF_map line 305
  29. lemma OAI.SubsphereCurrent.pmf_toMeasure_bind line 331
  30. lemma OAI.SubsphereCurrent.pmf_lintegral_bind line 340
  31. def OAI.SubsphereCurrent.detChain line 350
  32. def OAI.SubsphereCurrent.lawChain line 354
  33. lemma OAI.SubsphereCurrent.detChain_snoc line 359
  34. lemma OAI.SubsphereCurrent.measurable_detChain line 364
  35. lemma OAI.SubsphereCurrent.detChain_lintegral line 374
  36. lemma OAI.SubsphereCurrent.lawChain_bind_initial line 398
  37. instance OAI.SubsphereCurrent.sumMeasurableSingletonClass line 420
  38. lemma OAI.SubsphereCurrent.measurable_countable_select line 428
  39. lemma OAI.SubsphereRegression.Learner.measurable_run_of_rules line 439
  40. lemma OAI.SubsphereRegression.Learner.measurable_estimate_of_rules line 482
  41. abbrev OAI.SubsphereCurrent.KernelLearner.OutputTape line 502
  42. abbrev OAI.SubsphereCurrent.KernelLearner.Tape line 503
  43. def OAI.SubsphereCurrent.KernelLearner.outputTapeLaw line 505
  44. instance OAI.SubsphereCurrent.KernelLearner.outputTapeLaw_probability line 508
  45. def OAI.SubsphereCurrent.KernelLearner.tapeLaw line 515
  46. instance OAI.SubsphereCurrent.KernelLearner.tapeLaw_probability line 518
  47. def OAI.SubsphereCurrent.KernelLearner.tapeCoin line 521
  48. lemma OAI.SubsphereCurrent.KernelLearner.measurable_tapeCoin line 524
  49. def OAI.SubsphereCurrent.KernelLearner.asTape line 529
  50. lemma OAI.SubsphereCurrent.KernelLearner.asTape_measurable_transition line 535
  51. lemma OAI.SubsphereCurrent.KernelLearner.asTape_admissible line 541
  52. def OAI.SubsphereCurrent.KernelLearner.stepPMF line 556
  53. def OAI.SubsphereCurrent.KernelLearner.stepDet line 564
  54. lemma OAI.SubsphereCurrent.KernelLearner.stepDet_measurable line 573
  55. lemma OAI.SubsphereCurrent.KernelLearner.stepDet_map line 585
  56. lemma OAI.SubsphereCurrent.KernelLearner.run_eq_bind_chain line 600
  57. lemma OAI.SubsphereCurrent.KernelLearner.asTape_run_eq_detChain line 611
  58. def OAI.SubsphereCurrent.KernelLearner.finish line 625
  59. lemma OAI.SubsphereCurrent.KernelLearner.asTape_estimate_eq line 628
  60. lemma OAI.SubsphereCurrent.KernelLearner.lintegral_outputTape_eval line 636
  61. lemma OAI.SubsphereCurrent.KernelLearner.lintegral_asTape_estimate line 643
  62. instance OAI.SubsphereCurrent.sampleLaw_probability line 697
  63. instance OAI.SubsphereCurrent.uniformSphere_probability line 699
  64. def OAI.SubsphereCurrent.swapFirstTwo line 702
  65. lemma OAI.SubsphereCurrent.measurePreserving_swapFirstTwo line 709
  66. instance OAI.SubsphereCurrent.KernelLearner.estimateLaw_probability line 719
  67. lemma OAI.SubsphereCurrent.KernelLearner.conditionalSuccess_le_one line 724
  68. def OAI.SubsphereCurrent.KernelLearner.successTest line 728
  69. lemma OAI.SubsphereCurrent.KernelLearner.measurable_successTest line 731
  70. lemma OAI.SubsphereCurrent.KernelLearner.conditionalSuccess_eq_integral_tape line 741
  71. lemma OAI.SubsphereCurrent.KernelLearner.measurable_tape_test line 750
  72. lemma OAI.SubsphereCurrent.KernelLearner.measurable_conditionalSuccess line 759
  73. lemma OAI.SubsphereCurrent.KernelLearner.uniformSuccess_asTape line 766
  74. lemma OAI.SubsphereCurrent.SeededLearner.uniformSuccess_average_seed line 801
  75. lemma OAI.SubsphereCurrent.SeededLearner.uniformSuccess_of_pointwise line 821
  76. lemma OAI.SubsphereCurrent.SeededLearner.exists_good_seed line 830
  77. theorem OAI.SubsphereCurrent.explicit_precision line 866