def MultiplicativeWeights.countRounds (P : ℕ → Prop) [DecidablePred P] (t : ℕ) : ℕ

def MultiplicativeWeights.expertMistakes {n : ℕ} (wrong : Fin n → ℕ → Prop) [(i : Fin n) → (t : ℕ) → Decidable (wrong i t)] (i : Fin n) (t : ℕ) : ℕ

def MultiplicativeWeights.weight {n : ℕ} (wrong : Fin n → ℕ → Prop) [(i : Fin n) → (t : ℕ) → Decidable (wrong i t)] (ε : ℝ) (i : Fin n) (t : ℕ) : ℝ

def MultiplicativeWeights.Φ {n : ℕ} (wrong : Fin n → ℕ → Prop) [(i : Fin n) → (t : ℕ) → Decidable (wrong i t)] (ε : ℝ) (t : ℕ) : ℝ

def MultiplicativeWeights.algWrongAt {n : ℕ} (wrong : Fin n → ℕ → Prop) [(i : Fin n) → (t : ℕ) → Decidable (wrong i t)] (ε : ℝ) (k : ℕ) : Prop

noncomputable def MultiplicativeWeights.algMistakes {n : ℕ} (wrong : Fin n → ℕ → Prop) [(i : Fin n) → (t : ℕ) → Decidable (wrong i t)] (ε : ℝ) (t : ℕ) : ℕ

theorem MultiplicativeWeights.countRounds_succ (P : ℕ → Prop) [DecidablePred P] (t : ℕ) : countRounds P (t + 1) = countRounds P t + if P t then 1 else 0

theorem MultiplicativeWeights.weight_succ {n : ℕ} (wrong : Fin n → ℕ → Prop) [(i : Fin n) → (t : ℕ) → Decidable (wrong i t)] (ε : ℝ) (i : Fin n) (k : ℕ) : weight wrong ε i (k + 1) = weight wrong ε i k * if wrong i k then 1 - ε else 1

theorem MultiplicativeWeights.Φ_zero {n : ℕ} (wrong : Fin n → ℕ → Prop) [(i : Fin n) → (t : ℕ) → Decidable (wrong i t)] (ε : ℝ) : Φ wrong ε 0 = ↑n

theorem MultiplicativeWeights.Φ_step {n : ℕ} (wrong : Fin n → ℕ → Prop) [(i : Fin n) → (t : ℕ) → Decidable (wrong i t)] (ε : ℝ) (k : ℕ) : Φ wrong ε (k + 1) = Φ wrong ε k - ε * ∑ i : Fin n with wrong i k, weight wrong ε i k

theorem MultiplicativeWeights.Φ_drop_on_mistake {n : ℕ} (wrong : Fin n → ℕ → Prop) [(i : Fin n) → (t : ℕ) → Decidable (wrong i t)] {ε : ℝ} (hε_pos : 0 < ε) (_hε_lt : ε < 1) (k : ℕ) (hmistake : algWrongAt wrong ε k) : Φ wrong ε (k + 1) ≤ (1 - ε / 2) * Φ wrong ε k

theorem MultiplicativeWeights.Φ_nonincreasing {n : ℕ} (wrong : Fin n → ℕ → Prop) [(i : Fin n) → (t : ℕ) → Decidable (wrong i t)] {ε : ℝ} (hε_pos : 0 < ε) (hε_lt : ε < 1) (k : ℕ) : Φ wrong ε (k + 1) ≤ Φ wrong ε k

theorem MultiplicativeWeights.Φ_upper_bound {n : ℕ} (wrong : Fin n → ℕ → Prop) [(i : Fin n) → (t : ℕ) → Decidable (wrong i t)] {ε : ℝ} (hε_pos : 0 < ε) (hε_lt : ε < 1) (T : ℕ) : Φ wrong ε T ≤ ↑n * (1 - ε / 2) ^ algMistakes wrong ε T

