KADIRI: Limit of I_2(T), equation 14#1602
Open
Robby955 wants to merge 3 commits into
Open
Conversation
Robby955
changed the title
Contributor
Author
|
awaiting-review |
Robby955
force-pushed
the
kadiri-eq14-limit-i2-2026-06-18
branch
from
4022e32 to
7d3b86d
Compare
…n LaplaceInversion Remove the eight private duplicates of bridge, tendsto, cpow, and sinc-kernel lemmas that are already public in PrimeNumberTheoremAnd/LaplaceInversion.lean, and call the prefix-free versions directly.
Replace the over-specific convert/simp step for (volume : Measure ℝ).comap Neg.neg = volume with an explicit MeasurableEquiv.comap_symm rewrite, which closes the goal under the current mathlib normal form.
Robby955
force-pushed
the
kadiri-eq14-limit-i2-2026-06-18
branch
from
e02d5b7 to
4084ce9
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This packages equation (14) of Théorème 3.1 (Kadiri 2005): the
T → ∞limit ofI_2(T), the companion piece to equation (13).As with (13), the argument rests on the Laplace-inversion results merged in #1579 and #1589, and the supporting lemmas are isolated in a new
KadiriEq14module so theKadiri.leanchange is just the node and its wiring. This module is on the larger side; if maintainers would rather it be split further before review, let me know the suggested improvement in the code/design and I can break it up.refactoring to v4.31.0 in progress
Tags:
AI