OAI/Analysis/VlasovMaxwell/Flow/PhaseAcceleration.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RVM.phaseAcceleration line 36
  2. lemma OAI.RVM.PhaseFlowOn.velocity_hasDerivAt line 39
  3. lemma OAI.RVM.PhaseFlowOn.branchDirection_hasDerivAt line 45
  4. lemma OAI.RVM.PhaseFlowOn.actual_signed_identity line 64
  5. def OAI.RVM.DyadicWindow line 104
  6. lemma OAI.RVM.dyadicWindow_index_le line 107
  7. lemma OAI.RVM.dyadicWindow_card_le line 128
  8. lemma OAI.RVM.dyadicWindow_pair_card_le line 143
  9. lemma OAI.RVM.measurableSet_dyadicWindow line 169
  10. def OAI.RVM.sameTimeBudgetSet line 173
  11. def OAI.RVM.arrivalFinalDomain line 178
  12. def OAI.RVM.arrivalBudgetSet line 181
  13. lemma OAI.RVM.PhaseFlowOn.measurable_sameTimeBudgetSet line 191
  14. lemma OAI.RVM.PhaseFlowOn.measurable_arrivalBudgetSet line 224
  15. lemma OAI.RVM.dyadicWindow_sum_indicator line 257
  16. lemma OAI.RVM.jointBudget_pointwise line 274
  17. def OAI.RVM.prefixPhaseEnergy line 319
  18. lemma OAI.RVM.EnergyPrefix.measurable_prefixPhaseEnergy line 322
  19. def OAI.RVM.jointEnergyBudget line 337
  20. lemma OAI.RVM.jointEnergyBudget_eq line 343
  21. lemma OAI.RVM.PhaseFlowOn.jointEnergyBudget_sum_bound line 360
  22. lemma OAI.RVM.PhaseFlowOn.jointEnergyBudget_tsum_bound line 405
  23. lemma OAI.RVM.PhaseFlowOn.jointEnergyBudget_uniform line 414
  24. lemma OAI.RVM.PhaseFlowOn.jointEnergyBudget_finite line 436