OAI/Geometry/CubicTorus/Regularity/BVColumnHeight.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicTorus.normalColumnHeight line 15
  2. lemma OAI.CubicTorus.measurable_normalColumnHeight line 19
  3. lemma OAI.CubicTorus.normalColumn_integrable line 28
  4. lemma OAI.CubicTorus.normalColumnHeight_bound line 38
  5. lemma OAI.CubicTorus.trapped_frontier_torus_height line 52
  6. theorem OAI.CubicTorus.normalColumnHeight_eq_good_height line 69
  7. theorem OAI.CubicTorus.normalColumnHeight_disagreement_volume_le line 121
  8. theorem OAI.CubicTorus.normalColumnHeight_graph_L1_le line 157
  9. def OAI.CubicTorus.normalScalarTest line 215
  10. lemma OAI.CubicTorus.normalScalarTest_contDiff line 218
  11. lemma OAI.CubicTorus.normalRotation_single_succ line 224
  12. lemma OAI.CubicTorus.normalScalarTest_normal_line line 234
  13. lemma OAI.CubicTorus.normalScalarTest_plane_line line 243
  14. theorem OAI.CubicTorus.laplacian_normalScalarTest line 253
  15. lemma OAI.CubicTorus.fderiv_normalScalarTest_normal line 281
  16. lemma OAI.CubicTorus.normalScalarTest_tsupport line 300
  17. lemma OAI.CubicTorus.normalScalarTest_tsupport_ball line 313
  18. def OAI.CubicTorus.normalColumnChart line 345
  19. lemma OAI.CubicTorus.normalColumnChart_apply line 349
  20. lemma OAI.CubicTorus.normalColumnChart_measurePreserving line 356
  21. lemma OAI.CubicTorus.integral_normalColumnChart line 366
  22. lemma OAI.CubicTorus.normalColumnChart_height line 374
  23. lemma OAI.CubicTorus.normalColumnChart_projection line 380
  24. lemma OAI.CubicTorus.normalColumnChart_characteristic line 386
  25. lemma OAI.CubicTorus.normalColumnChart_ball line 392
  26. lemma OAI.CubicTorus.normalColumnChart_line_isometry line 412
  27. lemma OAI.CubicTorus.normalColumnChart_plane_isometry line 421
  28. lemma OAI.CubicTorus.halfspace_directional_integrable line 432
  29. lemma OAI.CubicTorus.integral_halfspace_normal_derivative line 440
  30. lemma OAI.CubicTorus.integral_halfspace_tangent_derivative line 468
  31. lemma OAI.CubicTorus.integral_halfspace_directional_derivative line 503
  32. theorem OAI.CubicTorus.integral_halfspace_divergence line 520
  33. def OAI.CubicTorus.normalMove line 567
  34. def OAI.CubicTorus.normalJacobian line 569
  35. def OAI.CubicTorus.normalPullback line 572
  36. lemma OAI.CubicTorus.normalMove_hasFDerivAt line 576
  37. lemma OAI.CubicTorus.normalMove_contDiff line 582
  38. lemma OAI.CubicTorus.normalPullback_contDiff line 585
  39. lemma OAI.CubicTorus.divergence_comp_normalMove line 593
  40. theorem OAI.CubicTorus.normalPullback_divergence line 611
  41. def OAI.CubicTorus.graphHeightExtension line 663
  42. def OAI.CubicTorus.graphShear line 666
  43. lemma OAI.CubicTorus.graphShear_projection line 669
  44. lemma OAI.CubicTorus.graphShear_inverse line 675
  45. lemma OAI.CubicTorus.graphShear_continuous line 683
  46. def OAI.CubicTorus.graphShearHomeomorph line 689
  47. lemma OAI.CubicTorus.graphShear_columnChart line 700
  48. lemma OAI.CubicTorus.columnShear_measurePreserving line 709
  49. lemma OAI.CubicTorus.graphShear_measurePreserving line 721
  50. lemma OAI.CubicTorus.graphHeightExtension_contDiff line 733
  51. lemma OAI.CubicTorus.graphHeightExtension_fderiv line 737
  52. lemma OAI.CubicTorus.graphHeightExtension_normal line 745
  53. lemma OAI.CubicTorus.graphShear_jacobian line 751
  54. def OAI.CubicTorus.graphSublevelIndicator line 768
  55. def OAI.CubicTorus.graphAreaVector line 771
  56. lemma OAI.CubicTorus.graphSublevelIndicator_shear line 774
  57. lemma OAI.CubicTorus.normalPullback_graph_compactSupport line 785
  58. lemma OAI.CubicTorus.graphAreaVector_pullback line 800
  59. lemma OAI.CubicTorus.graphSublevel_flux_integrable line 819
  60. theorem OAI.CubicTorus.integral_graphSublevel_divergence line 832