OAI/Analysis/VlasovMaxwell/Regularity/ParamPrimitive.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.hasFDerivAt_intervalIntegral line 31
  2. lemma OAI.RVM.contDiff_intervalIntegral_nat line 55
  3. lemma OAI.RVM.contDiff_intervalIntegral line 82
  4. def OAI.RVM.paramPrimitive line 91
  5. lemma OAI.RVM.paramPrimitive_scale line 94
  6. lemma OAI.RVM.contDiff_paramPrimitive line 100
  7. lemma OAI.RVM.paramPrimitive_fderiv_apply line 112
  8. def OAI.RVM.dirD line 134
  9. lemma OAI.RVM.contDiff_dirD line 138
  10. lemma OAI.RVM.dirD_dirD line 143
  11. lemma OAI.RVM.dirD_comm line 152
  12. lemma OAI.RVM.dirD_clm_comp line 159
  13. lemma OAI.RVM.deriv_slice_eq_dirD line 169
  14. lemma OAI.RVM.deriv_deriv_slice_eq_dirD line 176
  15. lemma OAI.RVM.dirD_prod_left line 186
  16. def OAI.RVM.volterra line 197
  17. lemma OAI.RVM.contDiff_volterra line 200
  18. lemma OAI.RVM.dirD_volterra line 204
  19. lemma OAI.RVM.spatialPartial_eq_dirD line 221
  20. lemma OAI.RVM.laplace_slice_eq_dirD line 224
  21. lemma OAI.RVM.laplace_volterra line 237
  22. def OAI.RVM.sourceWaveKernel line 271
  23. def OAI.RVM.sourceWave line 274
  24. lemma OAI.RVM.contDiff_sourceWaveKernel line 276
  25. lemma OAI.RVM.contDiff_sourceWave line 288
  26. lemma OAI.RVM.sourceWaveKernel_boundary line 291
  27. lemma OAI.RVM.sourceWave_timeDerivative line 295
  28. lemma OAI.RVM.sourceWaveKernel_timeDerivative line 301
  29. lemma OAI.RVM.sourceWaveKernel_secondTime line 313
  30. lemma OAI.RVM.sourceWave_initial_value line 328
  31. lemma OAI.RVM.sourceWave_initial_velocity line 331
  32. lemma OAI.RVM.sourceWave_equation line 336
  33. lemma OAI.RVM.contDiff_component line 377
  34. lemma OAI.RVM.contDiff_divergence line 381
  35. lemma OAI.RVM.contDiff_curl line 385
  36. lemma OAI.RVM.spatialPartial_sum line 391
  37. lemma OAI.RVM.spatialPartial_comm line 398
  38. lemma OAI.RVM.divergence_curl line 403
  39. lemma OAI.RVM.curl_gradient line 417
  40. lemma OAI.RVM.curl_curl_component line 425
  41. lemma OAI.RVM.deriv_moving_local_energy line 450
  42. lemma OAI.RVM.cone_energy_integrand_nonpos line 541
  43. lemma OAI.RVM.causal_local_energy_vanishes line 568
  44. lemma OAI.RVM.hasFDerivAt_integral_compactParam line 655
  45. lemma OAI.RVM.continuous_integral_compactParam line 682
  46. lemma OAI.RVM.contDiff_integral_compactParam_nat line 693
  47. lemma OAI.RVM.contDiff_integral_compactParam line 719
  48. lemma OAI.RVM.contDiff_integral_compactSet line 730
  49. lemma OAI.RVM.contDiff_integral_uniform_compact line 745
  50. lemma OAI.RVM.contDiff_rho_uniform_compact line 757
  51. lemma OAI.RVM.contDiff_current_uniform_compact line 765
  52. lemma OAI.RVM.integrable_conePotential line 775
  53. lemma OAI.RVM.sourceWave_ball line 790