`Learning.randomSampling_policy`🔗

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

`randomSampling_policy`🔗

LemmaLearning.randomSampling_policy

Details

No docstring.

theorem

Learning.randomSampling_policy.{u_1, u_2} {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨}
  (μ : MeasureTheory.Measure 𝓐) [MeasureTheory.IsProbabilityMeasure μ]
  (x✝ : ℕ) :
  Algorithm.policy (randomSampling μ) x✝ =
    ProbabilityTheory.Kernel.const (↥(Finset.Iic x✝) → 𝓐 × 𝓨) μ
Learning.randomSampling_policy.{u_1, u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨}
  (μ : MeasureTheory.Measure 𝓐)
  [MeasureTheory.IsProbabilityMeasure μ]
  (x✝ : ℕ) :
  Algorithm.policy (randomSampling μ) x✝ =
    ProbabilityTheory.Kernel.const
      (↥(Finset.Iic x✝) → 𝓐 × 𝓨) μ

Code

theorem randomSampling_policy : ∀ {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (μ : MeasureTheory.Measure 𝓐)
  [inst : MeasureTheory.IsProbabilityMeasure μ] (x : ℕ),
  (Learning.randomSampling μ).policy x = ProbabilityTheory.Kernel.const (↥(Finset.Iic x) → 𝓐 × 𝓨) μ

Type uses (2)

Used by (2)

Actions: Source · Open Issue

Proof

@[simps]

Dependency graph

Type dependencies (2)

`randomSampling`🔗

DefinitionLearning.randomSampling

Details

The Random Sampling algorithm, which samples from a fixed probability measure at each iteration.

def

Learning.randomSampling.{u_1, u_2} {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨}
  (μ : MeasureTheory.Measure 𝓐) [MeasureTheory.IsProbabilityMeasure μ] :
  Algorithm 𝓐 𝓨
Learning.randomSampling.{u_1, u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨}
  (μ : MeasureTheory.Measure 𝓐)
  [MeasureTheory.IsProbabilityMeasure μ] :
  Algorithm 𝓐 𝓨

Code

noncomputable def randomSampling (μ : Measure 𝓐) [IsProbabilityMeasure μ] : Algorithm 𝓐 𝓨 where
  policy _ := Kernel.const _ μ
  p0 := μ

Type uses (1)

Algorithm

Used by (5)

Actions: Source · Open Issue

`Algorithm`🔗

StructureLearning.Algorithm

Details

A stochastic, sequential algorithm.

structure

Learning.Algorithm.{u_4, u_5} (𝓐 : Type u_4) (𝓨 : Type u_5)
  [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] : Type (max u_4 u_5)
Learning.Algorithm.{u_4, u_5}
  (𝓐 : Type u_4) (𝓨 : Type u_5)
  [MeasurableSpace 𝓐]
  [MeasurableSpace 𝓨] : Type (max u_4 u_5)

Code

structure Algorithm (𝓐 𝓨 : Type*) [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] where
  /-- Policy or sampling rule: distribution of the next action. -/
  policy : (n : ℕ) → Kernel (Iic n → 𝓐 × 𝓨) 𝓐
  /-- The policy is a Markov kernel. -/
  [h_policy : ∀ n, IsMarkovKernel (policy n)]
  /-- Distribution of the first action. -/
  p0 : Measure 𝓐
  /-- The first action distribution is a probability measure. -/
  [hp0 : IsProbabilityMeasure p0]

Used by (216)

Actions: Source · Open Issue

Learning.randomSampling_policy🔗

randomSampling_policy🔗

randomSampling🔗

Algorithm🔗

`Learning.randomSampling_policy`🔗

`randomSampling_policy`🔗

`randomSampling`🔗

`Algorithm`🔗