OAI/Geometry/CubicTorus/Estimates/ChainAcceleration.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.volumeQuadratic_smulRight line 13
  2. lemma OAI.CubicTorus.normal_jet_acceleration_step line 24
  3. lemma OAI.CubicTorus.mass_jet_acceleration_step line 33
  4. lemma OAI.CubicTorus.divergence_smooth line 41
  5. lemma OAI.CubicTorus.divergence_derivative line 46
  6. def OAI.CubicTorus.Periodic.chainAcceleration line 68
  7. lemma OAI.CubicTorus.Periodic.chainAcceleration_smooth line 70
  8. lemma OAI.CubicTorus.Periodic.chainAcceleration_periodic line 73
  9. lemma OAI.CubicTorus.Periodic.chainAcceleration_append line 77
  10. lemma OAI.CubicTorus.Periodic.chainAcceleration_derivative_append line 83
  11. lemma OAI.CubicTorus.Periodic.variation_normal_derivative line 100
  12. lemma OAI.CubicTorus.Periodic.variation_cofactor_quadratic line 110
  13. theorem OAI.CubicTorus.Periodic.normalJet_second line 116
  14. lemma OAI.CubicTorus.Periodic.componentDivergence_eq line 134
  15. lemma OAI.CubicTorus.Periodic.variation_volume_quadratic line 138
  16. lemma OAI.CubicTorus.Periodic.massJet_divergence line 144
  17. theorem OAI.CubicTorus.Periodic.massJet_second line 158
  18. def OAI.CubicTorus.ambientAreaQuadratic line 189
  19. def OAI.CubicTorus.ambientQuadratic line 192
  20. lemma OAI.CubicTorus.volumeQuadratic_continuous line 197
  21. lemma OAI.CubicTorus.cofactorQuadratic_continuous line 201
  22. lemma OAI.CubicTorus.ambientAreaQuadratic_continuous line 211
  23. lemma OAI.CubicTorus.ambientAreaQuadratic_integrable line 218
  24. lemma OAI.CubicTorus.cube_integrable_continuous line 226
  25. lemma OAI.CubicTorus.periodic_normal_flux line 231
  26. lemma OAI.CubicTorus.Periodic.chainQuadratic_eq_ambient line 254
  27. theorem OAI.CubicTorus.Periodic.isMinimizerAt_ambient_stability line 295
  28. def OAI.CubicTorus.volumeCorrection line 326
  29. lemma OAI.CubicTorus.volumeCorrection_smooth line 329
  30. lemma OAI.CubicTorus.volumeCorrection_periodic line 334
  31. lemma OAI.CubicTorus.divergence_volumeCorrection line 339
  32. lemma OAI.CubicTorus.volumeQuadratic_boundary line 357
  33. def OAI.CubicTorus.ambientBoundaryQuadratic line 365
  34. lemma OAI.CubicTorus.ambientQuadratic_boundary line 368
  35. theorem OAI.CubicTorus.Periodic.isMinimizerAt_boundary_stability line 395
  36. lemma OAI.CubicTorus.adjoint_smulRight_unit line 425
  37. lemma OAI.CubicTorus.inner_adjoint_one line 434
  38. lemma OAI.CubicTorus.coverTrace_normal_square line 439
  39. lemma OAI.CubicTorus.ambientAreaQuadratic_formula line 459
  40. theorem OAI.CubicTorus.normal_hessian_algebra line 472
  41. lemma OAI.CubicTorus.smooth_unit_normal_derivative line 508
  42. lemma OAI.CubicTorus.adjoint_fderiv_one line 526
  43. theorem OAI.CubicTorus.normal_variation_hessian line 532
  44. lemma OAI.CubicTorus.surface_gradient_norm line 549
  45. def OAI.CubicTorus.normalExtensionJacobi line 568
  46. lemma OAI.CubicTorus.ambientBoundaryQuadratic_zero_of_notMem_tsupport line 573
  47. lemma OAI.CubicTorus.boundaryQuadratic_eq_normalExtension line 581
  48. theorem OAI.CubicTorus.Periodic.isMinimizerAt_normal_extension_stability line 603
  49. lemma OAI.CubicTorus.divergence_contDiff_top line 644
  50. lemma OAI.CubicTorus.tangentialDivergence_scalar_normal line 648
  51. theorem OAI.CubicTorus.weakCMC_normal_extension line 664
  52. theorem OAI.CubicTorus.Periodic.isMinimizerAt_normal_CMC_stability line 732
  53. def OAI.CubicTorus.regularizedNormal line 778
  54. lemma OAI.CubicTorus.regularizedNormal_denom_pos line 781
  55. lemma OAI.CubicTorus.regularizedNormal_contDiff line 788
  56. lemma OAI.CubicTorus.regularizedNormal_eq line 798
  57. lemma OAI.CubicTorus.regularizedNormal_unit_near line 804
  58. lemma OAI.CubicTorus.regularizedNormal_periodic line 817
  59. theorem OAI.CubicTorus.finite_normal_patch_gluing line 823