OAI/Analysis/VlasovMaxwell/Population/SelectedDirection.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.SmoothClassicalPrefix.selectedDirectionEnergyPrefix line 14
  2. lemma OAI.RVM.sum_lintegral_le_lintegral_sum line 30
  3. lemma OAI.RVM.directionWeight_family_label_kernel line 40
  4. def OAI.RVM.selectedMultiplierBulkDensity line 66
  5. def OAI.RVM.selectedMultiplierWeightDensity line 72
  6. def OAI.RVM.selectedMultiplierMovingDensity line 77
  7. lemma OAI.RVM.selectedMultiplierCosts_norm_le line 82
  8. lemma OAI.RVM.measurable_vec_clm_apply line 110
  9. lemma OAI.RVM.PhaseFlowOn.selectedMultiplierBulkDensity_measurable line 115
  10. lemma OAI.RVM.PhaseFlowOn.selectedMultiplierWeightDensity_measurable line 125
  11. lemma OAI.RVM.PhaseFlowOn.selectedMultiplierMovingDensity_measurable line 134
  12. lemma OAI.RVM.PhaseFlowOn.selectedMultiplierCosts_integral_bound line 143
  13. lemma OAI.RVM.PhaseFlowOn.selectedMultiplierCosts_family_bound line 176
  14. lemma OAI.RVM.unselected_multiplier_family_bound line 202
  15. lemma OAI.RVM.measurable_angularMultiplierCLM line 229
  16. lemma OAI.RVM.PhaseFlowOn.measurable_labelAngularMultiplier line 234
  17. lemma OAI.RVM.SmoothClassicalPrefix.actual_angular_family_bound line 247
  18. lemma OAI.RVM.PhaseFlowOn.measurable_labelConeKernel_localBorel line 326
  19. lemma OAI.RVM.PhaseFlowOn.partialCutoffLabelCost_measurable line 333
  20. lemma OAI.RVM.PhaseFlowOn.cutoff_label_integral_split line 344
  21. lemma OAI.RVM.Admissible.direction_receiverCutoff_label_log_bound line 381
  22. lemma OAI.RVM.Admissible.direction_selected_bulk_log_bound line 413
  23. lemma OAI.RVM.relativeRepresentative_momentum_subset line 476
  24. lemma OAI.RVM.relativeRepresentative_density_le line 482
  25. lemma OAI.RVM.transport_small_central_coefficient line 489
  26. lemma OAI.RVM.PhaseFlowOn.direct_transport_small_central line 500
  27. lemma OAI.RVM.Admissible.direct_transport_small_stable_radii line 540
  28. lemma OAI.RVM.transport_low_receiver_coefficient line 576
  29. lemma OAI.RVM.Admissible.direct_transport_low_receiver_radii line 606
  30. lemma OAI.RVM.Admissible.direct_transport_sharp_all_radii line 649
  31. lemma OAI.RVM.Admissible.direct_transport_sharp_physical_bound line 705
  32. lemma OAI.RVM.Admissible.direct_transport_sharp_physical_log_bound line 744
  33. lemma OAI.RVM.Admissible.direction_lorentz_log_bound line 784