`Bandits.prob_avg_add_sqrt_log_le`🔗

This page has the declaration's own card below, then its dependency graph, then a card for each dependency (type dependencies first, then the rest of the transitive closure). For a theorem, the graph and the dependency cards only follow its statement's dependencies (its proof is replaced by sorry, so what it proves doesn't depend on how); for everything else, both the type and the body/value are followed, since their content is part of what later declarations build on.

Minimal Lean file

`prob_avg_add_sqrt_log_le`🔗

LemmaBandits.prob_avg_add_sqrt_log_le

Details

No docstring.

theorem

Bandits.prob_avg_add_sqrt_log_le.{u_1} {𝓐 : Type u_1}
  {m𝓐 : MeasurableSpace 𝓐} {ν : ProbabilityTheory.Kernel 𝓐 ℝ}
  [ProbabilityTheory.IsMarkovKernel ν] {σ2 : NNReal} {c : ℝ}
  (hν :
    ∀ (a : 𝓐),
      ProbabilityTheory.HasSubgaussianMGF
        (fun x => x - ∫ (x : ℝ), id x ∂ν a) σ2 (ν a))
  (hσ2 : σ2 ≠ 0) (hc : 0 ≤ c) (a : 𝓐) (n k : ℕ) (hk : k ≠ 0) :
  (streamMeasure ν)
      {ω |
        (∑ m ∈ Finset.range k, ω m a) / ↑k +
            √(2 * c * ↑σ2 * Real.log (↑n + 1) / ↑k) ≤
          ∫ (x : ℝ), id x ∂ν a} ≤
    1 / (↑n + 1) ^ c
Bandits.prob_avg_add_sqrt_log_le.{u_1}
  {𝓐 : Type u_1} {m𝓐 : MeasurableSpace 𝓐}
  {ν : ProbabilityTheory.Kernel 𝓐 ℝ}
  [ProbabilityTheory.IsMarkovKernel ν]
  {σ2 : NNReal} {c : ℝ}
  (hν :
    ∀ (a : 𝓐),
      ProbabilityTheory.HasSubgaussianMGF
        (fun x =>
          x - ∫ (x : ℝ), id x ∂ν a)
        σ2 (ν a))
  (hσ2 : σ2 ≠ 0) (hc : 0 ≤ c) (a : 𝓐)
  (n k : ℕ) (hk : k ≠ 0) :
  (streamMeasure ν)
      {ω |
        (∑ m ∈ Finset.range k, ω m a) /
              ↑k +
            √(2 * c * ↑σ2 *
                  Real.log (↑n + 1) /
                ↑k) ≤
          ∫ (x : ℝ), id x ∂ν a} ≤
    1 / (↑n + 1) ^ c

Code

lemma prob_avg_add_sqrt_log_le {σ2 : ℝ≥0} {c : ℝ}
    (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (hσ2 : σ2 ≠ 0)
    (hc : 0 ≤ c) (a : 𝓐) (n k : ℕ) (hk : k ≠ 0) :
    streamMeasure ν {ω | (∑ m ∈ range k, ω m a) / k + √(2 * c * σ2 * log (n + 1) / k) ≤ (ν a)[id]} ≤
      1 / (n + 1) ^ c

Type uses (1)

streamMeasure

Body uses (1)

prob_sum_le_sqrt_log

Used by (1)

prob_ucbIndex_le

Actions: Source · Open Issue

Proof

by
  have h_log_nonneg : 0 ≤ log (n + 1) := log_nonneg (by simp)
  calc
    streamMeasure ν {ω | (∑ m ∈ range k, ω m a) / k + √(2 * c * σ2 * log (n + 1) / k) ≤ (ν a)[id]}
  _ = streamMeasure ν
      {ω | (∑ s ∈ range k, (ω s a - (ν a)[id])) / k ≤ - √(2 * c * σ2 * log (n + 1) / k)} := by
    congr with ω
    field_simp
    rw [Finset.sum_sub_distrib]
    simp
    grind
  _ = streamMeasure ν
      {ω | (∑ s ∈ range k, (ω s a - (ν a)[id])) ≤ - √(2 * c * k * σ2 * log (n + 1))} := by
    congr with ω
    field_simp
    congr! 2
    rw [sqrt_div (by positivity), ← mul_div_assoc, mul_comm, mul_div_assoc, div_sqrt,
      mul_assoc (k : ℝ), mul_assoc (k : ℝ), mul_assoc (k : ℝ),
      sqrt_mul (x := (k : ℝ)) (by positivity), mul_comm]
  _ ≤ 1 / (n + 1) ^ c := prob_sum_le_sqrt_log hν hσ2 hc a k hk

Dependency graph

Type dependencies (1)

`streamMeasure`🔗

DefinitionBandits.streamMeasure

Details

Measure of an infinite stream of rewards from each action.

def

Bandits.streamMeasure.{u_1, u_2} {𝓐 : Type u_1} {R : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐} {mR : MeasurableSpace R}
  (ν : ProbabilityTheory.Kernel 𝓐 R) : MeasureTheory.Measure (ℕ → 𝓐 → R)
Bandits.streamMeasure.{u_1, u_2}
  {𝓐 : Type u_1} {R : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {mR : MeasurableSpace R}
  (ν : ProbabilityTheory.Kernel 𝓐 R) :
  MeasureTheory.Measure (ℕ → 𝓐 → R)

Code

noncomputable
def streamMeasure (ν : Kernel 𝓐 R) : Measure (ℕ → 𝓐 → R) :=
  Measure.infinitePi fun _ ↦ Measure.infinitePi ν

Used by (56)

Actions: Source · Open Issue

Bandits.prob_avg_add_sqrt_log_le🔗

prob_avg_add_sqrt_log_le🔗

streamMeasure🔗

`Bandits.prob_avg_add_sqrt_log_le`🔗

`prob_avg_add_sqrt_log_le`🔗

`streamMeasure`🔗