OAI/Geometry/CubicTorus/Profiles/OctantVertex.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.isMinimizerAt_common_fixed_not_boundary line 13
  2. def OAI.CubicTorus.octantVertex line 37
  3. lemma OAI.CubicTorus.octantVertex_fixed line 40
  4. theorem OAI.CubicTorus.isMinimizerAt_reflection_origin_vertices line 54
  5. def OAI.CubicTorus.closedUpperOctant line 78
  6. def OAI.CubicTorus.octantContract line 80
  7. lemma OAI.CubicTorus.octantContract_apply line 83
  8. lemma OAI.CubicTorus.octantContract_mem line 86
  9. lemma OAI.CubicTorus.octantContract_mono line 94
  10. lemma OAI.CubicTorus.octantContract_tendsto line 104
  11. lemma OAI.CubicTorus.octant_downset_closed_endpoint line 113
  12. lemma OAI.CubicTorus.octant_downset_nonboundary_endpoint line 128
  13. lemma OAI.CubicTorus.LatticeIsometry.openRepresentative_preimage_null line 153
  14. lemma OAI.CubicTorus.reflection_invariant_openRepresentative line 161
  15. def OAI.CubicTorus.octantFlipSet line 170
  16. lemma OAI.CubicTorus.octantFlipSet_empty line 173
  17. lemma OAI.CubicTorus.octantFlipSet_insert line 176
  18. lemma OAI.CubicTorus.octantFlipSet_mem line 187
  19. lemma OAI.CubicTorus.reflection_invariant_fold line 197
  20. lemma OAI.CubicTorus.sibling_isMinimizerAt_openRepresentative_nonempty line 215
  21. def OAI.CubicTorus.upperVertex line 241
  22. def OAI.CubicTorus.orientedUpperVertex line 244
  23. lemma OAI.CubicTorus.upperVertex_mem line 247
  24. lemma OAI.CubicTorus.upperVertex_fixed line 252
  25. lemma OAI.CubicTorus.orientedUpperVertex_min line 265
  26. lemma OAI.CubicTorus.orientedUpperVertex_max line 273
  27. lemma OAI.CubicTorus.orientedUpperVertex_mono line 281
  28. lemma OAI.CubicTorus.isMinimizerAt_closure_openRepresentative_null line 289
  29. theorem OAI.CubicTorus.isMinimizerAt_vertex_order_ideal line 298
  30. lemma OAI.CubicTorus.representative_quotientMap_coordinate line 345
  31. theorem OAI.CubicTorus.isMinimizerAt_nonstandard_strict_octant line 350
  32. lemma OAI.CubicTorus.smooth_periodic_centered_primitive line 431
  33. lemma OAI.CubicTorus.axial_scalar_periodic line 457
  34. lemma OAI.CubicTorus.axial_scalar_fderiv line 462
  35. lemma OAI.CubicTorus.axial_field_tangentialDivergence line 469
  36. lemma OAI.CubicTorus.axial_field_divergence line 478
  37. theorem OAI.CubicTorus.sibling_axial_flux_derivative line 486
  38. def OAI.CubicTorus.axialTransverseMass line 513
  39. lemma OAI.CubicTorus.normal_component_continuous line 516
  40. lemma OAI.CubicTorus.normal_axial_integrable line 520
  41. lemma OAI.CubicTorus.normal_transverse_integrable line 529
  42. theorem OAI.CubicTorus.axial_flux_marginal line 533
  43. theorem OAI.CubicTorus.isMinimizerAt_axial_flux line 557
  44. theorem OAI.CubicTorus.isMinimizerAt_stationary_tubular_normal line 589
  45. lemma OAI.CubicTorus.normalSphere_sum_sq line 642
  46. lemma OAI.CubicTorus.normalSphere_coordinate_sq_le line 647
  47. lemma OAI.CubicTorus.axialTransverseMass_nonneg line 651
  48. lemma OAI.CubicTorus.axialTransverseMass_sum line 655
  49. lemma OAI.CubicTorus.axialTransverseMass_defect line 667
  50. theorem OAI.CubicTorus.isMinimizerAt_nonstandard_axial_mass_lt line 675
  51. def OAI.CubicTorus.circleMollifier line 721
  52. lemma OAI.CubicTorus.circleMollifier_tendsto line 727
  53. def OAI.CubicTorus.circleSmoothApprox line 732
  54. lemma OAI.CubicTorus.circleSmoothApprox_contDiff line 735
  55. lemma OAI.CubicTorus.circleSmoothApprox_periodic line 740
  56. lemma OAI.CubicTorus.circleSmoothApprox_tendsto line 748
  57. lemma OAI.CubicTorus.circleSmoothApprox_bound line 752
  58. lemma OAI.CubicTorus.circleSmoothApprox_integral_tendsto line 764
  59. lemma OAI.CubicTorus.circleSmoothApprox_integral_tendsto_finite line 783
  60. theorem OAI.CubicTorus.axial_flux_marginal_continuous line 791
  61. abbrev OAI.CubicTorus.AxisCircle line 833
  62. def OAI.CubicTorus.axialSurfaceMarginal line 835
  63. def OAI.CubicTorus.axialVolumeMarginal line 841