OAI/MathematicalPhysics/AlternatingFlow/DecayBounds.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.AlternatingNS.Effective.potential_bound line 13
  2. lemma OAI.AlternatingNS.Effective.slot_estimate line 59
  3. def OAI.AlternatingNS.Effective.readCost line 74
  4. lemma OAI.AlternatingNS.Effective.readCost_computable line 78
  5. lemma OAI.AlternatingNS.Effective.uniform_read_cost line 93
  6. lemma OAI.AlternatingNS.Effective.slot_decay line 122
  7. lemma OAI.AlternatingNS.Effective.loading_bound line 132
  8. lemma OAI.AlternatingNS.Effective.piece_decay line 143
  9. lemma OAI.AlternatingNS.Effective.pulse_scaled line 159
  10. lemma OAI.AlternatingNS.Effective.pulsePiece_decay line 171
  11. lemma OAI.AlternatingNS.Effective.epsilon_small line 213
  12. lemma OAI.AlternatingNS.Effective.weighted_epsilon line 224
  13. lemma OAI.AlternatingNS.Effective.weighted_amplitude_sum line 240