OAI/Geometry/Immersion/ClosedSurface/OscillatoryModel.lean

GitHub source file

129 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ClosedSurfaceR4.SmallModes.Base line 11
  2. abbrev OAI.ClosedSurfaceR4.SmallModes.Ambient line 12
  3. abbrev OAI.ClosedSurfaceR4.SmallModes.Field line 13
  4. abbrev OAI.ClosedSurfaceR4.SmallModes.Scalar line 14
  5. def OAI.ClosedSurfaceR4.SmallModes.dx line 16
  6. def OAI.ClosedSurfaceR4.SmallModes.dy line 17
  7. def OAI.ClosedSurfaceR4.SmallModes.coordDeriv line 19
  8. lemma OAI.ClosedSurfaceR4.SmallModes.partial_add line 22
  9. lemma OAI.ClosedSurfaceR4.SmallModes.partial_sub line 28
  10. lemma OAI.ClosedSurfaceR4.SmallModes.partial_dot line 34
  11. lemma OAI.ClosedSurfaceR4.SmallModes.partial_smul line 52
  12. def OAI.ClosedSurfaceR4.SmallModes.metric line 61
  13. def OAI.ClosedSurfaceR4.SmallModes.linearizedMetric line 65
  14. lemma OAI.ClosedSurfaceR4.SmallModes.metric_add line 68
  15. def OAI.ClosedSurfaceR4.SmallModes.gramDet line 79
  16. def OAI.ClosedSurfaceR4.SmallModes.liftX line 81
  17. def OAI.ClosedSurfaceR4.SmallModes.liftY line 84
  18. def OAI.ClosedSurfaceR4.SmallModes.tangentLift line 88
  19. lemma OAI.ClosedSurfaceR4.SmallModes.dot_tangentLift_left line 91
  20. lemma OAI.ClosedSurfaceR4.SmallModes.dot_tangentLift_right line 98
  21. def OAI.ClosedSurfaceR4.SmallModes.normalPart line 107
  22. lemma OAI.ClosedSurfaceR4.SmallModes.dot_normalPart_left line 110
  23. lemma OAI.ClosedSurfaceR4.SmallModes.dot_normalPart_right line 114
  24. lemma OAI.ClosedSurfaceR4.SmallModes.second_dot_split line 118
  25. lemma OAI.ClosedSurfaceR4.SmallModes.dot_normal_tangentLift line 124
  26. lemma OAI.ClosedSurfaceR4.SmallModes.normalPart_dot_reconstruct line 129
  27. lemma OAI.ClosedSurfaceR4.SmallModes.contDiff_coordDeriv line 140
  28. lemma OAI.ClosedSurfaceR4.SmallModes.second_coordDeriv line 144
  29. lemma OAI.ClosedSurfaceR4.SmallModes.second_coordDeriv_comm line 152
  30. def OAI.ClosedSurfaceR4.SmallModes.secondForm line 162
  31. def OAI.ClosedSurfaceR4.SmallModes.connectionX line 165
  32. def OAI.ClosedSurfaceR4.SmallModes.connectionY line 170
  33. def OAI.ClosedSurfaceR4.SmallModes.covector line 175
  34. lemma OAI.ClosedSurfaceR4.SmallModes.linearizedMetric_covector line 177
  35. lemma OAI.ClosedSurfaceR4.SmallModes.linearizedMetric_connection line 189
  36. lemma OAI.ClosedSurfaceR4.SmallModes.covector_reconstruct line 201
  37. def OAI.ClosedSurfaceR4.SmallModes.unitMode line 215
  38. def OAI.ClosedSurfaceR4.SmallModes.oscillate line 218
  39. lemma OAI.ClosedSurfaceR4.SmallModes.unitMode_hasFDerivAt line 220
  40. lemma OAI.ClosedSurfaceR4.SmallModes.coordDeriv_unitMode line 227
  41. lemma OAI.ClosedSurfaceR4.SmallModes.coordDeriv_oscillate line 233
  42. def OAI.ClosedSurfaceR4.SmallModes.conjugatedMetric line 243
  43. lemma OAI.ClosedSurfaceR4.SmallModes.linearizedMetric_oscillate line 247
  44. lemma OAI.ClosedSurfaceR4.SmallModes.conjugatedMetric_connection line 256
  45. def OAI.ClosedSurfaceR4.SmallModes.reconstruct line 274
  46. def OAI.ClosedSurfaceR4.SmallModes.connectionTerm line 277
  47. lemma OAI.ClosedSurfaceR4.SmallModes.covector_reconstruct_eventually line 280
  48. lemma OAI.ClosedSurfaceR4.SmallModes.secondForm_dot_reconstruct line 292
  49. lemma OAI.ClosedSurfaceR4.SmallModes.conjugatedMetric_reconstruct_xx line 297
  50. lemma OAI.ClosedSurfaceR4.SmallModes.conjugatedMetric_reconstruct_xy line 313
  51. lemma OAI.ClosedSurfaceR4.SmallModes.conjugatedMetric_reconstruct_yy line 329
  52. def OAI.ClosedSurfaceR4.SmallModes.goodSecond line 346
  53. def OAI.ClosedSurfaceR4.SmallModes.secondRatio line 348
  54. def OAI.ClosedSurfaceR4.SmallModes.normalElimination line 352
  55. lemma OAI.ClosedSurfaceR4.SmallModes.dot_normalElimination line 356
  56. lemma OAI.ClosedSurfaceR4.SmallModes.dot_normalElimination_yy line 363
  57. lemma OAI.ClosedSurfaceR4.SmallModes.normalElimination_perp line 373
  58. lemma OAI.ClosedSurfaceR4.SmallModes.normalElimination_perp_eventually line 383
  59. def OAI.ClosedSurfaceR4.SmallModes.reducedLx line 397
  60. def OAI.ClosedSurfaceR4.SmallModes.reducedLy line 401
  61. def OAI.ClosedSurfaceR4.SmallModes.reducedKx line 406
  62. def OAI.ClosedSurfaceR4.SmallModes.reducedKy line 409
  63. theorem OAI.ClosedSurfaceR4.SmallModes.normalElimination_residual line 414
  64. def OAI.ClosedSurfaceR4.SmallModes.firstCovectorX line 448
  65. def OAI.ClosedSurfaceR4.SmallModes.firstCovectorY line 451
  66. def OAI.ClosedSurfaceR4.SmallModes.firstParametrix line 454
  67. lemma OAI.ClosedSurfaceR4.SmallModes.conjugating_inverse line 459
  68. lemma OAI.ClosedSurfaceR4.SmallModes.firstParametrix_residual line 464
  69. lemma OAI.ClosedSurfaceR4.SmallModes.contDiffAt_dot line 491
  70. lemma OAI.ClosedSurfaceR4.SmallModes.contDiffAt_cdiv line 497
  71. lemma OAI.ClosedSurfaceR4.SmallModes.contDiffAt_coordDeriv line 503
  72. lemma OAI.ClosedSurfaceR4.SmallModes.contDiffAt_gramDet line 508
  73. lemma OAI.ClosedSurfaceR4.SmallModes.contDiffAt_liftX line 513
  74. lemma OAI.ClosedSurfaceR4.SmallModes.contDiffAt_liftY line 521
  75. lemma OAI.ClosedSurfaceR4.SmallModes.contDiffAt_tangentLift line 529
  76. lemma OAI.ClosedSurfaceR4.SmallModes.contDiffAt_normalPart line 536
  77. lemma OAI.ClosedSurfaceR4.SmallModes.contDiffAt_secondForm line 542
  78. lemma OAI.ClosedSurfaceR4.SmallModes.contDiffAt_connectionX line 549
  79. lemma OAI.ClosedSurfaceR4.SmallModes.contDiffAt_connectionY line 558
  80. lemma OAI.ClosedSurfaceR4.SmallModes.contDiffAt_connectionTerm line 567
  81. lemma OAI.ClosedSurfaceR4.SmallModes.contDiffAt_secondRatio line 573
  82. lemma OAI.ClosedSurfaceR4.SmallModes.contDiffAt_reconstruct line 582
  83. lemma OAI.ClosedSurfaceR4.SmallModes.contDiffAt_normalElimination line 589
  84. lemma OAI.ClosedSurfaceR4.SmallModes.contDiffAt_reducedKx line 600
  85. lemma OAI.ClosedSurfaceR4.SmallModes.contDiffAt_reducedKy line 609
  86. lemma OAI.ClosedSurfaceR4.SmallModes.contDiffAt_firstParametrix line 618
  87. lemma OAI.ClosedSurfaceR4.SmallModes.partial_const_mul line 637
  88. lemma OAI.ClosedSurfaceR4.SmallModes.tangentLift_mul line 643
  89. lemma OAI.ClosedSurfaceR4.SmallModes.connectionTerm_mul line 653
  90. lemma OAI.ClosedSurfaceR4.SmallModes.reducedLx_mul line 659
  91. lemma OAI.ClosedSurfaceR4.SmallModes.reducedLy_mul line 666
  92. lemma OAI.ClosedSurfaceR4.SmallModes.conjugatedMetric_sub line 674
  93. lemma OAI.ClosedSurfaceR4.SmallModes.contDiffAt_conjugatedMetric line 683
  94. abbrev OAI.ClosedSurfaceR4.SmallModes.Tensor line 695
  95. def OAI.ClosedSurfaceR4.SmallModes.tensorOf line 697
  96. def OAI.ClosedSurfaceR4.SmallModes.component line 699
  97. def OAI.ClosedSurfaceR4.SmallModes.conjugatedD line 701
  98. def OAI.ClosedSurfaceR4.SmallModes.initialAmplitude line 705
  99. def OAI.ClosedSurfaceR4.SmallModes.zeroParametrix line 708
  100. def OAI.ClosedSurfaceR4.SmallModes.residual line 711
  101. def OAI.ClosedSurfaceR4.SmallModes.modeApprox line 716
  102. lemma OAI.ClosedSurfaceR4.SmallModes.contDiffAt_initialAmplitude line 721
  103. lemma OAI.ClosedSurfaceR4.SmallModes.contDiffAt_zeroParametrix line 729
  104. lemma OAI.ClosedSurfaceR4.SmallModes.contDiffAt_conjugatedD line 736
  105. lemma OAI.ClosedSurfaceR4.SmallModes.contDiffAt_residual line 746
  106. lemma OAI.ClosedSurfaceR4.SmallModes.contDiffAt_modeApprox line 751
  107. lemma OAI.ClosedSurfaceR4.SmallModes.conjugatedD_sub line 760
  108. theorem OAI.ClosedSurfaceR4.SmallModes.residual_modeApprox_succ line 767
  109. def OAI.ClosedSurfaceR4.SmallModes.errorGenerator line 782
  110. lemma OAI.ClosedSurfaceR4.SmallModes.contDiffAt_reducedLx line 787
  111. lemma OAI.ClosedSurfaceR4.SmallModes.contDiffAt_reducedLy line 796
  112. lemma OAI.ClosedSurfaceR4.SmallModes.contDiffAt_errorGenerator line 806
  113. theorem OAI.ClosedSurfaceR4.SmallModes.residual_initialAmplitude line 822
  114. lemma OAI.ClosedSurfaceR4.SmallModes.reducedKx_zero_mul line 855
  115. lemma OAI.ClosedSurfaceR4.SmallModes.reducedKy_zero_mul line 862
  116. lemma OAI.ClosedSurfaceR4.SmallModes.errorGenerator_zero_mul line 869
  117. lemma OAI.ClosedSurfaceR4.SmallModes.reducedLx_congr line 891
  118. lemma OAI.ClosedSurfaceR4.SmallModes.reducedLy_congr line 897
  119. lemma OAI.ClosedSurfaceR4.SmallModes.errorGenerator_congr line 904
  120. def OAI.ClosedSurfaceR4.SmallModes.errorHierarchy line 919
  121. lemma OAI.ClosedSurfaceR4.SmallModes.contDiffAt_errorHierarchy line 923
  122. theorem OAI.ClosedSurfaceR4.SmallModes.residual_modeApprox_power line 936
  123. def OAI.ClosedSurfaceR4.SmallModes.freeCorrection line 994
  124. lemma OAI.ClosedSurfaceR4.SmallModes.initialAmplitude_free line 1001
  125. lemma OAI.ClosedSurfaceR4.SmallModes.initialAmplitude_congr line 1017
  126. lemma OAI.ClosedSurfaceR4.SmallModes.initialAmplitude_zero line 1032
  127. lemma OAI.ClosedSurfaceR4.SmallModes.conjugatedD_congr line 1039
  128. lemma OAI.ClosedSurfaceR4.SmallModes.conjugatedD_zero line 1044
  129. theorem OAI.ClosedSurfaceR4.SmallModes.modeApprox_vanishes line 1054