OAI/GroupTheory/SimpleAmenable/Amenability/BarrierCore.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.conjugateLineForm_site line 16
  2. def OAI.SimpleAmenable.conjugateIntersectionCoefficient line 34
  3. theorem OAI.SimpleAmenable.conjugateIntersectionCoefficient_nonneg line 38
  4. theorem OAI.SimpleAmenable.conjugateLineForm_bound line 41
  5. theorem OAI.SimpleAmenable.exists_barrierIntersection_core line 57
  6. theorem OAI.SimpleAmenable.exists_barrierIncoming_core line 90
  7. theorem OAI.SimpleAmenable.scaledSiteConjugate_eq_smul line 109
  8. theorem OAI.SimpleAmenable.norm_scaledSiteConjugate line 113
  9. theorem OAI.SimpleAmenable.conjugateLineForm_scaledSite line 118
  10. theorem OAI.SimpleAmenable.firstSignal_true_norm line 125
  11. theorem OAI.SimpleAmenable.firstSignal_true_in_box line 135
  12. def OAI.SimpleAmenable.finiteFirstMarks line 145
  13. theorem OAI.SimpleAmenable.mem_finiteFirstMarks_iff line 149
  14. theorem OAI.SimpleAmenable.firstSignal_true_finite line 156
  15. theorem OAI.SimpleAmenable.secondSignal_negative_empty line 164
  16. theorem OAI.SimpleAmenable.cutoff_mismatch_negative line 181