OAI/MathematicalPhysics/Elasticity/TransportAlgebra.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElasticityAugmented.normal line 12
2. def OAI.ElasticityAugmented.direction line 13
3. def OAI.ElasticityAugmented.leadingR line 14
4. def OAI.ElasticityAugmented.leadingS line 17
5. def OAI.ElasticityAugmented.leadingP line 20
6. lemma OAI.ElasticityAugmented.shifted_lap_expansion line 23
7. lemma OAI.ElasticityAugmented.leading_normal line 29
8. lemma OAI.ElasticityAugmented.RT_phase_polynomial line 39
9. lemma OAI.ElasticityAugmented.ST_phase_polynomial line 49
10. lemma OAI.ElasticityAugmented.RT_null_expansion line 59
11. lemma OAI.ElasticityAugmented.ST_null_expansion line 65
12. lemma OAI.ElasticityAugmented.transport_compatibility line 71

    Source documentation

    The exact first-order compatibility identity used by the physical recursion.

    lemma transport_compatibility (θ : Fin 3 → ℂ) (lam m : A) (u : Fin 3 → A) (b : A)
        (hD : ∀ i j f, D i (D j f)=D j (D i f)) :
        div D (leadingR D θ lam m u b)+normal θ (R D lam m u b)-leadingS D θ lam m u b =
          P D m (normal θ u)+leadingP D θ m (div D u-b) := by
    …

    Mentions: OAI.ElasticityAugmented.div, OAI.ElasticityAugmented.leadingR, OAI.ElasticityAugmented.normal, OAI.ElasticityAugmented.R, OAI.ElasticityAugmented.leadingS, OAI.ElasticityAugmented.P, OAI.ElasticityAugmented.leadingP

13. def OAI.ElasticityAugmented.truncation line 91
14. lemma OAI.ElasticityAugmented.truncation_zero line 92
15. lemma OAI.ElasticityAugmented.truncation_succ line 93
16. lemma OAI.ElasticityAugmented.truncated_transport line 98

    Source documentation

    Exact finite telescoping, not an asymptotic formal series.

    lemma truncated_transport (L T : V →ₗ[ℂ] W) (h : ℂ) (hh : h ≠ 0) (N : ℕ) (a : ℕ → V)
        (h₀ : T (a 0)=0) (hrec : ∀ j<N, T (a (j+1))=-L (a j)) :
        L (truncation h N a)+h⁻¹ • T (truncation h N a)=h^N • L (a N) := by
    …

    Mentions: OAI.ElasticityAugmented.truncation

17. abbrev OAI.ElasticityAugmented.Amplitude line 113
18. def OAI.ElasticityAugmented.Rpair line 115
19. def OAI.ElasticityAugmented.leadingRpair line 127
20. def OAI.ElasticityAugmented.divergenceDefect line 140
21. def OAI.ElasticityAugmented.normalPair line 149
22. lemma OAI.ElasticityAugmented.truncated_R line 156
23. lemma OAI.ElasticityAugmented.divT_expansion line 165
24. lemma OAI.ElasticityAugmented.truncated_divergence line 171

    Source documentation

    The physical divergence constraint telescopes independently.

    lemma truncated_divergence (θ : Fin 3 → ℂ) (h : ℂ) (hh : h ≠ 0) (N : ℕ) (a : ℕ → Amplitude A)
        (h₀ : normal θ (a 0).1=0)
        (hrec : ∀ j<N, normal θ (a (j+1)).1=-(div D (a j).1-(a j).2)) :
        divT (shifted D (h⁻¹ • θ)) (truncation h N a).1 =
          (truncation h N a).2+h^N • (div D (a N).1-(a N).2) := by
    …

    Mentions: OAI.ElasticityAugmented.Amplitude, OAI.ElasticityAugmented.normal, OAI.ElasticityAugmented.div, OAI.ElasticityAugmented.divT, OAI.ElasticityAugmented.shifted, OAI.ElasticityAugmented.truncation

