OAI/Analysis/VlasovMaxwell/Retarded/ReceiverRadialDomain.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RVM.PhaseFlowOn.arrival_strictMono line 29
2. def OAI.RVM.receiverRadialDomain line 44
3. def OAI.RVM.receiverRadial line 46
4. lemma OAI.RVM.isOpen_receiverRadialDomain line 49
5. lemma OAI.RVM.receiver_time_mem line 53
6. lemma OAI.RVM.PhaseFlowOn.receiver_injective line 57
7. lemma OAI.RVM.PhaseFlowOn.exists_arrival line 77
8. lemma OAI.RVM.PhaseFlowOn.receiver_image line 92
9. lemma OAI.RVM.PhaseFlowOn.receiver_differential line 146
10. lemma OAI.RVM.PhaseFlowOn.receiver_jacobian line 157
11. lemma OAI.RVM.PhaseFlowOn.receiver_integral line 181