OAI/Analysis/VlasovMaxwell/Retarded/RetardedRadiusSeparatedClosed.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RVM.PhaseFlowOn.retarded_radius_separated_closed line 38
2. lemma OAI.RVM.PhaseFlowOn.ae_full_retarded_branch line 72
3. lemma OAI.RVM.PhaseFlowOn.initial_branch_pullback line 102
4. lemma OAI.RVM.PhaseFlowOn.initial_signed_boundary_pullback line 128
5. lemma OAI.RVM.PhaseFlowOn.branch_weight_ac line 145
6. lemma OAI.RVM.PhaseFlowOn.actual_temporal_signed_identity_closed line 161
7. lemma OAI.RVM.deriv_comp_of_nonzero_strict line 218
8. lemma OAI.RVM.PhaseFlowOn.branch_weight_deriv line 237
9. lemma OAI.RVM.PhaseFlowOn.branch_weight_deriv_integral line 248
10. lemma OAI.RVM.PhaseFlowOn.actual_temporal_signed_formula line 263
11. lemma OAI.RVM.continuousOn_retardedPrimitive_space line 289
12. def OAI.RVM.initialClosedCone line 307
13. lemma OAI.RVM.PhaseFlowOn.initial_closed_branch_mem line 310
14. lemma OAI.RVM.PhaseFlowOn.initial_branch_lipschitz line 317
15. lemma OAI.RVM.PhaseFlowOn.initial_primitive_continuousOn line 348
16. lemma OAI.RVM.PhaseFlowOn.initial_primitive_measurable line 385