diff --git a/LeanAPAP.lean b/LeanAPAP.lean
index 972b636df7..aa88360b51 100644
--- a/LeanAPAP.lean
+++ b/LeanAPAP.lean
@@ -1,5 +1,6 @@
 import LeanAPAP.Extras.BSG
-import LeanAPAP.FiniteField.Basic
+import LeanAPAP.FiniteField
+import LeanAPAP.Integer
 import LeanAPAP.Mathlib.Algebra.Group.AddChar
 import LeanAPAP.Mathlib.Algebra.Group.Basic
 import LeanAPAP.Mathlib.Algebra.Order.BigOperators.Group.Finset
@@ -45,7 +46,6 @@ import LeanAPAP.Prereqs.Convolution.Norm
 import LeanAPAP.Prereqs.Convolution.Order
 import LeanAPAP.Prereqs.Convolution.ThreeAP
 import LeanAPAP.Prereqs.Convolution.WithConv
-import LeanAPAP.Prereqs.Curlog
 import LeanAPAP.Prereqs.Energy
 import LeanAPAP.Prereqs.Expect.Basic
 import LeanAPAP.Prereqs.Expect.Complex
diff --git a/LeanAPAP/Prereqs/Chang.lean b/LeanAPAP/Prereqs/Chang.lean
index f1dd32cdcd..c3fdfadb8d 100644
--- a/LeanAPAP/Prereqs/Chang.lean
+++ b/LeanAPAP/Prereqs/Chang.lean
@@ -1,6 +1,6 @@
 import Mathlib.Algebra.Order.Chebyshev
 import Mathlib.Analysis.MeanInequalities
-import LeanAPAP.Prereqs.Curlog
+import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.Real
 import LeanAPAP.Prereqs.Energy
 import LeanAPAP.Prereqs.LargeSpec
 import LeanAPAP.Prereqs.Rudin
@@ -12,9 +12,31 @@ import LeanAPAP.Prereqs.Rudin
 open Finset Fintype Function Real MeasureTheory
 open scoped ComplexConjugate ComplexOrder NNReal
 
-variable {G : Type*} [AddCommGroup G] [Fintype G] {f : G → ℂ} {η : ℝ} {ψ : AddChar G ℂ}
+variable {G : Type*} [AddCommGroup G] [Fintype G] {f : G → ℂ} {x η : ℝ} {ψ : AddChar G ℂ}
   {Δ : Finset (AddChar G ℂ)} {m : ℕ}
 
+local notation "𝓛" x:arg => 1 + log x⁻¹
+
+private lemma curlog_pos (hx₀ : 0 ≤ x) (hx₁ : x ≤ 1) : 0 < 𝓛 x := by
+  obtain rfl | hx₀ := hx₀.eq_or_lt
+  · simp
+  have : 0 ≤ log x⁻¹ := log_nonneg $ one_le_inv (by positivity) hx₁
+  positivity
+
+private lemma rpow_inv_neg_curlog_le (hx₀ : 0 ≤ x) (hx₁ : x ≤ 1) : x⁻¹ ^ (𝓛 x)⁻¹ ≤ exp 1 := by
+  obtain rfl | hx₀ := hx₀.eq_or_lt
+  · simp; positivity
+  obtain rfl | hx₁ := hx₁.eq_or_lt
+  · simp
+  have hx := one_lt_inv hx₀ hx₁
+  calc
+    x⁻¹ ^ (𝓛 x)⁻¹ ≤ x⁻¹ ^ (log x⁻¹)⁻¹ := by
+      gcongr
+      · exact hx.le
+      · exact log_pos hx
+      · simp
+    _ ≤ exp 1 := x⁻¹.rpow_inv_log_le_exp_one
+
 noncomputable def changConst : ℝ := 32 * exp 1
 
 lemma one_lt_changConst : 1 < changConst := one_lt_mul (by norm_num) $ one_lt_exp_iff.2 one_pos
@@ -151,13 +173,13 @@ lemma spec_hoelder (hη : 0 ≤ η) (hΔ : Δ ⊆ largeSpec f η) (hm : m ≠ 0)
 /-- **Chang's lemma**. -/
 lemma chang (hf : f ≠ 0) (hη : 0 < η) :
     ∃ Δ, Δ ⊆ largeSpec f η ∧
