Add Ehrhart's sharp volume inequality - #387
Open
Vilin97 wants to merge 8 commits into
Open
Conversation
Greptile SummaryThe PR imports and registers a modular formalization of Ehrhart's sharp volume inequality.
|
| Filename | Overview |
|---|---|
| LeanPool/EhrhartVolumeInequality.lean | Defines the documented project entry point and publicly re-exports the complete module chain. |
| LeanPool/EhrhartVolumeInequality/Convergence.lean | Contains the final convergence arguments and the publicly exposed sharp volume inequality. |
| LeanPool/EhrhartVolumeInequality/Foundations.lean | Establishes the foundational definitions and centered-simplex sharpness declarations used by the headline result. |
| LeanPool/EhrhartVolumeInequality/Convexity.lean | Adds the convexity portion of the proof pipeline and publicly links later and earlier modules. |
| LeanPool/EhrhartVolumeInequality/FourierAnalysis.lean | Adds the Fourier-analytic stage of the formalization within the transitive public import chain. |
| LeanPool/projects.yml | Registers the project, its four main results, upstream revision, Apache-2.0 license, and provenance. |
| LeanPool.lean | Adds the Ehrhart entry module and all component modules to the repository umbrella import. |
Reviews (8): Last reviewed commit: "Merge remote-tracking branch 'origin/mai..." | Re-trigger Greptile
Contributor
Proof profile (new / modified Lean files)
This build covers the changed modules and their dependency cones on top of the restored cache. The serial per-file sums below are useful for ranking slow files, not as a build budget. Total heartbeats: 7,135 maxHeartbeats units across 8 files (56,429 added LOC). Sum of Count-heartbeats wall-clock total: 344.00 s. Repeated import cost inside Heartbeat values come from Mathlib's LOC counts added lines in the profiled Lean files from this PR diff.
Aggregate phase totals
Slowest changed modules (from
|
| Changed module | Lake time |
|---|---|
LeanPool.EhrhartVolumeInequality.Regularization |
29.00 s |
LeanPool.EhrhartVolumeInequality.Resolvent |
29.00 s |
LeanPool.EhrhartVolumeInequality.Foundations |
23.00 s |
LeanPool.EhrhartVolumeInequality.Variation |
23.00 s |
LeanPool.EhrhartVolumeInequality.FourierAnalysis |
22.00 s |
LeanPool.EhrhartVolumeInequality.Convexity |
21.00 s |
LeanPool.EhrhartVolumeInequality.Convergence |
7.40 s |
LeanPool.EhrhartVolumeInequality |
1.50 s |
Per-file `lean --profile` output
LeanPool/EhrhartVolumeInequality.lean
import took 2.3s
cumulative profiling times:
elaboration 0.15ms
import 2.3s
initialization 41ms
interpretation 191ms
linting 0.343ms
module linting 0.00167ms
overlappingInstancesLinter 0.491ms
parsing 0.0364ms
tacticAnalysis 2.35ms
real 3.23
user 1.38
sys 1.08
LeanPool/EhrhartVolumeInequality/Convergence.lean
import took 2.47s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 319ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 161ms
tactic execution of Mathlib.Tactic.nlinarith took 249ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 104ms
cumulative profiling times:
aesop 88.8ms
attribute application 0.81ms
compilation (IR) 0.31ms
compilation (LCNF base) 2.77ms
compilation (LCNF impure) 1.26ms
compilation (LCNF mono) 1.92ms
congr simp thm 21.6ms
dsimp 84.8ms
elaboration 981ms
fix level params 7.16ms
import 2.47s
initialization 30.6ms
instantiate metavars 21.8ms
interpretation 2.74s
let-to-have transformation 1.34ms
linting 194ms
module linting 0.00201ms
norm_num 164ms
overlappingInstancesLinter 18.6ms
parsing 121ms
process pre-definitions 87.7ms
ring 197ms
share common exprs 77.3ms
simp 561ms
tactic execution 3.95s
tacticAnalysis 267ms
type checking 644ms
typeclass inference 3.07s
real 7.01
user 14.61
sys 1.34
LeanPool/EhrhartVolumeInequality/Convexity.lean
import took 1.79s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 119ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 983ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 174ms
elaboration took 145ms
tactic execution of Lean.Parser.Tactic.simpa took 222ms
tactic execution of Lean.Parser.Tactic.refine took 446ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 136ms
tactic execution of Mathlib.Tactic.nlinarith took 366ms
cumulative profiling times:
aesop 66.6ms
attribute application 4.34ms
blocked (unaccounted) 125ms
compilation (IR) 0.257ms
compilation (LCNF base) 1.89ms
compilation (LCNF impure) 0.916ms
compilation (LCNF mono) 1.4ms
congr simp thm 95.4ms
dsimp 286ms
elaboration 7.2s
fix level params 30.6ms
import 1.79s
initialization 30.4ms
instantiate metavars 58.7ms
interpretation 8.7s
let-to-have transformation 9.49ms
linting 661ms
module linting 0.00169ms
norm_num 332ms
overlappingInstancesLinter 89.2ms
parsing 480ms
process pre-definitions 340ms
ring 536ms
share common exprs 282ms
simp 1.23s
tactic execution 16s
tacticAnalysis 958ms
type checking 3.25s
typeclass inference 13.2s
real 17.68
user 55.19
sys 1.52
LeanPool/EhrhartVolumeInequality/Foundations.lean
import took 1.71s
tactic execution of Lean.Parser.Tactic.refine took 854ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 105ms
simp took 135ms
simp took 148ms
simp took 170ms
typeclass inference of CoeT took 122ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 124ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 131ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 105ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 267ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 198ms
cumulative profiling times:
aesop 171ms
attribute application 7.27ms
blocked (unaccounted) 7.23s
compilation (IR) 1.93ms
compilation (LCNF base) 29.1ms
compilation (LCNF impure) 7.73ms
compilation (LCNF mono) 14.9ms
congr simp thm 80.2ms
dsimp 162ms
elaboration 2.6s
fix level params 38.2ms
import 1.71s
initialization 39.4ms
instantiate metavars 83.3ms
interpretation 9.51s
let-to-have transformation 7.62ms
linting 737ms
module linting 0.00175ms
norm_num 537ms
overlappingInstancesLinter 124ms
parsing 513ms
process pre-definitions 461ms
ring 848ms
share common exprs 346ms
simp 2.85s
tactic execution 8.99s
tacticAnalysis 1.09s
type checking 3.34s
typeclass inference 15.6s
real 16.62
user 48.74
sys 1.81
LeanPool/EhrhartVolumeInequality/FourierAnalysis.lean
import took 1.72s
typeclass inference of Module.IsTorsionFree took 135ms
typeclass inference of ZeroHomClass took 117ms
tactic execution of Lean.Parser.Tactic.exact took 168ms
cumulative profiling times:
attribute application 13.1ms
blocked (unaccounted) 9.3s
compilation (IR) 0.584ms
compilation (LCNF base) 5.32ms
compilation (LCNF impure) 2.32ms
compilation (LCNF mono) 3.88ms
congr simp thm 59.5ms
dsimp 239ms
elaboration 4.04s
fix level params 34.2ms
import 1.72s
initialization 34.7ms
instantiate metavars 50.5ms
interpretation 6.54s
let-to-have transformation 12.8ms
linting 746ms
module linting 0.00173ms
norm_num 221ms
overlappingInstancesLinter 104ms
parsing 531ms
process pre-definitions 492ms
ring 420ms
share common exprs 291ms
simp 1.48s
tactic execution 10.3s
tacticAnalysis 1.01s
type checking 4.7s
typeclass inference 21.6s
real 19.01
user 53.99
sys 1.79
LeanPool/EhrhartVolumeInequality/Regularization.lean
import took 1.77s
elaboration took 112ms
simp took 164ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 106ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 103ms
typeclass inference of MeasureTheory.Measure.IsNegInvariant took 102ms
tactic execution of Lean.Parser.Tactic.exact took 171ms
tactic execution of Lean.Parser.Tactic.exact took 110ms
ring took 104ms
simp took 173ms
ring took 228ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 144ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 111ms
simp took 164ms
tactic execution of Lean.Parser.Tactic.change took 114ms
simp took 143ms
simp took 156ms
simp took 150ms
typeclass inference of SMul took 104ms
typeclass inference of SMul took 101ms
tactic execution of Lean.Parser.Tactic.refine took 205ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 170ms
tactic execution of Lean.Parser.Tactic.refine took 129ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 217ms
type checking took 144ms
cumulative profiling times:
attribute application 37ms
blocked (unaccounted) 1.56s
compilation (IR) 0.539ms
compilation (LCNF base) 4.86ms
compilation (LCNF impure) 2.05ms
compilation (LCNF mono) 3.56ms
congr simp thm 119ms
dsimp 287ms
elaboration 5.61s
fix level params 40.3ms
import 1.77s
initialization 34.7ms
instantiate metavars 72.6ms
interpretation 6.44s
let-to-have transformation 25.9ms
linting 715ms
module linting 0.00164ms
norm_num 159ms
overlappingInstancesLinter 113ms
parsing 527ms
process pre-definitions 506ms
ring 722ms
share common exprs 359ms
simp 3.77s
tactic execution 16.5s
tacticAnalysis 1.04s
type checking 5.36s
typeclass inference 29s
real 25.78
user 72.84
sys 1.68
LeanPool/EhrhartVolumeInequality/Resolvent.lean
import took 1.77s
tactic execution of Lean.calcTactic took 711ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 346ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 494ms
typeclass inference of Module.IsTorsionFree took 338ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 101ms
tactic execution of Lean.Parser.Tactic.change took 137ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 106ms
tactic execution of Lean.Parser.Tactic.refine took 130ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 207ms
type checking took 152ms
tactic execution of Mathlib.Tactic.nlinarith took 141ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 117ms
simp took 197ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 117ms
typeclass inference of SecondCountableTopologyEither took 152ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 136ms
cumulative profiling times:
attribute application 3.6ms
compilation (IR) 0.111ms
compilation (LCNF base) 1.52ms
compilation (LCNF impure) 0.422ms
compilation (LCNF mono) 0.759ms
congr simp thm 87.6ms
dsimp 360ms
elaboration 6.05s
fix level params 48ms
import 1.77s
initialization 30.7ms
instantiate metavars 94.7ms
interpretation 8.05s
let-to-have transformation 253ms
linting 716ms
module linting 0.00171ms
norm_num 119ms
overlappingInstancesLinter 95.3ms
parsing 538ms
process pre-definitions 588ms
ring 252ms
share common exprs 422ms
simp 2.64s
tactic execution 19.9s
tacticAnalysis 941ms
type checking 5.97s
typeclass inference 34.3s
real 26.88
user 82.93
sys 1.61
LeanPool/EhrhartVolumeInequality/Variation.lean
import took 1.68s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 133ms
tactic execution of Lean.Parser.Tactic.obtain took 108ms
tactic execution of Lean.Parser.Tactic.exact took 187ms
LeanPool/EhrhartVolumeInequality/Variation.lean:2965:34: error: unsolved goals
n k : ℕ
K : CenteredBody n
hk : 0 < k
F : SourceFiniteEnergyPotential K
htransport : finiteEnergySourceGradientPushforward F = normalizedTargetBodyMeasure K
b : OrthonormalBasis (Fin (bergmanDimension K k)) ℂ ↥(momentMonomialSpan K hk F htransport)
z : TorusCharacters.LogSpace n
s : ↥(momentMonomialSpan K hk F htransport)
hrepr :
(momentHolomorphicRepresentative K hk F htransport) (∑ i, ⟪b i, s⟫_ℂ • b i) z =
(momentHolomorphicRepresentative K hk F htransport) s z
i : Fin (bergmanDimension K k)
a✝ : i ∈ Finset.univ
⊢ ⟪↑((starRingEnd ℂ) ((momentHolomorphicRepresentative K hk F htransport) (b i) z) • b i), ↑s⟫_ℂ =
(momentHolomorphicRepresentative K hk F htransport) (b i) z * ⟪↑(b i), ↑s⟫_ℂ
tactic execution of Lean.Parser.Tactic.rewriteSeq took 212ms
typeclass inference of SeminormedAddCommGroup took 441ms
LeanPool/EhrhartVolumeInequality/Variation.lean:2969:42: warning: This simp argument is unused:
inner_smul_left
Hint: Omit it from the simp argument list.
[apply] simp only [Submodule.coe_inner, RingHomCompTriple.comp_apply, RingHom.id_apply]
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
LeanPool/EhrhartVolumeInequality/Variation.lean:2970:12: warning: This simp argument is unused:
RingHomCompTriple.comp_apply
Hint: Omit it from the simp argument list.
[apply] simp only [Submodule.coe_inner, inner_smul_left, RingHom.id_apply]
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
LeanPool/EhrhartVolumeInequality/Variation.lean:2971:12: warning: This simp argument is unused:
RingHom.id_apply
Hint: Omit it from the simp argument list.
[apply] simp only [Submodule.coe_inner, inner_smul_left, RingHomCompTriple.comp_apply]
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
tactic execution of Lean.Parser.Tactic.rewriteSeq took 172ms
tactic execution of Mathlib.Tactic.nlinarith took 142ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 149ms
tactic execution of Lean.Parser.Tactic.exact took 2.39s
tactic execution of Lean.Parser.Tactic.refine took 131ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 196ms
type checking took 111ms
tactic execution of Mathlib.Tactic.nlinarith took 270ms
cumulative profiling times:
aesop 69.6ms
attribute application 6.37ms
blocked (unaccounted) 3.1s
compilation (IR) 0.594ms
compilation (LCNF base) 7.6ms
compilation (LCNF impure) 2.46ms
compilation (LCNF mono) 3.9ms
congr simp thm 97.8ms
dsimp 276ms
elaboration 3.61s
fix level params 38.8ms
import 1.68s
initialization 31ms
instantiate metavars 61.3ms
interpretation 6.42s
let-to-have transformation 21.9ms
linting 740ms
module linting 0.00167ms
norm_num 164ms
overlappingInstancesLinter 98.4ms
parsing 489ms
process pre-definitions 472ms
ring 510ms
share common exprs 323ms
simp 2.74s
tactic execution 13.9s
tacticAnalysis 1.05s
type checking 4.37s
typeclass inference 22.6s
real 19.97
user 59.75
sys 1.67
error: profile command exited with status 1
Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.
Contributor
🤖 LLM review (
|
| Rubric | Verdict | Bottom line |
|---|---|---|
| Faithfulness | ✅ pass |
Based on the partial diff, all four headline declarations match their informal claims and expose exactly the stated geometric hypotheses. |
| Novelty | ✅ pass |
Based on the partial diff, none of the four headline results is already formalized in the supplied Mathlib or pool prior art. |
| Significance | ✅ pass |
Based on the partial diff, this is a good-fit research-level formalization of a named sharp theorem in convex geometry and geometry of numbers. |
| Sources | ✅ pass |
On the partial diff, the pinned ten-proofs repository is consistent as a provenance citation, but the cited commit’s contents are not visible enough to verify the theorem statement. |
| Code quality (advisory) | 🤔 discuss |
Partial-diff review: the proof code is structured, but the project carries a substantial block of semantically unrelated imports that needs dependency cleanup before merge. |
| Aspect | Value |
|---|---|
| Proves the claim | ✅ proves_it |
| Assumed, not proved | The main inequality takes the body’s convexity, compactness, full dimensionality, barycenter condition, and unique interior lattice point as hypotheses, all disclosed by the card; exists_centeredBody_sharp additionally assumes only 0 < n, while the two simplex equalities are unconditional. |
| Matches cited source | 🟡 unverifiable |
| Fit | ✅ good_fit |
| Level | research |
| Branch | convex geometry and geometry of numbers |
| Mode | theory_building |
| Code quality | 3 / 5 |
Statement check: The main theorem assumes 0 < n, convexity, compactness, nonempty interior, barycenter S = 0, and interiorLatticePoints S = {0}, then proves normalizedVolume S ≤ ((n : ℝ) + 1) ^ n / (n.factorial : ℝ); the other headlines establish the centered simplex’s exact volume and barycenter and construct it as a sharp CenteredBody witness.
The project proves Ehrhart's sharp volume bound via ehrhart_volume_inequality_for_sets and establishes sharpness through the centered simplex with exact volume, zero barycenter, and a unique interior lattice point.
Code quality findings (1)
- import-residue — PR-wide
The project uses unrelated number-theory, ring-theory, tactic-extension, and manifold modules as transitive dependency carriers. This obscures the actual requirements of each module and makes the development unnecessarily sensitive to unrelated Mathlib refactors. Replace these with direct imports for the declarations used in each consuming file, and remove tactic extensions that are not exercised.
Evidence: InLeanPool/EhrhartVolumeInequality/Foundations.lean:import Mathlib.NumberTheory.Height.NumberField,import Mathlib.NumberTheory.Height.Projectivization,import Mathlib.RingTheory.Etale.Weakly,import Mathlib.RingTheory.Henselian,import Mathlib.RingTheory.RegularLocalRing.Defs,import Mathlib.RingTheory.TotallySplit,import Mathlib.Tactic.NormNum.LegendreSymbol, andimport Mathlib.Tactic.NormNum.NatFib. The same pattern continues withimport Mathlib.Algebra.Ring.IsFormallyRealinVariation.leanandimport Mathlib.Geometry.Manifold.Sheaf.BasicinFourierAnalysis.lean.
Tokens: 2,498,798 in / 14,080 out across 5 rubric calls · Tier: flex · Effort: xhigh · Cost: $12.8108
Each rubric is an independent review against .github/review-rubrics/ on top of .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.
Owner
Author
|
/review |
Contributor
|
LLM review skipped: Lean Action CI conclusion was |
Vilin97
added
the
needs-maintainer
Owner
Author
|
Automation disposition: needs-maintainer Reviewed exact head bb8a246 after a verified repair pass. Unrelated imports were replaced by precise dependencies, the unused public dimension premise was removed, and the full project builds. The duplicated normalization-at-a-minimizer theory remains architectural, and the size-limited review still cannot cover the largest files; maintainer review is required before merge. |
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
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.
Summary
Optimization
Verification