OAI/Analysis/VlasovMaxwell/Retarded/ConeArgument.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RVM.coneArgument line 19
  2. def OAI.RVM.coneCutoff line 22
  3. lemma OAI.RVM.contDiff_coneArgument line 25
  4. lemma OAI.RVM.contDiff_coneCutoff line 30
  5. lemma OAI.RVM.deriv_transition_nonneg line 34
  6. lemma OAI.RVM.deriv_transition_zero_neg line 37
  7. lemma OAI.RVM.coneArgument_fderiv line 44
  8. lemma OAI.RVM.coneCutoff_fderiv line 59
  9. lemma OAI.RVM.coneArgument_neg_outside line 72
  10. lemma OAI.RVM.coneCutoff_zero_outside line 81
  11. def OAI.RVM.coneShellFlux line 85
  12. lemma OAI.RVM.coneShellFlux_zero_outside line 89
  13. lemma OAI.RVM.coneShellFlux_nonneg line 94
  14. lemma OAI.RVM.deriv_cone_energy line 114
  15. lemma OAI.RVM.classical_particle_flux_continuous_slab line 132
  16. lemma OAI.RVM.classical_total_flux_continuous_slab line 151
  17. lemma OAI.RVM.coneShellFlux_continuous_slab line 159
  18. lemma OAI.RVM.coneShellFlux_integral_continuous line 170
  19. lemma OAI.RVM.cone_energy_continuous line 178
  20. lemma OAI.RVM.coneShellFlux_bound line 188
  21. lemma OAI.RVM.deriv_transition_zero_gt_one line 221
  22. def OAI.RVM.radialConeWeight line 228
  23. lemma OAI.RVM.continuous_radialConeWeight line 231
  24. lemma OAI.RVM.radialConeWeight_nonneg line 236
  25. lemma OAI.RVM.deriv_radial_cone line 240
  26. lemma OAI.RVM.radialConeWeight_mass line 251
  27. lemma OAI.RVM.radialConeWeight_local line 261
  28. lemma OAI.RVM.radialConeWeight_tendsto line 270
  29. lemma OAI.RVM.sphere_norm line 316
  30. def OAI.RVM.radialConeProfile line 319
  31. lemma OAI.RVM.continuous_radialConeProfile line 322
  32. lemma OAI.RVM.continuous_spherical_radialConeProfile line 339
  33. lemma OAI.RVM.coneShellFlux_polar_kernel line 348
  34. lemma OAI.RVM.radialConeWeight_zero_above line 356
  35. lemma OAI.RVM.radialConeWeight_integral_Ioi line 363
  36. lemma OAI.RVM.coneShellFlux_polar line 375
  37. lemma OAI.RVM.coneShellFlux_tendsto line 415
  38. lemma OAI.RVM.integral_limit_nonneg_le line 426
  39. lemma OAI.RVM.classical_light_cone_flux line 457