OAI/Analysis/HardSphere/Geometry/EndpointDanger.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.Lattice.endpointDanger line 15
  2. lemma OAI.HardSphere.Lattice.fill_endpoint_danger line 18
  3. lemma OAI.HardSphere.Lattice.endpointsExterior_of_no_danger line 42
  4. def OAI.HardSphere.Lattice.acceptedEnvironment line 54
  5. lemma OAI.HardSphere.Lattice.small_star_of_no_large line 57
  6. lemma OAI.HardSphere.Lattice.rejection_subset line 72
  7. def OAI.HardSphere.Lattice.endpointAnimals line 81
  8. lemma OAI.HardSphere.Lattice.endpointAnimals_card line 84
  9. lemma OAI.HardSphere.Lattice.mem_endpointAnimals_card line 95
  10. lemma OAI.HardSphere.Lattice.danger_contains_endpointAnimal line 100
  11. theorem OAI.HardSphere.Lattice.endpointDanger_probability line 111
  12. lemma OAI.HardSphere.Lattice.endpoint_polynomial_le line 148
  13. lemma OAI.HardSphere.Lattice.endpoint_series_le line 160
  14. lemma OAI.HardSphere.Lattice.rejection_probability line 182
  15. lemma OAI.HardSphere.Lattice.large_rejection_eventually line 212
  16. lemma OAI.HardSphere.Lattice.pmf_complement_half line 237
  17. theorem OAI.HardSphere.Lattice.acceptedEnvironment_mass line 252
  18. def OAI.HardSphere.Lattice.SimpleGoodPath line 310
  19. lemma OAI.HardSphere.Lattice.exists_nominal_detour line 313
  20. def OAI.HardSphere.Lattice.detourSample line 332
  21. lemma OAI.HardSphere.Lattice.detourSample_attachment line 339
  22. def OAI.HardSphere.Lattice.goodPathKernel line 348
  23. lemma OAI.HardSphere.Lattice.pmf_map_expectation line 355
  24. def OAI.HardSphere.Lattice.pathNoiseTranspose line 364
  25. lemma OAI.HardSphere.Lattice.fourLaw_transpose line 370
  26. lemma OAI.HardSphere.Lattice.pair_expectation_transpose line 376