OAI/Analysis/VlasovMaxwell/Population/CappedRepresentativePos.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.cappedRepresentative_pos line 39
  2. lemma OAI.RVM.cappedRepresentative_le_one line 43
  3. lemma OAI.RVM.Admissible.geometry_cutoff_baseline_bin line 46
  4. lemma OAI.RVM.geometry_radial_ennreal_sum line 185
  5. lemma OAI.RVM.Admissible.geometry_cutoff_baseline_radial_sum line 212
  6. lemma OAI.RVM.source_far_sqrt_mass line 259
  7. lemma OAI.RVM.source_far_good_scalar line 268
  8. lemma OAI.RVM.source_far_magnetic_scalar line 276
  9. lemma OAI.RVM.source_far_magnetic_le line 286
  10. lemma OAI.RVM.ennreal_half_ofReal line 304
  11. lemma OAI.RVM.sqrt_energy_pair line 308
  12. lemma OAI.RVM.source_far_energy_scalar line 312
  13. lemma OAI.RVM.source_far_ennreal_scalar line 331
  14. lemma OAI.RVM.Admissible.projected_source_baseline_far line 364
  15. lemma OAI.RVM.Admissible.projected_source_baseline_radius_bound line 510
  16. lemma OAI.RVM.Admissible.direct_source_shared_radius_budget line 574