OAI/Geometry/CubicTorus/Profiles/PlanarRadialDownset.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.integral_closedCentralArc line 13
  2. lemma OAI.CubicTorus.integral_scaled_semicircle line 55
  3. theorem OAI.CubicTorus.planarTorusPerimeter_ge_semicircle_calibration line 64
  4. def OAI.CubicTorus.PlanarRadialDownset line 135
  5. def OAI.CubicTorus.planarAxisPoint line 138
  6. lemma OAI.CubicTorus.planarAxisPoint_continuous line 140
  7. lemma OAI.CubicTorus.planar_axis_can_grow line 147
  8. lemma OAI.CubicTorus.axisCircle_norm_le_half line 160
  9. lemma OAI.CubicTorus.axisCircle_norm_coe_small line 163
  10. theorem OAI.CubicTorus.planar_radial_extent line 167
  11. lemma OAI.CubicTorus.axisCircle_exists_centered_rep line 222
  12. def OAI.CubicTorus.planarFirstAxisPoint line 230
  13. lemma OAI.CubicTorus.planar_radial_empty_fiber line 232
  14. theorem OAI.CubicTorus.planar_radial_calibration line 256
  15. theorem OAI.CubicTorus.planar_radial_isoperimetric line 270
  16. def OAI.CubicTorus.planarQuotient line 301
  17. lemma OAI.CubicTorus.planarQuotient_representative line 303
  18. lemma OAI.CubicTorus.planarQuotient_add line 308
  19. lemma OAI.CubicTorus.planarQuotient_neg line 312
  20. lemma OAI.CubicTorus.planar_same_quotient_lattice line 317
  21. lemma OAI.CubicTorus.planeDivergence_translate line 331
  22. lemma OAI.CubicTorus.planeDivergence_periodic line 335
  23. lemma OAI.CubicTorus.planarAdmissibleField_translate line 342
  24. lemma OAI.CubicTorus.planar_flux_translation line 349
  25. lemma OAI.CubicTorus.planarTorusPerimeter_translation_le line 367
  26. theorem OAI.CubicTorus.planarTorusPerimeter_translation line 378
  27. lemma OAI.CubicTorus.axisCircle_norm_add_half line 401
  28. def OAI.CubicTorus.axialSectionCenter line 414
  29. def OAI.CubicTorus.centeredAxialSlice line 417
  30. lemma OAI.CubicTorus.upperFold_centered_slice line 420
  31. lemma OAI.CubicTorus.centeredAxialSlice_isOpen line 430
  32. lemma OAI.CubicTorus.centeredAxialSlice_closure_subset line 434
  33. theorem OAI.CubicTorus.isMinimizerAt_centered_section_radial line 441
  34. def OAI.CubicTorus.planarSquareCorner line 478
  35. lemma OAI.CubicTorus.centered_section_corner line 481
  36. lemma OAI.CubicTorus.centered_section_zero line 498
  37. lemma OAI.CubicTorus.centered_section_first_axis line 504
  38. lemma OAI.CubicTorus.centered_section_second_axis line 511
  39. lemma OAI.CubicTorus.centeredAxialSlice_volume line 518
  40. lemma OAI.CubicTorus.centeredAxialSlice_perimeter line 524
  41. theorem OAI.CubicTorus.isMinimizerAt_section_disk_perimeter line 528
  42. lemma OAI.CubicTorus.planar_descended_divergence_continuous line 571
  43. lemma OAI.CubicTorus.planar_integral_divergence_zero line 582
  44. lemma OAI.CubicTorus.planarAdmissibleField_neg line 597
  45. lemma OAI.CubicTorus.planeDivergence_neg line 603
  46. lemma OAI.CubicTorus.planar_integral_divergence_compl line 608
  47. theorem OAI.CubicTorus.planarTorusPerimeter_compl line 617
  48. lemma OAI.CubicTorus.planarTorusPerimeter_congr_ae line 632
  49. lemma OAI.CubicTorus.isMinimizerAt_complement_octant_downset line 653
  50. lemma OAI.CubicTorus.axialSectionCorner_reverse line 673
  51. lemma OAI.CubicTorus.openRepresentative_compl_eq line 682
  52. lemma OAI.CubicTorus.closure_openRepresentative_compl_eq line 688
  53. lemma OAI.CubicTorus.axialSlice_openRepresentative_compl_ae line 695
  54. lemma OAI.CubicTorus.axialSlice_complement_volume line 717
  55. lemma OAI.CubicTorus.axialSlice_complement_perimeter line 730
  56. theorem OAI.CubicTorus.isMinimizerAt_section_extent_perimeter line 750
  57. theorem OAI.CubicTorus.isMinimizerAt_section_complement_calibration line 795