OAI/Geometry/IsometricImmersion/Energy/WeightedMultiplier.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Weighted.edgeDistance line 17
  2. def OAI.SmoothLocal.Weighted.weightPhase line 19
  3. def OAI.SmoothLocal.Weighted.directedWeight line 22
  4. def OAI.SmoothLocal.Weighted.directedM line 25
  5. def OAI.SmoothLocal.Weighted.directedN line 28
  6. def OAI.SmoothLocal.Weighted.weightH0 line 31
  7. def OAI.SmoothLocal.Weighted.multiplierT line 33
  8. def OAI.SmoothLocal.Weighted.multiplierS line 36
  9. def OAI.SmoothLocal.Weighted.multiplierJ line 40
  10. theorem OAI.SmoothLocal.Weighted.directedWeight_differentiableAt line 46
  11. theorem OAI.SmoothLocal.Weighted.directedWeight_partial line 55
  12. theorem OAI.SmoothLocal.Weighted.directedWeight_partial_t line 72
  13. theorem OAI.SmoothLocal.Weighted.directedWeight_partial_s line 78
  14. theorem OAI.SmoothLocal.Weighted.directedWeight_partial_s_factored line 85
  15. theorem OAI.SmoothLocal.Weighted.directedWeight_contDiffOn line 94
  16. theorem OAI.SmoothLocal.Weighted.directedWeight_pos line 105
  17. theorem OAI.SmoothLocal.Weighted.directedWeight_edge_zero line 109
  18. theorem OAI.SmoothLocal.Weighted.directedWeight_partial_edge_zero line 113
  19. theorem OAI.SmoothLocal.Weighted.directedM_differentiableAt line 119
  20. theorem OAI.SmoothLocal.Weighted.directedN_differentiableAt line 124
  21. theorem OAI.SmoothLocal.Weighted.directedM_partial line 130
  22. theorem OAI.SmoothLocal.Weighted.directedN_partial line 137
  23. theorem OAI.SmoothLocal.Weighted.directed_mn_edge_zero line 150
  24. theorem OAI.SmoothLocal.Weighted.directed_coefficients line 155
  25. theorem OAI.SmoothLocal.Weighted.directedS_transverse_expansion line 196