OAI/Geometry/CubicTorus/Estimates/CorrectedChain.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.isMinimizerAt_chain_stability line 13
  2. def OAI.CubicTorus.Periodic.correctedChain line 56
  3. def OAI.CubicTorus.Periodic.correctedChainArea line 59
  4. lemma OAI.CubicTorus.Periodic.correctedChainCofactor_smooth line 63
  5. lemma OAI.CubicTorus.Periodic.correctedChainArea_smoothAt line 72
  6. lemma OAI.CubicTorus.Periodic.correctedChainArea_zero line 79
  7. theorem OAI.CubicTorus.Periodic.isMinimizerAt_chain_stability line 88
  8. lemma OAI.CubicTorus.hasDerivAt_norm_curve line 133
  9. lemma OAI.CubicTorus.second_derivative_norm_curve line 140
  10. lemma OAI.CubicTorus.deriv_parameter_slice line 176
  11. lemma OAI.CubicTorus.second_deriv_parameter_slice line 183
  12. lemma OAI.CubicTorus.second_deriv_compact_parameter_integral line 190
  13. theorem OAI.CubicTorus.normalArea_second_derivative line 214
  14. lemma OAI.CubicTorus.deriv_smooth line 280
  15. lemma OAI.CubicTorus.deriv_smooth_add line 283
  16. lemma OAI.CubicTorus.deriv_smooth_smul line 289
  17. lemma OAI.CubicTorus.second_deriv_zero_smul line 296
  18. lemma OAI.CubicTorus.correction_second_derivative line 305
  19. lemma OAI.CubicTorus.normalArea_second_zero_correction line 340
  20. def OAI.CubicTorus.Periodic.normalFirstVariation line 411
  21. theorem OAI.CubicTorus.Periodic.isMinimizerAt_chain_second_variation line 414
  22. theorem OAI.CubicTorus.Periodic.isMinimizerAt_exists_stable_weakCMC line 459
  23. theorem OAI.CubicTorus.normalArea_first_derivative line 493
  24. lemma OAI.CubicTorus.Periodic.simultaneousMass_single line 556
  25. lemma OAI.CubicTorus.Periodic.correctedSingleCofactor_deriv line 562
  26. lemma OAI.CubicTorus.Periodic.correctedSingleArea_deriv line 586
  27. theorem OAI.CubicTorus.Periodic.isMinimizerAt_mixed_stationary line 604
  28. theorem OAI.CubicTorus.Periodic.isMinimizerAt_exists_coordinate_multiplier line 637
  29. theorem OAI.CubicTorus.Periodic.isMinimizerAt_stable_periodic line 647
  30. theorem OAI.CubicTorus.Periodic.tangent_firstVariation_of_coordinate line 677
  31. theorem OAI.CubicTorus.Periodic.weakCMC_identity line 696
  32. lemma OAI.CubicTorus.deriv_id_smul_zero line 724
  33. lemma OAI.CubicTorus.second_deriv_id_smul_zero line 729
  34. lemma OAI.CubicTorus.deriv_add_time_smul line 739
  35. def OAI.CubicTorus.Periodic.chainVelocity line 748
  36. def OAI.CubicTorus.Periodic.chainNormalVelocity line 751
  37. def OAI.CubicTorus.Periodic.chainFlux line 754
  38. lemma OAI.CubicTorus.Periodic.simultaneousMass_append line 757
  39. lemma OAI.CubicTorus.Periodic.simultaneousMass_deriv line 763
  40. lemma OAI.CubicTorus.Periodic.simultaneousMove_deriv line 776
  41. lemma OAI.CubicTorus.Periodic.simultaneousCofactor_deriv line 791
  42. lemma OAI.CubicTorus.second_deriv_add_time_smul line 825
  43. def OAI.CubicTorus.Periodic.normalJet line 837
  44. lemma OAI.CubicTorus.Periodic.normalJet_append line 844
  45. lemma OAI.CubicTorus.Periodic.normalJet_first line 853