SequentialLearning.IonescuTulceaSpace

`trajMeasure`🔗

DefinitionLearning.trajMeasure

Details

Measure on the sequence of actions and observations generated by the algorithm/environment.

def

Learning.trajMeasure.{u_1, u_2} {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨}
  (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) :
  MeasureTheory.Measure (ℕ → 𝓐 × 𝓨)
Learning.trajMeasure.{u_1, u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨}
  (alg : Algorithm 𝓐 𝓨)
  (env : Environment 𝓐 𝓨) :
  MeasureTheory.Measure (ℕ → 𝓐 × 𝓨)

Code

noncomputable
def trajMeasure (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) :
    Measure (ℕ → 𝓐 × 𝓨) :=
  Kernel.trajMeasure (alg.p0 ⊗ₘ env.ν0) (stepKernel alg env)
deriving IsProbabilityMeasure

Type uses (2)

Body uses (2)

Used by (19)

Actions: Source · Open Issue

`instIsProbabilityMeasureForallNatProdTrajMeasure`🔗

InstanceLearning.instIsProbabilityMeasureForallNatProdTrajMeasure

Details

No docstring.

theorem

Learning.instIsProbabilityMeasureForallNatProdTrajMeasure.{u_1, u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓐 𝓨)
  (env : Environment 𝓐 𝓨) :
  MeasureTheory.IsProbabilityMeasure (trajMeasure alg env)
Learning.instIsProbabilityMeasureForallNatProdTrajMeasure.{u_1,
    u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨}
  (alg : Algorithm 𝓐 𝓨)
  (env : Environment 𝓐 𝓨) :
  MeasureTheory.IsProbabilityMeasure
    (trajMeasure alg env)

Code

deriving IsProbabilityMeasure

Type uses (3)

Body uses (4)

Used by (8)

Actions: Source · Open Issue

Proof

deriving IsProbabilityMeasure

`map_trajectory`🔗

LemmaLearning.IsAlgEnvSeq.map_trajectory

Details

No docstring.

theorem

Learning.IsAlgEnvSeq.map_trajectory.{u_1, u_2, u_4} {𝓐 : Type u_1}
  {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨}
  {Ω : Type u_4} {mΩ : MeasurableSpace Ω} {alg : Algorithm 𝓐 𝓨}
  {env : Environment 𝓐 𝓨} {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P] {A₁ : ℕ → Ω → 𝓐}
  {R₁ : ℕ → Ω → 𝓨} (h : IsAlgEnvSeq A₁ R₁ alg env P) :
  MeasureTheory.Measure.map (trajectory A₁ R₁) P = trajMeasure alg env
Learning.IsAlgEnvSeq.map_trajectory.{u_1,
    u_2, u_4}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} {Ω : Type u_4}
  {mΩ : MeasurableSpace Ω}
  {alg : Algorithm 𝓐 𝓨}
  {env : Environment 𝓐 𝓨}
  {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P]
  {A₁ : ℕ → Ω → 𝓐} {R₁ : ℕ → Ω → 𝓨}
  (h : IsAlgEnvSeq A₁ R₁ alg env P) :
  MeasureTheory.Measure.map
      (trajectory A₁ R₁) P =
    trajMeasure alg env

Code

lemma IsAlgEnvSeq.map_trajectory (h : IsAlgEnvSeq A₁ R₁ alg env P) :
    P.map (trajectory A₁ R₁) = trajMeasure alg env

Type uses (5)

Body uses (7)

Used by (1)

isAlgEnvSeq_unique

Actions: Source · Open Issue

Proof

by
  rw [trajMeasure]
  have h := (Kernel.hasLaw_trajMeasure (Y := fun n ω ↦ (A₁ n ω, R₁ n ω)) (P := P)
    (μ₀ := alg.p0 ⊗ₘ env.ν0) (κ := stepKernel alg env) (fun n ↦ ?_) ?_ (fun n ↦ ?_)).map_eq
  · exact h
  · have hA := h.measurable_action n
    have hR := h.measurable_feedback n
    fun_prop
  · exact h.hasLaw_step_zero
  · exact h.hasCondDistrib_step n

`eq_trajMeasure_map_frestrictLe_of_isAlgEnvSeqUntil`🔗

LemmaLearning.eq_trajMeasure_map_frestrictLe_of_isAlgEnvSeqUntil

Details

No docstring.

theorem

Learning.eq_trajMeasure_map_frestrictLe_of_isAlgEnvSeqUntil.{u_1, u_2,
    u_4}
  {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} {Ω : Type u_4} {mΩ : MeasurableSpace Ω}
  {alg : Algorithm 𝓐 𝓨} {env : Environment 𝓐 𝓨}
  {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P]
  {A₁ : ℕ → Ω → 𝓐} {R₁ : ℕ → Ω → 𝓨} {N : ℕ}
  (h : IsAlgEnvSeqUntil A₁ R₁ alg env P N) :
  MeasureTheory.Measure.map (fun ω n => (A₁ (↑n) ω, R₁ (↑n) ω)) P =
    MeasureTheory.Measure.map (Preorder.frestrictLe N)
      (trajMeasure alg env)
Learning.eq_trajMeasure_map_frestrictLe_of_isAlgEnvSeqUntil.{u_1,
    u_2, u_4}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} {Ω : Type u_4}
  {mΩ : MeasurableSpace Ω}
  {alg : Algorithm 𝓐 𝓨}
  {env : Environment 𝓐 𝓨}
  {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P]
  {A₁ : ℕ → Ω → 𝓐} {R₁ : ℕ → Ω → 𝓨}
  {N : ℕ}
  (h :
    IsAlgEnvSeqUntil A₁ R₁ alg env P N) :
  MeasureTheory.Measure.map
      (fun ω n => (A₁ (↑n) ω, R₁ (↑n) ω))
      P =
    MeasureTheory.Measure.map
      (Preorder.frestrictLe N)
      (trajMeasure alg env)

Code

lemma eq_trajMeasure_map_frestrictLe_of_isAlgEnvSeqUntil
    (h : IsAlgEnvSeqUntil A₁ R₁ alg env P N) :
    P.map (fun ω (n : Iic N) ↦ (A₁ n ω, R₁ n ω)) =
      (trajMeasure alg env).map (Preorder.frestrictLe N)

Type uses (4)

Body uses (7)

Used by (1)

isAlgEnvSeqUntil_unique

Actions: Source · Open Issue

Proof

by
  rw [trajMeasure]
  have h := Kernel.eq_trajMeasure_map_frestrictLe (Y := fun n ω ↦ (A₁ n ω, R₁ n ω))
    (P := P) (μ₀ := alg.p0 ⊗ₘ env.ν0) (κ := stepKernel alg env) ?_ (fun n hn ↦ ?_) (N := N)
  · exact h
  · exact h.hasLaw_step_zero
  · exact h.hasCondDistrib_step n hn

`isAlgEnvSeq_unique`🔗

LemmaLearning.isAlgEnvSeq_unique

Details

The law of the sequence of actions and observations generated by an algorithm-environment pair is unique: it does not depend on the probability space used.

theorem

