Mathematical models

LeanMFG contains rational finite games and real-valued deterministic control problems. Their types carry the probability, admissibility, or regularity conditions used by theorems.

General computational environment

The finite-horizon numerical model uses a general finite-horizon Environment with multidimensional state/action shapes, initial law, population-dependent reward and transition callbacks, and time-indexed policies. It uses native floating-point arrays and runtime validation. The smaller rational and continuous models below retain their proof-carrying interfaces; they do not restrict this computational model.

Static distributions

The generic finite static model supports any finite nonempty action type and a population-dependent reward. It defines expected reward and equilibrium, with a proved adapter for the original three-action game.

The rock-paper-scissors model has three actions and rational mixed strategies. The Distribution structure carries proofs that every probability is nonnegative and the three probabilities sum to one. The representative player's strategy p and population distribution m have the same type but separate roles: a unilateral deviation changes p while m stays fixed.

Finite-state dynamics

The finite-state model defines a rational distribution on any finite type, a policy assigning an action distribution to each state, and normalized stochastic transitions. Its update operator computes the next population law. evolve repeats the update for a sequence of policies. The game also specifies stage and terminal rewards.

See Verification for the conservation proof, which uses the actual update rule.

Continuous control

The deterministic control model uses real-valued time, state, and control. Time ends at 1, dynamics are x' = a, and the running cost is kinetic effort plus an exogenous potential. AdmissiblePath records its initial state, derivative relation, continuity of the control, and integrability of the running cost.

This control problem is a component useful for MFG theory; it does not yet couple a population evolution equation to the HJB equation.