Source indexedlemma · leanprover/lean4:v4.33.0-rc1

tendsto_KLDiv_id_left

PFR.Kullback · PFR/Kullback.lean:443 to 456

Mathematical statement

Exact Lean statement

lemma tendsto_KLDiv_id_left [TopologicalSpace G] [DiscreteTopology G] [Finite G]
    [DiscreteMeasurableSpace G] {Y : Ω → G} {μ : Measure Ω}
    {α : Type*} {l : Filter α} {ν : α → ProbabilityMeasure G} {ν' : ProbabilityMeasure G}
    (h : Tendsto ν l (𝓝 ν')) :
    Tendsto (fun n ↦ KL[id ; ν n # Y ; μ]) l (𝓝 (KL[id ; ν' # Y ; μ]))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma tendsto_KLDiv_id_left [TopologicalSpace G] [DiscreteTopology G] [Finite G]    [DiscreteMeasurableSpace G] {Y : Ω → G} {μ : Measure Ω}    {α : Type*} {l : Filter α} {ν : α → ProbabilityMeasure G} {ν' : ProbabilityMeasure G}    (h : Tendsto ν l (𝓝 ν')) :    Tendsto (fun n ↦ KL[id ; ν n # Y ; μ]) l (𝓝 (KL[id ; ν' # Y ; μ])) := by  cases nonempty_fintype G  simp_rw [KLDiv_eq_sum_negMulLog]  apply tendsto_finsetSum _ (fun g hg ↦ ?_)  apply Tendsto.const_mul  apply continuous_negMulLog.continuousAt.tendsto.comp  apply Tendsto.div_const  simp only [Measure.map_id, measureReal_def]  rw [ENNReal.tendsto_toReal_iff (by simp) (by simp)]  exact (ProbabilityMeasure.tendsto_iff_forall_apply_tendsto_ennreal _ _).1 h g