Learning.isAlgEnvSeq_unique.{u_1, u_2, u_4, u_5} {𝓐 : Type u_1}
  {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨}
  {Ω : Type u_4} {Ω' : Type u_5} {mΩ : MeasurableSpace Ω}
  {mΩ' : MeasurableSpace Ω'} {alg : Algorithm 𝓐 𝓨}
  {env : Environment 𝓐 𝓨} {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P] {P' : MeasureTheory.Measure Ω'}
  [MeasureTheory.IsProbabilityMeasure P'] {A₁ : ℕ → Ω → 𝓐}
  {R₁ : ℕ → Ω → 𝓨} {A₂ : ℕ → Ω' → 𝓐} {R₂ : ℕ → Ω' → 𝓨}
  (h1 : IsAlgEnvSeq A₁ R₁ alg env P)
  (h2 : IsAlgEnvSeq A₂ R₂ alg env P') :
  MeasureTheory.Measure.map (trajectory A₁ R₁) P =
    MeasureTheory.Measure.map (trajectory A₂ R₂) P'
Learning.isAlgEnvSeq_unique.{u_1, u_2,
    u_4, u_5}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} {Ω : Type u_4}
  {Ω' : Type u_5} {mΩ : MeasurableSpace Ω}
  {mΩ' : MeasurableSpace Ω'}
  {alg : Algorithm 𝓐 𝓨}
  {env : Environment 𝓐 𝓨}
  {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P]
  {P' : MeasureTheory.Measure Ω'}
  [MeasureTheory.IsProbabilityMeasure P']
  {A₁ : ℕ → Ω → 𝓐} {R₁ : ℕ → Ω → 𝓨}
  {A₂ : ℕ → Ω' → 𝓐} {R₂ : ℕ → Ω' → 𝓨}
  (h1 : IsAlgEnvSeq A₁ R₁ alg env P)
  (h2 : IsAlgEnvSeq A₂ R₂ alg env P') :
  MeasureTheory.Measure.map
      (trajectory A₁ R₁) P =
    MeasureTheory.Measure.map
      (trajectory A₂ R₂) P'

Code

lemma isAlgEnvSeq_unique (h1 : IsAlgEnvSeq A₁ R₁ alg env P)
    (h2 : IsAlgEnvSeq A₂ R₂ alg env P') :
    P.map (trajectory A₁ R₁) = P'.map (trajectory A₂ R₂)

Type uses (4)

Body uses (2)

Used by (3)

Actions: Source · Open Issue

Proof

by
  rw [h1.map_trajectory, h2.map_trajectory]

`identDistrib_trajectory`🔗

TheoremLearning.IsAlgEnvSeq.identDistrib_trajectory

Details

The law of the sequence of actions and observations generated by an algorithm-environment pair is unique: it does not depend on the probability space used.

theorem

Learning.IsAlgEnvSeq.identDistrib_trajectory.{u_1, u_2, u_4, u_5}
  {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} {Ω : Type u_4} {Ω' : Type u_5}
  {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'}
  {alg : Algorithm 𝓐 𝓨} {env : Environment 𝓐 𝓨}
  {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P]
  {P' : MeasureTheory.Measure Ω'}
  [MeasureTheory.IsProbabilityMeasure P'] {A₁ : ℕ → Ω → 𝓐}
  {R₁ : ℕ → Ω → 𝓨} {A₂ : ℕ → Ω' → 𝓐} {R₂ : ℕ → Ω' → 𝓨}
  (h1 : IsAlgEnvSeq A₁ R₁ alg env P)
  (h2 : IsAlgEnvSeq A₂ R₂ alg env P') :
  ProbabilityTheory.IdentDistrib (trajectory A₁ R₁) (trajectory A₂ R₂) P
    P'
Learning.IsAlgEnvSeq.identDistrib_trajectory.{u_1,
    u_2, u_4, u_5}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} {Ω : Type u_4}
  {Ω' : Type u_5} {mΩ : MeasurableSpace Ω}
  {mΩ' : MeasurableSpace Ω'}
  {alg : Algorithm 𝓐 𝓨}
  {env : Environment 𝓐 𝓨}
  {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P]
  {P' : MeasureTheory.Measure Ω'}
  [MeasureTheory.IsProbabilityMeasure P']
  {A₁ : ℕ → Ω → 𝓐} {R₁ : ℕ → Ω → 𝓨}
  {A₂ : ℕ → Ω' → 𝓐} {R₂ : ℕ → Ω' → 𝓨}
  (h1 : IsAlgEnvSeq A₁ R₁ alg env P)
  (h2 : IsAlgEnvSeq A₂ R₂ alg env P') :
  ProbabilityTheory.IdentDistrib
    (trajectory A₁ R₁) (trajectory A₂ R₂)
    P P'

Code

theorem IsAlgEnvSeq.identDistrib_trajectory (h1 : IsAlgEnvSeq A₁ R₁ alg env P)
    (h2 : IsAlgEnvSeq A₂ R₂ alg env P') :
    IdentDistrib (trajectory A₁ R₁) (trajectory A₂ R₂) P P' where
  aemeasurable_fst

Type uses (4)

Body uses (1)

isAlgEnvSeq_unique

Used by (1)

identDistrib_pullCount_sumRewards

Actions: Source · Open Issue

Proof

(measurable_pi_iff.2 fun n ↦ (h1.measurable_action n).prodMk
    (h1.measurable_feedback n)).aemeasurable
  aemeasurable_snd := (measurable_pi_iff.2 fun n ↦ (h2.measurable_action n).prodMk
    (h2.measurable_feedback n)).aemeasurable
  map_eq := isAlgEnvSeq_unique h1 h2

`isAlgEnvSeqUntil_unique`🔗

LemmaLearning.isAlgEnvSeqUntil_unique

Details

No docstring.

theorem

Learning.isAlgEnvSeqUntil_unique.{u_1, u_2, u_4, u_5} {𝓐 : Type u_1}
  {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨}
  {Ω : Type u_4} {Ω' : Type u_5} {mΩ : MeasurableSpace Ω}
  {mΩ' : MeasurableSpace Ω'} {alg : Algorithm 𝓐 𝓨}
  {env : Environment 𝓐 𝓨} {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P] {P' : MeasureTheory.Measure Ω'}
  [MeasureTheory.IsProbabilityMeasure P'] {A₁ : ℕ → Ω → 𝓐}
  {R₁ : ℕ → Ω → 𝓨} {A₂ : ℕ → Ω' → 𝓐} {R₂ : ℕ → Ω' → 𝓨} {N : ℕ}
  (h1 : IsAlgEnvSeqUntil A₁ R₁ alg env P N)
  (h2 : IsAlgEnvSeqUntil A₂ R₂ alg env P' N) :
  MeasureTheory.Measure.map (fun ω n => (A₁ (↑n) ω, R₁ (↑n) ω)) P =
    MeasureTheory.Measure.map (fun ω n => (A₂ (↑n) ω, R₂ (↑n) ω)) P'
Learning.isAlgEnvSeqUntil_unique.{u_1,
    u_2, u_4, u_5}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} {Ω : Type u_4}
  {Ω' : Type u_5} {mΩ : MeasurableSpace Ω}
  {mΩ' : MeasurableSpace Ω'}
  {alg : Algorithm 𝓐 𝓨}
  {env : Environment 𝓐 𝓨}
  {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P]
  {P' : MeasureTheory.Measure Ω'}
  [MeasureTheory.IsProbabilityMeasure P']
  {A₁ : ℕ → Ω → 𝓐} {R₁ : ℕ → Ω → 𝓨}
  {A₂ : ℕ → Ω' → 𝓐} {R₂ : ℕ → Ω' → 𝓨}
  {N : ℕ}
  (h1 :
    IsAlgEnvSeqUntil A₁ R₁ alg env P N)
  (h2 :
    IsAlgEnvSeqUntil A₂ R₂ alg env P' N) :
  MeasureTheory.Measure.map
      (fun ω n => (A₁ (↑n) ω, R₁ (↑n) ω))
      P =
    MeasureTheory.Measure.map
      (fun ω n => (A₂ (↑n) ω, R₂ (↑n) ω))
      P'

Code

lemma isAlgEnvSeqUntil_unique (h1 : IsAlgEnvSeqUntil A₁ R₁ alg env P N)
    (h2 : IsAlgEnvSeqUntil A₂ R₂ alg env P' N) :
    P.map (fun ω (n : Iic N) ↦ (A₁ n ω, R₁ n ω)) =
      P'.map (fun ω (n : Iic N) ↦ (A₂ n ω, R₂ n ω))

Type uses (3)

Body uses (2)

Actions: Source · Open Issue

Proof

by
  rw [eq_trajMeasure_map_frestrictLe_of_isAlgEnvSeqUntil h1,
    eq_trajMeasure_map_frestrictLe_of_isAlgEnvSeqUntil h2]

`step`🔗

DefinitionLearning.IT.step

Details

Action and feedback at step n.

def

Learning.IT.step.{u_1, u_2} {𝓐 : Type u_1} {𝓨 : Type u_2} (n : ℕ)
  (h : ℕ → 𝓐 × 𝓨) : 𝓐 × 𝓨
Learning.IT.step.{u_1, u_2} {𝓐 : Type u_1}
  {𝓨 : Type u_2} (n : ℕ) (h : ℕ → 𝓐 × 𝓨) :
  𝓐 × 𝓨

Code

def step (n : ℕ) (h : ℕ → 𝓐 × 𝓨) : 𝓐 × 𝓨 := h n

Used by (13)

Actions: Source · Open Issue

`action`🔗

DefinitionLearning.IT.action

Details

action n is the action pulled at time n. This is a random variable on the measurable space ℕ → 𝓐 × 𝓨.

def

Learning.IT.action.{u_1, u_2} {𝓐 : Type u_1} {𝓨 : Type u_2} (n : ℕ)
  (h : ℕ → 𝓐 × 𝓨) : 𝓐
Learning.IT.action.{u_1, u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2} (n : ℕ)
  (h : ℕ → 𝓐 × 𝓨) : 𝓐

Code

def action (n : ℕ) (h : ℕ → 𝓐 × 𝓨) : 𝓐 := (h n).1

Used by (31)

Actions: Source · Open Issue

`feedback`🔗

DefinitionLearning.IT.feedback

Details

feedback n is the feedback at time n. This is a random variable on the measurable space ℕ → 𝓐 × 𝓨.

def

Learning.IT.feedback.{u_1, u_2} {𝓐 : Type u_1} {𝓨 : Type u_2} (n : ℕ)
  (h : ℕ → 𝓐 × 𝓨) : 𝓨
Learning.IT.feedback.{u_1, u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2} (n : ℕ)
  (h : ℕ → 𝓐 × 𝓨) : 𝓨

Code

def feedback (n : ℕ) (h : ℕ → 𝓐 × 𝓨) : 𝓨 := (h n).2

Used by (16)

Actions: Source · Open Issue

`hist`🔗

DefinitionLearning.IT.hist

Details

hist n is the history up to time n. This is a random variable on the measurable space ℕ → 𝓐 × 𝓨.

def

Learning.IT.hist.{u_1, u_2} {𝓐 : Type u_1} {𝓨 : Type u_2} (n : ℕ)
  (h : ℕ → 𝓐 × 𝓨) : ↥(Finset.Iic n) → 𝓐 × 𝓨
Learning.IT.hist.{u_1, u_2} {𝓐 : Type u_1}
  {𝓨 : Type u_2} (n : ℕ) (h : ℕ → 𝓐 × 𝓨) :
  ↥(Finset.Iic n) → 𝓐 × 𝓨

Code

def hist (n : ℕ) (h : ℕ → 𝓐 × 𝓨) : Iic n → 𝓐 × 𝓨 := fun i ↦ h i

Used by (23)

Actions: Source · Open Issue

`fst_comp_step`🔗

LemmaLearning.IT.fst_comp_step

Details

No docstring.

theorem

Learning.IT.fst_comp_step.{u_1, u_2} {𝓐 : Type u_1} {𝓨 : Type u_2}
  (n : ℕ) : Prod.fst ∘ step n = action n
Learning.IT.fst_comp_step.{u_1, u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2} (n : ℕ) :
  Prod.fst ∘ step n = action n

Code

lemma fst_comp_step (n : ℕ) : Prod.fst ∘ step (𝓐

Type uses (2)

Used by (2)

Actions: Source · Open Issue

Proof

𝓐) (𝓨 := 𝓨) n = action n := rfl

`measurable_step`🔗

LemmaLearning.IT.measurable_step

Details

No docstring.

theorem

Learning.IT.measurable_step.{u_1, u_2} {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (n : ℕ) :
  Measurable (step n)
Learning.IT.measurable_step.{u_1, u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} (n : ℕ) :
  Measurable (step n)

Code

lemma measurable_step (n : ℕ) : Measurable (step n (𝓐

Type uses (1)

step

Used by (5)

Actions: Source · Open Issue

Proof

𝓐) (𝓨 := 𝓨)) := by
  unfold step; fun_prop

`measurable_step_prod`🔗

LemmaLearning.IT.measurable_step_prod

Details

No docstring.

theorem

Learning.IT.measurable_step_prod.{u_1, u_2} {𝓐 : Type u_1}
  {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} :
  Measurable fun p => step (Prod.fst p) (Prod.snd p)
Learning.IT.measurable_step_prod.{u_1,
    u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} :
  Measurable fun p =>
    step (Prod.fst p) (Prod.snd p)

Code

lemma measurable_step_prod : Measurable (fun p : ℕ × (ℕ → 𝓐 × 𝓨) ↦ step p.1 p.2)

Type uses (1)

step

Body uses (1)

measurable_step

Actions: Source · Open Issue

Proof

measurable_from_prod_countable_right fun n ↦ (by simp only; fun_prop)

`measurable_action`🔗

LemmaLearning.IT.measurable_action

Details

No docstring.

theorem

Learning.IT.measurable_action.{u_1, u_2} {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (n : ℕ) :
  Measurable (action n)
Learning.IT.measurable_action.{u_1, u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} (n : ℕ) :
  Measurable (action n)

Code

lemma measurable_action (n : ℕ) : Measurable (action n (𝓐

Type uses (1)

action

Used by (14)

Actions: Source · Open Issue

Proof

𝓐) (𝓨 := 𝓨)) := by
  unfold action; fun_prop

`measurable_action_prod`🔗

LemmaLearning.IT.measurable_action_prod

Details

No docstring.

theorem

Learning.IT.measurable_action_prod.{u_1, u_2} {𝓐 : Type u_1}
  {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} :
  Measurable fun p => action (Prod.fst p) (Prod.snd p)
Learning.IT.measurable_action_prod.{u_1,
    u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} :
  Measurable fun p =>
    action (Prod.fst p) (Prod.snd p)

Code

lemma measurable_action_prod : Measurable (fun p : ℕ × (ℕ → 𝓐 × 𝓨) ↦ action p.1 p.2)

Type uses (1)

action

Body uses (1)

measurable_action

Actions: Source · Open Issue

Proof

measurable_from_prod_countable_right fun n ↦ (by simp only; fun_prop)

`measurable_feedback`🔗

LemmaLearning.IT.measurable_feedback

Details

No docstring.

theorem

Learning.IT.measurable_feedback.{u_1, u_2} {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (n : ℕ) :
  Measurable (feedback n)
Learning.IT.measurable_feedback.{u_1, u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} (n : ℕ) :
  Measurable (feedback n)

Code

lemma measurable_feedback (n : ℕ) : Measurable (feedback n (𝓐

Type uses (1)

feedback

Used by (9)

Actions: Source · Open Issue

Proof

𝓐) (𝓨 := 𝓨)) := by
  unfold feedback; fun_prop

`measurable_feedback_prod`🔗

LemmaLearning.IT.measurable_feedback_prod

Details

No docstring.

theorem

Learning.IT.measurable_feedback_prod.{u_1, u_2} {𝓐 : Type u_1}
  {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} :
  Measurable fun p => feedback (Prod.fst p) (Prod.snd p)
Learning.IT.measurable_feedback_prod.{u_1,
    u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} :
  Measurable fun p =>
    feedback (Prod.fst p) (Prod.snd p)

Code

lemma measurable_feedback_prod : Measurable (fun p : ℕ × (ℕ → 𝓐 × 𝓨) ↦ feedback p.1 p.2)

Type uses (1)

feedback

Body uses (1)

measurable_feedback

Actions: Source · Open Issue

Proof

measurable_from_prod_countable_right fun n ↦ (by simp only; fun_prop)

`measurable_hist`🔗

LemmaLearning.IT.measurable_hist

Details

No docstring.

theorem

Learning.IT.measurable_hist.{u_1, u_2} {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (n : ℕ) :
  Measurable (hist n)
Learning.IT.measurable_hist.{u_1, u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} (n : ℕ) :
  Measurable (hist n)

Code

lemma measurable_hist (n : ℕ) : Measurable (hist n (𝓐

Type uses (1)

hist

Used by (5)

Actions: Source · Open Issue

Proof

𝓐) (𝓨 := 𝓨)) := by unfold hist; fun_prop

`hist_eq_frestrictLe`🔗

LemmaLearning.IT.hist_eq_frestrictLe

Details

No docstring.

theorem

Learning.IT.hist_eq_frestrictLe.{u_1, u_2} {𝓐 : Type u_1}
  {𝓨 : Type u_2} : hist = Preorder.frestrictLe
Learning.IT.hist_eq_frestrictLe.{u_1, u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2} :
  hist = Preorder.frestrictLe

Code

lemma hist_eq_frestrictLe :
    hist = Preorder.frestrictLe («π»

Type uses (1)

hist

Used by (1)

filtration_eq_comap

Actions: Source · Open Issue

Proof

fun _ ↦ 𝓐 × 𝓨) := by
  ext n h i : 3
  simp [hist, Preorder.frestrictLe]

`filtration`🔗

DefinitionLearning.IT.filtration

Details

Filtration of the algorithm Seq.

def

Learning.IT.filtration.{u_4, u_5} (𝓐 : Type u_4) (𝓨 : Type u_5)
  [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] :
  MeasureTheory.Filtration ℕ inferInstance
Learning.IT.filtration.{u_4, u_5}
  (𝓐 : Type u_4) (𝓨 : Type u_5)
  [MeasurableSpace 𝓐]
  [MeasurableSpace 𝓨] :
  MeasureTheory.Filtration ℕ inferInstance

Code

protected def filtration (𝓐 𝓨 : Type*) [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] :
    Filtration ℕ (inferInstance : MeasurableSpace (ℕ → 𝓐 × 𝓨)) :=
  MeasureTheory.Filtration.piLE (X := fun _ ↦ 𝓐 × 𝓨)

Used by (13)

Actions: Source · Open Issue

`filtration_eq_comap`🔗

LemmaLearning.IT.filtration_eq_comap

Details

No docstring.

theorem

Learning.IT.filtration_eq_comap.{u_1, u_2} {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (n : ℕ) :
  ↑(IT.filtration 𝓐 𝓨) n = MeasurableSpace.comap (hist n) inferInstance
Learning.IT.filtration_eq_comap.{u_1, u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} (n : ℕ) :
  ↑(IT.filtration 𝓐 𝓨) n =
    MeasurableSpace.comap (hist n)
      inferInstance

Code

lemma filtration_eq_comap (n : ℕ) :
    IT.filtration 𝓐 𝓨 n = MeasurableSpace.comap (hist n) inferInstance

Type uses (2)

Body uses (1)

hist_eq_frestrictLe

Used by (5)

Actions: Source · Open Issue

Proof

by
  simp [IT.filtration, Filtration.piLE_eq_comap_frestrictLe, ← hist_eq_frestrictLe]

`step_eq_eval_comp_hist`🔗

LemmaLearning.IT.step_eq_eval_comp_hist

Details

No docstring.

theorem

Learning.IT.step_eq_eval_comp_hist.{u_1, u_2} {𝓐 : Type u_1}
  {𝓨 : Type u_2} (n : ℕ) : step n = (fun x => x ⟨n, ⋯⟩) ∘ hist n
Learning.IT.step_eq_eval_comp_hist.{u_1,
    u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2} (n : ℕ) :
  step n = (fun x => x ⟨n, ⋯⟩) ∘ hist n

Code

lemma step_eq_eval_comp_hist (n : ℕ) :
    step (𝓐

Type uses (2)

Used by (1)

adapted_step

Actions: Source · Open Issue

Proof

𝓐) (𝓨 := 𝓨) n = (fun x ↦ x ⟨n, by simp⟩) ∘ (hist n) := rfl

`action_eq_eval_comp_hist`🔗

LemmaLearning.IT.action_eq_eval_comp_hist

Details

No docstring.

theorem

Learning.IT.action_eq_eval_comp_hist.{u_1, u_2} {𝓐 : Type u_1}
  {𝓨 : Type u_2} (n : ℕ) :
  action n = (fun x => Prod.fst (x ⟨n, ⋯⟩)) ∘ hist n
Learning.IT.action_eq_eval_comp_hist.{u_1,
    u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2} (n : ℕ) :
  action n =
    (fun x => Prod.fst (x ⟨n, ⋯⟩)) ∘
      hist n

Code

lemma action_eq_eval_comp_hist (n : ℕ) :
    action (𝓐

Type uses (2)

Used by (1)

adapted_action

Actions: Source · Open Issue

Proof

𝓐) (𝓨 := 𝓨) n = (fun x ↦ (x ⟨n, by simp⟩).1) ∘ (hist n) := rfl

`feedback_eq_eval_comp_hist`🔗

LemmaLearning.IT.feedback_eq_eval_comp_hist

Details

No docstring.

theorem

Learning.IT.feedback_eq_eval_comp_hist.{u_1, u_2} {𝓐 : Type u_1}
  {𝓨 : Type u_2} (n : ℕ) :
  feedback n = (fun x => Prod.snd (x ⟨n, ⋯⟩)) ∘ hist n
Learning.IT.feedback_eq_eval_comp_hist.{u_1,
    u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2} (n : ℕ) :
  feedback n =
    (fun x => Prod.snd (x ⟨n, ⋯⟩)) ∘
      hist n

Code

lemma feedback_eq_eval_comp_hist (n : ℕ) :
    feedback (𝓐

Type uses (2)

Used by (1)

adapted_feedback

Actions: Source · Open Issue

Proof

𝓐) (𝓨 := 𝓨) n = (fun x ↦ (x ⟨n, by simp⟩).2) ∘ (hist n) := rfl

`adapted_step`🔗

LemmaLearning.IT.adapted_step

Details

No docstring.

theorem

Learning.IT.adapted_step.{u_1, u_2} {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} :
  MeasureTheory.Adapted (IT.filtration 𝓐 𝓨) step
Learning.IT.adapted_step.{u_1, u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} :
  MeasureTheory.Adapted
    (IT.filtration 𝓐 𝓨) step

Code

lemma adapted_step : Adapted (IT.filtration 𝓐 𝓨) (step (𝓐

Type uses (2)

Body uses (4)

Actions: Source · Open Issue

Proof

𝓐) (𝓨 := 𝓨)) := by
  intro n
  rw [filtration_eq_comap, step_eq_eval_comp_hist]
  exact measurable_comp_comap _ (by fun_prop)

`adapted_hist`🔗

LemmaLearning.IT.adapted_hist

Details

No docstring.

theorem

Learning.IT.adapted_hist.{u_1, u_2} {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} :
  MeasureTheory.Adapted (IT.filtration 𝓐 𝓨) hist
Learning.IT.adapted_hist.{u_1, u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} :
  MeasureTheory.Adapted
    (IT.filtration 𝓐 𝓨) hist

Code

lemma adapted_hist : Adapted (IT.filtration 𝓐 𝓨) hist

Type uses (2)

Body uses (1)

filtration_eq_comap

Actions: Source · Open Issue

Proof

by
  intro n
  simp [filtration_eq_comap, measurable_iff_comap_le]

`adapted_action`🔗

LemmaLearning.IT.adapted_action

Details

No docstring.

theorem

Learning.IT.adapted_action.{u_1, u_2} {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} :
  MeasureTheory.Adapted (IT.filtration 𝓐 𝓨) action
Learning.IT.adapted_action.{u_1, u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} :
  MeasureTheory.Adapted
    (IT.filtration 𝓐 𝓨) action

Code

lemma adapted_action : Adapted (IT.filtration 𝓐 𝓨) action

Type uses (2)

Body uses (4)

Used by (3)

Actions: Source · Open Issue

Proof

by
  intro n
  rw [filtration_eq_comap, action_eq_eval_comp_hist]
  exact measurable_comp_comap _ (by fun_prop)

`adapted_feedback`🔗

LemmaLearning.IT.adapted_feedback

Details

No docstring.

theorem

Learning.IT.adapted_feedback.{u_1, u_2} {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} :
  MeasureTheory.Adapted (IT.filtration 𝓐 𝓨) feedback
Learning.IT.adapted_feedback.{u_1, u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} :
  MeasureTheory.Adapted
    (IT.filtration 𝓐 𝓨) feedback

Code

lemma adapted_feedback : Adapted (IT.filtration 𝓐 𝓨) feedback

Type uses (2)

Body uses (4)

Actions: Source · Open Issue

Proof

by
  intro n
  rw [filtration_eq_comap, feedback_eq_eval_comp_hist]
  exact measurable_comp_comap _ (by fun_prop)

`filtrationAction`🔗

DefinitionLearning.IT.filtrationAction

Details

Filtration generated by the history at time n-1 together with the action at time n.

def

Learning.IT.filtrationAction.{u_4, u_5} (𝓐 : Type u_4) (𝓨 : Type u_5)
  [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] :
  MeasureTheory.Filtration ℕ inferInstance
Learning.IT.filtrationAction.{u_4, u_5}
  (𝓐 : Type u_4) (𝓨 : Type u_5)
  [MeasurableSpace 𝓐]
  [MeasurableSpace 𝓨] :
  MeasureTheory.Filtration ℕ inferInstance

Code

def filtrationAction (𝓐 𝓨 : Type*) [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] :
    Filtration ℕ (inferInstance : MeasurableSpace (ℕ → 𝓐 × 𝓨)) where
  seq n := if n = 0 then MeasurableSpace.comap (action 0) inferInstance
    else IT.filtration 𝓐 𝓨 (n - 1) ⊔ MeasurableSpace.comap (action n) inferInstance
  mono' n m hnm := by
    simp only
    by_cases hn : n = 0
    · by_cases hm : m = 0
      · simp [hn, hm]
      · simp only [hn, ↓reduceIte, hm]
        refine le_sup_of_le_left ?_
        rw [← measurable_iff_comap_le]
        suffices Measurable[IT.filtration 𝓐 𝓨 0] (action 0) from
          this.mono ((IT.filtration 𝓐 𝓨).mono zero_le) le_rfl
        exact adapted_action 0
    have hm : m ≠ 0 := by grind
    simp only [hn, hm, ↓reduceIte]
    have hnm' : n - 1 ≤ m - 1 := by grind
    simp only [sup_le_iff]
    constructor
    · refine le_sup_of_le_left ?_
      exact (IT.filtration 𝓐 𝓨).mono hnm'
    · rcases eq_or_lt_of_le hnm with rfl | hlt
      · exact le_sup_of_le_right le_rfl
      refine le_sup_of_le_left ?_
      rw [← measurable_iff_comap_le]
      have h_le : n ≤ m - 1 := by grind
      suffices Measurable[IT.filtration 𝓐 𝓨 n] (action n) from
        this.mono ((IT.filtration 𝓐 𝓨).mono h_le) le_rfl
      exact adapted_action n
  le' n := by
    by_cases hn : n = 0
    · simp only [hn, ↓reduceIte]
      rw [← measurable_iff_comap_le]
      fun_prop
    simp only [hn, ↓reduceIte, sup_le_iff]
    constructor
    · exact (IT.filtration 𝓐 𝓨).le _
    · rw [← measurable_iff_comap_le]
      fun_prop

Body uses (4)

Used by (7)

Actions: Source · Open Issue

`filtrationAction_zero_eq_comap`🔗

LemmaLearning.IT.filtrationAction_zero_eq_comap

Details

No docstring.

theorem

Learning.IT.filtrationAction_zero_eq_comap.{u_1, u_2} {𝓐 : Type u_1}
  {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} :
  ↑(filtrationAction 𝓐 𝓨) 0 =
    MeasurableSpace.comap (action 0) inferInstance
Learning.IT.filtrationAction_zero_eq_comap.{u_1,
    u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} :
  ↑(filtrationAction 𝓐 𝓨) 0 =
    MeasurableSpace.comap (action 0)
      inferInstance

Code

lemma filtrationAction_zero_eq_comap :
    filtrationAction 𝓐 𝓨 0 = MeasurableSpace.comap (action 0) inferInstance

Type uses (2)

Body uses (1)

filtration

Used by (1)

filtrationAction_le_filtration_self

Actions: Source · Open Issue

Proof

by
  simp [filtrationAction]

`filtrationAction_eq_comap`🔗

LemmaLearning.IT.filtrationAction_eq_comap

Details

No docstring.

theorem

Learning.IT.filtrationAction_eq_comap.{u_1, u_2} {𝓐 : Type u_1}
  {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨}
  (n : ℕ) (hn : n ≠ 0) :
  ↑(filtrationAction 𝓐 𝓨) n =
    MeasurableSpace.comap (fun ω => (hist (n - 1) ω, action n ω))
      inferInstance
Learning.IT.filtrationAction_eq_comap.{u_1,
    u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} (n : ℕ)
  (hn : n ≠ 0) :
  ↑(filtrationAction 𝓐 𝓨) n =
    MeasurableSpace.comap
      (fun ω =>
        (hist (n - 1) ω, action n ω))
      inferInstance

Code

lemma filtrationAction_eq_comap (n : ℕ) (hn : n ≠ 0) :
    filtrationAction 𝓐 𝓨 n =
      MeasurableSpace.comap (fun ω ↦ (hist (n - 1) ω, action n ω)) inferInstance

Type uses (3)

Body uses (4)

Actions: Source · Open Issue

Proof

by
  simp only [filtrationAction, filtration_eq_comap, ← MeasurableSpace.comap_prodMk, hn, ↓reduceIte]
  rfl

`filtration_le_filtrationAction_add_one`🔗

LemmaLearning.IT.filtration_le_filtrationAction_add_one

Details

No docstring.

theorem

Learning.IT.filtration_le_filtrationAction_add_one.{u_1, u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} (n : ℕ) :
  ↑(IT.filtration 𝓐 𝓨) n ≤ ↑(filtrationAction 𝓐 𝓨) (n + 1)
Learning.IT.filtration_le_filtrationAction_add_one.{u_1,
    u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} (n : ℕ) :
  ↑(IT.filtration 𝓐 𝓨) n ≤
    ↑(filtrationAction 𝓐 𝓨) (n + 1)

Code

lemma filtration_le_filtrationAction_add_one (n : ℕ) :
    IT.filtration 𝓐 𝓨 n ≤ filtrationAction 𝓐 𝓨 (n + 1)

Type uses (2)

Body uses (1)

action

Used by (1)

filtration_le_filtrationAction

Actions: Source · Open Issue

Proof

le_sup_of_le_left le_rfl

`filtration_le_filtrationAction`🔗

LemmaLearning.IT.filtration_le_filtrationAction

Details

No docstring.

theorem

Learning.IT.filtration_le_filtrationAction.{u_1, u_2} {𝓐 : Type u_1}
  {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨}
  {m n : ℕ} (h : n < m) :
  ↑(IT.filtration 𝓐 𝓨) n ≤ ↑(filtrationAction 𝓐 𝓨) m
Learning.IT.filtration_le_filtrationAction.{u_1,
    u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} {m n : ℕ}
  (h : n < m) :
  ↑(IT.filtration 𝓐 𝓨) n ≤
    ↑(filtrationAction 𝓐 𝓨) m

Code

lemma filtration_le_filtrationAction {m n : ℕ} (h : n < m) :
    IT.filtration 𝓐 𝓨 n ≤ filtrationAction 𝓐 𝓨 m

Type uses (2)

Body uses (1)

filtration_le_filtrationAction_add_one

Actions: Source · Open Issue

Proof

by
  have h' : n + 1 ≤ m := by grind
  exact (filtration_le_filtrationAction_add_one n).trans ((filtrationAction 𝓐 𝓨).mono h')

`filtrationAction_le_filtration_self`🔗

LemmaLearning.IT.filtrationAction_le_filtration_self

Details

No docstring.

theorem

Learning.IT.filtrationAction_le_filtration_self.{u_1, u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} (n : ℕ) :
  ↑(filtrationAction 𝓐 𝓨) n ≤ ↑(IT.filtration 𝓐 𝓨) n
Learning.IT.filtrationAction_le_filtration_self.{u_1,
    u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} (n : ℕ) :
  ↑(filtrationAction 𝓐 𝓨) n ≤
    ↑(IT.filtration 𝓐 𝓨) n

Code

lemma filtrationAction_le_filtration_self (n : ℕ) :
    filtrationAction 𝓐 𝓨 n ≤ IT.filtration 𝓐 𝓨 n

Type uses (2)

Body uses (3)

Used by (1)

filtrationAction_le_filtration

Actions: Source · Open Issue

Proof

by
  by_cases hn : n = 0
  · simp only [hn, filtrationAction_zero_eq_comap]
    rw [← measurable_iff_comap_le]
    exact adapted_action 0
  simp only [filtrationAction, hn, ↓reduceIte, sup_le_iff]
  constructor
  · exact (IT.filtration 𝓐 𝓨).mono (by grind)
  · rw [← measurable_iff_comap_le]
    exact adapted_action _

`filtrationAction_le_filtration`🔗

LemmaLearning.IT.filtrationAction_le_filtration

Details

No docstring.

theorem

Learning.IT.filtrationAction_le_filtration.{u_1, u_2} {𝓐 : Type u_1}
  {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨}
  {m n : ℕ} (h : m ≤ n) :
  ↑(filtrationAction 𝓐 𝓨) m ≤ ↑(IT.filtration 𝓐 𝓨) n
Learning.IT.filtrationAction_le_filtration.{u_1,
    u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} {m n : ℕ}
  (h : m ≤ n) :
  ↑(filtrationAction 𝓐 𝓨) m ≤
    ↑(IT.filtration 𝓐 𝓨) n

Code

lemma filtrationAction_le_filtration {m n : ℕ} (h : m ≤ n) :
    filtrationAction 𝓐 𝓨 m ≤ IT.filtration 𝓐 𝓨 n

Type uses (2)

Body uses (1)

filtrationAction_le_filtration_self

Actions: Source · Open Issue

Proof

(filtrationAction_le_filtration_self m).trans ((IT.filtration 𝓐 𝓨).mono h)

`measurable_action_filtrationAction`🔗

LemmaLearning.IT.measurable_action_filtrationAction

Details

No docstring.

theorem

Learning.IT.measurable_action_filtrationAction.{u_1, u_2} {𝓐 : Type u_1}
  {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨}
  (n : ℕ) : Measurable (action n)
Learning.IT.measurable_action_filtrationAction.{u_1,
    u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} (n : ℕ) :
  Measurable (action n)

Code

lemma measurable_action_filtrationAction (n : ℕ) :
    Measurable[filtrationAction 𝓐 𝓨 n] (action n)

Type uses (2)

Body uses (1)

filtration

Actions: Source · Open Issue

Proof

by
  rw [measurable_iff_comap_le]
  simp only [filtrationAction]
  split_ifs with hn
  · simp [hn]
  · exact le_sup_of_le_right le_rfl

`hasLaw_step_zero`🔗

LemmaLearning.IT.hasLaw_step_zero

Details

No docstring.

theorem

Learning.IT.hasLaw_step_zero.{u_1, u_2} {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨}
  (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) :
  ProbabilityTheory.HasLaw (step 0)
    (MeasureTheory.Measure.compProd (Algorithm.p0 alg)
      (Environment.ν0 env))
    (trajMeasure alg env)
Learning.IT.hasLaw_step_zero.{u_1, u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨}
  (alg : Algorithm 𝓐 𝓨)
  (env : Environment 𝓐 𝓨) :
  ProbabilityTheory.HasLaw (step 0)
    (MeasureTheory.Measure.compProd
      (Algorithm.p0 alg)
      (Environment.ν0 env))
    (trajMeasure alg env)

Code

lemma hasLaw_step_zero (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) :
    HasLaw (step 0) (alg.p0 ⊗ₘ env.ν0) (trajMeasure alg env) where
  aemeasurable

Type uses (4)

Body uses (5)

Used by (2)

Actions: Source · Open Issue

Proof

Measurable.aemeasurable (by fun_prop)
  map_eq := by
    unfold step
    rw [← coe_default_Iic_zero]
    simp only [trajMeasure, Kernel.trajMeasure]
    rw [← Measure.deterministic_comp_eq_map (by fun_prop), Measure.comp_assoc,
      Kernel.deterministic_comp_eq_map, Kernel.traj_zero_map_eval_zero,
      Measure.deterministic_comp_eq_map, Measure.map_map (by fun_prop) (by fun_prop)]
    exact Measure.map_id

`hasLaw_action_zero`🔗

LemmaLearning.IT.hasLaw_action_zero

Details

No docstring.

theorem

Learning.IT.hasLaw_action_zero.{u_1, u_2} {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨}
  (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) :
  ProbabilityTheory.HasLaw (action 0) (Algorithm.p0 alg)
    (trajMeasure alg env)
Learning.IT.hasLaw_action_zero.{u_1, u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨}
  (alg : Algorithm 𝓐 𝓨)
  (env : Environment 𝓐 𝓨) :
  ProbabilityTheory.HasLaw (action 0)
    (Algorithm.p0 alg)
    (trajMeasure alg env)

Code

lemma hasLaw_action_zero (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) :
    HasLaw (action 0) alg.p0 (trajMeasure alg env) where
  map_eq

Type uses (4)

Body uses (7)

Used by (2)

Actions: Source · Open Issue

Proof

by
    rw [← fst_comp_step, ← Measure.map_map (by fun_prop) (by fun_prop),
      (hasLaw_step_zero alg env).map_eq, ← Measure.fst, Measure.fst_compProd]

`hasCondDistrib_feedback_zero`🔗

LemmaLearning.IT.hasCondDistrib_feedback_zero

Details

No docstring.

theorem

Learning.IT.hasCondDistrib_feedback_zero.{u_1, u_2} {𝓐 : Type u_1}
  {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨}
  (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) :
  ProbabilityTheory.HasCondDistrib (feedback 0) (action 0)
    (Environment.ν0 env) (trajMeasure alg env)
Learning.IT.hasCondDistrib_feedback_zero.{u_1,
    u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨}
  (alg : Algorithm 𝓐 𝓨)
  (env : Environment 𝓐 𝓨) :
  ProbabilityTheory.HasCondDistrib
    (feedback 0) (action 0)
    (Environment.ν0 env)
    (trajMeasure alg env)

Code

lemma hasCondDistrib_feedback_zero (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) :
    HasCondDistrib (feedback 0) (action 0) env.ν0 (trajMeasure alg env)

Type uses (5)

Body uses (5)

Used by (2)

Actions: Source · Open Issue

Proof

by
  have h_step := (hasLaw_step_zero alg env).map_eq
  have h_action := (hasLaw_action_zero alg env).map_eq
  exact ⟨by fun_prop, by rwa [h_action]⟩

`hasCondDistrib_trajMeasure`🔗

LemmaProbabilityTheory.Kernel.hasCondDistrib_trajMeasure

Details

No docstring.

theorem

ProbabilityTheory.Kernel.hasCondDistrib_trajMeasure.{u_1, u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} (alg : Learning.Algorithm 𝓐 𝓨)
  (env : Learning.Environment 𝓐 𝓨) (n : ℕ) :
  HasCondDistrib (Learning.IT.step (n + 1)) (Learning.IT.hist n)
    (Learning.stepKernel alg env n) (Learning.trajMeasure alg env)
ProbabilityTheory.Kernel.hasCondDistrib_trajMeasure.{u_1,
    u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨}
  (alg : Learning.Algorithm 𝓐 𝓨)
  (env : Learning.Environment 𝓐 𝓨)
  (n : ℕ) :
  HasCondDistrib
    (Learning.IT.step (n + 1))
    (Learning.IT.hist n)
    (Learning.stepKernel alg env n)
    (Learning.trajMeasure alg env)

Code

lemma _root_.ProbabilityTheory.Kernel.hasCondDistrib_trajMeasure
    (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) (n : ℕ) :
    HasCondDistrib (step (n + 1)) (hist n) (stepKernel alg env n) (trajMeasure alg env)

Type uses (6)

Body uses (5)

Used by (1)

hasCondDistrib_step

Actions: Source · Open Issue

Proof

⟨by fun_prop, Kernel.map_frestrictLe_trajMeasure_compProd_eq_map_trajMeasure.symm⟩

`hasCondDistrib_step`🔗

LemmaLearning.IT.hasCondDistrib_step

Details

No docstring.

theorem

Learning.IT.hasCondDistrib_step.{u_1, u_2} {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨}
  (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) (n : ℕ) :
  ProbabilityTheory.HasCondDistrib (step (n + 1)) (hist n)
    (stepKernel alg env n) (trajMeasure alg env)
Learning.IT.hasCondDistrib_step.{u_1, u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨}
  (alg : Algorithm 𝓐 𝓨)
  (env : Environment 𝓐 𝓨) (n : ℕ) :
  ProbabilityTheory.HasCondDistrib
    (step (n + 1)) (hist n)
    (stepKernel alg env n)
    (trajMeasure alg env)

Code

lemma hasCondDistrib_step (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) (n : ℕ) :
    HasCondDistrib (step (n + 1)) (hist n) (stepKernel alg env n) (trajMeasure alg env)

Type uses (6)

Body uses (1)

hasCondDistrib_trajMeasure

Used by (3)

Actions: Source · Open Issue

Proof

Kernel.hasCondDistrib_trajMeasure alg env n

`hasCondDistrib_action`🔗

LemmaLearning.IT.hasCondDistrib_action

Details

No docstring.

theorem

Learning.IT.hasCondDistrib_action.{u_1, u_2} {𝓐 : Type u_1}
  {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨}
  (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) (n : ℕ) :
  ProbabilityTheory.HasCondDistrib (action (n + 1)) (hist n)
    (Algorithm.policy alg n) (trajMeasure alg env)
Learning.IT.hasCondDistrib_action.{u_1,
    u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨}
  (alg : Algorithm 𝓐 𝓨)
  (env : Environment 𝓐 𝓨) (n : ℕ) :
  ProbabilityTheory.HasCondDistrib
    (action (n + 1)) (hist n)
    (Algorithm.policy alg n)
    (trajMeasure alg env)

Code

lemma hasCondDistrib_action (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) (n : ℕ) :
    HasCondDistrib (action (n + 1)) (hist n) (alg.policy n) (trajMeasure alg env)

Type uses (5)

Body uses (7)

Used by (3)

Actions: Source · Open Issue

Proof

by
  rw [← fst_comp_step, ← fst_stepKernel, Kernel.fst_eq]
  exact HasCondDistrib.comp_left (hasCondDistrib_step alg env n) measurable_fst

`hasCondDistrib_feedback`🔗

LemmaLearning.IT.hasCondDistrib_feedback

Details

No docstring.

theorem

Learning.IT.hasCondDistrib_feedback.{u_1, u_2} {𝓐 : Type u_1}
  {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨}
  (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) (n : ℕ) :
  ProbabilityTheory.HasCondDistrib (feedback (n + 1))
    (fun ω => (hist n ω, action (n + 1) ω)) (Environment.feedback env n)
    (trajMeasure alg env)
Learning.IT.hasCondDistrib_feedback.{u_1,
    u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨}
  (alg : Algorithm 𝓐 𝓨)
  (env : Environment 𝓐 𝓨) (n : ℕ) :
  ProbabilityTheory.HasCondDistrib
    (feedback (n + 1))
    (fun ω =>
      (hist n ω, action (n + 1) ω))
    (Environment.feedback env n)
    (trajMeasure alg env)

Code

lemma hasCondDistrib_feedback (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) (n : ℕ) :
    HasCondDistrib (feedback (n + 1)) (fun ω ↦ (hist n ω, action (n + 1) ω)) (env.feedback n)
      (trajMeasure alg env)

Type uses (6)

Body uses (8)

Used by (2)

Actions: Source · Open Issue

Proof

by
  have h_step := hasCondDistrib_step alg env n
  have h_action := hasCondDistrib_action alg env n
  refine ⟨by fun_prop, ?_⟩
  rw [h_action.map_eq, ← Measure.compProd_assoc, ← stepKernel, ← h_step.map_eq,
    Measure.map_map (by fun_prop) (by fun_prop)]
  rfl

`condDistrib_feedback_zero`🔗

LemmaLearning.IT.condDistrib_feedback_zero

Details

No docstring.

theorem

Learning.IT.condDistrib_feedback_zero.{u_1, u_2} {𝓐 : Type u_1}
  {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨}
  [StandardBorelSpace 𝓨] [Nonempty 𝓨] (alg : Algorithm 𝓐 𝓨)
  (env : Environment 𝓐 𝓨) :
  ⇑𝓛[feedback 0 | action 0;
        trajMeasure alg
          env] =ᵐ[MeasureTheory.Measure.map (action 0)
      (trajMeasure alg env)]
    ⇑(Environment.ν0 env)
Learning.IT.condDistrib_feedback_zero.{u_1,
    u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨}
  [StandardBorelSpace 𝓨] [Nonempty 𝓨]
  (alg : Algorithm 𝓐 𝓨)
  (env : Environment 𝓐 𝓨) :
  ⇑𝓛[feedback 0 | action 0;
        trajMeasure alg
          env] =ᵐ[MeasureTheory.Measure.map
      (action 0) (trajMeasure alg env)]
    ⇑(Environment.ν0 env)

Code

lemma condDistrib_feedback_zero [StandardBorelSpace 𝓨] [Nonempty 𝓨]
    (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) :
    condDistrib (feedback 0) (action 0) (trajMeasure alg env)
      =ᵐ[(trajMeasure alg env).map (action 0)] env.ν0

Type uses (6)

Body uses (3)

Actions: Source · Open Issue

Proof

(hasCondDistrib_feedback_zero alg env).condDistrib_eq

`condDistrib_step`🔗

LemmaLearning.IT.condDistrib_step

Details

No docstring.

theorem

Learning.IT.condDistrib_step.{u_1, u_2} {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨}
  [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨]
  [Nonempty 𝓨] (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) (n : ℕ) :
  ⇑𝓛[step (n + 1) | hist n;
        trajMeasure alg
          env] =ᵐ[MeasureTheory.Measure.map (hist n)
      (trajMeasure alg env)]
    ⇑(stepKernel alg env n)
Learning.IT.condDistrib_step.{u_1, u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨}
  [StandardBorelSpace 𝓐] [Nonempty 𝓐]
  [StandardBorelSpace 𝓨] [Nonempty 𝓨]
  (alg : Algorithm 𝓐 𝓨)
  (env : Environment 𝓐 𝓨) (n : ℕ) :
  ⇑𝓛[step (n + 1) | hist n;
        trajMeasure alg
          env] =ᵐ[MeasureTheory.Measure.map
      (hist n) (trajMeasure alg env)]
    ⇑(stepKernel alg env n)

Code

lemma condDistrib_step [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨]
    (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) (n : ℕ) :
    condDistrib (step (n + 1)) (hist n) (trajMeasure alg env)
      =ᵐ[(trajMeasure alg env).map (hist n)] stepKernel alg env n

Type uses (7)

Body uses (3)

Actions: Source · Open Issue

Proof

(hasCondDistrib_step alg env n).condDistrib_eq

`condDistrib_action`🔗

LemmaLearning.IT.condDistrib_action

Details

No docstring.

theorem

Learning.IT.condDistrib_action.{u_1, u_2} {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨}
  [StandardBorelSpace 𝓐] [Nonempty 𝓐] (alg : Algorithm 𝓐 𝓨)
  (env : Environment 𝓐 𝓨) (n : ℕ) :
  ⇑𝓛[action (n + 1) | hist n;
        trajMeasure alg
          env] =ᵐ[MeasureTheory.Measure.map (hist n)
      (trajMeasure alg env)]
    ⇑(Algorithm.policy alg n)
Learning.IT.condDistrib_action.{u_1, u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨}
  [StandardBorelSpace 𝓐] [Nonempty 𝓐]
  (alg : Algorithm 𝓐 𝓨)
  (env : Environment 𝓐 𝓨) (n : ℕ) :
  ⇑𝓛[action (n + 1) | hist n;
        trajMeasure alg
          env] =ᵐ[MeasureTheory.Measure.map
      (hist n) (trajMeasure alg env)]
    ⇑(Algorithm.policy alg n)

Code

lemma condDistrib_action [StandardBorelSpace 𝓐] [Nonempty 𝓐]
    (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) (n : ℕ) :
    condDistrib (action (n + 1)) (hist n) (trajMeasure alg env)
      =ᵐ[(trajMeasure alg env).map (hist n)] alg.policy n

Type uses (6)

Body uses (3)

Actions: Source · Open Issue

Proof

(hasCondDistrib_action alg env n).condDistrib_eq

`condDistrib_feedback`🔗

LemmaLearning.IT.condDistrib_feedback

Details

No docstring.

theorem

Learning.IT.condDistrib_feedback.{u_1, u_2} {𝓐 : Type u_1}
  {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨}
  [StandardBorelSpace 𝓨] [Nonempty 𝓨] (alg : Algorithm 𝓐 𝓨)
  (env : Environment 𝓐 𝓨) (n : ℕ) :
  ⇑𝓛[feedback (n + 1) | fun ω => (hist n ω, action (n + 1) ω);
        trajMeasure alg
          env] =ᵐ[MeasureTheory.Measure.map
      (fun ω => (hist n ω, action (n + 1) ω)) (trajMeasure alg env)]
    ⇑(Environment.feedback env n)
Learning.IT.condDistrib_feedback.{u_1,
    u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨}
  [StandardBorelSpace 𝓨] [Nonempty 𝓨]
  (alg : Algorithm 𝓐 𝓨)
  (env : Environment 𝓐 𝓨) (n : ℕ) :
  ⇑𝓛[feedback (n + 1) | fun ω =>
        (hist n ω, action (n + 1) ω);
        trajMeasure alg
          env] =ᵐ[MeasureTheory.Measure.map
      (fun ω =>
        (hist n ω, action (n + 1) ω))
      (trajMeasure alg env)]
    ⇑(Environment.feedback env n)

Code

lemma condDistrib_feedback [StandardBorelSpace 𝓨] [Nonempty 𝓨]
    (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) (n : ℕ) :
    condDistrib (feedback (n + 1)) (fun ω ↦ (hist n ω, action (n + 1) ω)) (trajMeasure alg env)
      =ᵐ[(trajMeasure alg env).map (fun ω ↦ (hist n ω, action (n + 1) ω))] env.feedback n

Type uses (7)

Body uses (3)

Actions: Source · Open Issue

Proof

(hasCondDistrib_feedback alg env n).condDistrib_eq

`isAlgEnvSeq_trajMeasure`🔗

LemmaLearning.IT.isAlgEnvSeq_trajMeasure

Details

No docstring.

theorem

Learning.IT.isAlgEnvSeq_trajMeasure.{u_1, u_2} {𝓐 : Type u_1}
  {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨}
  (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) :
  IsAlgEnvSeq action feedback alg env (trajMeasure alg env)
Learning.IT.isAlgEnvSeq_trajMeasure.{u_1,
    u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨}
  (alg : Algorithm 𝓐 𝓨)
  (env : Environment 𝓐 𝓨) :
  IsAlgEnvSeq action feedback alg env
    (trajMeasure alg env)

Code

lemma isAlgEnvSeq_trajMeasure (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) :
    IsAlgEnvSeq action feedback alg env (trajMeasure alg env) where
  hasLaw_action_zero

Type uses (7)

Body uses (7)

Used by (1)

isBayesAlgEnvSeq_bayesTrajMeasure

Actions: Source · Open Issue

Proof

hasLaw_action_zero alg env
  hasCondDistrib_feedback_zero := hasCondDistrib_feedback_zero alg env
  hasCondDistrib_action n := hasCondDistrib_action alg env n
  hasCondDistrib_feedback n := hasCondDistrib_feedback alg env n

3.5. SequentialLearning.IonescuTulceaSpace🔗

trajMeasure🔗

instIsProbabilityMeasureForallNatProdTrajMeasure🔗

map_trajectory🔗

eq_trajMeasure_map_frestrictLe_of_isAlgEnvSeqUntil🔗

isAlgEnvSeq_unique🔗

identDistrib_trajectory🔗

isAlgEnvSeqUntil_unique🔗

step🔗

action🔗

feedback🔗

hist🔗

fst_comp_step🔗

measurable_step🔗

measurable_step_prod🔗

measurable_action🔗

measurable_action_prod🔗

measurable_feedback🔗

measurable_feedback_prod🔗

measurable_hist🔗

hist_eq_frestrictLe🔗

filtration🔗

filtration_eq_comap🔗

step_eq_eval_comp_hist🔗

action_eq_eval_comp_hist🔗

feedback_eq_eval_comp_hist🔗

adapted_step🔗

adapted_hist🔗

adapted_action🔗

adapted_feedback🔗

filtrationAction🔗

filtrationAction_zero_eq_comap🔗

filtrationAction_eq_comap🔗

filtration_le_filtrationAction_add_one🔗

filtration_le_filtrationAction🔗

filtrationAction_le_filtration_self🔗

filtrationAction_le_filtration🔗

measurable_action_filtrationAction🔗

hasLaw_step_zero🔗

hasLaw_action_zero🔗

hasCondDistrib_feedback_zero🔗

hasCondDistrib_trajMeasure🔗

hasCondDistrib_step🔗

hasCondDistrib_action🔗

hasCondDistrib_feedback🔗

condDistrib_feedback_zero🔗

condDistrib_step🔗

condDistrib_action🔗

condDistrib_feedback🔗

isAlgEnvSeq_trajMeasure🔗

`trajMeasure`🔗

`instIsProbabilityMeasureForallNatProdTrajMeasure`🔗

`map_trajectory`🔗

`eq_trajMeasure_map_frestrictLe_of_isAlgEnvSeqUntil`🔗

`isAlgEnvSeq_unique`🔗

`identDistrib_trajectory`🔗

`isAlgEnvSeqUntil_unique`🔗

`step`🔗

`action`🔗

`feedback`🔗

`hist`🔗

`fst_comp_step`🔗

`measurable_step`🔗

`measurable_step_prod`🔗

`measurable_action`🔗

`measurable_action_prod`🔗

`measurable_feedback`🔗

`measurable_feedback_prod`🔗

`measurable_hist`🔗

`hist_eq_frestrictLe`🔗

`filtration`🔗

`filtration_eq_comap`🔗

`step_eq_eval_comp_hist`🔗

`action_eq_eval_comp_hist`🔗

`feedback_eq_eval_comp_hist`🔗

`adapted_step`🔗

`adapted_hist`🔗

`adapted_action`🔗

`adapted_feedback`🔗

`filtrationAction`🔗

`filtrationAction_zero_eq_comap`🔗

`filtrationAction_eq_comap`🔗

`filtration_le_filtrationAction_add_one`🔗

`filtration_le_filtrationAction`🔗

`filtrationAction_le_filtration_self`🔗

`filtrationAction_le_filtration`🔗

`measurable_action_filtrationAction`🔗

`hasLaw_step_zero`🔗

`hasLaw_action_zero`🔗

`hasCondDistrib_feedback_zero`🔗

`hasCondDistrib_trajMeasure`🔗

`hasCondDistrib_step`🔗

`hasCondDistrib_action`🔗

`hasCondDistrib_feedback`🔗

`condDistrib_feedback_zero`🔗

`condDistrib_step`🔗

`condDistrib_action`🔗

`condDistrib_feedback`🔗

`isAlgEnvSeq_trajMeasure`🔗