LeanMachineLearning exposition

3.11.ย SequentialLearning.Algorithms.RandomSampling๐Ÿ”—

Random Sampling

Implementation of the Random Sampling algorithm, which samples from a fixed probability measure at each iteration.

Main definitions

  • randomSampling: The random sampling algorithm that samples from a fixed distribution at each iteration.

Main statements

  • hasLaw_action: Each action follows the distribution ฮผ.

  • iIndep_action: Actions are mutually independent across time steps.

Module LeanMachineLearning.SequentialLearning.Algorithms.RandomSampling contains 5 exposed declarations.

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)
Used by (5)

Actions: Source ยท Open Issue

randomSampling_p0๐Ÿ”—

LemmaLearning.randomSampling_p0
Details

No docstring.

๐Ÿ”—theorem
Learning.randomSampling_p0.{u_1, u_2} {๐“ : Type u_1} {๐“จ : Type u_2}
  {m๐“ : MeasurableSpace ๐“} {m๐“จ : MeasurableSpace ๐“จ}
  (ฮผ : MeasureTheory.Measure ๐“) [MeasureTheory.IsProbabilityMeasure ฮผ] :
  Algorithm.p0 (randomSampling ฮผ) = ฮผ
Learning.randomSampling_p0.{u_1, u_2}
  {๐“ : Type u_1} {๐“จ : Type u_2}
  {m๐“ : MeasurableSpace ๐“}
  {m๐“จ : MeasurableSpace ๐“จ}
  (ฮผ : MeasureTheory.Measure ๐“)
  [MeasureTheory.IsProbabilityMeasure ฮผ] :
  Algorithm.p0 (randomSampling ฮผ) = ฮผ

Code

theorem randomSampling_p0 : โˆ€ {๐“ : Type u_1} {๐“จ : Type u_2} {m๐“ : MeasurableSpace ๐“} {m๐“จ : MeasurableSpace ๐“จ} (ฮผ : MeasureTheory.Measure ๐“)
  [inst : MeasureTheory.IsProbabilityMeasure ฮผ], (Learning.randomSampling ฮผ).p0 = ฮผ
Type uses (2)
Used by (1)

Actions: Source ยท Open Issue

Proof
@[simps]

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]

hasLaw_action๐Ÿ”—

LemmaLearning.randomSampling.hasLaw_action
Details

Each action follows the distribution ฮผ.

๐Ÿ”—theorem
Learning.randomSampling.hasLaw_action.{u_1, u_2, u_3} {๐“ : Type u_1}
  {๐“จ : Type u_2} {ฮฉ : Type u_3} {m๐“ : MeasurableSpace ๐“}
  {m๐“จ : MeasurableSpace ๐“จ} {mฮฉ : MeasurableSpace ฮฉ}
  {ฮผ : MeasureTheory.Measure ๐“} [MeasureTheory.IsProbabilityMeasure ฮผ]
  {P : MeasureTheory.Measure ฮฉ} [MeasureTheory.IsProbabilityMeasure P]
  {A : โ„• โ†’ ฮฉ โ†’ ๐“} {Y : โ„• โ†’ ฮฉ โ†’ ๐“จ} {env : Environment ๐“ ๐“จ}
  (h : IsAlgEnvSeq A Y (randomSampling ฮผ) env P) (n : โ„•) :
  ProbabilityTheory.HasLaw (A n) ฮผ P
Learning.randomSampling.hasLaw_action.{u_1,
    u_2, u_3}
  {๐“ : Type u_1} {๐“จ : Type u_2}
  {ฮฉ : Type u_3} {m๐“ : MeasurableSpace ๐“}
  {m๐“จ : MeasurableSpace ๐“จ}
  {mฮฉ : MeasurableSpace ฮฉ}
  {ฮผ : MeasureTheory.Measure ๐“}
  [MeasureTheory.IsProbabilityMeasure ฮผ]
  {P : MeasureTheory.Measure ฮฉ}
  [MeasureTheory.IsProbabilityMeasure P]
  {A : โ„• โ†’ ฮฉ โ†’ ๐“} {Y : โ„• โ†’ ฮฉ โ†’ ๐“จ}
  {env : Environment ๐“ ๐“จ}
  (h :
    IsAlgEnvSeq A Y (randomSampling ฮผ) env
      P)
  (n : โ„•) :
  ProbabilityTheory.HasLaw (A n) ฮผ P

