Lean module · Foundations

BanditRLProof.Algorithms.CausalParallelDesign

Constructed rarity parameter and normalized finite intervention design.

Module map

Source: BanditRLProof/Algorithms/CausalParallelDesign.lean
Teaching chapter: 1. Finite bandits, traces, and regret
Declarations: 25
Placeholders: 0

Imports

BanditRLProof.Algorithms.CausalOptimalAllocation

Imported by

BanditRLProof.Algorithms.CausalParallelLaw

Declarations

Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.

structure BanditRLProof.Causal.ParallelParameters 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.ParallelParameters

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

structure ParallelParameters (N : ℕ) where

Source line 9 Chapter context: Foundations

def BanditRLProof.Causal.ParallelParameters.rareIndices 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.ParallelParameters.rareIndices

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

noncomputable def rareIndices (tau : ℕ) : Finset (Fin N)

Source line 18 Chapter context: Foundations

theorem BanditRLProof.Causal.ParallelParameters.exists_rarity 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.ParallelParameters.exists_rarity

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem exists_rarity : ∃ m : ℕ, 2 ≤ m ∧ m ≤ N ∧ (p.rareIndices m).card ≤ m

Source line 21 Chapter context: Foundations

def BanditRLProof.Causal.ParallelParameters.rarity 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

Indexed settings: Causal bandits

Canonical node identity

declaration:BanditRLProof.Causal.ParallelParameters.rarity

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

noncomputable def rarity : ℕ

Source line 25 Chapter context: Foundations

theorem BanditRLProof.Causal.ParallelParameters.rarity_spec 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

Indexed settings: Causal bandits

Canonical node identity

declaration:BanditRLProof.Causal.ParallelParameters.rarity_spec

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem rarity_spec : 2 ≤ p.rarity ∧ p.rarity ≤ N ∧ (p.rareIndices p.rarity).card ≤ p.rarity

Source line 27 Chapter context: Foundations

theorem BanditRLProof.Causal.ParallelParameters.rarity_minimal 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

Indexed settings: Causal bandits

Canonical node identity

declaration:BanditRLProof.Causal.ParallelParameters.rarity_minimal

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem rarity_minimal (tau : ℕ) (h2 : 2 ≤ tau) (hN : tau ≤ N) (hc : (p.rareIndices tau).card ≤ tau) : p.rarity ≤ tau

Source line 30 Chapter context: Foundations

def BanditRLProof.Causal.ParallelParameters.valueProbability 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.ParallelParameters.valueProbability

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

def valueProbability (a : Fin N × Bool) : ℝ

Source line 34 Chapter context: Foundations

theorem BanditRLProof.Causal.ParallelParameters.valueProbability_nonneg 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.ParallelParameters.valueProbability_nonneg

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem valueProbability_nonneg (a : Fin N × Bool) : 0 ≤ p.valueProbability a

Source line 36 Chapter context: Foundations

theorem BanditRLProof.Causal.ParallelParameters.rarity_pos 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.ParallelParameters.rarity_pos

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem rarity_pos : (0 : ℝ) < p.rarity

Source line 40 Chapter context: Foundations

theorem BanditRLProof.Causal.ParallelParameters.rarity_reciprocal_le_half 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.ParallelParameters.rarity_reciprocal_le_half

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem rarity_reciprocal_le_half : 1/(p.rarity:ℝ) ≤ 1/2

Source line 44 Chapter context: Foundations

def BanditRLProof.Causal.ParallelParameters.rareActions 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.ParallelParameters.rareActions

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

noncomputable def rareActions : Finset (Fin N × Bool)

Source line 48 Chapter context: Foundations

theorem BanditRLProof.Causal.ParallelParameters.rareActions_card_le 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

Indexed settings: Causal bandits

Canonical node identity

declaration:BanditRLProof.Causal.ParallelParameters.rareActions_card_le

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem rareActions_card_le : p.rareActions.card ≤ p.rarity

Source line 51 Chapter context: Foundations

