Optimize PhaseRetrieval analytic and Hermite proofs

LeanPool/PhaseRetrieval/Constant/Internal/AnnulusLocalEstimate.lean

@@ -49,10 +49,10 @@ private lemma freqBlock_pairwiseDisjoint :
   simp only [Function.onFun, freqBlock, Finset.disjoint_left, Finset.mem_Icc]
   intro n hn₁ hn₂
   rcases Nat.lt_or_gt_of_ne hne with h | h
-  · have : (ℓ₁ + 1) ^ 2 ≤ ℓ₂ ^ 2 := by nlinarith
+  · have : (ℓ₁ + 1) ^ 2 ≤ ℓ₂ ^ 2 := by nlinarith only [h]
     have := Nat.pos_of_ne_zero (show (ℓ₁ + 1) ^ 2 ≠ 0 by positivity)
     omega
-  · have : (ℓ₂ + 1) ^ 2 ≤ ℓ₁ ^ 2 := by nlinarith
+  · have : (ℓ₂ + 1) ^ 2 ≤ ℓ₁ ^ 2 := by nlinarith only [h]
     have := Nat.pos_of_ne_zero (show (ℓ₂ + 1) ^ 2 ≠ 0 by positivity)
     omega
 
@@ -80,7 +80,7 @@ private lemma sum_odd_sq (a b : ℕ) (h : a ≤ b) :
     by_cases ha' : a ≤ n
     · rw [Finset.sum_Icc_succ_top (by omega)]
       have := ih ha'
-      nlinarith [show (n + 2) ^ 2 = (n + 1) ^ 2 + 2 * (n + 1) + 1 from by ring]
+      linarith only [this, show (n + 2) ^ 2 = (n + 1) ^ 2 + 2 * (n + 1) + 1 from by ring]
     · have : a = n + 1 := by omega
       subst this; simp; ring
 
@@ -89,7 +89,7 @@ private lemma card_biUnion_freqBlock (a b : ℕ) (h : a ≤ b) :
     ((Finset.Icc a b).biUnion freqBlock).card = (b + 1) ^ 2 - a ^ 2 := by
   rw [Finset.card_biUnion (freqBlock_pairwiseDisjoint _)]
   simp_rw [FockSPR.freqBlock_card]
-  have h1 : a ^ 2 ≤ (b + 1) ^ 2 := by nlinarith
+  have h1 : a ^ 2 ≤ (b + 1) ^ 2 := by nlinarith only [h]
   have h2 := sum_odd_sq a b h
   omega
 
@@ -119,7 +119,7 @@ private lemma activeFreqSet_pos {D j n : ℕ} (hn : n ∈ activeFreqSet D j) :
     Finset.mem_Icc] at hn
   obtain ⟨⟨ℓ, hℓ, hn_block⟩, _⟩ := hn
   simp only [freqBlock, Finset.mem_Icc] at hn_block
-  nlinarith [sq_nonneg ℓ, show 1 ≤ ℓ by omega]
+  nlinarith only [hℓ, hn_block, sq_nonneg ℓ, show 1 ≤ ℓ by omega]
 
 /-- `localPoly a 5 j (r * fourier 1 t)` equals a Fourier sum over `activeFreqSet`.
     This is a mechanical reindexing of the `Fin D` sum into a `Finset ℕ` sum. -/
