OAI/MathematicalPhysics/Elasticity/Planar.lean

GitHub source file

135 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ElasticityRegularity.exists_smooth_lp_multiplier line 16

   Source documentation

   A joint smooth compactly spatially supported coefficient yields a genuinely operator-norm-smooth family of actual L2 multipliers.

   theorem exists_smooth_lp_multiplier {S : Set E} (hS : IsCompact S)
       (a : P × E → ℂ) (ha : ContDiff ℝ (⊤ : ℕ∞) a)
       (hs : ∀ p x, x∉S → a (p,x)=0) :
       ∃ M : P → Lp ℂ 2 (volume : Measure E) →L[ℂ] Lp ℂ 2 (volume : Measure E),
         ContDiff ℝ (⊤ : ℕ∞) M ∧ ∀ p f,
           (M p f : 𝓢'(E,ℂ))=smulLeftCLM ℂ (fun x => a (p,x)) (f : 𝓢'(E,ℂ)) := by
   …

2. def OAI.ElasticityPlanar.testSubmodule line 49
3. abbrev OAI.ElasticityPlanar.Test line 66
4. instance OAI.ElasticityPlanar.(instance at line 68) line 68
5. lemma OAI.ElasticityPlanar.smooth line 70
6. lemma OAI.ElasticityPlanar.compact line 71
7. def OAI.ElasticityPlanar.d line 73
8. lemma OAI.ElasticityPlanar.d_apply line 90
9. def OAI.ElasticityPlanar.mulSmooth line 93
10. def OAI.ElasticityPlanar.Z line 105
11. def OAI.ElasticityPlanar.Zbar line 106
12. lemma OAI.ElasticityPlanar.Z_apply line 108
13. lemma OAI.ElasticityPlanar.Zbar_apply line 109
14. lemma OAI.ElasticityPlanar.d_Z line 111
15. lemma OAI.ElasticityPlanar.deriv_conj line 119
16. lemma OAI.ElasticityPlanar.d_Zbar line 125
17. lemma OAI.ElasticityPlanar.d_d line 134
18. lemma OAI.ElasticityPlanar.d_comm line 142
19. def OAI.ElasticityPlanar.pair line 150
20. lemma OAI.ElasticityPlanar.integrable_pair line 152
21. lemma OAI.ElasticityPlanar.pair_add_right line 155
22. lemma OAI.ElasticityPlanar.pair_add_left line 159
23. lemma OAI.ElasticityPlanar.pair_sub_right line 163
24. lemma OAI.ElasticityPlanar.pair_sub_left line 167
25. lemma OAI.ElasticityPlanar.pair_smul_right line 171
26. lemma OAI.ElasticityPlanar.pair_smul_left line 176
27. lemma OAI.ElasticityPlanar.pair_d line 181

    Source documentation

    Coordinate derivatives are skew adjoint on the actual test space.

    lemma pair_d (f g : Test) (v : ℂ) : pair f (d v g) = -pair (d v f) g := by
    …

    Mentions: OAI.ElasticityPlanar.Test, OAI.ElasticityPlanar.pair, OAI.ElasticityPlanar.d

28. lemma OAI.ElasticityPlanar.pair_Z line 191
29. lemma OAI.ElasticityPlanar.pair_Zbar line 196
30. def OAI.ElasticityPlanar.B line 202

    Source documentation

    Twice dbar conjugated by exp(t|z|²/2).

    def B (t : ℝ) : Test →ₗ[ℂ] Test := d 1 + Complex.I • d Complex.I - (t : ℂ) • Z

    Mentions: OAI.ElasticityPlanar.Test, OAI.ElasticityPlanar.d, OAI.ElasticityPlanar.Z

31. def OAI.ElasticityPlanar.C line 204

    Source documentation

    Formal Hermitian adjoint.

    def C (t : ℝ) : Test →ₗ[ℂ] Test := -d 1 + Complex.I • d Complex.I - (t : ℂ) • Zbar

    Mentions: OAI.ElasticityPlanar.Test, OAI.ElasticityPlanar.d, OAI.ElasticityPlanar.Zbar

