OAI/Analysis/VlasovMaxwell/Geometry/RelativeAngleCoordinate.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RVM.relativeAngleCoordinate line 38
  2. lemma OAI.RVM.relative_deficit_pos line 41
  3. lemma OAI.RVM.relativeAngleCoordinate_pos line 47
  4. lemma OAI.RVM.relativeAngleCoordinate_le_one line 50
  5. lemma OAI.RVM.relativeAngleCoordinate_lower line 56
  6. lemma OAI.RVM.relative_angle_index_lt line 78
  7. def OAI.RVM.relativePhysicalFactor line 87
  8. lemma OAI.RVM.relativePhysicalFactor_nonneg line 91
  9. lemma OAI.RVM.relativePhysicalFactor_partition line 95
  10. def OAI.RVM.relativeRepresentativeClosedBin line 102
  11. lemma OAI.RVM.relativePhysicalFactor_positive_closedBin line 107
  12. lemma OAI.RVM.relativePhysicalFactor_positive_indices line 122
  13. lemma OAI.RVM.exists_relative_dyadic_positive line 133
  14. def OAI.RVM.relativeBinRefinement line 143
  15. lemma OAI.RVM.relativeBinRefinement_base line 146
  16. lemma OAI.RVM.relativeBinRefinement_measure line 149
  17. lemma OAI.RVM.coneBinMomentumSet_relative_cover line 152
  18. lemma OAI.RVM.lintegral_coneBin_relative_cover line 162