OAI/Combinatorics/Progressions/Lattices/OriginalKernelResidueRetained.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.intervalUniformWeights_residue_weight line 14
  2. theorem OAI.Erdos3.intervalUniformWeights_residue_weight_error line 26
  3. theorem OAI.Erdos3.intervalUniformWeights_residue_l1_error line 46
  4. theorem OAI.Erdos3.scalarCubeResidueWeights_pi_complex_riemann line 67
  5. theorem OAI.Erdos3.kernelResidue_joint_complex_riemann line 117
  6. theorem OAI.Erdos3.kernelResidue_polynomial_complex_riemann line 146
  7. theorem OAI.Erdos3.principalCoefficientResidue_normalizer_lower line 192
  8. def OAI.Erdos3.principalCoefficientResidueSource line 229
  9. theorem OAI.Erdos3.principalCoefficientResidueSource_primitive line 239
  10. theorem OAI.Erdos3.weights_ext line 250
  11. theorem OAI.Erdos3.residue_one_eq_uniform line 257
  12. theorem OAI.Erdos3.principalSource_baseLaw line 275
  13. theorem OAI.Erdos3.reweight_mass_eq line 281
  14. theorem OAI.Erdos3.reweight_condition_weight line 289
  15. theorem OAI.Erdos3.principalCoefficientResidue_mass_pos line 305
  16. theorem OAI.Erdos3.principalCoefficientResidueSource_law line 329
  17. theorem OAI.Erdos3.principalCoefficientResidueSource_positive_support line 364
  18. theorem OAI.Erdos3.scalarCubeResidueSet_empty_eq_filter line 378
  19. theorem OAI.Erdos3.principalCoefficientResidue_mass_pos_filter line 391
  20. theorem OAI.Erdos3.principalCoefficientResidueSource_law_filter line 411
  21. def OAI.Erdos3.VectorPolynomial.allocatedPrincipalCoefficientResidueSource line 447
  22. theorem OAI.Erdos3.VectorPolynomial.allocatedPrincipalCoefficientResidue_mass_pos line 458
  23. theorem OAI.Erdos3.VectorPolynomial.allocatedPrincipalCoefficientResidueSource_law line 463
  24. theorem OAI.Erdos3.VectorPolynomial.allocatedPrincipalCoefficientResidueSource_primitive line 470
  25. theorem OAI.Erdos3.VectorPolynomial.allocatedPrincipalCoefficientResidueSource_positive_support line 476
  26. theorem OAI.Erdos3.integerScalarCubeWeights_empty_residue_law line 496
  27. theorem OAI.Erdos3.integerScalarCubeWeights_empty_residue_mass_pos line 508
  28. theorem OAI.Erdos3.integerScalarCubeWeights_empty_residue_condition line 516
  29. theorem OAI.Erdos3.integerScalarCubeWeights_empty_residue_l1 line 527
  30. theorem OAI.Erdos3.integerScalarCubeWeights_empty_pi_residue_disintegration line 538
  31. theorem OAI.Erdos3.integerScalarCubeWeights_empty_pi_uniform_residue_error line 564
  32. theorem OAI.Erdos3.originalKernel_residue_slow_quadrature line 609
  33. theorem OAI.Erdos3.integerScalarCubeWeights_empty_pi_residue_disintegration_varying line 663
  34. theorem OAI.Erdos3.integerScalarCubeWeights_empty_pi_uniform_residue_error_varying line 689
  35. theorem OAI.Erdos3.originalKernel_residue_slow_retained_quadrature line 731