theorem MultiplicativeWeights.Φ_lower_bound {n : ℕ} (wrong : Fin n → ℕ → Prop) [(i : Fin n) → (t : ℕ) → Decidable (wrong i t)] {ε : ℝ} (hε_lt : ε < 1) (i : Fin n) (t : ℕ) : weight wrong ε i t ≤ Φ wrong ε t

theorem MultiplicativeWeights.log_one_sub_half_eps_le {ε : ℝ} (hε_lt : ε < 2) : Real.log (1 - ε / 2) ≤ -ε / 2

theorem MultiplicativeWeights.neg_log_one_sub_le {ε : ℝ} (hε_pos : 0 < ε) (hε_le : ε ≤ 1 / 2) : -Real.log (1 - ε) ≤ ε + ε ^ 2

theorem MultiplicativeWeights.potential_inequality {n : ℕ} (wrong : Fin n → ℕ → Prop) [(i : Fin n) → (t : ℕ) → Decidable (wrong i t)] {ε : ℝ} (hε_pos : 0 < ε) (hε_lt : ε < 1) (i : Fin n) (T : ℕ) : (1 - ε) ^ expertMistakes wrong i T ≤ ↑n * (1 - ε / 2) ^ algMistakes wrong ε T

theorem MultiplicativeWeights.regret_bound_from_potential {n : ℕ} (hn : 0 < n) {ε : ℝ} (hε_pos : 0 < ε) (hε_le : ε ≤ 1 / 2) {m mᵢ : ℕ} (hpot : (1 - ε) ^ mᵢ ≤ ↑n * (1 - ε / 2) ^ m) : ↑m ≤ 2 * Real.log ↑n / ε + 2 * (1 + ε) * ↑mᵢ

theorem MultiplicativeWeights.weighted_majority_regret_bound {n : ℕ} (hn : 0 < n) (wrong : Fin n → ℕ → Prop) [(i : Fin n) → (t : ℕ) → Decidable (wrong i t)] {ε : ℝ} (hε_pos : 0 < ε) (hε_le : ε ≤ 1 / 2) (i : Fin n) (T : ℕ) : ↑(algMistakes wrong ε T) ≤ 2 * Real.log ↑n / ε + 2 * (1 + ε) * ↑(expertMistakes wrong i T)

def MultiplicativeWeights.generalWeight {n : ℕ} {P : Type u_1} (M : Fin n → P → ℝ) (ρ ε : ℝ) (outcomes : ℕ → P) (i : Fin n) : ℕ → ℝ

noncomputable def MultiplicativeWeights.generalΦ {n : ℕ} {P : Type u_1} (M : Fin n → P → ℝ) (ρ ε : ℝ) (outcomes : ℕ → P) (t : ℕ) : ℝ

noncomputable def MultiplicativeWeights.expertProb {n : ℕ} {P : Type u_1} (M : Fin n → P → ℝ) (ρ ε : ℝ) (outcomes : ℕ → P) (i : Fin n) (t : ℕ) : ℝ

noncomputable def MultiplicativeWeights.expectedPenalty {n : ℕ} {P : Type u_1} (M : Fin n → P → ℝ) (ρ ε : ℝ) (outcomes : ℕ → P) (t : ℕ) : ℝ

noncomputable def MultiplicativeWeights.totalExpectedPenalty {n : ℕ} {P : Type u_1} (M : Fin n → P → ℝ) (ρ ε : ℝ) (outcomes : ℕ → P) (T : ℕ) : ℝ

noncomputable def MultiplicativeWeights.totalNonnegPenalty {n : ℕ} {P : Type u_1} (M : Fin n → P → ℝ) (outcomes : ℕ → P) (i : Fin n) (T : ℕ) : ℝ

noncomputable def MultiplicativeWeights.totalNegPenalty {n : ℕ} {P : Type u_1} (M : Fin n → P → ℝ) (outcomes : ℕ → P) (i : Fin n) (T : ℕ) : ℝ

def MultiplicativeWeights.totalExpertPenalty {n : ℕ} {P : Type u_1} (M : Fin n → P → ℝ) (outcomes : ℕ → P) (i : Fin n) (T : ℕ) : ℝ

