OAI/Combinatorics/BalancedRyser/Profiles/ProfileGridDetection.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Balanced.ProfileGridDetection.BoundedSpace line 15
  2. def OAI.Balanced.ProfileGridDetection.clippedParameter line 17
  3. def OAI.Balanced.ProfileGridDetection.planeClipped line 19
  4. def OAI.Balanced.ProfileGridDetection.dClipped line 23
  5. def OAI.Balanced.ProfileGridDetection.cClipped line 27
  6. theorem OAI.Balanced.ProfileGridDetection.continuous_clippedParameter line 31
  7. theorem OAI.Balanced.ProfileGridDetection.continuous_planeClipped line 34
  8. theorem OAI.Balanced.ProfileGridDetection.continuous_dClipped line 39
  9. theorem OAI.Balanced.ProfileGridDetection.continuous_cClipped line 44
  10. theorem OAI.Balanced.ProfileGridDetection.planeClipped_eq line 49
  11. theorem OAI.Balanced.ProfileGridDetection.dClipped_eq line 55
  12. theorem OAI.Balanced.ProfileGridDetection.cClipped_eq line 66
  13. theorem OAI.Balanced.ProfileGridDetection.tendsto_comap_boundedProfiles line 77
  14. theorem OAI.Balanced.ProfileGridDetection.prod_comap_real_preimage line 89
  15. theorem OAI.Balanced.ProfileGridDetection.cutoff_real_eq_comap line 105
  16. theorem OAI.Balanced.ProfileGridDetection.profile_rightGrid_real line 148
  17. theorem OAI.Balanced.ProfileGridDetection.profile_powerGrid_real line 158
  18. def OAI.Balanced.ProfileGridDetection.clippedDiscrepancy line 168
  19. theorem OAI.Balanced.ProfileGridDetection.continuous_clippedDiscrepancy line 172
  20. theorem OAI.Balanced.ProfileGridDetection.moving_cutoff_liminf line 178
  21. theorem OAI.Balanced.ProfileGridDetection.actual_moving_cutoff_liminf line 230
  22. def OAI.Balanced.ProfileGridDetection.dGridCutoffMass line 288
  23. def OAI.Balanced.ProfileGridDetection.cGridCutoffMass line 295
  24. theorem OAI.Balanced.ProfileGridDetection.cGridCutoffMass_empty line 302
  25. theorem OAI.Balanced.ProfileGridDetection.dCutoff_le_liminf_actual_grid line 307
  26. theorem OAI.Balanced.ProfileGridDetection.cCutoff_le_liminf_of_card_tendsto line 363
  27. theorem OAI.Balanced.ProfileGridDetection.cGridCutoffMass_nonneg line 420
  28. theorem OAI.Balanced.ProfileGridDetection.cGridCutoffMass_le_one line 425
  29. theorem OAI.Balanced.ProfileGridDetection.cover_limit_mass line 445
  30. theorem OAI.Balanced.ProfileGridDetection.cCutoff_le_liminf_actual_grid line 462
  31. theorem OAI.Balanced.ProfileGridDetection.dGridCutoffMass_nonneg line 504
  32. theorem OAI.Balanced.ProfileGridDetection.dGridCutoffMass_le_two_mul line 508
  33. theorem OAI.Balanced.ProfileGridDetection.cutoff_sum_le_liminf_actual_grid line 535
  34. theorem OAI.Balanced.ProfileGridDetection.exists_cutoff_eventually_grid_excess line 566