OAI/MathematicalPhysics/Elasticity/Regularity.lean

GitHub source file

120 declarations, 0 contain sorry, 0 declared as axioms

Actual distributional elliptic regularity dependencies of the physical and planar weak-limit constructions. No regularity assumption on an L2 unknown is used in the gain of Sobolev order below.

  1. lemma OAI.ElasticityRegularity.fourierMultiplier_add line 22
  2. lemma OAI.ElasticityRegularity.besselPotential_two line 28
  3. lemma OAI.ElasticityRegularity.sobolev_real_smul line 37
  4. theorem OAI.ElasticityRegularity.laplacian_gain line 42

    Source documentation

    Whole-space elliptic gain for the actual distributional Laplacian.

    theorem laplacian_gain {s : ℝ} {u : 𝓱'(E,F)}
    (hu : MemSobolev s 2 u) (hΔ : MemSobolev s 2 (Δ u)) : MemSobolev (s+2) 2 u := by


  5. theorem OAI.ElasticityRegularity.coordinate_derivative_gain line 53

    Source documentation

    One derivative of gain from information on all coordinate first derivatives.

    theorem coordinate_derivative_gain {Îč : Type*} [Fintype Îč]
    (b : OrthonormalBasis Îč ℝ E) {s : ℝ} {u : 𝓱'(E,F)}
    (hu : MemSobolev s 2 u) (hd : ∀ i, MemSobolev s 2 (∂_{b i} u)) :
    MemSobolev (s+1) 2 u := by


  6. lemma OAI.ElasticityRegularity.compact_derivative line 78
  7. lemma OAI.ElasticityRegularity.smooth_derivative line 83
  8. lemma OAI.ElasticityRegularity.schwartz_leibniz line 88
  9. lemma OAI.ElasticityRegularity.distribution_leibniz line 104
  10. lemma OAI.ElasticityRegularity.compact_bounded_multiplier line 113
  11. lemma OAI.ElasticityRegularity.sobolev_zero_product line 123
  12. theorem OAI.ElasticityRegularity.sobolev_nat_product line 133

    Source documentation

    Smooth compact coefficients preserve every nonnegative integral Sobolev order. This is proved for the actual tempered distribution product, not an assumed bounded multiplier on an unspecified Sobolev completion.

    theorem sobolev_nat_product {Îč : Type*} [Fintype Îč] (b : OrthonormalBasis Îč ℝ E)
    (n : ℕ) {g : E → ℂ} (hg : ContDiff ℝ (⊀ : ℕ∞) g) (hc : HasCompactSupport g)
    {u : 𝓱'(E,F)} (hu : MemSobolev n 2 u) : MemSobolev n 2 (smulLeftCLM F g u) := by


  13. lemma OAI.ElasticityRegularity.sobolev_zero_product_derivative line 151
  14. abbrev OAI.ElasticityDistribution.X line 172
  15. abbrev OAI.ElasticityDistribution.Dist line 173
  16. def OAI.ElasticityDistribution.coefficientAlgebra line 176

    Source documentation

    Smooth temperate coefficients act on actual tempered distributions.

    def coefficientAlgebra : Subalgebra ℂ Smooth where


  17. abbrev OAI.ElasticityDistribution.Coeff line 183
  18. def OAI.ElasticityDistribution.eval line 185
  19. lemma OAI.ElasticityDistribution.growth line 186
  20. lemma OAI.ElasticityDistribution.eval_smooth line 187
  21. lemma OAI.ElasticityDistribution.eval_add line 189
  22. lemma OAI.ElasticityDistribution.eval_mul line 190
  23. lemma OAI.ElasticityDistribution.eval_one line 191
  24. instance OAI.ElasticityDistribution.(instance at line 193) line 193
  25. lemma OAI.ElasticityDistribution.smul_def line 194
  26. instance OAI.ElasticityDistribution.(instance at line 195) line 195
  27. instance OAI.ElasticityDistribution.(instance at line 204) line 204
  28. instance OAI.ElasticityDistribution.(instance at line 208) line 208
  29. def OAI.ElasticityDistribution.dc line 212

    Source documentation

    The coefficient derivative and distribution derivative are genuine derivatives.

    def dc (i : Fin 3) : Derivation ℂ Coeff Coeff := Derivation.mk' (R := ℂ) (A := Coeff) (M := Coeff)



    Mentions: OAI.ElasticityDistribution.Coeff

  30. def OAI.ElasticityDistribution.dd line 218
  31. lemma OAI.ElasticityDistribution.dd_apply line 219
  32. lemma OAI.ElasticityDistribution.dc_eval line 220
  33. lemma OAI.ElasticityDistribution.dc_commute line 221
  34. lemma OAI.ElasticityDistribution.dd_commute line 224
  35. lemma OAI.ElasticityDistribution.dd_leibniz line 230
  36. instance OAI.ElasticityDistribution.(instance at line 236) line 236
  37. instance OAI.ElasticityDistribution.(instance at line 237) line 237
  38. instance OAI.ElasticityDistribution.(instance at line 242) line 242
  39. instance OAI.ElasticityDistribution.(instance at line 244) line 244
  40. abbrev OAI.ElasticityDistribution.Ext line 247
  41. def OAI.ElasticityDistribution.de line 251

    Source documentation

    The square-zero algebra is only an algebraic way of reusing the physical compatibility identities: its genuine distribution component is never multiplied by another distribution.

    def de (i : Fin 3) : Derivation ℂ Ext Ext := Derivation.mk' (R := ℂ) (A := Ext) (M := Ext)



    Mentions: OAI.ElasticityDistribution.Ext

  42. lemma OAI.ElasticityDistribution.de_fst line 277
  43. lemma OAI.ElasticityDistribution.de_snd line 278
  44. lemma OAI.ElasticityDistribution.de_inl line 279
  45. lemma OAI.ElasticityDistribution.de_inr line 281
  46. lemma OAI.ElasticityDistribution.de_commute line 283
  47. def OAI.ElasticityDistribution.sd line 288
  48. lemma OAI.ElasticityDistribution.sd_apply line 289
  49. lemma OAI.ElasticityDistribution.shifted_inr line 290
  50. def OAI.ElasticityDistribution.lapd line 294
  51. def OAI.ElasticityDistribution.divd line 295
  52. def OAI.ElasticityDistribution.rd line 296
  53. def OAI.ElasticityDistribution.scd line 300
  54. def OAI.ElasticityDistribution.phys line 306
  55. lemma OAI.ElasticityDistribution.lapT_inr line 309
  56. lemma OAI.ElasticityDistribution.divT_inr line 312
  57. lemma OAI.ElasticityDistribution.LT_inr line 315
  58. lemma OAI.ElasticityDistribution.RT_inr line 318
  59. lemma OAI.ElasticityDistribution.ST_inr line 322
  60. theorem OAI.ElasticityDistribution.physical_expansion line 339

    Source documentation

    The genuine distributional physical equation has the same compatible augmented scalar-principal system as the smooth equation. No regularity of the unknown is used in this differential identity.

    theorem physical_expansion (z : Fin 3 → ℂ) (lam m : Coeff) (u : Fin 3 → Dist) (i : Fin 3) :
    phys z lam m u i = rd z lam m u (divd z u) i := by



    Mentions: OAI.ElasticityDistribution.Coeff, OAI.ElasticityDistribution.Dist, OAI.ElasticityDistribution.phys, OAI.ElasticityDistribution.rd, OAI.ElasticityDistribution.divd

  61. theorem OAI.ElasticityDistribution.physical_divergence line 345
  62. def OAI.ElasticityDistribution.normPair line 353
  63. lemma OAI.ElasticityDistribution.inl_two line 356
  64. lemma OAI.ElasticityDistribution.coff_inl_mul line 358
  65. lemma OAI.ElasticityDistribution.coff_inl_add line 360
  66. lemma OAI.ElasticityDistribution.coff_inl_sub line 362
  67. lemma OAI.ElasticityDistribution.dist_inr_sub line 364
  68. lemma OAI.ElasticityDistribution.coeff_two_smul line 366
  69. lemma OAI.ElasticityDistribution.coeffA_inl line 370
  70. lemma OAI.ElasticityDistribution.coeffV_inl line 377
  71. lemma OAI.ElasticityDistribution.normalizedPair_inr line 382
  72. theorem OAI.ElasticityDistribution.normalized_matrix line 396

    Source documentation

    Genuine scalar-principal matrix form for the actual distribution system.

    theorem normalized_matrix (z : Fin 3 → ℂ) (lam m n o : Coeff)
    (hn : n*m=1) (ho : o*(lam+m+m)=1) (U : Fin 4 → Dist) (i : Fin 4) :
    normPair z lam m n o (fun j => U j.succ) (U 0) i =
      lapd z (U i)+(∑ k, ∑ j, coeffA dc lam m n o k i j ‱ sd z k (U j))+
        (∑ j, coeffV dc lam m n o i j ‱ U j) := by



    Mentions: OAI.ElasticityDistribution.Coeff, OAI.ElasticityDistribution.Dist, OAI.ElasticityDistribution.normPair, OAI.ElasticityDistribution.lapd, OAI.ElasticityDistribution.dc, OAI.ElasticityDistribution.sd

  73. lemma OAI.ElasticityRegularity.sobolev_sum line 427
  74. theorem OAI.ElasticityRegularity.elliptic_all_orders line 441

    Source documentation

    Actual all-order elliptic bootstrap for scalar-principal systems. The unknown is only assumed to be represented by L2; its derivatives are the actual tempered-distribution derivatives. Compact smooth coefficients are sufficient for the localized physical augmented and planar systems.

    theorem elliptic_all_orders {Îč Îș : Type*} [Fintype Îč] [Fintype Îș]
    (b : OrthonormalBasis Îč ℝ E) (a : Îș → Îș → Îč → E → ℂ) (c : Îș → Îș → E → ℂ)
    (ha : ∀ i j d, ContDiff ℝ (⊀ : ℕ∞) (a i j d)) (hac : ∀ i j d, HasCompactSupport (a i j d))
    (hc : ∀ i j, ContDiff ℝ (⊀ : ℕ∞) (c i j)) (hcc : ∀ i j, HasCompactSupport (c i j))
    (f : Îș → 𝓱(E,F)) (u : Îș → 𝓱'(E,F)) (hu : ∀ i, MemSobolev 0 2 (u i))
    (heq : ∀ i, Δ (u i) = (∑ j, ∑ d, smulLeftCLM F (a i j d) (∂_{b d} (u j)))+
      (∑ j, smulLeftCLM F (c i j) (u j))+(f i : 𝓱'(E,F))) :
    ∀ n : ℕ, ∀ i, MemSobolev n 2 (u i) := by


  75. lemma OAI.ElasticityRegularity.decay_memLp line 488
  76. lemma OAI.ElasticityRegularity.weighted_decay_bound line 507
  77. lemma OAI.ElasticityRegularity.all_orders_fourier_moments line 519
  78. lemma OAI.ElasticityRegularity.l1_inverse_fourier_distribution line 583
  79. theorem OAI.ElasticityRegularity.all_orders_smooth_representative line 610

    Source documentation

    A tempered distribution lying in all integral Sobolev spaces has an actual bounded smooth representative. All moments of a single L1 Fourier representative are proved first, so the smooth representatives do not depend on the order.

    theorem all_orders_smooth_representative {u : 𝓱'(E,F)}
    (hu : ∀ n : ℕ, MemSobolev n 2 u) :
    ∃ g : BoundedContinuousFunction E F, ContDiff ℝ (⊀ : ℕ∞) (g : E → F) ∧
      u = ((g.memLp_top.toLp _ : Lp F ∞ (volume : Measure E)) : 𝓱'(E,F)) := by


  80. def OAI.ElasticityRegularity.LocalSobolev line 629

    Source documentation

    Local Bessel-potential regularity, using actual compact smooth multipliers.

    def LocalSobolev (Ω : Set E) (s : ℝ) (u : 𝓱'(E,F)) : Prop :=


  81. lemma OAI.ElasticityRegularity.derivative_support_subset line 634
  82. lemma OAI.ElasticityRegularity.LocalSobolev.mono line 639
  83. lemma OAI.ElasticityRegularity.LocalSobolev.product_derivative line 643
  84. lemma OAI.ElasticityRegularity.laplacian_product line 656
  85. def OAI.ElasticityRegularity.LocalEllipticEquation line 676

    Source documentation

    Local distributional equation with scalar Laplacian principal part. The coefficients need only be globally smooth: cutoff multiplication, not a hidden boundedness or temperedness condition, defines every coefficient product.

    def LocalEllipticEquation {Îč Îș : Type*} [Fintype Îč] [Fintype Îș]
    (Ω : Set E) (b : OrthonormalBasis Îč ℝ E)
    (a : Îș → Îș → Îč → E → ℂ) (c : Îș → Îș → E → ℂ) (f u : Îș → 𝓱'(E,F)) : Prop :=


  86. theorem OAI.ElasticityRegularity.local_elliptic_gain line 686

    Source documentation

    One full local Sobolev order of elliptic gain, including the initial L2-to-H1 step. This uses no regularity of the unknown beyond the stated order.

    theorem local_elliptic_gain {Îč Îș : Type*} [Fintype Îč] [Fintype Îș]
    {Ω : Set E} (b : OrthonormalBasis Îč ℝ E)
    (a : Îș → Îș → Îč → E → ℂ) (c : Îș → Îș → E → ℂ)
    (ha : ∀ i j d, ContDiff ℝ (⊀ : ℕ∞) (a i j d))
    (hc : ∀ i j, ContDiff ℝ (⊀ : ℕ∞) (c i j))
    {f u : Îș → 𝓱'(E,F)} (heq : LocalEllipticEquation Ω b a c f u)
    {s : ℝ} (hu : ∀ i, LocalSobolev Ω s (u i))
    (hf : ∀ i, LocalSobolev Ω (s-1) (f i)) :
    ∀ i, LocalSobolev Ω (s+1) (u i) := by



    Mentions: OAI.ElasticityRegularity.LocalEllipticEquation, OAI.ElasticityRegularity.LocalSobolev

  87. abbrev OAI.ElasticityDistribution.Test line 725
  88. def OAI.ElasticityDistribution.LocalEq line 728

    Source documentation

    Equality of actual distributions tested strictly within the open domain.

    def LocalEq (Ω : Set X) (u v : Dist) : Prop :=



    Mentions: OAI.ElasticityDistribution.X, OAI.ElasticityDistribution.Dist

  89. lemma OAI.ElasticityDistribution.LocalEq.refl line 732
  90. lemma OAI.ElasticityDistribution.LocalEq.symm line 733
  91. lemma OAI.ElasticityDistribution.LocalEq.trans line 734
  92. lemma OAI.ElasticityDistribution.LocalEq.add line 736
  93. lemma OAI.ElasticityDistribution.LocalEq.sub line 739
  94. lemma OAI.ElasticityDistribution.LocalEq.smul line 742
  95. lemma OAI.ElasticityDistribution.LocalEq.sum line 745
  96. lemma OAI.ElasticityDistribution.LocalEq.coeff line 750
  97. lemma OAI.ElasticityDistribution.LocalEq.derivative line 758
  98. lemma OAI.ElasticityDistribution.LocalEq.cutoff line 767
  99. lemma OAI.ElasticityDistribution.LocalEq.shifted line 779
  100. lemma OAI.ElasticityDistribution.LocalEq.divergence line 782
  101. def OAI.ElasticityDistribution.normSource line 786
  102. theorem OAI.ElasticityDistribution.local_normalized_system line 791

    Source documentation

    The local physical stress-divergence equation implies the true normalized augmented equation. The fourth component is the actual shifted divergence.

    theorem local_normalized_system {Ω : Set X} (z : Fin 3 → ℂ) (lam m n o : Coeff)
    (u F : Fin 3 → Dist) (h : ∀ i, LocalEq Ω (phys z lam m u i) (F i)) :
    ∀ i, LocalEq Ω (normPair z lam m n o u (divd z u) i) (normSource z m n o F i) := by



    Mentions: OAI.ElasticityDistribution.X, OAI.ElasticityDistribution.Coeff, OAI.ElasticityDistribution.Dist, OAI.ElasticityDistribution.LocalEq, OAI.ElasticityDistribution.phys, OAI.ElasticityDistribution.normPair, OAI.ElasticityDistribution.divd, OAI.ElasticityDistribution.normSource

  103. lemma OAI.ElasticityDistribution.lapd_expand line 805
  104. lemma OAI.ElasticityRegularity.MemSobolev.local_zero line 825
  105. theorem OAI.ElasticityRegularity.local_elliptic_all_orders line 830
  106. theorem OAI.ElasticityRegularity.local_elliptic_cutoff_smooth line 850

    Source documentation

    The actual cutoff of an L2 weak solution is represented by one bounded smooth function, simultaneously at all Sobolev orders. This is the distributional interior-regularity conclusion used for physical correction and planar limits.

    theorem local_elliptic_cutoff_smooth {Îč Îș : Type*} [Fintype Îč] [Fintype Îș]
    {Ω : Set E} (b : OrthonormalBasis Îč ℝ E)
    (a : Îș → Îș → Îč → E → ℂ) (c : Îș → Îș → E → ℂ)
    (ha : ∀ i j d, ContDiff ℝ (⊀ : ℕ∞) (a i j d))
    (hc : ∀ i j, ContDiff ℝ (⊀ : ℕ∞) (c i j))
    {f u : Îș → 𝓱'(E,F)} (heq : LocalEllipticEquation Ω b a c f u)
    (hu : ∀ i, LocalSobolev Ω 0 (u i))
    (hf : ∀ n : ℕ, ∀ i, LocalSobolev Ω n (f i))
    (i : Îș) {g : E → ℂ} (hg : ContDiff ℝ (⊀ : ℕ∞) g)
    (hgc : HasCompactSupport g) (hgs : tsupport g ⊆ Ω) :
    ∃ v : BoundedContinuousFunction E F, ContDiff ℝ (⊀ : ℕ∞) (v : E → F) ∧
      smulLeftCLM F g (u i) = ((v.memLp_top.toLp _ : Lp F ∞ (volume : Measure E)) : 𝓱'(E,F)) := by



    Mentions: OAI.ElasticityRegularity.LocalEllipticEquation, OAI.ElasticityRegularity.LocalSobolev

  107. lemma OAI.ElasticityDistribution.LocalSobolev.add line 875
  108. lemma OAI.ElasticityDistribution.LocalSobolev.sub line 881
  109. lemma OAI.ElasticityDistribution.LocalSobolev.smul line 887
  110. lemma OAI.ElasticityDistribution.LocalSobolev.sum line 892
  111. lemma OAI.ElasticityDistribution.LocalSobolev.coeff line 898
  112. lemma OAI.ElasticityDistribution.LocalSobolev.derivative line 905
  113. lemma OAI.ElasticityDistribution.LocalSobolev.shifted line 909
  114. lemma OAI.ElasticityDistribution.LocalSobolev.divergence line 912
  115. lemma OAI.ElasticityDistribution.LocalEq.localSobolev line 917
  116. theorem OAI.ElasticityDistribution.local_laplacian_gain line 925

    Source documentation

    Local gain from an actual distributional Laplacian; includes negative order starting points. The cutoff commutator is proved, not silently discarded.

    theorem local_laplacian_gain {Ω : Set X} {s : ℝ} {u : Dist}
    (hu : ElasticityRegularity.LocalSobolev Ω s u)
    (hΔ : ElasticityRegularity.LocalSobolev Ω (s-1) (Δ u)) :
    ElasticityRegularity.LocalSobolev Ω (s+1) u := by



    Mentions: OAI.ElasticityDistribution.X, OAI.ElasticityDistribution.Dist, OAI.ElasticityRegularity.LocalSobolev

  117. lemma OAI.ElasticityDistribution.normSource_local line 946
  118. theorem OAI.ElasticityDistribution.normalized_local_gain line 958

    Source documentation

    Interior elliptic gain for the genuine normalized physical distribution system, with no solution-regularity premise hidden in the equation.

    theorem normalized_local_gain {Ω : Set X} {s : ℝ} (z : Fin 3 → ℂ) (lam m n o : Coeff)
    (hn : n*m=1) (ho : o*(lam+m+m)=1) (U F : Fin 4 → Dist)
    (heq : ∀ i, LocalEq Ω (normPair z lam m n o (fun j => U j.succ) (U 0) i) (F i))
    (hU : ∀ i, ElasticityRegularity.LocalSobolev Ω s (U i))
    (hF : ∀ i, ElasticityRegularity.LocalSobolev Ω (s-1) (F i)) :
    ∀ i, ElasticityRegularity.LocalSobolev Ω (s+1) (U i) := by



    Mentions: OAI.ElasticityDistribution.X, OAI.ElasticityDistribution.Coeff, OAI.ElasticityDistribution.Dist, OAI.ElasticityDistribution.LocalEq, OAI.ElasticityDistribution.normPair, OAI.ElasticityRegularity.LocalSobolev

  119. theorem OAI.ElasticityDistribution.physical_local_all_orders line 997

    Source documentation

    All local Sobolev orders for an L2 physical solution with smooth source. The physical fourth unknown is the actual shifted divergence, initially H^-1, not an independent L2 unknown postulated as a hypothesis.

    theorem physical_local_all_orders {Ω : Set X} (z : Fin 3 → ℂ) (lam m n o : Coeff)
    (hn : n*m=1) (ho : o*(lam+m+m)=1) (u F : Fin 3 → Dist)
    (heq : ∀ i, LocalEq Ω (phys z lam m u i) (F i))
    (hu : ∀ i, ElasticityRegularity.LocalSobolev Ω 0 (u i))
    (hf : ∀ N : ℕ, ∀ i, ElasticityRegularity.LocalSobolev Ω N (F i)) :
    ∀ N : ℕ, ∀ i, ElasticityRegularity.LocalSobolev Ω N ((Fin.cons (divd z u) u : Fin 4 → Dist) i) := by



    Mentions: OAI.ElasticityDistribution.X, OAI.ElasticityDistribution.Coeff, OAI.ElasticityDistribution.Dist, OAI.ElasticityDistribution.LocalEq, OAI.ElasticityDistribution.phys, OAI.ElasticityRegularity.LocalSobolev, OAI.ElasticityDistribution.divd

  120. theorem OAI.ElasticityDistribution.physical_cutoff_smooth line 1028

    Source documentation

    Every compact cutoff of the actual augmented physical unknown has a single bounded smooth representative. This is a conclusion, not an assumed classical regularity theorem.

    theorem physical_cutoff_smooth {Ω : Set X} (z : Fin 3 → ℂ) (lam m n o : Coeff)
    (hn : n*m=1) (ho : o*(lam+m+m)=1) (u F : Fin 3 → Dist)
    (heq : ∀ i, LocalEq Ω (phys z lam m u i) (F i))
    (hu : ∀ i, ElasticityRegularity.LocalSobolev Ω 0 (u i))
    (hf : ∀ N : ℕ, ∀ i, ElasticityRegularity.LocalSobolev Ω N (F i))
    (i : Fin 4) {g : X → ℂ} (hg : ContDiff ℝ (⊀ : ℕ∞) g)
    (hgc : HasCompactSupport g) (hgs : tsupport g ⊆ Ω) :
    ∃ v : BoundedContinuousFunction X ℂ, ContDiff ℝ (⊀ : ℕ∞) (v : X → ℂ) ∧
      smulLeftCLM ℂ g ((Fin.cons (divd z u) u : Fin 4 → Dist) i) =
        ((v.memLp_top.toLp _ : Lp ℂ ∞ (volume : Measure X)) : Dist) := by



    Mentions: OAI.ElasticityDistribution.X, OAI.ElasticityDistribution.Coeff, OAI.ElasticityDistribution.Dist, OAI.ElasticityDistribution.LocalEq, OAI.ElasticityDistribution.phys, OAI.ElasticityRegularity.LocalSobolev, OAI.ElasticityDistribution.divd