32. lemma OAI.ElasticityPlanar.pair_B line 206
33. lemma OAI.ElasticityPlanar.pair_C line 214
34. lemma OAI.ElasticityPlanar.Z_Zbar line 221
35. lemma OAI.ElasticityPlanar.commutator line 228

    Source documentation

    Positive commutator of the two Gaussian-conjugated planar operators.

    lemma commutator (t : ℝ) (f : Test) :
        C t (B t f) - B t (C t f) = (4 * (t : ℂ)) • f := by
    …

    Mentions: OAI.ElasticityPlanar.Test, OAI.ElasticityPlanar.C, OAI.ElasticityPlanar.B

36. lemma OAI.ElasticityPlanar.energy_identity line 240
37. def OAI.ElasticityPlanar.mass line 248
38. lemma OAI.ElasticityPlanar.mass_integral line 250
39. lemma OAI.ElasticityPlanar.integrable_normSq line 255
40. lemma OAI.ElasticityPlanar.mass_nonneg line 260
41. lemma OAI.ElasticityPlanar.mass_eq_zero line 264
42. theorem OAI.ElasticityPlanar.gaussian_coercivity line 275

    Source documentation

    An actual weighted support estimate, independent of any frame existence.

    theorem gaussian_coercivity (t : ℝ) (f : Test) :
        4 * t * mass f ≤ mass (B t f) := by
    …

    Mentions: OAI.ElasticityPlanar.Test, OAI.ElasticityPlanar.mass, OAI.ElasticityPlanar.B

43. def OAI.ElasticityPlanar.gaussian line 283
44. lemma OAI.ElasticityPlanar.smooth_gaussian line 286
45. def OAI.ElasticityPlanar.W line 289
46. lemma OAI.ElasticityPlanar.W_apply line 291
47. lemma OAI.ElasticityPlanar.gaussian_ne_zero line 294
48. lemma OAI.ElasticityPlanar.fderiv_gaussian line 296
49. lemma OAI.ElasticityPlanar.d_W line 309
50. lemma OAI.ElasticityPlanar.gaussian_conjugation line 323

    Source documentation

    Exact Gaussian conjugation of twice the planar Cauchy--Riemann operator.

    lemma gaussian_conjugation (t : ℝ) (f : Test) :
        B t (W t f) = W t (d 1 f + I • d I f) := by
    …

    Mentions: OAI.ElasticityPlanar.Test, OAI.ElasticityPlanar.B, OAI.ElasticityPlanar.W, OAI.ElasticityPlanar.d

51. lemma OAI.ElasticityPlanar.normSq_sum_mul line 338
52. lemma OAI.ElasticityPlanar.mass_bound line 347
53. theorem OAI.ElasticityPlanar.compact_kernel_of_bound line 361

    Source documentation

    Compact-kernel uniqueness with a coefficient bound only where a column is nonzero. This is a genuine analytic theorem, not an assumed continuation rule.

    theorem compact_kernel_of_bound {n : Type*} [Fintype n]
        (a : n → n → ℂ → ℂ) (u : n → Test) (K : ℝ)
        (hb : ∀ z : ℂ, (∃ j, u j z ≠ 0) → ∀ i,
          (∑ j, Complex.normSq (a i j z)) ≤ K)
        (heq : ∀ i (z : ℂ),
          (d 1 (u i) + I • d I (u i) : Test) z = ∑ j, a i j z * u j z) :
        ∀ i, u i = 0 := by
    …

    Mentions: OAI.ElasticityPlanar.Test, OAI.ElasticityPlanar.d

54. theorem OAI.ElasticityPlanar.compact_kernel line 431

    Source documentation

    A smooth compactly supported solution of a planar matrix Cauchy--Riemann system with continuous coefficients is zero. No smallness is imposed.

    theorem compact_kernel {n : Type*} [Fintype n]
        (a : n → n → ℂ → ℂ) (ha : ∀ i j, Continuous (a i j))
        (u : n → Test)
        (heq : ∀ i (z : ℂ),
          (d 1 (u i) + I • d I (u i) : Test) z = ∑ j, a i j z * u j z) :
        ∀ i, u i = 0 := by
    …

    Mentions: OAI.ElasticityPlanar.Test, OAI.ElasticityPlanar.d

