OAI/Analysis/HotSpots/Hodge.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StrictHotSpots.H1.norm_value_sq line 14
  2. lemma OAI.StrictHotSpots.H1.norm_grad_sq line 19
  3. lemma OAI.StrictHotSpots.H1.rayleigh line 25
  4. def OAI.StrictHotSpots.H1.one line 36
  5. lemma OAI.StrictHotSpots.H1.one_ae line 41
  6. lemma OAI.StrictHotSpots.H1.mean_apply line 45
  7. def OAI.StrictHotSpots.meanZeroSubmodule line 51
  8. abbrev OAI.StrictHotSpots.N1 line 54
  9. instance OAI.StrictHotSpots.N1.normedAddCommGroup line 56
  10. instance OAI.StrictHotSpots.N1.innerProductSpace line 59
  11. instance OAI.StrictHotSpots.N1.completeSpace line 62
  12. def OAI.StrictHotSpots.N1.value line 70
  13. def OAI.StrictHotSpots.N1.grad line 73
  14. lemma OAI.StrictHotSpots.N1.norm_sq line 76
  15. lemma OAI.StrictHotSpots.N1.mean_zero line 79
  16. lemma OAI.StrictHotSpots.N1.rayleigh line 84
  17. def OAI.StrictHotSpots.N1.energy line 88
  18. lemma OAI.StrictHotSpots.N1.energy_apply line 97
  19. lemma OAI.StrictHotSpots.N1.energy_coercive line 100
  20. lemma OAI.StrictHotSpots.N1.existsUnique_energy_solution line 118
  21. lemma OAI.StrictHotSpots.Hodge.weakCurl_gradient line 141
  22. abbrev OAI.StrictHotSpots.Hodge.V2 line 157
  23. def OAI.StrictHotSpots.Hodge.rotL line 158
  24. lemma OAI.StrictHotSpots.Hodge.rotL_ae line 159
  25. lemma OAI.StrictHotSpots.Hodge.rotL_inner line 161
  26. lemma OAI.StrictHotSpots.Hodge.rotL_norm line 166
  27. lemma OAI.StrictHotSpots.Hodge.weakCurl_iff line 171
  28. lemma OAI.StrictHotSpots.Hodge.grad_rotGrad_orthogonal line 199
  29. lemma OAI.StrictHotSpots.Hodge.exists_meanZero_same_grad line 203
  30. def OAI.StrictHotSpots.Hodge.nFunctional line 242
  31. lemma OAI.StrictHotSpots.Hodge.nFunctional_apply line 244
  32. lemma OAI.StrictHotSpots.Hodge.nProjection line 247
  33. lemma OAI.StrictHotSpots.Hodge.nProjection_extend line 253
  34. lemma OAI.StrictHotSpots.Hodge.neumann_projection line 260
  35. def OAI.StrictHotSpots.Hodge.jFunctional line 265
  36. lemma OAI.StrictHotSpots.Hodge.jProjection line 267
  37. lemma OAI.StrictHotSpots.Hodge.dirichlet_projection line 273
  38. def OAI.StrictHotSpots.Hodge.residual line 291
  39. lemma OAI.StrictHotSpots.Hodge.inner_sub_sub_normal_zero line 295
  40. lemma OAI.StrictHotSpots.Hodge.residual_normal line 302
  41. lemma OAI.StrictHotSpots.Hodge.inner_sub_sub_zero line 311
  42. lemma OAI.StrictHotSpots.Hodge.residual_curl line 316
  43. lemma OAI.StrictHotSpots.Hodge.orthogonal_all_zero line 324
  44. lemma OAI.StrictHotSpots.Hodge.sub_sub_zero_iff line 340
  45. lemma OAI.StrictHotSpots.Hodge.residual_zero_iff line 343
  46. lemma OAI.StrictHotSpots.Hodge.norm_add_orthogonal line 348
  47. lemma OAI.StrictHotSpots.Hodge.decomposition_norm line 353
  48. lemma OAI.StrictHotSpots.Hodge.projection_eq line 370
  49. lemma OAI.StrictHotSpots.Hodge.projection_eq_exists line 380
  50. theorem OAI.StrictHotSpots.Hodge.decomposition line 389
  51. lemma OAI.StrictHotSpots.Hodge.scalar_energy_bound line 405
  52. lemma OAI.StrictHotSpots.Hodge.scalar_rayleigh_eq line 419
  53. def OAI.StrictHotSpots.Hodge.WeakNormalDiv line 432
  54. def OAI.StrictHotSpots.Hodge.WeakCurl line 435
  55. lemma OAI.StrictHotSpots.Hodge.pair_add_orthogonal_left line 439
  56. lemma OAI.StrictHotSpots.Hodge.pair_add_orthogonal_right line 443
  57. lemma OAI.StrictHotSpots.Hodge.neg_inner_bound line 447
  58. lemma OAI.StrictHotSpots.Hodge.energy_pair_normal line 451
  59. lemma OAI.StrictHotSpots.Hodge.energy_pair_curl line 457
  60. lemma OAI.StrictHotSpots.Hodge.energy_bound_normal line 464
  61. lemma OAI.StrictHotSpots.Hodge.energy_bound_curl line 472
  62. lemma OAI.StrictHotSpots.Hodge.energy_decomposition_of_eq line 480
  63. theorem OAI.StrictHotSpots.Hodge.energy_decomposition line 492
  64. theorem OAI.StrictHotSpots.Hodge.vector_inequality line 506
  65. lemma OAI.StrictHotSpots.Hodge.scalar_surplus_eq line 529
  66. lemma OAI.StrictHotSpots.Hodge.equality_norms line 540
  67. lemma OAI.StrictHotSpots.Hodge.add_map_zero line 549
  68. lemma OAI.StrictHotSpots.Hodge.equality_minimizer line 553
  69. lemma OAI.StrictHotSpots.Hodge.equality_of_decomposition line 562
  70. theorem OAI.StrictHotSpots.Hodge.vector_equality line 581
  71. lemma OAI.StrictHotSpots.Hodge.norm_minimizer_integral line 594
  72. lemma OAI.StrictHotSpots.Hodge.real_L2_pair line 601
  73. lemma OAI.StrictHotSpots.Hodge.minimizer_euler_H1 line 609
  74. lemma OAI.StrictHotSpots.Hodge.minimizer_euler_L2 line 619