OAI/Geometry/BallPacking/Annuli/AnnularMean.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PackingSufficiencySupport.Hamiltonian.annularMean line 14
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.annularMean_smooth line 17
  3. def OAI.PackingSufficiencySupport.Hamiltonian.annularNormalized line 28
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.annularNormalized_smooth line 31
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.annularNormalized_fderiv_radial line 40
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.annularNormalized_zero_period line 62
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.annularNormalized_periodic line 79
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_smooth_local_identity line 98
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.contDiffOn_fixed_integral line 127
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.hasFDerivAt_fixed_integral line 144
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.hasFDerivAt_fixed_integral_on line 174
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.hasFDerivAt_interval_integral line 204
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.hasFDerivAt_interval_integral_local line 230
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.hasDerivAt_interval_integral_local line 258
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.hasDerivAt_primitive_on line 273
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.stripPrimitive_hasDerivAt_second line 290
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.stripPrimitive_hasDerivAt_first line 301
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.stripPrimitive_fderiv line 337
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.strip_period_eq line 364
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.stripPrimitive_periodic line 386
  21. def OAI.PackingSufficiencySupport.Hamiltonian.normalizedAnnularPrimitive line 412
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.annular_normalization line 416
  23. def OAI.PackingSufficiencySupport.Hamiltonian.annularScalarDescent line 466
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.annularScalarDescent_turn line 470
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.annularScalarDescent_smoothOn line 475
  26. def OAI.PackingSufficiencySupport.Hamiltonian.parameterAnnulusCover line 489
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.parameterAnnulusCover_smooth line 492
  28. theorem OAI.PackingSufficiencySupport.Hamiltonian.annularScalarDescent_pullback line 499
  29. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_normalized_annular_scalar line 526