OAI/Combinatorics/CycleDecomposition/ReservoirSampling.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ErdosGallai.Sampling.eventually_monomial_lt line 13
  2. lemma OAI.ErdosGallai.Sampling.tendsto_monomial_exp_neg_power line 24
  3. lemma OAI.ErdosGallai.Sampling.eventually_log_le_small_power line 33
  4. def OAI.ErdosGallai.Sampling.samplingScaleError line 39
  5. lemma OAI.ErdosGallai.Sampling.samplingScaleError_tendsto line 44
  6. def OAI.ErdosGallai.Sampling.SamplingScaleReady line 53
  7. lemma OAI.ErdosGallai.Sampling.sampling_witness_error_le line 64
  8. lemma OAI.ErdosGallai.Sampling.eventually_samplingScaleReady line 154
  9. theorem OAI.ErdosGallai.Sampling.vertex_sampling_uniform line 247
  10. def OAI.ErdosGallai.Sampling.reservoirLabelPMF line 279
  11. def OAI.ErdosGallai.Sampling.labelIs line 289
  12. lemma OAI.ErdosGallai.Sampling.ofReal_unitInterval line 291
  13. lemma OAI.ErdosGallai.Sampling.labelIs_preserving line 298
  14. def OAI.ErdosGallai.Sampling.reservoirSample line 328
  15. def OAI.ErdosGallai.Sampling.reservoirMeasure line 330
  16. instance OAI.ErdosGallai.Sampling.reservoirMeasure_probability line 333
  17. lemma OAI.ErdosGallai.Sampling.reservoirSample_preserving line 336
  18. lemma OAI.ErdosGallai.Sampling.reservoirSamples_disjoint line 340
  19. theorem OAI.ErdosGallai.Sampling.three_reservoirs_uniform line 350