Individual-weight tracking for MWU

Tracks each column's weight through the T-round run. The hit counter mwuHitCount T c records the number of rounds t < T in which column c was hit by the selected row. The weight of c after T rounds is exactly (1 - η)^(hitCount T c).

Declarations here are internal infrastructure for the MWU analysis (shared across the ApproxMinimax headline proof) and not intended as standalone API.

def ProbabilityTheory.mwuHitCount {R : Type u_1} {C : Type u_2} [Fintype R] [Fintype C] [Nonempty C] (M : R → C → Bool) (η : ℝ) (hη1 : η < 1) (v : ℝ) (hrow : ∀ (q : FintypePMF C), ∃ (r : R), v ≤ ∑ c : C, q.prob c * if M r c = true then 1 else 0) (T : ℕ) : C → ℕ

Number of rounds (in the first T) in which column c was hit by the selected row.

Equations

• ProbabilityTheory.mwuHitCount M η hη1 v hrow 0 x✝ = 0
• ProbabilityTheory.mwuHitCount M η hη1 v hrow T.succ x✝ = ProbabilityTheory.mwuHitCount M η hη1 v hrow T x✝ + if M ⋯.choose x✝ = true then 1 else 0

theorem ProbabilityTheory.weight_le_potential {C : Type u_1} [Fintype C] (cfg : MWUConfig C) (c : C) : cfg.weights c ≤ cfg.potential

A single weight is bounded above by the configuration's total potential.

theorem ProbabilityTheory.mwu_weight_eq_pow_hitCount {R : Type u_1} {C : Type u_2} [Fintype R] [Fintype C] [Nonempty C] (M : R → C → Bool) (η : ℝ) (hη1 : η < 1) (v : ℝ) (hrow : ∀ (q : FintypePMF C), ∃ (r : R), v ≤ ∑ c : C, q.prob c * if M r c = true then 1 else 0) (T : ℕ) (c : C) : (mwuConfig M η hη1 v hrow T).weights c = (1 - η) ^ mwuHitCount M η hη1 v hrow T c

Individual-weight closed form: after T rounds, weights c = (1 - η)^(hitCount T c).

theorem ProbabilityTheory.mwuHitCount_eq_sum_indicator {R : Type u_1} {C : Type u_2} [Fintype R] [Fintype C] [Nonempty C] (M : R → C → Bool) (η : ℝ) (hη1 : η < 1) (v : ℝ) (hrow : ∀ (q : FintypePMF C), ∃ (r : R), v ≤ ∑ c : C, q.prob c * if M r c = true then 1 else 0) (T : ℕ) (c : C) : ↑(mwuHitCount M η hη1 v hrow T c) = ∑ t : Fin T, if M (mwuRows M η hη1 v hrow T t) c = true then 1 else 0

The hit counter agrees with the sum of Boolean indicators over the row sequence.