OAI/Analysis/LipschitzHilbert/Estimates/FiniteMatrixDiscard.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A finite matrix restricted to two retained index sets differs from the full matrix by at most the product bounds with one discarded factor.

  1. theorem OAI.LipschitzHilbert.finite_product_sum line 11
  2. theorem OAI.LipschitzHilbert.finite_matrix_discard_bound line 19