Skip to content

perf(NashEmbedding): cut median project build time by 12.45% #673

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Vilin97 merged 2 commits into from
Oct 18, 2026
Merged

perf(NashEmbedding): cut median project build time by 12.45% #673

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
1e22008
perf(NashEmbedding): narrow imports and streamline analytic estimates
Vilin97 Oct 17, 2026
af6d938
Remove unused compiler-private compatibility stubs
Vilin97 Oct 18, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions LeanPool/NashEmbedding.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,8 @@ Authors: David Wiygul
module


-- Preserve the entry point's tactic re-exports for downstream users.
public import Mathlib.Tactic -- shake: keep
public import LeanPool.NashEmbedding.NashEmbedding
public import LeanPool.NashEmbedding.NashEmbedding.Compact.AmbientMetric
public import LeanPool.NashEmbedding.NashEmbedding.Compact.Main
Expand Down
1 change: 1 addition & 0 deletions LeanPool/NashEmbedding/Imports.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -62,3 +62,4 @@ public import LeanPool.NashEmbedding.NashEmbeddingTest.NashCompact
public import LeanPool.NashEmbedding.NashEmbeddingTest.NashTorus
public import LeanPool.NashEmbedding.NashEmbeddingTest.RealizableMetrics
public import LeanPool.NashEmbedding.Solution
public import LeanPool.NashEmbedding.Tactics
2 changes: 1 addition & 1 deletion LeanPool/NashEmbedding/NashEmbedding/Compact/AmbientMetric.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ public import Mathlib.Geometry.Manifold.Algebra.LieGroup
public import Mathlib.Geometry.Manifold.Sheaf.Basic
public import Mathlib.Geometry.Manifold.VectorBundle.Riemannian
public import Mathlib.Geometry.Manifold.VectorField.Pullback
public import Mathlib.Tactic
public import LeanPool.NashEmbedding.Tactics

/-!
# The ambient metric along an immersion
Expand Down
2 changes: 1 addition & 1 deletion LeanPool/NashEmbedding/NashEmbedding/Compact/Main.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anthropic)
— at the request of David Wiygul
-/
public import Mathlib.Tactic
public import LeanPool.NashEmbedding.Tactics
public import Mathlib.Geometry.Manifold.Riemannian.Basic
public import LeanPool.NashEmbedding.NashEmbedding.Torus.Main
public import LeanPool.NashEmbedding.NashEmbedding.Compact.WhitneyExtension
Expand Down
2 changes: 1 addition & 1 deletion LeanPool/NashEmbedding/NashEmbedding/Compact/WhitneyExtension.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anth
-/
module

public import Mathlib.Tactic
public import LeanPool.NashEmbedding.Tactics
public import Mathlib.Geometry.Manifold.WhitneyEmbedding
import all Mathlib.Geometry.Manifold.WhitneyEmbedding