55. lemma OAI.ElasticityPlanar.normSq_add_le line 464
56. lemma OAI.ElasticityPlanar.mass_add_le line 470
57. lemma OAI.ElasticityPlanar.mass_mul_bound line 480
58. lemma OAI.ElasticityPlanar.mass_smul line 484
59. lemma OAI.ElasticityPlanar.pair_derivative_cross line 489
60. lemma OAI.ElasticityPlanar.dbar_energy line 496

    Source documentation

    The exact two-dimensional elliptic energy identity for the actual dbar operator.

    lemma dbar_energy (f : Test) :
        mass (d 1 f + I • d I f)=mass (d 1 f)+mass (d I f) := by
    …

    Mentions: OAI.ElasticityPlanar.Test, OAI.ElasticityPlanar.mass, OAI.ElasticityPlanar.d

61. theorem OAI.ElasticityPlanar.weighted_inhomogeneous_bound line 510

    Source documentation

    Quantitative Gaussian absorption for a system with no smallness of coefficients.

    theorem weighted_inhomogeneous_bound {n : Type*} [Fintype n]
        (a : n → n → ℂ → ℂ) (u v : n → Test) (K : ℝ) (hK : 0 ≤ K)
        (hb : ∀ z, (∃ j, u j z ≠ 0) → ∀ i, (∑ j, normSq (a i j z)) ≤ K)
        (heq : ∀ i z, (d 1 (u i)+I • d I (u i) : Test) z =
          v i z+∑ j, a i j z*u j z) :
        let t := (Fintype.card n : ℝ)*K+1
    …

    Mentions: OAI.ElasticityPlanar.Test, OAI.ElasticityPlanar.d

62. lemma OAI.ElasticityPlanar.gaussian_inv line 568
63. lemma OAI.ElasticityPlanar.supported_weight_bound line 575
64. lemma OAI.ElasticityPlanar.supported_weight_equivalence line 592
65. lemma OAI.ElasticityPlanar.matrix_bound_on_compact line 613
66. theorem OAI.ElasticityPlanar.supported_inhomogeneous_L2 line 631

    Source documentation

    A true unweighted supported L2 estimate, uniform over all test columns on a fixed compact set, for an arbitrary continuous matrix coefficient.

    theorem supported_inhomogeneous_L2 {n : Type*} [Fintype n]
        {S : Set ℂ} (hS : IsCompact S) (a : n → n → ℂ → ℂ)
        (ha : ∀ i j, Continuous (a i j)) :
        ∃ C : ℝ, 0<C ∧ ∀ u v : n → Test,
          (∀ i, tsupport (u i : ℂ → ℂ) ⊆ S) →
          (∀ i, tsupport (v i : ℂ → ℂ) ⊆ S) →
          (∀ i z, (d 1 (u i)+I • d I (u i) : Test) z=v i z+∑ j, a i j z*u j z) →
          (∑ i, mass (u i)) ≤ C*∑ i, mass (v i) := by
    …

    Mentions: OAI.ElasticityPlanar.C, OAI.ElasticityPlanar.Test, OAI.ElasticityPlanar.d, OAI.ElasticityPlanar.mass

67. lemma OAI.ElasticityDualSolvability.weak_unique_in_range line 665
68. theorem OAI.ElasticityDualSolvability.exists_linear_weak_solver line 679

    Source documentation

    Hilbert projection makes the actual Hahn--Banach solver canonical and linear. It will be used for smooth parameter dependence of the planar right inverse.

    theorem exists_linear_weak_solver (D : Submodule ℂ H) (A : D →ₗ[ℂ] H)
        (C : ℝ) (hC : 0 ≤ C) (hA : ∀ v : D, ‖(v : H)‖ ≤ C*‖A v‖) :
        ∃ T : H →L[ℂ] H, ‖T‖ ≤ C ∧ ∀ f v, inner ℂ (T f) (A v)=inner ℂ f (v : H) := by
    …

