OAI/Combinatorics/Progressions/Estimates/MixedPairPartitionPrecision.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.NativePolynomialOrbitFactors.mixedPairAnchoredVector line 29
  2. def OAI.Erdos3.NativePolynomialOrbitFactors.HasMixedPairLocalApproximation line 33
  3. theorem OAI.Erdos3.NativePolynomialOrbitFactors.hasMixedPairLocalApproximation_mono line 42
  4. theorem OAI.Erdos3.NativePolynomialOrbitFactors.mixedPairFrozenVector_diagonal line 55
  5. theorem OAI.Erdos3.NativePolynomialOrbitFactors.mixedPairFrozenVector_error line 69
  6. theorem OAI.Erdos3.exists_mixed_pair_local_approximation line 115
  7. theorem OAI.Erdos3.NativePolynomialOrbitFactors.hasMixedPairFrozenEquivalence_mono line 223
  8. def OAI.Erdos3.NativePolynomialOrbitFactors.HasMixedPairFrozenReduction line 228
  9. theorem OAI.Erdos3.NativePolynomialOrbitFactors.hasMixedPairFrozenReduction_mono line 231
  10. theorem OAI.Erdos3.NativePolynomialOrbitFactors.mixedPairFrozenEquivalence_at line 236
  11. theorem OAI.Erdos3.exists_mixed_pair_frozen_reduction line 246
  12. def OAI.Erdos3.mixedPairPartitionErrorBudget line 303
  13. theorem OAI.Erdos3.NativePolynomialOrbitFactors.mixedPairAnchoredVector_norm line 316
  14. theorem OAI.Erdos3.NativePolynomialOrbitFactors.select_mixed_pair_local_partition line 320
  15. theorem OAI.Erdos3.exists_mixed_pair_local_partition line 386
  16. structure OAI.Erdos3.NativeMixedPairPartition line 518
  17. def OAI.Erdos3.NativeMixedPairPartition.mono line 542
  18. theorem OAI.Erdos3.exists_mixed_pair_precise_partition line 555