OAI/Geometry/CubicTorus/Curvature/SurfaceJacobiLocalization.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.complex_eq_norm_smul_unitAngle line 13
  2. lemma OAI.CubicTorus.quotientMap_transverse_square line 20
  3. lemma OAI.CubicTorus.norm_le_unitSquareScale_of_gauge line 40
  4. theorem OAI.CubicTorus.TrueRadialTube.boundary_range line 52
  5. lemma OAI.CubicTorus.pair_periodic_descend line 86
  6. lemma OAI.CubicTorus.transverse_square_quotient_injective line 105
  7. lemma OAI.CubicTorus.radial_point_gauge_lt line 129
  8. lemma OAI.CubicTorus.unitAngle_eq_iff_addCircle line 137
  9. theorem OAI.CubicTorus.TrueRadialTube.homeomorphic_torus line 160
  10. theorem OAI.CubicTorus.isMinimizerAt_first_transition_nonstandard_torus line 224
  11. lemma OAI.CubicTorus.congruentAE_of_coordinatePermute line 248
  12. lemma OAI.CubicTorus.smallStandardRegion_of_coordinatePermute line 270
  13. lemma OAI.CubicTorus.smallStandardRegion_of_translated line 278
  14. theorem OAI.CubicTorus.isMinimizerAt_first_transition_nonstandard_toroidal_reduction line 286
  15. def OAI.CubicTorus.surfaceCutoffError line 313
  16. lemma OAI.CubicTorus.surfaceCutoffError_ae line 318
  17. theorem OAI.CubicTorus.surfaceJacobiB_cutoff_identity line 332
  18. theorem OAI.CubicTorus.surfaceH1_jacobi_cutoff_energy line 380
  19. theorem OAI.CubicTorus.surfaceH1_jacobi_caccioppoli line 402
  20. theorem OAI.CubicTorus.surfaceJacobiB_cutoff_commutator line 438
  21. theorem OAI.CubicTorus.surfaceH1_jacobi_cutoff_commutator line 484
  22. theorem OAI.CubicTorus.exists_periodic_local_identity line 506
  23. theorem OAI.CubicTorus.TrueRadialTube.uniform_square_gap line 532
  24. theorem OAI.CubicTorus.TrueRadialTube.periodic_transverse_germs line 560
  25. def OAI.CubicTorus.periodicCoordinate line 571
  26. lemma OAI.CubicTorus.periodicCoordinate_germ line 578
  27. theorem OAI.CubicTorus.TrueRadialTube.ambient_transverse_germs line 593
  28. lemma OAI.CubicTorus.periodicCoordinate_cross_derivative line 628
  29. def OAI.CubicTorus.periodicRotation line 639
  30. lemma OAI.CubicTorus.periodicRotation_contDiff line 644
  31. lemma OAI.CubicTorus.periodicRotation_periodic line 650
  32. lemma OAI.CubicTorus.periodicRotation_divergence line 656
  33. theorem OAI.CubicTorus.periodicRotation_normal_flux_zero line 667
  34. def OAI.CubicTorus.periodicRotationNormalScalar line 678
  35. theorem OAI.CubicTorus.periodicRotationNormalScalar_mean_zero line 688
  36. theorem OAI.CubicTorus.TrueRadialTube.periodic_rotation_germs line 701
  37. def OAI.CubicTorus.normalTangentRotation line 740
  38. lemma OAI.CubicTorus.normalTangentRotation_orthogonal line 743
  39. lemma OAI.CubicTorus.tangent_shape_cross line 749
  40. lemma OAI.CubicTorus.tangentialDivergence_sub_fields line 768
  41. lemma OAI.CubicTorus.normalTangentRotation_divergence line 778
  42. theorem OAI.CubicTorus.isMinimizerAt_normalTangentRotation_divergence line 796