OAI/Analysis/VlasovMaxwell/Retarded/SourceCellLast.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RVM.sourceCellLast line 37
  2. def OAI.RVM.sourceCellLo line 38
  3. def OAI.RVM.sourceCellHi line 39
  4. def OAI.RVM.selectedSourceCells line 41
  5. lemma OAI.RVM.sourceCellLast_le line 46
  6. lemma OAI.RVM.sourceCell_mem_prefix line 50
  7. lemma OAI.RVM.sourceCell_full line 65
  8. lemma OAI.RVM.sourceCell_cover line 76
  9. lemma OAI.RVM.selectedSourceCells_cover line 87
  10. lemma OAI.RVM.selectedSourceCells_subset_prefix line 98
  11. lemma OAI.RVM.selectedSourceCells_enlargement line 107
  12. lemma OAI.RVM.sourceCells_pairwise_disjoint line 116
  13. def OAI.RVM.goodFieldConeMass line 139
  14. def OAI.RVM.goodConeIntegrand line 144
  15. lemma OAI.RVM.EnergyPrefix.goodConeIntegrand_continuous line 147
  16. lemma OAI.RVM.EnergyPrefix.goodConeIntegrand_nonneg line 152
  17. lemma OAI.RVM.EnergyPrefix.goodConeIntegrand_sphere_continuous line 157
  18. lemma OAI.RVM.EnergyPrefix.goodConeIntegrand_sphere_integral_continuous line 163
  19. lemma OAI.RVM.EnergyPrefix.goodConeIntegrand_lintegral_eq line 170
  20. lemma OAI.RVM.EnergyPrefix.goodFieldConeMass_le_density line 187
  21. lemma OAI.RVM.EnergyPrefix.goodFieldConeMass_bound line 201
  22. lemma OAI.RVM.dyadicWindow_single_sum_indicator line 210
  23. lemma OAI.RVM.finset_sum_lintegral_le line 227
  24. def OAI.RVM.receiverAngularSet line 237
  25. def OAI.RVM.goodFieldBinConeMass line 240
  26. def OAI.RVM.goodFieldBudget line 246
  27. lemma OAI.RVM.goodFieldBinConeMass_sum_le line 249
  28. lemma OAI.RVM.EnergyPrefix.goodFieldBudget_sum_bound line 271
  29. lemma OAI.RVM.EnergyPrefix.goodFieldBudget_tsum_bound line 292
  30. lemma OAI.RVM.EnergyPrefix.goodFieldBudget_uniform line 301
  31. lemma OAI.RVM.EnergyPrefix.goodFieldBudget_finite line 321
  32. lemma OAI.RVM.EnergyPrefix.magnetic_lintegral_bound line 361
  33. def OAI.RVM.arrivalAngularSet line 375
  34. lemma OAI.RVM.PhaseFlowOn.measurable_arrivalAngularSet line 384
  35. lemma OAI.RVM.arrivalAngularSet_sum_indicator line 413
  36. def OAI.RVM.magneticFieldBudget line 444
  37. lemma OAI.RVM.EnergyPrefix.magneticFieldBudget_sum_bound line 449
  38. lemma OAI.RVM.EnergyPrefix.magneticFieldBudget_tsum_bound line 477
  39. lemma OAI.RVM.EnergyPrefix.magneticFieldBudget_uniform line 486