OAI/Geometry/SmoothYau/Smoothness/ChartDerivativeNeZeroTransfer.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.YauCounterexamples.manifoldSobolevRepresentative_localize line 36
  2. theorem OAI.YauCounterexamples.manifoldSobolevRepresentative_injective line 56
  3. def OAI.YauCounterexamples.chartLiftSmoothLinear line 96
  4. def OAI.YauCounterexamples.chartLiftToManifoldSobolev line 108
  5. lemma OAI.YauCounterexamples.chartLiftToManifoldSobolev_bound line 113
  6. def OAI.YauCounterexamples.sobolevChartLift line 127
  7. lemma OAI.YauCounterexamples.sobolevChartLift_schwartz line 133
  8. lemma OAI.YauCounterexamples.sobolevChartLift_representative line 143
  9. def OAI.YauCounterexamples.atlasSobolevGluing line 189
  10. lemma OAI.YauCounterexamples.chartLift_chartLocalize_buffer line 197
  11. lemma OAI.YauCounterexamples.atlasGluing_partition_identity line 214
  12. theorem OAI.YauCounterexamples.atlasSobolevGluing_leftInverse line 220
  13. lemma OAI.YauCounterexamples.contMDiff_chartLift_finite line 272
  14. lemma OAI.YauCounterexamples.manifoldSobolevRepresentative_eq_sum line 287
  15. theorem OAI.YauCounterexamples.contMDiff_manifoldSobolevRepresentative line 303
  16. structure OAI.YauCounterexamples.CompactMetricAtlas line 335
  17. theorem OAI.YauCounterexamples.nonempty_compactMetricAtlas line 352
  18. abbrev OAI.YauCounterexamples.CompactMetricAtlas.p line 363
  19. lemma OAI.YauCounterexamples.CompactMetricAtlas.chart_η line 365
  20. lemma OAI.YauCounterexamples.CompactMetricAtlas.chart_χ line 368
  21. lemma OAI.YauCounterexamples.CompactMetricAtlas.chart_ψ line 371
  22. abbrev OAI.YauCounterexamples.CompactMetricAtlas.H line 374
  23. def OAI.YauCounterexamples.CompactMetricAtlas.representative line 377
  24. def OAI.YauCounterexamples.CompactMetricAtlas.lift line 381
  25. lemma OAI.YauCounterexamples.CompactMetricAtlas.lift_representative line 388
  26. def OAI.YauCounterexamples.CompactMetricAtlas.χcoord line 398
  27. lemma OAI.YauCounterexamples.CompactMetricAtlas.compact_χcoord line 400
  28. lemma OAI.YauCounterexamples.CompactMetricAtlas.smooth_χcoord line 404
  29. lemma OAI.YauCounterexamples.CompactMetricAtlas.ψ_mul_χ line 409
  30. def OAI.YauCounterexamples.CompactMetricAtlas.localize line 414
  31. def OAI.YauCounterexamples.CompactMetricAtlas.patchParametrix line 419
  32. lemma OAI.YauCounterexamples.CompactMetricAtlas.patchParametrix_representative line 429
  33. def OAI.YauCounterexamples.CompactMetricAtlas.ψcoord line 476
  34. lemma OAI.YauCounterexamples.CompactMetricAtlas.compact_ψcoord line 478
  35. lemma OAI.YauCounterexamples.CompactMetricAtlas.smooth_ψcoord line 482
  36. lemma OAI.YauCounterexamples.CompactMetricAtlas.χcoord_support line 487
  37. lemma OAI.YauCounterexamples.CompactMetricAtlas.χcoord_unit_support line 496
  38. lemma OAI.YauCounterexamples.CompactMetricAtlas.χcoord_target line 505
  39. structure OAI.YauCounterexamples.CompactMetricAtlas.PatchCoefficients line 508
  40. lemma OAI.YauCounterexamples.CompactMetricAtlas.nonempty_patchCoefficients line 517
  41. def OAI.YauCounterexamples.CompactMetricAtlas.patchErrorTail line 524
  42. def OAI.YauCounterexamples.CompactMetricAtlas.patchError line 535
  43. lemma OAI.YauCounterexamples.CompactMetricAtlas.patchError_bound line 544
  44. lemma OAI.YauCounterexamples.CompactMetricAtlas.localize_representative line 581
  45. lemma OAI.YauCounterexamples.CompactMetricAtlas.χ_mul_η line 588
  46. lemma OAI.YauCounterexamples.CompactMetricAtlas.ψ_one_on_χcoord line 594
  47. lemma OAI.YauCounterexamples.CompactMetricAtlas.patchErrorTail_representative line 603
  48. lemma OAI.YauCounterexamples.CompactMetricAtlas.patchErrorTail_representative_inChart line 631
  49. lemma OAI.YauCounterexamples.CompactMetricAtlas.patchError_representative_inChart line 656
  50. lemma OAI.YauCounterexamples.CompactMetricAtlas.patchParametrix_equation line 676
  51. def OAI.YauCounterexamples.CompactMetricAtlas.parametrix line 751
  52. def OAI.YauCounterexamples.CompactMetricAtlas.error line 755
  53. def OAI.YauCounterexamples.CompactMetricAtlas.errorBound line 760
  54. lemma OAI.YauCounterexamples.CompactMetricAtlas.errorBound_nonneg line 766
  55. lemma OAI.YauCounterexamples.CompactMetricAtlas.error_norm_bound line 773
  56. lemma OAI.YauCounterexamples.CompactMetricAtlas.errorBound_tendsto line 788
  57. lemma OAI.YauCounterexamples.CompactMetricAtlas.eventually_admissible line 801
  58. lemma OAI.YauCounterexamples.CompactMetricAtlas.exists_parametrix_threshold line 808
  59. lemma OAI.YauCounterexamples.CompactMetricAtlas.representative_C2 line 821
  60. lemma OAI.YauCounterexamples.CompactMetricAtlas.parametrix_equation line 831
  61. def OAI.YauCounterexamples.CompactMetricAtlas.patchOutput line 867
  62. def OAI.YauCounterexamples.CompactMetricAtlas.parametrixBound line 874
  63. lemma OAI.YauCounterexamples.CompactMetricAtlas.parametrixBound_nonneg line 879
  64. lemma OAI.YauCounterexamples.CompactMetricAtlas.patchParametrix_bound line 886
  65. lemma OAI.YauCounterexamples.CompactMetricAtlas.parametrix_bound line 908
  66. lemma OAI.YauCounterexamples.CompactMetricAtlas.error_lt_one line 919
  67. def OAI.YauCounterexamples.CompactMetricAtlas.resolvent line 926
  68. lemma OAI.YauCounterexamples.CompactMetricAtlas.resolvent_bound line 934
  69. lemma OAI.YauCounterexamples.CompactMetricAtlas.resolvent_equation line 947
  70. lemma OAI.YauCounterexamples.complexLaplaceBeltrami_sub line 977
  71. lemma OAI.YauCounterexamples.complex_positive_shift_solution_unique line 988
  72. def OAI.YauCounterexamples.CompactMetricAtlas.transfer line 1006
  73. lemma OAI.YauCounterexamples.CompactMetricAtlas.transfer_representative line 1013
  74. def OAI.YauCounterexamples.CompactMetricAtlas.ofSmooth line 1025
  75. lemma OAI.YauCounterexamples.CompactMetricAtlas.ofSmooth_representative line 1030
  76. theorem OAI.YauCounterexamples.CompactMetricAtlas.regularity_step line 1037
  77. theorem OAI.YauCounterexamples.CompactMetricAtlas.represented_solution_smooth line 1065
  78. theorem OAI.YauCounterexamples.CompactMetricAtlas.exists_smooth_resolvent_threshold line 1099
  79. def OAI.YauCounterexamples.smoothMul line 1132
  80. def OAI.YauCounterexamples.smoothMulLinear line 1135
  81. lemma OAI.YauCounterexamples.CompactMetricAtlas.smooth_partition line 1149
  82. def OAI.YauCounterexamples.CompactMetricAtlas.smoothCutoffLocalization line 1158
  83. lemma OAI.YauCounterexamples.CompactMetricAtlas.smoothCutoffLocalization_bound line 1166
  84. def OAI.YauCounterexamples.CompactMetricAtlas.cutoffLocalization line 1189
  85. lemma OAI.YauCounterexamples.CompactMetricAtlas.cutoffLocalization_smooth line 1198
  86. lemma OAI.YauCounterexamples.CompactMetricAtlas.cutoffLocalization_representative line 1209
  87. lemma OAI.YauCounterexamples.CompactMetricAtlas.smooth_product_bound line 1234
  88. def OAI.YauCounterexamples.CompactMetricAtlas.smoothProduct line 1290
  89. def OAI.YauCounterexamples.CompactMetricAtlas.productConstant line 1296
  90. lemma OAI.YauCounterexamples.CompactMetricAtlas.productConstant_nonneg line 1300
  91. lemma OAI.YauCounterexamples.CompactMetricAtlas.smoothProduct_bound line 1304
  92. def OAI.YauCounterexamples.CompactMetricAtlas.product line 1310
  93. lemma OAI.YauCounterexamples.CompactMetricAtlas.product_smooth line 1320
  94. lemma OAI.YauCounterexamples.CompactMetricAtlas.product_bound line 1327
  95. lemma OAI.YauCounterexamples.CompactMetricAtlas.product_representative line 1333
  96. lemma OAI.YauCounterexamples.chartLocalize_eventually_eq line 1370
  97. def OAI.YauCounterexamples.CompactMetricAtlas.metricCoefficientSchwartz line 1386
  98. def OAI.YauCounterexamples.CompactMetricAtlas.laplacianPatch line 1391
  99. def OAI.YauCounterexamples.CompactMetricAtlas.laplacianCLM line 1400
  100. lemma OAI.YauCounterexamples.CompactMetricAtlas.laplacianPatch_representative line 1406
  101. lemma OAI.YauCounterexamples.CompactMetricAtlas.laplacianCLM_representative line 1450
  102. def OAI.YauCounterexamples.restrictBilinear line 1475
  103. lemma OAI.YauCounterexamples.norm_restrict_of_bound line 1483
  104. lemma OAI.YauCounterexamples.laplaceBeltrami_zero line 1498
  105. lemma OAI.YauCounterexamples.complexLaplaceBeltrami_ofReal line 1503
  106. abbrev OAI.YauCounterexamples.CompactMetricAtlas.realH line 1513
  107. instance OAI.YauCounterexamples.CompactMetricAtlas.realH_nacg line 1519
  108. instance OAI.YauCounterexamples.CompactMetricAtlas.realH_snacg line 1520
  109. instance OAI.YauCounterexamples.CompactMetricAtlas.realH_acg line 1521
  110. instance OAI.YauCounterexamples.CompactMetricAtlas.realH_ns line 1522
  111. instance OAI.YauCounterexamples.CompactMetricAtlas.realH_mod line 1523
  112. lemma OAI.YauCounterexamples.CompactMetricAtlas.realH_closed line 1526
  113. instance OAI.YauCounterexamples.CompactMetricAtlas.realH_completeSpace line 1535
  114. lemma OAI.YauCounterexamples.CompactMetricAtlas.realH_coe_representative line 1544
  115. def OAI.YauCounterexamples.CompactMetricAtlas.inclusion line 1550
  116. lemma OAI.YauCounterexamples.CompactMetricAtlas.inclusion_representative line 1555
  117. lemma OAI.YauCounterexamples.CompactMetricAtlas.norm_inclusion_le line 1563
  118. def OAI.YauCounterexamples.CompactMetricAtlas.realInclusion line 1567
  119. lemma OAI.YauCounterexamples.CompactMetricAtlas.product_mem_realH line 1571
  120. def OAI.YauCounterexamples.CompactMetricAtlas.realProduct line 1582
  121. lemma OAI.YauCounterexamples.CompactMetricAtlas.realProduct_representative line 1587
  122. lemma OAI.YauCounterexamples.CompactMetricAtlas.laplacian_mem_realH line 1594
  123. def OAI.YauCounterexamples.CompactMetricAtlas.realLaplacian line 1603
  124. lemma OAI.YauCounterexamples.CompactMetricAtlas.resolvent_mem_realH line 1607
  125. def OAI.YauCounterexamples.CompactMetricAtlas.realResolvent line 1625
  126. lemma OAI.YauCounterexamples.CompactMetricAtlas.realResolvent_norm_bound line 1630
  127. def OAI.YauCounterexamples.boundedDivergence line 1648
  128. lemma OAI.YauCounterexamples.boundedDivergence_norm line 1652
  129. def OAI.YauCounterexamples.CompactMetricAtlas.realValue line 1691
  130. lemma OAI.YauCounterexamples.CompactMetricAtlas.ofReal_realValue line 1694
  131. lemma OAI.YauCounterexamples.CompactMetricAtlas.realValue_add line 1698
  132. lemma OAI.YauCounterexamples.CompactMetricAtlas.realValue_sub line 1703
  133. lemma OAI.YauCounterexamples.CompactMetricAtlas.realValue_smul line 1708
  134. lemma OAI.YauCounterexamples.CompactMetricAtlas.realValue_product line 1713
  135. lemma OAI.YauCounterexamples.CompactMetricAtlas.realValue_inclusion line 1721
  136. lemma OAI.YauCounterexamples.CompactMetricAtlas.realValue_C2 line 1729
  137. lemma OAI.YauCounterexamples.CompactMetricAtlas.realValue_laplacian line 1734
  138. def OAI.YauCounterexamples.CompactMetricAtlas.realDivergence line 1742
  139. lemma OAI.YauCounterexamples.CompactMetricAtlas.realDivergence_value line 1749
  140. lemma OAI.YauCounterexamples.CompactMetricAtlas.realResolvent_value line 1768
  141. def OAI.YauCounterexamples.CompactMetricAtlas.realOfSmooth line 1783
  142. lemma OAI.YauCounterexamples.CompactMetricAtlas.realOfSmooth_value line 1789
  143. def OAI.YauCounterexamples.CompactMetricAtlas.ChartJetBound line 1833
  144. lemma OAI.YauCounterexamples.CompactMetricAtlas.chart_jet_representative_bound line 1838
  145. theorem OAI.YauCounterexamples.CompactMetricAtlas.exists_chart_jet_constant line 1855
  146. lemma OAI.YauCounterexamples.schwartz_L2_compact_bound line 1913
  147. lemma OAI.YauCounterexamples.schwartz_word_bound_of_jets line 1939
  148. theorem OAI.YauCounterexamples.CompactMetricAtlas.exists_jet_sobolev_constant line 1964
  149. lemma OAI.YauCounterexamples.chart_derivative_ne_zero_transfer line 2008
  150. lemma OAI.YauCounterexamples.CompactMetricAtlas.localization_real_germ line 2031
  151. abbrev OAI.YauCounterexamples.CompactMetricAtlas.highIndex line 2044
  152. lemma OAI.YauCounterexamples.CompactMetricAtlas.highIndex_bound line 2046
  153. lemma OAI.YauCounterexamples.CompactMetricAtlas.highIndex_bound_one line 2050
  154. def OAI.YauCounterexamples.CompactMetricAtlas.localizedRealValue line 2054
  155. def OAI.YauCounterexamples.CompactMetricAtlas.localizedFirstJet line 2058
  156. lemma OAI.YauCounterexamples.CompactMetricAtlas.localizedFirstJet_continuous line 2062
  157. lemma OAI.YauCounterexamples.CompactMetricAtlas.localizedFirstJet_ne_zero line 2073
  158. lemma OAI.YauCounterexamples.CompactMetricAtlas.eventually_localizedFirstJet_ne_zero line 2092
  159. lemma OAI.YauCounterexamples.CompactMetricAtlas.regular_of_localizedFirstJet line 2107
  160. theorem OAI.YauCounterexamples.CompactMetricAtlas.eventually_regular_realValue line 2132