perf(MetricCodes): narrow imports and simplify spectral proofs

LeanPool/MetricCodes/Binary.lean

@@ -7,6 +7,9 @@ module
 
 public import LeanPool.MetricCodes.Foundations
 import all Mathlib.Analysis.SpecialFunctions.BinaryEntropy
+import Mathlib.Algebra.Order.Floor.Semifield
+import Mathlib.Algebra.Order.Ring.Star
+import Mathlib.Algebra.Order.Star.Real
 
 /-!
 # Binary-code asymptotics

LeanPool/MetricCodes/Branching.lean

@@ -8,8 +8,14 @@ module
 public import LeanPool.MetricCodes.MatrixPerron
 public import LeanPool.MetricCodes.Representation
 public import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
-public import Mathlib.RingTheory.MvPolynomial.Groebner
 public import Mathlib.RingTheory.Regular.RegularSequence
+public import Mathlib.RingTheory.MvPolynomial.MonomialOrder
+import Mathlib.Algebra.Order.Floor.Semifield
+import Mathlib.Algebra.Order.Ring.Star
+import Mathlib.Algebra.Order.Star.Real
+import Mathlib.Algebra.Ring.IsFormallyReal
+import Mathlib.RingTheory.MvPolynomial.Groebner
+import Mathlib.Tactic.NormNum.RealSqrt
 
 /-!
 # Harmonic Young branching

LeanPool/MetricCodes/Conclusion.lean

@@ -6,6 +6,9 @@ Authors: OpenAI, Dean Cureton
 module
 
 public import LeanPool.MetricCodes.SpectralDecomposition
+import Mathlib.Algebra.Order.Floor.Semifield
+import Mathlib.LinearAlgebra.Eigenspace.Minpoly
+import Mathlib.Tactic.NormNum.RealSqrt
 
 /-!
 # Binary and spherical code bounds
@@ -206,7 +209,7 @@ theorem fixedLevelHierarchyCodeBound_of_actualCharacteristicMinor
     exact (boxSignature_interlaces a b hstable high).antitone_ambient
   intro p
   exact allRankCartanCharacteristicProjector_canonicalAxis_eq_physicalClebsch
-    lam mu h hgram hfinite hdom row hhigh hn p
+    (n := n) lam mu h hgram hfinite hdom row hhigh hn p
 
 end HigherYoungAllRankActualProjectedAxisCompletion
 
@@ -543,7 +546,7 @@ theorem physicalPaddedPieriChannel_adjoint_canonicalAxis_eq_zero_of_not_interlac
       (appendZeroWeight_antitone mu
         (interlaces_antitone_stabilizer h)) hbad
     intro a b
-    apply pieri_crossGram_intertwines_of_skew lam mu i C A
+    apply pieri_crossGram_intertwines_of_skew (n := n) lam mu i C A
       (youngAmbientRotation
         (paddedPieriSource (appendZeroWeight lam) i)
           a.castSucc b.castSucc)

LeanPool/MetricCodes/Foundations.lean

@@ -7,17 +7,20 @@ module
 
 public import LeanPool.MetricCodes.MatrixPerron
 public import Mathlib.InformationTheory.Hamming
-public import Mathlib.Algebra.Order.Chebyshev
-public import Mathlib.Algebra.Ring.IsFormallyReal
 public import Mathlib.Analysis.SpecialFunctions.BinaryEntropy
 import all Mathlib.Analysis.SpecialFunctions.BinaryEntropy
 public import Mathlib.Analysis.SpecialFunctions.Stirling
-public import Mathlib.Data.Nat.Dist
-public import Mathlib.LinearAlgebra.Matrix.PosDef
 public import Mathlib.LinearAlgebra.Matrix.Rank
-public import Mathlib.Algebra.Order.Floor.Semifield
-public import Mathlib.Algebra.Order.Star.Real
 public import Mathlib.Analysis.SpecialFunctions.Log.Base
+public import Mathlib.LinearAlgebra.Matrix.Hermitian
+import Mathlib.Algebra.Order.Archimedean.Real.Hom
+import Mathlib.Algebra.Order.Chebyshev
+import Mathlib.Algebra.Order.Floor.Semifield
+import Mathlib.Algebra.Order.Star.Real
+import Mathlib.Algebra.Ring.IsFormallyReal
+import Mathlib.Analysis.Matrix.Hermitian
+import Mathlib.Data.Nat.Dist
+import Mathlib.LinearAlgebra.Matrix.PosDef
 
 /-!
 # Foundations for binary and spherical code bounds
@@ -7551,59 +7554,62 @@ theorem associatedEdge_pos {n w p q j : ℕ}
       Nat.cast_add, Nat.cast_sub (by omega : w ≤ n)] using hcast
   have hJ : 0 < MetricCodes.johnsonJ n j := by
     unfold MetricCodes.johnsonJ
