BanditRLProof.Algorithms.CausalAllocation

No declaration docstring is present; use the chapter context and exact statement below.

theorem secondMoment_ge_one {A Z : Type*} [Fintype Z] (p : A → PMF Z) (q : PMF Z) (hc : Covers p q) (a : A) : 1 ≤ secondMoment (p a) q

No declaration docstring is present; use the chapter context and exact statement below.

theorem uniform_mass {A : Type*} [Fintype A] [Nonempty A] (a : A) : mass (PMF.uniformOfFintype A) a = (Fintype.card A : ℝ)⁻¹

No declaration docstring is present; use the chapter context and exact statement below.

theorem uniform_covers {A Z : Type*} [Fintype A] [Nonempty A] (p : A → PMF Z) : Covers p (mixture (PMF.uniformOfFintype A) p)

No declaration docstring is present; use the chapter context and exact statement below.

theorem uniform_ratio_le_card {A Z : Type*} [Fintype A] [Nonempty A] (p : A → PMF Z) (a : A) (z : Z) : ratio (p a) (mixture (PMF.uniformOfFintype A) p) z ≤ Fintype.card A

No declaration docstring is present; use the chapter context and exact statement below.

theorem uniform_secondMoment_le_card {A Z : Type*} [Fintype A] [Nonempty A] [Fintype Z] (p : A → PMF Z) (a : A) : secondMoment (p a) (mixture (PMF.uniformOfFintype A) p) ≤ Fintype.card A

No declaration docstring is present; use the chapter context and exact statement below.

noncomputable def designCost {A Z : Type*} [Fintype A] [Nonempty A] [Fintype Z] (p : A → PMF Z) (eta : PMF A) : ℝ

No declaration docstring is present; use the chapter context and exact statement below.

theorem secondMoment_le_designCost {A Z : Type*} [Fintype A] [Nonempty A] [Fintype Z] (p : A → PMF Z) (eta : PMF A) (a : A) : secondMoment (p a) (mixture eta p) ≤ designCost p eta

No declaration docstring is present; use the chapter context and exact statement below.

theorem designCost_ge_one {A Z : Type*} [Fintype A] [Nonempty A] [Fintype Z] (p : A → PMF Z) (eta : PMF A) (hc : Covers p (mixture eta p)) : 1 ≤ designCost p eta

No declaration docstring is present; use the chapter context and exact statement below.

theorem uniform_designCost_le_card {A Z : Type*} [Fintype A] [Nonempty A] [Fintype Z] (p : A → PMF Z) : designCost p (PMF.uniformOfFintype A) ≤ Fintype.card A

No declaration docstring is present; use the chapter context and exact statement below.

noncomputable def convexLaw {Z : Type*} (t : ℝ≥0) (ht : t ≤ 1) (p q : PMF Z) : PMF Z

No declaration docstring is present; use the chapter context and exact statement below.

theorem convexLaw_mass {Z : Type*} (t : ℝ≥0) (ht : t ≤ 1) (p q : PMF Z) (z : Z) : mass (convexLaw t ht p q) z = (t : ℝ) * mass p z + (1-(t : ℝ)) * mass q z

No declaration docstring is present; use the chapter context and exact statement below.

theorem inverse_convex (x y t : ℝ) (hx : 0 < x) (hy : 0 < y) (ht : 0 ≤ t) (ht1 : t ≤ 1) : (t*x+(1-t)*y)⁻¹ ≤ t*x⁻¹+(1-t)*y⁻¹

No declaration docstring is present; use the chapter context and exact statement below.

theorem convexLaw_covers {A Z : Type*} (p : A → PMF Z) (q₀ q₁ : PMF Z) (hc₀ : Covers p q₀) (hc₁ : Covers p q₁) (t : ℝ≥0) (ht : t ≤ 1) : Covers p (convexLaw t ht q₀ q₁)

No declaration docstring is present; use the chapter context and exact statement below.

theorem secondMoment_convex {A Z : Type*} [Fintype Z] (p : A → PMF Z) (q₀ q₁ : PMF Z) (hc₀ : Covers p q₀) (hc₁ : Covers p q₁) (a : A) (t : ℝ≥0) (ht : t ≤ 1) : secondMoment (p a) (convexLaw t ht q₀ q₁) ≤ (t : ℝ)*secondMoment (p a) q₀+(1-(t : ℝ))*secondMoment (p a) q₁

No declaration docstring is present; use the chapter context and exact statement below.

theorem mixture_convexLaw {A Z : Type*} (p : A → PMF Z) (eta₀ eta₁ : PMF A) (t : ℝ≥0) (ht : t ≤ 1) : mixture (convexLaw t ht eta₀ eta₁) p = convexLaw t ht (mixture eta₀ p) (mixture eta₁ p)

No declaration docstring is present; use the chapter context and exact statement below.

theorem designCost_convex {A Z : Type*} [Fintype A] [Nonempty A] [Fintype Z] (p : A → PMF Z) (eta₀ eta₁ : PMF A) (hc₀ : Covers p (mixture eta₀ p)) (hc₁ : Covers p (mixture eta₁ p)) (t : ℝ≥0) (ht : t ≤ 1) : designCost p (convexLaw t ht eta₀ eta₁) ≤ (t : ℝ)*designCost p eta₀+(1-(t : ℝ))*designCost p eta₁

No declaration docstring is present; use the chapter context and exact statement below.

theorem design_sublevel_mass_lower {A Z : Type*} [Fintype A] [Nonempty A] [Fintype Z] (p : A → PMF Z) (eta : PMF A) (hc : Covers p (mixture eta p)) (K : ℝ) (hK : 0 < K) (hcost : designCost p eta ≤ K) (a : A) (z : Z) : mass (p a) z ^ 2 / K ≤ mass (mixture eta p) z