LeanMachineLearning exposition

3.12.ย SequentialLearning.EvaluationEnv๐Ÿ”—

Function evaluation environments

We define two environments, onlineEvalEnv and evalEnv, where the feedback is given by evaluating a measurable function at the chosen action. The first one allows the function to change at every time step, while the second one uses a fixed function at every time step.

Main definitions

  • onlineEvalEnv g hg: A stationary environment where the feedback at time n is given by a deterministic kernel that evaluates the measurable function g n at the chosen action.

  • evalEnv f hf: A stationary environment where the feedback is given by a deterministic kernel that evaluates a fixed measurable function f at the chosen action.

They both satisfy the typeclasses IsObliviousEnv and IsDeterministicEnv.

Main statements

  • forall_feedback_onlineEvalEnv_ae_eq_eval_action: For almost all ฯ‰, the feedback at time n is equal to g n evaluated at the action taken at time n.

  • forall_feedback_evalEnv_ae_eq_eval_action: For almost all ฯ‰, the feedback at time n is equal to f evaluated at the action taken at time n.

Module LeanMachineLearning.SequentialLearning.EvaluationEnv contains 19 exposed declarations.

onlineEvalEnv๐Ÿ”—

DefinitionLearning.onlineEvalEnv
Details

The evaluation environment where the feedback is given by evaluating a fixed measurable function f at the chosen action.

๐Ÿ”—def
Learning.onlineEvalEnv.{u_1, u_2} {๐“ : Type u_1} {๐“จ : Type u_2}
  {m๐“ : MeasurableSpace ๐“} {m๐“จ : MeasurableSpace ๐“จ} (g : โ„• โ†’ ๐“ โ†’ ๐“จ)
  (hg : โˆ€ (n : โ„•), Measurable (g n)) : Environment ๐“ ๐“จ
Learning.onlineEvalEnv.{u_1, u_2}
  {๐“ : Type u_1} {๐“จ : Type u_2}
  {m๐“ : MeasurableSpace ๐“}
  {m๐“จ : MeasurableSpace ๐“จ} (g : โ„• โ†’ ๐“ โ†’ ๐“จ)
  (hg : โˆ€ (n : โ„•), Measurable (g n)) :
  Environment ๐“ ๐“จ

Code

noncomputable def onlineEvalEnv (g : โ„• โ†’ ๐“ โ†’ ๐“จ) (hg : โˆ€ n, Measurable (g n)) :=
  obliviousEnv (fun n โ†ฆ Kernel.deterministic (g n) (hg n))
Type uses (1)
Body uses (1)
Used by (11)

Actions: Source ยท Open Issue

instIsObliviousEnvOnlineEvalEnv๐Ÿ”—

InstanceLearning.instIsObliviousEnvOnlineEvalEnv
Details

No docstring.

๐Ÿ”—theorem
Learning.instIsObliviousEnvOnlineEvalEnv.{u_1, u_2} {๐“ : Type u_1}
  {๐“จ : Type u_2} {m๐“ : MeasurableSpace ๐“} {m๐“จ : MeasurableSpace ๐“จ}
  {g : โ„• โ†’ ๐“ โ†’ ๐“จ} {hg : โˆ€ (n : โ„•), Measurable (g n)} :
  IsObliviousEnv (onlineEvalEnv g hg)
Learning.instIsObliviousEnvOnlineEvalEnv.{u_1,
    u_2}
  {๐“ : Type u_1} {๐“จ : Type u_2}
  {m๐“ : MeasurableSpace ๐“}
  {m๐“จ : MeasurableSpace ๐“จ} {g : โ„• โ†’ ๐“ โ†’ ๐“จ}
  {hg : โˆ€ (n : โ„•), Measurable (g n)} :
  IsObliviousEnv (onlineEvalEnv g hg)

Code

instance : IsObliviousEnv (onlineEvalEnv g hg)
Type uses (2)
Body uses (1)
Used by (3)

Actions: Source ยท Open Issue

Proof
โŸจโŸจfun n โ†ฆ Kernel.deterministic (g n) (hg n), fun _ โ†ฆ inferInstance, rfl, fun _ โ†ฆ rflโŸฉโŸฉ

instIsDeterministicEnvOnlineEvalEnv๐Ÿ”—

InstanceLearning.instIsDeterministicEnvOnlineEvalEnv
Details

No docstring.

๐Ÿ”—theorem
Learning.instIsDeterministicEnvOnlineEvalEnv.{u_1, u_2} {๐“ : Type u_1}
  {๐“จ : Type u_2} {m๐“ : MeasurableSpace ๐“} {m๐“จ : MeasurableSpace ๐“จ}
  {g : โ„• โ†’ ๐“ โ†’ ๐“จ} {hg : โˆ€ (n : โ„•), Measurable (g n)} :
  IsDeterministicEnv (onlineEvalEnv g hg)
Learning.instIsDeterministicEnvOnlineEvalEnv.{u_1,
    u_2}
  {๐“ : Type u_1} {๐“จ : Type u_2}
  {m๐“ : MeasurableSpace ๐“}
  {m๐“จ : MeasurableSpace ๐“จ} {g : โ„• โ†’ ๐“ โ†’ ๐“จ}
  {hg : โˆ€ (n : โ„•), Measurable (g n)} :
  IsDeterministicEnv (onlineEvalEnv g hg)

