OAI/Geometry/SmoothYau/Estimates/LocalizedPacketSignProbability.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.YauCounterexamples.maskComplex line 16
2. lemma OAI.YauCounterexamples.complexValueVector_norm_le_sum line 19
3. lemma OAI.YauCounterexamples.complexValueVector_component_le line 28
4. lemma OAI.YauCounterexamples.maskComplex_far_error line 35
5. lemma OAI.YauCounterexamples.maskComplex_norm_ge line 47
6. lemma OAI.YauCounterexamples.masked_endpoint_vector_error line 53
7. lemma OAI.YauCounterexamples.masked_rotated_norm line 77
8. theorem OAI.YauCounterexamples.finite_near_far_sign_probability line 86
9. lemma OAI.YauCounterexamples.finite_packet_variance_lower line 147
10. lemma OAI.YauCounterexamples.finite_packet_standardized_mean line 174
11. theorem OAI.YauCounterexamples.localized_packet_sign_probability line 189