OAI/MathematicalPhysics/Elasticity/Bessel.lean

GitHub source file

313 declarations, 0 contain sorry, 0 declared as axioms

Concrete Fourier Bessel potentials for the required negative-order supported Carleman estimate. All functions and operators are actual Schwartz maps; no Sobolev-shift estimate is being assumed.

  1. abbrev OAI.ElasticityBessel.X line 13
  2. abbrev OAI.ElasticityBessel.S line 14
  3. def OAI.ElasticityBessel.weight line 16
  4. lemma OAI.ElasticityBessel.weight_pos line 18
  5. lemma OAI.ElasticityBessel.temperate_weight line 21
  6. lemma OAI.ElasticityBessel.temperate_complex_weight line 25
  7. lemma OAI.ElasticityBessel.weight_add line 29
  8. lemma OAI.ElasticityBessel.weight_zero line 33
  9. lemma OAI.ElasticityBessel.weight_neg line 35
  10. def OAI.ElasticityBessel.M line 39
  11. lemma OAI.ElasticityBessel.M_apply line 42
  12. lemma OAI.ElasticityBessel.M_add line 46
  13. lemma OAI.ElasticityBessel.M_zero line 51
  14. def OAI.ElasticityBessel.J line 55
  15. lemma OAI.ElasticityBessel.fourier_J line 57
  16. lemma OAI.ElasticityBessel.J_add_order line 60
  17. lemma OAI.ElasticityBessel.J_zero line 63
  18. lemma OAI.ElasticityBessel.J_neg_inverse line 66
  19. lemma OAI.ElasticityBessel.J_add line 69
  20. lemma OAI.ElasticityBessel.J_smul line 72
  21. lemma OAI.ElasticityBessel.J_deriv line 75
  22. abbrev OAI.ElasticityBessel.L2 line 85
  23. def OAI.ElasticityBessel.norm2 line 87
  24. lemma OAI.ElasticityBessel.norm2_nonneg line 89
  25. lemma OAI.ElasticityBessel.norm2_eq_zero line 91
  26. lemma OAI.ElasticityBessel.norm2_add_le line 97
  27. lemma OAI.ElasticityBessel.norm2_const_smul line 100
  28. lemma OAI.ElasticityBessel.norm2_bound line 103
  29. lemma OAI.ElasticityBessel.norm2_fourier line 111
  30. lemma OAI.ElasticityBessel.norm2_fourierInv line 114
  31. lemma OAI.ElasticityBessel.norm2_J line 119
  32. lemma OAI.ElasticityBessel.real_weight_bound line 122
  33. lemma OAI.ElasticityBessel.fderiv_weight line 132
  34. lemma OAI.ElasticityBessel.fderiv_complex_weight line 152
  35. def OAI.ElasticityBessel.Q line 162
  36. lemma OAI.ElasticityBessel.Q_apply line 165
  37. lemma OAI.ElasticityBessel.Q_real line 171
  38. lemma OAI.ElasticityBessel.deriv_M line 175
  39. lemma OAI.ElasticityBessel.fourier_Q line 193
  40. lemma OAI.ElasticityBessel.Q_J line 201
  41. def OAI.ElasticityBessel.ip line 216
  42. lemma OAI.ElasticityBessel.ip_integral line 218
  43. lemma OAI.ElasticityBessel.norm2_sq line 222
  44. lemma OAI.ElasticityBessel.ip_fourier line 225
  45. lemma OAI.ElasticityBessel.ip_M line 228
  46. lemma OAI.ElasticityBessel.ip_J line 235
  47. lemma OAI.ElasticityBessel.norm2_J_sq line 239
  48. lemma OAI.ElasticityBessel.weight_two line 243
  49. lemma OAI.ElasticityBessel.weight_one_sq line 247
  50. lemma OAI.ElasticityBessel.norm_le_weight_one line 251
  51. lemma OAI.ElasticityBessel.weight_mono line 257
  52. lemma OAI.ElasticityBessel.norm2_J_mono line 262
  53. lemma OAI.ElasticityBessel.norm2_J_nonpos line 268
  54. lemma OAI.ElasticityBessel.norm_fourier_deriv line 272
  55. lemma OAI.ElasticityBessel.semiclassical_frequency_bound line 281
  56. lemma OAI.ElasticityBessel.norm2_J_semideriv line 296
  57. abbrev OAI.ElasticitySchwartzCarleman.X line 325
  58. abbrev OAI.ElasticitySchwartzCarleman.Test line 326
  59. lemma OAI.ElasticitySchwartzCarleman.smooth line 328
  60. def OAI.ElasticitySchwartzCarleman.d line 330
  61. lemma OAI.ElasticitySchwartzCarleman.d_apply line 332
  62. lemma OAI.ElasticitySchwartzCarleman.d_d line 335
  63. lemma OAI.ElasticitySchwartzCarleman.d_comm line 343
  64. lemma OAI.ElasticitySchwartzCarleman.deriv_conj line 350
  65. def OAI.ElasticitySchwartzCarleman.pair line 356
  66. lemma OAI.ElasticitySchwartzCarleman.integrable_pair line 358
  67. lemma OAI.ElasticitySchwartzCarleman.pair_add_right line 365
  68. lemma OAI.ElasticitySchwartzCarleman.pair_add_left line 369
  69. lemma OAI.ElasticitySchwartzCarleman.pair_sub_right line 373
  70. lemma OAI.ElasticitySchwartzCarleman.pair_sub_left line 377
  71. lemma OAI.ElasticitySchwartzCarleman.pair_smul_right line 381
  72. lemma OAI.ElasticitySchwartzCarleman.pair_smul_left line 386
  73. lemma OAI.ElasticitySchwartzCarleman.pair_real_smul_left line 391

    Source documentation

    Coordinate derivatives are skew adjoint on the actual test space.

    lemma pair_real_smul_left (f g : Test) (a : ℝ) :
    pair (a • f) g = (a : ℂ) * pair f g := by
