OAI/Probability/SKValue/Evolution/GridConvergence.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKValue.OrderParameter.grid_tendsto line 17
  2. lemma OAI.SKValue.OrderParameter.grid_ae_tendsto line 31
  3. lemma OAI.SKValue.OrderParameter.grid_ae_error_bound line 41
  4. def OAI.SKValue.OrderParameter.gridError line 48
  5. lemma OAI.SKValue.OrderParameter.gridError_nonneg line 51
  6. lemma OAI.SKValue.OrderParameter.gridError_tendsto line 54
  7. lemma OAI.SKValue.OrderParameter.grid_shift_error_le line 71
  8. lemma OAI.SKValue.controlIntegral_eq_accum line 98
  9. lemma OAI.SKValue.phi_eq_elapsedValue line 107
  10. lemma OAI.SKValue.SmoothTerminal.profile_elapsedValue line 117
  11. def OAI.SKValue.smoothApprox line 130
  12. lemma OAI.SKValue.smoothApprox_evolution line 133
  13. lemma OAI.SKValue.smoothApprox_even line 139
  14. lemma OAI.SKValue.smoothApprox_value_bound line 143
  15. lemma OAI.SKValue.smoothApprox_tendsto line 172