OAI/Analysis/VlasovMaxwell/Retarded/ConeKernelInterior.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RVM.PhaseFlowOn.measurable_arrivalConeKernel_borel line 37
2. lemma OAI.RVM.PhaseFlowOn.arrivalConeKernel_polar_norm_borel line 69
3. lemma OAI.RVM.PhaseFlowOn.lintegral_norm_labelConeKernel_borel line 124
4. lemma OAI.RVM.PhaseFlowOn.labelConeKernel_polar_norm_borel line 144
5. lemma OAI.RVM.PhaseFlowOn.labelConeKernel_triangle_norm_borel line 155
6. def OAI.RVM.coneKernelInterior line 210
7. lemma OAI.RVM.measurableSet_coneKernelInterior line 213
8. lemma OAI.RVM.PhaseFlowOn.labelKernelState_mem_interior line 218
9. lemma OAI.RVM.PhaseFlowOn.labelConeKernel_interior_indicator line 226
10. lemma OAI.RVM.PhaseFlowOn.labelConeKernel_triangle_norm_interior line 237
11. def OAI.RVM.coneCutoffState line 264
12. def OAI.RVM.coneCutoffRate line 267
13. def OAI.RVM.normalisedSelectedCutoff line 277
14. lemma OAI.RVM.PhaseFlowOn.coneCutoffState_continuousOn line 282
15. lemma OAI.RVM.PhaseFlowOn.coneCutoffRate_continuousOn line 289
16. lemma OAI.RVM.PhaseFlowOn.normalisedSelectedCutoff_continuousOn line 316
17. lemma OAI.RVM.PhaseFlowOn.actualLabelCutoffCost_eq_normalised line 329
18. lemma OAI.RVM.PhaseFlowOn.actualLabelCutoffCost_polar_norm line 348