Code

instance : IsDeterministicEnv (onlineEvalEnv g hg) where
  exists_f0
Type uses (2)
Body uses (1)
Used by (3)

Actions: Source ยท Open Issue

Proof
โŸจg 0, hg 0, rflโŸฉ
  exists_f n := โŸจfun p โ†ฆ g (n + 1) p.2, by fun_prop, rflโŸฉ

feedbackCondAction_onlineEvalEnv๐Ÿ”—

LemmaLearning.feedbackCondAction_onlineEvalEnv
Details

No docstring.

๐Ÿ”—theorem
Learning.feedbackCondAction_onlineEvalEnv.{u_1, u_2} {๐“ : Type u_1}
  {๐“จ : Type u_2} {m๐“ : MeasurableSpace ๐“} {m๐“จ : MeasurableSpace ๐“จ}
  {g : โ„• โ†’ ๐“ โ†’ ๐“จ} {hg : โˆ€ (n : โ„•), Measurable (g n)} (n : โ„•) :
  feedbackCondAction (onlineEvalEnv g hg) n =
    ProbabilityTheory.Kernel.deterministic (g n) โ‹ฏ
Learning.feedbackCondAction_onlineEvalEnv.{u_1,
    u_2}
  {๐“ : Type u_1} {๐“จ : Type u_2}
  {m๐“ : MeasurableSpace ๐“}
  {m๐“จ : MeasurableSpace ๐“จ} {g : โ„• โ†’ ๐“ โ†’ ๐“จ}
  {hg : โˆ€ (n : โ„•), Measurable (g n)}
  (n : โ„•) :
  feedbackCondAction (onlineEvalEnv g hg)
      n =
    ProbabilityTheory.Kernel.deterministic
      (g n) โ‹ฏ

Code

lemma feedbackCondAction_onlineEvalEnv (n : โ„•) :
    feedbackCondAction (onlineEvalEnv g hg) n = Kernel.deterministic (g n) (hg n)
Type uses (3)
Body uses (1)
Used by (2)

Actions: Source ยท Open Issue

Proof
by
  simp [onlineEvalEnv]

feedbackFunZero_onlineEvalEnv๐Ÿ”—

LemmaLearning.feedbackFunZero_onlineEvalEnv
Details

No docstring.

๐Ÿ”—theorem
Learning.feedbackFunZero_onlineEvalEnv.{u_1, u_2} {๐“ : Type u_1}
  {๐“จ : Type u_2} {m๐“ : MeasurableSpace ๐“} {m๐“จ : MeasurableSpace ๐“จ}
  {g : โ„• โ†’ ๐“ โ†’ ๐“จ} {hg : โˆ€ (n : โ„•), Measurable (g n)}
  [MeasurableSpace.SeparatesPoints ๐“จ] :
  feedbackFunZero (onlineEvalEnv g hg) = g 0
Learning.feedbackFunZero_onlineEvalEnv.{u_1,
    u_2}
  {๐“ : Type u_1} {๐“จ : Type u_2}
  {m๐“ : MeasurableSpace ๐“}
  {m๐“จ : MeasurableSpace ๐“จ} {g : โ„• โ†’ ๐“ โ†’ ๐“จ}
  {hg : โˆ€ (n : โ„•), Measurable (g n)}
  [MeasurableSpace.SeparatesPoints ๐“จ] :
  feedbackFunZero (onlineEvalEnv g hg) =
    g 0

Code

lemma feedbackFunZero_onlineEvalEnv [MeasurableSpace.SeparatesPoints ๐“จ] :
    feedbackFunZero (onlineEvalEnv g hg) = g 0
Type uses (3)
Body uses (6)
Used by (1)

Actions: Source ยท Open Issue

Proof
by
  have h_eq := ฮฝ0_eq_deterministic (onlineEvalEnv g hg)
  simpa only [onlineEvalEnv, ฮฝ0_obliviousEnv, Kernel.prodMkLeft_deterministic,
    Kernel.deterministic_inj] using h_eq.symm

feedbackFun_onlineEvalEnv๐Ÿ”—

LemmaLearning.feedbackFun_onlineEvalEnv
Details

No docstring.

๐Ÿ”—theorem
Learning.feedbackFun_onlineEvalEnv.{u_1, u_2} {๐“ : Type u_1}
  {๐“จ : Type u_2} {m๐“ : MeasurableSpace ๐“} {m๐“จ : MeasurableSpace ๐“จ}
  {g : โ„• โ†’ ๐“ โ†’ ๐“จ} {hg : โˆ€ (n : โ„•), Measurable (g n)}
  [MeasurableSpace.SeparatesPoints ๐“จ] (n : โ„•) :
  feedbackFun (onlineEvalEnv g hg) n = fun p => g (n + 1) (Prod.snd p)
Learning.feedbackFun_onlineEvalEnv.{u_1,
    u_2}
  {๐“ : Type u_1} {๐“จ : Type u_2}
  {m๐“ : MeasurableSpace ๐“}
  {m๐“จ : MeasurableSpace ๐“จ} {g : โ„• โ†’ ๐“ โ†’ ๐“จ}
  {hg : โˆ€ (n : โ„•), Measurable (g n)}
  [MeasurableSpace.SeparatesPoints ๐“จ]
  (n : โ„•) :
  feedbackFun (onlineEvalEnv g hg) n =
    fun p => g (n + 1) (Prod.snd p)

