OAI/Probability/SKSupport/Control/VariableGrid.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ZeroTemperatureSK.Nonuniform.time line 16
  2. lemma OAI.ZeroTemperatureSK.Nonuniform.time_zero line 18
  3. lemma OAI.ZeroTemperatureSK.Nonuniform.time_succ line 19
  4. lemma OAI.ZeroTemperatureSK.Nonuniform.time_mono line 21
  5. lemma OAI.ZeroTemperatureSK.Nonuniform.coe_time_succ line 27
  6. def OAI.ZeroTemperatureSK.Nonuniform.controlled line 30
  7. lemma OAI.ZeroTemperatureSK.Nonuniform.controlled_adapted line 35
  8. lemma OAI.ZeroTemperatureSK.Nonuniform.controlled_integrable line 52
  9. lemma OAI.ZeroTemperatureSK.Nonuniform.controlled_formula line 67
  10. def OAI.ZeroTemperatureSK.Nonuniform.elementary line 74
  11. lemma OAI.ZeroTemperatureSK.Nonuniform.elementary_bound line 79
  12. lemma OAI.ZeroTemperatureSK.Nonuniform.elementary_progressive line 85
  13. lemma OAI.ZeroTemperatureSK.Nonuniform.elementary_on_step line 109
  14. lemma OAI.ZeroTemperatureSK.Nonuniform.elementary_integral_on_step line 123
  15. structure OAI.ZeroTemperatureSK.Nonuniform.GridData line 146
  16. def OAI.ZeroTemperatureSK.Nonuniform.profit line 169
  17. lemma OAI.ZeroTemperatureSK.Nonuniform.telescope_bound line 173
  18. lemma OAI.ZeroTemperatureSK.Nonuniform.GridData.mesh_upper line 184
  19. def OAI.ZeroTemperatureSK.Nonuniform.euler line 226
  20. lemma OAI.ZeroTemperatureSK.Nonuniform.euler_adapted line 231
  21. lemma OAI.ZeroTemperatureSK.Nonuniform.euler_controlled line 246
  22. lemma OAI.ZeroTemperatureSK.Nonuniform.GridData.mesh_lower line 261
  23. def OAI.ZeroTemperatureSK.Nonuniform.refineLengths line 330
  24. lemma OAI.ZeroTemperatureSK.Nonuniform.refine_time_block line 332
  25. lemma OAI.ZeroTemperatureSK.Nonuniform.refine_time_inside line 349
  26. lemma OAI.ZeroTemperatureSK.Nonuniform.refine_cell_subset line 359
  27. lemma OAI.ZeroTemperatureSK.Nonuniform.grid_drift_refinement line 373
  28. lemma OAI.ZeroTemperatureSK.Nonuniform.grid_cost_refinement line 395
  29. lemma OAI.ZeroTemperatureSK.Nonuniform.controlled_refinement line 416
  30. lemma OAI.ZeroTemperatureSK.Nonuniform.profit_refinement line 426
  31. def OAI.ZeroTemperatureSK.Nonuniform.GridData.refine line 446
  32. lemma OAI.ZeroTemperatureSK.Nonuniform.sum_error_refinement line 470
  33. lemma OAI.ZeroTemperatureSK.Nonuniform.refined_error_limit line 484
  34. def OAI.ZeroTemperatureSK.Nonuniform.objectives line 490
  35. lemma OAI.ZeroTemperatureSK.Nonuniform.objectives_nonempty line 496
  36. lemma OAI.ZeroTemperatureSK.Nonuniform.GridData.control_upper line 500
  37. lemma OAI.ZeroTemperatureSK.Nonuniform.GridData.control_lower line 523
  38. def OAI.ZeroTemperatureSK.Nonuniform.cascadeV line 543
  39. lemma OAI.ZeroTemperatureSK.Nonuniform.cascadeV_lipschitz line 547
  40. lemma OAI.ZeroTemperatureSK.Nonuniform.cascadeV_regular line 553
  41. def OAI.ZeroTemperatureSK.Nonuniform.cascadeVAt line 561
  42. def OAI.ZeroTemperatureSK.Nonuniform.cellVHeat line 564
  43. def OAI.ZeroTemperatureSK.Nonuniform.cellVRate line 567
  44. lemma OAI.ZeroTemperatureSK.Nonuniform.cellVHeat_verificationData line 570
  45. lemma OAI.ZeroTemperatureSK.Nonuniform.cellVHeat_left line 576
  46. lemma OAI.ZeroTemperatureSK.Nonuniform.cellVHeat_right line 594
  47. lemma OAI.ZeroTemperatureSK.Nonuniform.cellVHeat_seam line 601
  48. def OAI.ZeroTemperatureSK.Nonuniform.cellVHeat_gridData line 606
  49. theorem OAI.ZeroTemperatureSK.Nonuniform.cascadeV_eq_control_sup line 642