import Mathlib.MeasureTheory.Order.Lattice
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.InformationTheory.KullbackLeibler.Basic
import Mathlib.MeasureTheory.Integral.Indicator
import Mathlib.Probability.Martingale.Convergence
import Mathlib.InformationTheory.KullbackLeibler.DataProcessing
import Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
import Mathlib.InformationTheory.KullbackLeibler.ChainRule
import Mathlib.Probability.Kernel.Composition.RadonNikodym
import Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous
import Mathlib.Probability.Kernel.Composition.Lemmas

/-! # Standalone extraction for `Learning.klDiv_compProd_compProd_compProd_prodMkLeft_eq_klDiv_comp_compProd`
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 InformationTheory
end InformationTheory
namespace ENNReal
end ENNReal
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.DivergenceDecomposition ═══
section
open MeasureTheory ProbabilityTheory InformationTheory Finset
open scoped ENNReal RealInnerProductSpace ENat
namespace Learning
variable {𝓞 𝓐 𝓨 : Type*} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {Ω Ω' : Type*} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {P : Measure Ω} {P' : Measure Ω'} [IsProbabilityMeasure P] [IsProbabilityMeasure P'] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {O' : ℕ → Ω' → 𝓞} {A' : ℕ → Ω' → 𝓐} {Y' : ℕ → Ω' → 𝓨}
section
variable {α β γ δ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} {μ : Measure α} [IsFiniteMeasure μ]

/-- The divergence of one step of an observation/policy/reward decomposition, in
composition-product form: the observation kernel `o` and the policy `π` are shared and the reward
kernels `κ`, `η` (which ignore the history and the observation) differ, so the divergence is the
conditional divergence of the reward kernels given the played action, whose law is
`π ∘ₘ (μ ⊗ₘ o)`. -/
lemma klDiv_compProd_compProd_compProd_prodMkLeft_eq_klDiv_comp_compProd (μ : Measure α)
    [IsFiniteMeasure μ] (o : Kernel α β) [IsMarkovKernel o] (π : Kernel (α × β) γ)
    [IsMarkovKernel π] (κ η : Kernel γ δ) [IsFiniteKernel κ] [IsFiniteKernel η] :
    klDiv (μ ⊗ₘ (o ⊗ₖ (π ⊗ₖ κ.prodMkLeft (α × β))))
        (μ ⊗ₘ (o ⊗ₖ (π ⊗ₖ η.prodMkLeft (α × β)))) =
      klDiv ((π ∘ₘ (μ ⊗ₘ o)) ⊗ₘ κ) ((π ∘ₘ (μ ⊗ₘ o)) ⊗ₘ η) := sorry

end
end Learning
end