OAI/Geometry/CubicTorus/Estimates/ConeSlopeReciprocalArea.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.coverC1BoundaryAt_physical_patch line 13
  2. lemma OAI.CubicTorus.tangentialDivergence_neg_normal line 85
  3. lemma OAI.CubicTorus.reverseBlowupNormal_stationary line 89
  4. lemma OAI.CubicTorus.graph_superlevel_compl_ae line 97
  5. theorem OAI.CubicTorus.strict_C1_patch_stationary line 120
  6. lemma OAI.CubicTorus.normalPlaneCoordinates_tangent_graph line 204
  7. lemma OAI.CubicTorus.graph_vertical_variation line 216
  8. lemma OAI.CubicTorus.radialHeightCutoff_eventually_one line 234
  9. theorem OAI.CubicTorus.stationary_graph_weak_equation line 240
  10. lemma OAI.CubicTorus.cover_cone_boundary_smul line 312
  11. theorem OAI.CubicTorus.cone_graph_radial_derivative line 327
  12. lemma OAI.CubicTorus.cone_graph_radial_projection_ne_zero line 364
  13. lemma OAI.CubicTorus.slopeScalarTest_derivative line 388
  14. lemma OAI.CubicTorus.integral_mul_deriv_radial line 423
  15. theorem OAI.CubicTorus.integral_slope_separated line 436
  16. lemma OAI.CubicTorus.continuous_mul_shift_integrable line 486
  17. lemma OAI.CubicTorus.continuous_angular_smoothing_tendsto line 495
  18. theorem OAI.CubicTorus.continuous_constant_of_weak_derivative_zero line 511
  19. theorem OAI.CubicTorus.hasDerivAt_of_continuous_weak_derivative line 540
  20. theorem OAI.CubicTorus.hasDerivAt_of_continuousOn_weak_derivative line 574
  21. theorem OAI.CubicTorus.cone_slope_ODE_derivative line 625
  22. def OAI.CubicTorus.coneSlopeReciprocalArea line 694
  23. def OAI.CubicTorus.coneSlopeFlux line 697
  24. lemma OAI.CubicTorus.coneSlopeReciprocalArea_pos line 700
  25. lemma OAI.CubicTorus.coneSlopeReciprocalArea_metric line 704
  26. lemma OAI.CubicTorus.coneSlopeReciprocalArea_continuousOn line 710
  27. theorem OAI.CubicTorus.weak_cone_slope_derivative line 717
  28. theorem OAI.CubicTorus.weak_cone_slope_affine line 740
  29. def OAI.CubicTorus.slopeHorizontalVector line 773
  30. lemma OAI.CubicTorus.plane_inner_coordinates line 775
  31. lemma OAI.CubicTorus.plane_gradient_coordinates line 781
  32. lemma OAI.CubicTorus.planarWedgeChart_hasDerivAt_radial line 788
  33. lemma OAI.CubicTorus.planarWedgeChart_hasDerivAt_angular line 795
  34. theorem OAI.CubicTorus.euler_graph_homogeneous line 801
  35. lemma OAI.CubicTorus.graph_angular_slice_hasDerivAt line 825
  36. lemma OAI.CubicTorus.planarWedgeChart_expand line 833
  37. theorem OAI.CubicTorus.euler_graph_gradient line 838