OAI/MathematicalPhysics/Elasticity/Variational.lean

GitHub source file

132 declarations, 0 contain sorry, 0 declared as axioms

The physical energy is a continuous bilinear form on the actual Hilbert jet space. Bounded coefficients below are proved from admissibility later, rather than added to the inverse theorem.

  1. lemma OAI.Elasticity.coordDeriv_add line 15
  2. lemma OAI.Elasticity.coordDeriv_smul line 22
  3. lemma OAI.Elasticity.coordDeriv_zero line 28
  4. def OAI.Elasticity.smoothJetSubmodule line 32
  5. def OAI.Elasticity.testJetSubmodule line 66

    Source documentation

    Compactly supported interior test jets, with the actual support condition.

    def testJetSubmodule (Ω : Set X) : Submodule ℝ (Ambient Ω) where
…

    Mentions: OAI.Elasticity.X, OAI.Elasticity.Ambient

  6. lemma OAI.Elasticity.testJetSubmodule_le line 102
  7. def OAI.Elasticity.h1Submodule line 106
  8. def OAI.Elasticity.h10Submodule line 109
  9. lemma OAI.Elasticity.h10Submodule_le line 112
  10. lemma OAI.Elasticity.sameTrace_refl line 115
  11. lemma OAI.Elasticity.sameTrace_symm line 118
  12. lemma OAI.Elasticity.sameTrace_trans line 123
  13. abbrev OAI.Elasticity.JetH line 128
  14. def OAI.Elasticity.jetEquiv line 130
  15. lemma OAI.Elasticity.jetEquiv_apply line 141
  16. def OAI.Elasticity.H1Hilbert line 144
  17. def OAI.Elasticity.H10Hilbert line 147
  18. lemma OAI.Elasticity.isClosed_H1Hilbert line 150
  19. lemma OAI.Elasticity.isClosed_H10Hilbert line 153
  20. instance OAI.Elasticity.(instance at line 156) line 156
  21. instance OAI.Elasticity.(instance at line 157) line 157
  22. lemma OAI.Elasticity.H10Hilbert_le line 159
  23. def OAI.Elasticity.h1Equiv line 164

    Source documentation

    The Hilbert version is exactly the H¹ jet closure, not an extra regularity hypothesis or a replacement by a smaller test space.

    def h1Equiv (Ω : Set X) : (H1Hilbert Ω) ≃ H1 Ω where
…

    Mentions: OAI.Elasticity.X, OAI.Elasticity.H1Hilbert, OAI.Elasticity.H1

  24. abbrev OAI.Elasticity.ScalarL2 line 186
  25. structure OAI.Elasticity.BoundedCoefficient line 188
  26. lemma OAI.Elasticity.BoundedCoefficient.mul_memLp line 196
  27. def OAI.Elasticity.BoundedCoefficient.mulL line 202
  28. lemma OAI.Elasticity.BoundedCoefficient.mulL_ae line 235
  29. lemma OAI.Elasticity.BoundedCoefficient.inner_mulL line 238
  30. lemma OAI.Elasticity.lp_sum_ae line 249
  31. def OAI.Elasticity.jetEntry line 263
  32. def OAI.Elasticity.jetDiv line 267
  33. def OAI.Elasticity.jetStrain line 269
  34. lemma OAI.Elasticity.jetEntry_ae line 272
  35. lemma OAI.Elasticity.jetDiv_ae line 276
  36. lemma OAI.Elasticity.jetStrain_ae line 285
  37. def OAI.Elasticity.jetEnergy line 298
  38. lemma OAI.Elasticity.jetEnergy_apply line 304
  39. abbrev OAI.ElasticityKorn.X line 322
  40. abbrev OAI.ElasticityKorn.S line 323
  41. abbrev OAI.ElasticityKorn.L2 line 324
  42. def OAI.ElasticityKorn.norm2 line 326
  43. def OAI.ElasticityKorn.pair line 327
  44. def OAI.ElasticityKorn.e line 328
  45. def OAI.ElasticityKorn.d line 329
  46. lemma OAI.ElasticityKorn.d_apply line 330
  47. lemma OAI.ElasticityKorn.smooth line 332
  48. lemma OAI.ElasticityKorn.pair_integral line 333
  49. lemma OAI.ElasticityKorn.pair_self line 341
  50. lemma OAI.ElasticityKorn.pair_symm line 342
  51. lemma OAI.ElasticityKorn.pair_add_left line 343
  52. lemma OAI.ElasticityKorn.pair_add_right line 345
  53. lemma OAI.ElasticityKorn.pair_smul_left line 347
  54. lemma OAI.ElasticityKorn.pair_smul_right line 349
  55. lemma OAI.ElasticityKorn.pair_sum_left line 351
  56. lemma OAI.ElasticityKorn.pair_sum_right line 354
  57. lemma OAI.ElasticityKorn.pair_bound line 357
  58. lemma OAI.ElasticityKorn.integrable_pair line 358
  59. lemma OAI.ElasticityKorn.pair_d line 360
  60. lemma OAI.ElasticityKorn.d_d line 366
  61. lemma OAI.ElasticityKorn.d_comm line 373
  62. lemma OAI.ElasticityKorn.cross line 379
  63. def OAI.ElasticityKorn.divergence line 385
  64. def OAI.ElasticityKorn.gradEnergy line 386
  65. def OAI.ElasticityKorn.strainEnergy line 387
  66. lemma OAI.ElasticityKorn.norm2_half_add_sq line 389
  67. lemma OAI.ElasticityKorn.cross_sum line 394
  68. theorem OAI.ElasticityKorn.korn_identity line 405

    Source documentation

    The classical exact whole-space Korn identity, by two integrations by parts.

    theorem korn_identity (u : Fin 3 → S) :
    2*strainEnergy u = gradEnergy u + norm2 (divergence u)^2 := by
