OAI/Analysis/Steinitz/HeatL2.lean

GitHub source file

158 declarations, 0 contain sorry, 0 declared as axioms

Heat operators, weak coordinate derivatives, and Dirichlet energy.

  1. lemma OAI.HeatL2.memLp_mul_bounded line 17
  2. def OAI.HeatL2.mulLp line 25
  3. lemma OAI.HeatL2.mulLp_coe line 29
  4. def OAI.HeatL2.mulLinear line 33
  5. lemma OAI.HeatL2.mulLp_norm_le line 51
  6. def OAI.HeatL2.mulOp line 59
  7. lemma OAI.HeatL2.mulOp_coe line 63
  8. lemma OAI.HeatL2.mulOp_norm_le line 67
  9. lemma OAI.HeatL2.norm_sq_integral line 71
  10. lemma OAI.HeatL2.inner_mulOp line 78
  11. lemma OAI.HeatL2.inner_real_mulOp line 88
  12. def OAI.HeatL2.translate line 109
  13. lemma OAI.HeatL2.translate_coe line 112
  14. def OAI.HeatL2.phase line 116
  15. lemma OAI.HeatL2.phase_continuous line 119
  16. lemma OAI.HeatL2.phase_norm line 123
  17. def OAI.HeatL2.phaseOp line 125
  18. lemma OAI.HeatL2.phaseOp_coe line 129
  19. lemma OAI.HeatL2.translate_schwartz line 133
  20. lemma OAI.HeatL2.schwartz_fourier_translate line 141
  21. lemma OAI.HeatL2.fourier_translate line 152
  22. lemma OAI.HeatL2.translate_sub_norm_sq line 167
  23. lemma OAI.HeatL2.translate_sub_translate_norm_sq line 187
  24. lemma OAI.HeatL2.translate_continuous line 201
  25. lemma OAI.HeatL2.integrable_weight line 247
  26. def OAI.HeatL2.spectralOp line 256
  27. lemma OAI.HeatL2.spectralOp_fourier line 263
  28. lemma OAI.HeatL2.spectralOp_norm_le line 272
  29. lemma OAI.HeatL2.spectralOp_inner line 284
  30. lemma OAI.HeatL2.spectralOp_positive line 297
  31. def OAI.HeatL2.heat line 308
  32. def OAI.HeatL2.energy line 313
  33. lemma OAI.HeatL2.heat_inner line 316
  34. lemma OAI.HeatL2.energy_nonneg line 336
  35. def OAI.HeatL2.loss line 345
  36. lemma OAI.HeatL2.loss_nonneg line 347
  37. lemma OAI.HeatL2.loss_le_one line 350
  38. lemma OAI.HeatL2.loss_le_self line 354
  39. lemma OAI.HeatL2.loss_add_le line 358
  40. lemma OAI.HeatL2.loss_sum_le line 364
  41. lemma OAI.HeatL2.loss_dilate_le line 375
  42. lemma OAI.HeatL2.loss_sum_dilate_le line 389
  43. lemma OAI.HeatL2.loss_mean_ge line 395
  44. lemma OAI.HeatL2.loss_lower line 405
  45. lemma OAI.HeatL2.bound_by_loss line 415
  46. lemma OAI.HeatL2.indicator_one_norm_le line 436
  47. def OAI.HeatL2.mask line 440
  48. lemma OAI.HeatL2.mask_coe line 445
  49. lemma OAI.HeatL2.mask_norm_le line 455
  50. lemma OAI.HeatL2.mask_idempotent line 462
  51. lemma OAI.HeatL2.mask_inner line 469
  52. lemma OAI.HeatL2.mask_adjoint line 477
  53. def OAI.HeatL2.supported line 486
  54. lemma OAI.HeatL2.mask_eq_self_iff line 489
  55. lemma OAI.HeatL2.positive_norm_le_iff line 508
  56. lemma OAI.HeatL2.positive_exists_form_gt line 529
  57. def OAI.HeatL2.compressedHeat line 541
  58. lemma OAI.HeatL2.heat_positive line 546
  59. lemma OAI.HeatL2.compressedHeat_positive line 549
  60. lemma OAI.HeatL2.compressedHeat_inner line 555
  61. lemma OAI.HeatL2.compressedHeat_norm_le_one line 563
  62. lemma OAI.HeatL2.integrable_translate line 582
  63. lemma OAI.HeatL2.average_norm_le line 589
  64. def OAI.HeatL2.averageLinear line 595
  65. def OAI.HeatL2.average line 603
  66. lemma OAI.HeatL2.average_apply line 607
  67. lemma OAI.HeatL2.inner_average line 610
  68. def OAI.HeatL2.gaussianSymbol line 632
  69. lemma OAI.HeatL2.gaussianSymbol_nonneg line 636
  70. lemma OAI.HeatL2.gaussianSymbol_continuous line 641
  71. lemma OAI.HeatL2.integral_phase_gaussian line 646
  72. lemma OAI.HeatL2.average_gaussian_eq_heat line 660
  73. lemma OAI.HeatL2.integrable_energy line 692
  74. lemma OAI.HeatL2.energy_le_norm_sq line 702
  75. lemma OAI.HeatL2.energy_comparison line 710
  76. lemma OAI.HeatL2.energy_mean_ge line 719
  77. def OAI.HeatL2.directionalSymbol line 739
  78. lemma OAI.HeatL2.directionalSymbol_nonneg line 742
  79. lemma OAI.HeatL2.directionalSymbol_continuous line 745
  80. lemma OAI.HeatL2.phase_sub_one_sq_le line 750
  81. lemma OAI.HeatL2.phase_sub_one_sq_le_four line 763
  82. lemma OAI.HeatL2.directional_translate_bound line 768
  83. lemma OAI.HeatL2.sqrt_pair_sub_sq_le line 795
  84. lemma OAI.HeatL2.sqrt_mix_sub_sq_le line 809
  85. lemma OAI.HeatL2.sqrt_mix_bound line 820
  86. def OAI.HeatL2.mixFun line 833
  87. lemma OAI.HeatL2.mixFun_memLp line 836
  88. def OAI.HeatL2.mixture line 853
  89. lemma OAI.HeatL2.mixture_coe line 856
  90. lemma OAI.HeatL2.mixFun_norm_sq line 859
  91. lemma OAI.HeatL2.mixture_norm_sq line 864
  92. lemma OAI.HeatL2.mixFun_sub_sq_le line 874
  93. lemma OAI.HeatL2.mixture_supported line 885
  94. lemma OAI.HeatL2.mixture_translation_sq_le line 899
  95. lemma OAI.HeatL2.integrable_difference_sq line 935
  96. lemma OAI.HeatL2.average_difference_sq line 947
  97. lemma OAI.HeatL2.gaussian_energy_difference line 967
  98. lemma OAI.selfAdjoint_norm_pow line 977
  99. lemma OAI.HeatL2.abs_memLp line 1001
  100. def OAI.HeatL2.absolute line 1006
  101. lemma OAI.HeatL2.absolute_coe line 1009
  102. lemma OAI.HeatL2.absolute_norm line 1012
  103. def OAI.HeatL2.oneLp line 1021
  104. lemma OAI.HeatL2.oneLp_coe line 1023
  105. lemma OAI.HeatL2.integral_norm_le line 1025
  106. structure OAI.HeatL2.BoundedKernel line 1039
  107. def OAI.HeatL2.kernelFun line 1051
  108. lemma OAI.HeatL2.kernel_section_integrable line 1054
  109. lemma OAI.HeatL2.kernelFun_bound line 1064
  110. lemma OAI.HeatL2.kernelFun_norm_bound line 1075
  111. lemma OAI.HeatL2.kernelFun_memLp line 1080
  112. def OAI.HeatL2.kernelLp line 1087
  113. lemma OAI.HeatL2.kernelLp_coe line 1090
  114. lemma OAI.HeatL2.kernelLp_add line 1093
  115. lemma OAI.HeatL2.kernelLp_smul line 1105
  116. lemma OAI.HeatL2.kernelLp_norm_le line 1117
  117. def OAI.HeatL2.kernelLinear line 1126
  118. def OAI.HeatL2.kernelOp line 1131
  119. lemma OAI.HeatL2.kernelOp_coe line 1134
  120. lemma OAI.HeatL2.inner_one_eq_integral line 1136
  121. lemma OAI.HeatL2.kernelFun_domination line 1143
  122. lemma OAI.HeatL2.kernelOp_domination line 1159
  123. lemma OAI.HeatL2.kernel_pow_domination line 1166
  124. lemma OAI.HeatL2.kernel_norm_le_integral line 1174
  125. def OAI.HeatL2.pathMass line 1183
  126. lemma OAI.HeatL2.pathMass_eq_integral line 1186
  127. lemma OAI.HeatL2.pathMass_nonneg line 1192
  128. lemma OAI.HeatL2.pathMass_le line 1206
  129. lemma OAI.HeatL2.kernel_pow_norm_le_pathMass line 1221
  130. lemma OAI.HeatL2.kernel_pair_integrable line 1256
  131. lemma OAI.HeatL2.inner_kernel line 1271
  132. lemma OAI.HeatL2.kernelOp_selfAdjoint line 1278
  133. lemma OAI.HeatL2.le_of_pow_le_const_mul_pow line 1299
  134. lemma OAI.HeatL2.kernel_norm_pow_le_pathMass line 1317
  135. lemma OAI.HeatL2.norm_lower_of_pathMass_lower line 1323
  136. def OAI.HeatL2.extendLp line 1341
  137. lemma OAI.HeatL2.extendLp_coe line 1343
  138. lemma OAI.HeatL2.extendLp_norm line 1345
  139. lemma OAI.HeatL2.extendLp_supported line 1349
  140. def OAI.HeatL2.restrictLp line 1352
  141. lemma OAI.HeatL2.restrictLp_coe line 1354
  142. lemma OAI.HeatL2.extend_restrict line 1356
  143. lemma OAI.HeatL2.extend_restrict_supported line 1364
  144. lemma OAI.HeatL2.weighted_rpow_jensen line 1374
  145. lemma OAI.HeatL2.heat_inner_integral line 1407
  146. lemma OAI.HeatL2.heat_form_rpow line 1413
  147. lemma OAI.HeatL2.inner_translate_integral line 1449
  148. lemma OAI.HeatL2.integrable_translate_pair line 1457
  149. lemma OAI.HeatL2.inner_average_spatial line 1490
  150. lemma OAI.HeatL2.inner_average_density line 1502
  151. def OAI.HeatL2.densityKernel line 1523
  152. lemma OAI.HeatL2.integral_extend_mul line 1534
  153. lemma OAI.HeatL2.integral_extend_conj line 1544
  154. lemma OAI.HeatL2.inner_extend line 1554
  155. lemma OAI.HeatL2.densityKernel_inner line 1565
  156. lemma OAI.HeatL2.extend_kernel_eq line 1584
  157. lemma OAI.HeatL2.restrictLp_norm_le line 1596
  158. lemma OAI.HeatL2.compressedAverage_kernel_norm line 1600