OAI/MathematicalPhysics/Elasticity/Transport.lean

GitHub source file

100 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ElasticityPlanar.spatial_frame_of_left_inverse line 20

   Source documentation

   A smooth frame for the actual constant complex characteristic direction in ambient space. Transverse coordinates are obtained by a proved continuous left inverse, not assumed to exist. Arbitrary smooth coefficients are allowed.

   theorem spatial_frame_of_left_inverse (J : ℂ →L[ℝ] E) (K : E →L[ℝ] ℂ)
       (hK : Function.LeftInverse K J)
       {S Ω Ω' : Set ℂ} (hS : IsCompact S) (hΩS : Ω ⊆ S)
       (hΩ' : IsOpen Ω') (hsub : Ω' ⊆ Ω) (q : Basis n ℂ R)
       (A : E → R) (hA : ContDiff ℝ (⊤ : ℕ∞) A)
       {g : ℂ → ℂ} (hg : ContDiff ℝ (⊤ : ℕ∞) g) (hc : HasCompactSupport g)
       (hs : tsupport g ⊆ Ω) (h1 : Set.EqOn g 1 Ω') :
       ∃ V : E → R, ContDiff ℝ (⊤ : ℕ∞) V ∧ (∀ x, IsUnit (V x)) ∧
           ∀ x, K x∈Ω' → fderiv ℝ V x (J 1)+I • fderiv ℝ V x (J I)=A x*V x := by
   …

2. theorem OAI.ElasticityPlanar.exists_spatial_frame line 64

   Source documentation

   Actual frames on every compact physical region, with no coordinate, cutoff, or planar-solvability existence hypothesis.

   theorem exists_spatial_frame (J : ℂ →L[ℝ] E) (hJ : Function.Injective J)
       (q : Basis n ℂ R) (A : E → R) (hA : ContDiff ℝ (⊤ : ℕ∞) A)
       {C : Set E} (hC : IsCompact C) :
       ∃ V : E → R, ContDiff ℝ (⊤ : ℕ∞) V ∧ (∀ x, IsUnit (V x)) ∧
         ∀ x∈C, fderiv ℝ V x (J 1)+I • fderiv ℝ V x (J I)=A x*V x := by
   …

   Mentions: OAI.ElasticityPlanar.C

3. theorem OAI.ElasticityPlanar.exists_spatial_linear_frame line 97

   Source documentation

   Genuine invertible transport frames on any finite dimensional complex fiber, with arbitrary smooth coefficients. Applies to the rank-three physical null hyperplane plus scalar fiber, without assuming a frame exists.

   theorem exists_spatial_linear_frame (J : ℂ →L[ℝ] E) (hJ : Function.Injective J)
       (A : E → F →L[ℂ] F) (hA : ContDiff ℝ (⊤ : ℕ∞) A)
       {C : Set E} (hC : IsCompact C) :
       ∃ V : E → F →L[ℂ] F, ContDiff ℝ (⊤ : ℕ∞) V ∧
         (∀ x, IsUnit (V x)) ∧
         ∀ x∈C, fderiv ℝ V x (J 1)+I • fderiv ℝ V x (J I)=A x*V x := by
   …

   Mentions: OAI.ElasticityPlanar.C

4. def OAI.ElasticityPlanar.planeMap line 113
5. lemma OAI.ElasticityPlanar.planeMap_smooth line 114
6. lemma OAI.ElasticityPlanar.planeMap_closedEmbedding line 116
7. lemma OAI.ElasticityPlanar.plane_compact line 120
8. lemma OAI.ElasticityPlanar.plane_deriv line 125
9. theorem OAI.ElasticityPlanar.spatial_compact_kernel line 135

   Source documentation

   Compact kernel uniqueness in ambient physical space, by restriction to all affine characteristic planes. The plane embedding is actual and injective.

   theorem spatial_compact_kernel (J : ℂ →L[ℝ] E) (hJ : Function.Injective J)
       (a : n → n → E → ℂ) (ha : ∀ i j, Continuous (a i j))
       (u : n → E → ℂ) (hu : ∀ i, ContDiff ℝ (⊤ : ℕ∞) (u i))
       (hc : ∀ i, HasCompactSupport (u i))
       (he : ∀ i x, fderiv ℝ (u i) x (J 1)+Complex.I*fderiv ℝ (u i) x (J Complex.I)=
         ∑ j, a i j x*u j x) : ∀ i x, u i x=0 := by
   …

10. def OAI.ElasticityParameter.smoothAlgebra line 158
11. abbrev OAI.ElasticityParameter.Smooth line 179
12. lemma OAI.ElasticityParameter.smooth line 181
13. def OAI.ElasticityParameter.delta line 183
14. lemma OAI.ElasticityParameter.delta_apply line 202
15. lemma OAI.ElasticityParameter.delta_delta line 204
16. lemma OAI.ElasticityParameter.delta_commute line 211
17. def OAI.ElasticityParameter.pbar line 221

    Source documentation

    Parameter antiholomorphic derivative in fixed physical coordinates, without changing the physical point or differentiating any moving plane coordinates.

    def pbar : Derivation ℂ (Smooth (E × ℂ)) (Smooth (E × ℂ)) :=
    …

    Mentions: OAI.ElasticityParameter.Smooth

18. lemma OAI.ElasticityParameter.pbar_delta line 223
19. lemma OAI.ElasticityParameter.slice_deriv line 227
20. lemma OAI.ElasticityParameter.pbar_apply line 234
21. lemma OAI.ElasticityParameter.pbar_zero_of_holomorphic line 240
22. lemma OAI.ElasticityParameter.holomorphic_of_pbar_zero line 251
23. lemma OAI.ElasticityParameter.differentiate_transport line 268

    Source documentation

    Differentiating the transport in fixed coordinates produces a homogeneous transport for the antiholomorphic derivative.

    lemma differentiate_transport (Q : Derivation ℂ A A) (D : k → Derivation ℂ A A)
        (hQD : ∀ r f, Q (D r f)=D r (Q f))
        (θ : k → A) (a : n → n → A) (u : n → A)
        (hθ : ∀ r, Q (θ r)=0) (ha : ∀ i j, Q (a i j)=0)
        (he : ∀ i, ∑ r, θ r*D r (u i)=∑ j, a i j*u j) :
        ∀ i, ∑ r, θ r*D r (Q (u i))=∑ j, a i j*Q (u j) := by
    …

24. def OAI.ElasticityParameter.characteristicPlane line 284
25. lemma OAI.ElasticityParameter.characteristicPlane_one line 287
26. lemma OAI.ElasticityParameter.characteristicPlane_I line 289
27. lemma OAI.ElasticityParameter.spatial_slice_deriv line 291
28. lemma OAI.ElasticityParameter.characteristicPlane_principal line 298
29. lemma OAI.ElasticityParameter.compact_pbar_slice line 309
30. theorem OAI.ElasticityParameter.holomorphic_of_supported_transport line 322

    Source documentation

    Holomorphy of a supported comparison is derived, not assumed. The parameter is differentiated with the physical point fixed, including the holomorphic principal direction, and ambient compact kernel uniqueness then applies.

    theorem holomorphic_of_supported_transport
        (e : k → E) (θ : k → Smooth (E × ℂ))
        (hθx : ∀ r x z, (θ r : E × ℂ → ℂ) (x,z)=(θ r : E × ℂ → ℂ) (0,z))
        (hθ : ∀ r x, Differentiable ℂ (fun z => (θ r : E × ℂ → ℂ) (x,z)))
        (hplane : ∀ z, Function.Injective (characteristicPlane e (fun r => (θ r : E × ℂ → ℂ) (0,z))))
        (a : n → n → Smooth (E × ℂ))
        (ha : ∀ i j x, Differentiable ℂ (fun z => (a i j : E × ℂ → ℂ) (x,z)))
        (u : n → Smooth (E × ℂ))
        (he : ∀ i, ∑ r, θ r*delta (e r,0) (u i)=∑ j, a i j*u j)
        {S : Set E} (hS : IsCompact S) (c : n → ℂ)
        (hs : ∀ i x, x∉S → ∀ z, (u i : E × ℂ → ℂ) (x,z)=c i) :
        ∀ i x, Differentiable ℂ (fun z => (u i : E × ℂ → ℂ) (x,z)) := by
    …

    Mentions: OAI.ElasticityParameter.Smooth, OAI.ElasticityParameter.characteristicPlane, OAI.ElasticityParameter.delta

31. lemma OAI.ElasticityParameter.real_complex_plane_injective line 361
32. abbrev OAI.ElasticityParameter.X line 387
33. def OAI.ElasticityParameter.basis line 388
34. lemma OAI.ElasticityParameter.basis_sum_apply line 389
35. lemma OAI.ElasticityParameter.null_re_im line 393
36. lemma OAI.ElasticityParameter.null_plane_injective line 407
37. abbrev OAI.ElasticityFrame.X line 444
38. abbrev OAI.ElasticityFrame.Amp line 445
39. def OAI.ElasticityFrame.normal line 447
40. def OAI.ElasticityFrame.fiber line 453
41. abbrev OAI.ElasticityFrame.Fiber line 454
42. lemma OAI.ElasticityFrame.finrank_fiber line 456
43. def OAI.ElasticityFrame.scalarVector line 471
44. def OAI.ElasticityFrame.nullVector line 472
45. def OAI.ElasticityFrame.scalarPr line 473
46. def OAI.ElasticityFrame.vectorPr line 475
47. def OAI.ElasticityFrame.connection line 477
48. lemma OAI.ElasticityFrame.connection_vector line 483
49. lemma OAI.ElasticityFrame.connection_scalar line 487
50. lemma OAI.ElasticityFrame.connection_smooth line 492
51. theorem OAI.ElasticityFrame.exists_constraint_frame line 505

    Source documentation

    The actual rank-three constrained transport admits a smooth invertible frame on every compact physical region. The null-plane geometry and smooth planar solvability are proved dependencies, not existence hypotheses.

    theorem exists_constraint_frame (θ : Fin 3 → ℂ) (hθ : ∑ i,θ i*θ i=0) (hne : θ≠0)
        (t : X → ℂ) (q : Fin 3 → X → ℂ)
        (ht : ContDiff ℝ (⊤ : ℕ∞) t) (hq : ∀ i, ContDiff ℝ (⊤ : ℕ∞) (q i))
        {C : Set X} (hC : IsCompact C) :
        ∃ V : X → Fiber θ →L[ℂ] Fiber θ, ContDiff ℝ (⊤ : ℕ∞) V ∧
          (∀ x,IsUnit (V x)) ∧
          ∀ x∈C, fderiv ℝ V x (ElasticityParameter.characteristicPlane ElasticityParameter.basis θ 1)+
            I • fderiv ℝ V x (ElasticityParameter.characteristicPlane ElasticityParameter.basis θ I)=
            connection θ hθ (t x) (fun i => q i x)*V x := by
    …

    Mentions: OAI.ElasticityFrame.X, OAI.ElasticityFrame.Fiber, OAI.ElasticityParameter.characteristicPlane, OAI.ElasticityParameter.basis, OAI.ElasticityFrame.connection

52. theorem OAI.ElasticityPlanar.spatial_transport_of_left_inverse line 529

    Source documentation

    Inhomogeneous transport in the actual ambient characteristic plane, with arbitrary smooth coefficients and source.

    theorem spatial_transport_of_left_inverse (J : ℂ →L[ℝ] E) (K : E →L[ℝ] ℂ)
        (hK : Function.LeftInverse K J)
        {S Ω Ω' : Set ℂ} (hS : IsCompact S) (hΩS : Ω ⊆ S)
        (hΩ' : IsOpen Ω') (hsub : Ω' ⊆ Ω)
        (a : n → n → E → ℂ) (ha : ∀ i j, ContDiff ℝ (⊤ : ℕ∞) (a i j))
        (f : n → E → ℂ) (hf : ∀ i, ContDiff ℝ (⊤ : ℕ∞) (f i))
        {g : ℂ → ℂ} (hg : ContDiff ℝ (⊤ : ℕ∞) g) (hc : HasCompactSupport g)
        (hs : tsupport g ⊆ Ω) (h1 : Set.EqOn g 1 Ω') :
        ∃ u : n → E → ℂ, (∀ i, ContDiff ℝ (⊤ : ℕ∞) (u i)) ∧
          ∀ i x, K x∈Ω' → fderiv ℝ (u i) x (J 1)+I*fderiv ℝ (u i) x (J I)+
            ∑ j, a i j x*u j x=f i x := by
    …

53. theorem OAI.ElasticityPlanar.exists_spatial_transport line 577
54. theorem OAI.ElasticityPlanar.exists_spatial_linear_transport line 611

    Source documentation

    Inhomogeneous spatial transport on an actual finite-dimensional complex fiber, not a postulated planar inverse.

    theorem exists_spatial_linear_transport (J : ℂ →L[ℝ] E) (hJ : Function.Injective J)
        (A : E → F →L[ℂ] F) (hA : ContDiff ℝ (⊤ : ℕ∞) A)
        (f : E → F) (hf : ContDiff ℝ (⊤ : ℕ∞) f)
        {C : Set E} (hC : IsCompact C) :
        ∃ u : E → F, ContDiff ℝ (⊤ : ℕ∞) u ∧
          ∀ x∈C, fderiv ℝ u x (J 1)+I • fderiv ℝ u x (J I)=A x (u x)+f x := by
    …

    Mentions: OAI.ElasticityPlanar.C

55. theorem OAI.ElasticityFrame.exists_constraint_columns line 666

    Source documentation

    Three genuine independent smooth columns for the null constrained system, on an arbitrary compact physical region.

    theorem exists_constraint_columns (θ : Fin 3 → ℂ) (hθ : ∑ i,θ i*θ i=0) (hne : θ≠0)
        (t : X → ℂ) (q : Fin 3 → X → ℂ)
        (ht : ContDiff ℝ (⊤ : ℕ∞) t) (hq : ∀ i, ContDiff ℝ (⊤ : ℕ∞) (q i))
        {C : Set X} (hC : IsCompact C) :
        ∃ B : X → Basis (Fin 3) ℂ (Fiber θ),
          (∀ ν, ContDiff ℝ (⊤ : ℕ∞) (fun x => B x ν)) ∧
          ∀ ν x, x∈C →
            fderiv ℝ (fun x => B x ν) x (ElasticityParameter.characteristicPlane ElasticityParameter.basis θ 1)+
              I • fderiv ℝ (fun x => B x ν) x (ElasticityParameter.characteristicPlane ElasticityParameter.basis θ I)=
              connection θ hθ (t x) (fun i => q i x) (B x ν) := by
    …

    Mentions: OAI.ElasticityFrame.X, OAI.ElasticityFrame.Fiber, OAI.ElasticityParameter.characteristicPlane, OAI.ElasticityParameter.basis, OAI.ElasticityFrame.connection

56. theorem OAI.ElasticityFrame.exists_constraint_transport line 696

    Source documentation

    Inhomogeneous constrained transport has actual smooth solutions as well.

    theorem exists_constraint_transport (θ : Fin 3 → ℂ) (hθ : ∑ i,θ i*θ i=0) (hne : θ≠0)
        (t : X → ℂ) (q : Fin 3 → X → ℂ)
        (ht : ContDiff ℝ (⊤ : ℕ∞) t) (hq : ∀ i, ContDiff ℝ (⊤ : ℕ∞) (q i))
        (f : X → Fiber θ) (hf : ContDiff ℝ (⊤ : ℕ∞) f)
        {C : Set X} (hC : IsCompact C) :
        ∃ u : X → Fiber θ, ContDiff ℝ (⊤ : ℕ∞) u ∧
          ∀ x∈C, fderiv ℝ u x (ElasticityParameter.characteristicPlane ElasticityParameter.basis θ 1)+
            I • fderiv ℝ u x (ElasticityParameter.characteristicPlane ElasticityParameter.basis θ I)=
            connection θ hθ (t x) (fun i => q i x) (u x)+f x := by
    …

    Mentions: OAI.ElasticityFrame.X, OAI.ElasticityFrame.Fiber, OAI.ElasticityParameter.characteristicPlane, OAI.ElasticityParameter.basis, OAI.ElasticityFrame.connection

57. def OAI.ElasticityAugmented.smoothInv line 715
58. lemma OAI.ElasticityAugmented.smoothInv_apply line 717
59. lemma OAI.ElasticityAugmented.smoothInv_mul line 719
60. lemma OAI.ElasticityAugmented.coord_inv line 723
61. def OAI.ElasticityAugmented.thetaDerivation line 727
62. lemma OAI.ElasticityAugmented.thetaDerivation_apply line 728
63. lemma OAI.ElasticityAugmented.direction_mul line 731
64. lemma OAI.ElasticityAugmented.direction_add line 734
65. lemma OAI.ElasticityAugmented.direction_smul line 737
66. def OAI.ElasticityAugmented.changeP line 741
67. def OAI.ElasticityAugmented.logarithmicGrad line 742
68. def OAI.ElasticityAugmented.changeS line 744
69. theorem OAI.ElasticityAugmented.normal_form_top line 751

    Source documentation

    The physical displacement change gives the literal upper transport row, with actual coordinate derivations and no derivative identities postulated.

    theorem normal_form_top (θ : Fin 3 → ℂ) (k r : Smooth)
        (hr : ∀ x, (r : X → ℂ) x≠0) (a : Fin 3 → Smooth) (b : Smooth)
        (hR : leadingR coord θ (k-r*r) (r*r) a b=0) (i : Fin 3) :
        direction (A := Smooth) coord θ (changeP r a i)=θ i • changeS k r hr a b := by
    …

    Mentions: OAI.ElasticityAugmented.Smooth, OAI.ElasticityAugmented.X, OAI.ElasticityAugmented.leadingR, OAI.ElasticityAugmented.coord, OAI.ElasticityAugmented.direction, OAI.ElasticityAugmented.changeP, OAI.ElasticityAugmented.changeS

70. lemma OAI.ElasticityAugmented.direction_inv line 786
71. lemma OAI.ElasticityAugmented.gradient_square line 791
72. lemma OAI.ElasticityAugmented.transformed_gradient line 801
73. def OAI.ElasticityAugmented.thetaGamma line 811
74. lemma OAI.ElasticityAugmented.thetaGamma_eq line 813
75. lemma OAI.ElasticityAugmented.transformed_scalar line 821
76. lemma OAI.ElasticityAugmented.direction_sum line 863
77. lemma OAI.ElasticityAugmented.contraction_derivative line 866
78. lemma OAI.ElasticityAugmented.changeS_derivative line 879
79. lemma OAI.ElasticityAugmented.normal_scalar_algebra line 894
80. def OAI.ElasticityAugmented.transportT line 910
81. def OAI.ElasticityAugmented.transportQ line 914
82. lemma OAI.ElasticityAugmented.transportT_eq line 920
83. lemma OAI.ElasticityAugmented.transportQ_contract line 935
84. theorem OAI.ElasticityAugmented.normal_form_bottom line 947

    Source documentation

    The exact bottom connection row follows from the physical leading equations, not from a separately postulated transport system.

    theorem normal_form_bottom (θ : Fin 3 → ℂ) (k r : Smooth)
        (hr : ∀ x,(r : X → ℂ) x≠0) (hk : ∀ x,(k : X → ℂ) x≠0)
        (hl : ∀ x,((k+r*r : Smooth) : X → ℂ) x≠0) (a : Fin 3 → Smooth) (b : Smooth)
        (hR : leadingR coord θ (k-r*r) (r*r) a b=0)
        (hS : leadingS coord θ (k-r*r) (r*r) a b=0) :
        direction (A := Smooth) coord θ (changeS k r hr a b)=
    …

    Mentions: OAI.ElasticityAugmented.Smooth, OAI.ElasticityAugmented.X, OAI.ElasticityAugmented.leadingR, OAI.ElasticityAugmented.coord, OAI.ElasticityAugmented.leadingS, OAI.ElasticityAugmented.direction, OAI.ElasticityAugmented.changeS

85. def OAI.ElasticityAugmented.inverseP line 991
86. def OAI.ElasticityAugmented.inverseS line 993
87. lemma OAI.ElasticityAugmented.change_inverseP line 997
88. lemma OAI.ElasticityAugmented.inverse_changeP line 1004
89. lemma OAI.ElasticityAugmented.change_inverseS line 1011
90. lemma OAI.ElasticityAugmented.inverse_changeS line 1023
91. lemma OAI.ElasticityAugmented.normal_changeP line 1034
92. lemma OAI.ElasticityAugmented.leadingR_change line 1042

    Source documentation

    Exact intertwining of the vector leading equation, including nonzero source.

    lemma leadingR_change (θ : Fin 3 → ℂ) (k r : Smooth)
        (hr : ∀ x,(r : X → ℂ) x≠0) (a : Fin 3 → Smooth) (b : Smooth) (i : Fin 3) :
        leadingR coord θ (k-r*r) (r*r) a b i=
          2*r*(direction (A := Smooth) coord θ (changeP r a i)-θ i • changeS k r hr a b) := by
    …

    Mentions: OAI.ElasticityAugmented.Smooth, OAI.ElasticityAugmented.X, OAI.ElasticityAugmented.leadingR, OAI.ElasticityAugmented.coord, OAI.ElasticityAugmented.direction, OAI.ElasticityAugmented.changeP, OAI.ElasticityAugmented.changeS

93. lemma OAI.ElasticityAugmented.leadingR_iff line 1063
94. def OAI.ElasticityFrame.smoothProjection line 1079
95. lemma OAI.ElasticityFrame.projection_direction line 1083
96. def OAI.ElasticityFrame.vectorSmooth line 1101
97. def OAI.ElasticityFrame.scalarSmooth line 1103
98. lemma OAI.ElasticityFrame.smooth_normal line 1106
99. lemma OAI.ElasticityFrame.smooth_vector_equation line 1118
100. lemma OAI.ElasticityFrame.smooth_scalar_equation line 1129