Generalization of kl_pi

[LorenzoLuccioli]

The statement of kl_pi, the tensorization property over a finite number of measures for the KL divergence, is the following:

lemma kl_pi {ι : Type*} [hι : Fintype ι] {β : ι → Type*} [∀ i, MeasurableSpace (β i)]
    [∀ i, CountablyGenerated (β i)] {μ ν : (i : ι) → Measure (β i)}
    [∀ i, IsProbabilityMeasure (μ i)] [∀ i, IsProbabilityMeasure (ν i)] :
    kl (Measure.pi μ) (Measure.pi ν) = ∑ i, kl (μ i) (ν i) := by

In particular all the measure spaces are required to be countably generated and all the measures are required to be probability measures. On the other hand the following is the statement for the tensorization property over two pairs of measures:

lemma kl_prod_two [CountablyGenerated β] {ξ ψ : Measure β} [IsProbabilityMeasure ξ]
    [IsProbabilityMeasure ψ] [IsProbabilityMeasure μ] [IsFiniteMeasure ν] :
    kl (μ.prod ξ) (ν.prod ψ) = kl μ ν + kl ξ ψ := by

We can notice that here only the second space is required to be countably generated and only the second pair of measures are required to be probability measures. Therefore, since kl_pi is proven by induction using kl_prod_two, we could imagine a version of kl_pi where one of the spaces is allowed to be not countably generated, and the corresponding pair of measures are only required to be finite.
Nevertheless this generalization may be a bit hard to formalize. Some material that could be useful is in the implementation of product of kernels and measure spaces in the RD_it branch of Mathlib, where there is a structure for the product of measure spaces and some API, this may also be useful in order to generalize the chain rule.