OAI/Analysis/VlasovMaxwell/Retarded/CutoffSourceTangent.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.contDiffAt_physicalCutoffCoordinates line 39
  2. lemma OAI.RVM.hasDerivAt_cutoffRay line 59
  3. lemma OAI.RVM.stateCutoff_ray_deriv line 65
  4. lemma OAI.RVM.stateCutoff_partial_cancel line 74
  5. lemma OAI.RVM.stateCutoff_partial_boundary line 92
  6. def OAI.RVM.cutoffSourceTangent line 115
  7. def OAI.RVM.cutoffGeometryTangent line 116
  8. def OAI.RVM.cutoffReceiverTangent line 118
  9. lemma OAI.RVM.branchCutoffStateRate_split line 120
  10. lemma OAI.RVM.branchSelectedRate_split line 132
  11. lemma OAI.RVM.stateCutoff_partial_cancel_smul line 146
  12. lemma OAI.RVM.stateCutoff_curve_log_bound line 152
  13. lemma OAI.RVM.stateCutoff_source_bound line 171
  14. lemma OAI.RVM.stateCutoff_geometry_bound line 193
  15. lemma OAI.RVM.stateCutoff_receiver_bound line 241
  16. def OAI.RVM.partialCutoffLabelCost line 276
  17. lemma OAI.RVM.actualLabelCutoffCost_split line 282
  18. lemma OAI.RVM.PhaseFlowOn.partialCutoffLabelCost_compl line 300
  19. lemma OAI.RVM.PhaseFlowOn.partialCutoffLabelCost_boundary line 317
  20. lemma OAI.RVM.projected_physical_small_primitive line 340
  21. lemma OAI.RVM.projected_physical_cutoff_cost line 367
  22. lemma OAI.RVM.projected_source_cutoff_cost line 398
  23. lemma OAI.RVM.projected_geometry_cutoff_cost line 415
  24. lemma OAI.RVM.projected_receiver_cutoff_cost line 431
  25. def OAI.RVM.dyadicSelectionBoundary line 450
  26. lemma OAI.RVM.selectedDyadicCutoff_eq_one_of_active line 454
  27. lemma OAI.RVM.stateCutoff_partial_boundary_localization line 472
  28. lemma OAI.RVM.PhaseFlowOn.partialCutoffLabelCost_boundary_localization line 488
  29. lemma OAI.RVM.projected_receiver_cutoff_bin_cost line 545
  30. def OAI.RVM.physicalReceiverCutoffDensity line 578
  31. lemma OAI.RVM.physicalReceiverCutoffDensity_bound line 589
  32. lemma OAI.RVM.physicalReceiverCutoff_near line 626
  33. lemma OAI.RVM.Admissible.receiver_cutoff_near_constant line 673
  34. lemma OAI.RVM.unprojected_physical_small_primitive line 704
  35. lemma OAI.RVM.unprojected_physical_cutoff_cost line 729
  36. lemma OAI.RVM.unprojected_source_cutoff_cost line 760
  37. lemma OAI.RVM.unprojected_geometry_cutoff_cost line 777
  38. lemma OAI.RVM.unprojected_receiver_cutoff_cost line 793
  39. lemma OAI.RVM.unprojected_time_weight_cost line 812