…

    Mentions: OAI.ElasticitySchwartzCarleman.Test, OAI.ElasticitySchwartzCarleman.pair

  74. lemma OAI.ElasticitySchwartzCarleman.pair_d line 396
  75. def OAI.ElasticitySchwartzCarleman.mass line 406
  76. lemma OAI.ElasticitySchwartzCarleman.mass_integral line 408
  77. lemma OAI.ElasticitySchwartzCarleman.integrable_normSq line 413
  78. lemma OAI.ElasticitySchwartzCarleman.mass_nonneg line 418
  79. lemma OAI.ElasticitySchwartzCarleman.mass_eq_zero line 422
  80. def OAI.ElasticitySchwartzCarleman.e line 432
  81. def OAI.ElasticitySchwartzCarleman.qCLM line 434
  82. lemma OAI.ElasticitySchwartzCarleman.qCLM_apply line 436
  83. lemma OAI.ElasticitySchwartzCarleman.qCLM_e line 438
  84. def OAI.ElasticitySchwartzCarleman.Q line 441
  85. lemma OAI.ElasticitySchwartzCarleman.Q_apply line 443
  86. lemma OAI.ElasticitySchwartzCarleman.d_Q line 446
  87. lemma OAI.ElasticitySchwartzCarleman.pair_Q line 459
  88. def OAI.ElasticitySchwartzCarleman.G line 466

    Source documentation

    Affine normal derivative of the convexified linear weight.

    def G (a b : ℝ) : Test →ₗ[ℂ] Test := (a : ℂ) • LinearMap.id + (b : ℂ) • Q

    Mentions: OAI.ElasticitySchwartzCarleman.Test, OAI.ElasticitySchwartzCarleman.Q

  89. def OAI.ElasticitySchwartzCarleman.lap line 468
  90. lemma OAI.ElasticitySchwartzCarleman.lap_apply line 470
  91. def OAI.ElasticitySchwartzCarleman.A line 474
  92. def OAI.ElasticitySchwartzCarleman.B line 477
  93. def OAI.ElasticitySchwartzCarleman.P line 480
  94. lemma OAI.ElasticitySchwartzCarleman.G_apply line 482
  95. lemma OAI.ElasticitySchwartzCarleman.d_G line 488
  96. lemma OAI.ElasticitySchwartzCarleman.pair_G line 494
  97. lemma OAI.ElasticitySchwartzCarleman.lap_comm line 499
  98. lemma OAI.ElasticitySchwartzCarleman.lap_G line 505
  99. lemma OAI.ElasticitySchwartzCarleman.pair_dd line 511
  100. lemma OAI.ElasticitySchwartzCarleman.pair_lap line 515
  101. lemma OAI.ElasticitySchwartzCarleman.pair_A line 518
  102. lemma OAI.ElasticitySchwartzCarleman.pair_B line 524
  103. lemma OAI.ElasticitySchwartzCarleman.commutator line 534

    Source documentation

    The commutator producing the convexification gain.

    lemma commutator (h a b : ℝ) (f : Test) :
    A h a b (B h a b f) - B h a b (A h a b f) =
      (-4 * (h : ℂ)^3 * b) • d (e 0) (d (e 0) f) +
      (4 * (h : ℂ) * b) • G a b (G a b f) := by
