OAI/Geometry/BallPacking/Degree/HomotopyFlux.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.HigherDimensionalBallPacking.Rigidity.Degree.CoordinateSpace line 12
  2. def OAI.HigherDimensionalBallPacking.Rigidity.Degree.coordinateVector line 14
  3. def OAI.HigherDimensionalBallPacking.Rigidity.Degree.formFlux line 16
  4. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.formFlux_differentiable line 20
  5. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.formFlux_divergence line 25
  6. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.closedForm_box_boundary line 39
  7. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.closedForm_endpoint_flux line 61
  8. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.topForm_closed line 84
  9. def OAI.HigherDimensionalBallPacking.Rigidity.Degree.pullTopForm line 95
  10. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.pullTopForm_differentiable line 100
  11. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.pullTopForm_closed line 108
  12. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.pullTopForm_zero line 120
  13. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.finite_homotopy_flux line 127
  14. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.finite_homotopy_support_endpoint line 144
  15. def OAI.HigherDimensionalBallPacking.Rigidity.Degree.coordinateVolume line 164
  16. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.coordinateVolume_basis line 171
  17. def OAI.HigherDimensionalBallPacking.Rigidity.Degree.weightedVolume line 179
  18. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.weightedVolume_differentiable line 182
  19. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.weightedVolume_zero line 185
  20. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.weightedVolume_basis line 188
  21. def OAI.HigherDimensionalBallPacking.Rigidity.Degree.spaceInclusion line 192
  22. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.spaceInclusion_apply line 195
  23. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.spaceInclusion_coordinateVector line 199
  24. def OAI.HigherDimensionalBallPacking.Rigidity.Degree.timeFace line 206
  25. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.timeFace_hasFDerivAt line 208
  26. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.initial_spatial_derivative line 217
  27. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.initial_weighted_flux line 226
  28. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.topForm_evaluation line 246
  29. theorem OAI.HigherDimensionalBallPacking.Rigidity.Degree.topForm_chartMass_change line 263
  30. structure OAI.HigherDimensionalBallPacking.Rigidity.Degree.SignedSmoothAtlas line 322
  31. structure OAI.HigherDimensionalBallPacking.Rigidity.Degree.AtlasForm line 333
  32. def OAI.HigherDimensionalBallPacking.Rigidity.Degree.AtlasForm.SupportedIn line 343
  33. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.AtlasForm.contDiffOn_extDeriv line 346
  34. def OAI.HigherDimensionalBallPacking.Rigidity.Degree.AtlasForm.exterior line 350
  35. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.AtlasForm.exterior_supported line 366
  36. def OAI.HigherDimensionalBallPacking.Rigidity.Degree.AtlasForm.smul line 381
  37. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.AtlasForm.smul_supported line 393
  38. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.extDeriv_eq_zero_off_tsupport line 408
  39. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.continuous_extDeriv_coefficient line 416
  40. theorem OAI.HigherDimensionalBallPacking.Rigidity.Degree.compact_euclidean_stokes line 423