OAI/Combinatorics/Progressions/Estimates/AllocatedExternalCandidateAxisFreezingConclusion.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.keptInclusion line 36
  2. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.axisSlice line 38
  3. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.axisPoint line 44
  4. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.axisFixed line 47
  5. abbrev OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.freezeAxes line 53
  6. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.freezeAxes_path line 74
  7. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.freezeAxes_centerLift line 77
  8. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.freezeAxes_parameter line 80
  9. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.freezeAxes_physical line 91
  10. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.freezeAxes_chartValues line 97
  11. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.axisPolynomial line 107
  12. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.axisPolynomial_support line 110
  13. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.axisPolynomial_eval line 118
  14. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.axisPoint_mem line 125
  15. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.axisCoordinateEquiv line 135
  16. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.axisSlice_expect line 142
  17. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.axisOrbit line 175
  18. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.axisOrbit_eval line 180
  19. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.freezeAxes line 190
  20. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.freezeAxes_value line 197
  21. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.freezeAxes_score line 204
  22. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.freezeAxesScore line 212
  23. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.exists_freezeAxes line 216
  24. abbrev OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.restrictAxes line 276
  25. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.restrictAxes_path line 293
  26. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.restrictAxes_centerLift line 296
  27. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.restrictAxes_parameter line 299
  28. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.restrictAxes_physical line 304
  29. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.restrictAxes_chartValues line 309
  30. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.axisSlice_complexMean line 314
  31. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.restrictAxes line 347
  32. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.restrictAxes_value line 354
  33. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.localLaw_complexMean_parameter_value line 362
  34. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.restrictAxes_complexMean line 370
  35. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.exists_restrictAxes_norm line 380
  36. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.exists_restrictAxes_site_norm line 398
  37. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.axisPolynomial_top_independent line 453
  38. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.pairOrbitSymbol_axisPolynomial_independent line 475
  39. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.pairOrbitSymbol_axisOrbit_independent line 510
  40. structure OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.AxisFreezing line 570
  41. abbrev OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.AxisFreezing.problem line 587
  42. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.AxisFreezing.problem_productive line 611
  43. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.AxisFreezing.problem_centerLift line 613
  44. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.AxisFreezing.problem_chart line 615
  45. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.AxisFreezing.problem_chart_keep line 619
  46. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.AxisFreezing.problem_slice_dense line 622
  47. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.AxisFreezing.problem_slice_length line 629
  48. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.AxisFreezing.problem_slice_length_lower line 635
  49. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.AxisFreezing.problem_candidate line 642
  50. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.AxisFreezing.problem_score_mono line 646
  51. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.AxisFreezing.problem_slice_inside line 651
  52. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.exists_axisFreezing line 661
  53. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.thresholdKeep line 680
  54. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.exists_thresholdAxisFreezing line 683
  55. theorem OAI.Erdos3.ResidueBoxSlice.integerPoints_classical_eq line 704
  56. theorem OAI.Erdos3.isDenseCommonStrideBox_classical_iff line 712
  57. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.AxisFreezing.extendSlice line 763
  58. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.AxisFreezing.ambientScore_extendSlice line 768
  59. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.AxisFreezing.extendSlice_dense line 796
  60. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.AxisFreezing.extendSlice_inside line 814
  61. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.AxisFreezing.conclusion_subset line 837
  62. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.AxisFreezing.conclusion line 841