OAI/MathematicalPhysics/Elasticity/WeakSolutions.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Elasticity.realTest line 12
2. abbrev OAI.Elasticity.reTest line 13
3. abbrev OAI.Elasticity.imTest line 14
4. lemma OAI.Elasticity.realTest_d line 15
5. lemma OAI.Elasticity.test_parts line 23
6. def OAI.Elasticity.scalarDistribution line 27
7. lemma OAI.Elasticity.scalarDistribution_real line 30
8. lemma OAI.Elasticity.localEq_of_realTest line 55
9. def OAI.Elasticity.h1Distribution line 66
10. def OAI.Elasticity.h1GradientDistribution line 68
11. theorem OAI.Elasticity.h1_distribution_derivative line 71

    Source documentation

    Actual distributional identification of every H1 gradient.

    theorem h1_distribution_derivative (u : H1 Ω) (i j : Fin 3) :
        ElasticityDistribution.LocalEq Ω (ElasticityDistribution.dd j (h1Distribution u i))
          (h1GradientDistribution u i j) := by
    …

    Mentions: OAI.Elasticity.H1, OAI.ElasticityDistribution.LocalEq, OAI.ElasticityDistribution.dd, OAI.Elasticity.h1Distribution, OAI.Elasticity.h1GradientDistribution

12. def OAI.Elasticity.stressFun line 92
13. lemma OAI.Elasticity.stress_memLp line 94
14. def OAI.Elasticity.stressL2 line 106
15. lemma OAI.Elasticity.stressL2_ae line 108
16. lemma OAI.Elasticity.stress_pair line 111
17. lemma OAI.Elasticity.stress_pair_integrable line 121
18. lemma OAI.Elasticity.density_stress line 125
19. lemma OAI.Elasticity.energy_test_stress line 132
20. theorem OAI.Elasticity.weakSolution_stress line 145

    Source documentation

    The variational equation yields the actual scalar-test stress equation.

    theorem weakSolution_stress (hl : BoundedCoefficient Ω lam) (hm : BoundedCoefficient Ω mu)
        (u : H1 Ω) (hu : WeakSolution Ω lam mu u) (g : SchwartzMap X ℝ)
        (hc : HasCompactSupport (g : X → ℝ)) (hs : tsupport (g : X → ℝ)⊆Ω) (i : Fin 3) :
        (∑ j, inner ℝ (stressL2 hl hm u.val i j) (schwartzR Ω (ElasticityKorn.d (coordVector j) g)))=0 := by
    …

    Mentions: OAI.Elasticity.BoundedCoefficient, OAI.Elasticity.H1, OAI.Elasticity.WeakSolution, OAI.Elasticity.X, OAI.Elasticity.stressL2, OAI.Elasticity.schwartzR, OAI.ElasticityKorn.d, OAI.Elasticity.coordVector

21. lemma OAI.Elasticity.scalarDistribution_apply line 162
22. lemma OAI.Elasticity.scalarDistribution_mulL line 170
23. lemma OAI.Elasticity.stressL2_eq line 180
24. lemma OAI.Elasticity.stress_distribution line 211
25. theorem OAI.Elasticity.weak_stress_divergence line 224

    Source documentation

    The physical stress of a genuine weak solution has zero distributional divergence.

    theorem weak_stress_divergence (hl : BoundedCoefficient Ω lam) (hm : BoundedCoefficient Ω mu)
        (u : H1 Ω) (hu : WeakSolution Ω lam mu u) (i : Fin 3) :
        LocalEq Ω (∑ j, dd j (scalarDistribution Ω (stressL2 hl hm u.val i j))) 0 := by
    …

    Mentions: OAI.Elasticity.BoundedCoefficient, OAI.Elasticity.H1, OAI.Elasticity.WeakSolution, OAI.Elasticity.scalarDistribution, OAI.Elasticity.stressL2

