[Merged by Bors] - feat: elementary estimate for Real.log#20766
[Merged by Bors] - feat: elementary estimate for Real.log#20766
Conversation
|
messageFile.md |
tb65536
left a comment
There was a problem hiding this comment.
Why not simply generalize the existing log_pos_iff?
|
@tb65536 Thanks for your comment. Generalizing the existing If you reviewers believe that generalizing the existing |
|
My first instinct is also to generalise Also, one small thing: can you make sure the PR title follows the form e.g. "feat: elementary estimate for Real.log"? (Right now, that's the first line of your PR description, and the title is different. Mathlib's CI is a bit peculiar about this formatting; I've just corrected it for you.) Thanks! |
|
Thanks! I have one more comment (probably the last one). Can you also update the PR description to match what the PR does now? |
|
messageFile.md |
|
@grunweg Updated the PR description as you requested. The message by the github-action-bot leaves me puzzled. |
|
I implemented your suggestions and also fixed one very obvious typo in one of the docstrings of |
|
Thanks! The message by the bot should go away if you merge (or rebase on) the master branch. |
grunweg
left a comment
There was a problem hiding this comment.
Thanks!
maintainer merge
|
🚀 Pull request has been placed on the maintainer queue by grunweg. |
Generalize the theorem `log_pos_iff'`, weakening the hypothesis `hx : 0 < x` to the (perhaps more natural) hypothesis `hx : 0 ≤ x`. Do the same for `log_nonpos_iff` and depreciate `log_nonpos_iff'`. Fix one trivial typo in a docstring of `Mathlib/NumberTheory/Bertrand.lean`.
|
Build failed (retrying...): |
Generalize the theorem `log_pos_iff'`, weakening the hypothesis `hx : 0 < x` to the (perhaps more natural) hypothesis `hx : 0 ≤ x`. Do the same for `log_nonpos_iff` and depreciate `log_nonpos_iff'`. Fix one trivial typo in a docstring of `Mathlib/NumberTheory/Bertrand.lean`.
|
Build failed (retrying...): |
Generalize the theorem `log_pos_iff'`, weakening the hypothesis `hx : 0 < x` to the (perhaps more natural) hypothesis `hx : 0 ≤ x`. Do the same for `log_nonpos_iff` and depreciate `log_nonpos_iff'`. Fix one trivial typo in a docstring of `Mathlib/NumberTheory/Bertrand.lean`.
|
Build failed: |
PR summary fdc34626d8Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diffNo declarations were harmed in the making of this PR! 🐙 You can run this locally as follows## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for No changes to technical debt.You can run this locally as
|
|
@jcommelin It seems that my PR could not be merged because mathlib had changed meanwhile -- ironically, the conflicting change to 'master' was another PR of mine. I merged the master branch into kebekus/log and fixed the issue. Could you have a look and 'bors merge' again if all is fine? -- Thanks. |
|
Thanks! |
Generalize the theorem `log_pos_iff'`, weakening the hypothesis `hx : 0 < x` to the (perhaps more natural) hypothesis `hx : 0 ≤ x`. Do the same for `log_nonpos_iff` and depreciate `log_nonpos_iff'`. Fix one trivial typo in a docstring of `Mathlib/NumberTheory/Bertrand.lean`.
|
Pull request successfully merged into master. Build succeeded: |
* polynomial-sequences: (149 commits) Aha, here's how to get Lean to stop showing S.elems' in the infoview. Try satisfying the linter gods again. Probably enough initial tidying to send the PR. Kill more temporary names. Touch more natDegree. Does protected satisfy the docstring linter? Bit shorter. More Quiet linters. Remove redundant imports. Copyright header and more twiddling. Rename lemma to 'degree_smul_of_leadingCoeff_rightRegular' and split out feat(Polynomial): polynomial sequences are bases for R[X] chore(Dynamics/PeriodicPts): don't import `MonoidWithZero` (#20765) chore(Associated): split out `Ring` results (#20737) feat(AlgebraicGeometry): flat morphisms of schemes (#19790) feat(AlgebraicGeometry): scheme-theoretic fibre (#19427) chore: split Mathlib.Analysis.Asymptotics.Asymptotics (#20785) doc: typo (#20829) feat(CategoryTheory): condition for an induced functor between comma categories to be final (#20139) feat(1000.yaml): allow statements of theorems also (#20637) feat(Algebra/Homology/Embedding): homology of truncGE' (#19570) chore: cleanup many porting notes in Combinatorics (#20823) chore: eliminate porting notes about `deriving Fintype` (#20820) feat(Algebra/Lie): a Lie algebra is solvable iff it is solvable after faithfully flat base change (#20808) feat: define bases of root pairings (#20667) feat(Tactic): basic ConcreteCategory support for elementwise (#20811) feat(CategoryTheory): define unbundled `ConcreteCategory` class (#20810) chore(CategoryTheory): rename `ConcreteCategory` to `HasForget` (#20809) feat: `CommSemiring (NonemptyInterval ℚ≥0)` (#20783) chore(yaml_check.py): re-format (#20807) feat: elementary estimate for Real.log (#20766) feat: definition of linear topologies (#14990) feat(RingTheory): flatness over a semiring (#19115) feat(Algebra/Homology/Embedding): the canonical truncation truncLE (#19550) feat(Algebra/Homology/Embedding): API for the homology of an extension of homological complex (#19203) feat(Algebra/Ring): `RingEquiv.piUnique` (#20794) feat(RingTheory/LocalRing): add instance `Unique (MaximalSpectrum R)` for a local ring `R` (#20801) chore(GroupExtension/Defs): define `Section` and redefine `Splitting` (#20802) chore: restore `def` to `adicCompletion` (#20796) refactor: rename `UniqueContinuousFunctionalCalculus` to `ContinuousMap.UniqueHom` (#20643) feat(Algebra/Homology/Embedding): the morphism from a complex to its `truncGE` truncation (#19544) chore(Mathlib/Computability/TuringMachine): split file (#20790) feat(Data/Finset/Card): add `InjOn` and `SurjOn` versions of finset cardinality lemmas (#20753) feat(Order/WellFoundedSet): add convenience constructors for IsWF and IsPWO for WellFoundedLT types (#20752) feat(Set/Finite): a set is finite if its image and fibers are finite (#20751) chore: cleanup .gitignore files (#20795) feat(Topology/Group/Profinite): Profinite group is limit of finite group (#16992) feat(Combinatorics/SimpleGraph): vertices in cycles (#20602) CI: merge `bot_fix_style` actions (#20789) ...
Generalize the theorem
log_pos_iff', weakening the hypothesishx : 0 < xto the (perhaps more natural) hypothesishx : 0 ≤ x. Do the same forlog_nonpos_iffand depreciatelog_nonpos_iff'. Fix one trivial typo in a docstring ofMathlib/NumberTheory/Bertrand.lean.