-    nlinarith
+    linarith only [hhalf', hjw']
   have hM : 0 < MetricCodes.johnsonM n w := by
     unfold MetricCodes.johnsonM
-    nlinarith
+    linarith only [hhalf']
   have hJminusM : 0 < MetricCodes.johnsonJ n j - MetricCodes.johnsonM n w := by
     unfold MetricCodes.johnsonJ MetricCodes.johnsonM
-    linarith
+    linarith only [hjw']
   have hJplusM : 0 < MetricCodes.johnsonJ n j + MetricCodes.johnsonM n w := by
-    linarith
+    exact add_pos hJ hM
   have hJminusDelta :
       0 < MetricCodes.johnsonJ n j - MetricCodes.johnsonDelta n w p q := by
     unfold MetricCodes.johnsonJ MetricCodes.johnsonDelta
       MetricCodes.johnsonJ2 MetricCodes.johnsonJ1
     rw [Nat.cast_sub (by omega : w ≤ n)]
-    linarith
+    linarith only [hjleft']
   have hJplusDelta :
       0 < MetricCodes.johnsonJ n j + MetricCodes.johnsonDelta n w p q := by
     unfold MetricCodes.johnsonJ MetricCodes.johnsonDelta
       MetricCodes.johnsonJ2 MetricCodes.johnsonJ1
     rw [Nat.cast_sub (by omega : w ≤ n)]
-    linarith
+    linarith only [hjright']
   have hSigmaMinus :
       0 < MetricCodes.johnsonSigma n w p q + 1 -
         MetricCodes.johnsonJ n j := by
     unfold MetricCodes.johnsonSigma MetricCodes.johnsonJ1 MetricCodes.johnsonJ2
       MetricCodes.johnsonJ
     rw [Nat.cast_sub (by omega : w ≤ n)]
-    linarith
+    linarith only [hfirst']
   have hSigmaPlus :
       0 < MetricCodes.johnsonSigma n w p q + 1 +
         MetricCodes.johnsonJ n j := by
-    linarith
+    linarith only [hSigmaMinus, hJ]
   have hJM :
       0 < MetricCodes.johnsonJ n j ^ 2 - MetricCodes.johnsonM n w ^ 2 := by
-    nlinarith [mul_pos hJminusM hJplusM]
+    rw [sq_sub_sq]
+    exact mul_pos hJplusM hJminusM
   have hJDelta :
       0 < MetricCodes.johnsonJ n j ^ 2 -
         MetricCodes.johnsonDelta n w p q ^ 2 := by
-    nlinarith [mul_pos hJminusDelta hJplusDelta]
+    rw [sq_sub_sq]
+    exact mul_pos hJplusDelta hJminusDelta
   have hSigma :
       0 < (MetricCodes.johnsonSigma n w p q + 1) ^ 2 -
         MetricCodes.johnsonJ n j ^ 2 := by
-    nlinarith [mul_pos hSigmaMinus hSigmaPlus]
+    rw [sq_sub_sq]
+    exact mul_pos hSigmaPlus hSigmaMinus
   have hjstep : (j : ℝ) + 1 ≤ (w : ℝ) := by
     exact_mod_cast Nat.succ_le_of_lt hjw
   have hhalfstep :
       (2 : ℝ) * (w : ℝ) + 1 ≤ (n : ℝ) := by
     exact_mod_cast (show 2 * w + 1 ≤ n by omega)
   have hdenleft : 0 < 2 * MetricCodes.johnsonJ n j - 1 := by
     unfold MetricCodes.johnsonJ
-    nlinarith
+    linarith only [hjstep, hhalfstep]
   have hdenright : 0 < 2 * MetricCodes.johnsonJ n j + 1 := by
-    linarith
+    linarith only [hJ]
   have hnu : 0 < MetricCodes.johnsonNu n w p q j := by
     unfold MetricCodes.johnsonNu
     apply div_pos
@@ -8491,9 +8497,7 @@ def shellRate (α β γ u : ℝ) : ℝ :=
 
 theorem binaryEntropy_eq_binEntropy_div_log (u : ℝ) :
     MetricCodes.binaryEntropy u = Real.binEntropy u / Real.log 2 := by
-  simp only [MetricCodes.binaryEntropy, Real.logb, Real.binEntropy,
-    Real.log_inv]
-  ring
+  exact MetricCodes.Hamming.binaryEntropy_eq_binEntropy_div_log u
 
 theorem binaryEntropy_le_one (u : ℝ) :
     MetricCodes.binaryEntropy u ≤ 1 := by

LeanPool/MetricCodes/HarmonicAnalysis.lean

@@ -6,10 +6,21 @@ Authors: OpenAI, Dean Cureton
 module
 
 public import LeanPool.MetricCodes.Rates
-public import Mathlib.Algebra.Order.Antidiag.FinsuppEquiv
-public import Mathlib.Analysis.InnerProductSpace.Trace
-public import Mathlib.RingTheory.MvPolynomial.EulerIdentity
-public import Mathlib.Topology.MetricSpace.CoveringNumbers
+public import Mathlib.Algebra.MvPolynomial.PDeriv
+public import Mathlib.Algebra.Order.Archimedean.Real.Hom
+public import Mathlib.LinearAlgebra.Trace
+public import Mathlib.RingTheory.MvPolynomial.Homogeneous
+import Mathlib.Algebra.MvPolynomial.CommRing
+import Mathlib.Algebra.Order.Antidiag.FinsuppEquiv
+import Mathlib.Algebra.Order.Floor.Semifield
+import Mathlib.Algebra.Order.Star.Real
+import Mathlib.Algebra.Ring.IsFormallyReal
+import Mathlib.Analysis.InnerProductSpace.Trace
+import Mathlib.Analysis.Matrix.Hermitian
+import Mathlib.Data.Nat.Dist
+import Mathlib.RingTheory.MvPolynomial.EulerIdentity
+import Mathlib.Tactic.NormNum.RealSqrt
+import Mathlib.Topology.MetricSpace.CoveringNumbers
 
 /-!
 # Harmonic analysis for spherical codes
@@ -2693,7 +2704,7 @@ theorem harmonicAxisLift_injective
   have hc := harmonicAxisProjection_correction_nonneg hn k
   have hproduct := mul_nonneg hc hdnonneg
   have hpzero : Fischer.harmonicInner n (k + 1) p p = 0 := by
-    nlinarith
+    exact le_antisymm ((le_add_of_nonneg_right hproduct).trans_eq hidentity.symm) hpnonneg
   exact (fischer_harmonicInner_self_eq_zero_iff
     n (k + 1) p).mp hpzero
 
@@ -5384,7 +5395,7 @@ theorem harmonicDimension_scaled_choose
       simp only [harmonicDimension]
       rw [htop, Nat.choose_succ_succ, hshift, hfactor]
       simp only [Nat.succ_eq_add_one] at hchoose ⊢
-      nlinarith
+      nlinarith only [hchoose, hnsub]
 
 theorem harmonicDimension_cross_mul
     {n : ℕ} (hn : 3 ≤ n) (i : ℕ) :

LeanPool/MetricCodes/Hierarchy.lean

@@ -6,6 +6,10 @@ Authors: OpenAI, Dean Cureton
 module
 
 public import LeanPool.MetricCodes.HarmonicAnalysis
+import Mathlib.Algebra.Order.Floor.Semifield
+import Mathlib.Algebra.Order.Ring.Star
+import Mathlib.Algebra.Order.Star.Real
+import Mathlib.Tactic.NormNum.RealSqrt
 
 /-!
 # Spherical-code hierarchy

LeanPool/MetricCodes/HighestWeights.lean

@@ -6,6 +6,10 @@ Authors: OpenAI, Dean Cureton
 module
 
 public import LeanPool.MetricCodes.Interlacing
+import Mathlib.Algebra.MvPolynomial.Monad
+import Mathlib.Algebra.Order.Floor.Semifield
+import Mathlib.Algebra.Order.Star.Real
+import Mathlib.Tactic.NormNum.RealSqrt
 
 /-!
 # Highest-weight identities

LeanPool/MetricCodes/Interlacing.lean

@@ -6,8 +6,11 @@ Authors: OpenAI, Dean Cureton
 module
 
 public import LeanPool.MetricCodes.Branching
-public import Mathlib.Algebra.Lie.Basic
-public import Mathlib.RingTheory.Derivation.Basic
+import Mathlib.Algebra.MvPolynomial.Monad
+import Mathlib.Algebra.Order.Floor.Semifield
+import Mathlib.Algebra.Order.Star.Real
+import Mathlib.RingTheory.MvPolynomial.EulerIdentity
+import Mathlib.Tactic.NormNum.RealSqrt
 
 /-!
 # Arbitrary-rank interlacing

LeanPool/MetricCodes/MatrixPerron.lean

@@ -5,10 +5,10 @@ Authors: OpenAI, Dean Cureton
 -/
 module
 
-public import Mathlib.Algebra.Order.Archimedean.Real.Hom
 public import Mathlib.Analysis.InnerProductSpace.Rayleigh
-public import Mathlib.Analysis.Matrix.Hermitian
 public import Mathlib.Combinatorics.Quiver.ConnectedComponent
+import Mathlib.Algebra.Order.Archimedean.Real.Hom
+import Mathlib.Analysis.Matrix.Hermitian
 
 /-!
 # Perron eigenvectors of finite nonnegative symmetric matrices

LeanPool/MetricCodes/Rates.lean

@@ -6,11 +6,15 @@ Authors: OpenAI, Dean Cureton
 module
 
 public import LeanPool.MetricCodes.Binary
-public import Mathlib.Tactic.NormNum.RealSqrt
 public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
-public import Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
-public import Mathlib.LinearAlgebra.Lagrange
 public import Mathlib.Probability.Distributions.Beta
+import Mathlib.Algebra.Order.Archimedean.Real.Hom
+import Mathlib.Algebra.Order.Floor.Semifield
+import Mathlib.Algebra.Order.Star.Real
+import Mathlib.Algebra.Ring.IsFormallyReal
+import Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
+import Mathlib.LinearAlgebra.Lagrange
+import Mathlib.Tactic.NormNum.RealSqrt
 
 /-!
 # Strict rate improvements

LeanPool/MetricCodes/Representation.lean

@@ -6,9 +6,17 @@ Authors: OpenAI, Dean Cureton
 module
 
 public import LeanPool.MetricCodes.Hierarchy
-public import Mathlib.Algebra.MvPolynomial.Funext
-public import Mathlib.Algebra.MvPolynomial.Monad
 public import Mathlib.Analysis.InnerProductSpace.TensorProduct
+import Mathlib.Algebra.MvPolynomial.CommRing
+import Mathlib.Algebra.MvPolynomial.Funext
+import Mathlib.Algebra.MvPolynomial.Monad
+import Mathlib.Algebra.Order.Antidiag.FinsuppEquiv
+import Mathlib.Algebra.Order.Floor.Semifield
+import Mathlib.Algebra.Order.Ring.Star
+import Mathlib.Algebra.Order.Star.Real
+import Mathlib.Algebra.Ring.IsFormallyReal
+import Mathlib.RingTheory.MvPolynomial.EulerIdentity
+import Mathlib.Tactic.NormNum.RealSqrt
 
 /-!
 # Representation-theoretic foundations

LeanPool/MetricCodes/Rigidity.lean

@@ -6,6 +6,9 @@ Authors: OpenAI, Dean Cureton
 module
 
 public import LeanPool.MetricCodes.Weyl
+import Mathlib.Algebra.Order.Floor.Semifield
+import Mathlib.Algebra.Order.Star.Real
+import Mathlib.Tactic.NormNum.RealSqrt
 
 /-!
 # All-rank harmonic rigidity

LeanPool/MetricCodes/RootComplex.lean

@@ -6,10 +6,14 @@ Authors: OpenAI, Dean Cureton
 module
 
 public import LeanPool.MetricCodes.HighestWeights
-public import Mathlib.Algebra.Lie.OfAssociative
 public import Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
 public import Mathlib.Algebra.Polynomial.Homogenize
-public import Mathlib.Data.Set.PowersetCard
+public import Mathlib.LinearAlgebra.Vandermonde
+import Mathlib.Algebra.Lie.OfAssociative
+import Mathlib.Algebra.MvPolynomial.Monad
+import Mathlib.Algebra.Order.Floor.Semifield
+import Mathlib.RingTheory.MvPolynomial.EulerIdentity
+import Mathlib.Tactic.NormNum.RealSqrt
 
 /-!
 # Universal root complexes
@@ -5449,7 +5453,7 @@ theorem admissibleRootWedge_above_card_isEmpty {r k : ℕ}
   constructor
   intro S
   have hle : S.val.val.card ≤ Fintype.card (PositiveRoot r) := by
-    simpa only [Set.powersetCard.card_eq, Finset.card_univ] using
+    simpa only [Finset.card_univ] using
       (Finset.card_le_card (Finset.subset_univ S.val.val))
   have hcard : S.val.val.card = k := S.val.property
   omega

LeanPool/MetricCodes/SpectralDecomposition.lean

@@ -6,6 +6,11 @@ Authors: OpenAI, Dean Cureton
 module
 
 public import LeanPool.MetricCodes.Rigidity
+public import Mathlib.LinearAlgebra.Lagrange
+import Mathlib.Algebra.Order.Floor.Semifield
+import Mathlib.Algebra.Ring.IsFormallyReal
+import Mathlib.LinearAlgebra.Eigenspace.Minpoly
+import Mathlib.Tactic.NormNum.RealSqrt
 
 /-!
 # Canonical spectral decomposition

LeanPool/MetricCodes/Weyl.lean

@@ -6,6 +6,9 @@ Authors: OpenAI, Dean Cureton
 module
 
 public import LeanPool.MetricCodes.RootComplex
+import Mathlib.Algebra.Order.Floor.Semifield
+import Mathlib.Algebra.Order.Ring.Star
+import Mathlib.Tactic.NormNum.RealSqrt
 
 /-!
 # Weyl and root-complex identities