MWU configuration state

MWUConfig C carries a strictly-positive weight vector and its potential (the sum of the weights). The initial state sets all weights to 1; toPMF normalizes the weights to a FintypePMF distribution. These are the structural primitives consumed by the multiplicative-weights update and analysis in later shards.

structure ProbabilityTheory.MWUConfig (C : Type u_1) [Fintype C] : Type u_1

Multiplicative-weights-update state: a strictly-positive weight vector.

• weights : C → ℝ

  The weight assigned to each column.

• weights_pos (c : C) : 0 < self.weights c

  Weights are strictly positive.

def ProbabilityTheory.MWUConfig.potential {C : Type u_1} [Fintype C] (cfg : MWUConfig C) : ℝ

The potential of an MWU state is the sum of its weights.

Equations

• cfg.potential = ∑ c : C, cfg.weights c

theorem ProbabilityTheory.MWUConfig.potential_pos {C : Type u_1} [Fintype C] [Nonempty C] (cfg : MWUConfig C) : 0 < cfg.potential

def ProbabilityTheory.mwuInit (C : Type u_1) [Fintype C] : MWUConfig C

Initial configuration: all weights equal to 1.

Equations

• ProbabilityTheory.mwuInit C = { weights := fun (x : C) => 1, weights_pos := ⋯ }

theorem ProbabilityTheory.mwuInit_potential (C : Type u_1) [Fintype C] : (mwuInit C).potential = ↑(Fintype.card C)

noncomputable def ProbabilityTheory.MWUConfig.toPMF {C : Type u_1} [Fintype C] [Nonempty C] (cfg : MWUConfig C) : FintypePMF C

Normalize an MWU configuration to a FintypePMF.

Equations

• cfg.toPMF = ProbabilityTheory.FintypePMF.normalize cfg.weights ⋯