Lean module · Foundations
BanditRLProof.PowerCutoffNormalization
Exact normalization of the balanced polynomial cutoff into source powers.
Module map
Imports
BanditRLProof.PowerTailIntegral
Imported by
BanditRLProof, BanditRLProof.Algorithms.CUCBPolynomialRegret
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.PowerTailIntegral.source_cutoff_normalization
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.PowerTailIntegral.source_cutoff_normalizationReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem source_cutoff_normalization (C N γ ω : ℝ) (hC : 0<C) (hN : 0<N) (hγ : 0<γ) (hω : 0<ω) (hω1 : ω≤1) : (2/ω)/(2/ω-1)*(N*((C*γ^(2/ω))/N)^(1/(2/ω)))= (2*γ/(2-ω))*C^(ω/2)*N^(1-ω/2)