OAI/MathematicalPhysics/Elasticity/Solvability.lean

GitHub source file

77 declarations, 0 contain sorry, 0 declared as axioms

The Hahn--Banach / Riesz step used by the physical solvability argument. This proves the functional-analytic implication, rather than postulating existence of a right inverse. The physical test estimate is proved separately.

  1. theorem OAI.ElasticityDualSolvability.exists_weak_solution line 17

    Source documentation

    A lower norm estimate on an (unbounded) test operator gives a weak solution for every Hilbert-space forcing, with precisely the same constant. No density or completeness of the test space, or closedness of the range, is assumed.

    theorem exists_weak_solution (D : Submodule ℂ H) (A : D →ₗ[ℂ] H)
    (C : ℝ) (hC : 0 ≤ C) (hA : ∀ v : D, ‖(v : H)‖ ≤ C * ‖A v‖) (f : H) :
    ∃ z : H, ‖z‖ ≤ C * ‖f‖ ∧ ∀ v : D, inner ℂ z (A v) = inner ℂ f (v : H) := by
…
  2. abbrev OAI.ElasticityPhysicalDual.X line 62
  3. abbrev OAI.ElasticityPhysicalDual.H line 63
  4. def OAI.ElasticityPhysicalDual.embed line 65
  5. lemma OAI.ElasticityPhysicalDual.embed_apply line 70
  6. lemma OAI.ElasticityPhysicalDual.embed_injective line 72
  7. lemma OAI.ElasticityPhysicalDual.norm_embed line 78
  8. lemma OAI.ElasticityPhysicalDual.inner_embed line 82
  9. def OAI.ElasticityPhysicalDual.adjPhase line 89
  10. lemma OAI.ElasticityPhysicalDual.pair_neg_left line 91
  11. lemma OAI.ElasticityPhysicalDual.pair_neg_right line 94
  12. lemma OAI.ElasticityPhysicalDual.pair_shift line 97
  13. lemma OAI.ElasticityPhysicalDual.pair_mult line 103
  14. lemma OAI.ElasticityPhysicalDual.pair_two_shift line 111
  15. lemma OAI.ElasticityPhysicalDual.pair_eq_ip line 117
  16. lemma OAI.ElasticityPhysicalDual.pair_sum_left line 119
  17. lemma OAI.ElasticityPhysicalDual.pair_sum_right line 124
  18. lemma OAI.ElasticityPhysicalDual.physical_adjoint line 129
  19. def OAI.ElasticityPhysicalDual.supported line 144

    Source documentation

    Supported Schwartz vectors, regarded as an actual subspace of L2.

    def supported (R : ℝ) : Submodule ℂ (Fin 3 → S) where
…
  20. lemma OAI.ElasticityPhysicalDual.physical_add line 150
  21. lemma OAI.ElasticityPhysicalDual.physical_smul line 156
  22. def OAI.ElasticityPhysicalDual.physicalLM line 162

    Source documentation

    Exact shifted stress-divergence as a linear map, for duality on its range.

    def physicalLM (z : Fin 3 → ℂ) (lam m : X → ℂ) : (Fin 3 → S) →ₗ[ℂ] (Fin 3 → S) where
…

    Mentions: OAI.ElasticityPhysicalDual.X

  23. theorem OAI.ElasticityPhysicalDual.weak_physical_from_test line 169

    Source documentation

    The physical weak equation follows from the actual uniform test estimate. The forcing and unknown belong to the genuine vector-valued L2 Hilbert space.

    theorem weak_physical_from_test (R h : ℝ) (z : Fin 3 → ℂ) (lam m : X → ℂ)
    (C : ℝ) (hC : 0 ≤ C)
    (htest : ∀ u : Fin 3 → S, (∀ i, BallSupported R (u i)) →
      sobNorm h 0 u ≤ C*sobNorm h 0 (physical (adjPhase z) lam m u)) (F : H) :
    ∃ w : H, ‖w‖ ≤ C*‖F‖ ∧ ∀ v : Fin 3 → S, (∀ i, BallSupported R (v i)) →
      inner ℂ w (embed (physical (adjPhase z) lam m v)) = inner ℂ F (embed v) := by
