Lean module · Foundations

BanditRLProof.Algorithms.CausalOptimalAllocation

Attainment of the covered finite causal allocation objective.

Module map

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

Imports

BanditRLProof.Algorithms.CausalAllocation

Imported by

BanditRLProof, BanditRLProof.Algorithms.CausalParallelDesign, BanditRLProof.Algorithms.CausalSampling

Declarations

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

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

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

noncomputable def allocationOfWeights (w : A → ℝ) (hw : w ∈ stdSimplex ℝ A) : PMF A

Source line 12 Chapter context: Foundations

theorem BanditRLProof.Causal.allocationOfWeights_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.allocationOfWeights_mass

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

theorem allocationOfWeights_mass (w : A → ℝ) (hw : w ∈ stdSimplex ℝ A) (a : A) : mass (allocationOfWeights w hw) a = w a

Source line 18 Chapter context: Foundations

theorem BanditRLProof.Causal.mass_mem_simplex 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_mem_simplex

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

theorem mass_mem_simplex (eta : PMF A) : mass eta ∈ stdSimplex ℝ A

Source line 23 Chapter context: Foundations

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

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

noncomputable def mixtureWeight (p : A → PMF Z) (w : A → ℝ) (z : Z) : ℝ

Source line 26 Chapter context: Foundations

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

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

noncomputable def coordinateCost (p : A → PMF Z) (w : A → ℝ) : ℝ

Source line 29 Chapter context: Foundations

theorem BanditRLProof.Causal.coordinateCost_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.coordinateCost_mass

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

theorem coordinateCost_mass (p : A → PMF Z) (eta : PMF A) : coordinateCost p (mass eta) = designCost p eta

Source line 33 Chapter context: Foundations

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

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

def safeAllocations (p : A → PMF Z) : Set (A → ℝ)

Source line 43 Chapter context: Foundations

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

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

theorem continuous_mixtureWeight (p : A → PMF Z) (z : Z) : Continuous (fun w => mixtureWeight p w z)

Source line 47 Chapter context: Foundations

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

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

theorem safeAllocations_compact (p : A → PMF Z) : IsCompact (safeAllocations p)

Source line 53 Chapter context: Foundations

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

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

theorem sublevel_mem_safe (p : A → PMF Z) (eta : PMF A) (hc : Covers p (mixture eta p)) (hcost : designCost p eta ≤ Fintype.card A) : mass eta ∈ safeAllocations p

Source line 63 Chapter context: Foundations

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

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

theorem uniform_mem_safe (p : A → PMF Z) : mass (PMF.uniformOfFintype A) ∈ safeAllocations p

Source line 70 Chapter context: Foundations

theorem BanditRLProof.Causal.safe_denominator_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.safe_denominator_pos

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

theorem safe_denominator_pos (p : A → PMF Z) (w : A → ℝ) (hw : w ∈ safeAllocations p) (a : A) (z : Z) (hp : mass (p a) z ≠ 0) : 0 < mixtureWeight p w z

Source line 74 Chapter context: Foundations

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

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

theorem coordinateCost_continuousOn (p : A → PMF Z) : ContinuousOn (coordinateCost p) (safeAllocations p)

Source line 79 Chapter context: Foundations

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

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

theorem safe_allocation_covers (p : A → PMF Z) (w : A → ℝ) (hw : w ∈ safeAllocations p) : Covers p (mixture (allocationOfWeights w hw.1) p)

Source line 91 Chapter context: Foundations

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

Canonical node identity

declaration:BanditRLProof.Causal.exists_optimal_allocation

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

theorem exists_optimal_allocation (p : A → PMF Z) : ∃ eta : PMF A, Covers p (mixture eta p) ∧ designCost p eta ≤ Fintype.card A ∧ ∀ eta' : PMF A, Covers p (mixture eta' p) → designCost p eta ≤ designCost p eta'

Source line 97 Chapter context: Foundations

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

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

noncomputable def optimalAllocation (p : A → PMF Z) : PMF A

Source line 119 Chapter context: Foundations

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

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

theorem optimalAllocation_covers (p : A → PMF Z) : Covers p (mixture (optimalAllocation p) p)

Source line 122 Chapter context: Foundations

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

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

theorem optimalAllocation_cost_le_card (p : A → PMF Z) : designCost p (optimalAllocation p) ≤ Fintype.card A

Source line 125 Chapter context: Foundations

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

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

theorem optimalAllocation_minimizes (p : A → PMF Z) (eta : PMF A) (hc : Covers p (mixture eta p)) : designCost p (optimalAllocation p) ≤ designCost p eta

Source line 129 Chapter context: Foundations

theorem BanditRLProof.Causal.secondMoment_self 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_self

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

theorem secondMoment_self (q : PMF Z) : secondMoment q q = 1

Source line 133 Chapter context: Foundations

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

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

theorem constant_designCost (q : PMF Z) (eta : PMF A) : designCost (fun _ : A => q) eta = 1

Source line 138 Chapter context: Foundations