26. lemma OAI.Elasticity.dist_sd_zero line 244
27. lemma OAI.Elasticity.physical_gradient line 248
28. lemma OAI.Elasticity.physical_stress_sum line 262
29. theorem OAI.Elasticity.weak_physical line 273

    Source documentation

    Actual weak-to-distributional physical elasticity, for the closure-defined H1 space and its variational equation. No PDE regularity hypothesis is introduced.

    theorem weak_physical (hl : BoundedCoefficient Ω lam) (hm : BoundedCoefficient Ω mu)
        (L M : Coeff) (hL : ∀ᵐ x ∂(volume.restrict Ω), eval L x=(lam x : ℂ))
        (hM : ∀ᵐ x ∂(volume.restrict Ω), eval M x=(mu x : ℂ))
        (u : H1 Ω) (hu : WeakSolution Ω lam mu u) (i : Fin 3) :
        LocalEq Ω (phys 0 L M (h1Distribution u) i) 0 := by
    …

    Mentions: OAI.Elasticity.BoundedCoefficient, OAI.Elasticity.H1, OAI.Elasticity.WeakSolution, OAI.Elasticity.h1Distribution

30. lemma OAI.Elasticity.density_full_stress line 292
31. lemma OAI.Elasticity.energy_testJet_stress line 297
32. theorem OAI.Elasticity.weakSolution_of_stress line 332

    Source documentation

    The scalar-test stress equation is equivalent to the physical weak formulation; the nontrivial direction uses actual density of compact test jets.

    theorem weakSolution_of_stress (hl : BoundedCoefficient Ω lam) (hm : BoundedCoefficient Ω mu)
        (u : H1 Ω)
        (ht : ∀ (g : SchwartzMap X ℝ), HasCompactSupport (g : X → ℝ) → tsupport (g : X → ℝ)⊆Ω →
          ∀ i, (∑ j, inner ℝ (stressL2 hl hm u.val i j)
            (schwartzR Ω (ElasticityKorn.d (coordVector j) g)))=0) :
        WeakSolution Ω lam mu u := by
    …

    Mentions: OAI.Elasticity.BoundedCoefficient, OAI.Elasticity.H1, OAI.Elasticity.X, OAI.Elasticity.stressL2, OAI.Elasticity.schwartzR, OAI.ElasticityKorn.d, OAI.Elasticity.coordVector, OAI.Elasticity.WeakSolution

33. theorem OAI.Elasticity.weakSolution_of_physical line 357

    Source documentation

    A genuine H1 field satisfying the actual distributional physical equation is a genuine variational solution; no PDE interface is taken on faith.

    theorem weakSolution_of_physical (hl : BoundedCoefficient Ω lam) (hm : BoundedCoefficient Ω mu)
        (L M : Coeff) (hL : ∀ᵐ x ∂(volume.restrict Ω), eval L x=(lam x : ℂ))
        (hM : ∀ᵐ x ∂(volume.restrict Ω), eval M x=(mu x : ℂ)) (u : H1 Ω)
        (hu : ∀ i, LocalEq Ω (phys 0 L M (h1Distribution u) i) 0) : WeakSolution Ω lam mu u := by
    …

    Mentions: OAI.Elasticity.BoundedCoefficient, OAI.Elasticity.H1, OAI.Elasticity.h1Distribution, OAI.Elasticity.WeakSolution

