OAI/Probability/SpanningForest/BitRecovery.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem336.bitValue line 12
  2. def OAI.Problem336.slopeReadout line 14
  3. theorem OAI.Problem336.measurable_slopeReadout line 18
  4. theorem OAI.Problem336.slopeReadout_of_tendsto line 25
  5. theorem OAI.Problem336.slopeReadout_linear_add_noise line 33
  6. theorem OAI.Problem336.brownian_integer_slopes line 44
  7. theorem OAI.Problem336.ae_slopeReadout_brownian_observation line 70
  8. def OAI.Problem336.configurationReadout line 84
  9. theorem OAI.Problem336.measurable_configurationReadout line 87
  10. theorem OAI.Problem336.configurationReadout_reindex line 91
  11. theorem OAI.Problem336.brownian_observation_readout_hasLaw line 94
  12. theorem OAI.Problem336.sampler_hasLaw_of_brownian_inversion line 102