OAI/Analysis/VlasovMaxwell/Population/PartitionOccupation.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.pureOccupation_crude_scalar line 15
  2. lemma OAI.RVM.pureOccupation_clipped_ratio line 31
  3. lemma OAI.RVM.pureOccupation_stable_scalar line 42
  4. lemma OAI.RVM.pureOccupation_improved_scalar line 54
  5. lemma OAI.RVM.ImprovedWindow.min_mass line 77
  6. lemma OAI.RVM.pureOccupation_of_three line 85
  7. lemma OAI.RVM.WeightedDirectionPartition.halfopen_disjoint line 106
  8. lemma OAI.RVM.WeightedDirectionPartition.halfopen_cover line 117
  9. lemma OAI.RVM.WeightedDirectionPartition.cell_direction_oscillation line 123
  10. lemma OAI.RVM.Admissible.exists_bounded_direction_partition line 136
  11. lemma OAI.RVM.PhaseFlowOn.momentum_le_on_initial_tsupport line 174
  12. lemma OAI.RVM.momentum_ne_zero_of_band line 188
  13. lemma OAI.RVM.inv_q_sq_le_of_lower line 194
  14. lemma OAI.RVM.PhaseFlowOn.direction_partition_closed_duration line 199
  15. lemma OAI.RVM.Admissible.exists_stable_direction_partition line 243
  16. lemma OAI.RVM.Admissible.direction_stable_closed_cell_bound line 286
  17. lemma OAI.RVM.Admissible.direction_closed_bin_grid line 352
  18. lemma OAI.RVM.Admissible.direction_closedEulerian_grid line 427
  19. lemma OAI.RVM.eventually_log_power_le_positive_rpow line 478
  20. lemma OAI.RVM.eventually_direction_window line 502
  21. lemma OAI.RVM.eventually_direction_window_absorption line 572
  22. def OAI.RVM.directionGridRate line 583
  23. def OAI.RVM.directionGridConstant line 586
  24. lemma OAI.RVM.directionGridRate_lower line 589
  25. lemma OAI.RVM.directionGridConstant_pos line 593
  26. lemma OAI.RVM.directionGridRate_log_bound line 597
  27. lemma OAI.RVM.directionGridLength_scales line 606
  28. lemma OAI.RVM.direction_grid_count_scalar line 636
  29. lemma OAI.RVM.direction_short_occupation_scalar line 656
  30. lemma OAI.RVM.direction_long_occupation_scalar line 679
  31. lemma OAI.RVM.Admissible.direction_closedEulerian_improved line 699
  32. lemma OAI.RVM.Admissible.representative_pure_occupation line 804