def BanditRLProof.Causal.ParallelParameters.rareWeight 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.ParallelParameters.rareWeight

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

noncomputable def rareWeight : ℝ

Source line 74 Chapter context: Foundations

def BanditRLProof.Causal.ParallelParameters.atomicTotal 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.ParallelParameters.atomicTotal

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

noncomputable def atomicTotal : ℝ

Source line 75 Chapter context: Foundations

theorem BanditRLProof.Causal.ParallelParameters.rareWeight_pos 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.ParallelParameters.rareWeight_pos

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem rareWeight_pos : 0 < p.rareWeight

Source line 77 Chapter context: Foundations

theorem BanditRLProof.Causal.ParallelParameters.atomicTotal_bounds 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.ParallelParameters.atomicTotal_bounds

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem atomicTotal_bounds : 0 ≤ p.atomicTotal ∧ p.atomicTotal ≤ 1/2

Source line 81 Chapter context: Foundations

def BanditRLProof.Causal.ParallelParameters.allocationWeight 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.ParallelParameters.allocationWeight

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

noncomputable def allocationWeight : Option (Fin N × Bool) → ℝ | none => 1-p.atomicTotal | some a => if a ∈ p.rareActions then p.rareWeight else 0 theorem allocationWeight_nonneg (a : Option (Fin N × Bool)) : 0 ≤ p.allocationWeight a

Source line 91 Chapter context: Foundations

theorem BanditRLProof.Causal.ParallelParameters.allocationWeight_nonneg 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.ParallelParameters.allocationWeight_nonneg

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem allocationWeight_nonneg (a : Option (Fin N × Bool)) : 0 ≤ p.allocationWeight a

Source line 95 Chapter context: Foundations

theorem BanditRLProof.Causal.ParallelParameters.allocationWeight_sum 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

Indexed settings: Causal bandits

Canonical node identity

declaration:BanditRLProof.Causal.ParallelParameters.allocationWeight_sum

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem allocationWeight_sum : ∑ a, p.allocationWeight a = 1

Source line 100 Chapter context: Foundations

def BanditRLProof.Causal.ParallelParameters.allocation 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

Indexed settings: Causal bandits

Canonical node identity

declaration:BanditRLProof.Causal.ParallelParameters.allocation

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

noncomputable def allocation : PMF (Option (Fin N × Bool))

Source line 108 Chapter context: Foundations

theorem BanditRLProof.Causal.ParallelParameters.allocation_mass 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.ParallelParameters.allocation_mass

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem allocation_mass (a : Option (Fin N × Bool)) : mass p.allocation a = p.allocationWeight a

Source line 111 Chapter context: Foundations

theorem BanditRLProof.Causal.ParallelParameters.allocation_empty_ge_half 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.ParallelParameters.allocation_empty_ge_half

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem allocation_empty_ge_half : 1/2 ≤ mass p.allocation none

Source line 114 Chapter context: Foundations

theorem BanditRLProof.Causal.covers_of_mass_domination 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_of_mass_domination

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem covers_of_mass_domination {A Z : Type*} (p : A → PMF Z) (q : PMF Z) (C : ℝ) (h : ∀ a z, mass (p a) z ≤ C*mass q z) : Covers p q

Source line 121 Chapter context: Foundations

theorem BanditRLProof.Causal.ratio_le_of_mass_domination 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_le_of_mass_domination

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem ratio_le_of_mass_domination {Z : Type*} (p q : PMF Z) (C : ℝ) (hC : 0 ≤ C) (h : ∀ z, mass p z ≤ C*mass q z) (z : Z) : ratio p q z ≤ C

Source line 128 Chapter context: Foundations

theorem BanditRLProof.Causal.secondMoment_le_of_mass_domination 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_le_of_mass_domination

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem secondMoment_le_of_mass_domination {Z : Type*} [Fintype Z] (p q : PMF Z) (C : ℝ) (hC : 0 ≤ C) (h : ∀ z, mass p z ≤ C*mass q z) : secondMoment p q ≤ C

Source line 134 Chapter context: Foundations