OAI/MathematicalPhysics/Elasticity/Homotopy.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElasticityODE.frameDbar line 11
2. def OAI.ElasticityODE.coefficientDbar line 14
3. lemma OAI.ElasticityODE.frameDbar_hasDerivWithinAt line 16
4. lemma OAI.ElasticityODE.frameDbar_initial line 39
5. theorem OAI.ElasticityODE.fundamental_transport line 46

   Source documentation

   The homotopy defect vanishes. This derives the planar frame equation from an actual coefficient homotopy, instead of assuming an Oka trivialization.

   theorem fundamental_transport (b : ℂ → C(Time,R))
       (hb : ContDiff ℝ (⊤ : ℕ∞) b) (p : ℂ) (A : R)
       (he : ∀ t : Time, coefficientDbar b p t=A+(t:ℝ) • (A*b p t-b p t*A)) (t : Time) :
       frameDbar b p t=(t:ℝ) • (A*fundamental (b p) t) := by
   …

   Mentions: OAI.ElasticityODE.Time, OAI.ElasticityODE.coefficientDbar, OAI.ElasticityODE.frameDbar, OAI.ElasticityODE.fundamental

6. def OAI.ElasticityPlanar.coords line 99
7. def OAI.ElasticityPlanar.coord line 100
8. lemma OAI.ElasticityPlanar.coords_coord line 103
9. lemma OAI.ElasticityPlanar.coord_linear_apply line 105
10. def OAI.ElasticityPlanar.classicalDbar line 117
11. lemma OAI.ElasticityPlanar.coord_dbar line 119
12. theorem OAI.ElasticityPlanar.exists_algebra_homotopy line 132

    Source documentation

    The commutator homotopy equation in a genuine finite-dimensional complex Banach algebra, with actual joint smooth representatives.

    theorem exists_algebra_homotopy {S Ω Ω' : Set ℂ} (hS : IsCompact S)
        (hΩS : Ω ⊆ S) (hΩ' : IsOpen Ω') (hsub : Ω' ⊆ Ω)
        (q : Basis n ℂ R) (A : ℂ → R) (hA : ContDiff ℝ (⊤ : ℕ∞) A)
        (hAc : HasCompactSupport A) {g : ℂ → ℂ} (hg : ContDiff ℝ (⊤ : ℕ∞) g)
        (hc : HasCompactSupport g) (hs : tsupport g ⊆ Ω) (h1 : Set.EqOn g 1 Ω') :
        ∃ B : ℝ × ℂ → R, ContDiff ℝ (⊤ : ℕ∞) B ∧
          ∀ s z, z∈Ω' → classicalDbar (fun z => B (s,z)) z=
            A z+s • (A z*B (s,z)-B (s,z)*A z) := by
    …

    Mentions: OAI.ElasticityPlanar.B, OAI.ElasticityPlanar.classicalDbar

13. theorem OAI.ElasticityPlanar.exists_algebra_variable_homotopy line 211

    Source documentation

    The commutator homotopy equation in a genuine finite-dimensional complex Banach algebra, with actual joint smooth representatives.

    theorem exists_algebra_variable_homotopy {S Ω Ω' K : Set ℂ} (hS : IsCompact S)
        (hΩS : Ω ⊆ S) (hΩ' : IsOpen Ω') (hsub : Ω' ⊆ Ω)
        (hK : IsCompact K) (q : Basis n ℂ R) (A : P × ℂ → R) (hA : ContDiff ℝ (⊤ : ℕ∞) A)
        (hAc : ∀ p z, z∉K → A (p,z)=0) {g : ℂ → ℂ} (hg : ContDiff ℝ (⊤ : ℕ∞) g)
        (hc : HasCompactSupport g) (hs : tsupport g ⊆ Ω) (h1 : Set.EqOn g 1 Ω') :
        ∃ B : (ℝ × P) × ℂ → R, ContDiff ℝ (⊤ : ℕ∞) B ∧
          ∀ s p z, z∈Ω' → classicalDbar (fun z => B ((s,p),z)) z=
            A (p,z)+s • (A (p,z)*B ((s,p),z)-B ((s,p),z)*A (p,z)) := by
    …

    Mentions: OAI.ElasticityPlanar.B, OAI.ElasticityPlanar.classicalDbar

14. lemma OAI.ElasticityPlanar.dbar_evaluation line 290
15. lemma OAI.ElasticityPlanar.dbar_fundamental line 296
16. theorem OAI.ElasticityPlanar.exists_planar_frame line 304

    Source documentation

    A global smooth invertible planar frame on the prescribed inner domain. It is built from the proved planar solver and coefficient homotopy flow.

    theorem exists_planar_frame {S Ω Ω' : Set ℂ} (hS : IsCompact S)
        (hΩS : Ω ⊆ S) (hΩ' : IsOpen Ω') (hsub : Ω' ⊆ Ω)
        (q : Basis n ℂ R) (A : ℂ → R) (hA : ContDiff ℝ (⊤ : ℕ∞) A)
        (hAc : HasCompactSupport A) {g : ℂ → ℂ} (hg : ContDiff ℝ (⊤ : ℕ∞) g)
        (hc : HasCompactSupport g) (hs : tsupport g ⊆ Ω) (h1 : Set.EqOn g 1 Ω') :
        ∃ V : ℂ → R, ContDiff ℝ (⊤ : ℕ∞) V ∧ (∀ z, IsUnit (V z)) ∧
          ∀ z∈Ω', classicalDbar V z=A z*V z := by
    …

    Mentions: OAI.ElasticityPlanar.classicalDbar

17. theorem OAI.ElasticityPlanar.exists_variable_planar_frame line 343

    Source documentation

    A genuine jointly smooth global planar frame with arbitrary transverse parameters. Invertibility holds everywhere, not only at a chosen base point.

    theorem exists_variable_planar_frame {S Ω Ω' K : Set ℂ} (hS : IsCompact S)
        (hΩS : Ω ⊆ S) (hΩ' : IsOpen Ω') (hsub : Ω' ⊆ Ω)
        (hK : IsCompact K) (q : Basis n ℂ R) (A : P × ℂ → R) (hA : ContDiff ℝ (⊤ : ℕ∞) A)
        (hAc : ∀ p z, z∉K → A (p,z)=0) {g : ℂ → ℂ} (hg : ContDiff ℝ (⊤ : ℕ∞) g)
        (hc : HasCompactSupport g) (hs : tsupport g ⊆ Ω) (h1 : Set.EqOn g 1 Ω') :
        ∃ V : P × ℂ → R, ContDiff ℝ (⊤ : ℕ∞) V ∧ (∀ w, IsUnit (V w)) ∧
          ∀ p z, z∈Ω' → classicalDbar (fun z => V (p,z)) z=A (p,z)*V (p,z) := by
    …

    Mentions: OAI.ElasticityPlanar.classicalDbar