OAI/Analysis/VlasovMaxwell/Population/RepresentativeClosedBinSourceIndices.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.representativeClosedBin_source_indices line 39
  2. lemma OAI.RVM.PhaseFlowOn.eulerian_supported_momentum line 65
  3. lemma OAI.RVM.PhaseFlowOn.physicalBinDensity_source_truncate line 74
  4. lemma OAI.RVM.PhaseFlowOn.physicalBinDensity_integral_source_truncate line 95
  5. lemma OAI.RVM.exists_source_dyadic_count line 108
  6. lemma OAI.RVM.Admissible.central_density_stable_log_sum line 118
  7. lemma OAI.RVM.capped_radius_tail line 195
  8. lemma OAI.RVM.Admissible.central_density_near_bin line 235
  9. lemma OAI.RVM.Admissible.central_density_deficit_log_sum line 295
  10. lemma OAI.RVM.Admissible.direction_family_moving_log_bound line 416
  11. lemma OAI.RVM.Admissible.direction_family_weight_log_bound line 450
  12. lemma OAI.RVM.unselected_multiplier_support_congr line 482
  13. lemma OAI.RVM.SmoothClassicalPrefix.actual_angular_decomposition line 493
  14. lemma OAI.RVM.angularMultiplierCLM_norm_le line 543
  15. lemma OAI.RVM.extendedAngularCLM_norm_le line 554
  16. lemma OAI.RVM.directionWeight_integrable line 604
  17. lemma OAI.RVM.directionWeight_family_mass line 610
  18. lemma OAI.RVM.Admissible.direction_family_initial_bound line 644
  19. lemma OAI.RVM.Admissible.supported_boundary_force_bound line 685
  20. lemma OAI.RVM.Admissible.direction_family_datum_bound line 707