Code

lemma feedbackFun_onlineEvalEnv [MeasurableSpace.SeparatesPoints ๐“จ] (n : โ„•) :
    feedbackFun (onlineEvalEnv g hg) n = fun p โ†ฆ g (n + 1) p.2
Type uses (3)
Body uses (7)
Used by (1)

Actions: Source ยท Open Issue

Proof
by
  have h_eq := feedback_eq_deterministic (onlineEvalEnv g hg) n
  simpa only [onlineEvalEnv, feedback_obliviousEnv, Kernel.prodMkLeft_deterministic,
    Kernel.deterministic_inj] using h_eq.symm

hascondDistrib_feedback_onlineEvalEnv๐Ÿ”—

LemmaLearning.hascondDistrib_feedback_onlineEvalEnv
Details

No docstring.

๐Ÿ”—theorem
Learning.hascondDistrib_feedback_onlineEvalEnv.{u_1, u_2, u_3}
  {๐“ : Type u_1} {๐“จ : Type u_2} {m๐“ : MeasurableSpace ๐“}
  {m๐“จ : MeasurableSpace ๐“จ} {ฮฉ : Type u_3} {mฮฉ : MeasurableSpace ฮฉ}
  {alg : Algorithm ๐“ ๐“จ} {g : โ„• โ†’ ๐“ โ†’ ๐“จ}
  {hg : โˆ€ (n : โ„•), Measurable (g n)} {P : MeasureTheory.Measure ฮฉ}
  [MeasureTheory.IsProbabilityMeasure P] {A : โ„• โ†’ ฮฉ โ†’ ๐“} {Y : โ„• โ†’ ฮฉ โ†’ ๐“จ}
  (h : IsAlgEnvSeq A Y alg (onlineEvalEnv g hg) P) (n : โ„•) :
  ProbabilityTheory.HasCondDistrib (Y n) (A n)
    (ProbabilityTheory.Kernel.deterministic (g n) โ‹ฏ) P
Learning.hascondDistrib_feedback_onlineEvalEnv.{u_1,
    u_2, u_3}
  {๐“ : Type u_1} {๐“จ : Type u_2}
  {m๐“ : MeasurableSpace ๐“}
  {m๐“จ : MeasurableSpace ๐“จ} {ฮฉ : Type u_3}
  {mฮฉ : MeasurableSpace ฮฉ}
  {alg : Algorithm ๐“ ๐“จ} {g : โ„• โ†’ ๐“ โ†’ ๐“จ}
  {hg : โˆ€ (n : โ„•), Measurable (g n)}
  {P : MeasureTheory.Measure ฮฉ}
  [MeasureTheory.IsProbabilityMeasure P]
  {A : โ„• โ†’ ฮฉ โ†’ ๐“} {Y : โ„• โ†’ ฮฉ โ†’ ๐“จ}
  (h :
    IsAlgEnvSeq A Y alg
      (onlineEvalEnv g hg) P)
  (n : โ„•) :
  ProbabilityTheory.HasCondDistrib (Y n)
    (A n)
    (ProbabilityTheory.Kernel.deterministic
      (g n) โ‹ฏ)
    P

Code

lemma hascondDistrib_feedback_onlineEvalEnv
    (h : IsAlgEnvSeq A Y alg (onlineEvalEnv g hg) P) (n : โ„•) :
    HasCondDistrib (Y n) (A n) (Kernel.deterministic (g n) (hg n)) P
Type uses (3)
Body uses (4)
Used by (1)

Actions: Source ยท Open Issue

Proof
by
  simpa using IsObliviousEnv.hasCondDistrib_feedback h n

feedback_onlineEvalEnv_ae_eq_eval_action๐Ÿ”—

LemmaLearning.feedback_onlineEvalEnv_ae_eq_eval_action
Details

No docstring.

๐Ÿ”—theorem
Learning.feedback_onlineEvalEnv_ae_eq_eval_action.{u_1, u_2, u_3}
  {๐“ : Type u_1} {๐“จ : Type u_2} {m๐“ : MeasurableSpace ๐“}
  {m๐“จ : MeasurableSpace ๐“จ} {ฮฉ : Type u_3} {mฮฉ : MeasurableSpace ฮฉ}
  {alg : Algorithm ๐“ ๐“จ} {g : โ„• โ†’ ๐“ โ†’ ๐“จ}
  {hg : โˆ€ (n : โ„•), Measurable (g n)} {P : MeasureTheory.Measure ฮฉ}
  [MeasureTheory.IsProbabilityMeasure P] {A : โ„• โ†’ ฮฉ โ†’ ๐“} {Y : โ„• โ†’ ฮฉ โ†’ ๐“จ}
  [StandardBorelSpace ๐“จ] [Nonempty ๐“จ]
  (h : IsAlgEnvSeq A Y alg (onlineEvalEnv g hg) P) (n : โ„•) :
  Y n =แต[P] g n โˆ˜ A n
