BanditRLProof.LowerBounds.ConditionalKernelKL

The conditional KL term for two composition products with one common left measure is the iterated integral of `klFun` applied to the measurable kernel Radon--Nikodym derivative. This is the measurable formulation of the conditional-KL integral needed by the Chapter 15 history chain rule. Pointwise absolute continuity is explicit; without it, individual conditional KL terms may be infinite because of support mismatch.

theorem klDiv_compProd_same_left_eq_lintegral_kernelRN_ae {Base Target : Type*} [MeasurableSpace Base] [MeasurableSpace Target] [MeasurableSpace.CountablyGenerated Target] (mu : Measure Base) [IsFiniteMeasure mu] (kappa eta : Kernel Base Target) [IsMarkovKernel kappa] [IsMarkovKernel eta] (h_ac : ∀ᵐ base ∂mu, kappa base ≪ eta base) : InformationTheory.klDiv (mu ⊗ₘ kappa) (mu ⊗ₘ eta) = ∫⁻ x, ∫⁻ y, ENNReal.ofReal (InformationTheory.klFun ((kappa.rnDeriv eta x y).toReal)) ∂eta x ∂mu

Pointwise absolute continuity is a convenient sufficient specialization.

theorem klDiv_compProd_same_left_eq_lintegral_kernelRN {Base Target : Type*} [MeasurableSpace Base] [MeasurableSpace Target] [MeasurableSpace.CountablyGenerated Target] (mu : Measure Base) [IsFiniteMeasure mu] (kappa eta : Kernel Base Target) [IsMarkovKernel kappa] [IsMarkovKernel eta] (h_ac : forall base, kappa base ≪ eta base) : InformationTheory.klDiv (mu ⊗ₘ kappa) (mu ⊗ₘ eta) = ∫⁻ x, ∫⁻ y, ENNReal.ofReal (InformationTheory.klFun ((kappa.rnDeriv eta x y).toReal)) ∂eta x ∂mu

Under pointwise absolute continuity, the measurable kernel-RN formulation is equal to the familiar conditional-KL integral. This closes Mathlib's stated `klDiv_compProd_eq_add` TODO for the countably generated target-space branch.

theorem klDiv_compProd_same_left_eq_lintegral_klDiv {Base Target : Type*} [MeasurableSpace Base] [MeasurableSpace Target] [MeasurableSpace.CountablyGenerated Target] (mu : Measure Base) [IsFiniteMeasure mu] (kappa eta : Kernel Base Target) [IsMarkovKernel kappa] [IsMarkovKernel eta] (h_ac : forall base, kappa base ≪ eta base) : InformationTheory.klDiv (mu ⊗ₘ kappa) (mu ⊗ₘ eta) = ∫⁻ base, InformationTheory.klDiv (kappa base) (eta base) ∂mu

Conditional-KL integral under almost-everywhere conditional absolute continuity.

theorem klDiv_compProd_same_left_eq_lintegral_klDiv_ae {Base Target : Type*} [MeasurableSpace Base] [MeasurableSpace Target] [MeasurableSpace.CountablyGenerated Target] (mu : Measure Base) [IsFiniteMeasure mu] (kappa eta : Kernel Base Target) [IsMarkovKernel kappa] [IsMarkovKernel eta] (h_ac : ∀ᵐ base ∂mu, kappa base ≪ eta base) : InformationTheory.klDiv (mu ⊗ₘ kappa) (mu ⊗ₘ eta) = ∫⁻ base, InformationTheory.klDiv (kappa base) (eta base) ∂mu

If the conditional KL function is measurable, the same-left composition-product identity holds without an absolute-continuity hypothesis. Singular conditional fibres correctly contribute `∞` on sets of positive base measure.

theorem klDiv_compProd_same_left_eq_lintegral_klDiv_of_measurable {Base Target : Type*} [MeasurableSpace Base] [MeasurableSpace Target] [MeasurableSpace.CountablyGenerated Target] (mu : Measure Base) [IsFiniteMeasure mu] (kappa eta : Kernel Base Target) [IsMarkovKernel kappa] [IsMarkovKernel eta] (hmeasurable : Measurable (fun base => InformationTheory.klDiv (kappa base) (eta base))) : InformationTheory.klDiv (mu ⊗ₘ kappa) (mu ⊗ₘ eta) = ∫⁻ base, InformationTheory.klDiv (kappa base) (eta base) ∂mu

Relative entropy is invariant under a measurable equivalence.

