OAI/Probability/MemoryPrecision/KernelEvaluation.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MemoryPrecision.Kernel.Policy.measurable_angleTest line 21
  2. lemma OAI.MemoryPrecision.Kernel.Policy.measurable_chordTest line 25
  3. lemma OAI.MemoryPrecision.Kernel.Policy.angleTest_le_one line 28
  4. lemma OAI.MemoryPrecision.Kernel.Policy.chordTest_le_one line 31
  5. lemma OAI.MemoryPrecision.Kernel.Policy.outputTest_measurable line 33
  6. lemma OAI.MemoryPrecision.Kernel.Policy.outputTest_le_one line 36
  7. def OAI.MemoryPrecision.Kernel.Policy.marginal line 40
  8. lemma OAI.MemoryPrecision.Kernel.Policy.marginal_sum line 42
  9. lemma OAI.MemoryPrecision.Kernel.Policy.marginal_measurable line 47
  10. lemma OAI.MemoryPrecision.Kernel.Policy.measurable_eval line 55
  11. lemma OAI.MemoryPrecision.Kernel.Policy.eval_le_one line 72
  12. lemma OAI.MemoryPrecision.Kernel.Policy.pathValue_le_one line 84
  13. def OAI.MemoryPrecision.Kernel.Policy.cont line 91
  14. lemma OAI.MemoryPrecision.Kernel.Policy.measurable_cont line 96
  15. lemma OAI.MemoryPrecision.Kernel.Policy.cont_le_forced_sum line 111