34. def OAI.Elasticity.schwartzJet line 387
35. lemma OAI.Elasticity.schwartzJet_mem line 389
36. def OAI.Elasticity.schwartzH1 line 393
37. lemma OAI.Elasticity.schwartzH1_value line 394
38. lemma OAI.Elasticity.schwartzH1_gradient line 397
39. def OAI.Elasticity.componentTest line 400
40. lemma OAI.Elasticity.schwartzH1_distribution line 402
41. theorem OAI.Elasticity.schwartzH1_weak line 424

    Source documentation

    A classical real displacement gives the concrete variational H1 field, with its actual derivatives and physical equation.

    theorem schwartzH1_weak {lam mu : X → ℝ} (hl : BoundedCoefficient Ω lam) (hm : BoundedCoefficient Ω mu)
        (L M : Coeff) (hL : ∀ᵐ x ∂(volume.restrict Ω), eval L x=(lam x : ℂ))
        (hM : ∀ᵐ x ∂(volume.restrict Ω), eval M x=(mu x : ℂ)) (F : SchwartzMap X V)
        (he : ∀ i, LocalEq Ω (phys 0 L M (fun i => ((realTest (componentTest F i)) : Dist)) i) 0) :
        WeakSolution Ω lam mu (schwartzH1 (Ω := Ω) F) := by
    …

    Mentions: OAI.Elasticity.X, OAI.Elasticity.BoundedCoefficient, OAI.Elasticity.V, OAI.Elasticity.realTest, OAI.Elasticity.componentTest, OAI.Elasticity.WeakSolution, OAI.Elasticity.schwartzH1

42. lemma OAI.ElasticityDistribution.phys_add line 441
43. lemma OAI.ElasticityDistribution.phys_smul line 446
44. lemma OAI.Elasticity.physical_realTest line 455
45. theorem OAI.Elasticity.weakSolution_parts line 476

    Source documentation

    Real and imaginary parts of a physical H1 solution solve the original real variational problems. This is derived from the actual distribution equation.

    theorem weakSolution_parts (hl : BoundedCoefficient Ω lam) (hm : BoundedCoefficient Ω mu)
        (L M : Coeff) (hL : ∀ᵐ x ∂(volume.restrict Ω), eval L x=(lam x : ℂ))
        (hM : ∀ᵐ x ∂(volume.restrict Ω), eval M x=(mu x : ℂ)) (u v : H1 Ω)
        (he : ∀ i, LocalEq Ω (phys 0 L M (h1Distribution u+Complex.I • h1Distribution v) i) 0) :
        WeakSolution Ω lam mu u ∧ WeakSolution Ω lam mu v := by
    …

    Mentions: OAI.Elasticity.BoundedCoefficient, OAI.Elasticity.H1, OAI.Elasticity.h1Distribution, OAI.Elasticity.WeakSolution

46. def OAI.Elasticity.realVectorTest line 511
47. lemma OAI.Elasticity.realVectorTest_apply line 513
48. lemma OAI.Elasticity.component_realVectorTest line 516
49. def OAI.Elasticity.complexRealH1 line 520
50. def OAI.Elasticity.complexImagH1 line 522
51. lemma OAI.Elasticity.complexH1_value line 524
52. lemma OAI.Elasticity.complexH1_distribution line 533
53. lemma OAI.Elasticity.localEq_of_schwartz_eqOn line 543
54. theorem OAI.Elasticity.complexH1_weak line 555

    Source documentation

    A classical complex physical field embeds into the literal real DN problem through its two actual H1 parts, rather than a presumed complex boundary map.

    theorem complexH1_weak {lam mu : X → ℝ} (hl : BoundedCoefficient Ω lam) (hm : BoundedCoefficient Ω mu)
        (L M : Coeff) (hL : ∀ᵐ x ∂(volume.restrict Ω), eval L x=(lam x : ℂ))
        (hM : ∀ᵐ x ∂(volume.restrict Ω), eval M x=(mu x : ℂ)) (F : Fin 3 → SchwartzMap X ℂ)
        (he : ∀ i, Set.EqOn (ElasticityPhysicalAlgebra.physical 0 (eval L) (eval M) F i : X → ℂ) 0 Ω) :
        WeakSolution Ω lam mu (complexRealH1 (Ω := Ω) F) ∧
    …

    Mentions: OAI.Elasticity.X, OAI.Elasticity.BoundedCoefficient, OAI.ElasticityPhysicalAlgebra.physical, OAI.Elasticity.WeakSolution, OAI.Elasticity.complexRealH1

