OAI/Analysis/VlasovMaxwell/Population/ReceiverWeights.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.selectionWeight_pos line 14
  2. lemma OAI.RVM.selectionWeight_log line 17
  3. lemma OAI.RVM.selected_long_time_weight_scalar line 27
  4. lemma OAI.RVM.selectionWeight_sq line 74
  5. def OAI.RVM.spatialThresholdA line 85
  6. def OAI.RVM.spatialThresholdB line 88
  7. lemma OAI.RVM.spatialThresholdA_pos line 91
  8. lemma OAI.RVM.spatialThresholdB_pos line 94
  9. lemma OAI.RVM.spatial_polynomial_normalisation line 97
  10. lemma OAI.RVM.near_lower_radial_condition line 115
  11. lemma OAI.RVM.selected_neighbor_radial_condition line 143
  12. lemma OAI.RVM.spatial_crossing_datum_scale line 153
  13. lemma OAI.RVM.tsum_quad_pair_index line 164
  14. def OAI.RVM.centralIndexSector line 171
  15. lemma OAI.RVM.tsum_centralIndexSector line 176
  16. lemma OAI.RVM.representativeSmallSector_subset_centralIndexSector line 214
  17. lemma OAI.RVM.representativeSpatialCost_le_central_structural line 228
  18. lemma OAI.RVM.Admissible.spatial_structural_uniform line 239
  19. lemma OAI.RVM.EnergyPrefix.particleCone_lintegral line 283
  20. lemma OAI.RVM.EnergyPrefix.physicalBinDensity_particle_flux line 296
  21. lemma OAI.RVM.physicalBin_integral_le_cone line 313
  22. def OAI.RVM.prefixConeDensity line 344
  23. lemma OAI.RVM.EnergyPrefix.continuous_clamped_goodConeDensity line 347
  24. lemma OAI.RVM.EnergyPrefix.measurable_prefixConeDensity line 357
  25. lemma OAI.RVM.EnergyPrefix.physicalBin_radial_density_flux line 369
  26. def OAI.RVM.representativeReceiverCost line 451
  27. lemma OAI.RVM.receiver_near_scalar line 462
  28. lemma OAI.RVM.receiver_far_scalar line 468
  29. lemma OAI.RVM.Admissible.representative_receiver_envelope line 477
  30. lemma OAI.RVM.Admissible.selected_receiver_uniform line 567
  31. def OAI.RVM.representativeTimeWeightCost line 625
  32. lemma OAI.RVM.representativeTimeWeightCost_eq line 636
  33. lemma OAI.RVM.Admissible.time_weight_bin_near line 649
  34. lemma OAI.RVM.Admissible.selected_long_time_weight_uniform line 684
  35. lemma OAI.RVM.representativeTimeWeightCost_le_central line 719
  36. lemma OAI.RVM.Admissible.selected_time_weight_uniform line 761
  37. lemma OAI.RVM.PhaseFlowOn.bulkRemainder_density line 832
  38. lemma OAI.RVM.PhaseFlowOn.bulkRemainder_bin_integral line 941
  39. lemma OAI.RVM.PhaseFlowOn.bulkRate_bin_integral line 973