OAI/Analysis/VlasovMaxwell/Population/SelectedReceiverWeightBoundFinite.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.Admissible.selected_receiver_weight_bound_finite_sources line 39
  2. lemma OAI.RVM.source_angle_coordinate_lower line 134
  3. lemma OAI.RVM.source_energy_index_lt line 153
  4. lemma OAI.RVM.source_angle_index_lt line 162
  5. lemma OAI.RVM.physicalCutoff_positive_source_indices line 173
  6. lemma OAI.RVM.selectedDyadicCutoff_restrict line 214
  7. lemma OAI.RVM.PhaseFlowOn.labelWeight_rate_source_truncate line 229
  8. lemma OAI.RVM.Admissible.selected_receiver_weight_bound line 254
  9. def OAI.RVM.physicalDyadicMovingDensity line 279
  10. lemma OAI.RVM.physicalDyadicMovingDensity_le line 286
  11. lemma OAI.RVM.physicalDyadicMovingDensity_near_pointwise line 335
  12. lemma OAI.RVM.physicalDyadicMoving_triangle_near line 379
  13. lemma OAI.RVM.projectedDyadicRateKernel_polar_moving_density line 449
  14. lemma OAI.RVM.PhaseFlowOn.label_moving_primitive_near line 463
  15. lemma OAI.RVM.Admissible.label_moving_primitive_near_constant line 542
  16. lemma OAI.RVM.selected_representative_moving_bound line 570
  17. lemma OAI.RVM.Admissible.selected_moving_bound_finite_sources line 596
  18. lemma OAI.RVM.Admissible.selected_moving_bound line 693
  19. lemma OAI.RVM.directionWeight_deriv_outside line 719
  20. lemma OAI.RVM.directionWeight_lvariation line 723
  21. lemma OAI.RVM.directionWeight_ne_zero_interior line 739
  22. lemma OAI.RVM.directionWeight_sum_le_one line 750
  23. lemma OAI.RVM.directionWeight_sum_ofReal_le_one line 768
  24. lemma OAI.RVM.directionWeight_sum_kernel line 778
  25. def OAI.RVM.selectedAngularMovingCost line 796
  26. def OAI.RVM.selectedAngularWeightCost line 802
  27. lemma OAI.RVM.PhaseFlowOn.aemeasurable_receiver_force line 807
  28. lemma OAI.RVM.Admissible.direction_family_moving_bound line 817
  29. lemma OAI.RVM.Admissible.direction_family_weight_bound line 851