OAI/Geometry/BallPacking/Moser/AnnularFinalPacking.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.exists_global_surface_final_packing line 15
  2. def OAI.PackingSufficiencySupport.Hamiltonian.baseFiberMoment line 133
  3. def OAI.PackingSufficiencySupport.Hamiltonian.baseFiberInner line 136
  4. def OAI.PackingSufficiencySupport.Hamiltonian.baseFiberOuter line 139
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.baseFiber_bounds line 142
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.baseFiber_domain line 148
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.baseFiberMoment_smooth line 162
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_base_moser_cutoff line 173
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.horizontalModel_exterior_vertical line 193
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothOneFormFamily.parameter_contDiffAt line 215
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.productHorizontalLift_exterior_vertical line 229
  12. theorem OAI.PackingSufficiencySupport.constant_above_of_deriv_eq_zero line 298
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.CompactHamiltonianIsotopy.integral_constant_on_collar line 334
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.CompactHamiltonianIsotopy.preserves_integral_on_collar line 344
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.CompactHamiltonianIsotopy.inverse_preserves_integral_on_collar line 353
  16. def OAI.PackingSufficiencySupport.Hamiltonian.autonomousField line 364
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.autonomousField_contraction line 367
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.intertwines_autonomousField line 377
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.homeomorph_fderiv_inverse line 409
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.CompactHamiltonianIsotopy.inverse_symplectic line 419
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.CompactHamiltonianIsotopy.intertwines_on_collar line 433
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.CompactHamiltonianIsotopy.inverse_intertwines_on_collar line 444
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.hamiltonian_invariant_of_commutes line 457
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.invariant_pullback_on_collar line 466
  25. def OAI.PackingSufficiencySupport.Hamiltonian.CollarInvariant line 488
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.CollarInvariant.const line 491
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.CollarInvariant.add line 495
  28. theorem OAI.PackingSufficiencySupport.Hamiltonian.CollarInvariant.sub line 502
  29. theorem OAI.PackingSufficiencySupport.Hamiltonian.CollarInvariant.smul line 509
  30. theorem OAI.PackingSufficiencySupport.Hamiltonian.CollarInvariant.const_mul line 517
  31. theorem OAI.PackingSufficiencySupport.Hamiltonian.CollarInvariant.sum line 520
  32. theorem OAI.PackingSufficiencySupport.Hamiltonian.CollarInvariant.pullback line 530
  33. theorem OAI.PackingSufficiencySupport.Hamiltonian.CollarInvariant.inverse_pullback line 541
  34. theorem OAI.PackingSufficiencySupport.Hamiltonian.CompactHamiltonianIsotopy.hamiltonian_collarInvariant line 553
  35. theorem OAI.PackingSufficiencySupport.Hamiltonian.toric_collarInvariant line 566
  36. theorem OAI.PackingSufficiencySupport.Hamiltonian.globalHorizontalCoupling_face line 583
  37. theorem OAI.PackingSufficiencySupport.Hamiltonian.productCouplingPrimitive_vertical_value line 605
  38. theorem OAI.PackingSufficiencySupport.Hamiltonian.productCouplingPrimitive_face line 612
  39. theorem OAI.PackingSufficiencySupport.Hamiltonian.isInvertible_of_chartTwoForm line 637
  40. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldTwoForm_isOpen_nondegenerate line 656
  41. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldTwoForm_isOpen_nondegenerate_times line 687
  42. theorem OAI.PackingSufficiencySupport.Hamiltonian.productCouplingPrimitive_stationary line 709
  43. def OAI.PackingSufficiencySupport.Hamiltonian.baseFiberField line 718
  44. theorem OAI.PackingSufficiencySupport.Hamiltonian.productCouplingPrimitive_baseFiber_face line 725
  45. theorem OAI.PackingSufficiencySupport.Hamiltonian.horizontal_sublevel_moser line 747