OAI/Combinatorics/Progressions/Lattices/AllocatedFixedPathSlicedKernelResidueRiemann.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleFullSlice_residue_riemann line 38
2. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleFullSlice_full_residue_real_riemann line 123
3. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleFullSlice_full_residue_complex_riemann line 163
4. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSample_full_residue_perturbed_riemann line 237
5. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedSpatialKernelMap_lipschitz line 353
6. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPath_kernel_residue_riemann line 361
7. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPath_joint_residue_riemann line 413
8. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPath_joint_residue_weighted_riemann line 524
9. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPath_sliced_kernel_residue_riemann line 619