OAI/Probability/SKGap/Localization/CubeWeight.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGapCutoff.cubeWeight line 11
2. def OAI.SKGapCutoff.deletedWeight line 14
3. def OAI.SKGapCutoff.cubeExtension line 17
4. lemma OAI.SKGapCutoff.cubeWeight_sum line 20
5. lemma OAI.SKGapCutoff.cubeWeight_nonneg line 31
6. lemma OAI.SKGapCutoff.cubeWeight_vertex line 41
7. lemma OAI.SKGapCutoff.cubeExtension_vertex line 54
8. lemma OAI.SKGapCutoff.deletedWeight_flip line 59
9. lemma OAI.SKGapCutoff.cubeWeight_factor line 67
10. lemma OAI.SKGapCutoff.cubeWeight_flip_add line 71
11. lemma OAI.SKGapCutoff.cubeWeight_halfDiff line 77
12. lemma OAI.SKGapCutoff.cubeExtension_line_deriv line 107
13. lemma OAI.SKGapCutoff.weighted_mean_sq_le line 139
14. lemma OAI.SKGapCutoff.cubeExtension_gradient_sq_le line 157
15. lemma OAI.SKGapCutoff.spin_segment_mem line 175
16. lemma OAI.SKGapCutoff.spin_vertex_distance_sq line 182
17. lemma OAI.SKGapCutoff.cubeExtension_direction_bound line 192
18. theorem OAI.SKGapCutoff.euclidean_oscillation line 209