OAI/MathematicalPhysics/Elasticity/Restriction.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Elasticity.lpRestrictCLM line 12
  2. lemma OAI.Elasticity.lpRestrict_coe line 14
  3. def OAI.Elasticity.lpZeroValue line 17
  4. lemma OAI.Elasticity.lpZeroValue_coe line 20
  5. lemma OAI.Elasticity.lpZeroValue_add line 26
  6. lemma OAI.Elasticity.lpZeroValue_smul line 38
  7. def OAI.Elasticity.lpZeroExtend line 50
  8. lemma OAI.Elasticity.lpZeroExtend_norm line 54
  9. def OAI.Elasticity.lpZeroExtendCLM line 57
  10. lemma OAI.Elasticity.lpZeroExtend_coe line 59
  11. lemma OAI.Elasticity.lpRestrict_zeroExtend line 61
  12. def OAI.Elasticity.lpRestrictBetween line 76
  13. lemma OAI.Elasticity.lpRestrictBetween_coe line 79
  14. lemma OAI.Elasticity.lpRestrictBetween_toLp line 82
  15. def OAI.Elasticity.ambientRestrict line 88
  16. lemma OAI.Elasticity.restrict_smoothJet line 91
  17. lemma OAI.Elasticity.restrict_h1 line 101
  18. def OAI.Elasticity.h1Restrict line 105
  19. def OAI.Elasticity.lpExtendBetween line 106
  20. lemma OAI.Elasticity.lpExtendBetween_coe line 109
  21. lemma OAI.Elasticity.lpExtendBetween_toLp line 112
  22. def OAI.Elasticity.ambientExtend line 123
  23. lemma OAI.Elasticity.extend_testJet line 126
  24. lemma OAI.Elasticity.extend_h10 line 143
  25. def OAI.Elasticity.gradient line 157
  26. def OAI.Elasticity.elasticDensity line 158
  27. def OAI.Elasticity.ambientDensity line 161
  28. def OAI.Elasticity.ambientEnergy line 163
  29. lemma OAI.Elasticity.energy_eq_ambient line 165
  30. lemma OAI.Elasticity.elasticDensity_symm line 167
  31. lemma OAI.Elasticity.elasticDensity_zero_right line 179
  32. lemma OAI.Elasticity.gradient_restrict line 181
  33. lemma OAI.Elasticity.gradient_extend line 186
  34. lemma OAI.Elasticity.entry_memLp line 197
  35. lemma OAI.Elasticity.BoundedCoefficient.mul_memLp_fun line 200
  36. lemma OAI.Elasticity.ambientDensity_integrable line 206
  37. lemma OAI.Elasticity.ambientEnergy_symm line 222
  38. lemma OAI.Elasticity.ambientEnergy_extend_right line 236
  39. lemma OAI.Elasticity.ambientEnergy_extend_left line 257
  40. lemma OAI.Elasticity.BoundedCoefficient.restrict line 262
  41. lemma OAI.Elasticity.energy_coefficient_locality line 268
  42. lemma OAI.Elasticity.elasticDensity_add_left line 297
  43. lemma OAI.Elasticity.gradient_add line 304
  44. lemma OAI.Elasticity.ambientEnergy_add_left line 309
  45. lemma OAI.Elasticity.ambientEnergy_sub_left line 319
  46. lemma OAI.Elasticity.lpRestrictBetween_extend line 334
  47. lemma OAI.Elasticity.ambientRestrict_extend line 342
  48. def OAI.Elasticity.h1Extend line 348
  49. lemma OAI.Elasticity.weakSolution_restrict line 350
  50. def OAI.Elasticity.gluedH1 line 357
  51. lemma OAI.Elasticity.gluedH1_restrict line 361
  52. lemma OAI.Elasticity.gluedH1_exterior_gradient line 367
  53. lemma OAI.Elasticity.gluedH1_exterior_value line 374
  54. theorem OAI.Elasticity.physical_weak_transfer line 384
  55. def OAI.Elasticity.ambientScalar line 423
  56. lemma OAI.Elasticity.ambientScalar_ae line 425
  57. lemma OAI.Elasticity.scalar_pair_smooth line 428
  58. lemma OAI.Elasticity.smooth_ibp line 439
  59. def OAI.Elasticity.weakDerivativePair line 461
  60. lemma OAI.Elasticity.weakDerivativePair_smooth line 464
  61. theorem OAI.Elasticity.h1_weak_derivative line 487

    Source documentation

    The gradient components in the closure-of-jets H1 really are weak partial derivatives of its value. No weak-derivative property is assumed.

    theorem h1_weak_derivative (u : H1 Ω) (g : SchwartzMap X ℝ)
    (hc : HasCompactSupport (g : X → ℝ)) (hs : tsupport (g : X → ℝ) ⊆ Ω)
    (i j : Fin 3) :
    inner ℝ (ambientScalar Ω none i u.val) (schwartzR Ω (ElasticityKorn.d (coordVector j) g)) =
      -inner ℝ (ambientScalar Ω (some j) i u.val) (schwartzR Ω g) := by
…

    Mentions: OAI.Elasticity.H1, OAI.Elasticity.X, OAI.Elasticity.ambientScalar, OAI.Elasticity.schwartzR, OAI.ElasticityKorn.d, OAI.Elasticity.coordVector

  62. def OAI.Elasticity.testField line 512
  63. lemma OAI.Elasticity.testField_smooth line 513
  64. lemma OAI.Elasticity.testField_deriv line 515
  65. lemma OAI.Elasticity.testField_compact line 523
  66. lemma OAI.Elasticity.testField_support line 525
  67. lemma OAI.Elasticity.testField_memLp line 528
  68. lemma OAI.Elasticity.testField_deriv_memLp line 531
  69. def OAI.Elasticity.testFieldJet line 535
  70. lemma OAI.Elasticity.testFieldJet_mem line 537
  71. def OAI.Elasticity.testH1 line 541
  72. lemma OAI.Elasticity.testH1_zeroTrace line 544
  73. lemma OAI.Elasticity.testH1_gradient line 547
  74. lemma OAI.Elasticity.density_single line 557