Learning.feedback_onlineEvalEnv_ae_eq_eval_action.{u_1,
    u_2, u_3}
  {๐“ : Type u_1} {๐“จ : Type u_2}
  {m๐“ : MeasurableSpace ๐“}
  {m๐“จ : MeasurableSpace ๐“จ} {ฮฉ : Type u_3}
  {mฮฉ : MeasurableSpace ฮฉ}
  {alg : Algorithm ๐“ ๐“จ} {g : โ„• โ†’ ๐“ โ†’ ๐“จ}
  {hg : โˆ€ (n : โ„•), Measurable (g n)}
  {P : MeasureTheory.Measure ฮฉ}
  [MeasureTheory.IsProbabilityMeasure P]
  {A : โ„• โ†’ ฮฉ โ†’ ๐“} {Y : โ„• โ†’ ฮฉ โ†’ ๐“จ}
  [StandardBorelSpace ๐“จ] [Nonempty ๐“จ]
  (h :
    IsAlgEnvSeq A Y alg
      (onlineEvalEnv g hg) P)
  (n : โ„•) : Y n =แต[P] g n โˆ˜ A n

Code

lemma feedback_onlineEvalEnv_ae_eq_eval_action [StandardBorelSpace ๐“จ] [Nonempty ๐“จ]
    (h : IsAlgEnvSeq A Y alg (onlineEvalEnv g hg) P) (n : โ„•) :
    Y n =แต[P] g n โˆ˜ A n
Type uses (3)
Body uses (4)
Used by (2)

Actions: Source ยท Open Issue

Proof
ae_eq_of_condDistrib_eq_deterministic (hg n) (h.measurable_action n).aemeasurable
    (h.measurable_feedback n).aemeasurable
    (hascondDistrib_feedback_onlineEvalEnv h n).condDistrib_eq

forall_feedback_onlineEvalEnv_ae_eq_eval_action๐Ÿ”—

LemmaLearning.forall_feedback_onlineEvalEnv_ae_eq_eval_action
Details

No docstring.

๐Ÿ”—theorem
Learning.forall_feedback_onlineEvalEnv_ae_eq_eval_action.{u_1, u_2, u_3}
  {๐“ : Type u_1} {๐“จ : Type u_2} {m๐“ : MeasurableSpace ๐“}
  {m๐“จ : MeasurableSpace ๐“จ} {ฮฉ : Type u_3} {mฮฉ : MeasurableSpace ฮฉ}
  {alg : Algorithm ๐“ ๐“จ} {g : โ„• โ†’ ๐“ โ†’ ๐“จ}
  {hg : โˆ€ (n : โ„•), Measurable (g n)} {P : MeasureTheory.Measure ฮฉ}
  [MeasureTheory.IsProbabilityMeasure P] {A : โ„• โ†’ ฮฉ โ†’ ๐“} {Y : โ„• โ†’ ฮฉ โ†’ ๐“จ}
  [StandardBorelSpace ๐“จ] [Nonempty ๐“จ]
  (h : IsAlgEnvSeq A Y alg (onlineEvalEnv g hg) P) :
  โˆ€แต (ฯ‰ : ฮฉ) โˆ‚P, โˆ€ (n : โ„•), Y n ฯ‰ = g n (A n ฯ‰)
Learning.forall_feedback_onlineEvalEnv_ae_eq_eval_action.{u_1,
    u_2, u_3}
  {๐“ : Type u_1} {๐“จ : Type u_2}
  {m๐“ : MeasurableSpace ๐“}
  {m๐“จ : MeasurableSpace ๐“จ} {ฮฉ : Type u_3}
  {mฮฉ : MeasurableSpace ฮฉ}
  {alg : Algorithm ๐“ ๐“จ} {g : โ„• โ†’ ๐“ โ†’ ๐“จ}
  {hg : โˆ€ (n : โ„•), Measurable (g n)}
  {P : MeasureTheory.Measure ฮฉ}
  [MeasureTheory.IsProbabilityMeasure P]
  {A : โ„• โ†’ ฮฉ โ†’ ๐“} {Y : โ„• โ†’ ฮฉ โ†’ ๐“จ}
  [StandardBorelSpace ๐“จ] [Nonempty ๐“จ]
  (h :
    IsAlgEnvSeq A Y alg
      (onlineEvalEnv g hg) P) :
  โˆ€แต (ฯ‰ : ฮฉ) โˆ‚P,
    โˆ€ (n : โ„•), Y n ฯ‰ = g n (A n ฯ‰)

Code

lemma forall_feedback_onlineEvalEnv_ae_eq_eval_action [StandardBorelSpace ๐“จ] [Nonempty ๐“จ]
    (h : IsAlgEnvSeq A Y alg (onlineEvalEnv g hg) P) :
    โˆ€แต ฯ‰ โˆ‚P, โˆ€ n, Y n ฯ‰ = g n (A n ฯ‰)
Type uses (3)
Body uses (1)
Used by (1)

Actions: Source ยท Open Issue

Proof
by
  rw [ae_all_iff]
  intro n
  exact feedback_onlineEvalEnv_ae_eq_eval_action h n

evalEnv๐Ÿ”—

DefinitionLearning.evalEnv
Details

The evaluation environment where the feedback is given by evaluating a fixed measurable function f at the chosen action.

