OAI/Dynamics/ConditionalShuffle/OverlayRate.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Thorp.Conditional.OverlayEnergy.prepError line 10
  2. lemma OAI.Thorp.Conditional.OverlayEnergy.prepError_nonneg line 14
  3. lemma OAI.Thorp.Conditional.OverlayEnergy.error_scaled_sq line 16
  4. lemma OAI.Thorp.Conditional.OverlayEnergy.error_scaled_tendsto line 34
  5. lemma OAI.Thorp.Conditional.OverlayEnergy.prepError_tendsto line 47
  6. lemma OAI.Thorp.Conditional.OverlayEnergy.pow_add_bound line 51
  7. lemma OAI.Thorp.Conditional.OverlayEnergy.gamma_power line 63
  8. lemma OAI.Thorp.Conditional.OverlayEnergy.coefficient_scaled_tendsto line 65
  9. lemma OAI.Thorp.Conditional.OverlayEnergy.total_energy_tendsto line 91
  10. def OAI.Thorp.Conditional.OverlayEnergy.marginalRate line 100
  11. lemma OAI.Thorp.Conditional.OverlayEnergy.marginalRate_tendsto line 102