OAI/Analysis/VlasovMaxwell/Population/BinHits.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RVM.closedBinHits line 38
  2. lemma OAI.RVM.PhaseFlowOn.compact_closedBinHits_labels line 42
  3. lemma OAI.RVM.PhaseFlowOn.averaged_cell_occupation_interior line 55
  4. lemma OAI.RVM.dyadicWindow_momentum_enlarged line 79
  5. lemma OAI.RVM.dyadicWindow_angle_enlarged line 86
  6. lemma OAI.RVM.small_closed_bin_hit_geometry line 96
  7. lemma OAI.RVM.PhaseFlowOn.small_closed_bin_cell_data line 133
  8. lemma OAI.RVM.PhaseFlowOn.small_closed_bin_cell_payment line 216
  9. lemma OAI.RVM.sameTimeBudget_energy_le_joint line 264
  10. lemma OAI.RVM.closedBinHits_clip_receiver line 275
  11. lemma OAI.RVM.PhaseFlowOn.compact_closedBinHits_joint line 292
  12. lemma OAI.RVM.PhaseFlowOn.measurable_closedBinHits_duration line 315
  13. lemma OAI.RVM.PhaseFlowOn.closedBinHits_occupation_le_sum line 322
  14. lemma OAI.RVM.PhaseFlowOn.small_closed_bin_cells_payment line 351
  15. lemma OAI.RVM.PhaseFlowOn.small_closed_bin_cell_crude line 400
  16. lemma OAI.RVM.closedBinHits_clip_source line 455
  17. lemma OAI.RVM.ennreal_sum_le_erase_add line 471
  18. lemma OAI.RVM.PhaseFlowOn.small_closed_bin_refined_stable line 479
  19. lemma OAI.RVM.jointEnergyBudget_mono_interval line 575
  20. lemma OAI.RVM.stable_source_enlargement line 582
  21. lemma OAI.RVM.stable_source_enlargement_length line 589
  22. lemma OAI.RVM.PhaseFlowOn.stable_small_jointBudget_uniform line 593
  23. lemma OAI.RVM.occupation_divide_cell line 603
  24. lemma OAI.RVM.signedPrimitive_decomposition line 650
  25. lemma OAI.RVM.small_deficit_difference line 658
  26. lemma OAI.RVM.small_primitive_norm line 679
  27. lemma OAI.RVM.transverseProjection_add line 703
  28. lemma OAI.RVM.transverseProjection_smul line 707
  29. lemma OAI.RVM.transverseProjection_normal_dist line 710
  30. lemma OAI.RVM.small_primitive_transverse line 719
  31. lemma OAI.RVM.small_primitive_acceleration_pairing line 744
  32. lemma OAI.RVM.receiver_acceleration_bounds line 769
  33. lemma OAI.RVM.receiver_small_primitive_pairing line 798
  34. lemma OAI.RVM.receiver_bulk_vector_bound line 811
  35. lemma OAI.RVM.receiver_bulk_transverse_bound line 832
  36. lemma OAI.RVM.small_energy_ratio line 859
  37. lemma OAI.RVM.signedRemainder_physical_decomposition line 875
  38. lemma OAI.RVM.signedRemainder_small_norm line 885
  39. lemma OAI.RVM.PhaseFlowOn.cone_occupation_joint_budget line 926
  40. def OAI.RVM.closedBinEulerian line 973
  41. lemma OAI.RVM.measurableSet_spaceConeDomain line 979
  42. lemma OAI.RVM.PhaseFlowOn.measurable_closedBinEulerian line 985
  43. lemma OAI.RVM.PhaseFlowOn.mem_closedBinEulerian_iff line 994
  44. lemma OAI.RVM.PhaseFlowOn.closedBinEulerian_occupation_le line 1014
  45. lemma OAI.RVM.PhaseFlowOn.closedBinEulerian_properties line 1058
  46. lemma OAI.RVM.PhaseFlowOn.closedBinEulerian_in_arrivalBudget line 1072
  47. lemma OAI.RVM.PhaseFlowOn.closedBinEulerian_joint_occupation line 1084
  48. lemma OAI.RVM.lintegral_add_left_Ioo line 1108
  49. lemma OAI.RVM.lintegral_retarded_triangle line 1123
  50. lemma OAI.RVM.lintegral_retarded_triangle_parameter line 1171