…

    Mentions: OAI.ElasticitySchwartzCarleman.Test, OAI.ElasticitySchwartzCarleman.A, OAI.ElasticitySchwartzCarleman.B, OAI.ElasticitySchwartzCarleman.d, OAI.ElasticitySchwartzCarleman.e, OAI.ElasticitySchwartzCarleman.G

  104. lemma OAI.ElasticitySchwartzCarleman.energy_identity line 544
  105. lemma OAI.ElasticitySchwartzCarleman.mass_A_le line 568
  106. lemma OAI.ElasticitySchwartzCarleman.mass_G_le line 577
  107. lemma OAI.ElasticitySchwartzCarleman.normSq_G line 584
  108. lemma OAI.ElasticitySchwartzCarleman.lower_mass_G line 591
  109. lemma OAI.ElasticitySchwartzCarleman.upper_mass_G line 604
  110. lemma OAI.ElasticitySchwartzCarleman.mass_coercivity line 616
  111. lemma OAI.ElasticitySchwartzCarleman.pair_symm line 623
  112. lemma OAI.ElasticitySchwartzCarleman.pair_re_bound line 631
  113. def OAI.ElasticitySchwartzCarleman.gradientMass line 640
  114. lemma OAI.ElasticitySchwartzCarleman.gradientMass_nonneg line 642
  115. lemma OAI.ElasticitySchwartzCarleman.lap_energy line 645
  116. lemma OAI.ElasticitySchwartzCarleman.kinetic_identity line 650
  117. lemma OAI.ElasticitySchwartzCarleman.scalar_H1_coercivity line 663

    Source documentation

    A concrete positive-order supported Carleman estimate. This is not yet the negative-order estimate needed for the augmented system.

    lemma scalar_H1_coercivity (h a b : ℝ) (hh : 0 ≤ h) (hb : 0 ≤ b)
    (hsmall : h*b ≤ 1) (f : Test)
    (hlo : ∀ x : X, f x ≠ 0 → (1/4:ℝ) ≤ (a+b*x 0)^2)
    (hhi : ∀ x : X, f x ≠ 0 → (a+b*x 0)^2 ≤ (9/4:ℝ)) :
    h*b*(mass f + h^2*gradientMass f) ≤ (17/4:ℝ)*mass (P h a b f) := by
…

    Mentions: OAI.ElasticitySchwartzCarleman.Test, OAI.ElasticitySchwartzCarleman.X, OAI.ElasticitySchwartzCarleman.mass, OAI.ElasticitySchwartzCarleman.gradientMass, OAI.ElasticitySchwartzCarleman.P

  118. lemma OAI.ElasticitySchwartzCarleman.mass_add_bound line 679
  119. lemma OAI.ElasticitySchwartzCarleman.mass_ofReal_smul line 687
  120. lemma OAI.ElasticitySchwartzCarleman.lap_mass_bound line 693
  121. lemma OAI.ElasticitySchwartzCarleman.scalar_H2_coercivity line 714

    Source documentation

    The two-derivative, L²-forcing estimate in concrete derivative norms. The unproved Sobolev shift to H⁻¹ forcing is a separate required step.

    lemma scalar_H2_coercivity (h a b : ℝ) (hh : 0 ≤ h) (hb : 0 ≤ b)
    (hsmall : h*b ≤ 1) (f : Test)
    (hlo : ∀ x : X, f x ≠ 0 → (1/4:ℝ) ≤ (a+b*x 0)^2)
    (hhi : ∀ x : X, f x ≠ 0 → (a+b*x 0)^2 ≤ (9/4:ℝ)) :
    h*b*(mass f + 2*h^2*gradientMass f + h^4*mass (lap f)) ≤
      (21:ℝ)*mass (P h a b f) := by
