Optimize EhrhartVolumeInequality arithmetic and cancellation proofs

LeanPool/EhrhartVolumeInequality/Convergence.lean

@@ -284,7 +284,7 @@ private theorem momentNormalized_off_phase_setIntegral_le_exp_mul_base
       apply Real.exp_le_exp.mpr
       have h := hphase x hx
       unfold phase at h
-      nlinarith
+      linarith only [mul_le_mul_of_nonneg_left h (sub_nonneg.mpr hk)]
     _ ≤ ∫ x : Space n,
         Real.exp ((k - 1) * M) *
           monomialWeight 1 u (momentNormalizedPotential F) x
@@ -337,7 +337,7 @@ private theorem exists_momentNormalized_phase_gap_outside_ball
       simpa only [ge_iff_le, mul_comm] using (div_le_iff₀ hδ).mp hle
     have hscale := mul_lt_mul_of_pos_left hxnorm hδ
     have hcoerce := hcoercive x
-    nlinarith
+    linarith
   let t : Set (Space n) :=
     Metric.closedBall (0 : Space n) R ∩
       (Metric.ball x₀ r)ᶜ

LeanPool/EhrhartVolumeInequality/Convexity.lean

@@ -139,7 +139,7 @@ private theorem momentWeakHolomorphicJointMollifierLowerBound_le_mollification
                 dsimp [C,
                   momentWeakHolomorphicJointMollifierLowerBound,
                   momentWeakJointCoverFiniteMinorant]
-                nlinarith [BodyScale.canonicalScale_pos K]
+                nlinarith only [BodyScale.canonicalScale_pos K, hmin]
           _ ≤ momentWeakJointCoverUpperEnvelope
               K F htransport p (q - y) :=
             momentWeakJointCoverFiniteMinorant_le_upperEnvelope
@@ -860,7 +860,7 @@ private theorem momentTorusTruncatedJetOrderDensity_le_diagonal_mul_cutoff
       apply Finset.sum_le_sum
       intro i _
       apply mul_le_mul_of_nonneg_right
-      · exact_mod_cast
+      · exact Nat.cast_le.mpr <|
           momentTruncatedJetOrder_le
             K hk F htransport p N i
       · exact Complex.normSq_nonneg _
@@ -2721,7 +2721,7 @@ private theorem momentWeakHolomorphicStrictJointTorusWeight_le_support_add
     simp only [sourceJointTimeEmbedding, sourceTorusCoverPoint,
       MatrixTorusBochnerBridge.matrixSourceCoverPotential_logarithmicPoint]
   rw [href]
-  nlinarith
+  linarith
 
 private theorem momentWeakHolomorphicStrictJoint_centered_mem_resolventDefect_range_closure
     {n : ℕ} (K : CenteredBody n)
@@ -5418,7 +5418,7 @@ private theorem convexOn_momentWeakHolomorphicEnvelopeLogPartition_Ioi_of_strict
     · have ha0 : a = 0 := hazero.symm
       have hb1 : b = 1 := by linarith
       simp only [ha0, zero_mul, hb1, one_mul, zero_add, hy]
-    · nlinarith [mul_pos hapos hx, mul_nonneg hb hy.le]
+    · linarith [mul_pos hapos hx, mul_nonneg hb hy.le]
   have hmid :=
     tendsto_momentWeakHolomorphicStrictJointLogPartition
       K F htransport p ε hε hε₀ hε₁ hm
@@ -6585,7 +6585,7 @@ private theorem nonnegative_le_exp_mul_one_sub_exp_neg
     simp only [add_neg_cancel, Real.exp_zero]
   rw [hcancel] at hexp
   have hfactor : u * Real.exp (-u) ≤ 1 - Real.exp (-u) := by
-    nlinarith
+    linarith
   calc
     u = u * 1 := by ring
     _ ≤ u * Real.exp (C - u) := by

LeanPool/EhrhartVolumeInequality/Foundations.lean

@@ -1882,7 +1882,7 @@ private theorem exists_smooth_convex_potential_uniformly_close {n : ℕ}
     dsimp [δ]
     rw [← mul_div_assoc]
     apply (div_lt_iff₀ (by linarith : 0 < L + 1)).mpr
-    nlinarith
+    linarith
   rw [Real.dist_eq] at hdist
   exact lt_of_le_of_lt hdist (by simpa only [ρ, L] using hsmall)
 
