OAI/Analysis/AncientFlat/Kernel/ClassicalBase.lean

GitHub source file

517 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BiharmonicKernel.gaussian_moment_bound line 10
2. lemma OAI.BiharmonicKernel.polynomial_gaussian_bound line 37
3. def OAI.BiharmonicKernel.gaussian line 61
4. lemma OAI.BiharmonicKernel.norm_le_quadratic line 77
5. def OAI.BiharmonicKernel.multiplier line 87
6. lemma OAI.BiharmonicKernel.multiplier_apply line 93
7. def OAI.BiharmonicKernel.heatKernel line 103
8. lemma OAI.BiharmonicKernel.fourier_heatKernel line 106
9. lemma OAI.BiharmonicKernel.integral_heatKernel line 110
10. lemma OAI.BiharmonicKernel.heatKernel_decay line 115
11. lemma OAI.BiharmonicKernel.heatKernel_invariant line 126
12. lemma OAI.BiharmonicKernel.fourierInv_comp_smul line 139
13. lemma OAI.BiharmonicKernel.heatKernel_scaling line 149
14. lemma OAI.BiharmonicKernel.heatKernel_deriv_scaling line 161
15. lemma OAI.BiharmonicKernel.heatKernel_scaled_decay line 174
16. def OAI.BiharmonicKernel.symbol line 189
17. lemma OAI.BiharmonicKernel.symbol_nonneg line 192
18. lemma OAI.BiharmonicKernel.symbol_temperate line 195
19. def OAI.BiharmonicKernel.kernel line 203
20. lemma OAI.BiharmonicKernel.heatKernel_eq_kernel line 206
21. lemma OAI.BiharmonicKernel.kernel_hasDerivAt line 215
22. lemma OAI.BiharmonicKernel.biharmonic_eq_fourierMultiplier line 273
23. lemma OAI.BiharmonicKernel.kernel_heat_equation line 288
24. lemma OAI.BiharmonicKernel.kernel_eq_scaled line 306
25. lemma OAI.BiharmonicKernel.kernel_contDiffAt line 319
26. lemma OAI.BiharmonicKernel.integral_norm_heatKernel line 334
27. def OAI.C0Convolution.translate line 357
28. lemma OAI.C0Convolution.translate_apply line 360
29. lemma OAI.C0Convolution.translate_zero line 363
30. lemma OAI.C0Convolution.translate_add line 367
31. lemma OAI.C0Convolution.translate_smul line 370
32. lemma OAI.C0Convolution.norm_le_iff line 373
33. lemma OAI.C0Convolution.apply_norm_le line 377
34. lemma OAI.C0Convolution.norm_translate line 380
35. lemma OAI.C0Convolution.continuous_translate line 387
36. def OAI.C0Convolution.eval line 402
37. lemma OAI.C0Convolution.eval_apply line 409
38. lemma OAI.C0Convolution.integrable_translated line 413
39. def OAI.C0Convolution.convolve line 420
40. lemma OAI.C0Convolution.convolve_apply line 423
41. lemma OAI.C0Convolution.norm_convolve_le line 429
42. lemma OAI.C0Convolution.convolve_add line 435
43. lemma OAI.C0Convolution.convolve_smul line 445
44. def OAI.C0Convolution.convolveCLM line 449
45. lemma OAI.C0Convolution.norm_convolveCLM_le line 456
46. lemma OAI.C0Convolution.integrable_scaled_translated line 462
47. def OAI.C0Convolution.scaleConvolve line 471
48. lemma OAI.C0Convolution.continuous_scaleConvolve line 474
49. lemma OAI.C0Convolution.scaleConvolve_zero line 488
50. lemma OAI.C0Convolution.scaleConvolve_tendsto line 492
51. lemma OAI.C0Convolution.convolve_scaled line 501
52. lemma OAI.C0Convolution.convolve_coe line 521
53. lemma OAI.C0Convolution.convolve_assoc line 526
54. lemma OAI.BiharmonicKernel.heatKernel_semigroup line 556
55. def OAI.BiharmonicKernel.evolution line 569
56. lemma OAI.BiharmonicKernel.evolution_zero line 573
57. lemma OAI.BiharmonicKernel.evolution_continuous line 577
58. lemma OAI.BiharmonicKernel.evolution_initial_trace line 582
59. lemma OAI.BiharmonicKernel.evolution_eq_convolve line 586
60. lemma OAI.BiharmonicKernel.evolution_apply line 597
61. lemma OAI.BiharmonicKernel.evolution_norm_le line 602
62. lemma OAI.BiharmonicKernel.evolution_semigroup line 609
63. lemma OAI.SchwartzConvolution.shifted_majorant line 637
64. lemma OAI.SchwartzConvolution.integrable_integrand line 664
65. lemma OAI.SchwartzConvolution.hasFDerivAt_convolution line 674
66. lemma OAI.SchwartzConvolution.contDiff_convolution_nat line 700
67. lemma OAI.SchwartzConvolution.contDiff_convolution line 712
68. lemma OAI.SchwartzConvolution.fderiv_convolution line 717
69. lemma OAI.SchwartzConvolution.fderiv_convolution_apply line 723
70. lemma OAI.SchwartzConvolution.second_fderiv_convolution_apply line 731
71. lemma OAI.SchwartzConvolution.laplacian_convolution line 753
72. lemma OAI.SchwartzConvolution.scaled_majorant line 784
73. lemma OAI.LaplacianScaling.laplacian_scaled line 830
74. lemma OAI.BiharmonicKernel.laplacian_kernel_scaling line 848
75. lemma OAI.BiharmonicKernel.biharmonic_kernel_scaling line 861
76. lemma OAI.BiharmonicKernel.evolution_coe_convolution line 877
77. lemma OAI.BiharmonicKernel.evolution_smooth line 887
78. lemma OAI.BiharmonicKernel.evolution_biharmonic line 892
79. lemma OAI.BiharmonicKernel.kernel_deriv_majorant line 898
80. lemma OAI.BiharmonicKernel.evolution_hasDerivAt line 922
81. lemma OAI.BiharmonicKernel.evolution_heat_equation line 979
82. lemma OAI.BiharmonicKernel.kernel_majorant line 1004
83. lemma OAI.BiharmonicKernel.continuous_kernel_comp line 1015
84. def OAI.FrozenParametrix.value line 1032
85. lemma OAI.FrozenParametrix.integrable_value line 1035
86. lemma OAI.FrozenParametrix.continuous_value line 1048
87. lemma OAI.FrozenParametrix.zero_at_infty_value line 1067
88. def OAI.FrozenParametrix.frozen line 1095
89. def OAI.C0Multiplier.mul line 1111
90. lemma OAI.C0Multiplier.mul_apply line 1121
91. lemma OAI.C0Multiplier.norm_mul_le line 1124
92. def OAI.C0Multiplier.mulCLM line 1133
93. lemma OAI.C0Multiplier.continuous_mul line 1143
94. lemma OAI.C0Convolution.translate_sub line 1152
95. lemma OAI.C0Convolution.continuous_translate_comp line 1155
96. def OAI.FrozenParametrix.kernelFamily line 1177
97. lemma OAI.FrozenParametrix.continuous_kernelFamily line 1182
98. def OAI.FrozenParametrix.sourceMultiplier line 1189
99. lemma OAI.FrozenParametrix.continuous_sourceMultiplier line 1194
100. def OAI.FrozenParametrix.sourceData line 1202
101. lemma OAI.FrozenParametrix.continuous_sourceData line 1206
102. lemma OAI.FrozenParametrix.sourceData_apply line 1211
103. lemma OAI.FrozenParametrix.sourceData_norm_le line 1215
104. lemma OAI.FrozenParametrix.integrable_translated_sourceData line 1226
105. lemma OAI.FrozenParametrix.frozen_eq_integral line 1238
106. lemma OAI.FrozenParametrix.continuous_frozen line 1248
107. lemma OAI.FrozenParametrix.frozen_zero line 1265
108. lemma OAI.FrozenParametrix.frozen_tendsto_identity line 1273
109. lemma OAI.FrozenParametrix.norm_frozen_le line 1279
110. lemma OAI.FrozenParametrix.frozen_add line 1289
111. lemma OAI.FrozenParametrix.frozen_smul line 1301
112. lemma OAI.FrozenParametrix.exists_uniform_norm_bound line 1309
113. lemma OAI.FrozenParametrix.frozen_apply_unscaled line 1319
114. lemma OAI.SchwartzConvolution.scaled_weighted_majorant line 1353
115. def OAI.BiharmonicKernel.bilapKernel line 1414
116. lemma OAI.BiharmonicKernel.bilapKernel_eq_schwartz line 1416
117. lemma OAI.BiharmonicKernel.bilapKernel_eq_scaled line 1425
118. lemma OAI.BiharmonicKernel.bilapKernel_contDiffAt line 1441
119. lemma OAI.BiharmonicKernel.continuous_bilapKernel_comp line 1456
120. lemma OAI.BiharmonicKernel.bilapKernel_weighted_majorant line 1465
121. def OAI.C0Multiplier.mulLeftCLM line 1482
122. lemma OAI.C0Multiplier.continuous_mul_left line 1489
123. def OAI.FrozenFamily.family line 1498
124. lemma OAI.FrozenFamily.continuous_family line 1502
125. def OAI.FrozenFamily.multiplier line 1506
126. lemma OAI.FrozenFamily.continuous_multiplier line 1509
127. def OAI.FrozenFamily.data line 1514
128. lemma OAI.FrozenFamily.data_apply line 1517
129. lemma OAI.FrozenFamily.continuous_data line 1520
130. lemma OAI.FrozenFamily.norm_data_le line 1524
131. def OAI.FrozenFamily.residualData line 1534
132. lemma OAI.FrozenFamily.residualData_apply line 1539
133. lemma OAI.FrozenFamily.continuous_residualData line 1547
134. lemma OAI.FrozenFamily.norm_residualData_le line 1555
135. lemma OAI.FrozenFamily.integrable_residualData line 1572
136. def OAI.FrozenFamily.residual line 1591
137. lemma OAI.FrozenFamily.residual_apply line 1595
138. lemma OAI.FrozenFamily.norm_residual_le line 1605
139. lemma OAI.BiharmonicKernel.bilapKernel_scaling line 1638
140. def OAI.FrozenParametrix.bilapFamily line 1651
141. def OAI.FrozenParametrix.coefficient line 1657
142. lemma OAI.FrozenParametrix.coefficient_apply line 1662
143. def OAI.FrozenParametrix.principalResidual line 1665
144. lemma OAI.FrozenParametrix.principalResidual_apply_scaled line 1670
145. lemma OAI.FrozenParametrix.principalResidual_apply_unscaled line 1683
146. lemma OAI.FrozenParametrix.norm_principalResidual_le line 1708
147. lemma OAI.FrozenParametrix.exists_uniform_principalResidual_bound line 1725
148. def OAI.CompactComposition.compose line 1761
149. lemma OAI.CompactComposition.compose_apply line 1764
150. lemma OAI.CompactComposition.continuous_compose line 1767
151. lemma OAI.C0Multiplier.continuous_mul_joint line 1791
152. lemma OAI.FrozenFamily.continuous_multiplier_comp line 1804
153. lemma OAI.FrozenFamily.continuous_data_comp line 1812
154. lemma OAI.FrozenFamily.continuous_residualData_comp line 1818
155. lemma OAI.FrozenFamily.norm_residualData_le_uniform line 1834
156. lemma OAI.FrozenFamily.continuous_residual_comp line 1848
157. lemma OAI.FrozenFamily.residual_add line 1863
158. lemma OAI.FrozenFamily.residual_smul line 1879
159. lemma OAI.FrozenFamily.norm_residual_le_uniform line 1891
160. def OAI.FrozenFamily.residualCLM line 1901
161. def OAI.FrozenParametrix.frozenOp line 1919
162. lemma OAI.FrozenParametrix.kernel_majorant_nonneg line 1923
163. def OAI.FrozenParametrix.kernelMajorant line 1930
164. lemma OAI.FrozenParametrix.kernelMajorant_spec line 1932
165. def OAI.FrozenParametrix.frozenCLM line 1938
166. lemma OAI.FrozenParametrix.frozenCLM_apply line 1947
167. lemma OAI.FrozenParametrix.norm_frozenCLM_le line 1950
168. def OAI.FrozenParametrix.kernelFamilyCM line 1958
169. lemma OAI.FrozenParametrix.continuous_frozenOp_comp line 1964
170. lemma OAI.FrozenParametrix.continuous_coefficient_comp line 1986
171. lemma OAI.FrozenParametrix.norm_coefficient_le line 1992
172. def OAI.FrozenParametrix.bilapMajorant line 2001
173. lemma OAI.FrozenParametrix.bilapMajorant_spec line 2003
174. def OAI.FrozenParametrix.principalCLM line 2010
175. lemma OAI.FrozenParametrix.principalCLM_apply line 2016
176. lemma OAI.FrozenParametrix.continuous_principalCLM_apply line 2019
177. def OAI.FrozenParametrix.fullResidualCLM line 2035
178. lemma OAI.FrozenParametrix.fullResidualCLM_apply line 2039
179. lemma OAI.FrozenParametrix.continuous_fullResidualCLM_apply line 2043
180. lemma OAI.FrozenParametrix.exists_uniform_fullResidual_bound line 2052
181. abbrev OAI.StrongWeightedVolterra.UnitTime line 2084
182. abbrev OAI.StrongWeightedVolterra.Time line 2085
183. instance OAI.StrongWeightedVolterra.(instance at line 2087) line 2087
184. def OAI.StrongWeightedVolterra.weight line 2089
185. lemma OAI.StrongWeightedVolterra.weight_nonneg line 2091
186. lemma OAI.StrongWeightedVolterra.continuous_weight line 2094
187. lemma OAI.StrongWeightedVolterra.integrable_weight line 2100
188. def OAI.StrongWeightedVolterra.lag line 2121
189. lemma OAI.StrongWeightedVolterra.continuous_lag line 2125
190. structure OAI.StrongWeightedVolterra.Kernel line 2129
191. instance OAI.StrongWeightedVolterra.(instance at line 2133) line 2133
192. lemma OAI.StrongWeightedVolterra.continuous_apply_of_strong line 2135
193. def OAI.StrongWeightedVolterra.Kernel.ofStrong line 2152
194. def OAI.StrongWeightedVolterra.data line 2160
195. lemma OAI.StrongWeightedVolterra.continuous_data line 2163
196. lemma OAI.StrongWeightedVolterra.norm_data_le line 2170
197. lemma OAI.StrongWeightedVolterra.integrable_data line 2177
198. lemma OAI.StrongWeightedVolterra.continuous_integral_data line 2182
199. lemma OAI.StrongWeightedVolterra.norm_integral_data_le line 2191
200. def OAI.StrongWeightedVolterra.value line 2200
201. lemma OAI.StrongWeightedVolterra.continuous_value line 2203
202. lemma OAI.StrongWeightedVolterra.norm_value_le line 2207
203. def OAI.StrongWeightedVolterra.operator line 2217
204. lemma OAI.StrongWeightedVolterra.operator_apply line 2225
205. lemma OAI.StrongWeightedVolterra.norm_operator_le line 2228
206. lemma OAI.StrongWeightedVolterra.operator_add line 2235
207. lemma OAI.StrongWeightedVolterra.operator_smul line 2244
208. def OAI.StrongWeightedVolterra.operatorCLM line 2254
209. lemma OAI.StrongWeightedVolterra.norm_operatorCLM_le line 2262
210. theorem OAI.StrongWeightedVolterra.exists_unique_solution line 2268
211. lemma OAI.StrongWeightedVolterra.norm_solution_le line 2290
212. def OAI.StrongWeightedVolterra.unweighted line 2304
213. lemma OAI.StrongWeightedVolterra.unweighted_lag line 2308
214. def OAI.StrongWeightedVolterra.normalizedArg line 2315
215. def OAI.StrongWeightedVolterra.kernel line 2320
216. lemma OAI.StrongWeightedVolterra.normalizedArg_lag line 2325
217. lemma OAI.StrongWeightedVolterra.kernel_lag line 2332
218. lemma OAI.StrongWeightedVolterra.rescaling_scalar line 2341
219. lemma OAI.StrongWeightedVolterra.value_eq_volterra line 2357
220. lemma OAI.StrongWeightedVolterra.unweighted_at_time line 2380
221. lemma OAI.StrongWeightedVolterra.kernel_unweighted_lag line 2385
222. lemma OAI.StrongWeightedVolterra.intervalIntegrable_kernel_unweighted line 2395
223. lemma OAI.StrongWeightedVolterra.unweighted_solves line 2408
224. theorem OAI.StrongWeightedVolterra.exists_unweighted_solution line 2422
225. def OAI.ParabolicRadius.radius line 2446
226. lemma OAI.ParabolicRadius.pos line 2448
227. lemma OAI.ParabolicRadius.nonneg line 2449
228. lemma OAI.ParabolicRadius.pow_four line 2450
229. lemma OAI.ParabolicRadius.pow_three line 2453
230. lemma OAI.ParabolicRadius.inv_pow_three line 2456
231. lemma OAI.ParabolicRadius.le_one line 2460
232. lemma OAI.ParabolicRadius.continuous_comp line 2462
233. lemma OAI.ParabolicRadius.normalized_cancel line 2465
234. abbrev OAI.ParametrixVolterra.Slab line 2480
235. def OAI.ParametrixVolterra.now line 2482
236. def OAI.ParametrixVolterra.before line 2483
237. def OAI.ParametrixVolterra.elapsed line 2484
238. lemma OAI.ParametrixVolterra.continuous_now line 2486
239. lemma OAI.ParametrixVolterra.continuous_before line 2487
240. lemma OAI.ParametrixVolterra.continuous_elapsed line 2489
241. lemma OAI.ParametrixVolterra.elapsed_pos line 2492
242. lemma OAI.ParametrixVolterra.elapsed_le line 2494
243. lemma OAI.ParametrixVolterra.elapsed_eq_sub line 2497
244. def OAI.ParametrixVolterra.actualResidual line 2503
245. def OAI.ParametrixVolterra.normalized line 2507
246. lemma OAI.ParametrixVolterra.continuous_actualResidual_before line 2510
247. lemma OAI.ParametrixVolterra.continuous_normalized_apply line 2523
248. lemma OAI.ParametrixVolterra.exists_normalized_bound line 2529
249. theorem OAI.ParametrixVolterra.exists_correction line 2557
250. lemma OAI.ParametrixVolterra.exists_actualResidual_bound line 2576
251. def OAI.ParametrixVolterra.initial line 2595
252. lemma OAI.ParametrixVolterra.continuous_initialResidual line 2597
253. def OAI.ParametrixVolterra.sourceRHS line 2608
254. lemma OAI.ParametrixVolterra.continuous_sourceRHS line 2611
255. lemma OAI.ParametrixVolterra.norm_sourceRHS_le line 2616
256. def OAI.ParametrixVolterra.weightedSource line 2635
257. lemma OAI.ParametrixVolterra.unweighted_weightedSource line 2646
258. def OAI.ParametrixVolterra.residualKernel line 2657
259. lemma OAI.ParametrixVolterra.elapsed_normalizedArg line 2660
260. lemma OAI.ParametrixVolterra.before_normalizedArg line 2665
261. lemma OAI.ParametrixVolterra.kernel_eq_residualKernel line 2673
262. theorem OAI.ParametrixVolterra.exists_parametrix_correction line 2699
263. def OAI.MildVolterra.massWeight line 2743
264. lemma OAI.MildVolterra.massWeight_nonneg line 2744
265. lemma OAI.MildVolterra.continuous_massWeight line 2745
266. lemma OAI.MildVolterra.integrable_massWeight line 2747
267. def OAI.MildVolterra.data line 2756
268. lemma OAI.MildVolterra.continuous_data line 2759
269. lemma OAI.MildVolterra.norm_data_le line 2765
270. lemma OAI.MildVolterra.integrable_data line 2772
271. lemma OAI.MildVolterra.continuous_integral_data line 2777
272. lemma OAI.MildVolterra.norm_integral_data_le line 2786
273. def OAI.MildVolterra.value line 2795
274. lemma OAI.MildVolterra.continuous_value line 2798
275. lemma OAI.MildVolterra.norm_value_le line 2802
276. lemma OAI.MildVolterra.tendsto_value_zero line 2808
277. def OAI.MildVolterra.rawKernel line 2818
278. lemma OAI.MildVolterra.rawKernel_lag line 2822
279. lemma OAI.MildVolterra.rescaling_scalar line 2829
280. lemma OAI.MildVolterra.value_eq_integral line 2840
281. lemma OAI.MildVolterra.rawKernel_unweighted_lag line 2859
282. lemma OAI.MildVolterra.intervalIntegrable_rawKernel_unweighted line 2866
283. def OAI.ParametrixVolterra.actualFrozen line 2889
284. lemma OAI.ParametrixVolterra.continuous_actualFrozen_before line 2892
285. def OAI.ParametrixVolterra.frozenBound line 2900
286. lemma OAI.ParametrixVolterra.frozenBound_nonneg line 2901
287. lemma OAI.ParametrixVolterra.norm_actualFrozen_le line 2904
288. def OAI.ParametrixVolterra.mildKernel line 2908
289. lemma OAI.ParametrixVolterra.norm_mildKernel_le line 2913
290. lemma OAI.ParametrixVolterra.continuous_frozen_initial line 2917
291. lemma OAI.ParametrixVolterra.tendsto_frozen_initial line 2926
292. def OAI.ParametrixVolterra.mild line 2944
293. lemma OAI.ParametrixVolterra.continuous_mild line 2947
294. lemma OAI.ParametrixVolterra.tendsto_mild_initial line 2953
295. def OAI.ParametrixVolterra.frozenRaw line 2961
296. lemma OAI.ParametrixVolterra.rawKernel_eq_frozenRaw line 2964
297. lemma OAI.ParametrixVolterra.intervalIntegrable_frozenRaw line 2973
298. lemma OAI.ParametrixVolterra.mild_eq_integral line 2979
299. lemma OAI.ScaledSchwartzConvolution.scaled_decay line 3000
300. lemma OAI.ScaledSchwartzConvolution.shifted_majorant line 3031
301. def OAI.ScaledSchwartzConvolution.value line 3055
302. lemma OAI.ScaledSchwartzConvolution.integrable_integrand line 3059
303. lemma OAI.ScaledSchwartzConvolution.hasFDerivAt_value line 3072
304. lemma OAI.ScaledSchwartzConvolution.contDiff_value_nat line 3102
305. lemma OAI.ScaledSchwartzConvolution.contDiff_value line 3113
306. lemma OAI.ScaledSchwartzConvolution.fderiv_value line 3117
307. lemma OAI.ScaledSchwartzConvolution.fderiv_value_apply line 3123
308. lemma OAI.ScaledSchwartzConvolution.second_fderiv_value_apply line 3132
309. lemma OAI.ScaledSchwartzConvolution.laplacian_value line 3156
310. lemma OAI.ScaledSchwartzConvolution.bilaplacian_value line 3176
311. def OAI.FrozenParametrix.sourceScale line 3190
312. lemma OAI.FrozenParametrix.continuous_sourceScale line 3194
313. lemma OAI.FrozenParametrix.sourceScale_bounds line 3199
314. def OAI.FrozenParametrix.timeValue line 3204
315. lemma OAI.FrozenParametrix.timeValue_eq_scaled line 3207
316. lemma OAI.FrozenParametrix.timeValue_eq_frozenOp line 3218
317. lemma OAI.FrozenParametrix.contDiff_timeValue line 3228
318. lemma OAI.FrozenParametrix.bilaplacian_timeValue line 3237
319. lemma OAI.FrozenParametrix.integrable_timeValue_integrand line 3250
320. lemma OAI.FrozenParametrix.integrable_bilapValue_integrand line 3264
321. lemma OAI.BiharmonicKernel.bilapKernel_shifted_majorant line 3281
322. lemma OAI.BiharmonicKernel.hasDerivAt_kernel_bilap line 3293
323. lemma OAI.FrozenParametrix.hasDerivAt_timeValue line 3307
324. lemma OAI.FrozenParametrix.frozen_pde_residual line 3354
325. lemma OAI.KernelPairing.integrable_prod_of_translation_bound line 3388
326. lemma OAI.KernelPairing.integrable_pair line 3410
327. lemma OAI.KernelPairing.norm_pair_le line 3418
328. def OAI.KernelPairing.pairCLM line 3428
329. lemma OAI.KernelPairing.pairCLM_apply line 3443
330. lemma OAI.KernelPairing.laplacian_translate line 3453
331. lemma OAI.KernelPairing.schwartz_laplacian_translate line 3459
332. lemma OAI.KernelPairing.schwartz_bilaplacian_pair line 3467
333. lemma OAI.KernelPairing.bilaplacian_pair_kernel line 3473
334. lemma OAI.FrozenParametrix.integrable_kernel_pair_prod line 3513
335. lemma OAI.FrozenParametrix.integrable_bilap_pair_prod line 3534
336. lemma OAI.FrozenParametrix.pair_bilaplacian_timeValue line 3555
337. lemma OAI.FrozenParametrix.norm_bilap_integral_le line 3573
338. lemma OAI.FrozenParametrix.hasDerivAt_pair_timeValue line 3589
339. lemma OAI.FrozenParametrix.integrable_pair_bilaplacian line 3640
340. lemma OAI.FrozenParametrix.integrable_pair_timeValue line 3647
341. lemma OAI.FrozenParametrix.weak_frozen_residual line 3653
342. def OAI.FrozenParametrix.c0Time line 3694
343. lemma OAI.FrozenParametrix.continuous_c0Time line 3697
344. lemma OAI.FrozenParametrix.c0Time_zero line 3702
345. lemma OAI.FrozenParametrix.c0Time_apply line 3708
346. lemma OAI.FrozenParametrix.hasDerivAt_pair_c0Time line 3712
347. lemma OAI.FrozenParametrix.pair_c0Time_integral line 3726
348. lemma OAI.StrongWeightedVolterra.continuous_unweighted_on_time line 3754
349. lemma OAI.StrongWeightedVolterra.stronglyMeasurable_unweighted line 3759
350. lemma OAI.StrongWeightedVolterra.norm_unweighted_le line 3768
351. lemma OAI.StrongWeightedVolterra.intervalIntegrable_unweighted line 3777
352. lemma OAI.VolterraIntegral.integral_triangle_left line 3795
353. lemma OAI.VolterraIntegral.integral_triangle_right line 3809
354. lemma OAI.VolterraIntegral.integral_triangle_swap line 3823
355. lemma OAI.VolterraIntegral.integrableOn_triangle_of_bound line 3850
356. lemma OAI.VolterraIntegral.duhamel_integral_identity line 3868
357. def OAI.VolterraIntegral.sourceExtend line 3888
358. lemma OAI.VolterraIntegral.sourceExtend_apply line 3891
359. lemma OAI.VolterraIntegral.stronglyMeasurable_sourceExtend line 3894
360. lemma OAI.VolterraIntegral.integrableOn_sourceExtend line 3906
361. lemma OAI.VolterraIntegral.integrableOn_sourceExtend_triangle line 3917
362. lemma OAI.FrozenParametrix.continuous_c0Time_comp line 3941
363. lemma OAI.FrozenParametrix.norm_c0Time_le line 3954
364. lemma OAI.ParametrixVolterra.continuous_sourceMultiply line 3969
365. lemma OAI.ParametrixVolterra.norm_sourceMultiply_le line 3974
366. def OAI.ParametrixVolterra.sourceMultiply line 3980
367. lemma OAI.ParametrixVolterra.sourceMultiply_apply line 3983
368. lemma OAI.ParametrixVolterra.unweighted_sourceMultiply line 3986
369. def OAI.ParametrixVolterra.sourceFrozen line 4003
370. lemma OAI.ParametrixVolterra.continuous_sourceFrozen line 4006
371. lemma OAI.ParametrixVolterra.norm_sourceFrozen_le line 4012
372. lemma OAI.ParametrixVolterra.integrableOn_sourceFrozen_bound line 4018
373. lemma OAI.ParametrixVolterra.integrableOn_sourceFrozen_triangle line 4024
374. lemma OAI.ParametrixVolterra.intervalIntegrable_sourceFrozen line 4030
375. def OAI.ParametrixVolterra.duhamel line 4037
376. lemma OAI.ParametrixVolterra.sourceFrozen_eq_frozenRaw line 4040
377. lemma OAI.ParametrixVolterra.duhamel_eq_value line 4048
378. lemma OAI.ParametrixVolterra.continuousOn_duhamel line 4057
379. lemma OAI.ParametrixVolterra.continuousAt_duhamel line 4065
380. lemma OAI.ParametrixVolterra.integrableOn_pair_sourceFrozen_triangle line 4070
381. lemma OAI.ParametrixVolterra.sourceFrozen_weakFTC line 4077
382. lemma OAI.ParametrixVolterra.pair_duhamel_integral line 4106
383. lemma OAI.ParametrixVolterra.duhamel_zero line 4149
384. lemma OAI.ParametrixVolterra.norm_duhamel_le line 4151
385. lemma OAI.ParametrixVolterra.continuousWithinAt_duhamel_zero line 4162
386. lemma OAI.ParametrixVolterra.continuousOn_duhamel_Icc line 4179
387. lemma OAI.ParametrixVolterra.intervalIntegrable_duhamel line 4188
388. lemma OAI.ParametrixVolterra.hasDerivAt_pair_duhamel line 4194
389. lemma OAI.FrozenParametrix.pair_fullResidual line 4235
390. def OAI.ParametrixVolterra.adjointPair line 4260
391. lemma OAI.ParametrixVolterra.pair_residualKernel line 4265
392. lemma OAI.ParametrixVolterra.pair_integral_residualKernel line 4287
393. def OAI.ParametrixVolterra.mildTime line 4320
394. lemma OAI.ParametrixVolterra.mildTime_zero line 4323
395. lemma OAI.ParametrixVolterra.continuousOn_mildTime line 4326
396. lemma OAI.ParametrixVolterra.hasDerivAt_pair_mildTime line 4330
397. def OAI.StrongWeightedVolterra.dampWeight line 4375
398. lemma OAI.StrongWeightedVolterra.dampWeight_nonneg line 4377
399. lemma OAI.StrongWeightedVolterra.integrable_dampWeight line 4381
400. lemma OAI.StrongWeightedVolterra.eighth_exp_neg_le_one line 4400
401. lemma OAI.StrongWeightedVolterra.eighth_exp_scale_le line 4413
402. lemma OAI.StrongWeightedVolterra.damp_scalar_bound line 4431
403. def OAI.StrongWeightedVolterra.dampKernel line 4450
404. lemma OAI.StrongWeightedVolterra.norm_dampKernel_le line 4458
405. lemma OAI.StrongWeightedVolterra.norm_damp_data_le line 4470
406. lemma OAI.StrongWeightedVolterra.norm_damp_value_le line 4487
407. lemma OAI.StrongWeightedVolterra.norm_timeExp_le line 4499
408. def OAI.StrongWeightedVolterra.timeExp line 4506
409. lemma OAI.StrongWeightedVolterra.timeExp_apply line 4511
410. lemma OAI.StrongWeightedVolterra.timeExp_norm_le line 4514
411. lemma OAI.StrongWeightedVolterra.timeExp_add line 4519
412. lemma OAI.StrongWeightedVolterra.timeExp_comp line 4524
413. lemma OAI.StrongWeightedVolterra.timeExp_zero line 4529
414. lemma OAI.StrongWeightedVolterra.damp_data_conjugation line 4533
415. lemma OAI.StrongWeightedVolterra.damp_value_conjugation line 4544
416. lemma OAI.StrongWeightedVolterra.damp_operator_conjugation line 4550
417. lemma OAI.StrongWeightedVolterra.norm_damp_operator_le line 4557
418. lemma OAI.StrongWeightedVolterra.norm_damp_operatorCLM_le line 4567
419. lemma OAI.StrongWeightedVolterra.exists_damping_small line 4575
420. theorem OAI.StrongWeightedVolterra.exists_unique_solution_full line 4582
421. lemma OAI.StrongWeightedVolterra.norm_solution_full_le line 4615
422. theorem OAI.StrongWeightedVolterra.exists_full_inverse_bound line 4649
423. theorem OAI.StrongWeightedVolterra.exists_unweighted_solution_full line 4659
424. theorem OAI.ParametrixVolterra.exists_parametrix_correction_full line 4686
425. def OAI.ParametrixVolterra.coefficientTest line 4723
426. lemma OAI.ParametrixVolterra.coefficientTest_apply line 4729
427. theorem OAI.ParametrixVolterra.exists_weak_evolution line 4733
428. def OAI.SchwartzTimeScale.euler line 4782
429. lemma OAI.SchwartzTimeScale.euler_apply line 4788
430. def OAI.SchwartzTimeScale.atTime line 4791
431. lemma OAI.SchwartzTimeScale.hasDerivAt_atTime line 4794
432. lemma OAI.SchwartzTimeScale.atTime_eq_scaled line 4819
433. lemma OAI.SourceFrozenCancellation.parameter_envelope line 4837
434. lemma OAI.SourceFrozenCancellation.parameter_lipschitz_envelope line 4849
435. lemma OAI.SourceFrozenCancellation.integral_atTime_zero line 4860
436. lemma OAI.SourceFrozenCancellation.continuous_variable line 4867
437. lemma OAI.SourceFrozenCancellation.integrable_envelope_power line 4874
438. lemma OAI.SourceFrozenCancellation.norm_normalized_source_integral line 4891
439. def OAI.SchwartzDerivatives.iterated line 4964
440. lemma OAI.SchwartzDerivatives.iterated_coe line 4970
441. lemma OAI.SchwartzDerivatives.iterated_apply line 4981
442. lemma OAI.SchwartzDerivatives.integral_fderiv line 4991
443. lemma OAI.SchwartzDerivatives.integral_iterated line 4998
444. lemma OAI.ScaledSchwartzConvolution.iteratedFDeriv_value_smul line 5022
445. lemma OAI.ScaledSchwartzConvolution.iteratedFDeriv_value_smul_apply line 5057
446. lemma OAI.SourceFrozenScaling.normalized_integral line 5071
447. lemma OAI.SourceFrozenScaling.dimension_cancel line 5092
448. lemma OAI.SourceFrozenScaling.normalized_integral_order line 5096
449. def OAI.SourceFrozenRows.value line 5110
450. def OAI.SourceFrozenRows.row line 5114
451. lemma OAI.SourceFrozenRows.radius_bounds line 5121
452. lemma OAI.SourceFrozenRows.contDiff_value line 5129
453. lemma OAI.SourceFrozenRows.row_eq line 5137
454. lemma OAI.SourceFrozenRows.row_normalized line 5147
455. lemma OAI.SourceFrozenRows.exists_row_holder_bound line 5159
456. def OAI.SourceFrozenOrder.value line 5193
457. lemma OAI.SourceFrozenOrder.normalized line 5197
458. lemma OAI.SourceFrozenOrder.exists_norm_bound line 5209
459. lemma OAI.SourceFrozenOrder.hasFDerivAt_value line 5239
460. lemma OAI.SourceFrozenOrder.exists_bounds line 5256
461. def OAI.FrozenParametrix.bilapOne line 5278
462. def OAI.FrozenParametrix.heatOne line 5280
463. lemma OAI.FrozenParametrix.quarter_root line 5282
464. lemma OAI.FrozenParametrix.bilapKernel_ordered line 5286
465. lemma OAI.FrozenParametrix.kernel_ordered line 5295
466. lemma OAI.FrozenParametrix.integrable_ordered line 5307
467. lemma OAI.FrozenParametrix.principal_eq_ordered line 5319
468. lemma OAI.FrozenParametrix.frozen_eq_ordered line 5338
469. lemma OAI.ProductLipschitz.bound line 5352
470. lemma OAI.ProductLipschitz.inv_pow_le line 5368
471. lemma OAI.FrozenParametrix.norm_coefficient_le_pos line 5381
472. lemma OAI.FrozenParametrix.exists_principal_lipschitz_bound line 5388
473. lemma OAI.FrozenParametrix.exists_frozen_lipschitz_bound line 5434
474. lemma OAI.FrozenParametrix.exists_fullResidual_lipschitz_bound line 5458
475. lemma OAI.HolderInterpolation.scalar line 5486
476. lemma OAI.HolderInterpolation.scaled line 5499
477. lemma OAI.HolderInterpolation.residual line 5518
478. lemma OAI.ParabolicRadius.inv_pow_five line 5527
479. lemma OAI.ParametrixVolterra.exists_actualResidual_holder_bound line 5541
480. def OAI.BetaWeights.density line 5589
481. lemma OAI.BetaWeights.density_nonneg line 5591
482. lemma OAI.BetaWeights.intervalIntegrable_one line 5594
483. lemma OAI.BetaWeights.density_scaled line 5610
484. lemma OAI.BetaWeights.intervalIntegrable line 5617
485. lemma OAI.BetaWeights.integral_scale line 5629
486. def OAI.HolderIntegral.eval line 5652
487. lemma OAI.HolderIntegral.intervalIntegral_apply line 5660
488. lemma OAI.HolderIntegral.beta_holder line 5665
489. lemma OAI.ParametrixVolterra.holder_residual_integral line 5693
490. lemma OAI.ParametrixVolterra.correction_holder line 5723
491. lemma OAI.SourceFrozenRows.exists_row_zero_bound line 5773
492. lemma OAI.SourceFrozenRows.continuous_row line 5803
493. lemma OAI.SourceFrozenRows.hasFDerivAt_row line 5812
494. lemma OAI.SourceFrozenRows.stronglyMeasurable_time_row line 5826
495. lemma OAI.SourceFrozenRows.radius_weight line 5846
496. lemma OAI.SourceFrozenRows.integrableOn_lag_rpow line 5860
497. lemma OAI.SourceFrozenRows.exists_integrable_row_bound line 5866
498. def OAI.SourceFrozenRows.integralRow line 5918
499. lemma OAI.SourceFrozenRows.integrableOn_row line 5931
500. lemma OAI.SourceFrozenRows.continuous_integralRow line 5937
501. lemma OAI.SourceFrozenRows.hasFDerivAt_integralRow line 5951
502. lemma OAI.SourceFrozenRows.contDiff_integralRow line 5981
503. def OAI.SourceFrozenRows.duhamel line 6001
504. lemma OAI.SourceFrozenRows.duhamel_eq_integralRow_zero line 6014
505. lemma OAI.SourceFrozenRows.contDiff_duhamel line 6029
506. lemma OAI.SourceFrozenRows.iteratedFDeriv_duhamel line 6040
507. lemma OAI.SourceFrozenRows.exists_norm_iteratedFDeriv_duhamel_bound line 6056
508. lemma OAI.SourceFrozenRows.stronglyMeasurable_time_row_of_stronglyMeasurable line 6071
509. lemma OAI.SourceFrozenRows.exists_integrable_row_bound_weighted line 6093
510. lemma OAI.WeightedSourceFrozenRows.integrableOn_row line 6178
511. lemma OAI.WeightedSourceFrozenRows.continuous_integralRow line 6184
512. lemma OAI.WeightedSourceFrozenRows.hasFDerivAt_integralRow line 6198
513. lemma OAI.WeightedSourceFrozenRows.contDiff_integralRow line 6228
514. lemma OAI.WeightedSourceFrozenRows.duhamel_eq_integralRow_zero line 6242
515. lemma OAI.WeightedSourceFrozenRows.contDiff_duhamel line 6257
516. lemma OAI.WeightedSourceFrozenRows.iteratedFDeriv_duhamel line 6268
517. lemma OAI.WeightedSourceFrozenRows.exists_norm_iteratedFDeriv_duhamel_bound line 6284