OAI/GroupTheory/PolycyclicRecognition/Analysis/ProductProbeSelection.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Joint selection from product-measure concentration

Fubini selection retains a compact set of quarter mass satisfying the product bounds for all three finite prefix families.

  1. theorem OAI.PolycyclicRecognition.finite_dependent_bad_union_tendsto_zero line 17
  2. theorem OAI.PolycyclicRecognition.dependent_bad_distance_triangle_tendsto_zero line 29
  3. theorem OAI.PolycyclicRecognition.exists_compact_probes_from_supported_product_profiles line 54
  4. theorem OAI.PolycyclicRecognition.exists_supported_product_chain_probe_sequence line 85
  5. theorem OAI.PolycyclicRecognition.exists_supported_product_affine_probe_sequence line 177
  6. theorem OAI.PolycyclicRecognition.exists_supported_three_product_affine_probe_sequence line 232