Expand Down
7 changes: 7 additions & 0 deletions LeanPool/NashEmbedding/NashEmbedding/Riemannian/Pullback.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -382,6 +382,13 @@ theorem prodForm_contMDiff (g : ContMDiffRiemannianMetric I ∞ E (TangentSpace
have hsnd : ContMDiff (I.prod I') I' ∞ (Prod.snd : M × M' → M') := contMDiff_snd
have hA := pullbackForm_contMDiff (I := I.prod I') (J := I) g hfst
have hB := pullbackForm_contMDiff (I := I.prod I') (J := I') g' hsnd
-- Fix the bundle instances before asking for smoothness of the sum of sections.
let : ∀ p : M × M', AddCommGroup
(TangentSpace (I.prod I') p →L[ℝ] TangentSpace (I.prod I') p →L[ℝ] ℝ) :=
fun _ => inferInstance
let : ∀ p : M × M', Module ℝ
(TangentSpace (I.prod I') p →L[ℝ] TangentSpace (I.prod I') p →L[ℝ] ℝ) :=
fun _ => inferInstance
refine (hA.add_section hB).congr fun p => ?_
have hp : prodFormT g g' p =
(fun p => pullbackFormT (I := I.prod I') (J := I) Prod.fst g p) p +
Expand Down
2 changes: 1 addition & 1 deletion LeanPool/NashEmbedding/NashEmbedding/Sobolev/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ public import Mathlib.Analysis.InnerProductSpace.Basic
public import Mathlib.Analysis.LocallyConvex.AbsConvexOpen
public import Mathlib.Analysis.SpecialFunctions.ExpDeriv
public import Mathlib.Analysis.SpecialFunctions.Pow.Real
public import Mathlib.Tactic
public import LeanPool.NashEmbedding.Tactics

/-!
# Sobolev spaces on the torus — definitions
Expand Down
2 changes: 1 addition & 1 deletion LeanPool/NashEmbedding/NashEmbedding/Sobolev/CoeffTransport.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anthropic)
— at the request of David Wiygul
-/
public import Mathlib.Tactic
public import LeanPool.NashEmbedding.Tactics
public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Periodization
public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.SynthesisRegularity
public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.ConvolutionAlgebra
Expand Down
3 changes: 2 additions & 1 deletion LeanPool/NashEmbedding/NashEmbedding/Sobolev/CompactInclusion.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,8 +13,9 @@ Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anth
— at the request of David Wiygul
-/
public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
public import Mathlib.Data.Pi.Interval
public import Mathlib.Tactic
public import LeanPool.NashEmbedding.Tactics
public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Limits

/-!
Expand Down
2 changes: 1 addition & 1 deletion LeanPool/NashEmbedding/NashEmbedding/Sobolev/Convolution.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anth
— at the request of David Wiygul
-/
public import Mathlib.MeasureTheory.Measure.Haar.NormedSpace
public import Mathlib.Tactic
public import LeanPool.NashEmbedding.Tactics
public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Distribution

/-!
Expand Down
2 changes: 1 addition & 1 deletion LeanPool/NashEmbedding/NashEmbedding/Sobolev/ConvolutionAlgebra.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anthropic)
— at the request of David Wiygul
-/
public import Mathlib.Tactic
public import LeanPool.NashEmbedding.Tactics
public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Basic
public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Differentiation
public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.FourierSynthesis
Expand Down
2 changes: 1 addition & 1 deletion LeanPool/NashEmbedding/NashEmbedding/Sobolev/Differentiation.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anth
-/
public import Mathlib.Analysis.Normed.Group.Tannery
public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
public import Mathlib.Tactic
public import LeanPool.NashEmbedding.Tactics
public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Basic
public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Summability

Expand Down
2 changes: 1 addition & 1 deletion LeanPool/NashEmbedding/NashEmbedding/Sobolev/Distribution.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anthropic)
— at the request of David Wiygul
-/
public import Mathlib.Tactic
public import LeanPool.NashEmbedding.Tactics
public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Basic
public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.CompactInclusion
public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Summability
Expand Down
2 changes: 1 addition & 1 deletion LeanPool/NashEmbedding/NashEmbedding/Sobolev/FourierSynthesis.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anth
-/
public import Mathlib.Analysis.SpecialFunctions.Integrals.Basic
public import Mathlib.MeasureTheory.Integral.Pi
public import Mathlib.Tactic
public import LeanPool.NashEmbedding.Tactics
public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Basic
public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Summability
public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Differentiation
Expand Down
2 changes: 1 addition & 1 deletion LeanPool/NashEmbedding/NashEmbedding/Sobolev/Inequalities.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anth
— at the request of David Wiygul
-/
public import Mathlib.Data.Finsupp.Notation
public import Mathlib.Tactic
public import LeanPool.NashEmbedding.Tactics
public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Distribution
public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Periodization

Expand Down
2 changes: 1 addition & 1 deletion LeanPool/NashEmbedding/NashEmbedding/Sobolev/IntegrationByParts.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anth
— at the request of David Wiygul
-/
public import Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
public import Mathlib.Tactic
public import LeanPool.NashEmbedding.Tactics
public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Convolution
public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Periodization
public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.RiemannSum
Expand Down
2 changes: 1 addition & 1 deletion LeanPool/NashEmbedding/NashEmbedding/Sobolev/Limits.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anth
— at the request of David Wiygul
-/
public import Mathlib.Algebra.Order.Chebyshev
public import Mathlib.Tactic
public import LeanPool.NashEmbedding.Tactics
public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Basic
public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Differentiation

Expand Down
2 changes: 1 addition & 1 deletion LeanPool/NashEmbedding/NashEmbedding/Sobolev/Mollifier.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anth
public import Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
public import Mathlib.Analysis.Calculus.BumpFunction.Normed
public import Mathlib.Analysis.Real.Pi.Bounds
public import Mathlib.Tactic
public import LeanPool.NashEmbedding.Tactics
public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.RiemannSum
public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.IntegrationByParts

Expand Down
2 changes: 1 addition & 1 deletion LeanPool/NashEmbedding/NashEmbedding/Sobolev/Multiplication.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anth
public import Mathlib.Algebra.Ring.IsFormallyReal
public import Mathlib.Data.Int.Star
public import Mathlib.LinearAlgebra.Complex.FiniteDimensional
public import Mathlib.Tactic
public import LeanPool.NashEmbedding.Tactics
public import Mathlib.Topology.Separation.CompletelyRegular
public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Basic
public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Distribution
Expand Down
Loading
Loading