@@ -207,16 +207,22 @@ private lemma activeFreqSet_card_le {D : ℕ} (_hD : 1 ≤ D) {j : ℕ} (hj : j
       rw [hmax]
       -- (min(Λ,j+5)+1)^2 - (j-5)^2 ≤ (j+6)^2 - (j-5)^2 = 11*(2j+1) ≤ 17985
       have h_ub : min (maxBlockIndex D) (j + 5) + 1 ≤ j + 6 := by omega
-      have h_sq : (min (maxBlockIndex D) (j + 5) + 1) ^ 2 ≤ (j + 6) ^ 2 := by nlinarith
+      have h_sq : (min (maxBlockIndex D) (j + 5) + 1) ^ 2 ≤ (j + 6) ^ 2 := by
+        nlinarith only [
+          hrange, hmax, h_ub
+        ]
       suffices (j + 6) ^ 2 - (j - 5) ^ 2 ≤ 17985 by omega
       suffices (j + 6) ^ 2 = (j - 5) ^ 2 + 11 * (2 * j + 1) by omega
-      nlinarith [sq_nonneg (j - 5), Nat.sub_add_cancel (show 5 ≤ j by omega)]
+      nlinarith only [sq_nonneg (j - 5), Nat.sub_add_cancel (show 5 ≤ j by omega)]
     · -- j < 6: max(1,j-5) = 1
       have hmax : max 1 (j - 5) = 1 := by omega
       rw [hmax]
       have h_ub : min (maxBlockIndex D) (j + 5) + 1 ≤ j + 6 := by omega
-      have h_sq : (min (maxBlockIndex D) (j + 5) + 1) ^ 2 ≤ (j + 6) ^ 2 := by nlinarith
-      have h_jsm : (j + 6) ^ 2 ≤ 11 ^ 2 := by nlinarith
+      have h_sq : (min (maxBlockIndex D) (j + 5) + 1) ^ 2 ≤ (j + 6) ^ 2 := by
+        nlinarith only [
+          hrange, hmax, h_ub
+        ]
+      have h_jsm : (j + 6) ^ 2 ≤ 11 ^ 2 := by nlinarith only [hj6]
       omega
   · -- Empty range
     have : Finset.Icc (max 1 (j - 5)) (min (maxBlockIndex D) (j + 5)) = ∅ :=
@@ -276,7 +282,7 @@ private lemma high_freq_NL_condition (j : ℕ) (hj : 818 ≤ j) :
   have hk : 0 ≤ k := by omega
   rw [show (j : ℤ) - 5 = k + 813 from by omega,
       show 2 * (j : ℤ) + 1 = 2 * k + 1637 from by omega]
-  nlinarith [sq_nonneg k, sq_nonneg (k * k),
+  nlinarith only [sq_nonneg k, sq_nonneg (k * k),
     sq_nonneg (k * (k + 813)), hk]
 
 /-- `activeFreqSet` is contained in `Icc (j-5)² ((j+6)²-1)` for `j ≥ 6`. -/
@@ -290,7 +296,7 @@ private lemma activeFreqSet_subset_Icc {D j : ℕ} (hj6 : 6 ≤ j) :
   simp only [freqBlock, Finset.mem_Icc] at hn_block hℓ_range
   refine Finset.mem_Icc.mpr ⟨?_, ?_⟩
   · have : j - 5 ≤ ℓ := by omega
-    nlinarith
+    nlinarith only [hn_block, this]
   · have : ℓ + 1 ≤ j + 6 := by omega
     have : (ℓ + 1) ^ 2 ≤ (j + 6) ^ 2 :=
       Nat.pow_le_pow_left this 2
@@ -339,8 +345,8 @@ private lemma sum_Icc_eq_sum_Fin {α : Type*} [AddCommMonoid α]
 /-- `(j+6)^2 - 1 = (j-5)^2 + (11*(2*j+1)) - 1` for `j ≥ 5`. -/
 private lemma freq_range_eq (j : ℕ) (hj : 5 ≤ j) :
     (j + 6) ^ 2 - 1 = (j - 5) ^ 2 + (11 * (2 * j + 1)) - 1 := by
-  zify [show (j - 5) ^ 2 + (11 * (2 * j + 1)) ≥ 1 from by nlinarith,
-        show (j + 6) ^ 2 ≥ 1 from by nlinarith, show 5 ≤ j from hj]
+  zify [show (j - 5) ^ 2 + (11 * (2 * j + 1)) ≥ 1 from by nlinarith only [hj],
+        show (j + 6) ^ 2 ≥ 1 from by nlinarith only [hj], show 5 ≤ j from hj]
   ring
 
 /-- Case 2 (j ≥ 818): Apply `high_freq_band_estimate`. The high-frequency condition

LeanPool/PhaseRetrieval/Constant/Internal/BlockDecomposition.lean

@@ -98,7 +98,7 @@ private lemma freqBlock_unique {n ℓ₁ ℓ₂ : ℕ}
 /-- Every natural number belongs to `freqBlock (Nat.sqrt n)`. -/
 private lemma mem_freqBlock_sqrt (n : ℕ) : n ∈ freqBlock (Nat.sqrt n) := by
   simp only [freqBlock, Finset.mem_Icc]
-  exact ⟨by have := Nat.sqrt_le n; nlinarith,
+  exact ⟨by have := Nat.sqrt_le n; linarith only [this],
          by have h1 := Nat.lt_succ_sqrt' n; simp only [Nat.succ_eq_add_one] at h1; omega⟩
 
 /-- The cardinality of `freqBlock ℓ` is `2ℓ + 1`. -/
@@ -115,7 +115,7 @@ private lemma fourier_pow (t : AddCircle T) (n : ℕ) :
     ((fourier 1 t : ℂ)) ^ n = (fourier (↑n : ℤ) t : ℂ) := by
   induction n with
   | zero => simp
-  | succ n ih => rw [pow_succ, ih, ← fourier_add]; push_cast; ring_nf
+  | succ n ih => rw [pow_succ, ih, ← fourier_add]; push_cast; ring
 
 -- to_mathlib: Mathlib.Analysis.Fourier.AddCircle
 /-- Power of `fourier (-1)` equals the corresponding negative Fourier mode. -/
@@ -234,7 +234,7 @@ theorem blocks_cover (D : ℕ) (n : ℕ) (hn : 1 ≤ n) (_hnD : n ≤ D) :
   · exact Nat.sqrt_pos.mpr (by omega)
   · simp only [freqBlock, Finset.mem_Icc]
     refine ⟨?_, ?_⟩
-    · have := Nat.sqrt_le n; nlinarith
+    · have := Nat.sqrt_le n; linarith only [this]
     · have h1 := Nat.lt_succ_sqrt' n
       simp only [Nat.succ_eq_add_one] at h1; omega
 
@@ -354,15 +354,15 @@ theorem monomial_peak_localization {n ℓ : ℕ} (hℓ : 1 ≤ ℓ)
       rw [Real.sqrt_sq (by positivity)]]
     apply Real.sqrt_lt_sqrt (by positivity)
     have : (ℓ : ℝ) ^ 2 ≤ (n : ℝ) := by exact_mod_cast hn.1
-    linarith
+    linarith only [this]
   · rw [show (ℓ + 1 : ℝ) = Real.sqrt ((ℓ + 1 : ℝ) ^ 2) from by
       rw [Real.sqrt_sq (by positivity)]]
     apply Real.sqrt_lt_sqrt
-      (by linarith [show (0 : ℝ) ≤ n from Nat.cast_nonneg n])
+      (by linarith only [show (0 : ℝ) ≤ n from Nat.cast_nonneg n])
     have h1 : n + 1 ≤ (ℓ + 1) ^ 2 := by
       have : 0 < (ℓ + 1) ^ 2 := Nat.pos_of_ne_zero (by positivity)
       omega
     have : (n : ℝ) + 1 ≤ ((ℓ + 1 : ℕ) : ℝ) ^ 2 := by exact_mod_cast h1
-    push_cast at this ⊢; linarith
+    push_cast at this ⊢; linarith only [this]
 
 end FockSPR

LeanPool/PhaseRetrieval/Constant/Internal/Definitions.lean

@@ -182,7 +182,7 @@ private lemma norm_polyEvalCircle_le {D : ℕ} (a : Fin D → ℂ) (r : ℝ) (t
     Actually, we prove the simpler bound: ≤ (∑ ‖a_k‖ * |r|^{k+1})² . -/
 private lemma norm_sq_polyEvalCircle_le {D : ℕ} (a : Fin D → ℂ) (r : ℝ) (t : AddCircle T) :
     ‖polyEvalCircle a r t‖ ^ 2 ≤ (∑ k : Fin D, ‖a k‖ * |r| ^ (k.val + 1)) ^ 2 :=
-  sq_le_sq' (by linarith [norm_nonneg (polyEvalCircle a r t),
+  sq_le_sq' (by linarith only [norm_nonneg (polyEvalCircle a r t),
     Finset.sum_nonneg (fun k (_ : k ∈ Finset.univ) =>
       mul_nonneg (norm_nonneg (a k)) (pow_nonneg (abs_nonneg r) (k.val + 1)))])
     (norm_polyEvalCircle_le a r t)
