OAI/Analysis/VlasovMaxwell/Continuation/PrefixParticle.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.PhaseFlowOn.physical_hit_arrival line 36
  2. lemma OAI.RVM.dyadicWindow_one_inv line 60
  3. lemma OAI.RVM.dyadicWindow_one_sqrt line 73
  4. lemma OAI.RVM.PhaseFlowOn.closedBinHit_in_arrivalBudget line 91
  5. def OAI.RVM.prefixParticle line 111
  6. def OAI.RVM.prefixField line 114
  7. lemma OAI.RVM.EnergyPrefix.continuous_prefixParticle line 117
  8. lemma OAI.RVM.continuous_prefixField line 123
  9. lemma OAI.RVM.measurable_coneBinDensity line 130
  10. lemma OAI.RVM.physicalBinDensity_aemeasurable line 163
  11. lemma OAI.RVM.physicalBin_integral_le_budget line 178
  12. def OAI.RVM.prefixConeGood line 223
  13. lemma OAI.RVM.EnergyPrefix.measurable_prefixConeGood line 227
  14. lemma OAI.RVM.EnergyPrefix.physicalBin_goodField line 241