OAI/Combinatorics/Progressions/Lattices/DenseResidueScalarScoreNet.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Erdos3.DenseResidueSliceNetCode line 12
  2. def OAI.Erdos3.DenseResidueSliceNetCode.stride line 19
  3. def OAI.Erdos3.DenseResidueSliceNetCode.start line 21
  4. def OAI.Erdos3.DenseResidueSliceNetCode.length line 24
  5. def OAI.Erdos3.DenseResidueSliceNetCode.Valid line 27
  6. def OAI.Erdos3.DenseResidueSliceNetCode.fullParent line 32
  7. def OAI.Erdos3.DenseResidueSliceNetCode.realize line 37
  8. theorem OAI.Erdos3.DenseResidueSliceNetCode.realize_spec line 43
  9. theorem OAI.Erdos3.DenseResidueSliceNetCode.card line 60
  10. def OAI.Erdos3.DenseResidueSliceNetCode.meshCode line 67
  11. theorem OAI.Erdos3.DenseResidueSliceNetCode.meshCode_valid line 82
  12. theorem OAI.Erdos3.DenseResidueSliceNetCode.realize_meshCode line 101
  13. theorem OAI.Erdos3.DenseResidueSliceNetCode.exists_realize_meshRounded line 111
  14. theorem OAI.Erdos3.denseResidueCode_card_exp_bound line 134
  15. theorem OAI.Erdos3.exists_denseResidueScalarNet_power_budget line 152
  16. def OAI.Erdos3.ResidueBoxSlice.fullSliceSupport line 255
  17. theorem OAI.Erdos3.ResidueBoxSlice.fullSlicePointInIntegerBox_injective line 258

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

  18. theorem OAI.Erdos3.ResidueBoxSlice.fullSliceSupport_card line 270
  19. theorem OAI.Erdos3.ResidueBoxSlice.fullSliceSupport_nonempty line 276
  20. theorem OAI.Erdos3.ResidueBoxSlice.fullSliceLaw_mean_eq_support line 281
  21. theorem OAI.Erdos3.ResidueBoxSlice.fullSliceSupport_subset line 287
  22. theorem OAI.Erdos3.ResidueBoxSlice.fullSliceLaw_mean_sub_le_of_coordinate_deficit line 313
  23. theorem OAI.Erdos3.ResidueBoxSlice.fullSliceLaw_mean_sub_le_of_length_loss line 340
  24. theorem OAI.Erdos3.fullSliceLaw_sigma_congr line 370
  25. theorem OAI.Erdos3.exists_denseResidueSliceLaw_net line 378
  26. theorem OAI.Erdos3.exists_denseResidueScalarScore_net line 452