OAI/Combinatorics/Progressions/Estimates/AllocatedExternalCandidateOptionJointConclusion.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart line 31
  2. abbrev OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.Variables line 54
  3. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.integerChart line 56
  4. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.chartValues line 60
  5. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.parameter line 63
  6. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.parameter_mem line 66
  7. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.physical line 71
  8. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.site line 74
  9. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.physical_eq_sampler line 78
  10. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.integerChart_support line 82
  11. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.integerChart_spatial line 88
  12. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.chartValues_spatial line 93
  13. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.slice_parameter_mem line 97
  14. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.slice_index line 101
  15. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.path_support line 106
  16. structure OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate line 119
  17. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.value line 132
  18. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.score line 136
  19. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.mark_integerPoint line 141
  20. theorem OAI.Erdos3.ResidueBoxSlice.length_gt_of_dense_exp_side line 162
  21. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.slice_length_gt_of_dense_side line 204
  22. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.slice_length_gt_of_dense_cutoff line 214
  23. structure OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem line 263
  24. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.ambientScore line 279
  25. structure OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Conclusion line 287
  26. theorem OAI.Erdos3.VectorPolynomial.allocatedExternalLocal_mark_of_formal line 342
  27. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.ofFormalMark line 365
  28. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialOrbitIntegerChart_eval line 385
  29. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.optionJointLocalOrbits line 441
  30. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.optionJointLocalOrbits_none line 450
  31. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.optionJointLocalOrbits_some line 454
  32. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.optionJointMarkedOrbits line 460
  33. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.optionJoint line 466
  34. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.optionJoint_orbit line 504
  35. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.optionJoint_value_projection line 509
  36. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.optionJoint_score line 515
  37. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.changeTargetFiltration line 562
  38. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.changeTargetFiltration_orbit line 571
  39. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.changeTargetFiltration_value line 574
  40. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.changeTargetFiltration_score line 577
  41. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.optionJoint line 633
  42. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.optionJoint_productive line 653
  43. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.optionJoint_chart line 655
  44. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.optionJoint_candidate_orbit line 658
  45. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.onPaths line 663
  46. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.onPaths_productive line 677
  47. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.conclusion_of_onPaths line 681
  48. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.optionJoint_ambientScore line 752
  49. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.conclusion_of_optionJoint line 762
  50. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.conclusion_of_optionJoint_ambient line 780
  51. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.conclusion_of_optionJoint_retained line 785
  52. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.conclusion_of_optionJoint_step line 789
  53. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.conclusion_of_optionJoint_slice line 794