"Functional dependencies" with cardinality constraints
After searching around for paper some more (unfortunately, I found nothing in Ling Liu, M. Tamer Özsu eds. Encyclopedia of Database Systems), I managed to find out that these dependencies are called numerical dependencies. In particular, standard notation for my $\mathcal{A} \rightrightarrows^k \mathcal{B}$ is $\mathcal{A} \xrightarrow{k} \mathcal{B}$, which is also referred to as a $k$-dependency.

Unfortunately, they are not finitely axiomatizable:

John Grant and Jack Minker (1985). Normalization and axiomatization for numerical dependencies. In: Inf. Control 65(1), pp. 1-17. https://doi.org/10.1016/S0019-9958(85)80017-6

The entailment problem is in EXPSPACE. However, there is a sound branch-and-bound algorithm that may be used: 

Paolo Ciaccia, Matteo Golfarelli and Stefano Rizzi (2013). Efficient derivation of numerical dependencies. In: Inf. Syst. 38(3) pp. 410-429. https://doi.org/10.1016/j.is.2012.07.007

A general survey of the generalization of functional dependencies is

Loredana Caruccio, Vincenzo Deufemia and Giuseppe Polese (2016). Relaxed Functional Dependencies—A Survey of Approaches. In: IEEE Tran. Knowl. Data Eng. 28(1) pp. 147-165. https://doi.org/10.1109/TKDE.2015.2472010

An extension of numerical dependencies is $\mathit{CFD}^c$, conditional functional dependencies with cardinality constraints. This paper defines them, and gives some algorithms for satisfiability and entailment:

Wenguang Chen, Wenfei Fan and Shuai Ma (2009). Incorporating cardinality constraints and synonym rules into conditional functional dependencies. In: Inf. Process. Lett. 109(14) pp. 783-789. https://doi.org/10.1016/j.ipl.2009.03.021