…

    Mentions: OAI.ElasticityKorn.S, OAI.ElasticityKorn.strainEnergy, OAI.ElasticityKorn.gradEnergy, OAI.ElasticityKorn.norm2, OAI.ElasticityKorn.divergence

  69. theorem OAI.ElasticityKorn.korn line 415
  70. def OAI.ElasticityKorn.qCLM line 419
  71. def OAI.ElasticityKorn.Q line 420
  72. lemma OAI.ElasticityKorn.Q_apply line 421
  73. lemma OAI.ElasticityKorn.d_Q line 423
  74. lemma OAI.ElasticityKorn.pair_Q line 434
  75. lemma OAI.ElasticityKorn.norm2_Q_supported line 439
  76. theorem OAI.ElasticityKorn.poincare line 450

    Source documentation

    Supported Poincaré with explicit constant; support is imposed on the actual function, not on an abstract or assumed Sobolev norm.

    theorem poincare {R : ℝ} (f : S) (hf : ∀ x, f x ≠ 0 → |x 0| ≤ R) :
    norm2 f ≤ 2*R*norm2 (d (e 0) f) := by
…

    Mentions: OAI.ElasticityKorn.S, OAI.ElasticityKorn.norm2, OAI.ElasticityKorn.d, OAI.ElasticityKorn.e

  77. instance OAI.Elasticity.temperate_restrict_volume line 486
  78. abbrev OAI.Elasticity.schwartzR line 491
  79. lemma OAI.Elasticity.schwartzR_norm_sq line 494
  80. lemma OAI.Elasticity.schwartzR_supported_norm line 503
  81. def OAI.Elasticity.jetScalar line 515
  82. lemma OAI.Elasticity.jetScalar_ae line 520
  83. lemma OAI.Elasticity.scalar_projection_norm_sq line 524
  84. def OAI.Elasticity.jetValueSq line 542
  85. def OAI.Elasticity.jetGradSq line 543
  86. def OAI.Elasticity.jetStrainSq line 544
  87. lemma OAI.Elasticity.jet_norm_sq line 546
  88. lemma OAI.Elasticity.continuous_jetValueSq line 553
  89. lemma OAI.Elasticity.continuous_jetGradSq line 556
  90. lemma OAI.Elasticity.continuous_jetStrainSq line 559
  91. lemma OAI.Elasticity.coordDeriv_scalar line 564

    Source documentation

    The scalar derivatives of an actual vector-valued smooth test field.

    lemma coordDeriv_scalar (f : X → V) (hf : ContDiff ℝ (⊤ : ℕ∞) f)
    (i j : Fin 3) (x : X) :
    fderiv ℝ (fun y => (f y) i) x (coordVector j) = (coordDeriv f j x) i := by
