OAI/Probability/MemoryPrecision/SphericalProjection.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MemoryPrecision.radialShrink line 22
2. def OAI.MemoryPrecision.radialExpand line 25
3. lemma OAI.MemoryPrecision.radialShrink_mem_ball line 28
4. lemma OAI.MemoryPrecision.radialExpand_shrink line 38
5. lemma OAI.MemoryPrecision.radialExpand_differentiableOn line 55
6. lemma OAI.MemoryPrecision.radialShrink_preimage_null line 77
7. lemma OAI.MemoryPrecision.orthogonal_normalized_preimage_null line 93
8. lemma OAI.MemoryPrecision.sphere_projection_ac line 137
9. lemma OAI.MemoryPrecision.sphere_rows_ac line 159
10. theorem OAI.MemoryPrecision.spherical_projection_ac line 210