OAI/Analysis/MarkovType/TriangularLimitSeminorm.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MarkovSuperreflexivity.TriangularLimit.vectorAt line 23
  2. theorem OAI.MarkovSuperreflexivity.TriangularLimit.vectorAt_bound line 26
  3. def OAI.MarkovSuperreflexivity.TriangularLimit.realize line 33
  4. def OAI.MarkovSuperreflexivity.TriangularLimit.finiteSeminorm line 36
  5. theorem OAI.MarkovSuperreflexivity.TriangularLimit.finiteSeminorm_apply line 39
  6. theorem OAI.MarkovSuperreflexivity.TriangularLimit.finiteSeminorm_le line 42
  7. theorem OAI.MarkovSuperreflexivity.TriangularLimit.bounded line 53
  8. def OAI.MarkovSuperreflexivity.TriangularLimit.limitNorm line 59
  9. theorem OAI.MarkovSuperreflexivity.TriangularLimit.limitNorm_apply line 62
  10. theorem OAI.MarkovSuperreflexivity.TriangularLimit.limitNorm_le line 65
  11. def OAI.MarkovSuperreflexivity.TriangularLimit.tailForm line 70
  12. theorem OAI.MarkovSuperreflexivity.TriangularLimit.tailForm_single line 73
  13. theorem OAI.MarkovSuperreflexivity.TriangularLimit.finite_pairing line 77
  14. theorem OAI.MarkovSuperreflexivity.TriangularLimit.tailForm_le_finite line 91
  15. theorem OAI.MarkovSuperreflexivity.TriangularLimit.tailForm_le line 103
  16. theorem OAI.MarkovSuperreflexivity.TriangularLimit.tailForm_sub line 113
  17. theorem OAI.MarkovSuperreflexivity.TriangularLimit.coordinate_bound line 130
  18. theorem OAI.MarkovSuperreflexivity.TriangularLimit.definite line 140
  19. theorem OAI.MarkovSuperreflexivity.TriangularLimit.basis_bound line 149
  20. theorem OAI.MarkovSuperreflexivity.TriangularLimit.tailForm_basis line 157