OAI/MathematicalPhysics/Elasticity/CommonFrame.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Elasticity.dn_smooth_transport_column line 18
2. theorem OAI.Elasticity.dn_common_leading_frame line 105

   Source documentation

   Three actual transferred physical leading columns, in the same constrained fiber as the original globally independent frame. The new columns need not be assumed independent.

   theorem dn_common_leading_frame {Ω : Set X} (hΩ : IsOpen Ω) (hOB : Bornology.IsBounded Ω)
       (r₀ : ℝ) (hr₀ : 1≤r₀) (hK : closure Ω⊆Metric.closedBall 0 r₀)
       (α β : X) (hα : α≠0)
       (hθ : ∑ i,((α i : ℂ)+Complex.I*(β i : ℂ))*((α i : ℂ)+Complex.I*(β i : ℂ))=0)
       (lam m : Fin 2 → X → ℝ)
       (hl : ∀ q,ContDiff ℝ (⊤ : ℕ∞) (lam q)) (hm : ∀ q,ContDiff ℝ (⊤ : ℕ∞) (m q))
       (hp : ∀ q x,0 < m q x ∧ 0<3*lam q x+2*m q x)
       (hcll : ∀ q,ExteriorConstant (smoothOfReal (lam q) (hl q)))
       (hclm : ∀ q,ExteriorConstant (smoothOfReal (m q) (hm q)))
       (he : ∀ x∉Ω,lam 0 x=lam 1 x ∧ m 0 x=m 1 x)
       (hDN : DN Ω (lam 0) (m 0)=DN Ω (lam 1) (m 1)) :
       let θ := fun i => (α i : ℂ)+Complex.I*(β i : ℂ)
   …

   Mentions: OAI.Elasticity.X, OAI.Elasticity.DN

3. lemma OAI.ElasticityAugmented.smooth_sum_eval line 216
4. lemma OAI.ElasticityAugmented.eqOn_coord line 219
5. lemma OAI.ElasticityAugmented.eqOn_direction line 224
6. lemma OAI.ElasticityAugmented.eqOn_logarithmicGrad line 229
7. lemma OAI.ElasticityAugmented.eqOn_physical_change line 237
8. lemma OAI.ElasticityAugmented.eqOn_transport line 255
9. lemma OAI.Elasticity.null_real_imag line 295
10. theorem OAI.Elasticity.dn_common_normal_frame line 318

    Source documentation

    The DN-derived common physical frame in the exact normal variables. All coefficients and the exterior identification are still the actual Lamé pair.

    theorem dn_common_normal_frame {Ω : Set X} (hΩ : IsOpen Ω) (hOB : Bornology.IsBounded Ω)
        (r₀ : ℝ) (hr₀ : 1≤r₀) (hK : closure Ω⊆Metric.closedBall 0 r₀)
        (θ : Fin 3 → ℂ) (hθ : ∑ i,θ i*θ i=0) (hne : θ≠0)
        (lam m : Fin 2 → X → ℝ)
        (hl : ∀ q,ContDiff ℝ (⊤ : ℕ∞) (lam q)) (hm : ∀ q,ContDiff ℝ (⊤ : ℕ∞) (m q))
        (hp : ∀ q x,0 < m q x ∧ 0<3*lam q x+2*m q x)
        (hcll : ∀ q,ExteriorConstant (smoothOfReal (lam q) (hl q)))
        (hclm : ∀ q,ExteriorConstant (smoothOfReal (m q) (hm q)))
        (he : ∀ x∉Ω,lam 0 x=lam 1 x ∧ m 0 x=m 1 x)
        (hDN : DN Ω (lam 0) (m 0)=DN Ω (lam 1) (m 1)) :
        let k := fun q => smoothOfReal (lam q) (hl q)+smoothOfReal (m q) (hm q)
    …

    Mentions: OAI.Elasticity.X, OAI.Elasticity.DN