๐Ÿ”—def
Learning.evalEnv.{u_1, u_2} {๐“ : Type u_1} {๐“จ : Type u_2}
  {m๐“ : MeasurableSpace ๐“} {m๐“จ : MeasurableSpace ๐“จ} (f : ๐“ โ†’ ๐“จ)
  (hf : Measurable f) : Environment ๐“ ๐“จ
Learning.evalEnv.{u_1, u_2} {๐“ : Type u_1}
  {๐“จ : Type u_2} {m๐“ : MeasurableSpace ๐“}
  {m๐“จ : MeasurableSpace ๐“จ} (f : ๐“ โ†’ ๐“จ)
  (hf : Measurable f) : Environment ๐“ ๐“จ

Code

noncomputable def evalEnv (f : ๐“ โ†’ ๐“จ) (hf : Measurable f) := onlineEvalEnv (fun _ โ†ฆ f) (fun _ โ†ฆ hf)
Type uses (1)
Body uses (1)
Used by (9)

Actions: Source ยท Open Issue

instIsObliviousEnvEvalEnv๐Ÿ”—

InstanceLearning.instIsObliviousEnvEvalEnv
Details

No docstring.

๐Ÿ”—theorem
Learning.instIsObliviousEnvEvalEnv.{u_1, u_2} {๐“ : Type u_1}
  {๐“จ : Type u_2} {m๐“ : MeasurableSpace ๐“} {m๐“จ : MeasurableSpace ๐“จ}
  {f : ๐“ โ†’ ๐“จ} {hf : Measurable f} : IsObliviousEnv (evalEnv f hf)
Learning.instIsObliviousEnvEvalEnv.{u_1,
    u_2}
  {๐“ : Type u_1} {๐“จ : Type u_2}
  {m๐“ : MeasurableSpace ๐“}
  {m๐“จ : MeasurableSpace ๐“จ} {f : ๐“ โ†’ ๐“จ}
  {hf : Measurable f} :
  IsObliviousEnv (evalEnv f hf)

Code

instance : IsObliviousEnv (evalEnv f hf)
Type uses (2)
Body uses (2)
Used by (2)

Actions: Source ยท Open Issue

Proof
by unfold evalEnv; infer_instance

instIsDeterministicEnvEvalEnv๐Ÿ”—

InstanceLearning.instIsDeterministicEnvEvalEnv
Details

No docstring.

๐Ÿ”—theorem
Learning.instIsDeterministicEnvEvalEnv.{u_1, u_2} {๐“ : Type u_1}
  {๐“จ : Type u_2} {m๐“ : MeasurableSpace ๐“} {m๐“จ : MeasurableSpace ๐“จ}
  {f : ๐“ โ†’ ๐“จ} {hf : Measurable f} : IsDeterministicEnv (evalEnv f hf)
Learning.instIsDeterministicEnvEvalEnv.{u_1,
    u_2}
  {๐“ : Type u_1} {๐“จ : Type u_2}
  {m๐“ : MeasurableSpace ๐“}
  {m๐“จ : MeasurableSpace ๐“จ} {f : ๐“ โ†’ ๐“จ}
  {hf : Measurable f} :
  IsDeterministicEnv (evalEnv f hf)

Code

instance : IsDeterministicEnv (evalEnv f hf)
Type uses (2)
Body uses (2)
Used by (2)

Actions: Source ยท Open Issue

Proof
by unfold evalEnv; infer_instance

feedbackCondAction_evalEnv๐Ÿ”—

LemmaLearning.feedbackCondAction_evalEnv
Details

No docstring.

๐Ÿ”—theorem
Learning.feedbackCondAction_evalEnv.{u_1, u_2} {๐“ : Type u_1}
  {๐“จ : Type u_2} {m๐“ : MeasurableSpace ๐“} {m๐“จ : MeasurableSpace ๐“จ}
  {f : ๐“ โ†’ ๐“จ} {hf : Measurable f} (n : โ„•) :
  feedbackCondAction (evalEnv f hf) n =
    ProbabilityTheory.Kernel.deterministic f hf
Learning.feedbackCondAction_evalEnv.{u_1,
    u_2}
  {๐“ : Type u_1} {๐“จ : Type u_2}
  {m๐“ : MeasurableSpace ๐“}
  {m๐“จ : MeasurableSpace ๐“จ} {f : ๐“ โ†’ ๐“จ}
  {hf : Measurable f} (n : โ„•) :
  feedbackCondAction (evalEnv f hf) n =
    ProbabilityTheory.Kernel.deterministic
      f hf

Code

lemma feedbackCondAction_evalEnv (n : โ„•) :
    feedbackCondAction (evalEnv f hf) n = Kernel.deterministic f hf
Type uses (3)
Body uses (1)
Used by (1)

Actions: Source ยท Open Issue

Proof
by simp [evalEnv]

feedbackFunZero_evalEnv๐Ÿ”—

LemmaLearning.feedbackFunZero_evalEnv
Details

No docstring.

๐Ÿ”—theorem
Learning.feedbackFunZero_evalEnv.{u_1, u_2} {๐“ : Type u_1}
  {๐“จ : Type u_2} {m๐“ : MeasurableSpace ๐“} {m๐“จ : MeasurableSpace ๐“จ}
  {f : ๐“ โ†’ ๐“จ} {hf : Measurable f} [MeasurableSpace.SeparatesPoints ๐“จ] :
  feedbackFunZero (evalEnv f hf) = f
