OAI/Geometry/CubicTorus/Variation/ComponentDivergence.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.Periodic.simultaneousCofactor_second_deriv line 15
  2. theorem OAI.CubicTorus.Periodic.simultaneousArea_second_deriv line 46
  3. def OAI.CubicTorus.Periodic.componentDivergence line 69
  4. lemma OAI.CubicTorus.Periodic.componentDivergence_smooth line 72
  5. def OAI.CubicTorus.Periodic.massJet line 75
  6. lemma OAI.CubicTorus.Periodic.massJet_append line 80
  7. lemma OAI.CubicTorus.Periodic.massJet_first line 87
  8. lemma OAI.CubicTorus.Periodic.simultaneousJacobian_append line 95
  9. lemma OAI.CubicTorus.Periodic.simultaneousJacobian_deriv line 102
  10. lemma OAI.CubicTorus.Periodic.simultaneousJacobian_second_deriv line 114
  11. lemma OAI.CubicTorus.Periodic.simultaneousMass_second_deriv line 141
  12. theorem OAI.CubicTorus.Periodic.exists_chain_of_field line 162
  13. theorem OAI.CubicTorus.Periodic.isMinimizerAt_stable_fields line 190
  14. def OAI.CubicTorus.Periodic.chainQuadratic line 229
  15. theorem OAI.CubicTorus.Periodic.isMinimizerAt_expanded_stability line 235
  16. def OAI.CubicTorus.coverTrace line 276
  17. lemma OAI.CubicTorus.cover_decompose line 279
  18. lemma OAI.CubicTorus.cover_clm_component line 283
  19. lemma OAI.CubicTorus.coverTrace_zero line 290
  20. lemma OAI.CubicTorus.coverTrace_add line 291
  21. lemma OAI.CubicTorus.coverTrace_smul line 293
  22. def OAI.CubicTorus.coverTraceCLM line 296
  23. lemma OAI.CubicTorus.coverTraceCLM_apply line 301
  24. lemma OAI.CubicTorus.coverTrace_comp_comm line 303
  25. lemma OAI.CubicTorus.coverTrace_smulRight line 315
  26. lemma OAI.CubicTorus.divergence_eq_coverTrace line 324
  27. def OAI.CubicTorus.cofactorLinear line 327
  28. def OAI.CubicTorus.cofactorQuadratic line 330
  29. lemma OAI.CubicTorus.cofactorLinear_add line 334
  30. lemma OAI.CubicTorus.cofactorQuadratic_add line 339
  31. theorem OAI.CubicTorus.isMinimizerAt_halfspace_L1_tilt_small line 359
  32. theorem OAI.CubicTorus.isMinimizerAt_halfspace_L1_normal_charts line 407
  33. lemma OAI.CubicTorus.localL1_eventually_lt_model line 467
  34. theorem OAI.CubicTorus.isMinimizerAt_close_limit_fixed_scale_graphs line 486
  35. theorem OAI.CubicTorus.isMinimizerAt_close_limit_fixed_scale_normals line 589
  36. lemma OAI.CubicTorus.ae_closedBall_imp_of_ae_ball line 625
  37. lemma OAI.CubicTorus.localL1_limit_congr_ae_ball line 637
  38. lemma OAI.CubicTorus.volume_real_affine_preimage_ball line 650
  39. def OAI.CubicTorus.ActualBoundaryGraph line 681
  40. theorem OAI.CubicTorus.actual_primary_fixed_scale_packets line 691
  41. lemma OAI.CubicTorus.exists_uniform_subseq_of_bounded_modulus line 801
  42. def OAI.CubicTorus.normalGraphDerivative line 826
  43. lemma OAI.CubicTorus.transverse_inner_lower line 829
  44. lemma OAI.CubicTorus.normalGraphDerivative_continuousOn line 837
  45. def OAI.CubicTorus.rescaledActualBoundary line 858