OAI/Analysis/VlasovMaxwell/Retarded/ObservationCone.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.stable_positive_projection line 32
  2. lemma OAI.RVM.PhaseFlowOn.label_energy_bound line 45
  3. lemma OAI.RVM.PhaseFlowOn.label_occupation_cell_bound line 58
  4. lemma OAI.RVM.stable_cell_duration line 83
  5. lemma OAI.RVM.PhaseFlowOn.stable_cell_occupation line 103
  6. def OAI.RVM.observationCone line 126
  7. lemma OAI.RVM.contDiffAt_observationCone line 129
  8. lemma OAI.RVM.hasDerivAt_observationCone_source line 134
  9. lemma OAI.RVM.observationCone_source_partial line 143
  10. lemma OAI.RVM.exists_local_emission_branch line 154
  11. lemma OAI.RVM.emission_branch_fderiv line 183