Learning.feedbackFunZero_evalEnv.{u_1,
    u_2}
  {๐“ : Type u_1} {๐“จ : Type u_2}
  {m๐“ : MeasurableSpace ๐“}
  {m๐“จ : MeasurableSpace ๐“จ} {f : ๐“ โ†’ ๐“จ}
  {hf : Measurable f}
  [MeasurableSpace.SeparatesPoints ๐“จ] :
  feedbackFunZero (evalEnv f hf) = f

Code

lemma feedbackFunZero_evalEnv [MeasurableSpace.SeparatesPoints ๐“จ] :
    feedbackFunZero (evalEnv f hf) = f
Type uses (3)
Body uses (1)

Actions: Source ยท Open Issue

Proof
by simp [evalEnv]

feedbackFun_evalEnv๐Ÿ”—

LemmaLearning.feedbackFun_evalEnv
Details

No docstring.

๐Ÿ”—theorem
Learning.feedbackFun_evalEnv.{u_1, u_2} {๐“ : Type u_1} {๐“จ : Type u_2}
  {m๐“ : MeasurableSpace ๐“} {m๐“จ : MeasurableSpace ๐“จ} {f : ๐“ โ†’ ๐“จ}
  {hf : Measurable f} [MeasurableSpace.SeparatesPoints ๐“จ] (n : โ„•) :
  feedbackFun (evalEnv f hf) n = fun p => f (Prod.snd p)
Learning.feedbackFun_evalEnv.{u_1, u_2}
  {๐“ : Type u_1} {๐“จ : Type u_2}
  {m๐“ : MeasurableSpace ๐“}
  {m๐“จ : MeasurableSpace ๐“จ} {f : ๐“ โ†’ ๐“จ}
  {hf : Measurable f}
  [MeasurableSpace.SeparatesPoints ๐“จ]
  (n : โ„•) :
  feedbackFun (evalEnv f hf) n = fun p =>
    f (Prod.snd p)

Code

lemma feedbackFun_evalEnv [MeasurableSpace.SeparatesPoints ๐“จ] (n : โ„•) :
    feedbackFun (evalEnv f hf) n = fun p โ†ฆ f p.2
Type uses (3)
Body uses (1)

Actions: Source ยท Open Issue

Proof
by simp [evalEnv]

hascondDistrib_feedback_evalEnv๐Ÿ”—

LemmaLearning.hascondDistrib_feedback_evalEnv
Details

No docstring.

๐Ÿ”—theorem
Learning.hascondDistrib_feedback_evalEnv.{u_1, u_2, u_3} {๐“ : Type u_1}
  {๐“จ : Type u_2} {m๐“ : MeasurableSpace ๐“} {m๐“จ : MeasurableSpace ๐“จ}
  {ฮฉ : Type u_3} {mฮฉ : MeasurableSpace ฮฉ} {alg : Algorithm ๐“ ๐“จ}
  {f : ๐“ โ†’ ๐“จ} {hf : Measurable f} {P : MeasureTheory.Measure ฮฉ}
  [MeasureTheory.IsProbabilityMeasure P] {A : โ„• โ†’ ฮฉ โ†’ ๐“} {Y : โ„• โ†’ ฮฉ โ†’ ๐“จ}
  (h : IsAlgEnvSeq A Y alg (evalEnv f hf) P) (n : โ„•) :
  ProbabilityTheory.HasCondDistrib (Y n) (A n)
    (ProbabilityTheory.Kernel.deterministic f hf) P
Learning.hascondDistrib_feedback_evalEnv.{u_1,
    u_2, u_3}
  {๐“ : Type u_1} {๐“จ : Type u_2}
  {m๐“ : MeasurableSpace ๐“}
  {m๐“จ : MeasurableSpace ๐“จ} {ฮฉ : Type u_3}
  {mฮฉ : MeasurableSpace ฮฉ}
  {alg : Algorithm ๐“ ๐“จ} {f : ๐“ โ†’ ๐“จ}
  {hf : Measurable f}
  {P : MeasureTheory.Measure ฮฉ}
  [MeasureTheory.IsProbabilityMeasure P]
  {A : โ„• โ†’ ฮฉ โ†’ ๐“} {Y : โ„• โ†’ ฮฉ โ†’ ๐“จ}
  (h :
    IsAlgEnvSeq A Y alg (evalEnv f hf) P)
  (n : โ„•) :
  ProbabilityTheory.HasCondDistrib (Y n)
    (A n)
    (ProbabilityTheory.Kernel.deterministic
      f hf)
    P

Code

lemma hascondDistrib_feedback_evalEnv (h : IsAlgEnvSeq A Y alg (evalEnv f hf) P) (n : โ„•) :
    HasCondDistrib (Y n) (A n) (Kernel.deterministic f hf) P
Type uses (3)
Body uses (4)

Actions: Source ยท Open Issue

Proof
by
  simpa using IsObliviousEnv.hasCondDistrib_feedback h n

feedback_evalEnv_ae_eq_eval_action๐Ÿ”—

LemmaLearning.feedback_evalEnv_ae_eq_eval_action
Details

No docstring.