…

    Mentions: OAI.ElasticitySchwartzCarleman.Test, OAI.ElasticitySchwartzCarleman.X, OAI.ElasticitySchwartzCarleman.mass, OAI.ElasticitySchwartzCarleman.gradientMass, OAI.ElasticitySchwartzCarleman.lap, OAI.ElasticitySchwartzCarleman.P

  122. lemma OAI.ElasticitySchwartzCarleman.linear_weight_bounds line 728
  123. lemma OAI.ElasticitySchwartzCarleman.mass_neg line 736
  124. lemma OAI.ElasticitySchwartzCarleman.affine_mass_bounds line 740
  125. lemma OAI.ElasticitySchwartzCarleman.affine_square_mass_bound line 760
  126. lemma OAI.ElasticitySchwartzCarleman.scalar_H2_moment_bound line 775

    Source documentation

    Schwartz Carleman algebra with controlled moments, without a false compact-support claim for Bessel potentials.

    lemma scalar_H2_moment_bound (h b : ℝ) (hh : 0 ≤ h) (hb : 0 ≤ b)
    (hsmall : h*b ≤ 1) (f : Test) :
    h*b*(mass f+2*h^2*gradientMass f+h^4*mass (lap f)) ≤
      10*mass (P h (-1) b f) +
        h*b*(64*b^2*mass (Q f)+8*b^4*mass (Q (Q f))) := by
…

    Mentions: OAI.ElasticitySchwartzCarleman.Test, OAI.ElasticitySchwartzCarleman.mass, OAI.ElasticitySchwartzCarleman.gradientMass, OAI.ElasticitySchwartzCarleman.lap, OAI.ElasticitySchwartzCarleman.P, OAI.ElasticitySchwartzCarleman.Q

  127. abbrev OAI.ElasticityNegativeOrder.X line 813
  128. lemma OAI.ElasticityNegativeOrder.norm2_sq_mass line 815
  129. lemma OAI.ElasticityNegativeOrder.Q_bridge line 819
  130. lemma OAI.ElasticityNegativeOrder.fourier_d line 824
  131. lemma OAI.ElasticityNegativeOrder.J_two line 834
  132. lemma OAI.ElasticityNegativeOrder.mass_sub line 848
  133. lemma OAI.ElasticityNegativeOrder.H2_energy line 854
  134. lemma OAI.ElasticityNegativeOrder.d_eq line 863
  135. lemma OAI.ElasticityNegativeOrder.semideriv_bound line 867
  136. lemma OAI.ElasticityNegativeOrder.second_deriv_bound line 874
  137. lemma OAI.ElasticityNegativeOrder.Q_J line 882
  138. lemma OAI.ElasticityNegativeOrder.QQ_J line 889
  139. lemma OAI.ElasticityNegativeOrder.norm2_real_smul line 908
  140. lemma OAI.ElasticityNegativeOrder.norm2_sub_le line 912
  141. lemma OAI.ElasticityNegativeOrder.norm2_Q_supported line 915
  142. lemma OAI.ElasticityNegativeOrder.norm2_QQ_supported line 925
  143. lemma OAI.ElasticityNegativeOrder.semideriv_nonpos line 939
  144. lemma OAI.ElasticityNegativeOrder.second_deriv_nonpos line 944
  145. lemma OAI.ElasticityNegativeOrder.first_moment line 949
  146. lemma OAI.ElasticityNegativeOrder.norm2_four_terms line 968
  147. lemma OAI.ElasticityNegativeOrder.second_moment line 975
  148. lemma OAI.ElasticityNegativeOrder.J_sub line 1009
  149. lemma OAI.ElasticityNegativeOrder.d_J line 1013
  150. lemma OAI.ElasticityNegativeOrder.lap_J line 1016
  151. lemma OAI.ElasticityNegativeOrder.P_expanded line 1019
  152. lemma OAI.ElasticityNegativeOrder.P_shift line 1029
  153. lemma OAI.ElasticityNegativeOrder.norm2_six_terms line 1042
  154. lemma OAI.ElasticityNegativeOrder.norm2_P_shift line 1051
  155. lemma OAI.ElasticityNegativeOrder.moment_coefficient_small line 1086
  156. lemma OAI.ElasticityNegativeOrder.norm2_J_one_ge line 1093
  157. lemma OAI.ElasticityNegativeOrder.shifted_energy line 1097
  158. lemma OAI.ElasticityNegativeOrder.scalar_supported_shift line 1112

    Source documentation

    The missing scalar negative-order shift, obtained using actual nonlocal Bessel potentials and Schwartz moments, not a false preservation of support.

    lemma scalar_supported_shift (h b R : ℝ) (hh : 0 ≤ h) (hh1 : h ≤ 1)
    (hb : 0 ≤ b) (hR : 1 ≤ R) (hbR : b*R ≤ 1/100) (hhb : h*b ≤ 1/8000)
    (f : S) (hf : ∀ x : X, f x ≠ 0 → |x 0| ≤ R) :
    h*b*norm2 (J h 1 f)^2 ≤ 40*norm2 (J h (-1) (P h (-1) b f))^2 := by
