OAI/Geometry/SmoothYau/Estimates/ThreeNoncancelNormedSpace.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.YauCounterexamples.complex_coefficient_norm_le line 11
2. lemma OAI.YauCounterexamples.coupled_power_comparison line 19
3. lemma OAI.YauCounterexamples.coupled_power_uniform_bound line 39
4. lemma OAI.YauCounterexamples.productSphere_norm_sq line 83
5. lemma OAI.YauCounterexamples.productA_norm_le line 87
6. lemma OAI.YauCounterexamples.productB_norm_le line 92
7. def OAI.YauCounterexamples.productWeight line 97
8. lemma OAI.YauCounterexamples.productWeight_pos line 99
9. lemma OAI.YauCounterexamples.threeCoupled_direction_norm line 103
10. lemma OAI.YauCounterexamples.product_coefficient_bound line 108
11. lemma OAI.YauCounterexamples.threeCoupled_sprite_bounds line 117
12. lemma OAI.YauCounterexamples.threeCoupled_value_bound line 135
13. theorem OAI.YauCounterexamples.threeCoupled_global_noncancellation line 150