OAI/Analysis/VlasovMaxwell/Population/UnselectedCover.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.PhaseFlowOn.direct_source_representative_cost line 19
  2. lemma OAI.RVM.PhaseFlowOn.selectedSourceTriangle_direct_le line 55
  3. abbrev OAI.RVM.UnselectedCoverIndex line 84
  4. def OAI.RVM.unselectedCoverBin line 86
  5. def OAI.RVM.unselectedCoverSector line 89
  6. lemma OAI.RVM.physical_remaining_active_finite_cover line 95
  7. lemma OAI.RVM.physical_unselected_active_cover line 124
  8. lemma OAI.RVM.PhaseFlowOn.bulkUnselectedCone_support line 150
  9. lemma OAI.RVM.Admissible.unselected_small_source_uniform line 165
  10. lemma OAI.RVM.unselectedCover_tsum line 229
  11. lemma OAI.RVM.PhaseFlowOn.selectedSourceTriangle_v_integral_le line 241
  12. lemma OAI.RVM.PhaseFlowOn.selectedSourceTriangle_bin_integral_le line 259
  13. lemma OAI.RVM.PhaseFlowOn.unselectedSourceTriangle_physical_sum line 276
  14. lemma OAI.RVM.PhaseFlowOn.selectedTransportTriangle_direct_le line 310
  15. lemma OAI.RVM.PhaseFlowOn.selectedTransportTriangle_v_integral_le line 338
  16. lemma OAI.RVM.PhaseFlowOn.selectedTransportTriangle_bin_integral_le line 356
  17. lemma OAI.RVM.PhaseFlowOn.unselectedTransportTriangle_physical_sum line 373
  18. lemma OAI.RVM.Admissible.unselected_transport_uniform line 407
  19. lemma OAI.RVM.Admissible.unselected_source_uniform line 466
  20. lemma OAI.RVM.Admissible.unselected_label_uniform line 531