OAI/Analysis/VlasovMaxwell/Population/DirectionCutoffs.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.Admissible.central_density_low_receiver_log_sum line 41
  2. lemma OAI.RVM.Admissible.central_density_small_sector_log_sum line 165
  3. lemma OAI.RVM.Admissible.geometry_cutoff_small_sector_log_sum line 247
  4. lemma OAI.RVM.Admissible.projected_remainder_small_sector_log_sum line 322
  5. lemma OAI.RVM.Admissible.projected_source_near_bin line 427
  6. lemma OAI.RVM.sqrt_near_product line 559
  7. lemma OAI.RVM.source_near_good_scalar line 575
  8. lemma OAI.RVM.source_near_magnetic_scalar line 593
  9. lemma OAI.RVM.source_near_ennreal_scalar line 613
  10. lemma OAI.RVM.Admissible.projected_source_near_real_bin line 636
  11. lemma OAI.RVM.capped_radius_sqrt_sum line 671
  12. lemma OAI.RVM.source_low_receiver_scalar line 700
  13. lemma OAI.RVM.PhaseFlowOn.physicalProjectedSource_source_truncate line 746
  14. lemma OAI.RVM.PhaseFlowOn.physicalProjectedSource_integral_source_truncate line 768
  15. lemma OAI.RVM.Admissible.projected_source_low_receiver_log_sum line 781
  16. lemma OAI.RVM.Admissible.source_majorant_remaining_log_sum line 903
  17. def OAI.RVM.directionSelection line 981
  18. lemma OAI.RVM.dyadic_neighbor_product_le line 986
  19. lemma OAI.RVM.directionSelection_boundary_split line 1013
  20. lemma OAI.RVM.Admissible.projected_source_structural_edge_log_sum line 1037
  21. def OAI.RVM.directionSourceEdge line 1101
  22. def OAI.RVM.directionSourceLow line 1105
  23. def OAI.RVM.directionSourceFar line 1109
  24. lemma OAI.RVM.direction_source_cover_sum line 1116
  25. lemma OAI.RVM.Admissible.direction_boundary_source_log_sum line 1151
  26. lemma OAI.RVM.tsum_set_indicator_mono line 1221
  27. lemma OAI.RVM.Admissible.direction_sourceCutoff_label_log_bound line 1231
  28. lemma OAI.RVM.Admissible.direction_geometryCutoff_label_log_bound line 1269