OAI/Geometry/SmoothYau/Spectrum/SphereProjection.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.YauCounterexamples.sphereFrame line 27
  2. lemma OAI.YauCounterexamples.sphereFrame_orthogonal line 31
  3. lemma OAI.YauCounterexamples.sphere_chart_symm line 42
  4. lemma OAI.YauCounterexamples.sphere_chart_center line 51
  5. lemma OAI.YauCounterexamples.sphere_chart_target line 61
  6. lemma OAI.YauCounterexamples.sphere_coordinate_embedding line 65
  7. def OAI.YauCounterexamples.sphericalRadius line 96
  8. lemma OAI.YauCounterexamples.sphericalRadius_nonneg line 99
  9. lemma OAI.YauCounterexamples.sphericalRadius_sq line 102
  10. lemma OAI.YauCounterexamples.sphericalRadius_continuous line 107
  11. lemma OAI.YauCounterexamples.orthogonal_pair_sq_le line 111
  12. lemma OAI.YauCounterexamples.sphericalRadius_le_one line 122
  13. lemma OAI.YauCounterexamples.sphere_chart_source line 130
  14. abbrev OAI.YauCounterexamples.sourceAxisOne line 135
  15. abbrev OAI.YauCounterexamples.sourceAxisTwo line 136
  16. lemma OAI.YauCounterexamples.source_axes_orthonormal line 138
  17. def OAI.YauCounterexamples.sourcePole line 142
  18. lemma OAI.YauCounterexamples.sphericalRadius_neg_sourcePole line 144
  19. def OAI.YauCounterexamples.sourceSignPoint line 148
  20. lemma OAI.YauCounterexamples.sphericalRadius_sourceSignPoint line 159
  21. lemma OAI.YauCounterexamples.sphericalRadius_sublevel_in_source line 170
  22. def OAI.YauCounterexamples.sphericalCoverage line 181
  23. lemma OAI.YauCounterexamples.sphericalCoverage_compact line 184
  24. lemma OAI.YauCounterexamples.mem_sphericalCoverage_iff line 192
  25. lemma OAI.YauCounterexamples.sphericalCoverage_mono line 204
  26. lemma OAI.YauCounterexamples.sphere_chart_symm_continuous line 208
  27. lemma OAI.YauCounterexamples.sphericalCoverage_subset_open line 212
  28. lemma OAI.YauCounterexamples.sphericalCoverage_open line 219
  29. def OAI.YauCounterexamples.sphereProjection line 255
  30. lemma OAI.YauCounterexamples.sphereProjection_orthogonal line 258
  31. def OAI.YauCounterexamples.sphereCoordinates line 263
  32. lemma OAI.YauCounterexamples.sphereFrame_coordinates line 267
  33. lemma OAI.YauCounterexamples.sphereCoordinates_inner line 275
  34. lemma OAI.YauCounterexamples.sphereFrame_inner line 282
  35. lemma OAI.YauCounterexamples.sphere_inverse_gram_contraction line 289
  36. def OAI.YauCounterexamples.planarLinear line 299
  37. lemma OAI.YauCounterexamples.planarLinear_apply line 302
  38. lemma OAI.YauCounterexamples.planarLinear_apply_flip line 305
  39. lemma OAI.YauCounterexamples.complex_bilinear_expand line 310
  40. theorem OAI.YauCounterexamples.sphere_planar_contraction line 316