OAI/Combinatorics/Progressions/Estimates/AllocatedExternalCandidateTaggedPairFamily.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.ResidueBoxSlice.fullSlicePoints line 19
  2. theorem OAI.Erdos3.ResidueBoxSlice.fullSlicePointInIntegerBox_injective line 22

    Distinct definitions of this name: OAI/Combinatorics/Progressions/Lattices/DenseResidueScalarScoreNet.lean:258 (same statement text; different proof or body). Qualify references as OAI.Erdos3.ResidueBoxSlice.fullSlicePointInIntegerBox_injective@path.

  3. theorem OAI.Erdos3.ResidueBoxSlice.fullSlicePoints_image_val line 27
  4. theorem OAI.Erdos3.ResidueBoxSlice.fullSlicePoints_nonempty line 32
  5. theorem OAI.Erdos3.ResidueBoxSlice.expect_fullSlicePoints line 37
  6. theorem OAI.Erdos3.ResidueBoxSlice.fullSliceLaw_complexMean_eq_expect_points line 42
  7. theorem OAI.Erdos3.ResidueBoxSlice.fullSliceLaw_mean_eq_expect_points line 48
  8. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.low_residual line 86
  9. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.low_residual_on_slice line 102
  10. def OAI.Erdos3.VectorPolynomial.fullTaggedPhysicalIntegerPoint line 127
  11. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.chartValues_tag_eq_round line 160
  12. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.chartValues_eq_physicalIntegerPoint line 178
  13. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.chartValues_eq_physicalIntegerPoint_on_slice line 187
  14. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.chartValues_eq_physicalIntegerPoint_of_center line 194
  15. def OAI.Erdos3.zeroLayerPhysicalPoint line 216
  16. theorem OAI.Erdos3.fullTaggedPhysicalIntegerPoint_zero_layers line 219
  17. def OAI.Erdos3.zeroLayerSpatialChart line 228
  18. theorem OAI.Erdos3.zeroLayerSpatialChart_support line 231
  19. def OAI.Erdos3.PolynomialPatch.ofZeroLayerShearOrbit line 242
  20. theorem OAI.Erdos3.PolynomialPatch.ofZeroLayerShearOrbit_kernel line 248
  21. theorem OAI.Erdos3.PolynomialPatch.ofZeroLayerShearOrbit_complexity line 253
  22. theorem OAI.Erdos3.PolynomialPatch.ofZeroLayerShearOrbit_value_integer line 258
  23. theorem OAI.Erdos3.PolynomialPatch.exists_zeroLayer_physical_niltest line 281
  24. structure OAI.Erdos3.VectorPolynomial.AllocatedFrozenTaggedContext line 314
  25. def OAI.Erdos3.VectorPolynomial.AllocatedFrozenTaggedContext.sides line 346
  26. structure OAI.Erdos3.VectorPolynomial.AllocatedFrozenTaggedPairInput line 359
  27. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedFrozenTaggedPairInput_fixed_basis_step_drop line 408
  28. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.frozenTaggedContext line 488
  29. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.localLaw_complexMean_eq_fullSliceLaw line 543
  30. def OAI.Erdos3.VectorPolynomial.AllocatedFrozenTaggedPairInput.ofCandidate line 589
  31. theorem OAI.Erdos3.VectorPolynomial.AllocatedFrozenTaggedPairInput.ofCandidate_V_orbit line 652
  32. theorem OAI.Erdos3.VectorPolynomial.AllocatedFrozenTaggedPairInput.ofCandidate_W_orbit line 655
  33. def OAI.Erdos3.VectorPolynomial.AllocatedFrozenTaggedPairInput.ofCandidate_of_localLaw line 660
  34. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.withKeep_localLaw line 736
  35. structure OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateTaggedPairFamily line 745
  36. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateTaggedPairFamily.context line 827
  37. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateTaggedPairFamily.context_sides line 831
  38. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateTaggedPairFamily.chart line 833
  39. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateTaggedPairFamily.candidate line 836
  40. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateTaggedPairFamily.chart_keep line 839
  41. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateTaggedPairFamily.chart_localLaw line 841
  42. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateTaggedPairFamily.input line 844
  43. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateTaggedPairFamily.jointOrbit line 853
  44. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateTaggedPairFamily.input_η line 860
  45. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateTaggedPairFamily.input_θ line 862
  46. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateTaggedPairFamily.input_V_orbit line 864
  47. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateTaggedPairFamily.input_W_orbit line 867
  48. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateTaggedPairFamily.pair_symbol line 873