OAI/Analysis/RCDHeat/ExistingAnalytic.lean

GitHub source file

590 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: ExistingAnalytic.

  1. theorem OAI.RegularPointCoordinates.heatAt_exponential_square_integral_le line 26
  2. theorem OAI.RegularPointCoordinates.heatAt_tail_square_integral_le line 37
  3. theorem OAI.RegularPointCoordinates.exponential_weighted_moment_young line 65
  4. theorem OAI.RegularPointCoordinates.heatAt_weighted_moment_integrable line 75
  5. theorem OAI.RegularPointCoordinates.heatAt_weighted_moment_integral_le line 88
  6. theorem OAI.RegularPointCoordinates.heatAt_tail_moment_integral_le line 108
  7. def OAI.RegularPointCoordinates.entropyLogTest line 150
  8. def OAI.RegularPointCoordinates.entropyScore line 153
  9. theorem OAI.RegularPointCoordinates.entropyLogTest_low line 155
  10. theorem OAI.RegularPointCoordinates.entropyLogTest_high line 160
  11. theorem OAI.RegularPointCoordinates.entropyLogTest_middle line 165
  12. theorem OAI.RegularPointCoordinates.entropyLogTest_abs_le line 169
  13. theorem OAI.RegularPointCoordinates.continuous_entropyLogTest line 181
  14. theorem OAI.RegularPointCoordinates.entropyScore_difference_le line 188
  15. theorem OAI.RegularPointCoordinates.entropyScore_le_logTest line 200
  16. theorem OAI.RegularPointCoordinates.entropyScore_logTest_nonneg line 220
  17. theorem OAI.RegularPointCoordinates.entropyScore_logTest_mono line 225
  18. theorem OAI.RegularPointCoordinates.entropyScore_logTest_tendsto line 230
  19. def OAI.RegularPointCoordinates.entropyDualValue line 274
  20. def OAI.RegularPointCoordinates.entropyDual line 278
  21. theorem OAI.RegularPointCoordinates.lowerSemicontinuous_entropyDual line 284
  22. theorem OAI.RegularPointCoordinates.entropy_fenchel line 292
  23. theorem OAI.RegularPointCoordinates.rnDeriv_integral_mul line 306
  24. theorem OAI.RegularPointCoordinates.entropyDual_le_klDiv line 316
  25. theorem OAI.RegularPointCoordinates.clip_error_le line 347
  26. def OAI.RegularPointCoordinates.clipBCF line 361
  27. theorem OAI.RegularPointCoordinates.clipBCF_abs_le line 370
  28. theorem OAI.RegularPointCoordinates.exp_error_le line 376
  29. theorem OAI.RegularPointCoordinates.bounded_measurable_integrable line 386
  30. theorem OAI.RegularPointCoordinates.bounded_exp_integrable line 392
  31. theorem OAI.RegularPointCoordinates.entropyDualValue_error line 403
  32. theorem OAI.RegularPointCoordinates.entropyDualValue_measurable_le line 443
  33. theorem OAI.RegularPointCoordinates.entropyDualValue_bounded_measurable_le line 483
  34. theorem OAI.RegularPointCoordinates.absolutelyContinuous_of_entropyDual_ne_top line 495
  35. theorem OAI.RegularPointCoordinates.entropyDual_eq_klDiv line 538
  36. theorem OAI.RegularPointCoordinates.lowerSemicontinuous_klDiv line 598
  37. theorem OAI.RegularPointCoordinates.klFun_sub_le_log line 616
  38. def OAI.RegularPointCoordinates.entropyPerturb line 623
  39. def OAI.RegularPointCoordinates.entropyGap line 626
  40. def OAI.RegularPointCoordinates.entropyMixError line 629
  41. theorem OAI.RegularPointCoordinates.entropyMixError_nonneg line 632
  42. theorem OAI.RegularPointCoordinates.entropyGap_pos line 636
  43. theorem OAI.RegularPointCoordinates.entropyGap_mono line 640
  44. theorem OAI.RegularPointCoordinates.entropyPerturb_nonneg line 647
  45. theorem OAI.RegularPointCoordinates.entropyPerturb_kl_bound line 657
  46. theorem OAI.RegularPointCoordinates.exists_entropy_decreasing_perturbation line 720
  47. theorem OAI.RegularPointCoordinates.rnDeriv_le_const_of_le_smul line 828
  48. theorem OAI.RegularPointCoordinates.renyiIntegral_le_ac_support_volume line 838
  49. theorem OAI.RegularPointCoordinates.cd_midpoint_renyi_lower line 886
  50. theorem OAI.RegularPointCoordinates.FullCD.exists_midpoint_ac_support_bound line 933
  51. theorem OAI.RegularPointCoordinates.measure_sub_add_of_singular line 982
  52. theorem OAI.RegularPointCoordinates.rnDeriv_excess line 995
  53. theorem OAI.RegularPointCoordinates.transportExcessMass_add_le line 1017
  54. theorem OAI.RegularPointCoordinates.ac_support_saturated_of_excess_add_eq line 1030
  55. theorem OAI.RegularPointCoordinates.transportExcessMass_remove line 1055
  56. theorem OAI.RegularPointCoordinates.ac_support_saturated_of_minimizing_replacement line 1082
  57. theorem OAI.RegularPointCoordinates.excess_eq_singular_add_withDensity line 1094
  58. theorem OAI.RegularPointCoordinates.positive_region_mass line 1113
  59. theorem OAI.RegularPointCoordinates.exists_buffer_positive_region line 1155
  60. theorem OAI.RegularPointCoordinates.buffer_fraction_le_excess line 1192
  61. abbrev OAI.RegularPointCoordinates.midpointTime line 1246
  62. theorem OAI.RegularPointCoordinates.map_sub_of_le line 1251
  63. theorem OAI.RegularPointCoordinates.FullCD.replace_midpoint_region line 1262
  64. theorem OAI.RegularPointCoordinates.FullCD.improve_saturation_of_positive_minimal_excess line 1384
  65. theorem OAI.RegularPointCoordinates.FullCD.excess_minimizer_zero line 1474
  66. theorem OAI.RegularPointCoordinates.withDensity_ofReal_rnDeriv line 1547
  67. theorem OAI.RegularPointCoordinates.entropyPerturb_withDensity line 1558
  68. theorem OAI.RegularPointCoordinates.klDiv_eq_of_real_density line 1601
  69. theorem OAI.RegularPointCoordinates.exists_measure_entropy_decrease line 1622
  70. theorem OAI.RegularPointCoordinates.optimal_geodesic_plan_bounded line 1706
  71. def OAI.RegularPointCoordinates.clippedPathCost line 1741
  72. theorem OAI.RegularPointCoordinates.lintegral_clippedPathCost line 1757
  73. def OAI.RegularPointCoordinates.OptimalGeodesicPlans line 1771
  74. theorem OAI.RegularPointCoordinates.bounded_path_cost line 1776
  75. theorem OAI.RegularPointCoordinates.isCompact_optimal_geodesic_plans line 1791
  76. theorem OAI.RegularPointCoordinates.exists_optimal_geodesic_plan_minimizing_excess line 1840
  77. theorem OAI.RegularPointCoordinates.exists_optimal_geodesic_plan_minimizing_entropy line 1870
  78. theorem OAI.RegularPointCoordinates.rnDeriv_restrict_reference line 1901
  79. theorem OAI.RegularPointCoordinates.ac_support_volume_restrict line 1912
  80. theorem OAI.RegularPointCoordinates.FullCD.improve_localized_saturation line 1935
  81. theorem OAI.RegularPointCoordinates.FullCD.localized_excess_minimizer_zero line 2036
  82. theorem OAI.RegularPointCoordinates.FullCD.exists_compressed_midpoint_at_capacity line 2109
  83. def OAI.RegularPointCoordinates.midpointCapacity line 2179
  84. theorem OAI.RegularPointCoordinates.midpointCapacity_ne_top line 2182
  85. theorem OAI.RegularPointCoordinates.midpointCapacity_pos line 2189
  86. theorem OAI.RegularPointCoordinates.midpointCapacity_fill line 2196
  87. theorem OAI.RegularPointCoordinates.probability_capacity_ne_zero line 2209
  88. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.exists_compressed_midpoint line 2218
  89. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compressed_replacement_subplan line 2261
  90. theorem OAI.RegularPointCoordinates.klDiv_ne_top_of_bounded_density line 2363
  91. theorem OAI.RegularPointCoordinates.superlevel_mass_ne_zero_of_not_compressed line 2377
  92. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.entropy_minimizer_compressed line 2397
  93. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.exists_compressed_entropy_minimizing_midpoint line 2471
  94. theorem OAI.RegularPointCoordinates.rnDeriv_eq_indicator_of_supported line 2533
  95. theorem OAI.RegularPointCoordinates.density_transform_eq_indicator line 2539
  96. theorem OAI.RegularPointCoordinates.density_rpow_half_integrable_of_supported line 2550
  97. theorem OAI.RegularPointCoordinates.rnDeriv_localized line 2570
  98. theorem OAI.RegularPointCoordinates.localized_density_transform line 2579
  99. theorem OAI.RegularPointCoordinates.boltzmannEntropy_localized line 2593
  100. theorem OAI.RegularPointCoordinates.entropy_integrable_localized_iff line 2602
  101. theorem OAI.RegularPointCoordinates.toReal_klDiv_eq_boltzmannEntropy line 2613
  102. theorem OAI.RegularPointCoordinates.entropy_integrable_of_klDiv_ne_top line 2622
  103. theorem OAI.RegularPointCoordinates.entropy_integrable_of_bounded_support line 2629
  104. theorem OAI.RegularPointCoordinates.integrable_dist_sq_of_ae_bounded line 2653
  105. theorem OAI.RegularPointCoordinates.FullCD.exists_bounded_support_entropy_plan line 2664
  106. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.exists_compressed_entropy_midpoint line 2721
  107. def OAI.RegularPointCoordinates.OptimalPlanDistanceBound line 2797
  108. theorem OAI.RegularPointCoordinates.FullCD.replace_midpoint_region_short line 2803
  109. theorem OAI.RegularPointCoordinates.FullCD.improve_localized_saturation_short line 2930
  110. theorem OAI.RegularPointCoordinates.FullCD.localized_excess_minimizer_zero_short line 3030
  111. theorem OAI.RegularPointCoordinates.FullCD.exists_compressed_midpoint_at_capacity_short line 3096
  112. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.exists_compressed_midpoint_short line 3148
  113. theorem OAI.RegularPointCoordinates.OptimalPlanDistanceBound.normalized_subplan line 3191
  114. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compressed_replacement_subplan_short line 3217
  115. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.entropy_minimizer_compressed_short line 3319
  116. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.exists_compressed_entropy_minimizing_midpoint_short line 3394
  117. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.exists_compressed_entropy_midpoint_short line 3444
  118. theorem OAI.RegularPointCoordinates.exists_coupling_common_map line 3520
  119. abbrev OAI.RegularPointCoordinates.MatchedPaths line 3587
  120. def OAI.RegularPointCoordinates.leftHalfTime line 3590
  121. def OAI.RegularPointCoordinates.rightHalfTime line 3591
  122. theorem OAI.RegularPointCoordinates.continuous_leftHalfTime line 3593
  123. theorem OAI.RegularPointCoordinates.continuous_rightHalfTime line 3595
  124. theorem OAI.RegularPointCoordinates.leftHalfTime_zero line 3598
  125. theorem OAI.RegularPointCoordinates.rightHalfTime_one line 3599
  126. theorem OAI.RegularPointCoordinates.leftHalfTime_midpoint line 3600
  127. theorem OAI.RegularPointCoordinates.rightHalfTime_midpoint line 3602
  128. theorem OAI.RegularPointCoordinates.leftHalfTime_coe line 3605
  129. theorem OAI.RegularPointCoordinates.rightHalfTime_coe line 3609
  130. def OAI.RegularPointCoordinates.joinMatched line 3613
  131. theorem OAI.RegularPointCoordinates.joinMatched_continuous line 3623
  132. theorem OAI.RegularPointCoordinates.joinMatched_zero line 3639
  133. theorem OAI.RegularPointCoordinates.joinMatched_one line 3641
  134. theorem OAI.RegularPointCoordinates.joinMatched_midpoint line 3643
  135. theorem OAI.RegularPointCoordinates.joinMatched_apply_left line 3647
  136. theorem OAI.RegularPointCoordinates.joinMatched_apply_right line 3650
  137. theorem OAI.RegularPointCoordinates.isGeodesic_of_dist_le line 3659
  138. theorem OAI.RegularPointCoordinates.joinMatched_isGeodesic line 3686
  139. theorem OAI.RegularPointCoordinates.transportCost_plan_lintegral line 3742
  140. theorem OAI.RegularPointCoordinates.geodesic_plan_cost line 3749
  141. theorem OAI.RegularPointCoordinates.geodesic_plan_optimal_marginals line 3763
  142. theorem OAI.RegularPointCoordinates.quadratic_gluing_saturation line 3793
  143. theorem OAI.RegularPointCoordinates.measurableSet_matchedPaths line 3861
  144. theorem OAI.RegularPointCoordinates.exists_matched_path_law line 3866
  145. theorem OAI.RegularPointCoordinates.matched_law_eval line 3890
  146. theorem OAI.RegularPointCoordinates.matched_law_eval_right line 3897
  147. theorem OAI.RegularPointCoordinates.joined_law_eval_zero line 3918
  148. theorem OAI.RegularPointCoordinates.joined_law_eval_one line 3925
  149. theorem OAI.RegularPointCoordinates.joined_law_eval_midpoint line 3932
  150. theorem OAI.RegularPointCoordinates.midpoint_matched_law_optimal line 3939
  151. theorem OAI.RegularPointCoordinates.midpoint_laws_distance_bound line 4054
  152. theorem OAI.RegularPointCoordinates.geodesic_subpath_law line 4093
  153. theorem OAI.RegularPointCoordinates.OptimalPlanDistanceBound.midpoint_halves line 4111
  154. def OAI.RegularPointCoordinates.compressionStep line 4146
  155. def OAI.RegularPointCoordinates.compressionBudget line 4149
  156. theorem OAI.RegularPointCoordinates.midpointCapacity_eq line 4152
  157. theorem OAI.RegularPointCoordinates.midpointCapacity_le_compressionStep line 4165
  158. theorem OAI.RegularPointCoordinates.le_compressionStep line 4181
  159. theorem OAI.RegularPointCoordinates.compressionStep_ne_top line 4188
  160. theorem OAI.RegularPointCoordinates.compressionBudget_halve line 4191
  161. theorem OAI.RegularPointCoordinates.le_compressionBudget line 4198
  162. theorem OAI.RegularPointCoordinates.compressionBudget_ne_top line 4202
  163. abbrev OAI.RegularPointCoordinates.lowerTime line 4208
  164. abbrev OAI.RegularPointCoordinates.upperTime line 4209
  165. theorem OAI.RegularPointCoordinates.coe_lowerTime line 4211
  166. theorem OAI.RegularPointCoordinates.coe_upperTime line 4214
  167. def OAI.RegularPointCoordinates.dyadicGrid line 4218
  168. theorem OAI.RegularPointCoordinates.dyadicGrid_endpoints line 4222
  169. theorem OAI.RegularPointCoordinates.dyadicGrid_mono line 4230
  170. theorem OAI.RegularPointCoordinates.dyadicGrid_approx line 4242
  171. theorem OAI.RegularPointCoordinates.dense_dyadicGrid line 4266
  172. theorem OAI.RegularPointCoordinates.joinMatched_lowerTime line 4279
  173. theorem OAI.RegularPointCoordinates.joinMatched_upperTime line 4289
  174. theorem OAI.RegularPointCoordinates.joined_law_eval_lowerTime line 4299
  175. theorem OAI.RegularPointCoordinates.joined_law_eval_upperTime line 4306
  176. def OAI.RegularPointCoordinates.entropyChord line 4323
  177. theorem OAI.RegularPointCoordinates.entropyChord_zero line 4326
  178. theorem OAI.RegularPointCoordinates.entropyChord_one line 4328
  179. theorem OAI.RegularPointCoordinates.entropyChord_lower line 4331
  180. theorem OAI.RegularPointCoordinates.entropyChord_upper line 4338
  181. theorem OAI.RegularPointCoordinates.finiteSecondMoment_of_bounded line 4349
  182. theorem OAI.RegularPointCoordinates.geodesic_midpoint_wasserstein_sq line 4359
  183. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.exists_dyadic_compressed_entropy_plan line 4397
  184. theorem OAI.RegularPointCoordinates.compact_dyadic_selection line 4529
  185. theorem OAI.RegularPointCoordinates.continuous_time_marginals line 4561
  186. def OAI.RegularPointCoordinates.compressedKLConstraint line 4593
  187. theorem OAI.RegularPointCoordinates.isClosed_compressedKLConstraint line 4597
  188. theorem OAI.RegularPointCoordinates.entropy_bound_localized_iff line 4612
  189. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.exists_compressed_entropy_plan line 4658
  190. theorem OAI.RegularPointCoordinates.optimalPlanDistanceBound_of_bounded line 4741
  191. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.exists_bounded_entropy_plan line 4762
  192. theorem OAI.RegularPointCoordinates.entropy_plan_lp_signed_secant line 4828
  193. theorem OAI.RegularPointCoordinates.entropy_plan_lp_signed_derivative_le line 4866
  194. theorem OAI.RegularPointCoordinates.compact_entropy_plan_sobolev_bound line 4903
  195. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compact_log_subgradient line 4952
  196. theorem OAI.RegularPointCoordinates.integral_sq_le_mass_mul_sq line 5018
  197. theorem OAI.RegularPointCoordinates.testPlan_square_fubini line 5048
  198. theorem OAI.RegularPointCoordinates.IsRelaxedSlope.testPlan_integrated_square line 5078
  199. theorem OAI.RegularPointCoordinates.uniformOn_le_scaled line 5147
  200. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.dirichlet_integral_coercivity line 5154
  201. def OAI.RegularPointCoordinates.SobolevSpace.restrictLp line 5227
  202. theorem OAI.RegularPointCoordinates.SobolevSpace.restrictLp_coe line 5233
  203. theorem OAI.RegularPointCoordinates.SobolevSpace.restrictLp_eq_zero_iff line 5238
  204. def OAI.RegularPointCoordinates.SobolevSpace.dirichletCore line 5248
  205. def OAI.RegularPointCoordinates.SobolevSpace.dirichlet line 5270
  206. instance OAI.RegularPointCoordinates.SobolevSpace.dirichlet_completeSpace line 5273
  207. theorem OAI.RegularPointCoordinates.SobolevSpace.dirichlet_zero_off line 5278
  208. theorem OAI.RegularPointCoordinates.energyForm_multiplier_lower line 5306
  209. theorem OAI.RegularPointCoordinates.lpMultiplier_neg_weight line 5394
  210. theorem OAI.RegularPointCoordinates.lpAbs_norm line 5402
  211. theorem OAI.RegularPointCoordinates.energyForm_multiplier_error line 5410
  212. def OAI.RegularPointCoordinates.integerFold line 5457
  213. theorem OAI.RegularPointCoordinates.integerFold_lipschitz line 5459
  214. theorem OAI.RegularPointCoordinates.integerFold_zero line 5461
  215. theorem OAI.RegularPointCoordinates.integerFold_nonneg line 5465
  216. theorem OAI.RegularPointCoordinates.integerFold_le_one line 5467
  217. theorem OAI.RegularPointCoordinates.integerFold_affine line 5474
  218. def OAI.RegularPointCoordinates.scalarFold line 5485
  219. theorem OAI.RegularPointCoordinates.scalarFold_zero line 5487
  220. theorem OAI.RegularPointCoordinates.scalarFold_lipschitz line 5489
  221. theorem OAI.RegularPointCoordinates.scalarFold_bounds line 5500
  222. theorem OAI.RegularPointCoordinates.scalarFold_affine line 5505
  223. theorem OAI.RegularPointCoordinates.scalarFold_tendsto line 5513
  224. theorem OAI.RegularPointCoordinates.SobolevSpace.minimalSlope_eq_on_diff_level line 5532
  225. def OAI.RegularPointCoordinates.SobolevSpace.fold line 5551
  226. theorem OAI.RegularPointCoordinates.SobolevSpace.fold_coe line 5555
  227. theorem OAI.RegularPointCoordinates.SobolevSpace.minimalSlope_fold line 5560
  228. theorem OAI.RegularPointCoordinates.SobolevSpace.fold_tendsto_zero line 5585
  229. def OAI.RegularPointCoordinates.SobolevSpace.signed line 5611
  230. def OAI.RegularPointCoordinates.slopePair line 5614
  231. theorem OAI.RegularPointCoordinates.slopePair_signed line 5618
  232. theorem OAI.RegularPointCoordinates.slopePair_on_affine line 5630
  233. def OAI.RegularPointCoordinates.foldShift line 5653
  234. theorem OAI.RegularPointCoordinates.SobolevSpace.fold_affine_coe line 5657
  235. theorem OAI.RegularPointCoordinates.slopePair_fold line 5669
  236. def OAI.RegularPointCoordinates.SobolevSpace.mulLipschitzLinear line 5705
  237. def OAI.RegularPointCoordinates.multiplierGradientSquare line 5714
  238. theorem OAI.RegularPointCoordinates.multiplierGradientSquare_integrable line 5718
  239. theorem OAI.RegularPointCoordinates.multiplierGradientSquare_integral line 5726
  240. theorem OAI.RegularPointCoordinates.energyForm_linear_parallelogram line 5735
  241. theorem OAI.RegularPointCoordinates.multiplierGradientSquare_error_tendsto line 5743
  242. theorem OAI.RegularPointCoordinates.minimalSlope_norm_add_le line 5762
  243. theorem OAI.RegularPointCoordinates.multiplierGradientSquare_fold line 5773
  244. theorem OAI.RegularPointCoordinates.multiplierGradientSquare_fold_pair line 5778
  245. theorem OAI.RegularPointCoordinates.multiplierGradientSquare_parallelogram line 5806
  246. theorem OAI.RegularPointCoordinates.lpMultiplier_add_weight line 5879
  247. theorem OAI.RegularPointCoordinates.multiplierGradientSquare_add_weight line 5887
  248. theorem OAI.RegularPointCoordinates.multiplierGradientSquare_parallelogram_signed line 5892
  249. theorem OAI.RegularPointCoordinates.finiteMeasure_eq_of_lipschitz_compact line 5932
  250. theorem OAI.RegularPointCoordinates.integrable_nonneg_eq_of_lipschitz_compact line 5973
  251. theorem OAI.RegularPointCoordinates.minimalSlope_pointwise_parallelogram line 6002
  252. theorem OAI.RegularPointCoordinates.weightedGradientSquare_nonneg line 6051
  253. theorem OAI.RegularPointCoordinates.weightedGradientSquare_smul line 6055
  254. theorem OAI.RegularPointCoordinates.weightedGradientSquare_zero line 6066
  255. theorem OAI.RegularPointCoordinates.weightedGradientSquare_parallelogram line 6070
  256. theorem OAI.RegularPointCoordinates.weightedGradientSquare_line line 6085
  257. theorem OAI.RegularPointCoordinates.weightedGradientPair_eq_bracket line 6105
  258. def OAI.RegularPointCoordinates.localGamma line 6133
  259. theorem OAI.RegularPointCoordinates.localGamma_integrable line 6138
  260. theorem OAI.RegularPointCoordinates.integral_localGamma line 6145
  261. theorem OAI.RegularPointCoordinates.localGamma_memL1 line 6154
  262. theorem OAI.RegularPointCoordinates.localGamma_add_left line 6158
  263. theorem OAI.RegularPointCoordinates.localGamma_smul_left line 6170
  264. theorem OAI.RegularPointCoordinates.localGamma_comm line 6183
  265. theorem OAI.RegularPointCoordinates.localGamma_self line 6193
  266. theorem OAI.RegularPointCoordinates.localGamma_add_right line 6204
  267. theorem OAI.RegularPointCoordinates.localGamma_smul_right line 6210
  268. theorem OAI.RegularPointCoordinates.integral_localGamma_eq_energyForm line 6217
  269. theorem OAI.RegularPointCoordinates.localGamma_abs_le line 6237
  270. theorem OAI.RegularPointCoordinates.localGamma_sub_left line 6254
  271. theorem OAI.RegularPointCoordinates.localGamma_eq_on_eq line 6262
  272. theorem OAI.RegularPointCoordinates.localGamma_zero_on_level line 6274
  273. theorem OAI.RegularPointCoordinates.SobolevSpace.comp_sub_linear line 6294
  274. theorem OAI.RegularPointCoordinates.localGamma_comp_C1 line 6310
  275. theorem OAI.RegularPointCoordinates.nonneg_mul_regularizedReciprocal_le_one line 6364
  276. theorem OAI.RegularPointCoordinates.regularizedReciprocal_tendsto_pos line 6372
  277. theorem OAI.RegularPointCoordinates.localGamma_comp_C1_right line 6385
  278. theorem OAI.RegularPointCoordinates.weighted_log_pair_integral line 6396
  279. theorem OAI.RegularPointCoordinates.weighted_log_pair_tendsto line 6419
  280. theorem OAI.RegularPointCoordinates.localGamma_square line 6469
  281. theorem OAI.RegularPointCoordinates.localGamma_product_left line 6490
  282. theorem OAI.RegularPointCoordinates.localGamma_product_right line 6522
  283. def OAI.RegularPointCoordinates.SobolevSpace.cutoffLinear line 6536
  284. theorem OAI.RegularPointCoordinates.SobolevSpace.cutoffLinear_toLp line 6547
  285. def OAI.RegularPointCoordinates.SobolevSpace.cutoffCLM line 6555
  286. theorem OAI.RegularPointCoordinates.SobolevSpace.cutoffCLM_coe line 6570
  287. theorem OAI.RegularPointCoordinates.SobolevSpace.cutoffCLM_mem_dirichlet line 6582
  288. theorem OAI.RegularPointCoordinates.caccioppoli_scalar line 6612
  289. theorem OAI.RegularPointCoordinates.bounded_square_weight_integrable line 6629
  290. theorem OAI.RegularPointCoordinates.caccioppoli_weighted line 6636
  291. theorem OAI.RegularPointCoordinates.caccioppoli_forced line 6687
  292. theorem OAI.RegularPointCoordinates.bounded_square_tail_integral line 6741
  293. theorem OAI.RegularPointCoordinates.caccioppoli_tail line 6756
  294. theorem OAI.RegularPointCoordinates.caccioppoli_exterior line 6826
  295. theorem OAI.RegularPointCoordinates.SobolevSpace.cutoff_error_slope_sq line 6932
  296. theorem OAI.RegularPointCoordinates.SobolevSpace.radial_cutoff_error_norm_sq line 6975
  297. theorem OAI.RegularPointCoordinates.radialCutoff_mul_integrable line 7055
  298. theorem OAI.RegularPointCoordinates.radialCutoff_mass_defect line 7064
  299. theorem OAI.RegularPointCoordinates.norm_sub_normalized_cutoff_le line 7089
  300. def OAI.RegularPointCoordinates.SobolevSpace.radialProbabilityCutoff line 7114
  301. theorem OAI.RegularPointCoordinates.SobolevSpace.radialProbabilityCutoff_coe line 7119
  302. theorem OAI.RegularPointCoordinates.SobolevSpace.radialProbabilityCutoff_data line 7143
  303. def OAI.RegularPointCoordinates.inverseInitialDensityPlan line 7188
  304. theorem OAI.RegularPointCoordinates.inverseInitialDensityPlan_ac line 7192
  305. theorem OAI.RegularPointCoordinates.inverseInitialDensityPlan_initial line 7195
  306. theorem OAI.RegularPointCoordinates.inverseInitialDensityPlan_le line 7210
  307. theorem OAI.RegularPointCoordinates.inverseInitialDensityPlan_compression line 7220
  308. theorem OAI.RegularPointCoordinates.inverseInitialDensityPlan_finite line 7232
  309. theorem OAI.RegularPointCoordinates.inverseInitialDensityPlan_integral line 7239
  310. theorem OAI.RegularPointCoordinates.log_linear_remainder_nonneg line 7263
  311. theorem OAI.RegularPointCoordinates.log_linear_remainder_le line 7271
  312. theorem OAI.RegularPointCoordinates.log_linear_remainder_abs_le line 7279
  313. theorem OAI.RegularPointCoordinates.planInitialSecant_log_reweight_error line 7301
  314. theorem OAI.RegularPointCoordinates.planInitialSecant_log_reweight_tendsto line 7352
  315. theorem OAI.RegularPointCoordinates.memLp_log_of_lower line 7387
  316. theorem OAI.RegularPointCoordinates.reference_log_signed_variation line 7403
  317. theorem OAI.RegularPointCoordinates.reference_entropy_plan_bound line 7455
  318. def OAI.RegularPointCoordinates.compactPotentialLipschitz line 7522
  319. theorem OAI.RegularPointCoordinates.hopfLax_sub_const line 7525
  320. theorem OAI.RegularPointCoordinates.hopfLax_unit_uniform_lipschitz line 7538
  321. theorem OAI.RegularPointCoordinates.IsOptimalCoupling.normalized_compact_sobolev_potential line 7567
  322. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compact_energy_subgradient line 7633
  323. def OAI.RegularPointCoordinates.compactPotentialL2Bound line 7708
  324. theorem OAI.RegularPointCoordinates.compactPotentialL2Bound_nonneg line 7713
  325. theorem OAI.RegularPointCoordinates.normalized_potential_norm_le line 7718
  326. theorem OAI.RegularPointCoordinates.compact_dual_le_wasserstein line 7736
  327. theorem OAI.RegularPointCoordinates.heat_dual_secant line 7756
  328. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compact_heat_lower line 7795
  329. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compact_heat_probability line 7823
  330. def OAI.RegularPointCoordinates.heatEviRemainder line 7850
  331. theorem OAI.RegularPointCoordinates.heatEviRemainder_tendsto line 7854
  332. theorem OAI.RegularPointCoordinates.heatMeasure_le_const line 7866
  333. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compact_heat_EVI_secant line 7876
  334. theorem OAI.RegularPointCoordinates.heatGeneratorAt_hasDerivAt_split line 7937
  335. theorem OAI.RegularPointCoordinates.heatGeneratorAt_norm_sub_le line 7952
  336. theorem OAI.RegularPointCoordinates.heatEviRemainder_le line 7975
  337. theorem OAI.RegularPointCoordinates.heatSobolev_cutoff_norm_sq_le line 8021
  338. theorem OAI.RegularPointCoordinates.heatSobolev_cutoff_exponential_norm_sq_le line 8056
  339. theorem OAI.RegularPointCoordinates.heatSobolev_norm_uniform line 8113
  340. theorem OAI.RegularPointCoordinates.heat_radial_mass_defect_uniform line 8121
  341. theorem OAI.RegularPointCoordinates.heat_normalized_cutoff_exponential line 8142
  342. theorem OAI.RegularPointCoordinates.radial_probability_entropy_error line 8211
  343. theorem OAI.RegularPointCoordinates.heat_entropy_tail_uniform line 8316
  344. theorem OAI.RegularPointCoordinates.normalized_submeasure_wassersteinSq_le line 8410
  345. theorem OAI.RegularPointCoordinates.integral_realDensity line 8466
  346. theorem OAI.RegularPointCoordinates.bounded_density_potential_integral_tendsto line 8474
  347. theorem OAI.RegularPointCoordinates.normalized_submeasure_wassersteinSq_real_le line 8511
  348. theorem OAI.RegularPointCoordinates.radial_probability_measure_transport_le line 8541
  349. def OAI.RegularPointCoordinates.radialHeatMeasure line 8653
  350. theorem OAI.RegularPointCoordinates.heat_moment_tail_uniform line 8657
  351. theorem OAI.RegularPointCoordinates.radialHeatMeasure_entropy_exponential line 8673
  352. theorem OAI.RegularPointCoordinates.radialHeatMeasure_transport_exponential line 8717
  353. def OAI.RegularPointCoordinates.radialHeatSobolev line 8756
  354. theorem OAI.RegularPointCoordinates.radialHeatSobolev_measure line 8760
  355. theorem OAI.RegularPointCoordinates.radialHeatSobolev_data line 8774
  356. theorem OAI.RegularPointCoordinates.radialHeatMeasure_data line 8792
  357. theorem OAI.RegularPointCoordinates.finiteSecondMoment_of_ae_dist_le line 8822
  358. theorem OAI.RegularPointCoordinates.IsRelaxedSlope.quantitative_compact_bounded_recovery line 8844
  359. theorem OAI.RegularPointCoordinates.SobolevSpace.quantitative_strong_compact_bounded_recovery line 8937
  360. def OAI.RegularPointCoordinates.squareCoreRoot line 8976
  361. def OAI.RegularPointCoordinates.squareCoreContraction line 8977
  362. theorem OAI.RegularPointCoordinates.squareCoreRoot_lipschitz line 8979
  363. theorem OAI.RegularPointCoordinates.squareCoreRoot_zero line 8988
  364. theorem OAI.RegularPointCoordinates.squareCoreContraction_zero line 8990
  365. theorem OAI.RegularPointCoordinates.squareCoreRoot_nonneg line 8992
  366. theorem OAI.RegularPointCoordinates.squareCoreContraction_bounds line 8994
  367. theorem OAI.RegularPointCoordinates.squareCoreContraction_lipschitz line 9001
  368. theorem OAI.RegularPointCoordinates.squareCoreContraction_tendsto line 9031
  369. theorem OAI.RegularPointCoordinates.SobolevSpace.squareCoreContraction_tendsto line 9044
  370. theorem OAI.RegularPointCoordinates.SobolevSpace.quantitative_strong_square_core_recovery line 9095
  371. theorem OAI.RegularPointCoordinates.SobolevSpace.quantitative_strong_probability_square_recovery line 9171
  372. theorem OAI.RegularPointCoordinates.density_entropy_regularized_support line 9273
  373. theorem OAI.RegularPointCoordinates.integral_entropy_regularized_subgradient line 9286
  374. theorem OAI.RegularPointCoordinates.probability_entropy_regularized_subgradient line 9311
  375. theorem OAI.RegularPointCoordinates.entropy_regularized_subgradient_rep line 9339
  376. theorem OAI.RegularPointCoordinates.entropy_regularized_subgradient_localized line 9360
  377. theorem OAI.RegularPointCoordinates.planInitialSecant_log_reweight_error_path line 9395
  378. theorem OAI.RegularPointCoordinates.planInitialSecant_log_reweight_tendsto_path line 9440
  379. theorem OAI.RegularPointCoordinates.inverseInitialDensityPlan_le_path line 9462
  380. theorem OAI.RegularPointCoordinates.path_log_signed_variation line 9470
  381. theorem OAI.RegularPointCoordinates.planInitialSecant_log_reweight_error_at line 9523
  382. theorem OAI.RegularPointCoordinates.planInitialSecant_log_reweight_tendsto_eventual line 9570
  383. theorem OAI.RegularPointCoordinates.path_log_signed_variation_eventual line 9595
  384. theorem OAI.RegularPointCoordinates.abs_log_sub_le_div line 9646
  385. theorem OAI.RegularPointCoordinates.regularized_square_log_secant_bound line 9669
  386. theorem OAI.RegularPointCoordinates.inverseInitialDensityPlan_restrict_initial line 9723
  387. theorem OAI.RegularPointCoordinates.restrict_plan_compression line 9733
  388. theorem OAI.RegularPointCoordinates.lipschitz_geodesic_increment line 9739
  389. theorem OAI.RegularPointCoordinates.lipschitz_plan_increment_integrable line 9746
  390. theorem OAI.RegularPointCoordinates.lipschitz_plan_secant_restrict_error line 9757
  391. theorem OAI.RegularPointCoordinates.tendsto_integral_log_levels line 9782
  392. theorem OAI.RegularPointCoordinates.tendsto_integral_compl_log_levels line 9800
  393. theorem OAI.RegularPointCoordinates.log_level_path_bound line 9822
  394. theorem OAI.RegularPointCoordinates.log_core_restricted_signed_variation line 9847
  395. theorem OAI.RegularPointCoordinates.tendsto_of_uniform_secant_tails line 9905
  396. theorem OAI.RegularPointCoordinates.log_core_signed_variation line 9925
  397. theorem OAI.RegularPointCoordinates.log_core_entropy_subgradient line 9965
  398. theorem OAI.RegularPointCoordinates.inverseInitialDensityPlan_restrict line 10028
  399. def OAI.RegularPointCoordinates.pathLogControl line 10033
  400. theorem OAI.RegularPointCoordinates.pathLogControl_measurable line 10036
  401. theorem OAI.RegularPointCoordinates.pathLogControl_bound line 10042
  402. theorem OAI.RegularPointCoordinates.log_core_path_set_variation line 10047
  403. theorem OAI.RegularPointCoordinates.inverseInitialDensityPlan_initial_nonneg line 10134
  404. theorem OAI.RegularPointCoordinates.initial_density_pos line 10156
  405. theorem OAI.RegularPointCoordinates.initial_sqrt_inverse_integrable line 10165
  406. def OAI.RegularPointCoordinates.squareLogControl line 10187
  407. def OAI.RegularPointCoordinates.regularizedPlanLogSecant line 10189
  408. theorem OAI.RegularPointCoordinates.regularized_log_path_bound line 10193
  409. theorem OAI.RegularPointCoordinates.regularized_log_integrable_secant line 10213
  410. theorem OAI.RegularPointCoordinates.regularized_log_secant_restrict_error line 10229
  411. theorem OAI.RegularPointCoordinates.integrable_log_of_lower line 10260
  412. theorem OAI.RegularPointCoordinates.planInitialSecant_log_regularization_error_at line 10276
  413. theorem OAI.RegularPointCoordinates.sqrt_core_local_variation line 10337
  414. theorem OAI.RegularPointCoordinates.sqrt_core_signed_variation line 10411
  415. theorem OAI.RegularPointCoordinates.entropy_regularized_plan_secant line 10507
  416. theorem OAI.RegularPointCoordinates.entropy_regularized_plan_derivative_le line 10554
  417. def OAI.RegularPointCoordinates.setRetraction line 10602
  418. theorem OAI.RegularPointCoordinates.setRetraction_val_of_mem line 10607
  419. theorem OAI.RegularPointCoordinates.setRetraction_measurable line 10611
  420. theorem OAI.RegularPointCoordinates.map_setRetraction_val line 10617
  421. theorem OAI.RegularPointCoordinates.map_pair_setRetraction_val line 10626
  422. theorem OAI.RegularPointCoordinates.transportCost_subtype_map line 10642
  423. theorem OAI.RegularPointCoordinates.IsOptimalCoupling.retract_to_set line 10649
  424. theorem OAI.RegularPointCoordinates.clipped_distance_square_lipschitz line 10708
  425. theorem OAI.RegularPointCoordinates.truncated_squared_distance_eq_clip line 10728
  426. theorem OAI.RegularPointCoordinates.truncated_squared_distance_lipschitz line 10738
  427. def OAI.RegularPointCoordinates.truncatedCostTransform line 10751
  428. theorem OAI.RegularPointCoordinates.truncatedCostTransform_bdd line 10754
  429. theorem OAI.RegularPointCoordinates.truncatedCostTransform_le_cost line 10761
  430. theorem OAI.RegularPointCoordinates.truncatedCostTransform_le line 10766
  431. theorem OAI.RegularPointCoordinates.le_truncatedCostTransform line 10771
  432. theorem OAI.RegularPointCoordinates.truncatedCostTransform_lipschitz line 10778
  433. theorem OAI.RegularPointCoordinates.truncatedCostTransform_eq_const_outside line 10807
  434. theorem OAI.RegularPointCoordinates.hopfRadius_zero_outside line 10835
  435. theorem OAI.RegularPointCoordinates.hopfLeftRadius_zero_outside line 10850
  436. theorem OAI.RegularPointCoordinates.hopfScaledRadius_zero_outside line 10860
  437. theorem OAI.RegularPointCoordinates.hopfLeftLax_zero_outside line 10867
  438. theorem OAI.RegularPointCoordinates.hopfScaledRadius_bounds_proper line 10888
  439. theorem OAI.RegularPointCoordinates.hopfLeftRadius_memLp_proper line 10897
  440. theorem OAI.RegularPointCoordinates.hopfScaledRadius_memLp_proper line 10909
  441. theorem OAI.RegularPointCoordinates.hopfScaledRadius_toLp_tendsto_proper line 10922
  442. theorem OAI.RegularPointCoordinates.hopfLeft_toLp_tendsto_proper line 10948
  443. theorem OAI.RegularPointCoordinates.hopfLeftRadius_isRelaxed_proper line 10987
  444. theorem OAI.RegularPointCoordinates.hopfLeftRadius_minimalSlope_bound_proper line 11019
  445. theorem OAI.RegularPointCoordinates.IsOptimalCoupling.bounded_sobolev_potential line 11054
  446. theorem OAI.RegularPointCoordinates.sqrt_core_entropy_subgradient line 11182
  447. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.sqrt_core_energy_subgradient line 11224
  448. theorem OAI.RegularPointCoordinates.IsOptimalCoupling.uniform_compact_potentials line 11303
  449. theorem OAI.RegularPointCoordinates.IsOptimalCoupling.linear_radius_bounded_sobolev_potential line 11371
  450. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.linear_radius_sqrt_core_energy_subgradient line 11558
  451. theorem OAI.RegularPointCoordinates.optimal_plan_cost_real line 11642
  452. theorem OAI.RegularPointCoordinates.optimal_plan_dual_le line 11649
  453. theorem OAI.RegularPointCoordinates.optimal_plan_dual_eq line 11668
  454. theorem OAI.RegularPointCoordinates.IsOptimalCoupling.uniform_bounded_sobolev_potential line 11700
  455. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.uniform_sqrt_core_energy_subgradient line 11887
  456. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.bounded_density_dual_limit line 11962
  457. theorem OAI.RegularPointCoordinates.common_support_lipschitz_subsequence line 12061
  458. theorem OAI.RegularPointCoordinates.SobolevSpace.resolvent_dense_approx line 12115
  459. theorem OAI.RegularPointCoordinates.SobolevSpace.inner_tendsto_of_toLp_tendsto_bounded line 12130
  460. theorem OAI.RegularPointCoordinates.SobolevSpace.energyForm_tendsto_of_toLp_tendsto_bounded line 12179
  461. theorem OAI.RegularPointCoordinates.SobolevSpace.energyForm_tendsto_weak_strong line 12188
  462. theorem OAI.RegularPointCoordinates.SobolevSpace.eq_of_lipschitz_rep line 12218
  463. theorem OAI.RegularPointCoordinates.SobolevSpace.norm_le_of_common_support line 12226
  464. theorem OAI.RegularPointCoordinates.SobolevSpace.toLp_tendsto_of_common_support line 12263
  465. theorem OAI.RegularPointCoordinates.SobolevSpace.common_support_dual_subsequence line 12312
  466. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.quantitative_H1_energy_subgradient line 12357
  467. theorem OAI.RegularPointCoordinates.FullCD.compact_dual_le line 12488
  468. theorem OAI.RegularPointCoordinates.energyForm_abs_le_norm line 12505
  469. theorem OAI.RegularPointCoordinates.heat_cutoff_dual_secant line 12517
  470. theorem OAI.RegularPointCoordinates.SobolevSpace.linearRadiusPotential_norm_le line 12601
  471. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.cutoff_heat_secant line 12669
  472. theorem OAI.RegularPointCoordinates.metricAC_uniformContinuousOn line 12740
  473. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compact_heat_entropy_continuousAt line 12758
  474. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compact_heat_probability_continuousAt line 12776
  475. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compact_heat_wassersteinSq_continuousAt line 12794
  476. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_entropy_continuousAt line 12838
  477. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_probability_continuousAt line 12857
  478. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_wassersteinSq_continuousAt line 12874
  479. theorem OAI.RegularPointCoordinates.sq_dist_difference_le line 12909
  480. theorem OAI.RegularPointCoordinates.sq_dist_difference_exponential line 12918
  481. theorem OAI.RegularPointCoordinates.ACWassersteinProbability.dist_sq line 12941
  482. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.radial_heat_cost_exponential line 12961
  483. theorem OAI.RegularPointCoordinates.integral_bound_of_right_secants line 13022
  484. theorem OAI.RegularPointCoordinates.integral_bound_of_frequent_right_slopes line 13065
  485. theorem OAI.RegularPointCoordinates.exp_neg_mul_tendsto_zero line 13087
  486. theorem OAI.RegularPointCoordinates.frequent_right_slope_of_exponential_secants line 13091
  487. theorem OAI.RegularPointCoordinates.cutoff_secant_transfer line 13112
  488. theorem OAI.RegularPointCoordinates.diagonal_polynomial_exponential_error line 13128
  489. theorem OAI.RegularPointCoordinates.frequent_slope_of_expanding_cutoffs line 13164
  490. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.bounded_heat_frequent_EVI_slope line 13194
  491. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.bounded_heat_EVI line 13275
  492. theorem OAI.RegularPointCoordinates.integrated_evi_error_transfer line 13334
  493. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_competitor_cutoff_cost line 13370
  494. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_competitor_EVI line 13441
  495. theorem OAI.RegularPointCoordinates.two_flow_evi_frequent_slope line 13536
  496. theorem OAI.RegularPointCoordinates.two_flow_evi_contraction line 13598
  497. theorem OAI.RegularPointCoordinates.wassersteinSq_symm line 13631
  498. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_two_cost_continuousAt line 13636
  499. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_wasserstein_contraction_positive line 13671
  500. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_wasserstein_contraction line 13713
  501. def OAI.RegularPointCoordinates.uniformDensityLp line 13776
  502. theorem OAI.RegularPointCoordinates.uniformDensityLp_ae line 13781
  503. theorem OAI.RegularPointCoordinates.uniformDensityLp_nonneg line 13791
  504. theorem OAI.RegularPointCoordinates.uniformDensityLp_bound line 13799
  505. theorem OAI.RegularPointCoordinates.uniformDensityLp_integral line 13807
  506. theorem OAI.RegularPointCoordinates.uniformDensityLp_heat_zero line 13816
  507. theorem OAI.RegularPointCoordinates.heat_uniformDensityLp_pair line 13831
  508. theorem OAI.RegularPointCoordinates.square_integral_le_integral_square line 13855
  509. theorem OAI.RegularPointCoordinates.transportCost_real_integral line 13883
  510. theorem OAI.RegularPointCoordinates.optimal_transport_lipschitz_mean line 13897
  511. theorem OAI.RegularPointCoordinates.wassersteinSq_ball_bound line 13949
  512. theorem OAI.RegularPointCoordinates.exists_lipschitz_of_average_bound line 13993
  513. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_lipschitz line 14036
  514. theorem OAI.RegularPointCoordinates.optimal_transport_quadratic_dual line 14130
  515. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_average_quadratic_dual line 14178
  516. theorem OAI.RegularPointCoordinates.quadratic_comparison_of_average_bound line 14266
  517. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.openPos line 14324
  518. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_pointwise_quadratic_dual line 14331
  519. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_hopfLax_comparison line 14357
  520. theorem OAI.RegularPointCoordinates.slopeAtScale_real_bound line 14417
  521. theorem OAI.RegularPointCoordinates.hopfLax_gap_le_scale line 14430
  522. theorem OAI.RegularPointCoordinates.slopeAtScale_zero_outside line 14443
  523. theorem OAI.RegularPointCoordinates.memLp_of_bounded_ball_support line 14472
  524. theorem OAI.RegularPointCoordinates.compact_lipschitz_abs_bound line 14483
  525. theorem OAI.RegularPointCoordinates.compact_lipschitz_memLp line 14496
  526. theorem OAI.RegularPointCoordinates.hopfLax_compact_memLp line 14502
  527. theorem OAI.RegularPointCoordinates.slopeAtScale_sq_memLp line 14509
  528. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_slope_quadratic_bound line 14536
  529. theorem OAI.RegularPointCoordinates.quadratic_bound_of_rat line 14609
  530. theorem OAI.RegularPointCoordinates.localSlope_sq_le_of_quadratic_bound line 14625
  531. theorem OAI.RegularPointCoordinates.slopeAtScale_neg_eq line 14680
  532. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_scaled_gradient_bound line 14684
  533. theorem OAI.RegularPointCoordinates.slopeAtScale_toReal_tendsto line 14760
  534. theorem OAI.RegularPointCoordinates.localSlope_zero_outside_one line 14774
  535. theorem OAI.RegularPointCoordinates.localSlope_sq_compact_memLp line 14785
  536. theorem OAI.RegularPointCoordinates.slopeSq_toLp_tendsto line 14799
  537. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_local_gradient_bound line 14854
  538. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_lipschitz_gradient_compact line 14893
  539. theorem OAI.RegularPointCoordinates.lp_weighted_square_continuous line 14928
  540. theorem OAI.RegularPointCoordinates.SobolevSpace.minimalSlope_lipschitz line 14946
  541. theorem OAI.RegularPointCoordinates.SobolevSpace.minimalSlope_le_localSlope line 14958
  542. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_compact_weighted_gradient line 14988
  543. theorem OAI.RegularPointCoordinates.IsSlopeMajorant.compact_approximation line 15079
  544. theorem OAI.RegularPointCoordinates.IsRelaxedSlope.compact_recovery line 15154
  545. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_weighted_gradient line 15185
  546. def OAI.RegularPointCoordinates.weightedGamma line 15233
  547. theorem OAI.RegularPointCoordinates.weightedGamma_comm line 15237
  548. theorem OAI.RegularPointCoordinates.weightedGamma_self line 15244
  549. theorem OAI.RegularPointCoordinates.weightedGamma_add_left line 15254
  550. theorem OAI.RegularPointCoordinates.weightedGamma_smul_left line 15263
  551. theorem OAI.RegularPointCoordinates.SobolevSpace.minimalSlope_norm_le line 15273
  552. theorem OAI.RegularPointCoordinates.weightedGamma_norm_le line 15282
  553. def OAI.RegularPointCoordinates.weightedGammaCLM line 15308
  554. theorem OAI.RegularPointCoordinates.weighted_gradient_hasDerivAt line 15321
  555. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_weak_bochner line 15345
  556. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_compact_slope_bdd line 15449
  557. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_compact_gamma_memLp line 15492
  558. theorem OAI.RegularPointCoordinates.heatTail_weak_laplacian line 15524
  559. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_compact_weak_bochner line 15534
  560. theorem OAI.RegularPointCoordinates.weakLaplacian_resolvent_core line 15581
  561. theorem OAI.RegularPointCoordinates.heat_weakLaplacian_hasDerivAt line 15591
  562. theorem OAI.RegularPointCoordinates.abs_at_zero_of_exp_deriv_bound line 15610
  563. theorem OAI.RegularPointCoordinates.resolvent_pair_bound_of_heat line 15665
  564. theorem OAI.RegularPointCoordinates.average_lipschitz_center line 15736
  565. theorem OAI.RegularPointCoordinates.lipschitz_ball_average_bound line 15762
  566. theorem OAI.RegularPointCoordinates.uniformDensityLp_inner_average line 15783
  567. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.resolvent_lipschitz line 15801
  568. theorem OAI.RegularPointCoordinates.lipschitz_lp_pointwise_convergence line 15858
  569. theorem OAI.RegularPointCoordinates.lipschitz_pointwise_compact_convergence line 15905
  570. theorem OAI.RegularPointCoordinates.resolventLp_abs_bound line 15949
  571. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.boundedLaplacian_compact_approximation line 15964
  572. theorem OAI.RegularPointCoordinates.SobolevSpace.bounded_strong_recovery line 16036
  573. theorem OAI.RegularPointCoordinates.weakLaplacian_of_bounded_tests line 16083
  574. theorem OAI.RegularPointCoordinates.weakLaplacian_comp_C2 line 16095
  575. theorem OAI.RegularPointCoordinates.SobolevSpace.minimalSlope_le_lipschitz line 16184
  576. theorem OAI.RegularPointCoordinates.exists_boundedLaplacian_comp_C2 line 16236
  577. theorem OAI.RegularPointCoordinates.weakLaplacian_product_plateau line 16298
  578. theorem OAI.RegularPointCoordinates.exists_smooth_scalar_cutoff line 16344
  579. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.exists_boundedLaplacian_cutoff line 16399
  580. theorem OAI.RegularPointCoordinates.uniformDensityLp_norm_sq line 16503
  581. theorem OAI.RegularPointCoordinates.lipschitz_lp_pointwise_error line 16518
  582. def OAI.RegularPointCoordinates.cutoffVolumeFloor line 16557
  583. theorem OAI.RegularPointCoordinates.cutoffVolumeFloor_pos line 16560
  584. theorem OAI.RegularPointCoordinates.FullCD.cutoff_volume_comparison line 16563
  585. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.quantitative_radial_resolvent line 16592
  586. def OAI.RegularPointCoordinates.cutoffTimeFactor line 16679
  587. theorem OAI.RegularPointCoordinates.cutoffTimeFactor_pos line 16682
  588. theorem OAI.RegularPointCoordinates.cutoffVolumeFloor_uniform line 16685
  589. theorem OAI.RegularPointCoordinates.cutoffTimeFactor_admissible line 16705
  590. theorem OAI.RegularPointCoordinates.exists_uniform_boundedLaplacian_cutoff_constant line 16736