OAI/Geometry/SmoothYau/SphereMetric/ComplexRealResponse.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.YauCounterexamples.complexRealResponse line 41
2. lemma OAI.YauCounterexamples.complexRealResponse_selected line 44
3. lemma OAI.YauCounterexamples.measurable_complexRealResponse line 55
4. theorem OAI.YauCounterexamples.complex_three_wave_smallBall line 60
5. lemma OAI.YauCounterexamples.complexRealResponse_rotation line 110
6. theorem OAI.YauCounterexamples.complex_three_wave_rotated_smallBall line 120