`Bandits.StreamMeasure.prob_sum_range_sub_le_le_of_HasSubgaussianMGF'`🔗

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_sum_range_sub_le_le_of_HasSubgaussianMGF'`🔗

LemmaBandits.StreamMeasure.prob_sum_range_sub_le_le_of_HasSubgaussianMGF'

Details

No docstring.

theorem

Bandits.StreamMeasure.prob_sum_range_sub_le_le_of_HasSubgaussianMGF'.{u_1}
  {𝓐 : Type u_1} {m𝓐 : MeasurableSpace 𝓐}
  {ν : ProbabilityTheory.Kernel 𝓐 ℝ}
  [ProbabilityTheory.IsMarkovKernel ν] {n : ℕ} {a : 𝓐} {σ2 : NNReal}
  (hσ2 : 0 < σ2)
  (h :
    ProbabilityTheory.HasSubgaussianMGF
      (fun x => x - ∫ (x : ℝ), id x ∂ν a) σ2 (ν a))
  {δ : ℝ} (hδ : 0 < δ) (hn : 0 < n) :
  (streamMeasure ν)
      {ω |
        ∑ k ∈ Finset.range n, (ω k a - ∫ (x : ℝ), id x ∂ν a) ≤
          -√(2 * ↑n * ↑σ2 * Real.log (1 / δ))} ≤
    ENNReal.ofReal δ
Bandits.StreamMeasure.prob_sum_range_sub_le_le_of_HasSubgaussianMGF'.{u_1}
  {𝓐 : Type u_1} {m𝓐 : MeasurableSpace 𝓐}
  {ν : ProbabilityTheory.Kernel 𝓐 ℝ}
  [ProbabilityTheory.IsMarkovKernel ν]
  {n : ℕ} {a : 𝓐} {σ2 : NNReal}
  (hσ2 : 0 < σ2)
  (h :
    ProbabilityTheory.HasSubgaussianMGF
      (fun x => x - ∫ (x : ℝ), id x ∂ν a)
      σ2 (ν a))
  {δ : ℝ} (hδ : 0 < δ) (hn : 0 < n) :
  (streamMeasure ν)
      {ω |
        ∑ k ∈ Finset.range n,
            (ω k a -
              ∫ (x : ℝ), id x ∂ν a) ≤
          -√(2 * ↑n * ↑σ2 *
                Real.log (1 / δ))} ≤
    ENNReal.ofReal δ

Code

lemma prob_sum_range_sub_le_le_of_HasSubgaussianMGF' {σ2 : ℝ≥0} (hσ2 : 0 < σ2)
    (h : HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) {δ : ℝ} (hδ : 0 < δ) (hn : 0 < n) :
    streamMeasure ν {ω | ∑ k ∈ range n, (ω k a - (ν a)[id]) ≤
      -√(2 * n * σ2 * Real.log (1 / δ))} ≤ ENNReal.ofReal δ

Type uses (1)

streamMeasure

Body uses (1)

prob_sum_range_sub_le_le_of_HasSubgaussianMGF

Used by (1)

prob_sumRewards_sub_pullCount_mul_le_le

Actions: Source · Open Issue

Proof

calc
  _ ≤ ENNReal.ofReal (Real.exp (-√(2 * n * σ2 * Real.log (1 / δ)) ^ 2 / (2 * n * σ2))) :=
    prob_sum_range_sub_le_le_of_HasSubgaussianMGF h (by positivity) n
  _ ≤ ENNReal.ofReal δ := by
    gcongr
    exact exp_neg_sqrt_sq_div_le hσ2 hδ hn

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.StreamMeasure.prob_sum_range_sub_le_le_of_HasSubgaussianMGF'🔗

prob_sum_range_sub_le_le_of_HasSubgaussianMGF'🔗

streamMeasure🔗

`Bandits.StreamMeasure.prob_sum_range_sub_le_le_of_HasSubgaussianMGF'`🔗

`prob_sum_range_sub_le_le_of_HasSubgaussianMGF'`🔗

`streamMeasure`🔗