OAI/MathematicalPhysics/Elasticity/ForcedTransport.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElasticityAugmented.leadingP_neg line 11
2. lemma OAI.ElasticityAugmented.normal_sub line 14
3. lemma OAI.ElasticityAugmented.normal_neg line 16
4. lemma OAI.ElasticityAugmented.normal_particular line 19
5. lemma OAI.ElasticityAugmented.exists_normalizing_vector line 23
6. lemma OAI.ElasticityAugmented.residual_source_tangent line 29
7. def OAI.ElasticityFrame.tangentProjection line 45
8. lemma OAI.ElasticityFrame.tangentProjection_apply line 52
9. lemma OAI.ElasticityFrame.tangentProjection_of_normal line 54
10. lemma OAI.ElasticityFrame.tangentProjection_smooth line 58
11. lemma OAI.ElasticityFrame.smooth_vector_forced line 65
12. lemma OAI.ElasticityFrame.smooth_scalar_forced line 77
13. lemma OAI.ElasticityAugmented.transformed_scalar_exact line 104
14. lemma OAI.ElasticityAugmented.scalar_residual_algebra line 127
15. lemma OAI.ElasticityAugmented.normal_form_bottom_residual line 141
16. theorem OAI.ElasticityAugmented.leading_equations_iff line 186

    Source documentation

    Both directions of the actual physical leading transport equivalence.

    theorem leading_equations_iff (θ : 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) :
        (leadingR coord θ (k-r*r) (r*r) a b=0 ∧ leadingS coord θ (k-r*r) (r*r) a b=0) ↔
          (∀ i,direction (A := Smooth) coord θ (changeP r a i)=θ i • 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.changeP, OAI.ElasticityAugmented.changeS

17. lemma OAI.ElasticityAugmented.changeS_derivative_raw line 221
18. lemma OAI.ElasticityAugmented.transformed_scalar_raw line 234
19. lemma OAI.ElasticityAugmented.contraction_at line 251
20. lemma OAI.ElasticityAugmented.changeS_derivative_at line 261
21. lemma OAI.ElasticityAugmented.transformed_scalar_at line 275
22. lemma OAI.ElasticityAugmented.normal_form_bottom_residual_at line 288
23. lemma OAI.ElasticityAugmented.leadingR_contract line 342
24. lemma OAI.ElasticityAugmented.scalar_forced_residual line 352
25. lemma OAI.ElasticityAugmented.normal_form_forced_residual line 374

    Source documentation

    Exact forced transport intertwining, with no homogeneous leading-equation premise. This is the source term needed for the physical compatible recursion.

    lemma normal_form_forced_residual (θ : 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) :
        direction (A := Smooth) coord θ (changeS k r hr a b)-
    …

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

26. def OAI.ElasticityAugmented.topSource line 434
27. def OAI.ElasticityAugmented.scalarSource line 436
28. lemma OAI.ElasticityAugmented.forced_equations_at line 442
29. theorem OAI.ElasticityAugmented.leading_equations_at_iff line 489
30. lemma OAI.ElasticityAugmented.normal_inverseP line 535
31. theorem OAI.ElasticityAugmented.exists_physical_leading_frame line 543

    Source documentation

    Actual physical leading amplitudes, with three independent transformed columns and both augmented leading equations on any prescribed compact region. The equations are local: no global transport equation is assumed.

    theorem exists_physical_leading_frame (θ : Fin 3 → ℂ) (hθ : ∑ i,θ i*θ i=0) (hne : θ≠0)
        (k r : Smooth) (hr : ∀ x,(r : X → ℂ) x≠0) (hk : ∀ x,(k : X → ℂ) x≠0)
        (hl : ∀ x,((k+r*r : Smooth) : X → ℂ) x≠0)
        {C : Set X} (hC : IsCompact C) :
        ∃ a : Fin 3 → Fin 3 → Smooth, ∃ b : Fin 3 → Smooth,
        ∃ B : X → Module.Basis (Fin 3) ℂ (ElasticityFrame.Fiber θ),
          (∀ ν,normal θ (a ν)=0) ∧
          (∀ ν x, x∈C →
            (∀ i,((leadingR coord θ (k-r*r) (r*r) (a ν) (b ν) i : Smooth) : X → ℂ) x=0) ∧
            ((leadingS coord θ (k-r*r) (r*r) (a ν) (b ν) : Smooth) : X → ℂ) x=0) ∧
          ∀ ν x, ((B x ν : ElasticityFrame.Fiber θ) : ElasticityFrame.Amp)=
            ((fun i => (changeP r (a ν) i : X → ℂ) x),(changeS k r hr (a ν) (b ν) : X → ℂ) x) := by
    …

    Mentions: OAI.ElasticityAugmented.Smooth, OAI.ElasticityAugmented.X, OAI.ElasticityFrame.Fiber, OAI.ElasticityAugmented.normal, OAI.ElasticityAugmented.leadingR, OAI.ElasticityAugmented.coord, OAI.ElasticityAugmented.leadingS, OAI.ElasticityFrame.Amp, OAI.ElasticityAugmented.changeP, OAI.ElasticityAugmented.changeS

32. lemma OAI.ElasticityAugmented.normal_topSource line 591
33. theorem OAI.ElasticityAugmented.exists_physical_forced_transport line 599

    Source documentation

    Smooth physical leading equations with arbitrary tangent vector forcing. Solvability is proved from actual planar transport, not assumed. Forcing need only be tangent on the compact region on which the equations are requested.

    theorem exists_physical_forced_transport (θ : Fin 3 → ℂ) (hθ : ∑ i,θ i*θ i=0) (hne : θ≠0)
        (k r : Smooth) (hr : ∀ x,(r : X → ℂ) x≠0) (hk : ∀ x,(k : X → ℂ) x≠0)
        (hl : ∀ x,((k+r*r : Smooth) : X → ℂ) x≠0)
        (H : Fin 3 → Smooth) (K : Smooth) {C : Set X} (hC : IsCompact C)
        (hH : ∀ x∈C,((normal θ H : Smooth) : X → ℂ) x=0) :
        ∃ a : Fin 3 → Smooth, ∃ b : Smooth, normal θ a=0 ∧
          ∀ x∈C, (∀ i,((leadingR coord θ (k-r*r) (r*r) a b i : Smooth) : X → ℂ) x=(H i : X → ℂ) x) ∧
            ((leadingS coord θ (k-r*r) (r*r) a b : Smooth) : X → ℂ) x=(K : X → ℂ) x := by
    …

    Mentions: OAI.ElasticityAugmented.Smooth, OAI.ElasticityAugmented.X, OAI.ElasticityAugmented.normal, OAI.ElasticityAugmented.leadingR, OAI.ElasticityAugmented.coord, OAI.ElasticityAugmented.leadingS