OAI/Combinatorics/EditDistance/Cuts.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Finite scalar and absolutely summable cut decompositions

  1. lemma OAI.EditCuts.top_clipping_distance line 13
  2. def OAI.EditCuts.cut line 34
  3. theorem OAI.EditCuts.scalar_decomposition_aux line 36
  4. theorem OAI.EditCuts.scalar_decomposition line 86
  5. abbrev OAI.EditCuts.RealL1 line 98
  6. lemma OAI.EditCuts.l1_norm line 100
  7. lemma OAI.EditCuts.l1_summable line 103
  8. lemma OAI.EditCuts.l1_norm_sub line 106
  9. lemma OAI.EditCuts.cut_empty line 113
  10. lemma OAI.EditCuts.cut_univ line 114
  11. theorem OAI.EditCuts.scalar_decomposition_nontrivial line 116
  12. lemma OAI.EditCuts.weight_le_distance line 133
  13. theorem OAI.EditCuts.l1_decomposition line 143