OAI/Analysis/FreeWords/FlipNorm.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.KKFreeLiftDiagnostic.norm_entry_le_opNorm line 14
  2. theorem OAI.KKFreeLiftDiagnostic.normalizedTrace_norm_le line 25
  3. theorem OAI.KKFreeLiftDiagnostic.normalizedTrace_sub line 38
  4. theorem OAI.KKFreeLiftDiagnostic.flip_norm line 42
  5. theorem OAI.KKFreeLiftDiagnostic.left_norm line 46
  6. theorem OAI.KKFreeLiftDiagnostic.centeredFlip_close line 51
  7. theorem OAI.KKFreeLiftDiagnostic.centeredFlip_norm_le line 58
  8. theorem OAI.KKFreeLiftDiagnostic.norm_product_difference line 65
  9. theorem OAI.KKFreeLiftDiagnostic.four_product_difference line 71