OAI/Probability/MemoryPrecision/AmbientGram.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MemoryPrecision.Space line 18

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

2. def OAI.MemoryPrecision.J line 20

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

3. def OAI.MemoryPrecision.AmbientBallBound line 27

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

4. def OAI.MemoryPrecision.InverseGram line 31

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

5. lemma OAI.MemoryPrecision.sharp_inverse_unit line 41
6. lemma OAI.MemoryPrecision.ae_pos_of_power_tube line 110
7. lemma OAI.MemoryPrecision.sharp_inverse_scaled line 126
8. lemma OAI.MemoryPrecision.affine_tube_cover_radius line 174
9. lemma OAI.MemoryPrecision.ambient_tube_radius_factors line 231
10. lemma OAI.MemoryPrecision.ambient_tube line 237
11. lemma OAI.MemoryPrecision.ambient_mass_bound line 273
12. lemma OAI.MemoryPrecision.ambient_tube_scaled line 286
13. lemma OAI.MemoryPrecision.ambient_inverse_moment line 308
14. lemma OAI.MemoryPrecision.J_pos line 337
15. lemma OAI.MemoryPrecision.J_mono line 342
16. lemma OAI.MemoryPrecision.ambient_inverse_moment_le line 359
17. lemma OAI.MemoryPrecision.replica_integral_exact line 380
18. lemma OAI.MemoryPrecision.ae_replica_nondegenerate_exact line 416
19. lemma OAI.MemoryPrecision.measurable_joint_replicaWeight line 448
20. lemma OAI.MemoryPrecision.ae_joint_replica_independent line 454
21. lemma OAI.MemoryPrecision.joint_replica_integral_exact line 480
22. lemma OAI.MemoryPrecision.specialized_J_bound line 524
23. lemma OAI.MemoryPrecision.specialized_gram_product_bound line 561
24. def OAI.MemoryPrecision.AmbientGramStatement line 585

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

25. theorem OAI.MemoryPrecision.ambient_gram line 630