Lean module · Foundations
BanditRLProof.Algorithms.CausalImportanceTransport
Importance ratios and design cost under injective finite-state encoding.
Module map
Imports
BanditRLProof.Algorithms.CausalAllocation
Imported by
BanditRLProof.Algorithms.CausalHeterogeneousSampling, BanditRLProof.Algorithms.CausalParallelRegret
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.Causal.mass_map_injective
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.Causal.mass_map_injectiveReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem mass_map_injective (p : PMF Z) (e : Z → U) (he : Function.Injective e) (z : Z) : mass (p.map e) (e z) = mass p z
theorem
BanditRLProof.Causal.ratio_map_injective
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.Causal.ratio_map_injectiveReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem ratio_map_injective (p q : PMF Z) (e : Z → U) (he : Function.Injective e) (z : Z) : ratio (p.map e) (q.map e) (e z) = ratio p q z
theorem
BanditRLProof.Causal.mixture_map
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.Causal.mixture_mapReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem mixture_map (eta : PMF A) (p : A → PMF Z) (e : Z → U) : mixture eta (fun a => (p a).map e) = (mixture eta p).map e
theorem
BanditRLProof.Causal.covers_map_injective
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.Causal.covers_map_injectiveReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem covers_map_injective (p : A → PMF Z) (q : PMF Z) (hc : Covers p q) (e : Z → U) (he : Function.Injective e) : Covers (fun a => (p a).map e) (q.map e)
theorem
BanditRLProof.Causal.weightedBit_map_injective
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.Causal.weightedBit_map_injectiveReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem weightedBit_map_injective (p q : PMF Z) (e : Z → U) (he : Function.Injective e) (B : ℝ) (z : Z) (y : Bool) : weightedBit (p.map e) (q.map e) B (e z,y) = weightedBit p q B (z,y)
theorem
BanditRLProof.Causal.secondMoment_map_injective
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.Causal.secondMoment_map_injectiveReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem secondMoment_map_injective (p q : PMF Z) (e : Z → U) (he : Function.Injective e) : secondMoment (p.map e) (q.map e) = secondMoment p q
theorem
BanditRLProof.Causal.designCost_map_injective
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.Causal.designCost_map_injectiveReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem designCost_map_injective (p : A → PMF Z) (eta : PMF A) (e : Z → U) (he : Function.Injective e) : designCost (fun a => (p a).map e) eta = designCost p eta