OAI/Combinatorics/BalancedRyser/Profiles/ProfileWeakDetection.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.ProfileWeakDetection.prod_eq_mass_smul_normalized line 14
  2. theorem OAI.Balanced.ProfileWeakDetection.tendsto_finiteMeasure_prod line 25
  3. theorem OAI.Balanced.ProfileWeakDetection.finiteMeasure_le_liminf_open line 50
  4. theorem OAI.Balanced.ProfileWeakDetection.finiteMeasureReal_le_liminf_open line 80
  5. def OAI.Balanced.ProfileWeakDetection.detectionSet line 107
  6. theorem OAI.Balanced.ProfileWeakDetection.isOpen_detectionSet line 111
  7. theorem OAI.Balanced.ProfileWeakDetection.le_liminf_product_detection line 117
  8. theorem OAI.Balanced.ProfileWeakDetection.detectionSet_subset_of_uniform_approximation line 136
  9. theorem OAI.Balanced.ProfileWeakDetection.le_liminf_open_sections line 147
  10. theorem OAI.Balanced.ProfileWeakDetection.le_liminf_moving_product_detection line 171