Finite posterior entropy as a sum of scalar integrals

import Definitions.Def_OnlineNRM_TSFixed_OracleEntropy

open MeasureTheory ProbabilityTheory
open scoped BigOperators

theorem OnlineNRM.TSFixed.finitePosteriorEntropy_sum
    {Ω α : Type*} [mΩ : MeasurableSpace Ω] [Fintype α]
    (P : Measure Ω) [IsProbabilityMeasure P]
    (m : MeasurableSpace Ω)
    (w : Ω → α → ℝ)
    (hwmeas : ∀ a, @Measurable Ω ℝ mΩ inferInstance (fun ω => w ω a))
    (hw0 : ∀ ω a, 0 ≤ w ω a)
    (hwsum : ∀ ω, ∑ a : α, w ω a = 1) :
    @ProbabilityTheory.finitePosteriorEntropy Ω α mΩ inferInstance P m w =
      ∑ a : α, ∫ ω, Real.negMulLog ((P[fun ω' => w ω' a | m]) ω) ∂P := by sorry