Revision #1374 → #2833 · back to history
modifiedBinary logarithm678d331bd5c1
| Field | From #1374 | To #2833 |
|---|
| mathlib.module | Mathlib.Data.Nat.Log | Init.Data.Nat.Log2 |
| note | `Nat.log2` and `Real.logb 2` provide the binary logarithm, with `Nat.log2_eq_log_two` relating them. | `Nat.log2` (core) and `Real.logb 2` provide the binary logarithm; `Nat.log2_eq_log_two` in `Mathlib.Data.Nat.Log` relates `Nat.log2` to `Nat.log 2`. |
addedLogarithm of a quotientd28b7be3fceb
addedLogarithm of a power92895f5960df
modifiedExistence of logarithm (bijection)8d4c59515125
| Field | From #1374 | To #2833 |
|---|
| mathlib.module | Mathlib.Order.Hom.Basic | Mathlib.Order.Hom.Set |
| note | Strict monotonicity plus continuity yields injection/IVT-based surjection (e.g. `StrictMono.injective`, `Continuous.surjective`) but there isn't a single named bijectivity lemma. | Strict monotonicity plus continuity yields injection/IVT-based surjection (e.g. `StrictMono.injective`, `StrictMono.orderIsoOfSurjective`) but there isn't a single named bijectivity lemma tailored to log. |
addedIntermediate value theoremee51eea1ed71
addedLimit of log at infinity1d9c44995b81
addedLimit of log at 0cffbcdc21092
modifiedPower formula via integral81cc432d8ff7
| Field | From #1374 | To #2833 |
|---|
| mathlib.module | Mathlib.Analysis.SpecialFunctions.Log.Basic | Mathlib.Analysis.SpecialFunctions.Pow.Real |
addedTranscendental number156b441d5cdb
modifiedInverse hyperbolic tangent seriesd31b4c969c10
| Field | From #1374 | To #2833 |
|---|
| status | partial | formalized |
addedPrime-counting function4e40ae07839f
modifiedLog of n factorial43b22d5efadd
| Field | From #1374 | To #2833 |
|---|
| note | Stirling-style bounds on `log n!` (e.g. `le_log_factorial_stirling`) are in Mathlib, but the asymptotic `log n! ~ n log n - n` is not stated as such. | Stirling-style bounds on `log n!` (e.g. `Stirling.le_log_factorial_stirling`) are in Mathlib, but the asymptotic `log n! ~ n log n - n` is not stated as such. |
addedStirling's formula3e90f640609a
modifiedEuler's formulad2fe03360f8d
| Field | From #1374 | To #2833 |
|---|
| mathlib.module | Mathlib.Analysis.SpecialFunctions.Complex.Circle | Mathlib.Analysis.Complex.Trigonometric |
addedBranch cut975a820ebb61
addedExponential map (differential geometry)e691e740cce5
addedLambert W function9336c5c04beb