klDiv_eq_top_iff — Mathlib

English

KL(μ, ν) equals ∞ if and only if μ ≪ ν implies not Integrable(llr μ ν) μ.

Русский

KL(μ, ν) бесконечно тогда и только тогда, когда μ ≪ ν → не интегрируем llr μ ν по μ.

LaTeX

$$$klDiv\\,\\mu\\,\\nu = \\infty \\iff \\mu\\ll\\nu \\rightarrow \\neg Integrable\\,(llr\\,\\mu\\,\\nu)\\,\\mu$$$

Lean4

theorem klDiv_eq_top_iff : klDiv μ ν = ∞ ↔ μ ≪ ν → ¬Integrable (llr μ ν) μ :=
  by
  constructor <;> intro h
  · contrapose! h
    simp [klDiv_of_ac_of_integrable h.1 h.2]
  · rcases or_not_of_imp h with (h | h) <;> simp [h]

Похожие утверждения