OAI/Probability/SKGap/Localization/Error.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKGap.SourceError.real_op_norm_nonneg line 16
  2. lemma OAI.SKGap.SourceError.cauchy_bound line 18
  3. lemma OAI.SKGap.SourceError.double_cauchy line 26
  4. def OAI.SKGap.SourceError.traceAbsolute line 33
  5. lemma OAI.SKGap.SourceError.trace_le_traceAbsolute line 36
  6. lemma OAI.SKGap.SourceError.matrix_column_square_le line 43
  7. lemma OAI.SKGap.SourceError.matrix_row_square_le line 48
  8. lemma OAI.SKGap.SourceError.small_column_square line 52
  9. lemma OAI.SKGap.SourceError.small_row_square line 62
  10. lemma OAI.SKGap.SourceError.quadratic_trace_bound line 67
  11. lemma OAI.SKGap.SourceError.mixed_trace_bound line 78
  12. lemma OAI.SKGap.SourceError.parameter_square_trace_bound line 101
  13. theorem OAI.SKGap.SourceError.source_taylor_trace_bound line 120
  14. lemma OAI.SKGap.SourceError.fourth_holder line 146
  15. lemma OAI.SKGap.SourceError.sum_split_diagonal line 166
  16. lemma OAI.SKGap.SourceError.diagonal_product_trace_bound line 175
  17. lemma OAI.SKGap.SourceError.parameter_product_trace_bound line 190
  18. theorem OAI.SKGap.SourceError.source_product_trace_bound line 206
  19. lemma OAI.SKGap.SourceError.trace_square_eq line 245
  20. lemma OAI.SKGap.SourceError.frobenius_from_traces line 250
  21. theorem OAI.SKGap.SourceError.source_taylor_frobenius_bound line 256
  22. theorem OAI.SKGap.SourceError.source_product_frobenius_bound line 269
  23. lemma OAI.SKGap.SourceError.rank_one_trace_bound line 289