OAI/Analysis/VlasovMaxwell/Geometry/CrossCLM.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.cross_apply_cyclic line 34
  2. def OAI.RVM.crossCLM line 38
  3. lemma OAI.RVM.crossCLM_apply line 45
  4. lemma OAI.RVM.integral_cross_left line 47
  5. def OAI.RVM.retardedMagneticDensity line 51
  6. def OAI.RVM.retardedMagneticFlux line 54
  7. lemma OAI.RVM.integrable_retardedElectricDensity_integrand line 57
  8. lemma OAI.RVM.retardedMagneticDensity_component line 73
  9. lemma OAI.RVM.integrable_retarded_flux_integrand line 87
  10. lemma OAI.RVM.retardedMagneticFlux_components line 97
  11. lemma OAI.RVM.contDiffOn_retardedMagnetic_flux line 118
  12. lemma OAI.RVM.retarded_magnetic_flux_norm_bound line 133
  13. lemma OAI.RVM.retarded_magnetic_flux_tip line 161