OAI/MathematicalPhysics/Heisenberg/ExposedEnergy.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Heisenberg.Exposure.exposedStep_substochastic line 27
  2. lemma OAI.Heisenberg.Exposure.exposedSweep_contraction line 33
  3. theorem OAI.Heisenberg.Exposure.exposedSweep_energy line 43
  4. lemma OAI.Heisenberg.Exposure.quietEnergy_le_card line 58
  5. theorem OAI.Heisenberg.Exposure.exposedSweep_loss line 68
  6. def OAI.Heisenberg.Bernoulli.weight line 105
  7. def OAI.Heisenberg.Bernoulli.join line 107
  8. lemma OAI.Heisenberg.Bernoulli.join_at line 111
  9. lemma OAI.Heisenberg.Bernoulli.join_ne line 115
  10. lemma OAI.Heisenberg.Bernoulli.join_update line 119
  11. lemma OAI.Heisenberg.Bernoulli.weight_join line 126
  12. lemma OAI.Heisenberg.Bernoulli.sum_split line 132
  13. lemma OAI.Heisenberg.Bernoulli.scalar_bound line 144
  14. lemma OAI.Heisenberg.Bernoulli.weight_nonneg line 151
  15. lemma OAI.Heisenberg.Bernoulli.one_coin line 157
  16. def OAI.Heisenberg.Bernoulli.test line 178
  17. lemma OAI.Heisenberg.Bernoulli.test_nonneg line 180
  18. lemma OAI.Heisenberg.Bernoulli.test_update line 183
  19. lemma OAI.Heisenberg.Bernoulli.test_insert line 194
  20. theorem OAI.Heisenberg.Bernoulli.factorial_bound line 199
  21. theorem OAI.Heisenberg.Bernoulli.factorial_bound_rates line 220
  22. theorem OAI.Heisenberg.Bernoulli.polynomial_bound line 242
  23. lemma OAI.Heisenberg.Bernoulli.test_eq_prod line 255
  24. lemma OAI.Heisenberg.Bernoulli.weight_test_sum line 261