OAI/Geometry/PolarProducts/SmoothDegree.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SmoothDegree.Space line 16
  2. def OAI.SmoothDegree.basis line 18
  3. def OAI.SmoothDegree.vol line 20
  4. theorem OAI.SmoothDegree.vol_apply line 23
  5. theorem OAI.SmoothDegree.vol_basis line 25
  6. theorem OAI.SmoothDegree.vol_update_basis line 32
  7. theorem OAI.SmoothDegree.contract_basis line 44
  8. theorem OAI.SmoothDegree.extDeriv_contract_basis line 51
  9. theorem OAI.SmoothDegree.extDeriv_contract_eq_zero line 71
  10. def OAI.SmoothDegree.sqsum line 83
  11. theorem OAI.SmoothDegree.sqsum_pos line 85
  12. def OAI.SmoothDegree.dot line 89
  13. theorem OAI.SmoothDegree.dot_apply line 92
  14. theorem OAI.SmoothDegree.hasFDerivAt_sqsum line 95
  15. def OAI.SmoothDegree.radial line 105
  16. theorem OAI.SmoothDegree.hasFDerivAt_radial line 108
  17. theorem OAI.SmoothDegree.radial_divergence line 116
  18. def OAI.SmoothDegree.radialForm line 141
  19. theorem OAI.SmoothDegree.differentiableAt_radialForm line 144
  20. theorem OAI.SmoothDegree.closed_radialForm line 148
  21. def OAI.SmoothDegree.pullForm line 152
  22. theorem OAI.SmoothDegree.differentiableAt_pullForm line 156
  23. theorem OAI.SmoothDegree.closed_pullForm line 163
  24. def OAI.SmoothDegree.formVector line 175
  25. theorem OAI.SmoothDegree.differentiableAt_formVector line 179
  26. theorem OAI.SmoothDegree.divergence_formVector line 186
  27. theorem OAI.SmoothDegree.formVector_radialForm line 206
  28. theorem OAI.SmoothDegree.pullForm_eventually_id line 213
  29. theorem OAI.SmoothDegree.positive_integral_cube line 220
  30. theorem OAI.SmoothDegree.continuous_face line 233
  31. theorem OAI.SmoothDegree.radial_front_pos line 237
  32. theorem OAI.SmoothDegree.radial_back_neg line 245
  33. theorem OAI.SmoothDegree.face_norm_bound line 254
  34. theorem OAI.SmoothDegree.positive_flux line 259
  35. theorem OAI.SmoothDegree.divergence_obstruction line 276
  36. theorem OAI.SmoothDegree.exists_zero_of_identity_outside line 297
  37. theorem OAI.SmoothDegree.exists_zero_space line 322
  38. theorem OAI.SmoothDegree.exists_zero line 329
  39. theorem OAI.SmoothDegree.exists_zero_of_compactSupport line 350