From 646d9323ad8fed2322617c34904cc9e0cd324c7c Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Mon, 2 Nov 2026 14:15:59 +0000 Subject: [PATCH] Optimize EhrhartVolumeInequality arithmetic and cancellation proofs --- .../EhrhartVolumeInequality/Convergence.lean | 4 +-- .../EhrhartVolumeInequality/Convexity.lean | 10 +++---- .../EhrhartVolumeInequality/Foundations.lean | 30 +++++++++---------- .../FourierAnalysis.lean | 21 ++++++------- .../Regularization.lean | 26 ++++++++-------- .../EhrhartVolumeInequality/Resolvent.lean | 10 +++---- .../EhrhartVolumeInequality/Variation.lean | 17 +++++------ 7 files changed, 58 insertions(+), 60 deletions(-) diff --git a/LeanPool/EhrhartVolumeInequality/Convergence.lean b/LeanPool/EhrhartVolumeInequality/Convergence.lean index 4ff2aa3af4..c053d3dd9e 100644 --- a/LeanPool/EhrhartVolumeInequality/Convergence.lean +++ b/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)ᶜ diff --git a/LeanPool/EhrhartVolumeInequality/Convexity.lean b/LeanPool/EhrhartVolumeInequality/Convexity.lean index abffb6c06c..c89c1dc6fd 100644 --- a/LeanPool/EhrhartVolumeInequality/Convexity.lean +++ b/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 diff --git a/LeanPool/EhrhartVolumeInequality/Foundations.lean b/LeanPool/EhrhartVolumeInequality/Foundations.lean index 88d5f85623..0a3bc7bf08 100644 --- a/LeanPool/EhrhartVolumeInequality/Foundations.lean +++ b/LeanPool/EhrhartVolumeInequality/Foundations.lean @@ -1880,7 +1880,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) @@ -2246,11 +2246,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 → ℝ} @@ -2860,7 +2860,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 @@ -3073,7 +3073,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 @@ -3204,7 +3204,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 @@ -4178,7 +4178,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 : @@ -5581,7 +5581,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 := @@ -5606,7 +5606,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 @@ -5637,7 +5637,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) @@ -5975,7 +5975,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 @@ -6038,7 +6038,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) : @@ -6998,7 +6998,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 @@ -8195,13 +8195,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} diff --git a/LeanPool/EhrhartVolumeInequality/FourierAnalysis.lean b/LeanPool/EhrhartVolumeInequality/FourierAnalysis.lean index 6c589da55b..91279d7230 100644 --- a/LeanPool/EhrhartVolumeInequality/FourierAnalysis.lean +++ b/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 /-! @@ -246,7 +247,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} @@ -292,7 +293,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 @@ -366,7 +367,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 @@ -911,7 +912,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 @@ -952,7 +953,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)) @@ -4347,7 +4348,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 → ℝ) : @@ -5103,7 +5104,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 @@ -7855,7 +7856,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 @@ -9095,7 +9096,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 → ℝ} diff --git a/LeanPool/EhrhartVolumeInequality/Regularization.lean b/LeanPool/EhrhartVolumeInequality/Regularization.lean index aff4a4aea6..44290e742e 100644 --- a/LeanPool/EhrhartVolumeInequality/Regularization.lean +++ b/LeanPool/EhrhartVolumeInequality/Regularization.lean @@ -10,12 +10,12 @@ 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 all Mathlib.MeasureTheory.Function.LpSpace.Basic /-! # Ehrhart volume inequality: Regularization @@ -411,7 +411,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 := @@ -420,9 +420,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 @@ -1724,7 +1722,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⟩⟩, ?_⟩ @@ -1827,13 +1825,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) @@ -1922,13 +1920,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 @@ -2145,7 +2143,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 @@ -2158,7 +2156,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, @@ -3931,7 +3929,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 @@ -8982,7 +8980,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 diff --git a/LeanPool/EhrhartVolumeInequality/Resolvent.lean b/LeanPool/EhrhartVolumeInequality/Resolvent.lean index 3697127fea..0bc2424ac0 100644 --- a/LeanPool/EhrhartVolumeInequality/Resolvent.lean +++ b/LeanPool/EhrhartVolumeInequality/Resolvent.lean @@ -2253,7 +2253,7 @@ theorem complex_norm_sub_sq_le_two_mul_add have hsub := norm_sub_le z w have hsq : ‖z - w‖ ^ 2 ≤ (‖z‖ + ‖w‖) ^ 2 := by exact (sq_le_sq₀ (norm_nonneg _) (add_nonneg (norm_nonneg _) (norm_nonneg _))).mpr hsub - nlinarith [sq_nonneg (‖z‖ - ‖w‖)] + linarith [sq_nonneg (‖z‖ - ‖w‖)] private theorem complexEuclidean_antisymmetric_energy_le_two_norm_sq {n : ℕ} @@ -2284,7 +2284,7 @@ private theorem complexEuclidean_antisymmetric_energy_le_two_norm_sq rw [Finset.sum_comm] simp only [mul_add, Finset.sum_add_distrib, ← Finset.mul_sum] at hsum rw [hswap] at hsum - nlinarith + linarith private theorem sourceTorusBarPartial_cutoffPhysicalField_antisymmetric {n : ℕ} @@ -2779,7 +2779,7 @@ private theorem angularDolbeaultGraph_compact_barPartial_green_of_fundamentalCel (smul_eq_zero.mp hz).resolve_left (logarithmicCoverJacobianFactor_pos n).ne' rw [integral_const_mul] at hinner - linear_combination hinner + exact (eq_neg_of_add_eq_zero_left hinner).trans (neg_mul _ _).symm private theorem angularDolbeaultGraph_compact_barPartial_green {n : ℕ} {a : LogTorus n → ℝ} (ha : Continuous a) @@ -4469,7 +4469,7 @@ private theorem normalizedCoverMollificationL2_tendsto exact normalizedCoverMollificationL2_dist_le k u v _ < ε := by rw [dist_comm v u] - nlinarith [hN k hk] + linarith [hN k hk] private theorem normalizedCoverMollification_global_L2_tendsto {n : ℕ} {h : LogSpace n → ℂ} @@ -5374,7 +5374,7 @@ private theorem complexHilbert_norm_le_of_mem_closure_inner_bound exact hB · have hfpos : 0 < ‖f‖ := lt_of_le_of_ne (norm_nonneg _) (Ne.symm hfzero) - nlinarith + nlinarith only [hsq, hfpos] end RadialPhysicalResolventDefectReduction diff --git a/LeanPool/EhrhartVolumeInequality/Variation.lean b/LeanPool/EhrhartVolumeInequality/Variation.lean index 0d0f664123..b77d7d0e41 100644 --- a/LeanPool/EhrhartVolumeInequality/Variation.lean +++ b/LeanPool/EhrhartVolumeInequality/Variation.lean @@ -417,7 +417,7 @@ private theorem finiteEnergyTargetGeodesic_differenceQuotient_error t * v q ≤ |t| * (|v p - v q| + |t|) := by have habssq : |t| ^ 2 = t ^ 2 := sq_abs t - nlinarith + linarith have hfrac : (finiteEnergyTargetGeodesic F v t x - F.potential x) / t + v q = @@ -502,7 +502,7 @@ theorem abs_exp_sub_one_le_mul_exp_abs (z : ℝ) : simp only [neg_add_cancel, Real.exp_zero] rw [hinverse] at hmul rw [abs_of_nonneg hfirst, abs_of_nonneg hz] - nlinarith + linarith · have hz' : z ≤ 0 := le_of_not_ge hz have he : 0 < Real.exp (-z) := Real.exp_pos (-z) have hfirst : Real.exp z - 1 ≤ 0 := by @@ -515,7 +515,7 @@ theorem abs_exp_sub_one_le_mul_exp_abs (z : ℝ) : rw [abs_of_nonpos hfirst, abs_of_nonpos hz'] have hnonneg : 0 ≤ -z := neg_nonneg.mpr hz' have hscaled := mul_le_mul_of_nonneg_left hunit hnonneg - nlinarith + linarith private def finiteEnergyTargetDensityDifferenceQuotient {n : ℕ} {K : CenteredBody n} @@ -1496,7 +1496,7 @@ private theorem integrable_monomialWeight_finiteEnergySource_of_mem_interior ← Real.exp_add] apply Real.exp_le_exp.mpr have h := hcoerc x - nlinarith + linarith only [mul_le_mul_of_nonneg_left h hk.le] private theorem monomialWeight_momentNormalizedPotential_eq {n : ℕ} {K : CenteredBody n} @@ -4197,7 +4197,7 @@ private theorem momentZeroMonomialNorm_le_partition unfold monomialWeight pairing simp only [Pi.zero_apply, zero_mul, Finset.sum_const_zero, zero_sub] apply Real.exp_le_exp.mpr - nlinarith [F.nonnegative x] + nlinarith only [hkone, F.nonnegative x] have hshift : monomialNormSquared k (0 : Space n) (momentNormalizedPotential F) = @@ -4264,11 +4264,10 @@ private theorem momentJointGlobalLowerBound_le_zeroMonomial Real.log (finiteEnergySourcePartition F) ≤ |Real.log (finiteEnergySourcePartition F)| := le_abs_self _ _ ≤ (k : ℝ) * |Real.log (finiteEnergySourcePartition F)| := by - nlinarith [abs_nonneg - (Real.log (finiteEnergySourcePartition F))] + exact le_mul_of_one_le_left (abs_nonneg _) hkone unfold momentJointGlobalLowerBound apply (le_div_iff₀ hkreal).mpr - nlinarith + linarith private theorem inv_momentZeroMonomialNorm_le_diagonalKernel {n k : ℕ} (K : CenteredBody n) (hk : 0 < k) @@ -7372,7 +7371,7 @@ private theorem weighted_complex_coordinate_integration_by_parts_volume calc _ = ∫ z : E, (fderiv ℝ F z) v * W z ∂μ := hright.symm _ = -(∫ z : E, F z * (fderiv ℝ W z) v ∂μ) := by - linear_combination hip + exact ((congrArg Neg.neg hip).trans (neg_neg _)).symm _ = _ := congrArg Neg.neg hleft private theorem weighted_complex_coordinate_integration_by_parts