…

    Mentions: OAI.ElasticityNegativeOrder.X

  159. lemma OAI.ElasticityNegativeOrder.convexified_supported line 1142
  160. lemma OAI.ElasticityNegativeOrder.H1_energy line 1164
  161. def OAI.ElasticityNegativeOrder.mult line 1177
  162. lemma OAI.ElasticityNegativeOrder.mult_apply line 1179
  163. lemma OAI.ElasticityNegativeOrder.d_mult_apply line 1183
  164. lemma OAI.ElasticityNegativeOrder.mass_bound_two line 1195
  165. lemma OAI.ElasticityNegativeOrder.mult_mass line 1206
  166. lemma OAI.ElasticityNegativeOrder.mult_deriv_mass line 1215
  167. lemma OAI.ElasticityNegativeOrder.mult_H1 line 1238
  168. lemma OAI.ElasticityNegativeOrder.temperate_conj line 1263
  169. lemma OAI.ElasticityNegativeOrder.fderiv_conj line 1267
  170. lemma OAI.ElasticityNegativeOrder.ip_mult line 1273
  171. lemma OAI.ElasticityNegativeOrder.ip_shift line 1282
  172. lemma OAI.ElasticityNegativeOrder.ip_re_shift_bound line 1287
  173. lemma OAI.ElasticityNegativeOrder.mult_Hneg1 line 1292
  174. lemma OAI.ElasticityNegativeOrder.norm2_sum_le line 1326
  175. lemma OAI.ElasticityNegativeOrder.norm2_mult line 1330
  176. lemma OAI.ElasticityNegativeOrder.norm2_G_supported line 1337
  177. def OAI.ElasticityNegativeOrder.conjugatedDeriv line 1352
  178. lemma OAI.ElasticityNegativeOrder.norm2_conjugatedDeriv line 1355
  179. def OAI.ElasticityNegativeOrder.lowerOrder line 1374
  180. lemma OAI.ElasticityNegativeOrder.norm2_lowerOrder line 1377
  181. lemma OAI.ElasticityNegativeOrder.scalar_perturbed line 1405
  182. def OAI.ElasticityNegativeOrder.sumNorm line 1440

    Source documentation

    Componentwise ℓ¹ auxiliary norm; the actual Hermitian Sobolev norm is sobNorm below, and is compared explicitly, not substituted in the statement.

    def sumNorm {n : ℕ} (h s : ℝ) (U : Fin n → S) : ℝ :=
…
  183. def OAI.ElasticityNegativeOrder.sobNorm line 1443
  184. lemma OAI.ElasticityNegativeOrder.sumNorm_nonneg line 1446
  185. lemma OAI.ElasticityNegativeOrder.sobNorm_le_sumNorm line 1449
  186. lemma OAI.ElasticityNegativeOrder.sumNorm_four_le line 1460
  187. def OAI.ElasticityNegativeOrder.lowerSystem line 1470
  188. lemma OAI.ElasticityNegativeOrder.lowerSystem_bound line 1474
  189. lemma OAI.ElasticityNegativeOrder.system_perturbed_l1 line 1498
  190. lemma OAI.ElasticityNegativeOrder.system_four_perturbed line 1542
  191. def OAI.ElasticityNegativeOrder.BallSupported line 1571

    Source documentation

    Support in a fixed closed Euclidean ball.

    def BallSupported (R : ℝ) (f : S) : Prop :=
