OAI/Analysis/LipschitzEquivalence/SmoothCalculus.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LipschitzCounterexample.CompactWSC.smoothSubmodule line 14
  2. abbrev OAI.LipschitzCounterexample.CompactWSC.Smooth line 25
  3. def OAI.LipschitzCounterexample.CompactWSC.Smooth.eval line 29
  4. theorem OAI.LipschitzCounterexample.CompactWSC.Smooth.contDiff line 34
  5. theorem OAI.LipschitzCounterexample.CompactWSC.Smooth.differentiable line 37
  6. def OAI.LipschitzCounterexample.CompactWSC.Smooth.grad line 40
  7. theorem OAI.LipschitzCounterexample.CompactWSC.Smooth.grad_eq line 51
  8. theorem OAI.LipschitzCounterexample.CompactWSC.Smooth.norm_grad line 53
  9. theorem OAI.LipschitzCounterexample.CompactWSC.Smooth.grad_contDiff line 56
  10. theorem OAI.LipschitzCounterexample.CompactWSC.Smooth.grad_continuous line 60
  11. theorem OAI.LipschitzCounterexample.CompactWSC.Smooth.grad_norm_le line 63
  12. def OAI.LipschitzCounterexample.CompactWSC.Smooth.mul line 68
  13. theorem OAI.LipschitzCounterexample.CompactWSC.Smooth.mul_apply line 71
  14. theorem OAI.LipschitzCounterexample.CompactWSC.Smooth.grad_mul line 73
  15. def OAI.LipschitzCounterexample.CompactWSC.edge line 81
  16. theorem OAI.LipschitzCounterexample.CompactWSC.edge_continuous line 83
  17. theorem OAI.LipschitzCounterexample.CompactWSC.edge_mem line 88
  18. theorem OAI.LipschitzCounterexample.CompactWSC.edge_hasDerivAt line 95
  19. theorem OAI.LipschitzCounterexample.CompactWSC.smooth_edge_integral line 100
  20. def OAI.LipschitzCounterexample.CompactWSC.gradEnergy line 111
  21. def OAI.LipschitzCounterexample.CompactWSC.gradMass line 115
  22. theorem OAI.LipschitzCounterexample.CompactWSC.gradEnergy_nonneg line 119
  23. theorem OAI.LipschitzCounterexample.CompactWSC.gradMass_nonneg line 125
  24. theorem OAI.LipschitzCounterexample.CompactWSC.gradEnergy_midpoint line 131