BanditRLProof.Algorithms.CausalImportance

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

noncomputable def mass {Z : Type*} (p : PMF Z) (z : Z) : ℝ

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

theorem mass_nonneg {Z : Type*} (p : PMF Z) (z : Z) : 0 ≤ mass p z

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

theorem mass_le_one {Z : Type*} (p : PMF Z) (z : Z) : mass p z ≤ 1

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

theorem sum_mass {Z : Type*} [Fintype Z] (p : PMF Z) : ∑ z, mass p z = 1

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

noncomputable def mixture {A Z : Type*} (eta : PMF A) (p : A → PMF Z) : PMF Z

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

theorem mixture_mass {A Z : Type*} [Fintype A] (eta : PMF A) (p : A → PMF Z) (z : Z) : mass (mixture eta p) z = ∑ a, mass eta a * mass (p a) z

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

def Covers {A Z : Type*} (p : A → PMF Z) (q : PMF Z) : Prop

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

noncomputable def ratio {Z : Type*} (p q : PMF Z) (z : Z) : ℝ

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

theorem covered_cancel {A Z : Type*} (p : A → PMF Z) (q : PMF Z) (hc : Covers p q) (a : A) (z : Z) : mass q z * ratio (p a) q z = mass (p a) z

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

theorem importance_identity {A Z : Type*} [Fintype Z] (p : A → PMF Z) (q : PMF Z) (hc : Covers p q) (a : A) (f : Z → ℝ) : ∑ z, mass q z * (ratio (p a) q z * f z) = ∑ z, mass (p a) z * f z

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

theorem positive_allocation_covers {A Z : Type*} [Fintype A] (eta : PMF A) (p : A → PMF Z) (he : ∀ a, 0 < mass eta a) : Covers p (mixture eta p)

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

theorem ratio_nonneg {Z : Type*} (p q : PMF Z) (z : Z) : 0 ≤ ratio p q z

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

noncomputable def secondMoment {Z : Type*} [Fintype Z] (p q : PMF Z) : ℝ

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

theorem ratio_second_moment {A Z : Type*} [Fintype Z] (p : A → PMF Z) (q : PMF Z) (hc : Covers p q) (a : A) : ∑ z, mass q z * ratio (p a) q z ^ 2 = secondMoment (p a) q

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

noncomputable def truncationBias {Z : Type*} [Fintype Z] (p q : PMF Z) (r : Z → ℝ) (B : ℝ) : ℝ

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

noncomputable def truncatedMean {Z : Type*} [Fintype Z] (p q : PMF Z) (r : Z → ℝ) (B : ℝ) : ℝ

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

theorem truncatedMean_add_bias {A Z : Type*} [Fintype Z] (p : A → PMF Z) (q : PMF Z) (hc : Covers p q) (a : A) (r : Z → ℝ) (B : ℝ) : truncatedMean (p a) q r B + truncationBias (p a) q r B = ∑ z, mass (p a) z * r z

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

theorem truncationBias_nonneg {Z : Type*} [Fintype Z] (p q : PMF Z) (r : Z → ℝ) (hr : ∀ z, 0 ≤ r z) (B : ℝ) : 0 ≤ truncationBias p q r B

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

theorem truncationBias_le {Z : Type*} [Fintype Z] (p q : PMF Z) (r : Z → ℝ) (hr : ∀ z, r z ≤ 1) (B : ℝ) (hB : 0 < B) : truncationBias p q r B ≤ secondMoment p q / B

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

noncomputable def pairedLaw {Z V : Type*} (p : PMF Z) (k : Z → PMF V) : PMF (Z × V)

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

theorem mixture_pairedLaw {A Z V : Type*} (eta : PMF A) (p : A → PMF Z) (k : Z → PMF V) : mixture eta (fun a => pairedLaw (p a) k) = pairedLaw (mixture eta p) k

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

theorem pairedLaw_mass {Z V : Type*} (p : PMF Z) (k : Z → PMF V) (z : Z) (y : V) : mass (pairedLaw p k) (z,y) = mass p z * mass (k z) y

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

noncomputable def weightedBit {Z : Type*} (p q : PMF Z) (B : ℝ) (zy : Z × Bool) : ℝ

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

theorem weightedBit_mean {Z : Type*} [Fintype Z] (p q : PMF Z) (k : Z → PMF Bool) (B : ℝ) : (∑ z, ∑ y : Bool, mass (pairedLaw q k) (z,y) * weightedBit p q B (z,y)) = truncatedMean p q (fun z => mass (k z) true) B

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

theorem weightedBit_bounds {Z : Type*} (p q : PMF Z) (B : ℝ) (hB : 0 ≤ B) (zy : Z × Bool) : 0 ≤ weightedBit p q B zy ∧ weightedBit p q B zy ≤ B

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

theorem weightedBit_second_le {A Z : Type*} [Fintype Z] (p : A → PMF Z) (q : PMF Z) (hc : Covers p q) (a : A) (k : Z → PMF Bool) (B : ℝ) : (∑ z, ∑ y : Bool, mass (pairedLaw q k) (z,y) * weightedBit (p a) q B (z,y)^2) ≤ secondMoment (p a) q

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

theorem GraphModel.mixture_parent_joint {A V : Type*} [Inhabited V] {n : ℕ} (g : GraphModel V n) (actions : A → Fin n → Option V) (eta : PMF A) (i : Fin n) (hi : ∀ a, actions a i = none) : mixture eta (fun a => (joint (g.doModel (actions a)).table).map (fun x => (g.parentConfig i (history x i),x i))) = pairedLaw (mixture eta (fun a => g.parentLaw (actions a) i)) (g.parentTable i)