55. def OAI.Elasticity.scalarGlobal line 579
56. lemma OAI.Elasticity.scalarGlobal_ae line 581
57. lemma OAI.Elasticity.scalarGlobal_distribution line 590
58. def OAI.Elasticity.h1Global line 603
59. lemma OAI.Elasticity.h1Global_distribution line 605
60. lemma OAI.Elasticity.h1Global_ae line 607
61. theorem OAI.Elasticity.h1_classical_representative line 617

    Source documentation

    Interior regularization now applies to the genuine variational solution, not a hypothetical distribution satisfying an assumed physical equation.

    theorem h1_classical_representative (hΩ : IsOpen Ω) {Ω' : Set X} (hΩ' : IsOpen Ω') (hsub : Ω'⊆Ω)
        (hl : BoundedCoefficient Ω lam) (hm : BoundedCoefficient Ω mu)
        (L M N O : Coeff) (hN : N*M=1) (hO : O*(L+M+M)=1)
        (hL : ∀ᵐ x ∂(volume.restrict Ω), eval L x=(lam x : ℂ))
        (hM : ∀ᵐ x ∂(volume.restrict Ω), eval M x=(mu x : ℂ))
        (u : H1 Ω) (hu : WeakSolution Ω lam mu u)
        {g : X → ℂ} (hg : ContDiff ℝ (⊤ : ℕ∞) g) (hc : HasCompactSupport g)
        (hs : tsupport g⊆Ω) (h1 : Set.EqOn g 1 Ω') :
        ∃ v : Fin 3 → SchwartzMap X ℂ,
          (∀ i, ∀ᵐ x ∂volume, x∈Ω' → (u.val.1 x i : ℂ)=v i x) ∧
          ∀ i, Set.EqOn (ElasticityPhysicalAlgebra.physical 0 (eval L) (eval M) v i : X → ℂ) 0 Ω' := by
    …

    Mentions: OAI.Elasticity.X, OAI.Elasticity.BoundedCoefficient, OAI.Elasticity.H1, OAI.Elasticity.WeakSolution, OAI.ElasticityPhysicalAlgebra.physical

62. theorem OAI.Elasticity.physical_classical_transfer line 652

    Source documentation

    Actual smooth complex physical transfer on an interior ball, from the original real variational DN equality. No augmented/artificial DN map is used.

    theorem physical_classical_transfer
        (ha₁ : Admissible Ω lam₁ mu₁) (ha₂ : Admissible Ω lam₂ mu₂)
        (hΩ : IsOpen Ω) (hOB : Bornology.IsBounded Ω) (hΩB : Ω⊆B)
        (hB : IsOpen B) (hB' : IsOpen B') (hsub : B'⊆B)
        (hl₁ : BoundedCoefficient B lam₁) (hm₁ : BoundedCoefficient B mu₁)
        (hl₂ : BoundedCoefficient B lam₂) (hm₂ : BoundedCoefficient B mu₂)
        (he : ∀ x∉Ω, lam₁ x=lam₂ x ∧ mu₁ x=mu₂ x)
        (hDN : DN Ω lam₁ mu₁=DN Ω lam₂ mu₂)
        (L₁ M₁ L₂ M₂ N₂ O₂ : Coeff) (hN : N₂*M₂=1) (hO : O₂*(L₂+M₂+M₂)=1)
        (hL₁ : ∀ᵐ x ∂(volume.restrict B), eval L₁ x=(lam₁ x : ℂ))
        (hM₁ : ∀ᵐ x ∂(volume.restrict B), eval M₁ x=(mu₁ x : ℂ))
        (hL₂ : ∀ᵐ x ∂(volume.restrict B), eval L₂ x=(lam₂ x : ℂ))
    …

    Mentions: OAI.Elasticity.Admissible, OAI.Elasticity.BoundedCoefficient, OAI.Elasticity.DN