…

    Mentions: OAI.Elasticity.X, OAI.Elasticity.V, OAI.Elasticity.coordVector, OAI.Elasticity.coordDeriv

  92. lemma OAI.Elasticity.scalar_test_support line 573
  93. lemma OAI.Elasticity.jet_test_representation line 577
  94. lemma OAI.Elasticity.schwartz_d_support line 620
  95. lemma OAI.Elasticity.schwartz_strain_support line 624
  96. lemma OAI.Elasticity.jet_test_energies line 631
  97. lemma OAI.Elasticity.test_korn line 660
  98. lemma OAI.Elasticity.test_poincare line 666
  99. lemma OAI.Elasticity.h10_induction_closed line 688
  100. lemma OAI.Elasticity.h10_korn line 699
  101. lemma OAI.Elasticity.h10_poincare line 704
  102. lemma OAI.Elasticity.h10_norm_strain line 710
  103. lemma OAI.Elasticity.SmoothUpTo.continuousOn_closure line 739
  104. lemma OAI.Elasticity.SmoothUpTo.boundedCoefficient line 744
  105. lemma OAI.Elasticity.Admissible.uniform_positive line 753
  106. lemma OAI.Elasticity.trace_sq_le line 764
  107. lemma OAI.Elasticity.elasticity_density_lower line 775

    Source documentation

    Pointwise strong convexity controls the full physical symmetric strain, including negative lambda. This uses the exact hypothesis 3λ+2μ>0.

    lemma elasticity_density_lower (lam mu c : ℝ) (hc : 0 ≤ c) (hm : c ≤ mu)
    (hlm : c ≤ 3*lam+2*mu) (A : Fin 3 → Fin 3 → ℝ) :
    c*(∑ i, ∑ j, A i j^2) ≤ lam*(∑ i, A i i)^2+2*mu*(∑ i, ∑ j, A i j^2) := by
…
  108. lemma OAI.Elasticity.weighted_integrable line 789
  109. lemma OAI.Elasticity.jetEnergy_integral line 793
  110. lemma OAI.Elasticity.jetEnergy_eq_energy line 820
  111. lemma OAI.Elasticity.scalarL2_norm_sq line 845
  112. lemma OAI.Elasticity.scalarL2_integrable_sq line 850
  113. lemma OAI.Elasticity.jetDiv_strain_ae line 855
  114. lemma OAI.Elasticity.jetStrainSq_integral line 867
  115. lemma OAI.Elasticity.jetEnergy_lower line 875
  116. def OAI.Elasticity.zeroTraceEnergy line 900

    Source documentation

    The actual Dirichlet physical energy on the exact zero-trace Hilbert space.

    def zeroTraceEnergy (hl : BoundedCoefficient Ω lam) (hm : BoundedCoefficient Ω mu) :
    H10Hilbert Ω →L[ℝ] H10Hilbert Ω →L[ℝ] ℝ :=
…

    Mentions: OAI.Elasticity.BoundedCoefficient, OAI.Elasticity.H10Hilbert

  117. lemma OAI.Elasticity.zeroTraceEnergy_apply line 904
  118. theorem OAI.Elasticity.physical_coercive line 909

    Source documentation

    Korn, supported Poincare and the exact strong convexity yield coercivity; there is no sign restriction on lambda beyond 3 lambda + 2 mu > 0.

    theorem physical_coercive (ha : Admissible Ω lam mu) (hO : IsOpen Ω)
    (hB : Bornology.IsBounded Ω) :
    IsCoercive (zeroTraceEnergy (ha.1.boundedCoefficient hO hB)
      (ha.2.1.boundedCoefficient hO hB)) := by
…

    Mentions: OAI.Elasticity.Admissible, OAI.Elasticity.zeroTraceEnergy

  119. def OAI.Elasticity.traceSetoid line 937
  120. lemma OAI.Elasticity.trace_eq_iff line 941
  121. lemma OAI.Elasticity.hasZeroTrace_h1Equiv line 944
  122. lemma OAI.Elasticity.sameTrace_h1Equiv line 947
  123. lemma OAI.Elasticity.weakSolution_h1Equiv line 953
  124. theorem OAI.Elasticity.dirichlet_exists line 972

    Source documentation

    Lax--Milgram applied to the actual physical form and the exact jet closures. The prescribed trace is arbitrary, not restricted to smooth data.

    theorem dirichlet_exists (ha : Admissible Ω lam mu) (hO : IsOpen Ω)
    (hB : Bornology.IsBounded Ω) (f : BoundaryData Ω) :
    ∃ u : H1 Ω, trace Ω u=f ∧ WeakSolution Ω lam mu u := by
…

    Mentions: OAI.Elasticity.Admissible, OAI.Elasticity.BoundaryData, OAI.Elasticity.H1, OAI.Elasticity.trace, OAI.Elasticity.WeakSolution

  125. theorem OAI.Elasticity.dirichletSolution_spec line 1004
  126. theorem OAI.Elasticity.dirichlet_unique line 1012
  127. lemma OAI.Elasticity.jetEnergy_symm line 1054
  128. lemma OAI.Elasticity.energy_symm line 1070
  129. lemma OAI.Elasticity.energy_eq_of_sameTrace line 1076
  130. lemma OAI.Elasticity.DN_eq_energy line 1094
  131. lemma OAI.Elasticity.solution_eq_dirichlet line 1102
  132. theorem OAI.Elasticity.interior_physical_transfer line 1108