Correct rounding of base-two and base-ten posit logarithms

The inverse relation between logarithm and exponentiation transfers every exact boundary comparison to the rational-power kernel. The resulting theorem includes rational logarithms, irrational logarithms, exact ties, signed saturation, and invalid argument domains.

theorem FloatLib.Floats.Formats.Posit.Model.Logarithm.compareTarget_eq_real (base argument candidate : ℚ) (degree : ℕ) (hbase : 1 < base) (hargument : 0 < argument) : compareTarget base argument candidate degree = cmp (Real.logb ↑base ↑argument) ↑candidate

Inverse power comparisons have exactly the real-logarithm ordering.

theorem FloatLib.Floats.Formats.Posit.Model.Logarithm.roundRat_eq_real (format : Format) (base argument : ℚ) (hbase : 1 < base) (hargument : 0 < argument) : roundRat format base argument = RealRounding.round format (Real.logb ↑base ↑argument)

A positive rational argument is rounded according to its exact signed real logarithm.

theorem FloatLib.Floats.Formats.Posit.Model.Logarithm.roundRat_eq_nar (format : Format) (base argument : ℚ) (hargument : argument ≤ 0) : roundRat format base argument = nar format

Nonpositive logarithm arguments are rejected before real logarithm evaluation.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.Logarithm.apply_nar {format : Format} (base offset : ℚ) : apply base offset (nar format) = nar format

NaR propagates through every logarithm and exact-offset logarithm.

theorem FloatLib.Floats.Formats.Posit.Model.Logarithm.apply_eq_real {format : Format} (base offset : ℚ) (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) (hbase : 1 < base) (hargument : 0 < q + offset) : apply base offset value = RealRounding.round format (Real.logb (↑base) (↑q + ↑offset))

Exact offset formation and logarithm evaluation are fused into one final rounding.

theorem FloatLib.Floats.Formats.Posit.Model.Logarithm.apply_eq_nar {format : Format} (base offset : ℚ) (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) (hargument : q + offset ≤ 0) : apply base offset value = nar format

An invalid exact-offset argument yields NaR.

theorem FloatLib.Floats.Formats.Posit.Model.log2_eq_real {format : Format} (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) (hq : 0 < q) : value.log2 = RealRounding.round format (Real.logb 2 ↑q)

Base-two logarithm has the signed real rounding required by the Posit Standard.

theorem FloatLib.Floats.Formats.Posit.Model.log10_eq_real {format : Format} (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) (hq : 0 < q) : value.log10 = RealRounding.round format (Real.logb 10 ↑q)

Base-ten logarithm has the signed real rounding required by the Posit Standard.

theorem FloatLib.Floats.Formats.Posit.Model.log2Plus1_eq_real {format : Format} (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) (hq : -1 < q) : value.log2Plus1 = RealRounding.round format (Real.logb 2 (1 + ↑q))

The base-two Plus1 operation rounds the exact logarithm of 1 + x once.

theorem FloatLib.Floats.Formats.Posit.Model.log10Plus1_eq_real {format : Format} (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) (hq : -1 < q) : value.log10Plus1 = RealRounding.round format (Real.logb 10 (1 + ↑q))

The base-ten Plus1 operation rounds the exact logarithm of 1 + x once.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.log2_nar {format : Format} : (nar format).log2 = nar format

Base-two logarithm propagates NaR.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.log10_nar {format : Format} : (nar format).log10 = nar format

Base-ten logarithm propagates NaR.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.log2Plus1_nar {format : Format} : (nar format).log2Plus1 = nar format

Base-two Plus1 propagates NaR.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.log10Plus1_nar {format : Format} : (nar format).log10Plus1 = nar format

Base-ten Plus1 propagates NaR.

theorem FloatLib.Floats.Formats.Posit.Model.log2_eq_nar_of_nonpos {format : Format} (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) (hq : q ≤ 0) : value.log2 = nar format

Base-two logarithm rejects zero and negative finite inputs.

theorem FloatLib.Floats.Formats.Posit.Model.log10_eq_nar_of_nonpos {format : Format} (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) (hq : q ≤ 0) : value.log10 = nar format

Base-ten logarithm rejects zero and negative finite inputs.

theorem FloatLib.Floats.Formats.Posit.Model.log2Plus1_eq_nar_of_le_neg_one {format : Format} (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) (hq : q ≤ -1) : value.log2Plus1 = nar format

Base-two Plus1 rejects finite inputs at or below -1.

theorem FloatLib.Floats.Formats.Posit.Model.log10Plus1_eq_nar_of_le_neg_one {format : Format} (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) (hq : q ≤ -1) : value.log10Plus1 = nar format

Base-ten Plus1 rejects finite inputs at or below -1.