OAI/Dynamics/ConditionalShuffle/ResetEnergy.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Thorp.Conditional.halfDensity_after_step_rho line 9
  2. theorem OAI.Thorp.Conditional.expectedNoise_dimension_rho line 24
  3. theorem OAI.Thorp.Conditional.expectedNoise_bound_rho line 65
  4. theorem OAI.Thorp.Conditional.expectedEnergy_decay_rho line 78
  5. def OAI.Thorp.Conditional.resetS line 93
  6. lemma OAI.Thorp.Conditional.resetS_large line 95
  7. lemma OAI.Thorp.Conditional.reset_gamma_power line 101
  8. lemma OAI.Thorp.Conditional.reset_energy_bound line 127
  9. lemma OAI.Thorp.Conditional.reset_noise_scaled_tendsto line 149
  10. lemma OAI.Thorp.Conditional.reset_energy_eventually line 159