@@ -375,7 +375,7 @@ private lemma integrableOn_polar_norm {D : ℕ} (a : Fin D → ℂ) :
             -- Goal: r³ * (∑ x, r^x.val * ‖a x‖)² ≤ 4*C²*r^{2D+1} + 4*C²*r³
             have hC_nn : 0 ≤ C := Finset.sum_nonneg (fun k _ => norm_nonneg (a k))
             by_cases hD : D = 0
-            · subst hD; simp; nlinarith [sq_nonneg C, pow_nonneg hr.le 3]
+            · subst hD; simp; nlinarith only [hr, sq_nonneg C, pow_nonneg hr.le 3]
             · -- D ≥ 1
               have hD_pos : 0 < D := Nat.pos_of_ne_zero hD
               -- Each r^k ≤ 1 + r^(D-1) for k ∈ {0,...,D-1}
@@ -384,11 +384,11 @@ private lemma integrableOn_polar_norm {D : ℕ} (a : Fin D → ℂ) :
                 intro k
                 by_cases hr1 : r ≤ 1
                 · have : r ^ k.val ≤ 1 := pow_le_one₀ (n := k.val) hr_nn hr1
-                  linarith [pow_nonneg hr_nn (D - 1)]
+                  linarith only [hr_nn, this, pow_nonneg hr_nn (D - 1)]
                 · push Not at hr1
                   have : r ^ k.val ≤ r ^ (D - 1) :=
                     pow_le_pow_right₀ hr1.le (by omega : k.val ≤ D - 1)
