Lean module · Foundations
BanditRLProof.Algorithms.CausalSampleMGF
Centered MGF and signed sum tails on actual causal intervention samples.
Module map
Imports
BanditRLProof.Algorithms.CausalSampling, BanditRLProof.HeavyTailFixedTilt
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.Causal.GraphModel.sampleWeightedBit_signed_mgf
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.GraphModel.sampleWeightedBit_signed_mgfReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem GraphModel.sampleWeightedBit_signed_mgf (g : GraphModel V n) (rewardBit : V → Bool) (actions : A → Fin n → Option V) (eta : PMF A) (i : Fin n) (hi : ∀ a, actions a i = none) (hc : Covers (fun a => g.parentLaw (actions a) i) (mixture eta (fun a => g.parentLaw (actions a) i))) (a : A) (B : ℝ) (hB : 0 ≤ B) (T : ℕ) (t : Fin T) (sign tilt : ℝ) (hs : |sign| = 1) (hsmall : |tilt| * (2*B) ≤ 1) : Concentration.HasMGFUpperBoundAt (fun w => sign * (g.sampleWeightedBit rewardBit actions eta i a B t w - truncatedMean (g.parentLaw (actions a) i) (mixture eta (fun b => g.parentLaw (actions b) i)) (fun z => mass ((g.parentTable i z).map rewardBit) true) B)) tilt (tilt^2 * designCost (fun b => g.parentLaw (actions b) i) eta) (g.sampleLaw actions eta T)
theorem
BanditRLProof.Causal.GraphModel.sampleWeightedBit_signed_sum_mgf
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.GraphModel.sampleWeightedBit_signed_sum_mgfReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem GraphModel.sampleWeightedBit_signed_sum_mgf (g : GraphModel V n) (rewardBit : V → Bool) (actions : A → Fin n → Option V) (eta : PMF A) (i : Fin n) (hi : ∀ a, actions a i = none) (hc : Covers (fun a => g.parentLaw (actions a) i) (mixture eta (fun a => g.parentLaw (actions a) i))) (a : A) (B : ℝ) (hB : 0 ≤ B) (T : ℕ) (sign tilt : ℝ) (hs : |sign| = 1) (hsmall : |tilt| * (2*B) ≤ 1) : Concentration.HasMGFUpperBoundAt (fun w => ∑ t : Fin T, sign * (g.sampleWeightedBit rewardBit actions eta i a B t w - truncatedMean (g.parentLaw (actions a) i) (mixture eta (fun b => g.parentLaw (actions b) i)) (fun z => mass ((g.parentTable i z).map rewardBit) true) B)) tilt ((T:ℝ) * (tilt^2 * designCost (fun b => g.parentLaw (actions b) i) eta)) (g.sampleLaw actions eta T)
theorem
BanditRLProof.Causal.GraphModel.sampleWeightedBit_signed_sum_tail
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.GraphModel.sampleWeightedBit_signed_sum_tailReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem GraphModel.sampleWeightedBit_signed_sum_tail (g : GraphModel V n) (rewardBit : V → Bool) (actions : A → Fin n → Option V) (eta : PMF A) (i : Fin n) (hi : ∀ a, actions a i = none) (hc : Covers (fun a => g.parentLaw (actions a) i) (mixture eta (fun a => g.parentLaw (actions a) i))) (a : A) (B : ℝ) (hB : 0 ≤ B) (T : ℕ) (sign tilt r : ℝ) (hs : |sign| = 1) (ht : 0 ≤ tilt) (hsmall : |tilt| * (2*B) ≤ 1) : (g.sampleLaw actions eta T).real {w | r ≤ ∑ t : Fin T, sign * (g.sampleWeightedBit rewardBit actions eta i a B t w - truncatedMean (g.parentLaw (actions a) i) (mixture eta (fun b => g.parentLaw (actions b) i)) (fun z => mass ((g.parentTable i z).map rewardBit) true) B)} ≤ Real.exp (-tilt*r + (T:ℝ) * (tilt^2 * designCost (fun b => g.parentLaw (actions b) i) eta))