OAI/Analysis/FreeWords/AsymptoticProduct.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.KKAsymptoticTransport.NetBound.const line 19
  2. theorem OAI.KKAsymptoticTransport.NetBound.mul line 22
  3. theorem OAI.KKAsymptoticTransport.NetBound.sub line 30
  4. theorem OAI.KKAsymptoticTransport.NetBound.map line 36
  5. theorem OAI.KKAsymptoticTransport.NetBound.center line 42
  6. theorem OAI.KKAsymptoticTransport.NetBound.isBoundedUnder line 46
  7. theorem OAI.KKAsymptoticTransport.NetBound.netPair line 52
  8. theorem OAI.KKAsymptoticTransport.null_mul line 61
  9. theorem OAI.KKAsymptoticTransport.mul_null line 66
  10. theorem OAI.KKAsymptoticTransport.asymp_mul line 71
  11. theorem OAI.KKAsymptoticTransport.asymp_center line 79
  12. theorem OAI.KKAsymptoticTransport.pair_center_difference line 84
  13. theorem OAI.KKAsymptoticTransport.tendsto_E_of_difference line 101