Lean module · Foundations
BanditRLProof.LowerBounds.AffinityKL
The measure-level Jensen step in the Chapter 14 overlap proof.
Module map
Imports
BanditRLProof.LowerBounds.CommonDensityOverlap
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.LowerBounds.mul_exp_neg_half_log_eq_sqrt
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.LowerBounds.mul_exp_neg_half_log_eq_sqrtReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem mul_exp_neg_half_log_eq_sqrt {r : ℝ} (hr : 0 ≤ r) : r * Real.exp (-Real.log r / 2) = Real.sqrt r
theorem
BanditRLProof.LowerBounds.integrable_sqrt_rnDeriv
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.LowerBounds.integrable_sqrt_rnDerivReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integrable_sqrt_rnDeriv {α : Type*} [MeasurableSpace α] (P Q : Measure α) [IsFiniteMeasure P] [IsFiniteMeasure Q] : Integrable (fun x => Real.sqrt (P.rnDeriv Q x).toReal) Q
theorem
BanditRLProof.LowerBounds.integrable_exp_neg_half_llr
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.LowerBounds.integrable_exp_neg_half_llrReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integrable_exp_neg_half_llr {α : Type*} [MeasurableSpace α] (P Q : Measure α) [IsFiniteMeasure P] [IsFiniteMeasure Q] (hPQ : P ≪ Q) : Integrable (fun x => Real.exp (-llr P Q x / 2)) P
theorem
BanditRLProof.LowerBounds.integral_exp_neg_half_llr_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.LowerBounds.integral_exp_neg_half_llr_eqReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integral_exp_neg_half_llr_eq {α : Type*} [MeasurableSpace α] (P Q : Measure α) [IsFiniteMeasure P] [IsFiniteMeasure Q] (hPQ : P ≪ Q) : (∫ x, Real.exp (-llr P Q x / 2) ∂P) = ∫ x, Real.sqrt (P.rnDeriv Q x).toReal ∂Q
theorem
BanditRLProof.LowerBounds.exp_neg_half_integral_llr_le_rnAffinity
Compiled
Jensen's source proof step, in the RN representation and finite-KL branch.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.LowerBounds.exp_neg_half_integral_llr_le_rnAffinityReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem exp_neg_half_integral_llr_le_rnAffinity {α : Type*} [MeasurableSpace α] (P Q : Measure α) [IsProbabilityMeasure P] [IsProbabilityMeasure Q] (hPQ : P ≪ Q) (hi : Integrable (llr P Q) P) : Real.exp (-(∫ x, llr P Q x ∂P) / 2) ≤ ∫ x, Real.sqrt (P.rnDeriv Q x).toReal ∂Q
theorem
BanditRLProof.LowerBounds.rnAffinity_eq_commonDensityAffinity
Compiled
Change the RN affinity to any common sigma-finite dominating measure.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.LowerBounds.rnAffinity_eq_commonDensityAffinityReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem rnAffinity_eq_commonDensityAffinity {α : Type*} [MeasurableSpace α] (P Q μ : Measure α) [IsFiniteMeasure P] [IsFiniteMeasure Q] [SigmaFinite μ] (hPQ : P ≪ Q) (hQ : Q ≪ μ) : (∫ x, Real.sqrt (P.rnDeriv Q x).toReal ∂Q) = commonDensityAffinity P Q μ
theorem
BanditRLProof.LowerBounds.exp_neg_half_integral_llr_le_commonDensityAffinity
Compiled
The source's measure-level Jensen step with arbitrary common domination.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.LowerBounds.exp_neg_half_integral_llr_le_commonDensityAffinityReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem exp_neg_half_integral_llr_le_commonDensityAffinity {α : Type*} [MeasurableSpace α] (P Q μ : Measure α) [IsProbabilityMeasure P] [IsProbabilityMeasure Q] [SigmaFinite μ] (hPQ : P ≪ Q) (hQ : Q ≪ μ) (hi : Integrable (llr P Q) P) : Real.exp (-(∫ x, llr P Q x ∂P) / 2) ≤ commonDensityAffinity P Q μ
theorem
BanditRLProof.LowerBounds.bretagnolleHuberScale_le_half_commonDensityAffinity_sq
Compiled
The squared-affinity/KL bound, with the infinite-KL branch explicit.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret · Chapter 14: Foundations of Information Theory
Canonical node identity
declaration:BanditRLProof.LowerBounds.bretagnolleHuberScale_le_half_commonDensityAffinity_sqReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem bretagnolleHuberScale_le_half_commonDensityAffinity_sq {α : Type*} [MeasurableSpace α] (P Q μ : Measure α) [IsProbabilityMeasure P] [IsProbabilityMeasure Q] [SigmaFinite μ] (hQ : Q ≪ μ) : bretagnolleHuberScale (relativeEntropy P Q) ≤ (1 / 2 : ℝ) * commonDensityAffinity P Q μ ^ 2