theorem MultiplicativeWeights.expert_penalty_split {n : ℕ} {P : Type u_1} (M : Fin n → P → ℝ) (outcomes : ℕ → P) (i : Fin n) (T : ℕ) : totalExpertPenalty M outcomes i T = totalNonnegPenalty M outcomes i T + totalNegPenalty M outcomes i T

theorem MultiplicativeWeights.general_mw_regret_bound {P : Type u_1} {n : ℕ} (hn : 0 < n) (M : Fin n → P → ℝ) (ρ ε : ℝ) (outcomes : ℕ → P) (hε_pos : 0 < ε) (hε_le : ε ≤ 1 / 2) (hρ_pos : 0 < ρ) (hM : ∀ (i : Fin n) (j : P), M i j ∈ Set.Icc (-ρ) ρ) (i : Fin n) (T : ℕ) : totalExpectedPenalty M ρ ε outcomes T ≤ ρ * Real.log ↑n / ε + (1 + ε) * totalNonnegPenalty M outcomes i T + (1 - ε) * totalNegPenalty M outcomes i T

theorem MultiplicativeWeights.corollary_algebraic_core (totalExp expertTotal A B ρ logn δ : ℝ) (T : ℕ) (hT_pos : 0 < ↑T) (hρ_pos : 0 < ρ) (hδ_pos : 0 < δ) (hAB : A + B = expertTotal) (hAmB : A - B ≤ ↑T * ρ) (hbound : totalExp ≤ ρ * logn / (δ / (4 * ρ)) + (1 + δ / (4 * ρ)) * A + (1 - δ / (4 * ρ)) * B) (hT_big : 16 * ρ ^ 2 * logn / δ ^ 2 ≤ ↑T) : totalExp / ↑T ≤ δ + expertTotal / ↑T

theorem MultiplicativeWeights.abs_penalty_sum_le {n : ℕ} {P : Type u_1} {ρ : ℝ} (M : Fin n → P → ℝ) (outcomes : ℕ → P) (hM : ∀ (i : Fin n) (j : P), M i j ∈ Set.Icc (-ρ) ρ) (_hρ_pos : 0 < ρ) (i : Fin n) (T : ℕ) : totalNonnegPenalty M outcomes i T - totalNegPenalty M outcomes i T ≤ ↑T * ρ

theorem MultiplicativeWeights.mw_average_penalty_bound {P : Type u_1} {n : ℕ} (hn : 0 < n) (M : Fin n → P → ℝ) {ρ : ℝ} (outcomes : ℕ → P) (hρ_pos : 0 < ρ) (hM : ∀ (i : Fin n) (j : P), M i j ∈ Set.Icc (-ρ) ρ) {δ : ℝ} (hδ_pos : 0 < δ) (hε_le : δ / (4 * ρ) ≤ 1 / 2) {T : ℕ} (hT_pos : 0 < T) (hT_big : 16 * ρ ^ 2 * Real.log ↑n / δ ^ 2 ≤ ↑T) (i : Fin n) : totalExpectedPenalty M ρ (δ / (4 * ρ)) outcomes T / ↑T ≤ δ + totalExpertPenalty M outcomes i T / ↑T

noncomputable def MultiplicativeWeights.expectedMistakes {n : ℕ} (wrong : Fin n → ℕ → Prop) [(i : Fin n) → (t : ℕ) → Decidable (wrong i t)] (ε : ℝ) (T : ℕ) : ℝ

theorem MultiplicativeWeights.randomized_mw_expected_regret_bound {n : ℕ} (hn : 0 < n) (wrong : Fin n → ℕ → Prop) [(i : Fin n) → (t : ℕ) → Decidable (wrong i t)] {ε : ℝ} (hε_pos : 0 < ε) (hε_lt : ε < 1 / 2) (i : Fin n) (T : ℕ) : expectedMistakes wrong ε T ≤ Real.log ↑n / ε + (1 + ε) * ↑(expertMistakes wrong i T)