OAI/Analysis/VlasovMaxwell/Regularity/PhysicalCutoffCoordinates.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RVM.physicalCutoffCoordinates line 37
  2. lemma OAI.RVM.physicalCutoffCoordinates_pos line 41
  3. lemma OAI.RVM.real_deficit_le_two line 50
  4. lemma OAI.RVM.physicalCutoffCoordinates_le_one line 54
  5. lemma OAI.RVM.angularCoordinate_log_deriv line 71
  6. lemma OAI.RVM.dyadicMultiFactor_curve_locally_finite line 83
  7. def OAI.RVM.selectedDyadicBox line 116
  8. def OAI.RVM.selectedDyadicCutoff line 120
  9. lemma OAI.RVM.selectedDyadicCutoff_curve_eventually line 123
  10. lemma OAI.RVM.differentiableAt_selectedDyadicCutoff_curve line 140
  11. lemma OAI.RVM.selectedDyadicCutoff_local_box line 147
  12. lemma OAI.RVM.selectedDyadicBox_compl line 163
  13. lemma OAI.RVM.selectedDyadicCutoff_derivative_cancel line 168
  14. lemma OAI.RVM.selectedDyadicCutoff_derivative_boundary line 182