OAI/Analysis/AncientFlat/Regularity/ResidualSmoothing.lean

GitHub source file

337 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ResidualSmoothing.BiharmonicKernel.gaussian_moment_bound line 13
2. lemma OAI.ResidualSmoothing.BiharmonicKernel.polynomial_gaussian_bound line 42
3. def OAI.ResidualSmoothing.BiharmonicKernel.gaussian line 66
4. lemma OAI.ResidualSmoothing.BiharmonicKernel.norm_le_quadratic line 82
5. def OAI.ResidualSmoothing.BiharmonicKernel.multiplier line 92
6. lemma OAI.ResidualSmoothing.BiharmonicKernel.multiplier_apply line 98
7. def OAI.ResidualSmoothing.BiharmonicKernel.heatKernel line 108
8. lemma OAI.ResidualSmoothing.BiharmonicKernel.fourier_heatKernel line 111
9. lemma OAI.ResidualSmoothing.BiharmonicKernel.integral_heatKernel line 115
10. lemma OAI.ResidualSmoothing.BiharmonicKernel.heatKernel_decay line 120
11. lemma OAI.ResidualSmoothing.BiharmonicKernel.heatKernel_invariant line 131
12. lemma OAI.ResidualSmoothing.BiharmonicKernel.fourierInv_comp_smul line 144
13. lemma OAI.ResidualSmoothing.BiharmonicKernel.heatKernel_scaling line 154
14. lemma OAI.ResidualSmoothing.BiharmonicKernel.heatKernel_deriv_scaling line 166
15. lemma OAI.ResidualSmoothing.BiharmonicKernel.heatKernel_scaled_decay line 179
16. def OAI.ResidualSmoothing.BiharmonicKernel.symbol line 194
17. lemma OAI.ResidualSmoothing.BiharmonicKernel.symbol_nonneg line 197
18. lemma OAI.ResidualSmoothing.BiharmonicKernel.symbol_temperate line 200
19. def OAI.ResidualSmoothing.BiharmonicKernel.kernel line 208
20. lemma OAI.ResidualSmoothing.BiharmonicKernel.heatKernel_eq_kernel line 211
21. lemma OAI.ResidualSmoothing.BiharmonicKernel.kernel_hasDerivAt line 220
22. lemma OAI.ResidualSmoothing.BiharmonicKernel.biharmonic_eq_fourierMultiplier line 278
23. lemma OAI.ResidualSmoothing.BiharmonicKernel.kernel_heat_equation line 293
24. lemma OAI.ResidualSmoothing.BiharmonicKernel.kernel_eq_scaled line 311
25. lemma OAI.ResidualSmoothing.BiharmonicKernel.kernel_contDiffAt line 324
26. lemma OAI.ResidualSmoothing.BiharmonicKernel.integral_norm_heatKernel line 339
27. def OAI.ResidualSmoothing.C0Convolution.translate line 362
28. lemma OAI.ResidualSmoothing.C0Convolution.translate_apply line 365
29. lemma OAI.ResidualSmoothing.C0Convolution.translate_zero line 368
30. lemma OAI.ResidualSmoothing.C0Convolution.translate_add line 372
31. lemma OAI.ResidualSmoothing.C0Convolution.translate_smul line 375
32. lemma OAI.ResidualSmoothing.C0Convolution.norm_le_iff line 378
33. lemma OAI.ResidualSmoothing.C0Convolution.apply_norm_le line 382
34. lemma OAI.ResidualSmoothing.C0Convolution.norm_translate line 385
35. lemma OAI.ResidualSmoothing.C0Convolution.continuous_translate line 392
36. def OAI.ResidualSmoothing.C0Convolution.eval line 407
37. lemma OAI.ResidualSmoothing.C0Convolution.eval_apply line 414
38. lemma OAI.ResidualSmoothing.C0Convolution.integrable_translated line 418
39. def OAI.ResidualSmoothing.C0Convolution.convolve line 425
40. lemma OAI.ResidualSmoothing.C0Convolution.convolve_apply line 428
41. lemma OAI.ResidualSmoothing.C0Convolution.norm_convolve_le line 434
42. lemma OAI.ResidualSmoothing.C0Convolution.convolve_add line 440
43. lemma OAI.ResidualSmoothing.C0Convolution.convolve_smul line 450
44. def OAI.ResidualSmoothing.C0Convolution.convolveCLM line 454
45. lemma OAI.ResidualSmoothing.C0Convolution.norm_convolveCLM_le line 461
46. lemma OAI.ResidualSmoothing.C0Convolution.integrable_scaled_translated line 467
47. def OAI.ResidualSmoothing.C0Convolution.scaleConvolve line 476
48. lemma OAI.ResidualSmoothing.C0Convolution.continuous_scaleConvolve line 479
49. lemma OAI.ResidualSmoothing.C0Convolution.scaleConvolve_zero line 493
50. lemma OAI.ResidualSmoothing.C0Convolution.scaleConvolve_tendsto line 497
51. lemma OAI.ResidualSmoothing.C0Convolution.convolve_scaled line 506
52. lemma OAI.ResidualSmoothing.C0Convolution.convolve_coe line 526
53. lemma OAI.ResidualSmoothing.C0Convolution.convolve_assoc line 531
54. lemma OAI.ResidualSmoothing.BiharmonicKernel.heatKernel_semigroup line 561
55. def OAI.ResidualSmoothing.BiharmonicKernel.evolution line 574
56. lemma OAI.ResidualSmoothing.BiharmonicKernel.evolution_zero line 578
57. lemma OAI.ResidualSmoothing.BiharmonicKernel.evolution_continuous line 582
58. lemma OAI.ResidualSmoothing.BiharmonicKernel.evolution_initial_trace line 587
59. lemma OAI.ResidualSmoothing.BiharmonicKernel.evolution_eq_convolve line 591
60. lemma OAI.ResidualSmoothing.BiharmonicKernel.evolution_apply line 602
61. lemma OAI.ResidualSmoothing.BiharmonicKernel.evolution_norm_le line 607
62. lemma OAI.ResidualSmoothing.BiharmonicKernel.evolution_semigroup line 614
63. lemma OAI.ResidualSmoothing.SchwartzConvolution.shifted_majorant line 642
64. lemma OAI.ResidualSmoothing.SchwartzConvolution.integrable_integrand line 669
65. lemma OAI.ResidualSmoothing.SchwartzConvolution.hasFDerivAt_convolution line 679
66. lemma OAI.ResidualSmoothing.SchwartzConvolution.contDiff_convolution_nat line 705
67. lemma OAI.ResidualSmoothing.SchwartzConvolution.contDiff_convolution line 717
68. lemma OAI.ResidualSmoothing.SchwartzConvolution.fderiv_convolution line 722
69. lemma OAI.ResidualSmoothing.SchwartzConvolution.fderiv_convolution_apply line 728
70. lemma OAI.ResidualSmoothing.SchwartzConvolution.second_fderiv_convolution_apply line 736
71. lemma OAI.ResidualSmoothing.SchwartzConvolution.laplacian_convolution line 758
72. lemma OAI.ResidualSmoothing.SchwartzConvolution.scaled_majorant line 789
73. lemma OAI.ResidualSmoothing.LaplacianScaling.laplacian_scaled line 835
74. lemma OAI.ResidualSmoothing.BiharmonicKernel.laplacian_kernel_scaling line 853
75. lemma OAI.ResidualSmoothing.BiharmonicKernel.biharmonic_kernel_scaling line 866
76. lemma OAI.ResidualSmoothing.BiharmonicKernel.evolution_coe_convolution line 882
77. lemma OAI.ResidualSmoothing.BiharmonicKernel.evolution_smooth line 892
78. lemma OAI.ResidualSmoothing.BiharmonicKernel.evolution_biharmonic line 897
79. lemma OAI.ResidualSmoothing.BiharmonicKernel.kernel_deriv_majorant line 903
80. lemma OAI.ResidualSmoothing.BiharmonicKernel.evolution_hasDerivAt line 927
81. lemma OAI.ResidualSmoothing.BiharmonicKernel.evolution_heat_equation line 984
82. lemma OAI.ResidualSmoothing.BiharmonicKernel.kernel_majorant line 1009
83. lemma OAI.ResidualSmoothing.BiharmonicKernel.continuous_kernel_comp line 1020
84. def OAI.ResidualSmoothing.FrozenParametrix.value line 1037
85. lemma OAI.ResidualSmoothing.FrozenParametrix.integrable_value line 1040
86. lemma OAI.ResidualSmoothing.FrozenParametrix.continuous_value line 1053
87. lemma OAI.ResidualSmoothing.FrozenParametrix.zero_at_infty_value line 1072
88. def OAI.ResidualSmoothing.FrozenParametrix.frozen line 1100
89. def OAI.ResidualSmoothing.C0Multiplier.mul line 1116
90. lemma OAI.ResidualSmoothing.C0Multiplier.mul_apply line 1126
91. lemma OAI.ResidualSmoothing.C0Multiplier.norm_mul_le line 1129
92. def OAI.ResidualSmoothing.C0Multiplier.mulCLM line 1138
93. lemma OAI.ResidualSmoothing.C0Multiplier.continuous_mul line 1148
94. lemma OAI.ResidualSmoothing.C0Convolution.translate_sub line 1157
95. lemma OAI.ResidualSmoothing.C0Convolution.continuous_translate_comp line 1160
96. def OAI.ResidualSmoothing.FrozenParametrix.kernelFamily line 1182
97. lemma OAI.ResidualSmoothing.FrozenParametrix.continuous_kernelFamily line 1187
98. def OAI.ResidualSmoothing.FrozenParametrix.sourceMultiplier line 1194
99. lemma OAI.ResidualSmoothing.FrozenParametrix.continuous_sourceMultiplier line 1199
100. def OAI.ResidualSmoothing.FrozenParametrix.sourceData line 1207
101. lemma OAI.ResidualSmoothing.FrozenParametrix.continuous_sourceData line 1211
102. lemma OAI.ResidualSmoothing.FrozenParametrix.sourceData_apply line 1216
103. lemma OAI.ResidualSmoothing.FrozenParametrix.sourceData_norm_le line 1220
104. lemma OAI.ResidualSmoothing.FrozenParametrix.integrable_translated_sourceData line 1231
105. lemma OAI.ResidualSmoothing.FrozenParametrix.frozen_eq_integral line 1243
106. lemma OAI.ResidualSmoothing.FrozenParametrix.continuous_frozen line 1253
107. lemma OAI.ResidualSmoothing.FrozenParametrix.frozen_zero line 1270
108. lemma OAI.ResidualSmoothing.FrozenParametrix.frozen_tendsto_identity line 1278
109. lemma OAI.ResidualSmoothing.FrozenParametrix.norm_frozen_le line 1284
110. lemma OAI.ResidualSmoothing.FrozenParametrix.frozen_add line 1294
111. lemma OAI.ResidualSmoothing.FrozenParametrix.frozen_smul line 1306
112. lemma OAI.ResidualSmoothing.FrozenParametrix.exists_uniform_norm_bound line 1314
113. lemma OAI.ResidualSmoothing.FrozenParametrix.frozen_apply_unscaled line 1324
114. lemma OAI.ResidualSmoothing.SchwartzConvolution.scaled_weighted_majorant line 1358
115. def OAI.ResidualSmoothing.BiharmonicKernel.bilapKernel line 1419
116. lemma OAI.ResidualSmoothing.BiharmonicKernel.bilapKernel_eq_schwartz line 1421
117. lemma OAI.ResidualSmoothing.BiharmonicKernel.bilapKernel_eq_scaled line 1430
118. lemma OAI.ResidualSmoothing.BiharmonicKernel.bilapKernel_contDiffAt line 1446
119. lemma OAI.ResidualSmoothing.BiharmonicKernel.continuous_bilapKernel_comp line 1461
120. lemma OAI.ResidualSmoothing.BiharmonicKernel.bilapKernel_weighted_majorant line 1470
121. def OAI.ResidualSmoothing.C0Multiplier.mulLeftCLM line 1487
122. lemma OAI.ResidualSmoothing.C0Multiplier.continuous_mul_left line 1494
123. def OAI.ResidualSmoothing.FrozenFamily.family line 1503
124. lemma OAI.ResidualSmoothing.FrozenFamily.continuous_family line 1507
125. def OAI.ResidualSmoothing.FrozenFamily.multiplier line 1511
126. lemma OAI.ResidualSmoothing.FrozenFamily.continuous_multiplier line 1514
127. def OAI.ResidualSmoothing.FrozenFamily.data line 1519
128. lemma OAI.ResidualSmoothing.FrozenFamily.data_apply line 1522
129. lemma OAI.ResidualSmoothing.FrozenFamily.continuous_data line 1525
130. lemma OAI.ResidualSmoothing.FrozenFamily.norm_data_le line 1529
131. def OAI.ResidualSmoothing.FrozenFamily.residualData line 1539
132. lemma OAI.ResidualSmoothing.FrozenFamily.residualData_apply line 1544
133. lemma OAI.ResidualSmoothing.FrozenFamily.continuous_residualData line 1552
134. lemma OAI.ResidualSmoothing.FrozenFamily.norm_residualData_le line 1560
135. lemma OAI.ResidualSmoothing.FrozenFamily.integrable_residualData line 1577
136. def OAI.ResidualSmoothing.FrozenFamily.residual line 1596
137. lemma OAI.ResidualSmoothing.FrozenFamily.residual_apply line 1600
138. lemma OAI.ResidualSmoothing.FrozenFamily.norm_residual_le line 1610
139. lemma OAI.ResidualSmoothing.BiharmonicKernel.bilapKernel_scaling line 1643
140. def OAI.ResidualSmoothing.FrozenParametrix.bilapFamily line 1656
141. def OAI.ResidualSmoothing.FrozenParametrix.coefficient line 1662
142. lemma OAI.ResidualSmoothing.FrozenParametrix.coefficient_apply line 1667
143. def OAI.ResidualSmoothing.FrozenParametrix.principalResidual line 1670
144. lemma OAI.ResidualSmoothing.FrozenParametrix.principalResidual_apply_scaled line 1675
145. lemma OAI.ResidualSmoothing.FrozenParametrix.principalResidual_apply_unscaled line 1688
146. lemma OAI.ResidualSmoothing.FrozenParametrix.norm_principalResidual_le line 1713
147. lemma OAI.ResidualSmoothing.FrozenParametrix.exists_uniform_principalResidual_bound line 1730
148. def OAI.ResidualSmoothing.CompactComposition.compose line 1766
149. lemma OAI.ResidualSmoothing.CompactComposition.compose_apply line 1769
150. lemma OAI.ResidualSmoothing.CompactComposition.continuous_compose line 1772
151. lemma OAI.ResidualSmoothing.C0Multiplier.continuous_mul_joint line 1796
152. lemma OAI.ResidualSmoothing.FrozenFamily.continuous_multiplier_comp line 1809
153. lemma OAI.ResidualSmoothing.FrozenFamily.continuous_data_comp line 1817
154. lemma OAI.ResidualSmoothing.FrozenFamily.continuous_residualData_comp line 1823
155. lemma OAI.ResidualSmoothing.FrozenFamily.norm_residualData_le_uniform line 1839
156. lemma OAI.ResidualSmoothing.FrozenFamily.continuous_residual_comp line 1853
157. lemma OAI.ResidualSmoothing.FrozenFamily.residual_add line 1868
158. lemma OAI.ResidualSmoothing.FrozenFamily.residual_smul line 1884
159. lemma OAI.ResidualSmoothing.FrozenFamily.norm_residual_le_uniform line 1896
160. def OAI.ResidualSmoothing.FrozenFamily.residualCLM line 1906
161. def OAI.ResidualSmoothing.FrozenParametrix.frozenOp line 1924
162. lemma OAI.ResidualSmoothing.FrozenParametrix.kernel_majorant_nonneg line 1928
163. def OAI.ResidualSmoothing.FrozenParametrix.kernelMajorant line 1935
164. lemma OAI.ResidualSmoothing.FrozenParametrix.kernelMajorant_spec line 1937
165. def OAI.ResidualSmoothing.FrozenParametrix.frozenCLM line 1943
166. lemma OAI.ResidualSmoothing.FrozenParametrix.frozenCLM_apply line 1952
167. lemma OAI.ResidualSmoothing.FrozenParametrix.norm_frozenCLM_le line 1955
168. def OAI.ResidualSmoothing.FrozenParametrix.kernelFamilyCM line 1963
169. lemma OAI.ResidualSmoothing.FrozenParametrix.continuous_frozenOp_comp line 1969
170. lemma OAI.ResidualSmoothing.FrozenParametrix.continuous_coefficient_comp line 1991
171. lemma OAI.ResidualSmoothing.FrozenParametrix.norm_coefficient_le line 1997
172. def OAI.ResidualSmoothing.FrozenParametrix.bilapMajorant line 2006
173. lemma OAI.ResidualSmoothing.FrozenParametrix.bilapMajorant_spec line 2008
174. def OAI.ResidualSmoothing.FrozenParametrix.principalCLM line 2015
175. lemma OAI.ResidualSmoothing.FrozenParametrix.principalCLM_apply line 2021
176. lemma OAI.ResidualSmoothing.FrozenParametrix.continuous_principalCLM_apply line 2024
177. def OAI.ResidualSmoothing.FrozenParametrix.fullResidualCLM line 2040
178. lemma OAI.ResidualSmoothing.FrozenParametrix.fullResidualCLM_apply line 2044
179. lemma OAI.ResidualSmoothing.FrozenParametrix.continuous_fullResidualCLM_apply line 2048
180. lemma OAI.ResidualSmoothing.FrozenParametrix.exists_uniform_fullResidual_bound line 2057
181. abbrev OAI.ResidualSmoothing.StrongWeightedVolterra.UnitTime line 2089
182. abbrev OAI.ResidualSmoothing.StrongWeightedVolterra.Time line 2090
183. instance OAI.ResidualSmoothing.StrongWeightedVolterra.(instance at line 2092) line 2092
184. def OAI.ResidualSmoothing.StrongWeightedVolterra.weight line 2094
185. lemma OAI.ResidualSmoothing.StrongWeightedVolterra.weight_nonneg line 2096
186. lemma OAI.ResidualSmoothing.StrongWeightedVolterra.continuous_weight line 2099
187. lemma OAI.ResidualSmoothing.StrongWeightedVolterra.integrable_weight line 2105
188. def OAI.ResidualSmoothing.StrongWeightedVolterra.lag line 2126
189. lemma OAI.ResidualSmoothing.StrongWeightedVolterra.continuous_lag line 2130
190. structure OAI.ResidualSmoothing.StrongWeightedVolterra.Kernel line 2134
191. instance OAI.ResidualSmoothing.StrongWeightedVolterra.(instance at line 2138) line 2138
192. lemma OAI.ResidualSmoothing.StrongWeightedVolterra.continuous_apply_of_strong line 2140
193. def OAI.ResidualSmoothing.StrongWeightedVolterra.Kernel.ofStrong line 2157
194. def OAI.ResidualSmoothing.StrongWeightedVolterra.data line 2165
195. lemma OAI.ResidualSmoothing.StrongWeightedVolterra.continuous_data line 2168
196. lemma OAI.ResidualSmoothing.StrongWeightedVolterra.norm_data_le line 2175
197. lemma OAI.ResidualSmoothing.StrongWeightedVolterra.integrable_data line 2182
198. lemma OAI.ResidualSmoothing.StrongWeightedVolterra.continuous_integral_data line 2187
199. lemma OAI.ResidualSmoothing.StrongWeightedVolterra.norm_integral_data_le line 2196
200. def OAI.ResidualSmoothing.StrongWeightedVolterra.value line 2205
201. lemma OAI.ResidualSmoothing.StrongWeightedVolterra.continuous_value line 2208
202. lemma OAI.ResidualSmoothing.StrongWeightedVolterra.norm_value_le line 2212
203. def OAI.ResidualSmoothing.StrongWeightedVolterra.operator line 2222
204. lemma OAI.ResidualSmoothing.StrongWeightedVolterra.operator_apply line 2230
205. lemma OAI.ResidualSmoothing.StrongWeightedVolterra.norm_operator_le line 2233
206. lemma OAI.ResidualSmoothing.StrongWeightedVolterra.operator_add line 2240
207. lemma OAI.ResidualSmoothing.StrongWeightedVolterra.operator_smul line 2249
208. def OAI.ResidualSmoothing.StrongWeightedVolterra.operatorCLM line 2259
209. lemma OAI.ResidualSmoothing.StrongWeightedVolterra.norm_operatorCLM_le line 2267
210. theorem OAI.ResidualSmoothing.StrongWeightedVolterra.exists_unique_solution line 2273
211. lemma OAI.ResidualSmoothing.StrongWeightedVolterra.norm_solution_le line 2295
212. def OAI.ResidualSmoothing.StrongWeightedVolterra.unweighted line 2309
213. lemma OAI.ResidualSmoothing.StrongWeightedVolterra.unweighted_lag line 2313
214. def OAI.ResidualSmoothing.StrongWeightedVolterra.normalizedArg line 2320
215. def OAI.ResidualSmoothing.StrongWeightedVolterra.kernel line 2325
216. lemma OAI.ResidualSmoothing.StrongWeightedVolterra.normalizedArg_lag line 2330
217. lemma OAI.ResidualSmoothing.StrongWeightedVolterra.kernel_lag line 2337
218. lemma OAI.ResidualSmoothing.StrongWeightedVolterra.rescaling_scalar line 2346
219. lemma OAI.ResidualSmoothing.StrongWeightedVolterra.value_eq_volterra line 2362
220. lemma OAI.ResidualSmoothing.StrongWeightedVolterra.unweighted_at_time line 2385
221. lemma OAI.ResidualSmoothing.StrongWeightedVolterra.kernel_unweighted_lag line 2390
222. lemma OAI.ResidualSmoothing.StrongWeightedVolterra.intervalIntegrable_kernel_unweighted line 2400
223. lemma OAI.ResidualSmoothing.StrongWeightedVolterra.unweighted_solves line 2413
224. theorem OAI.ResidualSmoothing.StrongWeightedVolterra.exists_unweighted_solution line 2427
225. def OAI.ResidualSmoothing.ParabolicRadius.radius line 2451
226. lemma OAI.ResidualSmoothing.ParabolicRadius.pos line 2453
227. lemma OAI.ResidualSmoothing.ParabolicRadius.nonneg line 2454
228. lemma OAI.ResidualSmoothing.ParabolicRadius.pow_four line 2455
229. lemma OAI.ResidualSmoothing.ParabolicRadius.pow_three line 2458
230. lemma OAI.ResidualSmoothing.ParabolicRadius.inv_pow_three line 2461
231. lemma OAI.ResidualSmoothing.ParabolicRadius.le_one line 2465
232. lemma OAI.ResidualSmoothing.ParabolicRadius.continuous_comp line 2467
233. lemma OAI.ResidualSmoothing.ParabolicRadius.normalized_cancel line 2470
234. abbrev OAI.ResidualSmoothing.ParametrixVolterra.Slab line 2485
235. def OAI.ResidualSmoothing.ParametrixVolterra.now line 2487
236. def OAI.ResidualSmoothing.ParametrixVolterra.before line 2488
237. def OAI.ResidualSmoothing.ParametrixVolterra.elapsed line 2489
238. lemma OAI.ResidualSmoothing.ParametrixVolterra.continuous_now line 2491
239. lemma OAI.ResidualSmoothing.ParametrixVolterra.continuous_before line 2492
240. lemma OAI.ResidualSmoothing.ParametrixVolterra.continuous_elapsed line 2494
241. lemma OAI.ResidualSmoothing.ParametrixVolterra.elapsed_pos line 2497
242. lemma OAI.ResidualSmoothing.ParametrixVolterra.elapsed_le line 2499
243. lemma OAI.ResidualSmoothing.ParametrixVolterra.elapsed_eq_sub line 2502
244. def OAI.ResidualSmoothing.ParametrixVolterra.actualResidual line 2508
245. def OAI.ResidualSmoothing.ParametrixVolterra.normalized line 2512
246. lemma OAI.ResidualSmoothing.ParametrixVolterra.continuous_actualResidual_before line 2515
247. lemma OAI.ResidualSmoothing.ParametrixVolterra.continuous_normalized_apply line 2528
248. lemma OAI.ResidualSmoothing.ParametrixVolterra.exists_normalized_bound line 2534
249. theorem OAI.ResidualSmoothing.ParametrixVolterra.exists_correction line 2562
250. lemma OAI.ResidualSmoothing.ParametrixVolterra.exists_actualResidual_bound line 2581
251. def OAI.ResidualSmoothing.ParametrixVolterra.initial line 2600
252. lemma OAI.ResidualSmoothing.ParametrixVolterra.continuous_initialResidual line 2602
253. def OAI.ResidualSmoothing.ParametrixVolterra.sourceRHS line 2613
254. lemma OAI.ResidualSmoothing.ParametrixVolterra.continuous_sourceRHS line 2616
255. lemma OAI.ResidualSmoothing.ParametrixVolterra.norm_sourceRHS_le line 2621
256. def OAI.ResidualSmoothing.ParametrixVolterra.weightedSource line 2640
257. lemma OAI.ResidualSmoothing.ParametrixVolterra.unweighted_weightedSource line 2651
258. def OAI.ResidualSmoothing.ParametrixVolterra.residualKernel line 2662
259. lemma OAI.ResidualSmoothing.ParametrixVolterra.elapsed_normalizedArg line 2665
260. lemma OAI.ResidualSmoothing.ParametrixVolterra.before_normalizedArg line 2670
261. lemma OAI.ResidualSmoothing.ParametrixVolterra.kernel_eq_residualKernel line 2678
262. theorem OAI.ResidualSmoothing.ParametrixVolterra.exists_parametrix_correction line 2704
263. def OAI.ResidualSmoothing.SchwartzTimeScale.euler line 2751
264. lemma OAI.ResidualSmoothing.SchwartzTimeScale.euler_apply line 2757
265. def OAI.ResidualSmoothing.SchwartzTimeScale.atTime line 2760
266. lemma OAI.ResidualSmoothing.SchwartzTimeScale.hasDerivAt_atTime line 2763
267. lemma OAI.ResidualSmoothing.SchwartzTimeScale.atTime_eq_scaled line 2788
268. lemma OAI.ResidualSmoothing.SourceFrozenCancellation.parameter_envelope line 2806
269. lemma OAI.ResidualSmoothing.SourceFrozenCancellation.parameter_lipschitz_envelope line 2818
270. lemma OAI.ResidualSmoothing.SourceFrozenCancellation.integral_atTime_zero line 2829
271. lemma OAI.ResidualSmoothing.SourceFrozenCancellation.continuous_variable line 2836
272. lemma OAI.ResidualSmoothing.SourceFrozenCancellation.integrable_envelope_power line 2843
273. lemma OAI.ResidualSmoothing.SourceFrozenCancellation.norm_normalized_source_integral line 2860
274. def OAI.ResidualSmoothing.SchwartzDerivatives.iterated line 2933
275. lemma OAI.ResidualSmoothing.SchwartzDerivatives.iterated_coe line 2939
276. lemma OAI.ResidualSmoothing.SchwartzDerivatives.iterated_apply line 2950
277. lemma OAI.ResidualSmoothing.SchwartzDerivatives.integral_fderiv line 2960
278. lemma OAI.ResidualSmoothing.SchwartzDerivatives.integral_iterated line 2967
279. lemma OAI.ResidualSmoothing.ScaledSchwartzConvolution.scaled_decay line 2996
280. lemma OAI.ResidualSmoothing.ScaledSchwartzConvolution.shifted_majorant line 3027
281. def OAI.ResidualSmoothing.ScaledSchwartzConvolution.value line 3051
282. lemma OAI.ResidualSmoothing.ScaledSchwartzConvolution.integrable_integrand line 3055
283. lemma OAI.ResidualSmoothing.ScaledSchwartzConvolution.hasFDerivAt_value line 3068
284. lemma OAI.ResidualSmoothing.ScaledSchwartzConvolution.contDiff_value_nat line 3098
285. lemma OAI.ResidualSmoothing.ScaledSchwartzConvolution.contDiff_value line 3109
286. lemma OAI.ResidualSmoothing.ScaledSchwartzConvolution.fderiv_value line 3113
287. lemma OAI.ResidualSmoothing.ScaledSchwartzConvolution.fderiv_value_apply line 3119
288. lemma OAI.ResidualSmoothing.ScaledSchwartzConvolution.second_fderiv_value_apply line 3128
289. lemma OAI.ResidualSmoothing.ScaledSchwartzConvolution.laplacian_value line 3153
290. lemma OAI.ResidualSmoothing.ScaledSchwartzConvolution.bilaplacian_value line 3173
291. lemma OAI.ResidualSmoothing.ScaledSchwartzConvolution.iteratedFDeriv_value_smul line 3187
292. lemma OAI.ResidualSmoothing.ScaledSchwartzConvolution.iteratedFDeriv_value_smul_apply line 3222
293. lemma OAI.ResidualSmoothing.SourceFrozenScaling.normalized_integral line 3236
294. lemma OAI.ResidualSmoothing.SourceFrozenScaling.dimension_cancel line 3257
295. lemma OAI.ResidualSmoothing.SourceFrozenScaling.normalized_integral_order line 3261
296. def OAI.ResidualSmoothing.SourceFrozenRows.value line 3275
297. def OAI.ResidualSmoothing.SourceFrozenRows.row line 3279
298. lemma OAI.ResidualSmoothing.SourceFrozenRows.radius_bounds line 3286
299. lemma OAI.ResidualSmoothing.SourceFrozenRows.contDiff_value line 3294
300. lemma OAI.ResidualSmoothing.SourceFrozenRows.row_eq line 3302
301. lemma OAI.ResidualSmoothing.SourceFrozenRows.row_normalized line 3312
302. lemma OAI.ResidualSmoothing.SourceFrozenRows.exists_row_holder_bound line 3324
303. def OAI.ResidualSmoothing.SourceFrozenOrder.value line 3358
304. lemma OAI.ResidualSmoothing.SourceFrozenOrder.normalized line 3362
305. lemma OAI.ResidualSmoothing.SourceFrozenOrder.exists_norm_bound line 3374
306. lemma OAI.ResidualSmoothing.SourceFrozenOrder.hasFDerivAt_value line 3404
307. lemma OAI.ResidualSmoothing.SourceFrozenOrder.exists_bounds line 3421
308. def OAI.ResidualSmoothing.FrozenParametrix.bilapOne line 3443
309. def OAI.ResidualSmoothing.FrozenParametrix.heatOne line 3445
310. lemma OAI.ResidualSmoothing.FrozenParametrix.quarter_root line 3447
311. lemma OAI.ResidualSmoothing.FrozenParametrix.bilapKernel_ordered line 3451
312. lemma OAI.ResidualSmoothing.FrozenParametrix.kernel_ordered line 3460
313. lemma OAI.ResidualSmoothing.FrozenParametrix.integrable_ordered line 3472
314. lemma OAI.ResidualSmoothing.FrozenParametrix.principal_eq_ordered line 3484
315. lemma OAI.ResidualSmoothing.FrozenParametrix.frozen_eq_ordered line 3503
316. lemma OAI.ResidualSmoothing.ProductLipschitz.bound line 3517
317. lemma OAI.ResidualSmoothing.ProductLipschitz.inv_pow_le line 3533
318. lemma OAI.ResidualSmoothing.FrozenParametrix.norm_coefficient_le_pos line 3546
319. lemma OAI.ResidualSmoothing.FrozenParametrix.exists_principal_lipschitz_bound line 3553
320. lemma OAI.ResidualSmoothing.FrozenParametrix.exists_frozen_lipschitz_bound line 3599
321. lemma OAI.ResidualSmoothing.FrozenParametrix.exists_fullResidual_lipschitz_bound line 3623
322. lemma OAI.ResidualSmoothing.HolderInterpolation.scalar line 3651
323. lemma OAI.ResidualSmoothing.HolderInterpolation.scaled line 3664
324. lemma OAI.ResidualSmoothing.HolderInterpolation.residual line 3683
325. lemma OAI.ResidualSmoothing.ParabolicRadius.inv_pow_five line 3692
326. lemma OAI.ResidualSmoothing.ParametrixVolterra.exists_actualResidual_holder_bound line 3706
327. def OAI.ResidualSmoothing.BetaWeights.density line 3754
328. lemma OAI.ResidualSmoothing.BetaWeights.density_nonneg line 3756
329. lemma OAI.ResidualSmoothing.BetaWeights.intervalIntegrable_one line 3759
330. lemma OAI.ResidualSmoothing.BetaWeights.density_scaled line 3775
331. lemma OAI.ResidualSmoothing.BetaWeights.intervalIntegrable line 3782
332. lemma OAI.ResidualSmoothing.BetaWeights.integral_scale line 3794
333. def OAI.ResidualSmoothing.HolderIntegral.eval line 3817
334. lemma OAI.ResidualSmoothing.HolderIntegral.intervalIntegral_apply line 3825
335. lemma OAI.ResidualSmoothing.HolderIntegral.beta_holder line 3830
336. lemma OAI.ResidualSmoothing.ParametrixVolterra.holder_residual_integral line 3858
337. lemma OAI.ResidualSmoothing.ParametrixVolterra.correction_holder line 3888