OAI/Geometry/CubicTorus/Regularity/GradientCalibration.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.cutoff_integration_by_parts line 15
  2. def OAI.CubicTorus.gradientCalibration line 32
  3. lemma OAI.CubicTorus.gradientCalibration_admissible line 35
  4. lemma OAI.CubicTorus.inner_gradientCalibration line 55
  5. theorem OAI.CubicTorus.integral_norm_gradient_le line 66
  6. lemma OAI.CubicTorus.characteristic_nonneg line 123
  7. lemma OAI.CubicTorus.smoothApprox_characteristic_range line 126
  8. lemma OAI.CubicTorus.characteristic_lift_periodic line 136
  9. lemma OAI.CubicTorus.torusApprox_eq_integral line 141
  10. theorem OAI.CubicTorus.smoothApprox_flux_le line 147
  11. theorem OAI.CubicTorus.smoothApprox_gradient_bound line 213
  12. lemma OAI.CubicTorus.integrableOn_characteristic_mul line 231
  13. lemma OAI.CubicTorus.gradient_const_sub line 238
  14. lemma OAI.CubicTorus.characteristic_union line 242
  15. lemma OAI.CubicTorus.cutoff_union_flux_le line 248
  16. theorem OAI.CubicTorus.perimeter_union_le_of_measurable line 316
  17. theorem OAI.CubicTorus.perimeter_union_le line 370
  18. theorem OAI.CubicTorus.perimeter_diff_le line 383
  19. theorem OAI.CubicTorus.FinitePerimeter.union line 390
  20. theorem OAI.CubicTorus.FinitePerimeter.diff line 394
  21. lemma OAI.CubicTorus.smoothApprox_flux_tendsto line 404
  22. lemma OAI.CubicTorus.smooth_flux_le_gradient line 425
  23. theorem OAI.CubicTorus.smoothApprox_gradient_tendsto line 441
  24. abbrev OAI.CubicTorus.NormalSphere line 474
  25. instance OAI.CubicTorus.(instance at line 476) line 476
  26. abbrev OAI.CubicTorus.NormalBundle line 491
  27. def OAI.CubicTorus.normalizedVector line 493
  28. lemma OAI.CubicTorus.normalizedVector_norm line 496
  29. lemma OAI.CubicTorus.measurable_normalizedVector line 503
  30. def OAI.CubicTorus.unitNormal line 507
  31. lemma OAI.CubicTorus.measurable_unitNormal line 509
  32. lemma OAI.CubicTorus.norm_smul_normalizedVector line 511
  33. def OAI.CubicTorus.smoothNormalMap line 517
  34. lemma OAI.CubicTorus.measurable_smoothNormalMap line 520
  35. def OAI.CubicTorus.smoothNormalMeasure line 525
  36. lemma OAI.CubicTorus.integral_smoothNormalMeasure line 533
  37. lemma OAI.CubicTorus.smoothNormalMeasure_mass line 544
  38. def OAI.CubicTorus.normalTest line 552
  39. lemma OAI.CubicTorus.smoothNormalMeasure_flux line 557
  40. theorem OAI.CubicTorus.exists_normalMeasure line 577
  41. def OAI.CubicTorus.IsNormalMeasure line 628
  42. lemma OAI.CubicTorus.normalMeasure_flux line 634
  43. def OAI.CubicTorus.coordinateMove line 664
  44. def OAI.CubicTorus.coordinateMoveDeriv line 667
  45. def OAI.CubicTorus.coordinateJacobian line 671
  46. lemma OAI.CubicTorus.coordinateMove_contDiff line 674
  47. lemma OAI.CubicTorus.coordinateMove_hasFDerivAt line 680
  48. lemma OAI.CubicTorus.coordinateMove_periodic line 694
  49. lemma OAI.CubicTorus.coordinateMove_apply line 700
  50. lemma OAI.CubicTorus.coordinateMoveDeriv_det line 704
  51. lemma OAI.CubicTorus.coordinateMove_injective line 721
  52. lemma OAI.CubicTorus.divergence_sub_fields line 751
  53. lemma OAI.CubicTorus.linearForm_apply_basis line 758
  54. lemma OAI.CubicTorus.divergence_comp_coordinateMove line 766
  55. def OAI.CubicTorus.coordinatePullback line 787
  56. lemma OAI.CubicTorus.coordinateJacobian_contDiff line 792
  57. lemma OAI.CubicTorus.coordinatePullback_contDiff line 799
  58. lemma OAI.CubicTorus.coordinatePullback_periodic line 810
  59. lemma OAI.CubicTorus.coordinatePullback_divergence line 817
  60. lemma OAI.CubicTorus.coordinateJacobian_norm_le line 867
  61. lemma OAI.CubicTorus.coordinateJacobian_pos line 879