…
  192. lemma OAI.ElasticityNegativeOrder.BallSupported.add line 1574
  193. lemma OAI.ElasticityNegativeOrder.BallSupported.smul line 1582
  194. lemma OAI.ElasticityNegativeOrder.BallSupported.d line 1587
  195. lemma OAI.ElasticityNegativeOrder.BallSupported.Q line 1594
  196. lemma OAI.ElasticityNegativeOrder.BallSupported.mult line 1599
  197. lemma OAI.ElasticityNegativeOrder.BallSupported.coordinate line 1604
  198. def OAI.ElasticityNegativeOrder.cutoff line 1611
  199. def OAI.ElasticityNegativeOrder.expQuad line 1617
  200. lemma OAI.ElasticityNegativeOrder.smooth_expQuad line 1619
  201. lemma OAI.ElasticityNegativeOrder.fderiv_expQuad line 1622
  202. def OAI.ElasticityNegativeOrder.weightCut line 1634
  203. lemma OAI.ElasticityNegativeOrder.compact_weightCut line 1637
  204. lemma OAI.ElasticityNegativeOrder.smooth_weightCut line 1642
  205. lemma OAI.ElasticityNegativeOrder.temperate_weightCut line 1646
  206. def OAI.ElasticityNegativeOrder.W line 1650
  207. lemma OAI.ElasticityNegativeOrder.W_apply line 1652
  208. lemma OAI.ElasticityNegativeOrder.BallSupported.W line 1663
  209. lemma OAI.ElasticityNegativeOrder.d_W line 1666
  210. lemma OAI.ElasticityNegativeOrder.lap_W line 1679
  211. lemma OAI.ElasticityNegativeOrder.W_inverse line 1692
  212. lemma OAI.ElasticityNegativeOrder.Q_W line 1700
  213. lemma OAI.ElasticityNegativeOrder.mult_W line 1707
  214. lemma OAI.ElasticityNegativeOrder.P_W line 1714
  215. lemma OAI.ElasticityNegativeOrder.conjugatedDeriv_W line 1721
  216. lemma OAI.ElasticityNegativeOrder.lowerOrder_W line 1730
  217. lemma OAI.ElasticityNegativeOrder.compact_mult_bounds line 1737
  218. lemma OAI.ElasticityNegativeOrder.sobNorm_map_bound line 1763
  219. lemma OAI.ElasticityNegativeOrder.lowerSystem_W line 1778
  220. lemma OAI.ElasticityNegativeOrder.system_four_real_fixed line 1789

    Source documentation

    Removal of the fixed quadratic convexification by actual smooth Schwartz multipliers; the constant is independent of the small parameter h.

    lemma system_four_real_fixed (ε R : ℝ) (hε : 0 < ε) (hR : 1 ≤ R)
    (a : Fin 3 → Fin 4 → Fin 4 → X → ℂ) (v : Fin 4 → Fin 4 → X → ℂ)
    (ha : ∀ k i j, (a k i j).HasTemperateGrowth)
    (hv : ∀ i j, (v i j).HasTemperateGrowth)
    (A V : ℝ) (hA : 0 ≤ A) (hV : 0 ≤ V)
    (haA : ∀ k i j x, ‖a k i j x‖ ≤ A) (hvV : ∀ i j x, ‖v i j x‖ ≤ V)
    (habsorb : 56*(9*A+V)*Real.sqrt ε ≤ 1) :
    ∃ C : ℝ, 0 < C ∧ ∀ h : ℝ, 0 < h → h ≤ 1 → (h/ε)*R ≤ 1/8000 →
    ∀ U : Fin 4 → S, (∀ i, BallSupported R (U i)) →
    sobNorm h 1 U ≤ (C/h)*sobNorm h (-1)
      (fun i => P h (-1) 0 (U i)+lowerSystem h 0 a v U i) := by