๐Ÿ”—theorem
Learning.feedback_evalEnv_ae_eq_eval_action.{u_1, u_2, u_3}
  {๐“ : Type u_1} {๐“จ : Type u_2} {m๐“ : MeasurableSpace ๐“}
  {m๐“จ : MeasurableSpace ๐“จ} {ฮฉ : Type u_3} {mฮฉ : MeasurableSpace ฮฉ}
  {alg : Algorithm ๐“ ๐“จ} {f : ๐“ โ†’ ๐“จ} {hf : Measurable f}
  {P : MeasureTheory.Measure ฮฉ} [MeasureTheory.IsProbabilityMeasure P]
  {A : โ„• โ†’ ฮฉ โ†’ ๐“} {Y : โ„• โ†’ ฮฉ โ†’ ๐“จ} [StandardBorelSpace ๐“จ] [Nonempty ๐“จ]
  (h : IsAlgEnvSeq A Y alg (evalEnv f hf) P) (n : โ„•) : Y n =แต[P] f โˆ˜ A n
Learning.feedback_evalEnv_ae_eq_eval_action.{u_1,
    u_2, u_3}
  {๐“ : Type u_1} {๐“จ : Type u_2}
  {m๐“ : MeasurableSpace ๐“}
  {m๐“จ : MeasurableSpace ๐“จ} {ฮฉ : Type u_3}
  {mฮฉ : MeasurableSpace ฮฉ}
  {alg : Algorithm ๐“ ๐“จ} {f : ๐“ โ†’ ๐“จ}
  {hf : Measurable f}
  {P : MeasureTheory.Measure ฮฉ}
  [MeasureTheory.IsProbabilityMeasure P]
  {A : โ„• โ†’ ฮฉ โ†’ ๐“} {Y : โ„• โ†’ ฮฉ โ†’ ๐“จ}
  [StandardBorelSpace ๐“จ] [Nonempty ๐“จ]
  (h :
    IsAlgEnvSeq A Y alg (evalEnv f hf) P)
  (n : โ„•) : Y n =แต[P] f โˆ˜ A n

Code

lemma feedback_evalEnv_ae_eq_eval_action [StandardBorelSpace ๐“จ] [Nonempty ๐“จ]
  (h : IsAlgEnvSeq A Y alg (evalEnv f hf) P) (n : โ„•) :
    Y n =แต[P] f โˆ˜ A n
Type uses (3)
Body uses (1)

Actions: Source ยท Open Issue

Proof
feedback_onlineEvalEnv_ae_eq_eval_action h n

forall_feedback_evalEnv_ae_eq_eval_action๐Ÿ”—

LemmaLearning.forall_feedback_evalEnv_ae_eq_eval_action
Details

No docstring.

๐Ÿ”—theorem
Learning.forall_feedback_evalEnv_ae_eq_eval_action.{u_1, u_2, u_3}
  {๐“ : Type u_1} {๐“จ : Type u_2} {m๐“ : MeasurableSpace ๐“}
  {m๐“จ : MeasurableSpace ๐“จ} {ฮฉ : Type u_3} {mฮฉ : MeasurableSpace ฮฉ}
  {alg : Algorithm ๐“ ๐“จ} {f : ๐“ โ†’ ๐“จ} {hf : Measurable f}
  {P : MeasureTheory.Measure ฮฉ} [MeasureTheory.IsProbabilityMeasure P]
  {A : โ„• โ†’ ฮฉ โ†’ ๐“} {Y : โ„• โ†’ ฮฉ โ†’ ๐“จ} [StandardBorelSpace ๐“จ] [Nonempty ๐“จ]
  (h : IsAlgEnvSeq A Y alg (evalEnv f hf) P) :
  โˆ€แต (ฯ‰ : ฮฉ) โˆ‚P, โˆ€ (n : โ„•), Y n ฯ‰ = f (A n ฯ‰)
Learning.forall_feedback_evalEnv_ae_eq_eval_action.{u_1,
    u_2, u_3}
  {๐“ : Type u_1} {๐“จ : Type u_2}
  {m๐“ : MeasurableSpace ๐“}
  {m๐“จ : MeasurableSpace ๐“จ} {ฮฉ : Type u_3}
  {mฮฉ : MeasurableSpace ฮฉ}
  {alg : Algorithm ๐“ ๐“จ} {f : ๐“ โ†’ ๐“จ}
  {hf : Measurable f}
  {P : MeasureTheory.Measure ฮฉ}
  [MeasureTheory.IsProbabilityMeasure P]
  {A : โ„• โ†’ ฮฉ โ†’ ๐“} {Y : โ„• โ†’ ฮฉ โ†’ ๐“จ}
  [StandardBorelSpace ๐“จ] [Nonempty ๐“จ]
  (h :
    IsAlgEnvSeq A Y alg (evalEnv f hf)
      P) :
  โˆ€แต (ฯ‰ : ฮฉ) โˆ‚P,
    โˆ€ (n : โ„•), Y n ฯ‰ = f (A n ฯ‰)

Code

lemma forall_feedback_evalEnv_ae_eq_eval_action [StandardBorelSpace ๐“จ] [Nonempty ๐“จ]
    (h : IsAlgEnvSeq A Y alg (evalEnv f hf) P) :
    โˆ€แต ฯ‰ โˆ‚P, โˆ€ n, Y n ฯ‰ = f (A n ฯ‰)
