OAI/Combinatorics/Progressions/Estimates/NativeMixedReflectionBridge.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.mixedSlotInput line 10
  2. theorem OAI.Erdos3.mixedSlotInput_update line 13
  3. def OAI.Erdos3.mixedExchangeCoordinate line 29
  4. def OAI.Erdos3.mixedReflectionLinear line 32
  5. def OAI.Erdos3.mixedReflectionOffset line 40
  6. def OAI.Erdos3.mixedReflectionAffineInput line 44
  7. theorem OAI.Erdos3.mixedReflectionAffineInput_none line 48
  8. theorem OAI.Erdos3.mixedReflectionAffineInput_some line 52
  9. theorem OAI.Erdos3.mixedReflectionInput_sum line 65
  10. theorem OAI.Erdos3.mixedReflectionInput_left line 73
  11. theorem OAI.Erdos3.mixedReflectionInput_right line 79
  12. theorem OAI.Erdos3.exists_separated_sample_correlation line 99
  13. def OAI.Erdos3.NativeMultidegreeNilcharacter.mixedReflectionSource line 174
  14. def OAI.Erdos3.NativeMultidegreeNilcharacter.mixedReflectionTarget line 180
  15. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_mixed_reflected_factor_equivalence line 189
  16. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_mixed_reflected_pair_equivalence line 236
  17. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixed_reflection_target_unit line 264
  18. theorem OAI.Erdos3.exists_separated_family_correlation line 293
  19. def OAI.Erdos3.NativeMultidegreeNilcharacter.mixedAntisymmetric line 411
  20. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_mixed_reflection_weights line 417
  21. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_mixed_antisymmetric_family line 479
  22. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_mixed_separated_correlation line 544
  23. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_mixed_sum_antisymmetric_correlation line 612