…

    Mentions: OAI.ElasticityNegativeOrder.X, OAI.ElasticityNegativeOrder.BallSupported, OAI.ElasticityNegativeOrder.sobNorm, OAI.ElasticityNegativeOrder.lowerSystem

  221. lemma OAI.ElasticityNegativeOrder.system_four_real line 1832
  222. def OAI.ElasticityNegativeOrder.osc line 1865
  223. lemma OAI.ElasticityNegativeOrder.norm_osc line 1867
  224. lemma OAI.ElasticityNegativeOrder.smooth_osc line 1870
  225. lemma OAI.ElasticityNegativeOrder.fderiv_osc line 1874
  226. lemma OAI.ElasticityNegativeOrder.semideriv_osc line 1891
  227. def OAI.ElasticityNegativeOrder.oscCut line 1898
  228. lemma OAI.ElasticityNegativeOrder.compact_oscCut line 1901
  229. lemma OAI.ElasticityNegativeOrder.smooth_oscCut line 1905
  230. lemma OAI.ElasticityNegativeOrder.temperate_oscCut line 1909
  231. def OAI.ElasticityNegativeOrder.O line 1913
  232. lemma OAI.ElasticityNegativeOrder.O_apply line 1915
  233. lemma OAI.ElasticityNegativeOrder.BallSupported.O line 1926
  234. lemma OAI.ElasticityNegativeOrder.O_inverse line 1929
  235. lemma OAI.ElasticityNegativeOrder.osc_multiplier_bounds line 1936
  236. lemma OAI.ElasticityNegativeOrder.BallSupported.sub line 1983
  237. lemma OAI.ElasticityNegativeOrder.BallSupported.zero line 1987
  238. lemma OAI.ElasticityNegativeOrder.BallSupported.sum line 1990
  239. lemma OAI.ElasticityNegativeOrder.BallSupported.lap line 2000
  240. lemma OAI.ElasticityNegativeOrder.BallSupported.P_zero line 2005
  241. lemma OAI.ElasticityNegativeOrder.BallSupported.conjugatedDeriv_zero line 2012
  242. lemma OAI.ElasticityNegativeOrder.BallSupported.lowerOrder_zero line 2021
  243. lemma OAI.ElasticityNegativeOrder.BallSupported.lowerSystem_zero line 2028
  244. def OAI.ElasticityNegativeOrder.phaseSystem line 2039

    Source documentation

    The actual conjugated differential operator, with a local cutoff that is identically one on the support, not an abstract operator hypothesis.

    def phaseSystem (R : ℝ) (hR : 1 ≤ R) (β : X) (h : ℝ)
    (a : Fin 3 → Fin 4 → Fin 4 → X → ℂ) (v : Fin 4 → Fin 4 → X → ℂ)
    (U : Fin 4 → S) (i : Fin 4) : S :=
…

    Mentions: OAI.ElasticityNegativeOrder.X

  245. lemma OAI.ElasticityNegativeOrder.system_four_phase line 2045
  246. def OAI.ElasticityNegativeOrder.oscRate line 2085
  247. lemma OAI.ElasticityNegativeOrder.d_O line 2087
  248. lemma OAI.ElasticityNegativeOrder.lap_O line 2100
  249. def OAI.ElasticityNegativeOrder.Pbeta line 2113
  250. lemma OAI.ElasticityNegativeOrder.P_O line 2118
  251. def OAI.ElasticityNegativeOrder.betaDeriv line 2125
  252. lemma OAI.ElasticityNegativeOrder.conjugatedDeriv_O line 2129
  253. lemma OAI.ElasticityNegativeOrder.mult_O line 2136
  254. def OAI.ElasticityNegativeOrder.lowerBeta line 2143
  255. lemma OAI.ElasticityNegativeOrder.lowerOrder_O line 2146
  256. lemma OAI.ElasticityNegativeOrder.BallSupported.Pbeta line 2153
  257. lemma OAI.ElasticityNegativeOrder.BallSupported.betaDeriv line 2165
  258. lemma OAI.ElasticityNegativeOrder.BallSupported.lowerBeta line 2172
  259. def OAI.ElasticityNegativeOrder.betaSystem line 2179
  260. lemma OAI.ElasticityNegativeOrder.phaseSystem_eq_betaSystem line 2184
  261. def OAI.ElasticityNegativeOrder.rot line 2196
  262. lemma OAI.ElasticityNegativeOrder.rot_apply line 2199
  263. lemma OAI.ElasticityNegativeOrder.rot_inverse line 2201
  264. lemma OAI.ElasticityNegativeOrder.fourier_rot line 2205
  265. lemma OAI.ElasticityNegativeOrder.fourierInv_rot line 2209
  266. lemma OAI.ElasticityNegativeOrder.M_rot line 2215
  267. lemma OAI.ElasticityNegativeOrder.J_rot line 2220
  268. lemma OAI.ElasticityNegativeOrder.mass_rot line 2224
  269. lemma OAI.ElasticityNegativeOrder.norm2_rot line 2229
  270. lemma OAI.ElasticityNegativeOrder.sobNorm_rot line 2233
  271. lemma OAI.ElasticityNegativeOrder.BallSupported.rot line 2237
  272. lemma OAI.ElasticityNegativeOrder.d_rot line 2243
  273. lemma OAI.ElasticityNegativeOrder.lap_rot line 2247
  274. lemma OAI.ElasticityNegativeOrder.d_sum_basis line 2252
  275. lemma OAI.ElasticityNegativeOrder.exists_rotation line 2263
  276. def OAI.ElasticityNegativeOrder.Pdir line 2269

    Source documentation

    Minus the semiclassical conjugated Laplacian for the real/imaginary parts α,β of the phase. The last term vanishes exactly for null phases.

    def Pdir (h : ℝ) (α β : X) (f : S) : S :=