@@ -2248,11 +2248,11 @@ private theorem exists_phase_maximizer {n : ℕ}
     have hrange : (C - phase u φ 0) / δ ≤ R :=
       le_max_right _ _
     have hscale := (div_le_iff₀ hδ).mp hrange
-    nlinarith
+    linarith
   have hnorm := SupportFunction.norm_le_sum_abs x
   have hscale := mul_lt_mul_of_pos_left hxnorm hδ
   have hcoerce := hcoercive x
-  nlinarith [mul_le_mul_of_nonneg_left hnorm hδ.le]
+  linarith [mul_le_mul_of_nonneg_left hnorm hδ.le]
 
 private theorem legendreTransform_eq_of_maximizer {n : ℕ}
     {u : Space n} {φ : Space n → ℝ}
@@ -2862,7 +2862,7 @@ private theorem convexOn_logarithmicPotential {ι : Type*} [Fintype ι]
       · have hvar :=
           exponentialMoment_sq_le_partition_mul_second
             w order hw t
-        nlinarith
+        linarith
       · exact sq_nonneg _
     · exact hk.le
 
@@ -3075,7 +3075,7 @@ private theorem tendsto_normalized_jetLayercake_profile {n : ℕ}
   have hkne : (k : ℝ) ≠ 0 := by exact_mod_cast Nat.ne_of_gt hkpos
   have hdne :
       (BergmanMonomials.bergmanDimension K k : ℝ) ≠ 0 := by
-    exact_mod_cast
+    exact Nat.cast_ne_zero.mpr <|
       (BergmanMonomials.bergmanDimension_pos K hkpos).ne'
   rw [pow_succ]
   field_simp
