OAI/Combinatorics/Progressions/Sampling/AveragedNormalizedTwistForecastJointModel.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.FiniteProbabilityWeights.forecastAugmented_envelope_tail_le line 13
  2. theorem OAI.Erdos3.FiniteProbabilityWeights.forecastAugmented_envelope_le_on_good line 46
  3. def OAI.Erdos3.forecastCorrelationLinearMap line 63
  4. def OAI.Erdos3.forecastSingleSeminorm line 76
  5. theorem OAI.Erdos3.forecastSingleSeminorm_le line 80
  6. def OAI.Erdos3.forecastFamilySeminorm line 98
  7. theorem OAI.Erdos3.forecastFamilySeminorm_bddAbove line 102
  8. theorem OAI.Erdos3.forecastFamilySeminorm_apply line 112
  9. theorem OAI.Erdos3.forecastFamilySeminorm_le line 120
  10. theorem OAI.Erdos3.forecast_correlation_le_family line 127
  11. theorem OAI.Erdos3.exists_forecast_augmented_model line 138
  12. theorem OAI.Erdos3.forecast_detector_of_atom_approximation line 249
  13. theorem OAI.Erdos3.exists_forecast_augmented_model_of_expansions line 277
  14. theorem OAI.Erdos3.exists_forecast_augmented_native_model_of_expansions line 323
  15. def OAI.Erdos3.forecastAugmentedUnitThreshold line 375
  16. theorem OAI.Erdos3.forecastAugmentedUnitThreshold_bounds line 379
  17. theorem OAI.Erdos3.forecastAugmentedUnitThreshold_source_precision line 423
  18. theorem OAI.Erdos3.forecastAugmentedUnitThreshold_half_source_precision line 431
  19. theorem OAI.Erdos3.forecastAugmentedUnitThreshold_atom_gain line 445
  20. theorem OAI.Erdos3.forecastAugmented_model_error line 478
  21. theorem OAI.Erdos3.forecastAugmented_model_size line 496
  22. theorem OAI.Erdos3.forecastAugmented_separate_source_precision line 527
  23. theorem OAI.Erdos3.forecastAugmented_approximation_precision line 541
  24. theorem OAI.Erdos3.forecastAugmented_model_parameters line 562
  25. theorem OAI.Erdos3.forecastAugmented_model_parameters_bound line 576
  26. theorem OAI.Erdos3.fixedCenterForecast_source_threshold line 598
  27. theorem OAI.Erdos3.fixedCenterForecast_source_threshold_half_le_one line 613
  28. theorem OAI.Erdos3.VectorPolynomial.exists_normalizedTwist_forecast_approximation line 629
  29. theorem OAI.Erdos3.VectorPolynomial.exists_normalizedTwist_forecast_model line 745
  30. theorem OAI.Erdos3.VectorPolynomial.exists_averaged_normalizedTwist_forecast_joint_model line 838