69. def OAI.ElasticityPlanar.toSchwartz line 713
70. lemma OAI.ElasticityPlanar.toSchwartz_apply line 717
71. lemma OAI.ElasticityPlanar.toSchwartz_injective line 718
72. def OAI.ElasticityPlanar.L2 line 723
73. lemma OAI.ElasticityPlanar.L2_injective line 725
74. lemma OAI.ElasticityPlanar.inner_L2 line 726
75. lemma OAI.ElasticityPlanar.norm_L2_sq line 730
76. def OAI.ElasticityPlanar.cj line 734
77. lemma OAI.ElasticityPlanar.cj_apply line 736
78. lemma OAI.ElasticityPlanar.cj_cj line 737
79. lemma OAI.ElasticityPlanar.cj_d line 738
80. lemma OAI.ElasticityPlanar.cj_add line 742
81. lemma OAI.ElasticityPlanar.cj_neg line 743
82. lemma OAI.ElasticityPlanar.cj_smul line 744
83. lemma OAI.ElasticityPlanar.mass_cj line 749
84. lemma OAI.ElasticityPlanar.support_cj line 754
85. abbrev OAI.ElasticityPlanar.Hilbert line 761
86. def OAI.ElasticityPlanar.embed line 762
87. lemma OAI.ElasticityPlanar.embed_apply line 766
88. lemma OAI.ElasticityPlanar.embed_injective line 767
89. lemma OAI.ElasticityPlanar.norm_embed_sq line 772
90. lemma OAI.ElasticityPlanar.norm_embed_cj line 775
91. def OAI.ElasticityPlanar.transport line 781

    Source documentation

    Actual first-order matrix transport on compactly supported smooth tests.

    def transport (a : n → n → ℂ → ℂ) (ha : ∀ i j, ContDiff ℝ (⊤ : ℕ∞) (a i j)) :
        (n → Test) →ₗ[ℂ] (n → Test) where
    …

    Mentions: OAI.ElasticityPlanar.Test

92. lemma OAI.ElasticityPlanar.transport_supported line 792
93. theorem OAI.ElasticityPlanar.supported_transport_estimate line 813

    Source documentation

    A true L2 lower bound for the actual transport operator.

    theorem supported_transport_estimate {S : Set ℂ} (hS : IsCompact S)
        (a : n → n → ℂ → ℂ) (ha : ∀ i j, ContDiff ℝ (⊤ : ℕ∞) (a i j)) :
        ∃ C : ℝ, 0<C ∧ ∀ u : n → Test, (∀ i, tsupport (u i : ℂ → ℂ) ⊆ S) →
          ‖embed u‖ ≤ C*‖embed (transport a ha u)‖ := by
    …

    Mentions: OAI.ElasticityPlanar.C, OAI.ElasticityPlanar.Test, OAI.ElasticityPlanar.embed, OAI.ElasticityPlanar.transport

94. def OAI.ElasticityPlanar.adjTransport line 839

    Source documentation

    The genuine Hermitian formal adjoint of dbar+a, written using conjugation and the transpose coefficient. No elliptic right inverse is assumed.

    def adjTransport (a : n → n → ℂ → ℂ) (ha : ∀ i j, ContDiff ℝ (⊤ : ℕ∞) (a i j)) :
        (n → Test) →ₗ[ℂ] (n → Test) where
    …

    Mentions: OAI.ElasticityPlanar.Test

95. lemma OAI.ElasticityPlanar.norm_adjTransport line 856
96. def OAI.ElasticityPlanar.supported line 863

    Source documentation

    Supported test vectors form the actual L2 domain for the adjoint.

    def supported (S : Set ℂ) : Submodule ℂ (n → Test) where
    …

    Mentions: OAI.ElasticityPlanar.Test

97. theorem OAI.ElasticityPlanar.exists_planar_weak_inverse line 872

    Source documentation

    Actual supported matrix transport has a bounded linear L2 weak right inverse. The estimate comes from the proved Gaussian positive commutator, not a smallness assumption or a globally given frame.

    theorem exists_planar_weak_inverse {S : Set ℂ} (hS : IsCompact S)
        (a : n → n → ℂ → ℂ) (ha : ∀ i j, ContDiff ℝ (⊤ : ℕ∞) (a i j)) :
        ∃ C : ℝ, 0<C ∧ ∃ T : Hilbert n →L[ℂ] Hilbert n, ‖T‖ ≤ C ∧
          ∀ f : Hilbert n, ∀ u : n → Test, (∀ i, tsupport (u i : ℂ → ℂ) ⊆ S) →
            inner ℂ (T f) (embed (adjTransport a ha u))=inner ℂ f (embed u) := by
    …

    Mentions: OAI.ElasticityPlanar.C, OAI.ElasticityPlanar.Hilbert, OAI.ElasticityPlanar.Test, OAI.ElasticityPlanar.embed, OAI.ElasticityPlanar.adjTransport

