Lean module · Foundations

BanditRLProof.Algorithms.HOORewardFamily

Arbitrary reward-family interface for the source-repaired HOO rate. Only the countable representative-node law must be measurable. The internal discrete-domain transport preserves the actual action and trajectory.

Module map

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

Imports

BanditRLProof.Algorithms.HOOActualRegret

Imported by

BanditRLProof

Declarations

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

def BanditRLProof.HOO.Covering.familyNodeLaw 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

Indexed settings: Lipschitz bandits

Canonical node identity

declaration:BanditRLProof.HOO.Covering.familyNodeLaw

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

noncomputable def Covering.familyNodeLaw {X : Type*} (C : Covering X) (law : X → Measure ℝ) : Kernel Node ℝ where

Source line 11 Chapter context: Foundations

theorem BanditRLProof.HOO.Covering.familyNodeLaw_apply 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.HOO.Covering.familyNodeLaw_apply

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

theorem Covering.familyNodeLaw_apply {X : Type*} (C : Covering X) (law : X → Measure ℝ) (v : Node) : C.familyNodeLaw law v = law (C.representative v)

Source line 21 Chapter context: Foundations

theorem BanditRLProof.HOO.Covering.familyNodeLaw_eq_nodeLaw 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.HOO.Covering.familyNodeLaw_eq_nodeLaw

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

theorem Covering.familyNodeLaw_eq_nodeLaw {X : Type*} [MeasurableSpace X] (C : Covering X) (law : Kernel X ℝ) : C.familyNodeLaw (fun x => law x) = C.nodeLaw law

Source line 25 Chapter context: Foundations

def BanditRLProof.HOO.RegularCovering.discrete 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.HOO.RegularCovering.discrete

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

noncomputable def RegularCovering.discrete {X : Type*} [MeasurableSpace X] (C : RegularCovering X) : @RegularCovering X ⊤

Source line 29 Chapter context: Foundations

def BanditRLProof.HOO.familyDiscreteKernel 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.HOO.familyDiscreteKernel

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

noncomputable def familyDiscreteKernel {X : Type*} (law : X → Measure ℝ) : @Kernel X ℝ ⊤ (inferInstance : MeasurableSpace ℝ)

Source line 36 Chapter context: Foundations

theorem BanditRLProof.HOO.RegularCovering.expected_pseudoRegret_rate_family 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

Indexed settings: Lipschitz bandits

Canonical node identity

declaration:BanditRLProof.HOO.RegularCovering.expected_pseudoRegret_rate_family

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

theorem RegularCovering.expected_pseudoRegret_rate_family {X : Type*} [MeasurableSpace X] (C : RegularCovering X) (law : X → Measure ℝ) [∀ x, IsProbabilityMeasure (law x)] (f : X → ℝ) (best d : ℝ) (hmean : ∀ x, (∫ y, y ∂law x)=f x) (hf : ∀ x, f x≤best) (hfrange : ∀ x, f x ∈ Set.Icc (0:ℝ) 1) (hbest : regionSup f Set.univ=best) (hw : WeaklyLipschitz f C.ell best) (hbound : ∀ x, ∀ᵐ y ∂law x, y ∈ Set.Icc (0:ℝ) 1) (hd : C.nearOptimalityDimension f best (4*C.nu1/C.nu2) < (d:EReal)) : ∃ γ : ℝ, 0<γ ∧ ∀ N : ℕ, 1≤N → (∫ Y, (∑ n ∈ Finset.range N, (best-f (C.toCovering.arm C.nu1 C.rho Y n))) ∂trajectory C.nu1 C.rho (C.toCovering.familyNodeLaw law)) ≤ γ*(N:ℝ)^((d+1)/(d+2))*(Real.log (max (N:ℝ) 2))^(1/(d+2))

Source line 45 Chapter context: Foundations

theorem BanditRLProof.HOO.RegularCovering.expected_actual_eq_pseudoRegret_family 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

Indexed settings: Lipschitz bandits

Canonical node identity

declaration:BanditRLProof.HOO.RegularCovering.expected_actual_eq_pseudoRegret_family

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

theorem RegularCovering.expected_actual_eq_pseudoRegret_family {X : Type*} [MeasurableSpace X] (C : RegularCovering X) (law : X → Measure ℝ) [∀ x, IsProbabilityMeasure (law x)] (f : X → ℝ) (best : ℝ) (hmean : ∀ x, (∫ y, y ∂law x)=f x) (hfrange : ∀ x, f x ∈ Set.Icc (0:ℝ) 1) (hbound : ∀ x, ∀ᵐ y ∂law x, y ∈ Set.Icc (0:ℝ) 1) (N : ℕ) : (∫ Y, (∑ n ∈ Finset.range N, (best-Y n)) ∂trajectory C.nu1 C.rho (C.toCovering.familyNodeLaw law)) = (∫ Y, (∑ n ∈ Finset.range N, (best-f (C.toCovering.arm C.nu1 C.rho Y n))) ∂trajectory C.nu1 C.rho (C.toCovering.familyNodeLaw law))

Source line 59 Chapter context: Foundations

theorem BanditRLProof.HOO.RegularCovering.expected_actualRegret_rate_family 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

Indexed settings: Lipschitz bandits

Canonical node identity

declaration:BanditRLProof.HOO.RegularCovering.expected_actualRegret_rate_family

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

theorem RegularCovering.expected_actualRegret_rate_family {X : Type*} [MeasurableSpace X] (C : RegularCovering X) (law : X → Measure ℝ) [∀ x, IsProbabilityMeasure (law x)] (f : X → ℝ) (best d : ℝ) (hmean : ∀ x, (∫ y, y ∂law x)=f x) (hf : ∀ x, f x≤best) (hfrange : ∀ x, f x ∈ Set.Icc (0:ℝ) 1) (hbest : regionSup f Set.univ=best) (hw : WeaklyLipschitz f C.ell best) (hbound : ∀ x, ∀ᵐ y ∂law x, y ∈ Set.Icc (0:ℝ) 1) (hd : C.nearOptimalityDimension f best (4*C.nu1/C.nu2) < (d:EReal)) : ∃ γ : ℝ, 0<γ ∧ ∀ N : ℕ, 1≤N → (∫ Y, (∑ n ∈ Finset.range N, (best-Y n)) ∂trajectory C.nu1 C.rho (C.toCovering.familyNodeLaw law)) ≤ γ*(N:ℝ)^((d+1)/(d+2))*(Real.log (max (N:ℝ) 2))^(1/(d+2))

Source line 71 Chapter context: Foundations