Revision #1092 → #2101 · back to history
modifiedCommon logarithm32acaa19837a
| Field | From #1092 | To #2101 |
|---|
| mathlib.decl | — | Real.logb |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.Analysis.SpecialFunctions.Log.Base |
| note | — | Mathlib defines the general base-b logarithm `Real.logb`; the common logarithm is the specialization `Real.logb 10`, with no dedicated `log10` wrapper. |
| status | — | formalized |
addedMantissa property of base-10 logarithms966fd66c19f6
modifiedMantissa3e1bd4e26681
| Field | From #1092 | To #2101 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Mathlib has no definition of the mantissa of a base-10 logarithm; one would form `Int.fract (Real.logb 10 x)` ad hoc. |
| status | — | not_formalized |
modifiedCharacteristic3e316566e291
| Field | From #1092 | To #2101 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Mathlib does not define the characteristic (integer part) of a base-10 logarithm as a named concept. |
| status | — | not_formalized |
modifiedLogarithm of 120a0a1befc9a62
| Field | From #1092 | To #2101 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Concrete numeric demonstration; no specific worked-example lemma exists in Mathlib. |
| status | — | not_formalized |
modifiedNegative logarithms of numbers less than 1a14dd1fd2617
| Field | From #1092 | To #2101 |
|---|
| mathlib.decl | — | Real.logb_neg |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.Analysis.SpecialFunctions.Log.Base |
| note | — | `Real.logb_neg` states that for `1 < b` and `0 < x < 1`, `Real.logb b x < 0`, generalizing the base-10 claim. |
| status | — | formalized |
modifiedBar notationb12d0c29ddd4
| Field | From #1092 | To #2101 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Bar notation is a historical typographic convention for log tables; Mathlib has no such formalization. |
| status | — | not_formalized |
modifiedBar notation calculation of 0.012 × 0.85e1d044bd91ab
| Field | From #1092 | To #2101 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Worked numeric example with a non-formalized notation; not represented in Mathlib. |
| status | — | not_formalized |
modifiedMantissa invariance across powers of tencc1ee651ea9e
| Field | From #1092 | To #2101 |
|---|
| mathlib.decl | — | Real.logb_mul |
| mathlib.match_kind | — | — |
| mathlib.module | — | Mathlib.Analysis.SpecialFunctions.Log.Base |
| note | — | Derivable from `Real.logb_mul` and `Real.logb_pow`/`Real.logb_zpow`, but the explicit mantissa-invariance statement is not in Mathlib. |
| status | — | partial |
modifiedNumeric value identities for log base 1076f8d520bdea
| Field | From #1092 | To #2101 |
|---|
| mathlib.decl | — | Real.log_div_log |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.Analysis.SpecialFunctions.Log.Base |
| note | — | `Real.log_div_log` gives `Real.log x / Real.log b = Real.logb b x`, the change-of-base identity that underlies computing `log₁₀` from natural log. |
| status | — | formalized |
modifiedDerivative of a logarithmc2e26258e654
| Field | From #1092 | To #2101 |
|---|
| mathlib.decl | — | Real.deriv_log |
| mathlib.match_kind | — | — |
| mathlib.module | — | Mathlib.Analysis.SpecialFunctions.Log.Deriv |
| note | — | Mathlib has `Real.deriv_log` (`deriv Real.log x = x⁻¹`) but no dedicated derivative lemma for `Real.logb`; the base-b form must be obtained by combining `Real.log_div_log` with `Real.deriv_log`. |
| status | — | partial |