OAI/Probability/SKValue/Gaussian/SplitConvergence.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKValue.gridDelta_le_one line 14
  2. lemma OAI.SKValue.OrderParameter.splitGrid_le line 18
  3. lemma OAI.SKValue.OrderParameter.splitGrid_tendsto line 24
  4. def OAI.SKValue.OrderParameter.splitError line 40
  5. lemma OAI.SKValue.OrderParameter.splitError_nonneg line 42
  6. lemma OAI.SKValue.OrderParameter.splitError_tendsto line 44
  7. lemma OAI.SKValue.OrderParameter.split_shift_error line 73
  8. def OAI.SKValue.profileHeight line 95
  9. lemma OAI.SKValue.profileHeight_nonneg line 98
  10. lemma OAI.SKValue.profileHeight_mem line 102
  11. def OAI.SKValue.splitSmoothParameter line 109
  12. lemma OAI.SKValue.splitSmoothParameter_pos line 111
  13. lemma OAI.SKValue.splitSmoothParameter_ge line 113
  14. def OAI.SKValue.splitSmooth line 115
  15. lemma OAI.SKValue.splitSmooth_evolution line 117
  16. lemma OAI.SKValue.splitSmooth_value_bound line 122
  17. lemma OAI.SKValue.splitSmooth_tendsto line 152
  18. lemma OAI.SKValue.splitSmooth_bulk_jets line 163
  19. lemma OAI.SKValue.splitSmooth_jet_limits line 181