OAI/Combinatorics/Progressions/Sampling/MarkedKernelProjectionScoreRestoration.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.integral_threshold_indicator_lower line 17
  2. theorem OAI.Erdos3.exists_common_translation_retained_scores line 44
  3. def OAI.Erdos3.FiniteProbabilityWeights.finiteScore line 101
  4. theorem OAI.Erdos3.FiniteProbabilityWeights.finiteScore_measurable line 106
  5. theorem OAI.Erdos3.FiniteProbabilityWeights.finiteScore_integrable line 112
  6. theorem OAI.Erdos3.FiniteProbabilityWeights.finiteScore_abs_le line 120
  7. theorem OAI.Erdos3.FiniteProbabilityWeights.finiteScore_le line 131
  8. theorem OAI.Erdos3.FiniteProbabilityWeights.integral_finiteScore line 137
  9. theorem OAI.Erdos3.FiniteProbabilityWeights.finiteScore_probability_data line 148
  10. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.exists_kernelProjection_common_translation line 183
  11. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.exists_kernelProjection_restored_orbit line 225
  12. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.exists_external_kernelProjection_common_translation line 272
  13. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.exists_external_kernelProjection_restored_orbit line 316
  14. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialOrbitRealEval_constantGroupOrbit line 359
  15. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.exists_kernelProjection_marked_restored_orbit line 379