import Mathlib.MeasureTheory.Order.Lattice
import Mathlib.Order.CompletePartialOrder
import Mathlib.Probability.Martingale.BorelCantelli
import Mathlib.Probability.Kernel.Basic
import Mathlib.Probability.Kernel.IonescuTulcea.Traj
import Mathlib.Probability.Process.FiniteDimensionalLaws
import Mathlib.Probability.HasCondDistrib
import Mathlib.MeasureTheory.Measure.ProbabilityMeasure
import Mathlib.Probability.Independence.Basic
import Mathlib.Probability.Independence.Conditional
import Mathlib.MeasureTheory.Measure.SubFinite
import Mathlib.Probability.Kernel.RadonNikodym
import Mathlib.MeasureTheory.MeasurableSpace.Embedding
import Mathlib.Order.Restriction
import Mathlib.Probability.Kernel.IonescuTulcea.Maps
import Mathlib.Analysis.Normed.Ring.Basic
import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

/-! # Standalone extraction for `Learning.rewardByCountUntil_congr`
Definitions are copied verbatim; theorem proofs are replaced by `sorry`.
Auto-generated by ChallengeGen. -/

set_option quotPrecheck false

-- Namespace stubs (so later `open`s resolve).
namespace Finset
end Finset
namespace MeasureTheory
end MeasureTheory
namespace Learning
end Learning

-- ═══ ForMathlib.MeasureTheory.Order.Lattice ═══
section
open Finset
variable {α δ : Type*} [MeasurableSpace δ] [SemilatticeInf α] {m : MeasurableSpace α} [MeasurableInf₂ α]
attribute [to_dual existing] MeasurableInf₂
end

-- ═══ SequentialLearning.FiniteActions ═══
section
open MeasureTheory Finset Learning
namespace Learning
variable {𝓞 𝓐 R Ω : Type*} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {mR : MeasurableSpace R} {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐] {P : Measure Ω} [IsProbabilityMeasure P] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} {a : 𝓐} {m n t : ℕ} {ω : Ω}
section PullCount

/-- Number of times action `a` was chosen up to time `t` (excluding `t`). -/
noncomputable
def pullCount (A : ℕ → Ω → 𝓐) (a : 𝓐) (t : ℕ) (ω : Ω) : ℕ :=
  #(filter (fun s ↦ A s ω = a) (range t))

end PullCount
section RewardByCount
variable {ω : Ω × (ℕ → 𝓐 → R)}

/-- Array of rewards by count, truncated at time `t`: the entry `(a, m)` is the reward received at
the `(m + 1)`-th pull of action `a` if that pull happened before time `t`, and the entry
`(m + 1, a)` of the auxiliary array `ω.2` otherwise.

This is an auxiliary definition used to prove results about the distribution of `rewardByCount`.

It is defined recursively: at time `t`, the
entry `(A t, pullCount A (A t) t)` is replaced by the reward `R' t`.
See `rewardByCountUntil_apply_of_lt_pullCount` and `rewardByCountUntil_apply_of_pullCount_le`. -/
noncomputable
def rewardByCountUntil (A : ℕ → Ω → 𝓐) (R' : ℕ → Ω → R) : ℕ → Ω × (ℕ → 𝓐 → R) → 𝓐 × ℕ → R
  | 0, ω => fun p ↦ ω.2 (p.2 + 1) p.1
  | t + 1, ω => Function.update (rewardByCountUntil A R' t ω)
      (A t ω.1, pullCount A (A t ω.1) t ω.1) (R' t ω.1)

/-- `rewardByCountUntil A R' t (x, z) p` depends on `z` only through `z (p.2 + 1) p.1`. -/
lemma rewardByCountUntil_congr {x : Ω} {z z' : ℕ → 𝓐 → R} (t : ℕ) (p : 𝓐 × ℕ)
    (hz : z (p.2 + 1) p.1 = z' (p.2 + 1) p.1) :
    rewardByCountUntil A R' t (x, z) p = rewardByCountUntil A R' t (x, z') p := sorry

end RewardByCount
end Learning
end