…

    Mentions: OAI.ElasticityPhysicalDual.X, OAI.ElasticityPhysicalDual.adjPhase, OAI.ElasticityPhysicalDual.H, OAI.ElasticityPhysicalDual.embed

  24. lemma OAI.ElasticityPhysicalDual.adjPhase_phase line 200
  25. abbrev OAI.ElasticityDistribution.S line 219
  26. def OAI.ElasticityDistribution.cj line 220
  27. lemma OAI.ElasticityDistribution.cj_apply line 221
  28. lemma OAI.ElasticityDistribution.cj_add line 222
  29. lemma OAI.ElasticityDistribution.cj_smul line 223
  30. lemma OAI.ElasticityDistribution.cj_sum line 224
  31. lemma OAI.ElasticityDistribution.cj_cj line 227
  32. lemma OAI.ElasticityDistribution.cj_deriv line 228
  33. lemma OAI.ElasticityDistribution.cj_shift line 233
  34. lemma OAI.ElasticityDistribution.cj_mult line 238
  35. lemma OAI.ElasticityDistribution.cj_physical line 243
  36. lemma OAI.ElasticityDistribution.cj_supported line 250
  37. lemma OAI.ElasticityDistribution.Lp_test line 253
  38. lemma OAI.ElasticityDistribution.sd_test line 267
  39. lemma OAI.ElasticityDistribution.coeff_test line 273
  40. lemma OAI.ElasticityDistribution.coeff_smul_add line 275
  41. lemma OAI.ElasticityDistribution.two_sd_test line 277
  42. theorem OAI.ElasticityDistribution.physical_transpose line 285

    Source documentation

    Formal transpose of the actual complex physical distribution operator. It is proved by evaluation on Schwartz tests, so no integration-by-parts regularity of the unknown is assumed.

    theorem physical_transpose (z : Fin 3 → ℂ) (lam m : Coeff) (u : Fin 3 → Dist) (φ : Fin 3 → S) :
    (∑ i, phys z lam m u i (φ i)) =
      ∑ i, u i (ElasticityPhysicalAlgebra.physical (-z) (eval lam) (eval m) φ i) := by
…

    Mentions: OAI.ElasticityDistribution.Coeff, OAI.ElasticityDistribution.Dist, OAI.ElasticityDistribution.S, OAI.ElasticityDistribution.phys, OAI.ElasticityPhysicalAlgebra.physical, OAI.ElasticityDistribution.eval

  43. theorem OAI.ElasticityDistribution.weak_to_vector_distribution line 306

    Source documentation

    The actual Hilbert weak equation is the actual physical distribution equation. This lemma does not assume regularity of the unknown and does not replace the physical stress-divergence operator by an abstract PDE hypothesis.

    theorem weak_to_vector_distribution (R : ℝ) (z : Fin 3 → ℂ) (lam m : Coeff)
    (hrl : ∀ x, star (eval lam x)=eval lam x) (hrm : ∀ x, star (eval m x)=eval m x)
    (w F : H)
    (heq : ∀ v : Fin 3 → S, (∀ i, BallSupported R (v i)) →
      inner ℂ w (embed (physical (adjPhase z) (eval lam) (eval m) v)) = inner ℂ F (embed v))
    (φ : Fin 3 → S) (hφ : ∀ i, BallSupported R (φ i)) :
    (∑ i, phys z lam m (fun j => (w j : Dist)) i (φ i)) =
      ∑ i, (F i : Dist) (φ i) := by
…

    Mentions: OAI.ElasticityDistribution.Coeff, OAI.ElasticityDistribution.eval, OAI.ElasticityDistribution.H, OAI.ElasticityDistribution.S, OAI.ElasticityDistribution.phys, OAI.ElasticityDistribution.Dist

  44. theorem OAI.ElasticityDistribution.weak_to_local_physical line 327
  45. abbrev OAI.ElasticityCoeffBounds.X line 352
  46. def OAI.ElasticityCoeffBounds.ExteriorConstant line 354
  47. lemma OAI.ElasticityCoeffBounds.ExteriorConstant.growth line 357
  48. lemma OAI.ElasticityCoeffBounds.ExteriorConstant.bound line 365
  49. lemma OAI.ElasticityCoeffBounds.ExteriorConstant.const line 377
  50. lemma OAI.ElasticityCoeffBounds.ExteriorConstant.add line 382
  51. lemma OAI.ElasticityCoeffBounds.ExteriorConstant.mul line 396
  52. lemma OAI.ElasticityCoeffBounds.ExteriorConstant.neg line 413
  53. lemma OAI.ElasticityCoeffBounds.ExteriorConstant.sub line 423
  54. lemma OAI.ElasticityCoeffBounds.ExteriorConstant.coord line 427
  55. lemma OAI.ElasticityCoeffBounds.ExteriorConstant.zero line 437
  56. lemma OAI.ElasticityCoeffBounds.ExteriorConstant.natCast line 440
  57. lemma OAI.ElasticityCoeffBounds.ExteriorConstant.sum line 443
  58. lemma OAI.ElasticityCoeffBounds.exterior_coeffA line 453
  59. lemma OAI.ElasticityCoeffBounds.exterior_coeffV line 478
  60. lemma OAI.ElasticityCoeffBounds.exterior_cPhys line 489
  61. lemma OAI.ElasticityCoeffBounds.ExteriorConstant.uniform_bound line 493
  62. def OAI.ElasticityCoeffBounds.reciprocal line 502

    Source documentation

    The reciprocal is the pointwise reciprocal, not an abstract inverse assumption.

    def reciprocal (f : Smooth) (hf : ∀ x, (f : X → ℂ) x ≠ 0) : Smooth :=
