Lean module · Foundations
BanditRLProof.HeavyTailSourceSchedule
Original source log schedule and signed adaptive-prefix confidence. Counts are handled by a finite union, never by asserting selected samples IID.
Module map
Imports
BanditRLProof.HeavyTailSourceConfidence
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.HeavyTail.sourceConfidenceLog
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.HeavyTail.sourceConfidenceLogReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def sourceConfidenceLog (t : ℕ) : ℝ
def
BanditRLProof.HeavyTail.sourceConfidenceRadius
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.HeavyTail.sourceConfidenceRadiusReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def sourceConfidenceRadius (ε u : ℝ) (t n : ℕ) : ℝ
theorem
BanditRLProof.HeavyTail.sourceConfidenceLog_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.HeavyTail.sourceConfidenceLog_posReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem sourceConfidenceLog_pos (t : ℕ) (ht : 0 < t) : 0 < sourceConfidenceLog t
theorem
BanditRLProof.HeavyTail.source_adaptive_mean_upper_tail
Compiled
The count is arbitrary; the set explicitly restricts it to the available prefixes.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.HeavyTail.source_adaptive_mean_upper_tailReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem source_adaptive_mean_upper_tail {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (count : Ω → ℕ) (ε u mean : ℝ) (t : ℕ) (hXm : ∀ i, Measurable (X i)) (hi : iIndepFun X μ) (hε0 : 0 ≤ ε) (hε : ε ≤ 1) (hu : 0 < u) (hX : ∀ i, Integrable (X i) μ) (hmean : ∀ i, (∫ ω, X i ω ∂μ) = mean) (hm : ∀ i, Integrable (fun ω => |X i ω|^(1+ε)) μ) (hraw : ∀ i, (∫ ω, |X i ω|^(1+ε) ∂μ) ≤ u) : μ.real {ω | 0 < count ω ∧ count ω ≤ t ∧ sourceConfidenceRadius ε u t (count ω) ≤ (∑ s ∈ Finset.range (count ω), truncate (sourceTruncationThreshold ε u (sourceConfidenceLog t) s) (X s ω)) / count ω - mean} ≤ t*Real.exp (-(5/4 : ℝ)*sourceConfidenceLog t)
theorem
BanditRLProof.HeavyTail.source_adaptive_mean_lower_tail
Compiled
Reflection retains the identical count, schedule and raw moment hypotheses.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.HeavyTail.source_adaptive_mean_lower_tailReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem source_adaptive_mean_lower_tail {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (count : Ω → ℕ) (ε u mean : ℝ) (t : ℕ) (hXm : ∀ i, Measurable (X i)) (hi : iIndepFun X μ) (hε0 : 0 ≤ ε) (hε : ε ≤ 1) (hu : 0 < u) (hX : ∀ i, Integrable (X i) μ) (hmean : ∀ i, (∫ ω, X i ω ∂μ) = mean) (hm : ∀ i, Integrable (fun ω => |X i ω|^(1+ε)) μ) (hraw : ∀ i, (∫ ω, |X i ω|^(1+ε) ∂μ) ≤ u) : μ.real {ω | 0 < count ω ∧ count ω ≤ t ∧ sourceConfidenceRadius ε u t (count ω) ≤ mean - (∑ s ∈ Finset.range (count ω), truncate (sourceTruncationThreshold ε u (sourceConfidenceLog t) s) (X s ω)) / count ω} ≤ t*Real.exp (-(5/4 : ℝ)*sourceConfidenceLog t)
theorem
BanditRLProof.HeavyTail.inverse_sqrt_step
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.HeavyTail.inverse_sqrt_stepReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem inverse_sqrt_step (x : ℝ) (hx : 0 < x) : 1 / (Real.sqrt (x+1))^3 ≤ 2*(1/Real.sqrt x - 1/Real.sqrt (x+1))
theorem
BanditRLProof.HeavyTail.source_schedule_exp_eq
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.HeavyTail.source_schedule_exp_eqReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem source_schedule_exp_eq (t : ℕ) : Real.exp (-(5/4 : ℝ)*sourceConfidenceLog t) = 1/(Real.sqrt ((t : ℝ)+1))^5
theorem
BanditRLProof.HeavyTail.source_schedule_tail_le_telescope
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.HeavyTail.source_schedule_tail_le_telescopeReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem source_schedule_tail_le_telescope (t : ℕ) (ht : 0 < t) : t*Real.exp (-(5/4 : ℝ)*sourceConfidenceLog t) ≤ 2*(1/Real.sqrt (t : ℝ)-1/Real.sqrt ((t : ℝ)+1))
theorem
BanditRLProof.HeavyTail.source_schedule_tail_sum_le_two
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.HeavyTail.source_schedule_tail_sum_le_twoReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem source_schedule_tail_sum_le_two (T : ℕ) : (∑ t ∈ Finset.range T, t*Real.exp (-(5/4 : ℝ)*sourceConfidenceLog t)) ≤ 2