Deterministic algorithms #
noncomputable def
Learning.detAlgorithm
{α : Type u_1}
{R : Type u_2}
{mα : MeasurableSpace α}
{mR : MeasurableSpace R}
(nextaction : (n : ℕ) → (↥(Finset.Iic n) → α × R) → α)
(h_next : ∀ (n : ℕ), Measurable (nextaction n))
(action0 : α)
:
Algorithm α R
A deterministic algorithm.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
Learning.detAlgorithm_policy
{α : Type u_1}
{R : Type u_2}
{mα : MeasurableSpace α}
{mR : MeasurableSpace R}
(nextaction : (n : ℕ) → (↥(Finset.Iic n) → α × R) → α)
(h_next : ∀ (n : ℕ), Measurable (nextaction n))
(action0 : α)
(n : ℕ)
:
(detAlgorithm nextaction h_next action0).policy n = ProbabilityTheory.Kernel.deterministic (nextaction n) ⋯
@[simp]
theorem
Learning.detAlgorithm_p0
{α : Type u_1}
{R : Type u_2}
{mα : MeasurableSpace α}
{mR : MeasurableSpace R}
(nextaction : (n : ℕ) → (↥(Finset.Iic n) → α × R) → α)
(h_next : ∀ (n : ℕ), Measurable (nextaction n))
(action0 : α)
:
theorem
Learning.HasLaw_action_zero_detAlgorithm
{α : Type u_1}
{R : Type u_2}
{mα : MeasurableSpace α}
{mR : MeasurableSpace R}
{nextaction : (n : ℕ) → (↥(Finset.Iic n) → α × R) → α}
{h_next : ∀ (n : ℕ), Measurable (nextaction n)}
{action0 : α}
{env : Environment α R}
:
ProbabilityTheory.HasLaw (action 0) (MeasureTheory.Measure.dirac action0)
(trajMeasure (detAlgorithm nextaction h_next action0) env)
theorem
Learning.action_zero_detAlgorithm
{α : Type u_1}
{R : Type u_2}
{mα : MeasurableSpace α}
{mR : MeasurableSpace R}
{nextaction : (n : ℕ) → (↥(Finset.Iic n) → α × R) → α}
{h_next : ∀ (n : ℕ), Measurable (nextaction n)}
{action0 : α}
{env : Environment α R}
[MeasurableSingletonClass α]
:
action 0 =ᵐ[trajMeasure (detAlgorithm nextaction h_next action0) env] fun (x : ℕ → α × R) => action0
theorem
Learning.action_detAlgorithm_ae_eq
{α : Type u_1}
{R : Type u_2}
{mα : MeasurableSpace α}
{mR : MeasurableSpace R}
{nextaction : (n : ℕ) → (↥(Finset.Iic n) → α × R) → α}
{h_next : ∀ (n : ℕ), Measurable (nextaction n)}
{action0 : α}
{env : Environment α R}
[StandardBorelSpace α]
[Nonempty α]
[StandardBorelSpace R]
[Nonempty R]
(n : ℕ)
:
action (n + 1) =ᵐ[trajMeasure (detAlgorithm nextaction h_next action0) env] fun (h : ℕ → α × R) =>
nextaction n fun (i : ↥(Finset.Iic n)) => h ↑i