LeanMachineLearning exposition

Bandits.hasLaw_ZπŸ”—

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

hasLaw_ZπŸ”—

LemmaBandits.hasLaw_Z
Details

No docstring.

πŸ”—theorem
Bandits.hasLaw_Z.{u_1, u_2} {𝓐 : Type u_1} {Ξ© : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐} {mΞ© : MeasurableSpace Ξ©}
  {P : MeasureTheory.Measure Ξ©} [MeasureTheory.IsProbabilityMeasure P]
  {Ξ½ : ProbabilityTheory.Kernel 𝓐 ℝ}
  [ProbabilityTheory.IsMarkovKernel Ξ½] (a : 𝓐) (m : β„•) :
  ProbabilityTheory.HasLaw (fun Ο‰ => Prod.snd Ο‰ m a) (Ξ½ a)
    (MeasureTheory.Measure.prod P (streamMeasure Ξ½))
Bandits.hasLaw_Z.{u_1, u_2} {𝓐 : Type u_1}
  {Ξ© : Type u_2} {m𝓐 : MeasurableSpace 𝓐}
  {mΞ© : MeasurableSpace Ξ©}
  {P : MeasureTheory.Measure Ξ©}
  [MeasureTheory.IsProbabilityMeasure P]
  {Ξ½ : ProbabilityTheory.Kernel 𝓐 ℝ}
  [ProbabilityTheory.IsMarkovKernel Ξ½]
  (a : 𝓐) (m : β„•) :
  ProbabilityTheory.HasLaw
    (fun Ο‰ => Prod.snd Ο‰ m a) (Ξ½ a)
    (MeasureTheory.Measure.prod P
      (streamMeasure Ξ½))

Code

lemma hasLaw_Z (a : 𝓐) (m : β„•) :
  HasLaw (fun Ο‰ ↦ Ο‰.2 m a) (Ξ½ a) 𝔓 where
  map_eq
Type uses (1)
Body uses (1)
Used by (1)

Actions: Source Β· Open Issue

Proof
by
    calc (𝔓).map (fun Ο‰ ↦ Ο‰.2 m a)
    _ = ((𝔓).snd).map (fun Ο‰ ↦ Ο‰ m a) := by
      rw [Measure.snd, Measure.map_map (by fun_prop) (by fun_prop)]
      rfl
    _ = (streamMeasure Ξ½).map (fun Ο‰ ↦ Ο‰ m a) := by simp
    _ = ((Measure.infinitePi fun _ ↦ Measure.infinitePi Ξ½).map (fun Ο‰ ↦ Ο‰ m)).map
        (fun Ο‰ ↦ Ο‰ a) := by
      rw [streamMeasure, Measure.map_map (by fun_prop) (by fun_prop)]
      rfl
    _ = Ξ½ a := by simp_rw [(measurePreserving_eval_infinitePi _ _).map_eq]

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