OAI/Combinatorics/Progressions/Lattices/NativeIntegerAffinePullbackHom.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Erdos3.NativeIntegerModelFamily line 12
  2. def OAI.Erdos3.NativeIntegerModelFamily.mono line 37
  3. theorem OAI.Erdos3.NativeIntegerModelFamily.mono_dim line 41
  4. structure OAI.Erdos3.NativeIntegerExpansion line 56
  5. def OAI.Erdos3.NativeIntegerExpansion.mono line 86
  6. def OAI.Erdos3.NativeIntegerExpansion.conjugate line 93
  7. def OAI.Erdos3.NativeIntegerExpansion.ofTest line 106
  8. def OAI.Erdos3.NativeIntegerExpansion.ofModelFamily line 125
  9. theorem OAI.Erdos3.NativeIntegerExpansion.select_sample_correlation line 146
  10. theorem OAI.Erdos3.NativeIntegerExpansion.norm_eval_le line 190
  11. def OAI.Erdos3.NativeIntegerExpansion.ofFamily line 219
  12. def OAI.Erdos3.NativeIntegerExpansion.weightedSum line 244
  13. def OAI.Erdos3.NativeIntegerExpansion.affinePullback line 287
  14. def OAI.Erdos3.NativeIntegerExpansion.toCyclic line 298
  15. def OAI.Erdos3.NativeIntegerExpansion.cyclicAffinePullback line 312
  16. def OAI.Erdos3.NativeIntegerExpansion.scaleNormLeOne line 333
  17. def OAI.Erdos3.NativeIntegerExpansion.substitutedValue line 366
  18. def OAI.Erdos3.NativeIntegerExpansion.substituteExpansion line 371
  19. theorem OAI.Erdos3.NativeIntegerExpansion.substitutedValue_eq line 379
  20. def OAI.Erdos3.halvingPolynomial line 394
  21. theorem OAI.Erdos3.halvingPolynomial_support line 397
  22. theorem OAI.Erdos3.halvingPolynomial_eval line 406
  23. structure OAI.Erdos3.NativeIntegerVectorEquivalence line 426
  24. theorem OAI.Erdos3.NativeIntegerVectorEquivalence.mono line 438
  25. theorem OAI.Erdos3.NativeIntegerVectorEquivalence.symm line 446
  26. theorem OAI.Erdos3.NativeIntegerVectorEquivalence.conjugate line 456
  27. theorem OAI.Erdos3.NativeIntegerVectorEquivalence.affinePullback line 467
  28. theorem OAI.Erdos3.NativeIntegerVectorEquivalence.cyclicAffinePullback line 477
  29. def OAI.Erdos3.NativeIntegerVectorEquivalence.selectedExpansion line 508
  30. theorem OAI.Erdos3.NativeIntegerVectorEquivalence.transfer_sample_correlation line 513
  31. def OAI.Erdos3.NativeIntegerExpansion.linearPullbackHom line 559
  32. theorem OAI.Erdos3.NativeIntegerVectorEquivalence.linearPullbackHom line 574
  33. theorem OAI.Erdos3.NativeIntegerVectorEquivalence.coordinatePullback line 585
  34. theorem OAI.Erdos3.NativeIntegerVectorEquivalence.selectedChoice_card_bound line 604
  35. theorem OAI.Erdos3.NativeIntegerVectorEquivalence.selectedChainedChoice_card_bound line 616
  36. theorem OAI.Erdos3.NativeIntegerVectorEquivalence.affinePullbackHom line 643