OAI/Analysis/VlasovMaxwell/Flow/BranchIntegral.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.PhaseFlowOn.branch_integral line 35
  2. lemma OAI.RVM.PhaseFlowOn.branch_integrable_iff line 50
  3. lemma OAI.RVM.PhaseFlowOn.branch_retardedSource line 66
  4. lemma OAI.RVM.PhaseFlowOn.actual_branch_force line 89
  5. lemma OAI.RVM.datum_moment_bounds line 137
  6. lemma OAI.RVM.norm_coordinate_le line 151
  7. lemma OAI.RVM.norm_le_three_of_coordinate_bound line 154
  8. lemma OAI.RVM.freeWave_bound_compact line 162
  9. lemma OAI.RVM.norm_initial_cone_flux line 172
  10. lemma OAI.RVM.norm_initial_magnetic_cone_flux line 197
  11. lemma OAI.RVM.norm_sphere_integral_le line 222
  12. lemma OAI.RVM.abs_sphere_integral_le line 227
  13. lemma OAI.RVM.waveK_bound_of_bounded line 231
  14. lemma OAI.RVM.electricConeBoundary_datum_bound line 242
  15. lemma OAI.RVM.magneticConeBoundary_datum_bound line 290
  16. lemma OAI.RVM.boundaryLorentzForce_datum_bound line 345