BanditRLProof.DelayedFeedback.ActionLaw

A line-15 allocation together with the exact hypotheses needed to make its coordinates a probability distribution. EAP must eventually construct these fields; this structure does not assume that obligation away.

structure DelayedSAPOAllocation (K : Nat) where

The Algorithm 5 line-15 probability coordinate associated with a certified allocation.

noncomputable def probability {K : Nat} (allocation : DelayedSAPOAllocation K) (i : Fin K) : ℝ

No declaration docstring is present; use the chapter context and exact statement below.

theorem probability_nonnegative {K : Nat} (allocation : DelayedSAPOAllocation K) (i : Fin K) : 0 ≤ allocation.probability i

No declaration docstring is present; use the chapter context and exact statement below.

theorem sum_probability_eq_one {K : Nat} (allocation : DelayedSAPOAllocation K) : ∑ i, allocation.probability i = 1

Reuse the library's finite-action probability-vector interface instead of introducing a second ad hoc sampling semantics for Delayed SAPO.

theorem finiteActionDistribution {K : Nat} (allocation : DelayedSAPOAllocation K) : Exp3.FiniteActionDistribution (Finset.univ : Finset (Fin K)) allocation.probability where

One-round randomized action law induced by the certified line-15 allocation. A measurable history kernel and recursive generated trajectory remain separate obligations.

noncomputable def actionMeasure {K : Nat} (allocation : DelayedSAPOAllocation K) : Measure (Fin K)

No declaration docstring is present; use the chapter context and exact statement below.

theorem actionMeasure_isProbabilityMeasure {K : Nat} (allocation : DelayedSAPOAllocation K) : IsProbabilityMeasure allocation.actionMeasure

Convert a causal allocation rule into a causal, measure-valued action rule. The only input remains `ActionTimeView`; hidden delays and unobserved losses are not added to the algorithm interface.

noncomputable def causalDelayedSAPOActionMeasureRule {K : Nat} {Loss : Type*} (rule : CausalDecisionRule (Fin K) Loss (DelayedSAPOAllocation K)) : CausalDecisionRule (Fin K) Loss (Measure (Fin K))

Every output of the causal measure-valued rule is a probability measure.

theorem causalDelayedSAPOActionMeasureRule_isProbabilityMeasure {K : Nat} {Loss : Type*} (rule : CausalDecisionRule (Fin K) Loss (DelayedSAPOAllocation K)) (t : Nat) (view : ActionTimeView (Fin K) Loss) : IsProbabilityMeasure (causalDelayedSAPOActionMeasureRule rule t view)

Observation-equivalent hidden worlds induce exactly the same one-round Delayed SAPO action law for every allocation rule typed on the causal view.

theorem causalDelayedSAPOActionMeasureRule_eq_of_observation_equivalent {K : Nat} {Loss : Type*} (rule : CausalDecisionRule (Fin K) Loss (DelayedSAPOAllocation K)) (delay₁ delay₂ : Nat → Nat) (action₁ action₂ : Nat → Fin K) (loss₁ loss₂ : Nat → Loss) (t : Nat) (hvisible : observedBefore delay₁ t = observedBefore delay₂ t) (haction : ∀ s, s < t → action₁ s = action₂ s) (hloss : ∀ s, s ∈ observedBefore delay₁ t → loss₁ s = loss₂ s) : causalDelayedSAPOActionMeasureRule rule t (actionTimeViewAt delay₁ action₁ loss₁ t) = causalDelayedSAPOActionMeasureRule rule t (actionTimeViewAt delay₂ action₂ loss₂ t)