OAI/Analysis/HardSphere/Geometry/BinaryValue.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.Lattice.binaryValue line 12
  2. lemma OAI.HardSphere.Lattice.binaryValue_injective line 16
  3. def OAI.HardSphere.Lattice.signedValue line 31
  4. lemma OAI.HardSphere.Lattice.signedValue_injective line 34
  5. lemma OAI.HardSphere.Lattice.pmf_map_injective_atom_le line 42
  6. theorem OAI.HardSphere.Lattice.signed_uniform_atom line 58
  7. lemma OAI.HardSphere.Lattice.pmf_independent_shift_atom_le line 65
  8. def OAI.HardSphere.Lattice.spin line 77
  9. lemma OAI.HardSphere.Lattice.abs_spin line 79
  10. lemma OAI.HardSphere.Lattice.binaryValue_snoc line 81
  11. lemma OAI.HardSphere.Lattice.signedValue_snoc line 102
  12. def OAI.HardSphere.Lattice.OffSpine line 109
  13. instance OAI.HardSphere.Lattice.offSpineFintype line 113
  14. instance OAI.HardSphere.Lattice.offSpineNonempty line 120
  15. abbrev OAI.HardSphere.Lattice.TreeNoise line 127
  16. def OAI.HardSphere.Lattice.leaves line 129
  17. lemma OAI.HardSphere.Lattice.length_leaves line 135
  18. lemma OAI.HardSphere.Lattice.abs_of_mem_leaves line 141
  19. def OAI.HardSphere.Lattice.offSum line 154
  20. lemma OAI.HardSphere.Lattice.sum_leaves line 160
  21. lemma OAI.HardSphere.Lattice.uniform_product line 172
  22. theorem OAI.HardSphere.Lattice.leaf_sum_atom line 181
  23. def OAI.HardSphere.Lattice.branchEquiv line 201
  24. abbrev OAI.HardSphere.Lattice.BranchContext line 208
  25. def OAI.HardSphere.Lattice.branchAt line 210
  26. def OAI.HardSphere.Lattice.branchRoot line 228
  27. def OAI.HardSphere.Lattice.branchBefore line 231
  28. def OAI.HardSphere.Lattice.branchAfter line 237
  29. lemma OAI.HardSphere.Lattice.leaves_branchAt line 243
  30. lemma OAI.HardSphere.Lattice.length_branchBefore line 250
  31. def OAI.HardSphere.Lattice.BlockContext line 254
  32. instance OAI.HardSphere.Lattice.blockContextFintype line 258
  33. instance OAI.HardSphere.Lattice.blockContextNonempty line 264
  34. def OAI.HardSphere.Lattice.rotateProd line 270
  35. def OAI.HardSphere.Lattice.extractNoise line 276
  36. def OAI.HardSphere.Lattice.blockRoot line 287
  37. def OAI.HardSphere.Lattice.blockBefore line 291
  38. def OAI.HardSphere.Lattice.blockAfter line 296
  39. lemma OAI.HardSphere.Lattice.leaves_extractNoise line 301
  40. def OAI.HardSphere.Lattice.addressIndex line 313
  41. lemma OAI.HardSphere.Lattice.length_blockBefore line 317
  42. lemma OAI.HardSphere.Lattice.uniform_equiv line 325
  43. lemma OAI.HardSphere.Lattice.pair_map_apply line 335
  44. lemma OAI.HardSphere.Lattice.conditional_atom line 342
  45. lemma OAI.HardSphere.Lattice.addressIndex_lt line 356
  46. lemma OAI.HardSphere.Lattice.addressIndex_surjective line 365
  47. lemma OAI.HardSphere.Lattice.take_sum_block line 379
  48. def OAI.HardSphere.Lattice.walk line 386
  49. def OAI.HardSphere.Lattice.incrementHistory line 388
  50. theorem OAI.HardSphere.Lattice.aligned_prediction line 390