OAI/Geometry/WeakMTW/Variations/ActionBranch.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.WeakMTWGlobalSupport.WeakMTW.ActionBranch line 23
  2. theorem OAI.WeakMTWGlobalSupport.WeakMTW.ActionBranch.exists_of_nonconjugate line 32
  3. def OAI.WeakMTWGlobalSupport.WeakMTW.ActionBranch.value line 39
  4. theorem OAI.WeakMTWGlobalSupport.WeakMTW.ActionBranch.smooth_value line 41
  5. theorem OAI.WeakMTWGlobalSupport.WeakMTW.ActionBranch.inverse_state line 44
  6. theorem OAI.WeakMTWGlobalSupport.WeakMTW.ActionBranch.target_state line 49
  7. theorem OAI.WeakMTWGlobalSupport.WeakMTW.ActionBranch.gradient_state line 55
  8. theorem OAI.WeakMTWGlobalSupport.WeakMTW.ActionBranch.value_state line 62
  9. theorem OAI.WeakMTWGlobalSupport.WeakMTW.ActionBranch.gradient_center line 71
  10. theorem OAI.WeakMTWGlobalSupport.WeakMTW.ActionBranch.eq_cost_near line 80
  11. theorem OAI.WeakMTWGlobalSupport.WeakMTW.ActionBranch.hessian_limit line 89