OAI/Geometry/BallPacking/SurfaceArea/QuadricSmoothExhaustion.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.projectionDomain_frontier_norm line 15
  2. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.projectionDomain_frontier_regular line 26
  3. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.projectionDomain_smoothBoundary line 36
  4. def OAI.PackingSufficiencySupport.DiagonalQuadrics.exhaustionRadius line 63
  5. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.exhaustionRadius_pos line 66
  6. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.exhaustionRadius_branch line 71
  7. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.exists_actual_smooth_projection_exhaustion line 79
  8. def OAI.PackingSufficiencySupport.DiagonalQuadrics.signFlip line 97
  9. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.signFlip_projection line 104
  10. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.signFlip_continuous line 106
  11. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.signFlip_fixed_branch line 117
  12. def OAI.PackingSufficiencySupport.DiagonalQuadrics.fiberMix line 130
  13. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.fiberMix_empty line 139
  14. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.fiberMix_univ line 146
  15. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.fiberMix_insert line 153
  16. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.signStable_contains_fiber line 175
  17. theorem OAI.PackingSufficiencySupport.component_image_eq_univ line 194
  18. theorem OAI.PackingSufficiencySupport.component_preserved_of_fixed_fiber line 202
  19. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.curveProjection_surjective line 225
  20. def OAI.PackingSufficiencySupport.DiagonalQuadrics.signFlipOver line 230
  21. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.signFlipOver_continuous line 234
  22. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.projection_preimage_preconnected line 240
  23. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.projection_preimage_connected line 274
  24. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.actual_curve_connected line 282
  25. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.projectionDomain_interior line 289
  26. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.sqrt_mem_disk line 299
  27. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.projectionDomain_interior_connected line 306
  28. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.exists_actual_connected_smooth_exhaustion line 312
  29. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.compact_eventually_subset_projectionDomain line 336
  30. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.compact_area_le_degree line 348
  31. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.tendsto_exhaustion_area line 360
  32. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.tendsto_normalized_exhaustion_area line 383
  33. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.general_curveCutoffDefect_end_coefficient line 396
  34. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.curveEndCutoff_variable_residue_partition_mass line 423
  35. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.curveEndCutoff_variable_residue_mass line 477
  36. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.tendsto_curveEndCutoff_variable_residue line 504