OAI/Probability/MemoryPrecision/CubeGeometry.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MemoryPrecision.CubeSet line 18

    Also declared: ComparatorChallenges/MemoryPrecision.lean:354 (same declaration text).

  2. abbrev OAI.MemoryPrecision.Cube line 31

    Also declared: ComparatorChallenges/MemoryPrecision.lean:368 (same declaration text).

  3. def OAI.MemoryPrecision.CubeLaw line 32

    Also declared: ComparatorChallenges/MemoryPrecision.lean:370 (same declaration text).

  4. lemma OAI.MemoryPrecision.cube_second_coordinate_lt line 34

    Also declared: ComparatorChallenges/MemoryPrecision.lean:373 (same declaration text).

  5. def OAI.MemoryPrecision.cubeRaw line 38

    Also declared: ComparatorChallenges/MemoryPrecision.lean:377 (same declaration text).

  6. def OAI.MemoryPrecision.CubeEmbedding line 51

    Also declared: ComparatorChallenges/MemoryPrecision.lean:391 (same declaration text).

  7. def OAI.MemoryPrecision.CubeBall line 52

    Also declared: ComparatorChallenges/MemoryPrecision.lean:393 (same declaration text).

  8. def OAI.MemoryPrecision.CubeLocal line 54

    Also declared: ComparatorChallenges/MemoryPrecision.lean:396 (same declaration text).

  9. lemma OAI.MemoryPrecision.cubeSet_closed line 69
  10. lemma OAI.MemoryPrecision.cubeSet_measurable line 74
  11. lemma OAI.MemoryPrecision.cubeLaw_probability line 77
  12. instance OAI.MemoryPrecision.(instance at line 90) line 90
  13. lemma OAI.MemoryPrecision.cubeBall_measurable line 92
  14. lemma OAI.MemoryPrecision.cubeRaw_continuous line 95
  15. lemma OAI.MemoryPrecision.cubeEmbedding_continuous line 104
  16. lemma OAI.MemoryPrecision.cubeEmbedding_measurable line 107
  17. lemma OAI.MemoryPrecision.sum_fin_split line 110

    Also declared: ComparatorChallenges/MemoryPrecision.lean:417 (same declaration text).

  18. def OAI.MemoryPrecision.cubeCoords line 118

    Also declared: ComparatorChallenges/MemoryPrecision.lean:425 (same declaration text).

  19. lemma OAI.MemoryPrecision.cubeCoords_first line 130

    Also declared: ComparatorChallenges/MemoryPrecision.lean:437 (same declaration text).

  20. lemma OAI.MemoryPrecision.cubeCoords_second line 134

    Also declared: ComparatorChallenges/MemoryPrecision.lean:441 (same declaration text).

  21. lemma OAI.MemoryPrecision.cubeCoords_tail line 138

    Also declared: ComparatorChallenges/MemoryPrecision.lean:445 (same declaration text).

  22. lemma OAI.MemoryPrecision.cubeCoords_sum line 142

    Also declared: ComparatorChallenges/MemoryPrecision.lean:449 (same declaration text).

  23. lemma OAI.MemoryPrecision.cube_coordinate_square_le line 158

    Also declared: ComparatorChallenges/MemoryPrecision.lean:413 (same declaration text).

  24. lemma OAI.MemoryPrecision.cubeEmbedding_norm line 162

    Also declared: ComparatorChallenges/MemoryPrecision.lean:465 (same declaration text).

  25. lemma OAI.MemoryPrecision.sqrt_pair_lipschitz line 182
  26. lemma OAI.MemoryPrecision.cubeCoords_sub_norm line 202
  27. lemma OAI.MemoryPrecision.cubeEmbedding_dist line 229
  28. def OAI.MemoryPrecision.cubeProject line 241
  29. lemma OAI.MemoryPrecision.cubeProject_continuous line 244
  30. lemma OAI.MemoryPrecision.cubeProject_norm line 248
  31. lemma OAI.MemoryPrecision.cubeProject_sub line 256
  32. lemma OAI.MemoryPrecision.cubeProject_embedding line 260
  33. lemma OAI.MemoryPrecision.cubeProject_parameter_dist line 265