OAI/Probability/CriticalPercolation/Exploration/SequentialExposure.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CriticalPercolation.FiniteProduct.freeze line 16
  2. lemma OAI.CriticalPercolation.FiniteProduct.freeze_self line 20
  3. lemma OAI.CriticalPercolation.FiniteProduct.freeze_depends line 26
  4. lemma OAI.CriticalPercolation.FiniteProduct.expect_exposureLaw line 36
  5. structure OAI.CriticalPercolation.FiniteProduct.Exposure line 52
  6. lemma OAI.CriticalPercolation.FiniteProduct.Exposure.disintegrate line 62
  7. lemma OAI.CriticalPercolation.FiniteProduct.Exposure.weighted_bound line 76
  8. def OAI.CriticalPercolation.BondGraph.incidenceExposure line 107
  9. lemma OAI.CriticalPercolation.BondGraph.clusterObject_cut_closed line 127
  10. def OAI.CriticalPercolation.BondGraph.scheduledContact line 135
  11. lemma OAI.CriticalPercolation.BondGraph.scheduledContact_second line 142
  12. lemma OAI.CriticalPercolation.LazyDFS.compile_contactScore_incidence line 196
  13. lemma OAI.CriticalPercolation.LazyDFS.search_contactScore_incidence line 236
  14. lemma OAI.CriticalPercolation.FiniteProduct.Exposure.bits_congr line 249
  15. lemma OAI.CriticalPercolation.BondGraph.clusterObject_refines line 262
  16. lemma OAI.CriticalPercolation.BondGraph.scheduledContact_record line 274
  17. theorem OAI.CriticalPercolation.FiniteProduct.sequential_bound line 297
  18. def OAI.CriticalPercolation.BondGraph.anchorSet line 335
  19. lemma OAI.CriticalPercolation.BondGraph.anchorSet_mono line 338
  20. lemma OAI.CriticalPercolation.BondGraph.anchor_mem_anchorSet line 344
  21. theorem OAI.CriticalPercolation.BondGraph.scheduled_contact_product line 349
  22. theorem OAI.CriticalPercolation.BondGraph.scheduled_contact_exponential line 377
  23. theorem OAI.CriticalPercolation.SearchTree.contactScore_eq_queryDelta_sum line 418
  24. def OAI.CriticalPercolation.BondGraph.contactWeight line 457
  25. lemma OAI.CriticalPercolation.BondGraph.sum_contactWeight line 462
  26. lemma OAI.CriticalPercolation.BondGraph.contactWeight_nonneg line 470
  27. def OAI.CriticalPercolation.BondGraph.contactKernel line 485
  28. lemma OAI.CriticalPercolation.BondGraph.contactKernel_nonneg line 494
  29. theorem OAI.CriticalPercolation.BondGraph.contactKernel_normalized line 510
  30. lemma OAI.CriticalPercolation.LazyDFS.compile_queryDelta_incidence line 555
  31. lemma OAI.CriticalPercolation.LazyDFS.search_queryDelta_incidence line 598
  32. lemma OAI.CriticalPercolation.BondGraph.contactKernel_record line 614
  33. lemma OAI.CriticalPercolation.FiniteProduct.Exposure.weighted_identity line 646
  34. theorem OAI.CriticalPercolation.BondGraph.adaptive_marked_step line 674