OAI/GroupTheory/PolycyclicRecognition/Analysis/TupleFixedSlicePacking.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Fixed-slice lower packing for correlated tuples

An ambient product ball pulls back to a product of fixed-slice balls. The set to be packed need not be a product set.

  1. theorem OAI.PolycyclicRecognition.lower_count_rate_of_volume line 19
  2. theorem OAI.PolycyclicRecognition.tuple_fixedSlice_ball_measure line 49
  3. theorem OAI.PolycyclicRecognition.exists_tuple_fixedSlice_separated_net line 68
  4. theorem OAI.PolycyclicRecognition.exists_tuple_fixedSlice_count_rate line 84