`Bandits.StreamMeasure.prob_sum_range_sub_ge_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_ge_le_of_HasSubgaussianMGF`🔗

LemmaBandits.StreamMeasure.prob_sum_range_sub_ge_le_of_HasSubgaussianMGF

Details

No docstring.

theorem

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

Code

lemma prob_sum_range_sub_ge_le_of_HasSubgaussianMGF {σ2 : ℝ≥0}
    (h : HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) {ε : ℝ} (hε : 0 ≤ ε) (n : ℕ) :
    streamMeasure ν {ω | ε ≤ ∑ k ∈ range n, (ω k a - (ν a)[id])} ≤
      ENNReal.ofReal (Real.exp (-ε ^ 2 / (2 * n * σ2)))

Type uses (1)

streamMeasure

Body uses (3)

Used by (1)

prob_sum_range_sub_ge_le_of_HasSubgaussianMGF'

Actions: Source · Open Issue

Proof

by
  rw [← ofReal_measureReal]
  gcongr
  apply HasSubgaussianMGF.measure_sum_range_ge_le_of_iIndepFun _ _ hε
  · exact (iIndepFun_eval_streamMeasure'' ν a).comp (fun _ x ↦ x - (ν a)[id]) (by fun_prop)
  · intro _ _
    exact h.congr_identDistrib ((identDistrib_eval_eval_id_streamMeasure _ _ _).symm.sub_const _)

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_ge_le_of_HasSubgaussianMGF🔗

prob_sum_range_sub_ge_le_of_HasSubgaussianMGF🔗

streamMeasure🔗

`Bandits.StreamMeasure.prob_sum_range_sub_ge_le_of_HasSubgaussianMGF`🔗

`prob_sum_range_sub_ge_le_of_HasSubgaussianMGF`🔗

`streamMeasure`🔗