@@ -3206,7 +3206,7 @@ private theorem convex_centeredSimplex (n : ℕ) :
     change -(1 : ℝ) ≤ a * x i + b * y i
     have hax : 0 ≤ a * (x i + 1) := mul_nonneg ha (by linarith [hx'.1 i])
     have hby : 0 ≤ b * (y i + 1) := mul_nonneg hb (by linarith [hy'.1 i])
-    nlinarith
+    linarith
   · change (∑ i, (a * x i + b * y i)) ≤ 1
     rw [Finset.sum_add_distrib, ← Finset.mul_sum, ← Finset.mul_sum]
     calc
@@ -4180,7 +4180,7 @@ private theorem roundedLatticeExponent_coordinate_error {n : ℕ}
   constructor
   · apply (div_le_iff₀ hkreal).mpr
     change (⌊(k : ℝ) * u i⌋ : ℝ) ≤ u i * (k : ℝ)
-    nlinarith
+    linarith
   · change u i - (⌊(k : ℝ) * u i⌋ : ℝ) / (k : ℝ) <
       1 / (k : ℝ)
     have heq :
@@ -5583,7 +5583,7 @@ private theorem exists_uniform_inner_supportBall {n : ℕ}
     have hznorm : ‖z‖ < ρ := by
       rw [hzform, norm_smul, Real.norm_eq_abs]
       norm_num
-      nlinarith
+      linarith
     have hzball : z ∈ Metric.ball (0 : Space n) r := by
       simpa only [Metric.mem_ball, dist_eq_norm, sub_zero] using hznorm.trans hρr
     have hzK : z ∈ K.carrier :=
@@ -5608,7 +5608,7 @@ private theorem exists_uniform_inner_supportBall {n : ℕ}
     have hznorm : ‖z‖ < ρ := by
       rw [hzform, norm_smul, Real.norm_eq_abs]
       norm_num
-      nlinarith
+      linarith
     have hzbound :
         |SupportFunction.pairing z x| ≤
           (d / 4) * ‖x‖ := by
@@ -5639,7 +5639,7 @@ private theorem exists_uniform_inner_supportBall {n : ℕ}
       SupportFunction.pairing_smul_left]
     have hzlow := (abs_le.mp hzbound).1
     norm_num
-    nlinarith [mul_nonneg hd.le (norm_nonneg x)]
+    linarith [mul_nonneg hd.le (norm_nonneg x)]
 
 private theorem realVolume_uniformInnerBall {n : ℕ}
     (c : Space n)
@@ -5977,7 +5977,7 @@ private theorem exists_minimumNormalizedSource_strong_moser_trudinger
     have hscaled := mul_le_mul_of_nonneg_left hc ht.le
     rw [← Real.exp_add]
     apply Real.exp_le_exp.mpr
-    nlinarith
+    linarith
   have hbound :
       minimumNormalizedSourcePartition D ≤
         Real.exp (t * B * minimumNormalizedSourceBodyEnergy D) * I := by
@@ -6040,7 +6040,7 @@ private theorem exists_sourceMomentBerman_superlevel_uniformEnergy
   intro D hL
   have hfunctional := minimumNormalizedSourceBermanFunctional_eq D
   unfold minimumNormalizedSourceBermanFunctional at hfunctional
-  nlinarith [hA D]
+  linarith [hA D]
 
 private theorem exists_sourceMomentBerman_maximizingSequence_uniformEnergy
     {n : ℕ} (K : CenteredBody n) :
@@ -7000,7 +7000,7 @@ private theorem exists_smooth_sourceSupportClipping_recovery {n : ℕ}
     dsimp [δ]
     rw [← mul_div_assoc]
     apply (div_lt_iff₀ (by linarith : 0 < L + 1)).mpr
-    nlinarith
+    linarith
   have hclose : ∀ x : Space n,
       |D.potential x - sourceSupportClipping F R x| < ε := by
     intro x
@@ -8197,13 +8197,13 @@ private theorem exists_finiteEnergyTargetGeodesic_minimum
           (finiteEnergyTargetGeodesic F v t 0 + C) / δ ≤ R :=
         le_max_right 0 _
       have h := (div_le_iff₀ hδ).mp hmax
-      nlinarith
+      linarith
     have hxcoerc := hcoerc x
     have hzeroMin := hmin hzero
     change
       finiteEnergyTargetGeodesic F v t m ≤
         finiteEnergyTargetGeodesic F v t 0 at hzeroMin
-    nlinarith [mul_lt_mul_of_pos_left hnorm hδ]
+    linarith [mul_lt_mul_of_pos_left hnorm hδ]
 
 private def finiteEnergyTargetGeodesicMinimumPoint
     {n : ℕ} {K : CenteredBody n}

LeanPool/EhrhartVolumeInequality/FourierAnalysis.lean

@@ -9,7 +9,8 @@ module
 public import LeanPool.EhrhartVolumeInequality.Variation
 public import Mathlib.MeasureTheory.Function.LpSpace.Basic
 import all LeanPool.EhrhartVolumeInequality.Variation
-import Mathlib.Analysis.Matrix.Order
+import Mathlib.Algebra.Order.Star.Real
+import Mathlib.Analysis.CStarAlgebra.Classes
 import Mathlib.Analysis.SpecialFunctions.PolarCoord
 import Mathlib.Geometry.Manifold.PartitionOfUnity
 
@@ -247,7 +248,7 @@ private theorem exists_momentNormalizedPhaseMaximizer
   have hbound := hcoerc x
   change phase u φ x ≤ phase u φ 0
   change phase u φ x ≤ C - δ * ‖x‖ at hbound
-  nlinarith
+  linarith
 
 private theorem momentNormalized_monomialIntegral_le_exp_mul_base
     {n : ℕ} {K : CenteredBody n}
@@ -293,7 +294,7 @@ private theorem momentNormalized_monomialIntegral_le_exp_mul_base
             apply Real.exp_le_exp.mpr
             have hx := hM x
             unfold phase at hx
-            nlinarith
+            linarith only [mul_le_mul_of_nonneg_left hx (sub_nonneg.mpr hk)]
     _ = Real.exp ((k - 1) * M) *
         (∫ x : Space n,
           monomialWeight 1 u
@@ -367,7 +368,7 @@ private theorem momentNormalized_log_monomialIntegral_div_le
                   (monomialIntegral 1 u
                     (momentNormalizedPotential F))| :=
               abs_nonneg _
-            nlinarith
+            exact le_mul_of_one_le_left hnonneg hk
     _ = (|M| +
             |Real.log
               (monomialIntegral 1 u
@@ -912,7 +913,7 @@ private theorem eventually_momentNormalized_moving_phase_le_max_add
   have hboundary : C - d * R ≤ M := by
     have hratio : (C - M) / d ≤ R := le_max_right _ _
     have hmul := (div_le_iff₀ hd).mp hratio
-    nlinarith
+    linarith
   have hnorm :
       Tendsto (fun k : ℕ => ‖u k - u₀‖)
         atTop (𝓝 (0 : ℝ)) := by
@@ -953,7 +954,7 @@ private theorem eventually_momentNormalized_moving_phase_le_max_add
     have hdecay : C - d * ‖z‖ ≤ M := by
       calc
         C - d * ‖z‖ ≤ C - d * R := by
-          nlinarith
+          exact sub_le_sub_left (mul_le_mul_of_nonneg_left hz'.le hd.le) C
         _ ≤ M := hboundary
     exact (hk z).trans
       (hdecay.trans (by dsimp [M]; linarith))
@@ -4348,7 +4349,7 @@ namespace ComplexMatrixWeightedHilbert
 
 open Set Function MeasureTheory Filter Matrix
 open scoped BigOperators ContDiff Convolution ENNReal InnerProductSpace
-  MatrixOrder Matrix.Norms.L2Operator Topology
+  Topology
 
 private def sourceMatrixHessian {n : ℕ}
     (φ : Space n → ℝ) :
@@ -5104,7 +5105,7 @@ private theorem weighted_complex_bochner_coordinate_identity_compact_right
         barPartialCoordinate
           (fun w => weightedHolomorphicDerivative a F i w) z j *
             conj (G z) ∂μ) := by
-    linear_combination hfirst
+    exact ((congrArg Neg.neg hfirst).trans (neg_neg _)).symm
   have hsecond :=
     weighted_holomorphic_hermitian_integration_by_parts_compact_right
       haone hFbar hgone hGcompact i
@@ -7856,7 +7857,7 @@ private theorem angularWeakDolbeaultResolvent_form_adjoint {n : ℕ}
       (WithLp.fst (v : angularDolbeaultGraphAmbient a)) := by
   rw [inner_sub_left]
   have h := angularWeakDolbeaultResolvent_moment_components a f v
-  linear_combination h
+  exact eq_sub_of_add_eq' h
 
 end WeightedTorusDolbeault
 
@@ -9096,7 +9097,7 @@ private theorem integrable_angularTorusFormExteriorDerivativeDensity
     sourceTorusFormFullDerivativeDensity W p -
       sourceTorusFormMixedDerivativeDensity W p =
         sourceTorusFormExteriorDerivativeDensity W p
-  linear_combination -hp
+  exact sub_eq_iff_eq_add.mpr hp.symm
 
 private theorem angularTorus_weighted_complex_dolbeault_form_bochner_identity
     {n : ℕ} {a : LogTorus n → ℝ}

LeanPool/EhrhartVolumeInequality/Regularization.lean

@@ -10,13 +10,13 @@ public import LeanPool.EhrhartVolumeInequality.FourierAnalysis
 public import Mathlib.Analysis.Calculus.Deriv.Basic
 public import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
 import all LeanPool.EhrhartVolumeInequality.FourierAnalysis
-import all Mathlib.MeasureTheory.Function.LpSpace.Basic
 import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
 import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
 import Mathlib.Analysis.Calculus.DerivativeTest
 import Mathlib.Analysis.Convex.Integral
 import Mathlib.Analysis.Matrix.Order
 import Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
+import all Mathlib.MeasureTheory.Function.LpSpace.Basic
 
 /-!
 # Ehrhart volume inequality: Regularization
@@ -412,7 +412,7 @@ private theorem angularWeakScalarResolventCLM_fixed_iff_graph_zero
             angularDolbeaultGraphAmbient a))
           (WithLp.snd (angularWeakDolbeaultResolvent a f :
             angularDolbeaultGraphAmbient a)) = 0 := by
-      linear_combination hvar
+      exact add_eq_left.mp hvar
     have hgradient :
         WithLp.snd (angularWeakDolbeaultResolvent a f :
           angularDolbeaultGraphAmbient a) = 0 :=
@@ -421,9 +421,7 @@ private theorem angularWeakScalarResolventCLM_fixed_iff_graph_zero
         (angularWeakDolbeaultResolvent a f :
           angularDolbeaultGraphAmbient a) =
             WithLp.toLp 2 (f, (0 : angularWeightedFormL2 a)) := by
-      apply (WithLp.prodContinuousLinearEquiv 2 ℂ
-        (angularWeightedScalarL2 a)
-        (angularWeightedFormL2 a)).injective
+      apply WithLp.ofLp_injective 2
       exact Prod.ext hscalar hgradient
     rw [← hpair]
     exact (angularWeakDolbeaultResolvent a f).property
@@ -1725,7 +1723,7 @@ private theorem exists_sourceJointCoverCircle_uniform_bounds
   have hzmem : z ∈ Metric.closedBall q S := by
     apply Metric.mem_closedBall.mpr
     dsimp [S]
-    nlinarith [abs_nonneg R, norm_nonneg v,
+    linarith [abs_nonneg R, norm_nonneg v,
       mul_nonneg (abs_nonneg R) (norm_nonneg v)]
   refine ⟨⟨hL ⟨_, hzmem, rfl⟩,
     hC ⟨_, hzmem, rfl⟩⟩, ?_⟩
@@ -1828,13 +1826,13 @@ private theorem sourceJointCover_complex_line_submean_of_convergent_finite_appro
     have hmprod :
         (2 * Real.pi) * F (i m) (q m) ≤
           ∫ θ in 0..2 * Real.pi, u (γ m θ) := by
-      nlinarith [(le_div_iff₀ Real.two_pi_pos).mp hmdiv]
+      linarith [(le_div_iff₀ Real.two_pi_pos).mp hmdiv]
     rw [← intervalIntegral.integral_of_le Real.two_pi_pos.le,
       intervalIntegral.integral_sub
         (hangleint m) intervalIntegrable_const]
     simp only [intervalIntegral.integral_const,
       sub_zero, smul_eq_mul]
-    nlinarith
+    linarith
   have hshiftint (m : ℕ) :
       Integrable
         (fun θ : ℝ => u (γ m θ) - L)
@@ -1923,13 +1921,13 @@ private theorem sourceJointCover_complex_line_submean_of_convergent_finite_appro
   have hprod :
       (2 * Real.pi) * u q₀ ≤
         ∫ θ in 0..2 * Real.pi, u (γ₀ θ) := by
-    nlinarith
+    linarith
   have hdiv :
       u q₀ ≤
         (∫ θ in 0..2 * Real.pi, u (γ₀ θ)) /
           (2 * Real.pi) := by
     apply (le_div_iff₀ Real.two_pi_pos).mpr
-    nlinarith
+    linarith
   simpa only [mul_comm, mul_inv_rev, ge_iff_le, div_eq_mul_inv] using hdiv
 
 private theorem sourceJointCover_upperRegularization_family_complex_line_submean_all_radius
@@ -2146,7 +2144,7 @@ private theorem support_sourceJointTrueRadialBump_subset_closedBall
     have hprod : 0 ≤ (((k + 1 : ℕ) : ℝ) * ‖q.1 i‖) :=
       mul_nonneg hk.le (norm_nonneg _)
     apply (le_div_iff₀ hk).mpr
-    nlinarith
+    nlinarith only [hsq]
   have haux :
       ‖q.2‖ ≤ 1 / ((k + 1 : ℕ) : ℝ) := by
     have hs := sourceJointRadialNormSq_auxiliary_le q
@@ -2159,7 +2157,7 @@ private theorem support_sourceJointTrueRadialBump_subset_closedBall
     have hprod : 0 ≤ (((k + 1 : ℕ) : ℝ) * ‖q.2‖) :=
       mul_nonneg hk.le (norm_nonneg _)
     apply (le_div_iff₀ hk).mpr
-    nlinarith
+    nlinarith only [hsq]
   rw [Metric.mem_closedBall, dist_zero_right, Prod.norm_def,
     max_le_iff]
   exact ⟨(pi_norm_le_iff_of_nonneg (by positivity)).mpr hcoord,
@@ -3932,7 +3930,7 @@ private theorem hasDerivAt_momentStrictRadialCoordinateDerivative
     simp only [neg_add_cancel, Real.exp_zero]
   refine h.congr_deriv ?_
   congr 1
-  nlinarith [he]
+  linarith [he]
 
 private theorem momentStrictRadialCoordinateSecond_pos (y : ℝ) :
     0 < momentStrictRadialCoordinateSecond y := by
@@ -8983,7 +8981,7 @@ private theorem barPartial_complexReal_convolution_eq_of_compact_green
       (2 : ℂ) *
         (∫ t : E, G j t * (κ (x - t) : ℂ) ∂μ) := by
     rw [integral_neg] at hnegative
-    linear_combination -hnegative
+    exact neg_injective (hnegative.trans (neg_mul _ _))
   have hderiv := hκcompact.hasFDerivAt_convolution_right
     L hg hκ x
   have hint : Integrable