98. abbrev OAI.ElasticityPlanarDistribution.Test line 906
99. abbrev OAI.ElasticityPlanarDistribution.Dist line 907
100. def OAI.ElasticityPlanarDistribution.dbar line 908
101. def OAI.ElasticityPlanarDistribution.dhol line 909
102. lemma OAI.ElasticityPlanarDistribution.schwartz_derivative_commute line 911
103. lemma OAI.ElasticityPlanarDistribution.derivative_commute line 923
104. lemma OAI.ElasticityPlanarDistribution.dhol_dbar line 928
105. lemma OAI.ElasticityPlanarDistribution.dhol_sum line 935
106. lemma OAI.ElasticityPlanarDistribution.dhol_add line 938
107. lemma OAI.ElasticityPlanarDistribution.LocalEqual.dhol line 941
108. lemma OAI.ElasticityPlanarDistribution.LocalSobolev.dhol line 944
109. def OAI.ElasticityPlanarDistribution.Equation line 950

     Source documentation

     Actual planar first-order equation on distributions, not an abstract regularity or frame existence interface.

     def Equation {n : Type*} [Fintype n] (Ω : Set ℂ) (a : n → n → ℂ → ℂ) (u f : n → Dist) : Prop :=
     …

     Mentions: OAI.ElasticityPlanarDistribution.Dist

110. theorem OAI.ElasticityPlanarDistribution.local_gain line 953
111. theorem OAI.ElasticityPlanarDistribution.local_all_orders line 967
112. theorem OAI.ElasticityPlanarDistribution.cutoff_smooth line 980
113. lemma OAI.ElasticityPlanar.toSchwartz_d line 996
114. lemma OAI.ElasticityPlanar.toSchwartz_mul line 999
115. lemma OAI.ElasticityPlanar.Lp_test line 1004
116. lemma OAI.ElasticityPlanar.vector_transpose line 1014
117. lemma OAI.ElasticityPlanar.weak_to_vector_distribution line 1034
118. lemma OAI.ElasticityPlanar.weak_to_local_equation line 1053
119. theorem OAI.ElasticityRegularity.exists_continuous_lift line 1079

     Source documentation

     The closed graph argument supplies norms for genuine distribution operators, not additional quantitative regularity assumptions.

     theorem exists_continuous_lift
         {X Y Z : Type*} [NormedAddCommGroup X] [NormedSpace ℂ X] [CompleteSpace X]
         [NormedAddCommGroup Y] [NormedSpace ℂ Y] [CompleteSpace Y]
         [AddCommGroup Z] [Module ℂ Z] [TopologicalSpace Z] [T2Space Z]
         (J : Y →L[ℂ] Z) (hJ : Function.Injective J) (T : X →L[ℂ] Z)
         (hT : ∀ x, ∃ y, J y=T x) :
         ∃ L : X →L[ℂ] Y, ∀ x, J (L x)=T x := by
     …

120. lemma OAI.ElasticityRegularity.lp_distribution_injective line 1109
121. def OAI.ElasticityRegularity.sobolevInjection line 1120

     Source documentation

     H^s is represented isometrically by L2 via J^{-s}; its injection is into the actual space of tempered distributions.

     def sobolevInjection (s : ℝ) : Lp ℂ 2 (volume : Measure E) →L[ℂ] 𝓢'(E,ℂ) :=
     …

122. lemma OAI.ElasticityRegularity.sobolevInjection_injective line 1123
123. lemma OAI.ElasticityRegularity.sobolevInjection_mem line 1133
124. lemma OAI.ElasticityRegularity.memSobolev_iff_range line 1140
125. theorem OAI.ElasticityRegularity.exists_sobolev_realization line 1153

     Source documentation

     A qualitative everywhere-defined Sobolev mapping theorem for a continuous actual distribution operator automatically gives its bounded Sobolev realization. This is useful for smooth multipliers and coordinate derivatives on cutoffs.

     theorem exists_sobolev_realization (s t : ℝ) (P : 𝓢'(E,ℂ) →L[ℂ] 𝓢'(E,ℂ))
         (hP : ∀ u, MemSobolev s 2 u → MemSobolev t 2 (P u)) :
         ∃ L : Lp ℂ 2 (volume : Measure E) →L[ℂ] Lp ℂ 2 (volume : Measure E),
           ∀ f, sobolevInjection t (L f)=P (sobolevInjection s f) := by
     …

     Mentions: OAI.ElasticityRegularity.sobolevInjection

