OAI/Analysis/VlasovMaxwell/Population/DirectionCounts.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.SmoothClassicalPrefix.directionCountsEnergyPrefix line 15
  2. def OAI.RVM.directionRemaining line 31
  3. lemma OAI.RVM.direction_unselected_source_sum line 34
  4. lemma OAI.RVM.PhaseFlowOn.unselected_source_label_physical_sum line 72
  5. lemma OAI.RVM.PhaseFlowOn.selected_transport_label_le line 123
  6. lemma OAI.RVM.PhaseFlowOn.unselected_force_label_integral_split line 139
  7. lemma OAI.RVM.Admissible.direction_unselected_label_log_bound line 155
  8. lemma OAI.RVM.Admissible.supported_boundary_force_uniform_bound line 202
  9. lemma OAI.RVM.Admissible.direction_family_datum_uniform_bound line 224
  10. lemma OAI.RVM.Admissible.direction_lorentz_uniform_log_bound line 266
  11. def OAI.RVM.directionUnionBudget line 323
  12. lemma OAI.RVM.Admissible.direction_physical_family_log_bound line 330
  13. structure OAI.RVM.WeightedDirectionPartition line 451
  14. lemma OAI.RVM.IncrementBootstrap.weighted_direction_partition line 471
  15. lemma OAI.RVM.WeightedDirectionPartition.cell_subset line 529
  16. lemma OAI.RVM.WeightedDirectionPartition.interiors_disjoint line 533
  17. lemma OAI.RVM.WeightedDirectionPartition.weight_sum line 547
  18. lemma OAI.RVM.WeightedDirectionPartition.complete_force_lower line 560
  19. lemma OAI.RVM.WeightedDirectionPartition.total_variation line 569
  20. lemma OAI.RVM.vec_integrable_smul line 584
  21. lemma OAI.RVM.SmoothClassicalPrefix.multiplier_retarded_force_integrable line 589
  22. lemma OAI.RVM.SmoothClassicalPrefix.direction_weighted_force_integrable line 638
  23. lemma OAI.RVM.directionWeight_interval_eq_global line 672
  24. lemma OAI.RVM.SmoothClassicalPrefix.direction_force_family_triangle line 688
  25. lemma OAI.RVM.Admissible.direction_complete_count_cost_bound line 711
  26. def OAI.RVM.directionUnionConstant line 773
  27. lemma OAI.RVM.directionUnionConstant_nonneg line 778
  28. lemma OAI.RVM.directionUnionBudget_scalar_bound line 785
  29. lemma OAI.RVM.direction_receiver_charge_scalar_bound line 815
  30. lemma OAI.RVM.direction_force_budget_scalar_bound line 831
  31. lemma OAI.RVM.eventually_direction_absorption line 859
  32. lemma OAI.RVM.direction_count_cost_scalar_bound line 915
  33. lemma OAI.RVM.direction_count_absorb line 957
  34. def OAI.RVM.datumEnergyNumber line 977
  35. lemma OAI.RVM.Admissible.datumEnergyNumber_nonneg line 980
  36. lemma OAI.RVM.SmoothClassicalPrefix.initial_energy_eq line 987
  37. lemma OAI.RVM.Admissible.direction_complete_count_real_bound line 993
  38. lemma OAI.RVM.Admissible.direction_count_bound line 1065