structure CommutingRepetition.FiniteEventLaw (Ω : Type u_1) [Fintype Ω] : Type u_1

• weight : Ω → ℝ
• weight_nonneg (ω : Ω) : 0 ≤ self.weight ω
• weight_sum : ∑ ω : Ω, self.weight ω = 1

def CommutingRepetition.FiniteEventLaw.eventMass {Ω : Type u_1} [Fintype Ω] (law : FiniteEventLaw Ω) (event : Finset Ω) : ℝ

Equations

• law.eventMass event = ∑ ω ∈ event, law.weight ω

theorem CommutingRepetition.FiniteEventLaw.eventMass_univ {Ω : Type u_1} [Fintype Ω] (law : FiniteEventLaw Ω) : law.eventMass Finset.univ = 1

theorem CommutingRepetition.FiniteEventLaw.eventMass_mono {Ω : Type u_1} [Fintype Ω] (law : FiniteEventLaw Ω) {s t : Finset Ω} (h : s ⊆ t) : law.eventMass s ≤ law.eventMass t

def CommutingRepetition.FiniteEventLaw.winEvent {Ω : Type u_1} {ι : Type u_2} [Fintype Ω] [Fintype ι] (wins : ι → Ω → Bool) (D : Finset ι) : Finset Ω

Equations

• CommutingRepetition.FiniteEventLaw.winEvent wins D = {ω : Ω | ∀ i ∈ D, wins i ω = true}

theorem CommutingRepetition.FiniteEventLaw.winEvent_empty {Ω : Type u_1} {ι : Type u_2} [Fintype Ω] [Fintype ι] (wins : ι → Ω → Bool) : winEvent wins ∅ = Finset.univ

theorem CommutingRepetition.FiniteEventLaw.winEvent_antitone {Ω : Type u_1} {ι : Type u_2} [Fintype Ω] [Fintype ι] (wins : ι → Ω → Bool) {D E : Finset ι} (h : D ⊆ E) : winEvent wins E ⊆ winEvent wins D

theorem CommutingRepetition.FiniteEventLaw.allWinMass_le_partial {Ω : Type u_1} {ι : Type u_2} [Fintype Ω] [Fintype ι] (law : FiniteEventLaw Ω) (wins : ι → Ω → Bool) (D : Finset ι) : law.eventMass (winEvent wins Finset.univ) ≤ law.eventMass (winEvent wins D)

def CommutingRepetition.FiniteEventLaw.failureMass {Ω : Type u_1} {ι : Type u_2} [Fintype Ω] [Fintype ι] [DecidableEq ι] (law : FiniteEventLaw Ω) (wins : ι → Ω → Bool) (D : Finset ι) (i : ι) : ℝ

Equations

• law.failureMass wins D i = law.eventMass (CommutingRepetition.FiniteEventLaw.winEvent wins D) - law.eventMass (CommutingRepetition.FiniteEventLaw.winEvent wins (insert i D))

theorem CommutingRepetition.FiniteEventLaw.exists_greedy_stopping {ι : Type u_2} [Fintype ι] [DecidableEq ι] (mass : Finset ι → ℝ) {θ η : ℝ} {T : ℕ} (_hθ : 0 < θ) (_hη : 0 < η) (hη_one : η ≤ 1) (hT : T ≤ Fintype.card ι) (hempty : mass ∅ = 1) (hfloor : ∀ (D : Finset ι), θ ≤ mass D) (h_terminal : (1 - η) ^ T < θ) : ∃ (D : Finset ι), D.card < T ∧ θ ≤ mass D ∧ ∑ i ∈ Finset.univ \ D, (mass D - mass (insert i D)) < ↑(Finset.univ \ D).card * (η * mass D)

theorem CommutingRepetition.FiniteEventLaw.exists_conditioned_win_set {Ω : Type u_1} {ι : Type u_2} [Fintype Ω] [Fintype ι] [DecidableEq ι] (law : FiniteEventLaw Ω) (wins : ι → Ω → Bool) {θ η : ℝ} {T : ℕ} (hθ : 0 < θ) (hη : 0 < η) (hη_one : η ≤ 1) (hT : T ≤ Fintype.card ι) (hwin : θ ≤ law.eventMass (winEvent wins Finset.univ)) (h_terminal : (1 - η) ^ T < θ) : ∃ (D : Finset ι), D.card < T ∧ θ ≤ law.eventMass (winEvent wins D) ∧ ∑ i ∈ Finset.univ \ D, law.failureMass wins D i < ↑(Finset.univ \ D).card * (η * law.eventMass (winEvent wins D))