25. lemma OAI.ElasticityAugmented.RT_scalar_add line 192
26. theorem OAI.ElasticityAugmented.truncated_physical_residual line 197
27. lemma OAI.ElasticityAugmented.P_neg line 215
28. theorem OAI.ElasticityAugmented.recursive_normal_compatibility line 220

    Source documentation

    Compatibility at every recursive stage follows from both augmented rows and the preceding physical constraint. No extra compatibility is assumed.

    theorem recursive_normal_compatibility (hD : ∀ i j f, D i (D j f)=D j (D i f))
        (θ : Fin 3 → ℂ) (lam m : A) (u v : Fin 3 → A) (b c : A)
        (hR : leadingR D θ lam m u b=-R D lam m v c)
        (hS : leadingS D θ lam m u b=-S D lam m v c)
        (hn : normal θ u=-(div D v-c)) :
        normal θ (R D lam m u b)=leadingP D θ m (div D u-b) := by
    …

    Mentions: OAI.ElasticityAugmented.leadingR, OAI.ElasticityAugmented.R, OAI.ElasticityAugmented.leadingS, OAI.ElasticityAugmented.S, OAI.ElasticityAugmented.normal, OAI.ElasticityAugmented.div, OAI.ElasticityAugmented.leadingP

29. lemma OAI.ElasticityAugmented.leading_stage_compatibility line 234
30. def OAI.ElasticityAugmented.restriction line 252
31. abbrev OAI.ElasticityAugmented.LocalSmooth line 259
32. def OAI.ElasticityAugmented.restrictSmooth line 260
33. lemma OAI.ElasticityAugmented.restrictSmooth_surjective line 261
34. lemma OAI.ElasticityAugmented.restrictSmooth_eq_iff line 263
35. lemma OAI.ElasticityAugmented.restrictSmooth_zero_iff line 272
36. lemma OAI.ElasticityAugmented.restrict_coord_zero line 276
37. def OAI.ElasticityAugmented.localCoord line 286
38. lemma OAI.ElasticityAugmented.localCoord_restrict line 289
39. lemma OAI.ElasticityAugmented.localCoord_commute line 292
40. lemma OAI.ElasticityAugmented.restrict_div line 297
41. lemma OAI.ElasticityAugmented.restrict_normal line 300
42. lemma OAI.ElasticityAugmented.restrict_direction line 303
43. lemma OAI.ElasticityAugmented.restrict_R line 306
44. lemma OAI.ElasticityAugmented.restrict_S line 311
45. lemma OAI.ElasticityAugmented.restrict_leadingR line 316
46. lemma OAI.ElasticityAugmented.restrict_leadingS line 322
47. lemma OAI.ElasticityAugmented.restrict_coeffA line 338
48. lemma OAI.ElasticityAugmented.restrict_coeffV line 347
49. lemma OAI.ElasticityAugmented.inverse_eqOn line 356
50. theorem OAI.ElasticityAugmented.normalized_coefficients_eqOn line 370

    Source documentation

    Equality of the original coefficients on an open set gives equality of both actual normalized matrices there. Reciprocals are not extra exterior identifications: they follow from their defining inverse identities.

    theorem normalized_coefficients_eqOn {B : Set X} (hB : IsOpen B)
        (l₁ m₁ n₁ o₁ l₂ m₂ n₂ o₂ : Smooth)
        (hn₁ : n₁*m₁=1) (hn₂ : n₂*m₂=1)
        (ho₁ : o₁*(l₁+m₁+m₁)=1) (ho₂ : o₂*(l₂+m₂+m₂)=1)
        (hel : EqOn (l₁ : X → ℂ) l₂ B) (hem : EqOn (m₁ : X → ℂ) m₂ B) :
        (∀ k i j,EqOn ((coeffA coord l₁ m₁ n₁ o₁ k i j : Smooth) : X → ℂ)
          ((coeffA coord l₂ m₂ n₂ o₂ k i j : Smooth) : X → ℂ) B) ∧
        (∀ i j,EqOn ((coeffV coord l₁ m₁ n₁ o₁ i j : Smooth) : X → ℂ)
          ((coeffV coord l₂ m₂ n₂ o₂ i j : Smooth) : X → ℂ) B) := by
    …

    Mentions: OAI.ElasticityAugmented.X, OAI.ElasticityAugmented.Smooth, OAI.ElasticityAugmented.coeffA, OAI.ElasticityAugmented.coord, OAI.ElasticityAugmented.coeffV