PhysicalResampledRegret.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The deterministic first-crossing transfer under literal parent-only resampling.

theorem OAI.EditApproximation.sampledPrefixRegret_current_sample_congr line 13

Source documentation

A sampled regret at time t uses only the action sampled at that time.

theorem sampledPrefixRegret_current_sample_congr {β σ : Type*} [Fintype β]
    (charge κ : ℝ) (table : ℕ → β × σ → ℝ) (clipped : ℕ → ℝ)
    (first second : ℕ → β → σ) (t : ℕ) (heq : first t = second t) :
    sampledPrefixRegret charge κ table clipped first t =
      sampledPrefixRegret charge κ table clipped second t := by
…

Mentions: OAI.EditApproximation.clipped, OAI.EditApproximation.sampledPrefixRegret

theorem OAI.EditApproximation.physicalNode_resampled_regret line 20