OAI/Geometry/BallPacking/Layers/LayerAreaForm.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PackingSufficiencySupport.Hamiltonian.layerHamiltonian line 15
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.layerHamiltonian_smooth line 19
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.scalar_area_slice line 26
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.areaLayerForm_apply line 33
  5. def OAI.PackingSufficiencySupport.Hamiltonian.areaHamiltonianForm line 79
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.areaHamiltonianForm_apply line 90
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.areaHamiltonianForm_layer line 96
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.finite_area_layer_packing line 119
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.normalizedAreaDensity_smooth line 161
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.normalizedAreaDensity_pos line 174
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_normalized_positive_area line 180
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.angularReparam_smoothOn line 207
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.angularReparam_isEmbedding line 212
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.angularReparam_injOn line 229
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.angular_packing_transport line 245
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.finite_weighted_layer_packing line 320
  17. def OAI.PackingSufficiencySupport.Hamiltonian.surfaceRemainder line 376
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceRemainder_smooth line 379
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceRemainder_gap line 386
  20. def OAI.PackingSufficiencySupport.Hamiltonian.surfaceFirstLayer line 394
  21. def OAI.PackingSufficiencySupport.Hamiltonian.surfaceFinalLayer line 397
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceFirstLayer_smooth line 401
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceFinalLayer_smooth line 406
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.first_partial_eq_deriv line 414
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceFirstLayer_firstDerivative line 420
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceFinalLayer_firstDerivative line 426
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceFinalLayer_firstDerivative_nonneg line 443
  28. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceFinalLayer_lower line 454
  29. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceFinalLayer_upper line 459
  30. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceFinalLayer_on_ordered_interval line 471
  31. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_surface_layer_clocks line 498