theorem klDiv_map_measurableEquiv {Source Target : Type*} [MeasurableSpace Source] [MeasurableSpace Target] (mu nu : Measure Source) [IsFiniteMeasure mu] [IsFiniteMeasure nu] (equiv : Source ≃ᵐ Target) : InformationTheory.klDiv (mu.map equiv) (nu.map equiv) = InformationTheory.klDiv mu nu

For one adaptive bandit round, a common randomized policy contributes no KL cost of its own. The conditional history-extension cost is the first-law policy average of the selected arm reward-law KL divergences. The policy is an arbitrary Markov kernel from the complete visible history to the action space; in particular, this statement is not restricted to a deterministic action rule.

theorem klDiv_historyStep_samePolicy_eq_iterated_lintegral_armKL {History Action Reward : Type*} [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSpace.CountablyGenerated Action] [MeasurableSpace Reward] [MeasurableSpace.CountablyGenerated Reward] (historyLaw : Measure History) [IsFiniteMeasure historyLaw] (policy : Kernel History Action) [IsMarkovKernel policy] (armLaw referenceArmLaw : Kernel Action Reward) [IsMarkovKernel armLaw] [IsMarkovKernel referenceArmLaw] (h_ac : forall arm, armLaw arm ≪ referenceArmLaw arm) : InformationTheory.klDiv (historyLaw ⊗ₘ (policy ⊗ₖ armLaw.comap Prod.snd measurable_snd)) (historyLaw ⊗ₘ (policy ⊗ₖ referenceArmLaw.comap Prod.snd measurable_snd)) = ∫⁻ history, ∫⁻ arm, InformationTheory.klDiv (armLaw arm) (referenceArmLaw arm) ∂policy history ∂historyLaw

A finite action law admits the conditional-KL identity without an AC hypothesis.

theorem klDiv_finiteAction_compProd_eq_lintegral_armKL {K : Nat} {Reward : Type*} [MeasurableSpace Reward] [MeasurableSpace.CountablyGenerated Reward] (actionLaw : Measure (Fin K)) [IsFiniteMeasure actionLaw] (armLaw referenceArmLaw : Kernel (Fin K) Reward) [IsMarkovKernel armLaw] [IsMarkovKernel referenceArmLaw] : InformationTheory.klDiv (actionLaw ⊗ₘ armLaw) (actionLaw ⊗ₘ referenceArmLaw) = ∫⁻ arm, InformationTheory.klDiv (armLaw arm) (referenceArmLaw arm) ∂actionLaw

Finite-action conditional KL written as a weighted finite sum.

theorem klDiv_finiteAction_compProd_eq_sum_mass_mul_armKL {K : Nat} {Reward : Type*} [MeasurableSpace Reward] [MeasurableSpace.CountablyGenerated Reward] (actionLaw : Measure (Fin K)) [IsFiniteMeasure actionLaw] (armLaw referenceArmLaw : Kernel (Fin K) Reward) [IsMarkovKernel armLaw] [IsMarkovKernel referenceArmLaw] : InformationTheory.klDiv (actionLaw ⊗ₘ armLaw) (actionLaw ⊗ₘ referenceArmLaw) = ∑ arm : Fin K, actionLaw ({arm} : Set (Fin K)) * InformationTheory.klDiv (armLaw arm) (referenceArmLaw arm)

General finite-action same-policy one-round KL identity. Unlike the AC specialization above, this theorem also covers infinite arm divergences and zero-probability singular arms, with the standard `ENNReal` convention `0 * ∞ = 0`.

theorem klDiv_historyStep_samePolicy_eq_iterated_lintegral_armKL_general {History Reward : Type*} {K : Nat} [MeasurableSpace History] [MeasurableSpace Reward] [MeasurableSpace.CountablyGenerated Reward] (historyLaw : Measure History) [IsFiniteMeasure historyLaw] (policy : Kernel History (Fin K)) [IsMarkovKernel policy] (armLaw referenceArmLaw : Kernel (Fin K) Reward) [IsMarkovKernel armLaw] [IsMarkovKernel referenceArmLaw] : InformationTheory.klDiv (historyLaw ⊗ₘ (policy ⊗ₖ armLaw.comap Prod.snd measurable_snd)) (historyLaw ⊗ₘ (policy ⊗ₖ referenceArmLaw.comap Prod.snd measurable_snd)) = ∫⁻ history, ∫⁻ arm, InformationTheory.klDiv (armLaw arm) (referenceArmLaw arm) ∂policy history ∂historyLaw