OAI/Probability/GaussianReplacement/ArrayBounds.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentProjection.arrayReference line 13
  2. lemma OAI.CurrentProjection.observationSignalLaw_fst_as_observed line 17
  3. lemma OAI.CurrentProjection.arrayReference_eq line 25
  4. lemma OAI.CurrentProjection.freshArrayLaw_assoc_first line 40
  5. lemma OAI.CurrentProjection.freshArrayLaw_aligned line 48
  6. lemma OAI.CurrentProjection.arrayReference_aligned line 69
  7. lemma OAI.CurrentProjection.arrayReference_prefix_step line 83
  8. def OAI.CurrentProjection.baselineCost line 113
  9. def OAI.CurrentProjection.hybridBaselineConstant line 117
  10. lemma OAI.CurrentProjection.hybridBaselineConstant_pos line 119
  11. lemma OAI.CurrentProjection.baselineCost_finite line 123
  12. lemma OAI.CurrentProjection.arrayReference_finite_bound line 139
  13. lemma OAI.CurrentProjection.arrayReference_exposed_chain line 165
  14. lemma OAI.CurrentProjection.exposedInformation_finite line 175
  15. lemma OAI.CurrentProjection.rowInformation_finite_bound line 185
  16. lemma OAI.CurrentProjection.freshReference_from_array_bound line 199
  17. lemma OAI.CurrentProjection.freshSlope_from_array_bound line 217
  18. lemma OAI.CurrentProjection.arrayReference_actual_step line 240
  19. lemma OAI.CurrentProjection.nextActualRowLaw_signal_row line 252
  20. lemma OAI.CurrentProjection.gaussian_sphere_inner_mixture line 267
  21. lemma OAI.CurrentProjection.nextActualRowLaw_label line 278
  22. lemma OAI.CurrentProjection.hybrid_one_step line 292