OAI/Analysis/VlasovMaxwell/Maxwell/ExtendedField.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.doubling_log_bound line 25
  2. lemma OAI.RVM.doubling_interval_lower_bound line 39
  3. lemma OAI.RVM.no_bounded_harmonic_gaps line 66
  4. lemma OAI.RVM.no_bounded_doubling_times line 88
  5. lemma OAI.RVM.det_time_triangular line 119
  6. def OAI.RVM.extendedField line 138
  7. lemma OAI.RVM.trace_extendedField line 140
  8. lemma OAI.RVM.extended_time_component line 167
  9. lemma OAI.RVM.exists_local_time_volume_flow line 180
  10. def OAI.RVM.lorentzField line 237
  11. lemma OAI.RVM.contDiff_lorentzField line 240
  12. lemma OAI.RVM.trace_lorentzField line 248
  13. lemma OAI.RVM.exists_local_lorentz_volume_flow line 254