OAI/Analysis/VlasovMaxwell/Retarded/InitialPuncturedCone.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.PhaseFlowOn.initial_label_lintegral line 38
  2. def OAI.RVM.initialPuncturedCone line 110
  3. lemma OAI.RVM.isOpen_initialPuncturedCone line 113
  4. lemma OAI.RVM.initialPuncturedCone_sub line 118
  5. lemma OAI.RVM.PhaseFlowOn.initial_spherical_label_mem line 126
  6. def OAI.RVM.initialConeState line 141
  7. lemma OAI.RVM.PhaseFlowOn.initial_state_regular line 145
  8. lemma OAI.RVM.PhaseFlowOn.initial_selected_cutoff line 177
  9. def OAI.RVM.selectedInitialKernel line 192
  10. lemma OAI.RVM.PhaseFlowOn.selected_initial_kernel_measurable line 200
  11. lemma OAI.RVM.PhaseFlowOn.selected_initial_kernel_pullback line 223
  12. lemma OAI.RVM.selectedInitialKernel_integrable_bound line 238
  13. lemma OAI.RVM.PhaseFlowOn.selected_label_branch_formula line 303
  14. lemma OAI.RVM.PhaseFlowOn.branchDomain_empty_of_not_initial line 414
  15. lemma OAI.RVM.PhaseFlowOn.ae_selected_label_formula line 426
  16. lemma OAI.RVM.PhaseFlowOn.selected_signed_fubini line 467
  17. lemma OAI.RVM.integrable_bounded_clm_apply line 493
  18. lemma OAI.RVM.PhaseFlowOn.integrable_receiver_multiplier line 503
  19. def OAI.RVM.selectedMultiplierForce line 512
  20. def OAI.RVM.selectedMultiplierCosts line 516
  21. lemma OAI.RVM.PhaseFlowOn.selectedMultiplier_integrable line 522
  22. lemma OAI.RVM.PhaseFlowOn.receiver_multiplier_closed_regularity line 539
  23. lemma OAI.RVM.PhaseFlowOn.selected_multiplier_branch_formula line 573
  24. lemma OAI.RVM.PhaseFlowOn.ae_selected_multiplier_formula line 651
  25. lemma OAI.RVM.PhaseFlowOn.selected_multiplier_fubini line 694