…

    Mentions: OAI.ElasticityCoeffBounds.X

  63. lemma OAI.ElasticityCoeffBounds.reciprocal_mul line 505
  64. lemma OAI.ElasticityCoeffBounds.ExteriorConstant.reciprocal line 511
  65. theorem OAI.ElasticityCoeffBounds.physical_test_exterior line 526
  66. abbrev OAI.ElasticityPhysicalSolvability.X line 582
  67. theorem OAI.ElasticityPhysicalSolvability.weak_solvability line 584
  68. def OAI.ElasticityPhysicalSolvability.realSmooth line 602

    Source documentation

    The real smooth coefficients are embedded pointwise, not abstractly.

    def realSmooth (f : X → ℝ) (hf : ContDiff ℝ (⊤ : ℕ∞) f) : Smooth :=
…

    Mentions: OAI.ElasticityPhysicalSolvability.X

  69. lemma OAI.ElasticityPhysicalSolvability.realSmooth_real line 605
  70. lemma OAI.ElasticityPhysicalSolvability.exterior_of_ball line 609
  71. theorem OAI.ElasticityPhysicalSolvability.real_weak_solvability line 618

    Source documentation

    Coefficient assumptions for this PDE lemma: smooth, strongly convex, constant outside a ball. No bounds on their derivatives are assumed.

    theorem real_weak_solvability (R : ℝ) (hR : 1 ≤ R) (α β : X) (hα : α ≠ 0)
    (lam m : X → ℝ) (hl : ContDiff ℝ (⊤ : ℕ∞) lam) (hm : ContDiff ℝ (⊤ : ℕ∞) m)
    (hpos : ∀ x, 0 < m x ∧ 0 < 3*lam x+2*m x)
    (Rext cl cm : ℝ) (hext : ∀ x, Rext ≤ ‖x‖ → lam x=cl ∧ m x=cm) :
    ∃ C h₀ : ℝ, 0 < C ∧ 0 < h₀ ∧ ∀ h : ℝ, 0 < h → h ≤ h₀ →
      ∀ F : H, ∃ w : H, ‖w‖ ≤ C*‖F‖ ∧ ∀ v : Fin 3 → S,
        (∀ i, BallSupported R (v i)) →
        inner ℂ w (embed (physical (adjPhase (phase h α β))
          (realSmooth lam hl) (realSmooth m hm) v)) = inner ℂ F (embed v) := by
…

    Mentions: OAI.ElasticityPhysicalSolvability.X, OAI.ElasticityPhysicalSolvability.realSmooth

  72. lemma OAI.ElasticityDistribution.lp_local_zero line 648
  73. lemma OAI.ElasticityDistribution.schwartz_local_nat line 651
  74. def OAI.ElasticityDistribution.exteriorCoeff line 658

    Source documentation

    Real physical coefficients and pointwise inverses are the actual smooth coefficients in the distribution formulation.

    def exteriorCoeff (f : Smooth) (hf : ExteriorConstant f) : Coeff := ⟨f,hf.growth⟩

    Mentions: OAI.ElasticityDistribution.Coeff

  75. def OAI.ElasticityDistribution.inverseCoeff line 659
  76. lemma OAI.ElasticityDistribution.inverseCoeff_mul line 661
  77. theorem OAI.ElasticityDistribution.weak_smooth_solvability line 670

    Source documentation

    Actual uniform physical weak solvability together with proved interior smoothness of every cutoff of the physical displacement and shifted divergence. This combines the supported Carleman/Hahn--Banach construction with the true augmented distribution identity rather than assuming elliptic regularity.

    theorem weak_smooth_solvability (R : ℝ) (hR : 1 ≤ R)
    (Ω : Set X) (hΩ : Ω ⊆ Metric.closedBall 0 R) (α β : X) (hα : α ≠ 0)
    (lam m : Smooth) (hl : ExteriorConstant lam) (hm : ExteriorConstant m)
    (hrl : ∀ x, star ((lam : X → ℂ) x)=(lam : X → ℂ) x)
    (hrm : ∀ x, star ((m : X → ℂ) x)=(m : X → ℂ) x)
    (hm0 : ∀ x, (m : X → ℂ) x ≠ 0)
    (he0 : ∀ x, ((lam+m+m : Smooth) : X → ℂ) x ≠ 0) :
    ∃ C h₀ : ℝ, 0 < C ∧ 0 < h₀ ∧ ∀ h : ℝ, 0 < h → h ≤ h₀ →
      ∀ f : Fin 3 → S, ∃ w : H, ‖w‖ ≤ C*‖embed f‖ ∧
        (∀ i, LocalEq Ω (phys (phase h α β) (exteriorCoeff lam hl) (exteriorCoeff m hm)
          (fun j => (w j : Dist)) i) (f i : Dist)) ∧
        ∀ i : Fin 4, ∀ g : X → ℂ, ContDiff ℝ (⊤ : ℕ∞) g → HasCompactSupport g → tsupport g ⊆ Ω →
…

    Mentions: OAI.ElasticityDistribution.X, OAI.ElasticityDistribution.S, OAI.ElasticityDistribution.H, OAI.ElasticityDistribution.LocalEq, OAI.ElasticityDistribution.phys, OAI.ElasticityDistribution.exteriorCoeff, OAI.ElasticityDistribution.Dist