OAI/Geometry/CubicTorus/Estimates/ChainMass.lean

GitHub source file

87 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.chainPullback_contDiff line 13
  2. lemma OAI.CubicTorus.chainPullback_periodic line 19
  3. lemma OAI.CubicTorus.chainPullback_norm line 26
  4. lemma OAI.CubicTorus.chainPullback_divergence line 35
  5. lemma OAI.CubicTorus.chain_inner_pullback line 45
  6. lemma OAI.CubicTorus.chainRegion_measurable line 54
  7. lemma OAI.CubicTorus.chainRegion_finite line 64
  8. lemma OAI.CubicTorus.integral_chainRegion line 75
  9. lemma OAI.CubicTorus.wallVelocity_contDiff line 101
  10. lemma OAI.CubicTorus.chainCofactor_contDiff line 107
  11. lemma OAI.CubicTorus.chainCofactor_continuous_normal line 119
  12. theorem OAI.CubicTorus.perimeter_chainRegion_le_normalArea line 124
  13. lemma OAI.CubicTorus.chainMove_append line 147
  14. lemma OAI.CubicTorus.chainJacobian_append line 153
  15. lemma OAI.CubicTorus.chainCofactor_append line 161
  16. lemma OAI.CubicTorus.chainRegion_append line 167
  17. lemma OAI.CubicTorus.ChainValid.append line 173
  18. def OAI.CubicTorus.chainMass line 180
  19. lemma OAI.CubicTorus.volume_chainRegion line 183
  20. def OAI.CubicTorus.chainTransportedFlux line 191
  21. lemma OAI.CubicTorus.integrableOn_fundamentalCube_of_continuous line 195
  22. lemma OAI.CubicTorus.chainMass_append line 200
  23. lemma OAI.CubicTorus.Periodic.wallVelocity_contDiff line 228
  24. lemma OAI.CubicTorus.Periodic.chainCofactor_contDiff line 234
  25. lemma OAI.CubicTorus.Periodic.chainCofactor_continuous_normal line 246
  26. theorem OAI.CubicTorus.Periodic.perimeter_chainRegion_le_normalArea line 251
  27. lemma OAI.CubicTorus.Periodic.chainMove_append line 274
  28. lemma OAI.CubicTorus.Periodic.chainJacobian_append line 280
  29. lemma OAI.CubicTorus.Periodic.chainCofactor_append line 288
  30. lemma OAI.CubicTorus.Periodic.chainRegion_append line 294
  31. lemma OAI.CubicTorus.Periodic.ChainValid.append line 300
  32. def OAI.CubicTorus.Periodic.chainMass line 307
  33. lemma OAI.CubicTorus.Periodic.volume_chainRegion line 310
  34. def OAI.CubicTorus.Periodic.chainTransportedFlux line 318
  35. lemma OAI.CubicTorus.Periodic.chainMass_append line 322
  36. def OAI.CubicTorus.Periodic.simultaneousChain line 351
  37. lemma OAI.CubicTorus.Periodic.simultaneousMove_smooth line 353
  38. lemma OAI.CubicTorus.Periodic.simultaneousJacobian_smooth line 363
  39. lemma OAI.CubicTorus.Periodic.simultaneousCofactor_smooth line 376
  40. lemma OAI.CubicTorus.Periodic.simultaneousMove_zero line 389
  41. lemma OAI.CubicTorus.Periodic.simultaneousJacobian_zero line 395
  42. lemma OAI.CubicTorus.Periodic.simultaneousCofactor_zero line 401
  43. lemma OAI.CubicTorus.Periodic.simultaneousChain_eventually_valid line 407
  44. lemma OAI.CubicTorus.Periodic.simultaneousMass_zero line 421
  45. lemma OAI.CubicTorus.Periodic.simultaneousFlux_zero line 426
  46. def OAI.CubicTorus.simultaneousChain line 443
  47. lemma OAI.CubicTorus.simultaneousMove_smooth line 445
  48. lemma OAI.CubicTorus.simultaneousJacobian_smooth line 455
  49. lemma OAI.CubicTorus.simultaneousCofactor_smooth line 468
  50. lemma OAI.CubicTorus.simultaneousMove_zero line 481
  51. lemma OAI.CubicTorus.simultaneousJacobian_zero line 487
  52. lemma OAI.CubicTorus.simultaneousCofactor_zero line 493
  53. lemma OAI.CubicTorus.simultaneousChain_eventually_valid line 499
  54. lemma OAI.CubicTorus.simultaneousMass_zero line 513
  55. lemma OAI.CubicTorus.simultaneousFlux_zero line 518
  56. lemma OAI.CubicTorus.integrable_of_continuous_compact_carrier line 539
  57. lemma OAI.CubicTorus.hasDerivAt_compact_parameter_integral line 546
  58. theorem OAI.CubicTorus.contDiff_compact_parameter_integral line 566
  59. lemma OAI.CubicTorus.cubeIntersection_compact_carrier line 601
  60. lemma OAI.CubicTorus.simultaneousMass_smooth line 608
  61. lemma OAI.CubicTorus.simultaneousFlux_smooth line 613
  62. lemma OAI.CubicTorus.smooth_quotient_extension line 621
  63. def OAI.CubicTorus.chainCorrection line 643
  64. lemma OAI.CubicTorus.chainCorrection_zero line 646
  65. lemma OAI.CubicTorus.chainCorrection_eventually_exact line 650
  66. lemma OAI.CubicTorus.Periodic.simultaneousMass_smooth line 687
  67. lemma OAI.CubicTorus.Periodic.simultaneousFlux_smooth line 692
  68. def OAI.CubicTorus.Periodic.chainCorrection line 700
  69. lemma OAI.CubicTorus.Periodic.chainCorrection_zero line 703
  70. lemma OAI.CubicTorus.Periodic.chainCorrection_eventually_exact line 707
  71. def OAI.CubicTorus.normSmoothingBump line 744
  72. def OAI.CubicTorus.smoothNormalLength line 746
  73. lemma OAI.CubicTorus.smoothNormalLength_smooth line 749
  74. lemma OAI.CubicTorus.smoothNormalLength_eq line 760
  75. def OAI.CubicTorus.normalEmbedding line 767
  76. lemma OAI.CubicTorus.normalEmbedding_continuous line 769
  77. def OAI.CubicTorus.normalCarrier line 772
  78. lemma OAI.CubicTorus.normalCarrier_compact line 774
  79. lemma OAI.CubicTorus.normalEmbedding_mem line 777
  80. lemma OAI.CubicTorus.normalMap_ae_carrier line 780
  81. theorem OAI.CubicTorus.normalArea_smoothAt line 786
  82. lemma OAI.CubicTorus.second_derivative_nonneg_of_local_min line 824
  83. def OAI.CubicTorus.correctedChain line 836
  84. def OAI.CubicTorus.correctedChainArea line 839
  85. lemma OAI.CubicTorus.correctedChainCofactor_smooth line 843
  86. lemma OAI.CubicTorus.correctedChainArea_smoothAt line 852
  87. lemma OAI.CubicTorus.correctedChainArea_zero line 859