Code

lemma hasLaw_action (h : IsAlgEnvSeq A Y (randomSampling ฮผ) env P) (n : โ„•) :
    HasLaw (A n) ฮผ P
Type uses (3)
Body uses (2)
Used by (1)

Actions: Source ยท Open Issue

Proof
by
  by_cases hn : n = 0
  ยท rw [hn]
    exact h.hasLaw_action_zero
  ยท push Not at hn
    obtain โŸจk, rflโŸฉ := Nat.exists_eq_succ_of_ne_zero hn
    exact (h.hasCondDistrib_action k).hasLaw_of_const

iIndep_action๐Ÿ”—

LemmaLearning.randomSampling.iIndep_action
Details

Actions are mutually independent.

๐Ÿ”—theorem
Learning.randomSampling.iIndep_action.{u_1, u_2, u_3} {๐“ : Type u_1}
  {๐“จ : Type u_2} {ฮฉ : Type u_3} {m๐“ : MeasurableSpace ๐“}
  {m๐“จ : MeasurableSpace ๐“จ} {mฮฉ : MeasurableSpace ฮฉ}
  {ฮผ : MeasureTheory.Measure ๐“} [MeasureTheory.IsProbabilityMeasure ฮผ]
  {P : MeasureTheory.Measure ฮฉ} [MeasureTheory.IsProbabilityMeasure P]
  {A : โ„• โ†’ ฮฉ โ†’ ๐“} {Y : โ„• โ†’ ฮฉ โ†’ ๐“จ} {env : Environment ๐“ ๐“จ}
  (h : IsAlgEnvSeq A Y (randomSampling ฮผ) env P) :
  ProbabilityTheory.iIndepFun A P
Learning.randomSampling.iIndep_action.{u_1,
    u_2, u_3}
  {๐“ : Type u_1} {๐“จ : Type u_2}
  {ฮฉ : Type u_3} {m๐“ : MeasurableSpace ๐“}
  {m๐“จ : MeasurableSpace ๐“จ}
  {mฮฉ : MeasurableSpace ฮฉ}
  {ฮผ : MeasureTheory.Measure ๐“}
  [MeasureTheory.IsProbabilityMeasure ฮผ]
  {P : MeasureTheory.Measure ฮฉ}
  [MeasureTheory.IsProbabilityMeasure P]
  {A : โ„• โ†’ ฮฉ โ†’ ๐“} {Y : โ„• โ†’ ฮฉ โ†’ ๐“จ}
  {env : Environment ๐“ ๐“จ}
  (h :
    IsAlgEnvSeq A Y (randomSampling ฮผ) env
      P) :
  ProbabilityTheory.iIndepFun A P

Code

lemma iIndep_action (h : IsAlgEnvSeq A Y (randomSampling ฮผ) env P) :
    iIndepFun A P
Type uses (3)
Body uses (6)

Actions: Source ยท Open Issue

Proof
by
  have hA := h.measurable_action
  rw [iIndepFun_nat_iff_forall_indepFun (by fun_prop)]
  intro n
  have map_eq := (h.hasCondDistrib_action n).map_eq
  simp only [randomSampling_policy, Measure.compProd_const] at map_eq
  have law_eq : P.map (A (n + 1)) = ฮผ := (hasLaw_action h (n + 1)).map_eq
  rw [โ† law_eq, โ† indepFun_iff_map_prod_eq_prod_map_map] at map_eq
  ยท change A (n + 1) โŸ‚แตข[P] (fun (f : Iic n โ†’ ๐“ ร— ๐“จ) โ†ฆ (fun i โ†ฆ (f i).1))โˆ˜ (history A Y n)
    refine map_eq.symm.comp measurable_id (by fun_prop)
  ยท exact (h.measurable_history n).aemeasurable
  ยท exact (h.measurable_action (n + 1)).aemeasurable
  1. Learning.randomSampling
  2. Learning.randomSampling_p0
  3. Learning.randomSampling_policy
  4. Learning.randomSampling.hasLaw_action
  5. Learning.randomSampling.iIndep_action