OAI/Analysis/VlasovMaxwell/Retarded/RetardedDifferentiation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RVM.norm_velocity_integral_bound line 12
2. lemma OAI.RVM.retarded_packet_integrable line 24
3. lemma OAI.RVM.retarded_packet_spatial_fderiv line 44
4. lemma OAI.RVM.retarded_packet_derivative_zero line 50
5. lemma OAI.RVM.hasDerivAt_retarded_packet_line line 60
6. lemma OAI.RVM.hasDerivAt_retarded_packet_integral line 90