…

    Mentions: OAI.ElasticityNegativeOrder.X

  277. lemma OAI.ElasticityNegativeOrder.Pbeta_eq_Pdir line 2274
  278. def OAI.ElasticityNegativeOrder.dirDeriv line 2288
  279. lemma OAI.ElasticityNegativeOrder.betaDeriv_eq_dirDeriv line 2291
  280. lemma OAI.ElasticityNegativeOrder.Pdir_rot line 2300
  281. lemma OAI.ElasticityNegativeOrder.d_basis_rot line 2304
  282. lemma OAI.ElasticityNegativeOrder.basis_expansion line 2316
  283. lemma OAI.ElasticityNegativeOrder.map_coord line 2322
  284. lemma OAI.ElasticityNegativeOrder.dirDeriv_basis_rot line 2329
  285. lemma OAI.ElasticityNegativeOrder.temperate_comp_rot line 2337
  286. lemma OAI.ElasticityNegativeOrder.mult_rot line 2341
  287. def OAI.ElasticityNegativeOrder.lowerDir line 2346
  288. def OAI.ElasticityNegativeOrder.dirSystem line 2349
  289. lemma OAI.ElasticityNegativeOrder.betaSystem_eq_dirSystem line 2354
  290. def OAI.ElasticityNegativeOrder.rotCoeff line 2361
  291. lemma OAI.ElasticityNegativeOrder.temperate_rotCoeff line 2364
  292. lemma OAI.ElasticityNegativeOrder.norm_rotCoord_le line 2371
  293. lemma OAI.ElasticityNegativeOrder.norm_rotCoeff_le line 2377
  294. lemma OAI.ElasticityNegativeOrder.lowerDir_rot line 2389
  295. lemma OAI.ElasticityNegativeOrder.dirSystem_rot line 2403
  296. lemma OAI.ElasticityNegativeOrder.system_four_unit_direction line 2414
  297. lemma OAI.ElasticityNegativeOrder.Pdir_null line 2446
  298. lemma OAI.ElasticityNegativeOrder.weight_one_sq line 2452
  299. lemma OAI.ElasticityNegativeOrder.weight_hscale_one line 2456
  300. lemma OAI.ElasticityNegativeOrder.weight_hscale_neg_one line 2470
  301. lemma OAI.ElasticityNegativeOrder.norm2_J_of_weight_bound line 2478
  302. lemma OAI.ElasticityNegativeOrder.norm2_J_hscale_one line 2490
  303. lemma OAI.ElasticityNegativeOrder.norm2_J_hscale_neg_one line 2494
  304. lemma OAI.ElasticityNegativeOrder.sobNorm_component_bound line 2498
  305. lemma OAI.ElasticityNegativeOrder.sobNorm_hscale_one line 2513
  306. lemma OAI.ElasticityNegativeOrder.sobNorm_hscale_neg_one line 2517
  307. lemma OAI.ElasticityNegativeOrder.d_real_smul line 2521
  308. lemma OAI.ElasticityNegativeOrder.Pdir_scale line 2525
  309. lemma OAI.ElasticityNegativeOrder.dirDeriv_scale line 2532
  310. lemma OAI.ElasticityNegativeOrder.lowerDir_scale line 2538
  311. lemma OAI.ElasticityNegativeOrder.dirSystem_scale line 2544
  312. lemma OAI.ElasticityNegativeOrder.sobNorm_smul line 2552
  313. lemma OAI.ElasticityNegativeOrder.system_four_direction line 2557