OAI/Analysis/VlasovMaxwell/Population/SpatialEstimates.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.deficit_sqrt_representative_bounds line 15
  2. lemma OAI.RVM.small_bin_deficit_order line 25
  3. lemma OAI.RVM.unprojected_geometry_bin_cost line 31
  4. lemma OAI.RVM.unprojected_source_bin_cost line 56
  5. lemma OAI.RVM.trianglePartial_eq_polar line 105
  6. lemma OAI.RVM.partialCutoffTriangle_norm_le_polar line 126
  7. def OAI.RVM.representativeMagneticCost line 144
  8. lemma OAI.RVM.PhaseFlowOn.bulkSource_pointwise line 156
  9. def OAI.RVM.representativeSpatialTransition line 202
  10. lemma OAI.RVM.Admissible.regular_spatial_transition_pair_sum line 207
  11. def OAI.RVM.bulkSelection line 321
  12. lemma OAI.RVM.physicalCutoff_positive_source_floor line 325
  13. lemma OAI.RVM.bulkSelection_neighbor_aperture line 340
  14. lemma OAI.RVM.bulkSelection_derivative_physical_cover line 349
  15. lemma OAI.RVM.bulkSelection_positive_smallSector line 378
  16. lemma OAI.RVM.partialCutoffTriangle_nonzero_data line 388
  17. lemma OAI.RVM.PhaseFlowOn.partialCutoffTriangle_physical_nonzero line 416
  18. lemma OAI.RVM.PhaseFlowOn.bulkCutoffTriangle_support line 436
  19. lemma OAI.RVM.bulkSelection_derivative_small_cover line 451
  20. lemma OAI.RVM.PhaseFlowOn.bulkCutoffTriangle_small_support line 480
  21. def OAI.RVM.bulkSourceBoundary line 495
  22. lemma OAI.RVM.tsum_structuralCentralSector line 500
  23. lemma OAI.RVM.Admissible.bulk_source_good_uniform line 527
  24. lemma OAI.RVM.PhaseFlowOn.bulkSource_density line 582
  25. lemma OAI.RVM.PhaseFlowOn.bulkSource_bin_integral line 637
  26. lemma OAI.RVM.Admissible.spatial_transition_regular_uniform line 679
  27. lemma OAI.RVM.spatial_exception_radial_sum line 766
  28. lemma OAI.RVM.spatial_exception_angle_radial_sum line 785
  29. lemma OAI.RVM.spatial_exception_triple_sum line 811
  30. def OAI.RVM.representativeExceptionSpatialCost line 839
  31. lemma OAI.RVM.Admissible.representative_exception_spatial_triple_sum line 844
  32. lemma OAI.RVM.Admissible.spatial_exception_uniform line 914
  33. lemma OAI.RVM.Admissible.spatial_transition_uniform line 998
  34. lemma OAI.RVM.PhaseFlowOn.bulkRemainder_selected_sum line 1074
  35. lemma OAI.RVM.Admissible.bulk_remainder_uniform line 1143
  36. lemma OAI.RVM.PhaseFlowOn.bulkRate_selected_sum line 1199
  37. lemma OAI.RVM.Admissible.bulk_rate_uniform line 1267