WithZero

In this file we provide some basic API lemmas for the WithZero construction and we define the morphism WithZeroMultInt.toNNReal.

Main Definitions

• WithZeroMultInt.toNNReal : The MonoidWithZeroHom from ℤᵐ⁰ → ℝ≥0 sending 0 ↦ 0 and x ↦ e^(WithZero.log x) when x ≠ 0, for a nonzero e : ℝ≥0.

Main Results

• WithZeroMultInt.toNNReal_strictMono : The map withZeroMultIntToNNReal is strictly monotone whenever 1 < e.

Tags

WithZero, multiplicative, nnreal

noncomputable def WithZeroMulInt.toNNReal {e : NNReal} (he : e ≠ 0) : WithZero (Multiplicative ℤ) →*₀ NNReal

Given a nonzero e : ℝ≥0, this is the map ℤᵐ⁰ → ℝ≥0 sending 0 ↦ 0 and x ↦ e^(WithZero.log x) when x ≠ 0 as a MonoidWithZeroHom.

Equations

• WithZeroMulInt.toNNReal he = { toFun := fun (x : WithZero (Multiplicative ℤ)) => if hx : x = 0 then 0 else e ^ x.log, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }

theorem WithZeroMulInt.toNNReal_pos_apply {e : NNReal} (he : e ≠ 0) {x : WithZero (Multiplicative ℤ)} (hx : x = 0) : (toNNReal he) x = 0

theorem WithZeroMulInt.toNNReal_neg_apply {e : NNReal} (he : e ≠ 0) {x : WithZero (Multiplicative ℤ)} (hx : x ≠ 0) : (toNNReal he) x = e ^ x.log

theorem WithZeroMulInt.toNNReal_ne_zero {e : NNReal} {m : WithZero (Multiplicative ℤ)} (he : e ≠ 0) (hm : m ≠ 0) : (toNNReal he) m ≠ 0

toNNReal sends nonzero elements to nonzero elements.

theorem WithZeroMulInt.toNNReal_pos {e : NNReal} {m : WithZero (Multiplicative ℤ)} (he : e ≠ 0) (hm : m ≠ 0) : 0 < (toNNReal he) m

toNNReal sends nonzero elements to positive elements.

theorem WithZeroMulInt.toNNReal_strictMono {e : NNReal} (he : 1 < e) : StrictMono ⇑(toNNReal ⋯)

The map toNNReal is strictly monotone whenever 1 < e.

theorem WithZeroMulInt.toNNReal_eq_one_iff {e : NNReal} (m : WithZero (Multiplicative ℤ)) (he0 : e ≠ 0) (he1 : e ≠ 1) : (toNNReal he0) m = 1 ↔ m = 1

theorem WithZeroMulInt.toNNReal_lt_one_iff {e : NNReal} {m : WithZero (Multiplicative ℤ)} (he : 1 < e) : (toNNReal ⋯) m < 1 ↔ m < 1

theorem WithZeroMulInt.toNNReal_le_one_iff {e : NNReal} {m : WithZero (Multiplicative ℤ)} (he : 1 < e) : (toNNReal ⋯) m ≤ 1 ↔ m ≤ 1