Type uses (3)
Body uses (1)
Used by (1)

Actions: Source ยท Open Issue

Proof
forall_feedback_onlineEvalEnv_ae_eq_eval_action h

feedback_evalEnv_ae_eq_eval_action_comp๐Ÿ”—

LemmaLearning.feedback_evalEnv_ae_eq_eval_action_comp
Details

No docstring.

๐Ÿ”—theorem
Learning.feedback_evalEnv_ae_eq_eval_action_comp.{u_1, u_2, u_3, u_4}
  {๐“ : Type u_1} {๐“จ : Type u_2} {m๐“ : MeasurableSpace ๐“}
  {m๐“จ : MeasurableSpace ๐“จ} {ฮฉ : Type u_3} {mฮฉ : MeasurableSpace ฮฉ}
  {alg : Algorithm ๐“ ๐“จ} {f : ๐“ โ†’ ๐“จ} {hf : Measurable f}
  {P : MeasureTheory.Measure ฮฉ} [MeasureTheory.IsProbabilityMeasure P]
  {A : โ„• โ†’ ฮฉ โ†’ ๐“} {Y : โ„• โ†’ ฮฉ โ†’ ๐“จ} {ฮฒ : Type u_4} [StandardBorelSpace ๐“จ]
  [Nonempty ๐“จ] (h : IsAlgEnvSeq A Y alg (evalEnv f hf) P) {n : โ„•}
  (g : (โ†ฅ(Finset.Iic n) โ†’ ๐“จ) โ†’ ฮฒ) :
  โˆ€แต (ฯ‰ : ฮฉ) โˆ‚P, (g fun i => Y (โ†‘i) ฯ‰) = g fun i => f (A (โ†‘i) ฯ‰)
Learning.feedback_evalEnv_ae_eq_eval_action_comp.{u_1,
    u_2, u_3, u_4}
  {๐“ : Type u_1} {๐“จ : Type u_2}
  {m๐“ : MeasurableSpace ๐“}
  {m๐“จ : MeasurableSpace ๐“จ} {ฮฉ : Type u_3}
  {mฮฉ : MeasurableSpace ฮฉ}
  {alg : Algorithm ๐“ ๐“จ} {f : ๐“ โ†’ ๐“จ}
  {hf : Measurable f}
  {P : MeasureTheory.Measure ฮฉ}
  [MeasureTheory.IsProbabilityMeasure P]
  {A : โ„• โ†’ ฮฉ โ†’ ๐“} {Y : โ„• โ†’ ฮฉ โ†’ ๐“จ}
  {ฮฒ : Type u_4} [StandardBorelSpace ๐“จ]
  [Nonempty ๐“จ]
  (h :
    IsAlgEnvSeq A Y alg (evalEnv f hf) P)
  {n : โ„•}
  (g : (โ†ฅ(Finset.Iic n) โ†’ ๐“จ) โ†’ ฮฒ) :
  โˆ€แต (ฯ‰ : ฮฉ) โˆ‚P,
    (g fun i => Y (โ†‘i) ฯ‰) =
      g fun i => f (A (โ†‘i) ฯ‰)

Code

lemma feedback_evalEnv_ae_eq_eval_action_comp {ฮฒ : Type*} [StandardBorelSpace ๐“จ] [Nonempty ๐“จ]
    (h : IsAlgEnvSeq A Y alg (evalEnv f hf) P) {n : โ„•} (g : (Iic n โ†’ ๐“จ) โ†’ ฮฒ) :
    โˆ€แต ฯ‰ โˆ‚P, g (fun i โ†ฆ Y i ฯ‰) = g (fun i โ†ฆ f (A i ฯ‰))
Type uses (3)
Body uses (1)

Actions: Source ยท Open Issue

Proof
by
  filter_upwards [forall_feedback_evalEnv_ae_eq_eval_action h] with ฯ‰ hฯ‰
  simp_rw [hฯ‰]
  1. Learning.onlineEvalEnv
  2. Learning.instIsObliviousEnvOnlineEvalEnv
  3. Learning.instIsDeterministicEnvOnlineEvalEnv
  4. Learning.feedbackCondAction_onlineEvalEnv
  5. Learning.feedbackFunZero_onlineEvalEnv
  6. Learning.feedbackFun_onlineEvalEnv
  7. Learning.hascondDistrib_feedback_onlineEvalEnv
  8. Learning.feedback_onlineEvalEnv_ae_eq_eval_action
  9. Learning.forall_feedback_onlineEvalEnv_ae_eq_eval_action
  10. Learning.evalEnv
  11. Learning.instIsObliviousEnvEvalEnv
  12. Learning.instIsDeterministicEnvEvalEnv
  13. Learning.feedbackCondAction_evalEnv
  14. Learning.feedbackFunZero_evalEnv
  15. Learning.feedbackFun_evalEnv
  16. Learning.hascondDistrib_feedback_evalEnv
  17. Learning.feedback_evalEnv_ae_eq_eval_action
  18. Learning.forall_feedback_evalEnv_ae_eq_eval_action
  19. Learning.feedback_evalEnv_ae_eq_eval_action_comp