-                  linarith
+                  linarith only [this]
               -- ∑ r^k * ‖a k‖ ≤ (1 + r^(D-1)) * C
               have hsum_le : ∑ x : Fin D, r ^ x.val * ‖a x‖ ≤
                   (1 + r ^ (D - 1)) * C := by
@@ -402,17 +402,20 @@ private lemma integrableOn_polar_norm {D : ℕ} (a : Fin D → ℂ) :
                 Finset.sum_nonneg (fun k _ =>
                   mul_nonneg (pow_nonneg hr_nn k.val) (norm_nonneg _))
               have hfact_nn : 0 ≤ (1 + r ^ (D - 1)) * C :=
-                mul_nonneg (by linarith [pow_nonneg hr_nn (D - 1)]) hC_nn
+                mul_nonneg (by linarith only [hr_nn, pow_nonneg hr_nn (D - 1)]) hC_nn
               have hsq : (∑ x : Fin D, r ^ x.val * ‖a x‖) ^ 2 ≤
                   ((1 + r ^ (D - 1)) * C) ^ 2 :=
-                sq_le_sq' (by linarith) hsum_le
+                sq_le_sq' (by linarith only [hsum_le, hsum_nn]) hsum_le
               -- ((1+a)*b)² = (1+a)²*b²
               -- (1+a)² = 1 + 2a + a² ≤ 2 + 2a² = 2(1+a²)
               -- So ((1+a)*b)² ≤ 2(1+a²)*b²
               -- With a = r^(D-1): (1+r^(D-1))²*C² ≤ 2*(1+(r^(D-1))²)*C² = 2*(1+r^(2*(D-1)))*C²
               have hrd := pow_nonneg hr_nn (D - 1)
               have hsq2 : ((1 + r ^ (D - 1)) * C) ^ 2 ≤
-                  2 * (1 + (r ^ (D - 1)) ^ 2) * C ^ 2 := by nlinarith [sq_nonneg (1 - r ^ (D - 1))]
+                  2 * (1 + (r ^ (D - 1)) ^ 2) * C ^ 2 := by
+                    nlinarith only [
+                      sq_nonneg (1 - r ^ (D - 1))
+                    ]
               -- r^3 * 2 * (1 + (r^(D-1))²) * C² ≤ 4 * (r^3 + r^3*(r^(D-1))²) * C²
               -- r^3 * (r^(D-1))² = r^(2D+1)
               have hpow_eq : r ^ 3 * (r ^ (D - 1)) ^ 2 = r * r ^ (D * 2) := by
