OAI/Combinatorics/Progressions/Estimates/AntisymmetricPairVerticalModel.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.exists_antisymmetric_pair_outer_control line 20
  2. theorem OAI.Erdos3.NativeSampleCorrelation.antisymmetricPairPolynomialMap_coefficient line 100
  3. theorem OAI.Erdos3.NativePolynomialOrbitFactors.pair_projected_product line 119
  4. theorem OAI.Erdos3.NativePolynomialOrbitFactors.pair_eval_component line 129
  5. theorem OAI.Erdos3.NativePolynomialOrbitFactors.pair_projected_middle_zero line 146
  6. theorem OAI.Erdos3.NativePolynomialOrbitFactors.pair_projected_rational_zero line 151
  7. theorem OAI.Erdos3.NativePolynomialOrbitFactors.pair_projected_top_agreement line 156
  8. theorem OAI.Erdos3.NativePolynomialOrbitFactors.pair_projected_bracket_agreement line 166
  9. theorem OAI.Erdos3.NativePolynomialOrbitFactors.pair_first_layer_bracket_agreement line 181
  10. theorem OAI.Erdos3.NativeSampleCorrelation.antisymmetricPairPolynomialMap_value line 221
  11. theorem OAI.Erdos3.NativePolynomialOrbitFactors.pairFrozenVector_diagonal line 243
  12. theorem OAI.Erdos3.NativePolynomialOrbitFactors.hasPairFrozenEquivalence_mono line 282
  13. def OAI.Erdos3.NativePolynomialOrbitFactors.HasPairFrozenReduction line 287
  14. theorem OAI.Erdos3.NativePolynomialOrbitFactors.hasPairFrozenReduction_mono line 290
  15. theorem OAI.Erdos3.NativePolynomialOrbitFactors.pairFrozenEquivalence_at line 295
  16. theorem OAI.Erdos3.exists_antisymmetric_pair_frozen_reduction line 305
  17. def OAI.Erdos3.NativePolynomialOrbitFactors.HasPairLocalApproximation line 370
  18. theorem OAI.Erdos3.NativePolynomialOrbitFactors.hasPairLocalApproximation_mono line 379
  19. theorem OAI.Erdos3.NativePolynomialOrbitFactors.pairFrozenVector_error line 392
  20. theorem OAI.Erdos3.exists_antisymmetric_pair_local_approximation line 442
  21. def OAI.Erdos3.NativePolynomialOrbitFactors.pairAnchoredVector line 545
  22. theorem OAI.Erdos3.NativePolynomialOrbitFactors.pairAnchoredVector_norm line 549
  23. theorem OAI.Erdos3.NativePolynomialOrbitFactors.select_pair_local_partition line 553
  24. theorem OAI.Erdos3.exists_antisymmetric_pair_local_partition line 629
  25. theorem OAI.Erdos3.NativePolynomialOrbitFactors.pairCoordinate_common_vertical line 749
  26. theorem OAI.Erdos3.NativePolynomialOrbitFactors.pairCoordinate_comparison_invariant line 786
  27. theorem OAI.Erdos3.exists_antisymmetric_anchor_equivalence line 811
  28. def OAI.Erdos3.NativePolynomialOrbitFactors.FrozenMiddleRealization.pairMiddleTest line 946
  29. theorem OAI.Erdos3.NativePolynomialOrbitFactors.FrozenMiddleRealization.pairMiddleTest_eval line 952
  30. theorem OAI.Erdos3.NativePolynomialOrbitFactors.FrozenMiddleRealization.pairMiddleTest_unit line 957
  31. theorem OAI.Erdos3.NativePolynomialOrbitFactors.FrozenMiddleRealization.pairMiddleTest_complexity line 963
  32. theorem OAI.Erdos3.NativePolynomialOrbitFactors.FrozenMiddleRealization.pairMiddleTest_common_vertical line 972
  33. theorem OAI.Erdos3.exists_antisymmetric_pair_middle_model line 1017
  34. def OAI.Erdos3.pairMiddleVerticalBudget line 1124
  35. def OAI.Erdos3.NativePolynomialOrbitFactors.pairMiddleFrequency line 1138
  36. theorem OAI.Erdos3.NativePolynomialOrbitFactors.pairMiddleFrequency_real line 1143
  37. theorem OAI.Erdos3.NativePolynomialOrbitFactors.FrozenMiddleRealization.pairMiddleFrequency_height line 1168
  38. theorem OAI.Erdos3.NativePolynomialOrbitFactors.FrozenMiddleRealization.pairMiddleFrequency_integral line 1183
  39. def OAI.Erdos3.NativePolynomialOrbitFactors.FrozenMiddleRealization.pairMiddleVertical line 1199
  40. theorem OAI.Erdos3.NativePolynomialOrbitFactors.FrozenMiddleRealization.pairMiddleVertical_eval line 1232