OAI/Analysis/MarkovType/TriangularNonreflexivity.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MarkovSuperreflexivity.unit_eval_abs_le line 18
  2. theorem OAI.MarkovSuperreflexivity.unit_eval_bounded line 26
  3. theorem OAI.MarkovSuperreflexivity.unit_eval_ulim_bound line 30
  4. def OAI.MarkovSuperreflexivity.unitSequenceBidualLinear line 37
  5. def OAI.MarkovSuperreflexivity.unitSequenceBidual line 47
  6. theorem OAI.MarkovSuperreflexivity.unitSequenceBidual_apply line 54
  7. theorem OAI.MarkovSuperreflexivity.unitSequenceBidual_norm_le line 58
  8. theorem OAI.MarkovSuperreflexivity.unitSequenceBidual_eval_of_eventually_eq line 65
  9. def OAI.MarkovSuperreflexivity.eventualKernelSubmodule line 72
  10. theorem OAI.MarkovSuperreflexivity.triangular_eventually_zero_on_span line 82
  11. theorem OAI.MarkovSuperreflexivity.triangular_functionals_tendsto_zero line 97
  12. theorem OAI.MarkovSuperreflexivity.not_canonicallyReflexive_of_triangular_dense line 116