LeanMachineLearning exposition

Learning.Algorithm.measurable_densityπŸ”—

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

measurable_densityπŸ”—

LemmaLearning.Algorithm.measurable_density
Details

No docstring.

πŸ”—theorem
Learning.Algorithm.measurable_density.{u_1, u_2} {𝓐 : Type u_1}
  {𝓨 : Type u_2} [MeasurableSpace 𝓐] [MeasurableSpace 𝓨]
  [MeasurableSpace.CountablyGenerated 𝓐] (alg algβ‚€ : Algorithm 𝓐 𝓨)
  (n : β„•) : Measurable (density alg algβ‚€ n)
Learning.Algorithm.measurable_density.{u_1,
    u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  [MeasurableSpace 𝓐] [MeasurableSpace 𝓨]
  [MeasurableSpace.CountablyGenerated 𝓐]
  (alg algβ‚€ : Algorithm 𝓐 𝓨) (n : β„•) :
  Measurable (density alg algβ‚€ n)

Code

lemma measurable_density [MeasurableSpace.CountablyGenerated 𝓐] (alg algβ‚€ : Algorithm 𝓐 𝓨) (n : β„•) :
    Measurable (alg.density algβ‚€ n)
Type uses (2)
Body uses (1)
Used by (4)

Actions: Source Β· Open Issue

Proof
by
  induction n with
  | zero => simp_rw [density]; fun_prop
  | succ n ih => simp_rw [density]; fun_prop

Dependency graph

Type dependencies (2)

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

densityπŸ”—

DefinitionLearning.Algorithm.density
Details

If the algorithm alg is absolutely continuous with respect to the algorithm algβ‚€ and they are both interacting with the same environment, then the law of the history at time n under alg is the law of the history at time n under algβ‚€ with density alg.density algβ‚€ n.

πŸ”—def
Learning.Algorithm.density.{u_1, u_2} {𝓐 : Type u_1} {𝓨 : Type u_2}
  [MeasurableSpace 𝓐] [MeasurableSpace 𝓨]
  [MeasurableSpace.CountablyGenerated 𝓐] (alg algβ‚€ : Algorithm 𝓐 𝓨)
  (n : β„•) : (β†₯(Finset.Iic n) β†’ 𝓐 Γ— 𝓨) β†’ ENNReal
Learning.Algorithm.density.{u_1, u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  [MeasurableSpace 𝓐] [MeasurableSpace 𝓨]
  [MeasurableSpace.CountablyGenerated 𝓐]
  (alg algβ‚€ : Algorithm 𝓐 𝓨) (n : β„•) :
  (β†₯(Finset.Iic n) β†’ 𝓐 Γ— 𝓨) β†’ ENNReal

Code

noncomputable
def density [MeasurableSpace.CountablyGenerated 𝓐] (alg algβ‚€ : Algorithm 𝓐 𝓨) :
    (n : β„•) β†’ (Iic n β†’ 𝓐 Γ— 𝓨) β†’ ℝβ‰₯0∞
  | 0, h => (alg.p0.rnDeriv algβ‚€.p0 (h ⟨0, by simp⟩).1)
  | n + 1, h =>
    let p := MeasurableEquiv.IicSuccProd (fun _ ↦ 𝓐 Γ— 𝓨) n h
    alg.density algβ‚€ n p.1 * (alg.policy n).rnDeriv (algβ‚€.policy n) p.1 p.2.1
Type uses (1)
Body uses (1)
Used by (5)

Actions: Source Β· Open Issue

All dependencies, transitively (1)

IicSuccProdπŸ”—

DefinitionMeasurableEquiv.IicSuccProd
Details

Measurable equivalence between a product up to n + 1 and the pair of the product up to n and the space at n + 1.

πŸ”—def
MeasurableEquiv.IicSuccProd.{u_3} (X : β„• β†’ Type u_3)
  [(n : β„•) β†’ MeasurableSpace (X n)] (n : β„•) :
  ((i : β†₯(Finset.Iic (n + 1))) β†’ X ↑i) ≃ᡐ
    ((i : β†₯(Finset.Iic n)) β†’ X ↑i) Γ— X (n + 1)
MeasurableEquiv.IicSuccProd.{u_3}
  (X : β„• β†’ Type u_3)
  [(n : β„•) β†’ MeasurableSpace (X n)]
  (n : β„•) :
  ((i : β†₯(Finset.Iic (n + 1))) β†’ X ↑i) ≃ᡐ
    ((i : β†₯(Finset.Iic n)) β†’ X ↑i) Γ—
      X (n + 1)

Code

def _root_.MeasurableEquiv.IicSuccProd (X : β„• β†’ Type*) [βˆ€ n, MeasurableSpace (X n)] (n : β„•) :
    MeasurableEquiv (Ξ  i : Iic (n + 1), X i) ((Ξ  i : Iic n, X i) Γ— X (n + 1)) :=
  (MeasurableEquiv.IicProdIoc (Nat.le_succ n)).symm.trans
    (MeasurableEquiv.prodCongr (MeasurableEquiv.refl _) (MeasurableEquiv.piSingleton n).symm)
Used by (11)

Actions: Source Β· Open Issue