@@ -425,9 +428,10 @@ private lemma integrableOn_polar_norm {D : ℕ} (a : Fin D → ℂ) :
                 _ = 2 * C ^ 2 * (r ^ 3 + r ^ 3 * (r ^ (D - 1)) ^ 2) := by ring
                 _ = 2 * C ^ 2 * (r ^ 3 + r * r ^ (D * 2)) := by rw [hpow_eq]
                 _ ≤ r * r ^ (D * 2) * C ^ 2 * 4 + r ^ 3 * C ^ 2 * 4 := by
-                    nlinarith [pow_nonneg hr_nn 3,
-                      mul_nonneg hr_nn (pow_nonneg hr_nn (D * 2)),
-                      sq_nonneg C]
+                    nlinarith only [
+                      hr_nn, pow_nonneg hr_nn 3, mul_nonneg hr_nn (pow_nonneg hr_nn (D * 2)),
+                      sq_nonneg C
+                    ]
 
 /-- IntegrableOn for the polar-coordinate integrand with ρ(polyEvalCircle)². -/
 private lemma integrableOn_polar_rho {D : ℕ} (a : Fin D → ℂ) :
@@ -461,7 +465,7 @@ private lemma integrableOn_polar_rho {D : ℕ} (a : Fin D → ℂ) :
     have hle := rho_le_norm (polyEvalCircle a r (QuotientAddGroup.mk θ))
     have hnn := norm_nonneg (polyEvalCircle a r (QuotientAddGroup.mk θ))
     have hrho_nn : 0 ≤ rho (polyEvalCircle a r (QuotientAddGroup.mk θ)) := abs_nonneg _
-    exact sq_le_sq' (by linarith) hle
+    exact sq_le_sq' (by linarith only [hnn, hrho_nn]) hle
 
 /-! ## Lemma 1.7: Polar-coordinate decomposition of the Fock norm -/
 
@@ -667,7 +671,7 @@ private lemma radial_gaussian_integral (n : ℕ) :
     (n.factorial : ℝ) := by
   -- Use integral_rpow_mul_exp_neg_rpow with p = 2, q = 2*n + 1
   have hp : (0 : ℝ) < 2 := two_pos
-  have hq : (-1 : ℝ) < (2 * (n : ℝ) + 1) := by linarith [Nat.cast_nonneg (α := ℝ) n]
+  have hq : (-1 : ℝ) < (2 * (n : ℝ) + 1) := by linarith only [Nat.cast_nonneg (α := ℝ) n]
   -- First convert ℕ powers to ℝ powers so we can apply integral_rpow_mul_exp_neg_rpow
   have pow_eq : ∀ (r : ℝ), r ∈ Set.Ioi (0 : ℝ) →
       r ^ (2 * n + 1) * Real.exp (-r ^ 2) =

LeanPool/PhaseRetrieval/Constant/Internal/HighFreqBandEstimate.lean

@@ -91,7 +91,7 @@ private lemma rho_sq_lower (α w z : ℂ)
   have h2 : ‖α * w - α * z‖ = ‖w - z‖ := by rw [← mul_sub, norm_mul, hα, one_mul]
   exact nonneg_safe_square _ _ _
     (rho_nonneg' _) (rho_nonneg' _)
-    (norm_nonneg _) (by linarith)
+    (norm_nonneg _) (by linarith only [h1, h2])
 
 /-! ## Interval partition quantities -/
 
@@ -200,7 +200,7 @@ private lemma bias_variance_interval (a b : ℝ) (hab : a < b)
   have h_pw : ∀ t, ‖g t‖ ^ 2 - ‖g t - c‖ ^ 2 =
       2 * @inner ℝ ℂ _ c (g t - c) + ‖c‖ ^ 2 := by
     intro t; have := norm_add_sq_real c (g t - c)
-    simp only [add_sub_cancel] at this; linarith
+    simp only [add_sub_cancel] at this; linarith only [this]
   -- Step 4: Integrate and combine
   have h1 : ∫ t in a..b,
       (‖g t‖ ^ 2 - ‖g t - c‖ ^ 2) =
@@ -234,7 +234,7 @@ private lemma bias_variance_interval (a b : ℝ) (hab : a < b)
       intervalIntegral.integral_const_mul,
       intervalIntegral.integral_const, smul_eq_mul]
   -- Combine
