OAI/Geometry/BallPacking/BallMaps/QuadricRelativeShellFlow.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.exists_quadric_relative_shell_map line 15
  2. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.mixedHopf_affine_pullback line 102
  3. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.mixedHopf_affine line 141
  4. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.exists_quadric_global_affine_moser line 148
  5. def OAI.PackingSufficiencySupport.DiagonalQuadrics.affinePhaseEquiv line 231
  6. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.affinePhaseEquiv_apply line 234
  7. def OAI.PackingSufficiencySupport.DiagonalQuadrics.affineRadialTarget line 239
  8. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.affineRadialTarget_smooth line 242
  9. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.affineRadialTarget_isEmbedding line 246
  10. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.affineRadialTarget_mem line 251
  11. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.affineRadialTarget_pullback line 257
  12. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.exists_polynomial_target_embedding line 270
  13. def OAI.PackingSufficiencySupport.Hamiltonian.headComplexAmbient line 297
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.headComplexAmbient_apply line 310
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.headComplexAmbient_capacity line 313
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.headComplexAmbient_form line 319
  17. def OAI.PackingSufficiencySupport.Hamiltonian.phasePlusPlaneAmbient line 326
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.phasePlusPlaneAmbient_capacity line 329
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.phasePlusPlaneAmbient_form line 334
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.phasePlusPlaneAmbient_first line 341
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.phasePlusPlanePrimitive_exterior line 347
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.firstDiskRadial_mem_unit line 368
  23. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.exists_quadric_exact_affine_moser line 390
  24. def OAI.PackingSufficiencySupport.DiagonalQuadrics.affineLinePhase line 413
  25. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.affineLinePhase_primitive line 416
  26. def OAI.PackingSufficiencySupport.DiagonalQuadrics.affineLineRadial line 429
  27. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.affineLineRadial_smoothOn line 432
  28. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.affineLineRadial_primitive line 436
  29. def OAI.PackingSufficiencySupport.DiagonalQuadrics.affineLineTarget line 456
  30. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.affineLineTarget_smoothOn line 459
  31. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.affineLineTarget_isEmbedding line 463
  32. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.affineLineTarget_mem line 476
  33. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.affineLineTarget_first line 482
  34. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.affineLineTarget_pullback line 486
  35. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.exists_polynomial_first_line_target line 504