OAI/MathematicalPhysics/Elasticity/Basic.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Variational isotropic elasticity

H¹ is the closure of smooth value/gradient jets in L². Boundary data are the quotient by the closure of compactly supported smooth jets, and the Dirichlet-to-Neumann map is the physical variational displacement-to-traction pairing. Arbitrary-data Dirichlet well-posedness and independence of representatives are proved, not assumed. Identification of the quotient norm with boundary-chart fractional Sobolev norms is not established here.

  1. abbrev OAI.Elasticity.X line 22

    Also declared: ComparatorChallenges/ElasticityUniqueness.lean:19 (same declaration text).

  2. abbrev OAI.Elasticity.V line 23

    Also declared: ComparatorChallenges/ElasticityUniqueness.lean:20 (same declaration text).

  3. def OAI.Elasticity.coordVector line 25

    Also declared: ComparatorChallenges/ElasticityUniqueness.lean:22 (same declaration text).

  4. def OAI.Elasticity.SmoothBoundary line 27

    Also declared: ComparatorChallenges/ElasticityUniqueness.lean:24 (same declaration text).

  5. def OAI.Elasticity.Domain line 35

    Also declared: ComparatorChallenges/ElasticityUniqueness.lean:32 (same declaration text).

  6. def OAI.Elasticity.SmoothUpTo line 38

    Also declared: ComparatorChallenges/ElasticityUniqueness.lean:35 (same declaration text).

  7. def OAI.Elasticity.Admissible line 41

    Also declared: ComparatorChallenges/ElasticityUniqueness.lean:38 (same declaration text).

  8. abbrev OAI.Elasticity.Ambient line 45

    Also declared: ComparatorChallenges/ElasticityUniqueness.lean:42 (same declaration text).

  9. def OAI.Elasticity.coordDeriv line 48

    Also declared: ComparatorChallenges/ElasticityUniqueness.lean:45 (same declaration text).

  10. def OAI.Elasticity.SmoothJets line 51

    Also declared: ComparatorChallenges/ElasticityUniqueness.lean:48 (same declaration text).

  11. def OAI.Elasticity.TestJets line 57

    Also declared: ComparatorChallenges/ElasticityUniqueness.lean:54 (same declaration text).

  12. abbrev OAI.Elasticity.H1 line 63

    Also declared: ComparatorChallenges/ElasticityUniqueness.lean:60 (same declaration text).

  13. def OAI.Elasticity.HasZeroTrace line 65

    Also declared: ComparatorChallenges/ElasticityUniqueness.lean:62 (same declaration text).

  14. def OAI.Elasticity.SameTrace line 68

    Also declared: ComparatorChallenges/ElasticityUniqueness.lean:65 (same declaration text).

  15. abbrev OAI.Elasticity.BoundaryData line 72

    Source documentation

    Variational boundary data: the quotient by the closure of compactly supported smooth jets.

    Also declared: ComparatorChallenges/ElasticityUniqueness.lean:68 (same declaration text).

    abbrev BoundaryData (Ω : Set X) := Quot (SameTrace Ω)

    Mentions: OAI.Elasticity.X, OAI.Elasticity.SameTrace

  16. def OAI.Elasticity.trace line 74

    Also declared: ComparatorChallenges/ElasticityUniqueness.lean:70 (same declaration text).

  17. def OAI.Elasticity.div line 76

    Also declared: ComparatorChallenges/ElasticityUniqueness.lean:72 (same declaration text).

  18. def OAI.Elasticity.strain line 79

    Also declared: ComparatorChallenges/ElasticityUniqueness.lean:75 (same declaration text).

  19. def OAI.Elasticity.energy line 82

    Also declared: ComparatorChallenges/ElasticityUniqueness.lean:78 (same declaration text).

  20. def OAI.Elasticity.WeakSolution line 87

    Also declared: ComparatorChallenges/ElasticityUniqueness.lean:83 (same declaration text).

  21. def OAI.Elasticity.dirichletSolution line 92

    Source documentation

    A definition by choice, not a wellposedness assumption. The fallback is irrelevant once the Dirichlet problem has been proved solvable.

    Also declared: ComparatorChallenges/ElasticityUniqueness.lean:86 (same declaration text).

    def dirichletSolution (Ω : Set X) (lam mu : X → ℝ)
    (f : BoundaryData Ω) : H1 Ω := by
…

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

  22. def OAI.Elasticity.DN line 100

    Source documentation

    The weak displacement-to-traction pairing; definition (physical-dn).

    Also declared: ComparatorChallenges/ElasticityUniqueness.lean:93 (same declaration text).

    def DN (Ω : Set X) (lam mu : X → ℝ) : BoundaryData Ω → BoundaryData Ω → ℝ :=
…

    Mentions: OAI.Elasticity.X, OAI.Elasticity.BoundaryData

  23. def OAI.Elasticity.MainClaim line 103

    Also declared: ComparatorChallenges/ElasticityUniqueness.lean:96 (same declaration text).