OAI/Analysis/VlasovMaxwell/Population/SourceWeightedPacket.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RVM.Magnetic.sourceWeightedPacket line 13
2. lemma OAI.RVM.Magnetic.sourceWeightedPacket_contDiffAt line 16
3. lemma OAI.RVM.Magnetic.sourceWeightedPacket_fderiv line 27
4. lemma OAI.RVM.Magnetic.source_packet_estimates line 50
5. lemma OAI.RVM.Magnetic.hasDerivAt_magnetic_source_integral line 90
6. lemma OAI.RVM.Magnetic.retarded_packet_inner_integrable line 116
7. lemma OAI.RVM.Magnetic.norm_integral_ball_inverse_le line 125
8. def OAI.RVM.Magnetic.sourceReceiverParticlePacket line 137
9. lemma OAI.RVM.Magnetic.sourceReceiverParticlePacket_continuousAt line 140
10. lemma OAI.RVM.Magnetic.source_receiver_packet_bound line 151
11. lemma OAI.RVM.Magnetic.magnetic_source_receiver_integral_bound line 175
12. lemma OAI.RVM.Magnetic.magnetic_source_deriv_bound line 197