-  linarith [h1, h_split, h_rhs, h_cross]
+  linarith only [h1, h_split, h_rhs, h_cross]
 
 /-- 4.1b: Parseval partition identity.
     On each I_k, ∫|Q|² = |q_k|²·(T/N)/T + ∫|Q−q_k|²
@@ -510,7 +510,7 @@ private lemma deriv_norm_le_circleNormSq {N L : ℕ} (hN : 1 ≤ N)
   apply mul_le_mul_of_nonneg_right _ (sq_nonneg _)
   have hm : (m.val : ℝ) ≤ ↑L - 1 := by
     have := m.isLt; exact_mod_cast (show (m.val : ℤ) ≤ (L : ℤ) - 1 by omega)
-  exact sq_le_sq' (by linarith [Nat.cast_nonneg (α := ℝ) m.val]) hm
+  exact sq_le_sq' (by linarith only [hm, Nat.cast_nonneg (α := ℝ) m.val]) hm
 
 
 /-- Interval integral shift: ∫_a^{a+h} g = ∫_0^h g(·+a). -/
@@ -546,7 +546,7 @@ private lemma hasDerivAt_slowFactor_shift {L : ℕ} (b : Fin L → ℂ) (a x : 
         (hasDerivAt_id x |>.add (hasDerivAt_const x a))
     simp only [add_zero, one_smul] at hd
     exact hd.const_mul _
-  simpa only [slowFactor] using
+  exact
     HasDerivAt.fun_sum (u := Finset.univ) fun m _ => hterm m
 
 /-- Poincaré on each subinterval: shifted to [0, h] and
@@ -586,7 +586,7 @@ private lemma poincare_per_interval {N L : ℕ} (hN : 1 ≤ N)
       ∫ x in (0 : ℝ)..h, ‖f' x‖ ^ 2 := by
     simp only [f']
     exact integral_shift (fun t => ‖Q' t‖ ^ 2) a h
-  have h_ak : iLeft N (k.val + 1) = a + h := by simp only [a, h]; linarith [iLeft_diff N k.val]
+  have h_ak : iLeft N (k.val + 1) = a + h := by simp only [a, h]; linarith only [iLeft_diff N k.val]
   rw [h_ak, h_shift_lhs, h_shift_rhs]
   have hf_deriv :
       ∀ x ∈ Set.Icc 0 h,
@@ -898,7 +898,7 @@ private lemma assembly {N L : ℕ} (hN : 1 ≤ N)
       rw [hPQ]; change _ ≤ (rho (fourier (↑↑N) ↑t * slowFactor b ↑t)) ^ 2
       have := rho_sq_lower (fourier (N : ℤ) (↑t : AddCircle T))
         (slowFactor b (↑t : AddCircle T)) (qAvg b N k) (norm_fourier_apply _ _)
-      linarith
+      linarith only [this]
     -- Integrate the pointwise bound
     have hT_inv_pos : (0 : ℝ) < 1 / T := div_pos one_pos hT_pos
     have hi1 : IntervalIntegrable (fun t => (rho (P (↑t : AddCircle T))) ^ 2)
@@ -944,7 +944,7 @@ private lemma assembly {N L : ℕ} (hN : 1 ≤ N)
     -- Expand 1/T * (1/2 * A - B) = 1/2 * (1/T * A) - 1/T * B
     have h_expand : 1 / T * (1 / 2 * A - B) = 1 / 2 * (1 / T * A) - 1 / T * B := by ring
     rw [h_expand] at h_mul
-    linarith
+    linarith only [h_mul, h_frozen]
   -- Sum over k
   have h_sum : (1 / T) • ∑ k : Fin N,
       ∫ t in iLeft N k.val..iLeft N (k.val + 1),
@@ -970,11 +970,11 @@ private lemma assembly {N L : ℕ} (hN : 1 ≤ N)
         rw [← Finset.mul_sum]
         have : (↑N : ℝ) ≠ 0 := ne_of_gt hN_pos; field_simp
       · unfold totalDelta; rw [Finset.mul_sum]
-    linarith
+    linarith only [h_sum_ge, h_rhs_eq]
   -- Apply parseval_partition
   have h_parseval := parseval_partition hN b
   -- h_parseval: C = (1/N)∑|q_k|² + δ, so (1/N)∑|q_k|² = C - δ
-  linarith
+  linarith only [h_sum, h_parseval]
 
 /-! ## Auxiliary -/
 
@@ -1000,7 +1000,7 @@ The hypothesis `1343 * L^2 ≤ N^2` implies `136π²(L-1)² ≤ 136π²L² ≤ 1
 private lemma pi_sq_bound : 136 * Real.pi ^ 2 < 1343 := by
   have hpi : Real.pi < 3.141593 := Real.pi_lt_d6
   have hpi_pos : (0 : ℝ) < Real.pi := Real.pi_pos
-  nlinarith [sq_nonneg (3.141593 - Real.pi)]
+  nlinarith only [hpi, hpi_pos, sq_nonneg (3.141593 - Real.pi)]
 
 private lemma rho_integral_lower_bound {N L : ℕ}
     (hN : 1 ≤ N) (hL : 1 ≤ L)
@@ -1028,7 +1028,7 @@ private lemma rho_integral_lower_bound {N L : ℕ}
   -- Since (L-1)² ≤ L² and 136π² < 1343: 136π²(L-1)² ≤ 1343L² ≤ N²
   have hpi2 := pi_sq_bound
   have hL_real : (1 : ℝ) ≤ (↑L : ℝ) := Nat.one_le_cast.mpr hL
-  have hL_cast : (0 : ℝ) ≤ (↑L : ℝ) - 1 := by linarith
+  have hL_cast : (0 : ℝ) ≤ (↑L : ℝ) - 1 := by linarith only [hL_real]
   have hN_pos : (0 : ℝ) < (↑N : ℝ) := Nat.cast_pos.mpr (by omega)
   have hN2_pos : (0 : ℝ) < (↑N : ℝ) ^ 2 := by positivity
   have hNL_cast : (1343 : ℝ) * (↑L : ℝ) ^ 2 ≤ (↑N : ℝ) ^ 2 := by
@@ -1038,17 +1038,17 @@ private lemma rho_integral_lower_bound {N L : ℕ}
   have h_rate_bound : 34 * (4 * Real.pi ^ 2 * (↑L - 1) ^ 2) ≤ (↑N : ℝ) ^ 2 := by
     have hLm1_sq : ((↑L : ℝ) - 1) ^ 2 ≤ (↑L : ℝ) ^ 2 := by apply sq_le_sq' <;> linarith
     -- 34 * 4π² * (L-1)² ≤ 136π² * L² < 1343 * L² ≤ N²
-    nlinarith [sq_nonneg Real.pi, sq_nonneg (↑L : ℝ)]
+    nlinarith only [hpi2, hL_real, hNL_cast, sq_nonneg Real.pi, sq_nonneg (↑L : ℝ)]
   -- r·C ≤ C/34 where r = 4π²(L-1)²/N²
   have h_key : 4 * Real.pi ^ 2 * (↑L - 1) ^ 2 / ↑N ^ 2 * C ≤ C / 34 := by
     have h1 : 4 * Real.pi ^ 2 * (↑L - 1) ^ 2 / ↑N ^ 2 ≤ 1 / 34 := by
       rw [div_le_div_iff₀ hN2_pos (by norm_num : (0:ℝ) < 34)]
-      linarith
+      linarith only [h_rate_bound]
     calc 4 * Real.pi ^ 2 * (↑L - 1) ^ 2 / ↑N ^ 2 * C
-        ≤ (1 / 34) * C := by nlinarith
+        ≤ (1 / 34) * C := by nlinarith only [h_nn, h1]
       _ = C / 34 := by ring
   -- Combine: ∫ρ² ≥ C/16 - (17/16)δ ≥ C/16 - (17/16)·(C/34) = C/16 - C/32 = C/32
-  linarith
+  linarith only [h_asm, h_poi, h_key]
 
 /-! ## Main theorem -/
 
@@ -1070,6 +1070,6 @@ theorem high_freq_band_estimate {N L : ℕ}
   have h_eq := circleNormSq_P_eq_Q b P hP
   have h_lb :=
     rho_integral_lower_bound hN hL hNL b P hP
-  linarith
+  linarith only [h_eq, h_lb]
 
 end FockSPR