-      Δ.card ≤ ⌈changConst * exp 1 * ⌈curlog (α f)⌉₊ / η ^ 2⌉₊ ∧ largeSpec f η ⊆ Δ.addSpan := by
+      Δ.card ≤ ⌈changConst * exp 1 * ⌈𝓛 (α f)⌉₊ / η ^ 2⌉₊ ∧ largeSpec f η ⊆ Δ.addSpan := by
   refine exists_subset_addSpan_card_le_of_forall_addDissociated fun Δ hΔη hΔ ↦ ?_
   obtain hΔ' | hΔ' := @eq_zero_or_pos _ _ Δ.card
   · simp [hΔ']
   have : 0 < α f := α_pos hf
-  set β := ⌈curlog (α f)⌉₊
-  have hβ : 0 < β := Nat.ceil_pos.2 (curlog_pos (α_pos hf) $ α_le_one _)
+  set β := ⌈𝓛 (α f)⌉₊
+  have hβ : 0 < β := Nat.ceil_pos.2 (curlog_pos (by positivity) $ α_le_one _)
   refine le_of_pow_le_pow_left hβ.ne' zero_le' $ Nat.cast_le.1 $ le_of_mul_le_mul_right ?_
     (by positivity : 0 < ↑Δ.card ^ β * (η ^ (2 * β) * α f))
   push_cast
@@ -173,5 +195,8 @@ lemma chang (hf : f ≠ 0) (hη : 0 < η) :
     _ = _ := by ring
   refine le_mul_of_one_le_right (by positivity) ?_
   rw [← inv_pos_le_iff_one_le_mul']
-  exact inv_le_exp_curlog.trans $ exp_monotone $ Nat.le_ceil _
+  calc
+    (α f)⁻¹ = exp (0 + log (α f)⁻¹) := by rw [zero_add, exp_log]; norm_cast; positivity
+    _ ≤ exp ⌈0 + log (α f)⁻¹⌉₊ := by gcongr; exact Nat.le_ceil _
+    _ ≤ exp β := by unfold_let β; gcongr; exact zero_le_one
   all_goals positivity
diff --git a/LeanAPAP/Prereqs/Curlog.lean b/LeanAPAP/Prereqs/Curlog.lean
deleted file mode 100644
index a5440548cf..0000000000
--- a/LeanAPAP/Prereqs/Curlog.lean
+++ /dev/null
@@ -1,61 +0,0 @@
-import Mathlib.Analysis.SpecialFunctions.Pow.Real
-import Mathlib.Analysis.SpecialFunctions.Log.Basic
-
-/-!
-# Miscellaneous definitions
--/
-
-open Set
-open scoped ComplexConjugate NNReal
-
-namespace Real
-variable {x : ℝ}
-
--- Maybe define as `2 - log x`
-@[pp_nodot] noncomputable def curlog (x : ℝ) : ℝ := log (exp 2 / x)
-
-@[simp] lemma curlog_zero : curlog 0 = 0 := by simp [curlog]
-
-lemma two_le_curlog (hx₀ : 0 < x) (hx : x ≤ 1) : 2 ≤ x.curlog :=
-  (le_log_iff_exp_le (by positivity)).2 (le_div_self (exp_pos _).le hx₀ hx)
-
-lemma curlog_pos (hx₀ : 0 < x) (hx : x ≤ 1) : 0 < x.curlog :=
-  zero_lt_two.trans_le $ two_le_curlog hx₀ hx
-
-lemma curlog_nonneg (hx₀ : 0 ≤ x) (hx : x ≤ 1) : 0 ≤ x.curlog := by
-  obtain rfl | hx₀ := hx₀.eq_or_lt
-  · simp
-  · exact (curlog_pos hx₀ hx).le
-
-lemma inv_le_exp_curlog : x⁻¹ ≤ exp (curlog x) := by
-  obtain hx | hx := le_or_lt x 0
-  · exact (inv_nonpos.2 hx).trans (exp_pos _).le
-  rw [curlog, exp_log, ← one_div, div_le_div_right hx]
-  · norm_num
-  · positivity
-
-lemma curlog_eq_log_inv_add_two (hx : x ≠ 0) : curlog x = log x⁻¹ + 2 := by
-  rw [curlog, log_div (exp_ne_zero _) hx, log_exp, log_inv, neg_add_eq_sub]
-
-lemma log_inv_le_curlog : log x⁻¹ ≤ curlog x := by
-  obtain rfl | hx := eq_or_ne x 0
-  · simp
-  · rw [curlog_eq_log_inv_add_two hx]
-    exact le_add_of_nonneg_right zero_le_two
-
-lemma rpow_neg_inv_curlog_le (hx₀ : 0 ≤ x) (hx₁ : x ≤ 1) : x ^ (-(curlog x)⁻¹) ≤ exp 1 := by
-  obtain rfl | hx₀ := hx₀.eq_or_lt
-  · simp
-  obtain rfl | hx₁ := hx₁.eq_or_lt
-  · simp
-  have : -1 / log x⁻¹ ≤ -1 / curlog x := by
-    rw [neg_div, neg_div, neg_le_neg_iff]
-    gcongr
-    · exact log_pos $ one_lt_inv hx₀ hx₁
-    · exact log_inv_le_curlog
-  rw [← one_div, ← neg_div]
-  refine (rpow_le_rpow_of_exponent_ge hx₀ hx₁.le this).trans ?_
-  rw [log_inv, rpow_def_of_pos hx₀, neg_div_neg_eq, mul_one_div, div_self]
-  exact log_ne_zero_of_pos_of_ne_one hx₀ hx₁.ne
-
-end Real