OAI/Combinatorics/Progressions/Lattices/AllocatedOriginalSampleResidueMixtureForecast.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.forecastInactive_kernel_disintegration line 14
  2. theorem OAI.Erdos3.forecastInactive_indicator_disintegration line 46
  3. theorem OAI.Erdos3.forecastInactive_positiveResidue_mass_sum line 62
  4. def OAI.Erdos3.VectorPolynomial.forecastInactivePhysicalJointKernel line 96
  5. theorem OAI.Erdos3.VectorPolynomial.forecastInactive_physical_fiber_kernel line 105
  6. theorem OAI.Erdos3.VectorPolynomial.forecastInactive_physical_kernel_disintegration line 122
  7. theorem OAI.Erdos3.FiniteProbabilityWeights.condition_complexMean_fiber_apply line 153
  8. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_positiveResidue_disintegration line 164
  9. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_positiveResidue_weighted_disintegration line 186
  10. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_positiveResidue_weighted_error line 200
  11. def OAI.Erdos3.VectorPolynomial.allocatedUnconditionalShortPrincipalLaw line 262
  12. def OAI.Erdos3.VectorPolynomial.allocatedUnconditionalActivePrincipalLaw line 267
  13. def OAI.Erdos3.VectorPolynomial.allocatedPrincipalResidueJoin line 272
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedPrincipalResidueJoin_label_join line 276
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedPrincipalResidue_short_marginal line 287
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedPrincipalResidue_mixture_reconstruct line 297
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedPrincipalResidue_mixture_partition line 310
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedPrincipalResidue_mixture_active_residue line 326
  19. theorem OAI.Erdos3.VectorPolynomial.allocatedPrincipalResidue_mixture_active_uniform line 368
  20. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleForecastSource_active_uniform line 395
  21. theorem OAI.Erdos3.VectorPolynomial.scalarIntegerMean_congr line 454
  22. theorem OAI.Erdos3.VectorPolynomial.allocatedUnconditionalActivePrincipalLaw_integer_mean line 461
  23. theorem OAI.Erdos3.VectorPolynomial.allocatedPrincipal_integer_partition line 475
  24. theorem OAI.Erdos3.VectorPolynomial.allocatedJointLongForecast_residue_decoupling line 527
  25. theorem OAI.Erdos3.VectorPolynomial.allocatedJointLongForecast_weighted_residue_decoupling line 581
  26. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSample_residue_mixture_forecast_comparison line 661