OAI/Combinatorics/Progressions/Lattices/AllocatedResidueInterpolationMixture.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.principalSupportedCoordinateWeights line 21
  2. theorem OAI.Erdos3.principalSupportedResidueWeights_eq_pi line 34
  3. theorem OAI.Erdos3.principalSupportedResiduePMF_eq_product line 40
  4. def OAI.Erdos3.principalSupportedAxisTuplePMF line 46
  5. theorem OAI.Erdos3.principalSupportedResidue_full_axis_law line 50
  6. theorem OAI.Erdos3.principalSupportedResidue_selected_axis_law line 59
  7. theorem OAI.Erdos3.scalarCubeResidue_fiber_eq line 80
  8. theorem OAI.Erdos3.principalSupportedResidue_marginal line 96
  9. def OAI.Erdos3.principalSupportedAxisSources line 135
  10. theorem OAI.Erdos3.principalSupportedAxisSources_primitive line 143
  11. theorem OAI.Erdos3.principalSupportedResidue_axis_marginal line 151
  12. theorem OAI.Erdos3.principalSupportedResidue_axis_integer_law line 164
  13. theorem OAI.Erdos3.principalSupportedResidue_axis_jet_sum_law line 177
  14. def OAI.Erdos3.principalSupportedAxisWeights line 212
  15. theorem OAI.Erdos3.principalSupportedResidueWeights_partition_weight line 222
  16. theorem OAI.Erdos3.principalSupportedResidueWeights_partition line 231
  17. theorem OAI.Erdos3.principalSupportedResidueWeights_partition_mul line 240
  18. theorem OAI.Erdos3.principalSupportedAxisWeights_eq_residueWeights line 252
  19. def OAI.Erdos3.VectorPolynomial.allocatedActiveResidueSources line 296
  20. theorem OAI.Erdos3.VectorPolynomial.allocatedActiveResidueSources_length line 306
  21. theorem OAI.Erdos3.VectorPolynomial.allocatedActiveResidueSources_primitive line 311
  22. theorem OAI.Erdos3.VectorPolynomial.allocatedActiveResidueSources_jet_sum_law line 321
  23. theorem OAI.Erdos3.VectorPolynomial.allocatedActiveResidueSources_coeff_jet_law line 386
  24. def OAI.Erdos3.VectorPolynomial.allocatedSupportedResidueJetPMF line 474
  25. theorem OAI.Erdos3.VectorPolynomial.allocatedSupportedResidueJetPMF_source line 483
  26. theorem OAI.Erdos3.VectorPolynomial.allocatedSupportedResidueJetPMF_constant_mixture line 498
  27. theorem OAI.Erdos3.VectorPolynomial.allocatedResidueInterpolation_constant_mixture line 578
  28. theorem OAI.Erdos3.VectorPolynomial.allocatedNormalizedResidueInterpolation_constant_mixture line 597