[Merged by Bors] - feat: add function log⁺ (=positive part of the logarithm) and prove standard estimates by kebekus · Pull Request #21289 · leanprover-community/mathlib4

kebekus · 2025-01-31T12:08:05Z

Introduce the function log⁺, the positive part of the logarithm, as used in (Complex|Functional|Harmonic) Analysis and Probability Theory. Provide standard estimates for log⁺ of sums and products, as discussed on p.168 of Introduction of Complex Hyperbolic Spaces or p.4 of Nevanlinna Theory in Several Complex Variables and Diophantine Approximation.

This material is used in Project VD, which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane.

github-actions · 2025-01-31T12:09:02Z

PR summary 4c4f32850c

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Analysis.SpecialFunctions.Log.PosLog` (new file)	1529

Declarations diff

+ half_mul_log_add_log_abs
+ log_of_nat_eq_posLog
+ monotoneOn_posLog
+ posLog
+ posLog_abs
+ posLog_add
+ posLog_def
+ posLog_eq_log
+ posLog_eq_zero_iff
+ posLog_mul
+ posLog_nat_mul
+ posLog_neg
+ posLog_nonneg
+ posLog_prod
+ posLog_sub_posLog_inv
+ posLog_sum

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 script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

Mathlib/Analysis/SpecialFunctions/Log/Poslog.lean

Co-authored-by: Sebastien Gouezel <sebastien.gouezel@univ-rennes1.fr>

kebekus · 2025-01-31T13:08:06Z

@sgouezel Thanks for your blazing-fast response. I implemented all your suggestions. Should we also rename the file to PosLog then?

sgouezel · 2025-01-31T13:50:39Z

Yes, renaming the file is a good idea!

kebekus · 2025-01-31T13:56:09Z

The file has been renamed. Thanks.

Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean

Co-authored-by: Sebastien Gouezel <sebastien.gouezel@univ-rennes1.fr>

kebekus · 2025-01-31T15:39:58Z

Implemented all your suggestions, thanks.

sgouezel

bors d+
Thanks!

Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean

mathlib-bors · 2025-01-31T19:33:42Z

✌️ kebekus can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

Co-authored-by: Sebastien Gouezel <sebastien.gouezel@univ-rennes1.fr>

kebekus · 2025-01-31T19:36:57Z

bors r+

…tandard estimates (#21289) Introduce the function `log⁺`, the positive part of the logarithm, as used in (Complex|Functional|Harmonic) Analysis and Probability Theory. Provide standard estimates for `log⁺` of sums and products, as discussed on p.168 of [Introduction of Complex Hyperbolic Spaces](https://link.springer.com/book/10.1007/978-1-4757-1945-1) or p.4 of [Nevanlinna Theory in Several Complex Variables and Diophantine Approximation](https://link.springer.com/book/10.1007/978-4-431-54571-2). This material is used in [Project VD](https://github.com/kebekus/ProjectVD), which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane.

mathlib-bors · 2025-01-31T20:13:10Z

Pull request successfully merged into master.

Build succeeded:

kebekus · 2025-01-31T20:21:11Z

Thanks again!

* factorial-dvd-int: (143 commits) Apply suggestions from code review feat(Factorial): k! divides the product of any k successive integers feat(CategoryTheory): creation of finite limits (#21320) chore: update Mathlib dependencies 2025-02-01 (#21328) chore(GroupTheory/SpecificGroups/Alternating.lean): follow last minute review of JX (#21314) feat: `‖x‖ₑ.toNNReal = ‖x‖₊` (#21306) chore: cleanup imports in Archive/IfNormalization (#21318) doc: fix several typos (#21315) feat(CategoryTheory): transfer being iso along an iso in the arrow category (#21310) chore: delete declarations deprecated between 2024-01 and 2024-07 (#21271) feat(Analysis/Normed/Module/Dual): polar in a normed space as a submodule (#20084) chore(Data/ZMod/Basic): split `ZMod.valMinAbs` off (#21308) feat(GroupTheory/Perm/Centralizer): study the centralizer of a permutation (#17522) feat(RingTheory/LocalRing): `IsLocalRing` for subrings (#21168) chore: update Mathlib dependencies 2025-02-01 (#21312) chore: update Mathlib dependencies 2025-01-31 (#21311) feat: generalize `mem_dite` to `Membership α β` (#21262) feat: Lemmas for some monomial orders (#16177) feat(CategoryTheory): the localized category is monoidal (#12728) feat: add function log⁺ (=positive part of the logarithm) and prove standard estimates (#21289) feat(RingTheory/WittVector): ring of Witt vectors is p-adically complete (#21295) feat(GroupTheory/GroupAction/Blocks): more on blocks (#21284) fix(FieldTheory/KrullTopology): make `krullTopology_discreteTopology_of_finiteDimensional` universe polymorphic (#21299) feat(RingTheory/Artinian): integral non-zero-divisors are units over artinian rings (#21199) refactor(Topology/Gluing): simplify definition of `TopCat.GlueData.Rel` (#20653) feat(RingTheory/PowerSeries): binomial series (#20192) chore(Mathlib/RingTheory/MvPolynomial): rename MonomiaOrder.lCoeff to MonomialOrder.leadingCoeff (#21290) chore (RingTheory/HahnSeries): fix names that use coeff (#21279) feat: let `notation3` distinguish `Prop` vs `Type _ ` vs `Sort _` (#21233) chore(MeasureTheory/Function/StronglyMeasurable): split Basic into Basic and AEStronglyMeasurable (#21273) feat(CategoryTheory): the monoidal category structure on a localization (#20951) feat(Analysis/Complex/Hadamard): generalize Hadamard's three lines theorem (#15009) feat(Order/CompleteBooleanAlgebra): Himp in terms of sSup (#20328) feat(ENNReal/Basic): add `ofNat_ne_top` and `top_ne_ofNat` (#14486) feat: Function.const as a PartialEquiv (#21137) chore(NonZeroDivisors): don't import rings (#20871) feat(Data/Set/Lattice): insert distributivity with iUnion/iInter (#21267) feat(GroupTheory/SpecificGroups/AlternatingGroup): subgroups of index 2 of Equiv.Perm (#21190) feat(GroupTheory/GroupAction/Transitive): basic results on transitive actions (#21285) perf(MeasureTheory/Function/LpSpace.lean): speed up (#21179) feat(Order): order isomorphisms from `Fin n` for small `n` (#21120) refactor(Topology/Group): turn morphisms in ProfiniteGrp into one field structures (#20740) feat: Sylow's first theorem for elementary `p`-groups (#21072) chore(Submonoid/Membership): don't import `MonoidWithZero` (#20748) refactor(Algebra/Algebra/Pi): cleanup and renaming (#21213) feat(GroupTheory/IndexNormal): subgroups of small index are normal (#21186) feat(Algebra/Group/Action): add definition of equidecomposition (#16936) feat(CategoryTheory/Subpresheaf): equalizer (#21096) feat: add lemmas about products of `Matrix.stdBasisMatrix` (#21204) chore: update Mathlib dependencies 2025-01-31 (#21282) ...

…tandard estimates (#21289) Introduce the function `log⁺`, the positive part of the logarithm, as used in (Complex|Functional|Harmonic) Analysis and Probability Theory. Provide standard estimates for `log⁺` of sums and products, as discussed on p.168 of [Introduction of Complex Hyperbolic Spaces](https://link.springer.com/book/10.1007/978-1-4757-1945-1) or p.4 of [Nevanlinna Theory in Several Complex Variables and Diophantine Approximation](https://link.springer.com/book/10.1007/978-4-431-54571-2). This material is used in [Project VD](https://github.com/kebekus/ProjectVD), which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane.

Add positive part of the logarithm

80649ec

kebekus requested a review from sgouezel January 31, 2025 12:08

github-actions bot added the t-analysis Analysis (normed *, calculus) label Jan 31, 2025

sgouezel reviewed Jan 31, 2025

View reviewed changes

sgouezel added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 31, 2025

kebekus and others added 6 commits January 31, 2025 13:54

Update Mathlib/Analysis/SpecialFunctions/Log/Poslog.lean

b02536d

Co-authored-by: Sebastien Gouezel <sebastien.gouezel@univ-rennes1.fr>

Update Mathlib/Analysis/SpecialFunctions/Log/Poslog.lean

7e436d5

Co-authored-by: Sebastien Gouezel <sebastien.gouezel@univ-rennes1.fr>

Update Mathlib/Analysis/SpecialFunctions/Log/Poslog.lean

aff5997

Co-authored-by: Sebastien Gouezel <sebastien.gouezel@univ-rennes1.fr>

Update Poslog.lean

5cb3705

Update Poslog.lean

5c2b3b6

Implement reviewer suggestion

ad58707

kebekus removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 31, 2025

Fix typos

fcdc759

Rename file

4184f77

sgouezel reviewed Jan 31, 2025

View reviewed changes

kebekus and others added 5 commits January 31, 2025 16:12

Update Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean

05fc216

Co-authored-by: Sebastien Gouezel <sebastien.gouezel@univ-rennes1.fr>

Update Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean

f1a1e24

Co-authored-by: Sebastien Gouezel <sebastien.gouezel@univ-rennes1.fr>

Update Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean

3d51ded

Co-authored-by: Sebastien Gouezel <sebastien.gouezel@univ-rennes1.fr>

Update Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean

74e0150

Co-authored-by: Sebastien Gouezel <sebastien.gouezel@univ-rennes1.fr>

Implement reviewer's suggestions

8273b2d

sgouezel reviewed Jan 31, 2025

View reviewed changes

Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean Outdated Show resolved Hide resolved

ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jan 31, 2025

Update Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean

4c4f328

Co-authored-by: Sebastien Gouezel <sebastien.gouezel@univ-rennes1.fr>

mathlib-bors bot changed the title ~~feat: add function log⁺ (=positive part of the logarithm) and prove standard estimates~~ [Merged by Bors] - feat: add function log⁺ (=positive part of the logarithm) and prove standard estimates Jan 31, 2025

mathlib-bors bot closed this Jan 31, 2025

mathlib-bors bot deleted the kebekus/poslog branch January 31, 2025 20:13

Conversation

kebekus commented Jan 31, 2025

Uh oh!

github-actions bot commented Jan 31, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 4c4f32850c

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

kebekus commented Jan 31, 2025

Uh oh!

sgouezel commented Jan 31, 2025

Uh oh!

kebekus commented Jan 31, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

kebekus commented Jan 31, 2025

Uh oh!

sgouezel left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

mathlib-bors bot commented Jan 31, 2025

Uh oh!

kebekus commented Jan 31, 2025

Uh oh!

mathlib-bors bot commented Jan 31, 2025

Uh oh!

kebekus commented Jan 31, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

github-actions bot commented Jan 31, 2025 •

edited

Loading