OAI/GroupTheory/SimpleAmenable/RandomFields/FlagAveragingMatrices.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SimpleAmenable.planeTent line 16
  2. theorem OAI.SimpleAmenable.planeTent_posSemidef line 19
  3. theorem OAI.SimpleAmenable.planeTent_nonneg line 23
  4. theorem OAI.SimpleAmenable.planeTent_le_one line 26
  5. theorem OAI.SimpleAmenable.planeTent_self line 31
  6. def OAI.SimpleAmenable.flagSiteOrdinary line 34
  7. def OAI.SimpleAmenable.scaledSiteConjugate line 37
  8. def OAI.SimpleAmenable.flagAveragingMatrix line 41
  9. theorem OAI.SimpleAmenable.flagAveragingMatrix_posSemidef line 50
  10. theorem OAI.SimpleAmenable.flagAveragingMatrix_cutoff_left line 81
  11. theorem OAI.SimpleAmenable.flagAveragingMatrix_cutoff_right line 86
  12. theorem OAI.SimpleAmenable.flagSite_cutoff_finite line 91
  13. theorem OAI.SimpleAmenable.flagAveragingMatrix_finite_support line 107
  14. theorem OAI.SimpleAmenable.tentFactor_ne_zero line 124
  15. theorem OAI.SimpleAmenable.planeTent_ne_zero line 130
  16. theorem OAI.SimpleAmenable.flagAveragingMatrix_localization line 134
  17. theorem OAI.SimpleAmenable.flagAveragingMatrix_row_card line 159
  18. theorem OAI.SimpleAmenable.flagAveragingMatrix_entry_bounds line 173
  19. theorem OAI.SimpleAmenable.flagAveragingMatrix_row_energy line 200