OAI/MathematicalPhysics/Heisenberg/WeightedLeakage.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Heisenberg.FiniteLeakage.weighted_young line 22
  2. lemma OAI.Heisenberg.FiniteLeakage.weighted_suffix line 39
  3. theorem OAI.Heisenberg.FiniteLeakage.weighted_leakage line 45
  4. lemma OAI.Heisenberg.FiniteLeakage.sum_succ_real line 82
  5. lemma OAI.Heisenberg.FiniteLeakage.fin_prefix_succ line 88
  6. def OAI.Heisenberg.FiniteLeakage.triangle line 104
  7. lemma OAI.Heisenberg.FiniteLeakage.triangle_nonneg line 106
  8. lemma OAI.Heisenberg.FiniteLeakage.triangle_sum line 108
  9. lemma OAI.Heisenberg.FiniteLeakage.triangle_prefix line 114
  10. lemma OAI.Heisenberg.FiniteLeakage.triangle_prefix_pos line 125
  11. theorem OAI.Heisenberg.FiniteLeakage.triangle_remainder line 130
  12. theorem OAI.Heisenberg.FiniteLeakage.contraction_loss_lower line 152
  13. theorem OAI.Heisenberg.FiniteLeakage.finite_future_loss line 162
  14. def OAI.Heisenberg.FiniteLeakage.chain line 183
  15. lemma OAI.Heisenberg.FiniteLeakage.chain_zero line 187
  16. lemma OAI.Heisenberg.FiniteLeakage.chain_succ line 188
  17. lemma OAI.Heisenberg.FiniteLeakage.chain_contraction line 191
  18. lemma OAI.Heisenberg.FiniteLeakage.suffix_telescope line 198
  19. lemma OAI.Heisenberg.FiniteLeakage.suffix_telescope_fin line 213
  20. theorem OAI.Heisenberg.FiniteLeakage.contraction_chain_leakage line 220