OAI/Analysis/HotSpots/VectorEnergy.lean

GitHub source file

125 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StrictHotSpots.HasH1Gradient.mul_smooth line 15
  2. def OAI.StrictHotSpots.H1.smoothMul line 73
  3. lemma OAI.StrictHotSpots.H1.smoothMul_value_ae line 76
  4. lemma OAI.StrictHotSpots.H1.smoothMul_grad_ae line 80
  5. lemma OAI.StrictHotSpots.Hodge.rotL_skew line 93
  6. def OAI.StrictHotSpots.Hodge.skewEnergy line 100
  7. lemma OAI.StrictHotSpots.Hodge.skewEnergy_skew line 102
  8. lemma OAI.StrictHotSpots.Hodge.skewEnergy_zero_right line 105
  9. lemma OAI.StrictHotSpots.Hodge.skewEnergy_zero_left line 108
  10. lemma OAI.StrictHotSpots.Hodge.skewEnergy_add_left line 111
  11. lemma OAI.StrictHotSpots.Hodge.skewEnergy_add_right line 114
  12. def OAI.StrictHotSpots.Hodge.boundaryDefect line 121
  13. lemma OAI.StrictHotSpots.Hodge.boundaryDefect_symm line 124
  14. lemma OAI.StrictHotSpots.Hodge.boundaryDefect_zero_right line 129
  15. lemma OAI.StrictHotSpots.Hodge.boundaryDefect_add_right line 135
  16. lemma OAI.StrictHotSpots.Hodge.boundaryDefect_add_left line 141
  17. lemma OAI.StrictHotSpots.Hodge.boundaryDefect_class_right line 145
  18. lemma OAI.StrictHotSpots.Hodge.boundaryDefect_class line 153
  19. lemma OAI.StrictHotSpots.Hodge.skewEnergy_integral line 160
  20. lemma OAI.StrictHotSpots.Hodge.boundaryDefect_integral line 168
  21. lemma OAI.StrictHotSpots.Hodge.defect_multiplier_algebra line 179
  22. lemma OAI.StrictHotSpots.Hodge.defect_multiplier_substitute line 192
  23. theorem OAI.StrictHotSpots.Hodge.boundaryDefect_multiplier line 208
  24. def OAI.StrictHotSpots.Hodge.coordinateL line 243
  25. lemma OAI.StrictHotSpots.Hodge.coordinateL_ae line 245
  26. def OAI.StrictHotSpots.Hodge.axisL line 253
  27. lemma OAI.StrictHotSpots.Hodge.axisL_ae line 255
  28. def OAI.StrictHotSpots.Hodge.partialL line 259
  29. lemma OAI.StrictHotSpots.Hodge.scalar_pair_L2 line 262
  30. lemma OAI.StrictHotSpots.Hodge.partialL_compact_integration_by_parts line 270
  31. lemma OAI.StrictHotSpots.Hodge.partialL_integration_by_parts line 295
  32. def OAI.StrictHotSpots.Hodge.vectorValue line 304
  33. def OAI.StrictHotSpots.Hodge.divergenceL line 306
  34. def OAI.StrictHotSpots.Hodge.curlL line 308
  35. lemma OAI.StrictHotSpots.Hodge.axis_coordinate_pair line 311
  36. lemma OAI.StrictHotSpots.Hodge.coordinateL_rot_zero line 319
  37. lemma OAI.StrictHotSpots.Hodge.coordinateL_rot_one line 326
  38. lemma OAI.StrictHotSpots.Hodge.axis_sum_pair line 333
  39. lemma OAI.StrictHotSpots.Hodge.axis_sum_rot_pair line 338
  40. lemma OAI.StrictHotSpots.Hodge.partialL_test_curl line 343
  41. lemma OAI.StrictHotSpots.Hodge.vectorValue_zero_trace_normal line 355
  42. lemma OAI.StrictHotSpots.Hodge.axis_coordinates line 387
  43. lemma OAI.StrictHotSpots.Hodge.coordinate_pair line 396
  44. lemma OAI.StrictHotSpots.Hodge.coordinate_rot_pair line 401
  45. lemma OAI.StrictHotSpots.Hodge.axis_inner_point line 406
  46. lemma OAI.StrictHotSpots.Hodge.axis_sum_ae line 413
  47. lemma OAI.StrictHotSpots.Hodge.axis_sum_inner line 419
  48. lemma OAI.StrictHotSpots.Hodge.divcurl_pair_algebra line 432
  49. def OAI.StrictHotSpots.Hodge.cartesianEnergy line 440
  50. def OAI.StrictHotSpots.Hodge.vectorForm line 443
  51. def OAI.StrictHotSpots.Hodge.cartesianForm line 447
  52. lemma OAI.StrictHotSpots.Hodge.vectorValue_pair line 451
  53. theorem OAI.StrictHotSpots.Hodge.vectorForm_eq_cartesian_add_defect line 458
  54. def OAI.StrictHotSpots.Hodge.TangentWeak line 477
  55. lemma OAI.StrictHotSpots.Hodge.vectorValue_add line 480
  56. lemma OAI.StrictHotSpots.Hodge.vectorValue_smul line 484
  57. lemma OAI.StrictHotSpots.Hodge.partialL_add line 487
  58. lemma OAI.StrictHotSpots.Hodge.partialL_smul line 489
  59. lemma OAI.StrictHotSpots.Hodge.divergenceL_add line 491
  60. lemma OAI.StrictHotSpots.Hodge.divergenceL_smul line 495
  61. lemma OAI.StrictHotSpots.Hodge.curlL_add line 498
  62. lemma OAI.StrictHotSpots.Hodge.curlL_smul line 501
  63. lemma OAI.StrictHotSpots.Hodge.TangentWeak.add line 504
  64. lemma OAI.StrictHotSpots.Hodge.TangentWeak.smul line 509
  65. lemma OAI.StrictHotSpots.Hodge.tangentWeak_zero_trace line 514
  66. lemma OAI.StrictHotSpots.Hodge.TangentWeak.of_class line 518
  67. lemma OAI.StrictHotSpots.Hodge.vectorForm_symm line 527
  68. lemma OAI.StrictHotSpots.Hodge.vectorForm_add_left line 530
  69. lemma OAI.StrictHotSpots.Hodge.vectorForm_smul_left line 534
  70. lemma OAI.StrictHotSpots.Hodge.vectorForm_add_right line 538
  71. lemma OAI.StrictHotSpots.Hodge.vectorForm_smul_right line 541
  72. theorem OAI.StrictHotSpots.Hodge.vectorForm_nonneg line 546
  73. lemma OAI.StrictHotSpots.Hodge.quadratic_null_pair line 556
  74. theorem OAI.StrictHotSpots.Hodge.vectorForm_null_pair line 573
  75. lemma OAI.StrictHotSpots.Hodge.divergenceL_ae line 594
  76. lemma OAI.StrictHotSpots.Hodge.vectorValue_ae line 599
  77. lemma OAI.StrictHotSpots.Hodge.divergence_multiplier_algebra line 602
  78. lemma OAI.StrictHotSpots.Hodge.vectorValue_smoothMul_ae line 614
  79. lemma OAI.StrictHotSpots.Hodge.divergenceL_smoothMul_ae line 625
  80. lemma OAI.StrictHotSpots.Hodge.normal_pair_integral line 637
  81. lemma OAI.StrictHotSpots.Hodge.normal_multiplier_algebra line 645
  82. lemma OAI.StrictHotSpots.Hodge.normal_pair_smoothMul line 651
  83. theorem OAI.StrictHotSpots.Hodge.TangentWeak.smoothMul line 666
  84. theorem OAI.StrictHotSpots.Hodge.boundaryClass_multiplier_identity line 687
  85. theorem OAI.StrictHotSpots.Hodge.boundaryClass_multiplier_nonneg line 711
  86. lemma OAI.StrictHotSpots.Hodge.scalar_eq_zero_of_H10_pair line 737
  87. lemma OAI.StrictHotSpots.Hodge.vectorValue_test_normal line 743
  88. lemma OAI.StrictHotSpots.Hodge.gradient_curl_zero line 755
  89. def OAI.StrictHotSpots.Hodge.NeumannEuler line 765
  90. lemma OAI.StrictHotSpots.Hodge.inner_add_smul_zero line 768
  91. lemma OAI.StrictHotSpots.Hodge.gradient_divergence line 774
  92. lemma OAI.StrictHotSpots.Hodge.gradient_tangent line 789
  93. lemma OAI.StrictHotSpots.Hodge.gradient_form_algebra line 796
  94. theorem OAI.StrictHotSpots.Hodge.gradient_vector_null line 805
  95. def OAI.StrictHotSpots.Hodge.eigenGradientField line 827
  96. lemma OAI.StrictHotSpots.Hodge.eigenGradientField_value_ae line 832
  97. lemma OAI.StrictHotSpots.Hodge.eigenGradientField_vector line 839
  98. lemma OAI.StrictHotSpots.Hodge.eigen_NeumannEuler line 855
  99. theorem OAI.StrictHotSpots.Hodge.eigenGradientField_null line 874
  100. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.boundarySolution_datum_class line 897
  101. def OAI.StrictHotSpots.Conformal.ClosedDiskChart.datumCorrection line 913
  102. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.datumCorrection_spec line 917
  103. def OAI.StrictHotSpots.Conformal.ClosedDiskChart.physicalSolution line 924
  104. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.physicalSolution_class line 930
  105. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.physicalSolution_grad_pair line 937
  106. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.physicalSolution_mass_pair line 961
  107. theorem OAI.StrictHotSpots.Conformal.ClosedDiskChart.physicalSolution_energy line 998
  108. def OAI.StrictHotSpots.Conformal.ClosedDiskChart.scalarSolution line 1037
  109. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.scalarSolution_class line 1040
  110. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.datumCorrection_eq_zero_of_helmholtz line 1045
  111. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.physicalSolution_eq_of_helmholtz line 1059
  112. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.scalarSolution_eq_of_helmholtz line 1076
  113. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.scalarSolution_energy line 1082
  114. lemma OAI.StrictHotSpots.smoothMul_smooth_closure line 1099
  115. lemma OAI.StrictHotSpots.closed_directional_helmholtz line 1112
  116. lemma OAI.StrictHotSpots.PlaneGreen.harmonic_multiplier_integral line 1134
  117. lemma OAI.StrictHotSpots.PlaneGreen.interaction_multiplier_integral line 1153
  118. lemma OAI.StrictHotSpots.PlaneGreen.multiplier_integrand_integrable line 1189
  119. theorem OAI.StrictHotSpots.PlaneGreen.boundaryForm_multiplier_difference line 1211
  120. def OAI.StrictHotSpots.Conformal.ClosedDiskChart.multipliedGradient line 1272
  121. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.multipliedGradient_class line 1276
  122. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.multipliedGradient_square_class line 1285
  123. theorem OAI.StrictHotSpots.Conformal.ClosedDiskChart.multipliedGradient_identity line 1311
  124. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.multipliedGradient_tangent line 1327
  125. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.multipliedGradient_nonneg line 1333