Conditional entropy of a finite probability vector decreases with more information

import Definitions.Def_OnlineNRM_TSFixed_OracleEntropy

open MeasureTheory ProbabilityTheory
open scoped BigOperators

theorem OnlineNRM.TSFixed.finitePosteriorEntropy_mono
    {Ω α : Type*} [mΩ : MeasurableSpace Ω] [Fintype α]
    (P : Measure Ω) [IsProbabilityMeasure P]
    (m₁ m₂ : MeasurableSpace Ω) (hm : m₁ ≤ m₂)
    (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 ≤
      @ProbabilityTheory.finitePosteriorEntropy Ω α mΩ inferInstance P m₁ w := by sorry