OAI/Analysis/VlasovMaxwell/Geometry/ActualLabelCutoffCost.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RVM.actualLabelCutoffCost line 37
  2. lemma OAI.RVM.PhaseFlowOn.actualLabelCutoffCost_measurable line 42
  3. lemma OAI.RVM.PhaseFlowOn.actualLabelCutoffCost_integrable line 47
  4. def OAI.RVM.labelReceiverTime line 77
  5. lemma OAI.RVM.PhaseFlowOn.labelReceiverTime_measurable line 80
  6. lemma OAI.RVM.PhaseFlowOn.labelReceiverTime_mem line 87
  7. def OAI.RVM.labelSelectedCutoff line 97
  8. lemma OAI.RVM.PhaseFlowOn.labelSelectedCutoff_bound line 102
  9. def OAI.RVM.actualLabelRatePrimitive line 119
  10. def OAI.RVM.normalisedRatePrimitive line 123
  11. lemma OAI.RVM.PhaseFlowOn.normalisedRatePrimitive_continuousOn line 127
  12. lemma OAI.RVM.PhaseFlowOn.actualLabelRatePrimitive_eq line 149
  13. lemma OAI.RVM.PhaseFlowOn.actualLabelRatePrimitive_integrable line 166
  14. lemma OAI.RVM.PhaseFlowOn.actualLabelRatePrimitive_measurable line 172