import Mathlib.MeasureTheory.Order.Lattice
import Mathlib.Probability.Kernel.Representation
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
import Mathlib.Probability.Kernel.Composition.MapComap
import Mathlib.Order.CompletePartialOrder
import Mathlib.Probability.Martingale.BorelCantelli
import Mathlib.Probability.IdentDistrib
import Mathlib.Probability.Independence.InfinitePi
import Mathlib.MeasureTheory.Function.FactorsThrough

/-! # Standalone extraction for `Bandits.ArrayModel.measurable_truncRow`
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 ProbabilityTheory
end ProbabilityTheory
namespace Learning
end Learning
namespace ENNReal
end ENNReal
namespace Bandits
end Bandits
namespace Bandits.ArrayModel
end Bandits.ArrayModel

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

-- ═══ Online.Bandit.ArrayProbSpace ═══
section
open MeasureTheory ProbabilityTheory Filter Finset Learning
open scoped ENNReal NNReal
namespace Bandits
variable {𝓐 𝓡 : Type*} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡}
section MeasureSpace
namespace ArrayModel
open unitInterval
section ProbabilitySpace

variable (𝓐 𝓡) in
/-- Probability space for the array model of stochastic bandits. -/
abbrev probSpace : Type _ := (ℕ → I) × (ℕ → 𝓐 → 𝓡)

/-- Modification of `ω` in which the rewards of action `a` are read only up to index `m - 1`:
in row `a` of the reward array, the entry at index `i` is kept if `i < m` and replaced by the entry
at index `m + 1 + i` otherwise. The result does not depend on the coordinate `(m, a)` of the
array. -/
def truncRow [DecidableEq 𝓐] (a : 𝓐) (m : ℕ) (ω : probSpace 𝓐 𝓡) : probSpace 𝓐 𝓡 :=
  (ω.1, fun i b ↦ if b = a then ω.2 (if i < m then i else m + 1 + i) b else ω.2 i b)

@[fun_prop]
lemma measurable_truncRow [DecidableEq 𝓐] (a : 𝓐) (m : ℕ) :
    Measurable (truncRow a m : probSpace 𝓐 𝓡 → probSpace 𝓐 𝓡) := sorry

variable [Nonempty 𝓐] [StandardBorelSpace 𝓐]
end ProbabilitySpace
variable [Nonempty 𝓐] [StandardBorelSpace 𝓐]
variable [DecidableEq 𝓐]
end ArrayModel
end MeasureSpace
end Bandits
end