126. theorem OAI.ElasticityRegularity.exists_bounded_sobolev_derivative line 1161
127. theorem OAI.ElasticityRegularity.exists_bounded_sobolev_inclusion line 1167
128. theorem OAI.ElasticityRegularity.sobolev_neg_one_product line 1184

     Source documentation

     Compact smooth multiplication on the negative initial Sobolev order in which the physical divergence is initially controlled.

     theorem sobolev_neg_one_product {g : E → ℂ}
         (hg : ContDiff ℝ (⊤ : ℕ∞) g) (hc : HasCompactSupport g)
         {u : 𝓢'(E,ℂ)} (hu : MemSobolev (-1) 2 u) :
         MemSobolev (-1) 2 (smulLeftCLM ℂ g u) := by
     …

129. lemma OAI.ElasticityRegularity.sobolev_product_step_down line 1213
130. theorem OAI.ElasticityRegularity.sobolev_negative_product line 1252

     Source documentation

     Smooth compact multiplication preserves every integral Sobolev order, including the H^-2 forcing order in the first augmented bootstrap step.

     theorem sobolev_negative_product (n : ℕ) {g : E → ℂ}
         (hg : ContDiff ℝ (⊤ : ℕ∞) g) (hc : HasCompactSupport g)
         {u : 𝓢'(E,ℂ)} (hu : MemSobolev (-(n : ℝ)) 2 u) :
         MemSobolev (-(n : ℝ)) 2 (smulLeftCLM ℂ g u) := by
     …

131. theorem OAI.ElasticityRegularity.exists_bounded_negative_multiplier line 1267
132. theorem OAI.ElasticityRegularity.exists_bounded_nat_multiplier line 1274
133. theorem OAI.ElasticityDualSolvability.perturbed_weak_solver line 1285

     Source documentation

     A bounded zeroth-order perturbation of an actual weak right inverse.

     theorem perturbed_weak_solver (D : Submodule ℂ H) (A : D →ₗ[ℂ] H)
         (T B Q : H →L[ℂ] H)
         (hT : ∀ f v, inner ℂ (T f) (A v)=inner ℂ f (v : H))
         (hQ : (1+B*T)*Q=1) (f : H) (v : D) :
         inner ℂ ((T*Q) f) (A v+B.adjoint (v : H))=inner ℂ f (v : H) := by
     …

134. theorem OAI.ElasticityDualSolvability.perturbed_weak_inverse line 1298

     Source documentation

     The perturbative solver exists without adding a range surjectivity assumption. The smallness condition is strictly local in parameter space.

     theorem perturbed_weak_inverse (D : Submodule ℂ H) (A : D →ₗ[ℂ] H)
         (T B : H →L[ℂ] H)
         (hT : ∀ f v, inner ℂ (T f) (A v)=inner ℂ f (v : H))
         (hBT : ‖B*T‖<1) :
         ∀ f v, inner ℂ ((T*Ring.inverse (1+B*T)) f) (A v+B.adjoint (v : H))=
           inner ℂ f (v : H) := by
     …

135. theorem OAI.ElasticityDualSolvability.smooth_local_weak_inverse line 1311

     Source documentation

     Smooth dependence of the local Neumann inverse, established with the stock Banach-algebra inversion theorem.

     theorem smooth_local_weak_inverse {P : Type*} [NormedAddCommGroup P] [NormedSpace ℝ P]
         (T : H →L[ℂ] H) (B : P → H →L[ℂ] H) {p : P}
         (hB : ContDiffAt ℝ (⊤ : ℕ∞) B p) (hBT : ‖B p*T‖<1) :
         ContDiffAt ℝ (⊤ : ℕ∞) (fun q => T*Ring.inverse (1+B q*T)) p := by
     …