ENNReal lemmas #

@[reducible, inline]

abbrev Function.fsupport {α : Type u_1} {β : Type u_2} [Top β] [Zero β] (f : α → β) :

The finite support of a function X : α → β with top and zero elements is the set of points where X is neither ⊤ nor 0.

Equations

Instances For

theorem Function.fsupport_compl {α : Type u_1} {β : Type u_2} [Top β] [Zero β] (X : α → β) :

(fsupport X)ᶜ = {ω : α | X ω = ⊤} ∪ {ω : α | X ω = 0}

theorem Function.fsupport_compl_disjoint {α : Type u_1} {β : Type u_2} [Top β] [Zero β] (X : α → β) (h : 0 ≠ ⊤) :

Disjoint {ω : α | X ω = ⊤} {ω : α | X ω = 0}

theorem Function.not_mem_fsupport_iff {α : Type u_1} {β : Type u_2} [Top β] [Zero β] (X : α → β) (ω : α) :

ω ∉ fsupport X ↔ X ω = ⊤ ∨ X ω = 0

theorem ENNReal.eq_of_div_eq_one {a b : ENNReal} (h : a / b = 1) :

a = b

theorem ENNReal.inv_div_fsupport {α : Type u_1} (f g : α → ENNReal) (x : α) :

x ∈ Function.fsupport g → ((f / g) x)⁻¹ = g x / f x

(a / b).log = a.log - b.log

Documentation