OAI/MathematicalPhysics/Elasticity/Augmented.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

Exact differential-algebra identities of the physical and normalized augmented elasticity systems. Smooth derivatives are constructed below; commutation and Leibniz are proved, not postulated for the physical operator.

  1. abbrev OAI.ElasticityAugmented.X line 12
  2. def OAI.ElasticityAugmented.e line 13
  3. def OAI.ElasticityAugmented.smoothAlgebra line 15
  4. abbrev OAI.ElasticityAugmented.Smooth line 37
  5. lemma OAI.ElasticityAugmented.smooth_coe line 39
  6. def OAI.ElasticityAugmented.coord line 42

    Source documentation

    Actual coordinate derivative, as a derivation of the smooth function algebra.

    def coord (i : Fin 3) : Derivation ℂ Smooth Smooth := Derivation.mk'
…

    Mentions: OAI.ElasticityAugmented.Smooth

  7. lemma OAI.ElasticityAugmented.coord_apply line 68
  8. lemma OAI.ElasticityAugmented.coord_coord line 71
  9. lemma OAI.ElasticityAugmented.coord_commute line 79
  10. lemma OAI.ElasticityAugmented.partial_mul line 93
  11. def OAI.ElasticityAugmented.lap line 96
  12. def OAI.ElasticityAugmented.div line 97
  13. def OAI.ElasticityAugmented.cm line 98
  14. def OAI.ElasticityAugmented.R line 100
  15. def OAI.ElasticityAugmented.S line 102
  16. def OAI.ElasticityAugmented.P line 106
  17. lemma OAI.ElasticityAugmented.partial_lap line 111
  18. lemma OAI.ElasticityAugmented.div_lap line 117
  19. lemma OAI.ElasticityAugmented.div_cm line 126
  20. theorem OAI.ElasticityAugmented.augmented_identity line 157

    Source documentation

    The independent scalar compatibility identity, before imposing d=div u.

    theorem augmented_identity (lam m : A) (u : ι → A) (d : A) :
    div D (R D lam m u d) - S D lam m u d = P D m (div D u-d) := by
…

    Mentions: OAI.ElasticityAugmented.div, OAI.ElasticityAugmented.R, OAI.ElasticityAugmented.S, OAI.ElasticityAugmented.P

  21. theorem OAI.ElasticityAugmented.smooth_augmented_identity line 173

    Source documentation

    No commuting-derivation hypothesis remains for actual smooth functions.

    theorem smooth_augmented_identity (lam m : Smooth) (u : Fin 3 → Smooth) (d : Smooth) :
    div coord (R coord lam m u d) - S coord lam m u d = P coord m (div coord u-d) :=
…

    Mentions: OAI.ElasticityAugmented.Smooth, OAI.ElasticityAugmented.div, OAI.ElasticityAugmented.coord, OAI.ElasticityAugmented.R, OAI.ElasticityAugmented.S, OAI.ElasticityAugmented.P

  22. def OAI.ElasticityAugmented.lapT line 182
  23. def OAI.ElasticityAugmented.divT line 183
  24. def OAI.ElasticityAugmented.cmT line 184
  25. def OAI.ElasticityAugmented.RT line 186
  26. def OAI.ElasticityAugmented.ST line 188
  27. def OAI.ElasticityAugmented.PT line 192
  28. lemma OAI.ElasticityAugmented.covariant_div_lap line 199
  29. lemma OAI.ElasticityAugmented.covariant_div_cm line 209
  30. theorem OAI.ElasticityAugmented.covariant_augmented_identity line 242

    Source documentation

    Compatibility after conjugation, proved for the genuine connection Leibniz rule rather than falsely treating a shifted derivative as a derivation.

    theorem covariant_augmented_identity (lam m : A) (u : ι → A) (d : A) :
    divT T (RT D T lam m u d) - ST D T lam m u d = PT D T m (divT T u-d) := by
…

    Mentions: OAI.ElasticityAugmented.divT, OAI.ElasticityAugmented.RT, OAI.ElasticityAugmented.ST, OAI.ElasticityAugmented.PT

  31. def OAI.ElasticityAugmented.LT line 256

    Source documentation

    The physical stress-divergence, using the conjugated coordinate derivative.

    def LT (lam m : A) (u : ι → A) (i : ι) : A :=
…
  32. lemma OAI.ElasticityAugmented.physical_conjugated_expansion line 260
  33. def OAI.ElasticityAugmented.shifted line 273

    Source documentation

    A complex constant phase shifts an actual coordinate derivative.

    def shifted (z : ι → ℂ) (i : ι) : A →ₗ[ℂ] A :=
…
  34. lemma OAI.ElasticityAugmented.shifted_apply line 277
  35. lemma OAI.ElasticityAugmented.shifted_mul line 281
  36. lemma OAI.ElasticityAugmented.shifted_commute line 288
  37. theorem OAI.ElasticityAugmented.shifted_physical_expansion line 294
  38. theorem OAI.ElasticityAugmented.shifted_physical_divergence line 299
  39. lemma OAI.ElasticityAugmented.grad_cm line 319
  40. lemma OAI.ElasticityAugmented.grad_RT line 335
  41. lemma OAI.ElasticityAugmented.normalized_vector line 346
  42. lemma OAI.ElasticityAugmented.normalized_scalar_numerator line 354
  43. lemma OAI.ElasticityAugmented.normalized_scalar line 366