refactor(SimpleGraph): make triangleRemovalBound positive more often (#29540)

It wasn't positive when `ε > 4`, but that is a junk value anyway, so we change the junk value to a positive one.

See #29496 for more context.

Author: YaelDillies

Mathlib/Combinatorics/Additive/Corner/Roth.lean

@@ -87,10 +87,7 @@ theorem corners_theorem (ε : ℝ) (hε : 0 < ε) (hG : cornersTheoremBound ε 
     rwa [mul_le_iff_le_one_left] at this
     positivity
   have := noAccidental hA
-  rw [Nat.floor_lt' (by positivity), inv_lt_iff_one_lt_mul₀'] at hG
-  swap
-  · have := triangleRemovalBound_pos (ε := ε / 9) (by linarith) (by linarith)
-    linarith
+  rw [Nat.floor_lt' (by positivity), inv_lt_iff_one_lt_mul₀' (by positivity)] at hG
   refine hG.not_ge (le_of_mul_le_mul_right ?_ (by positivity : (0 : ℝ) < card G ^ 2))
   classical
   have h₁ := (farFromTriangleFree_graph hAε).le_card_cliqueFinset

Mathlib/Combinatorics/SimpleGraph/DeleteEdges.lean

@@ -221,6 +221,9 @@ alias ⟨DeleteFar.le_card_sub_card, _⟩ := deleteFar_iff
 theorem DeleteFar.mono (h : G.DeleteFar p r₂) (hr : r₁ ≤ r₂) : G.DeleteFar p r₁ := fun _ hs hG =>
   hr.trans <| h hs hG
 
+lemma DeleteFar.le_card_edgeFinset (h : G.DeleteFar p r) (hp : p ⊥) : r ≤ #G.edgeFinset :=
+  h subset_rfl (by simpa)
+
 end DeleteFar
 
 end SimpleGraph

Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean

@@ -8,6 +8,7 @@ import Mathlib.Algebra.Order.Ring.Abs
 import Mathlib.Combinatorics.Enumerative.DoubleCounting
 import Mathlib.Combinatorics.SimpleGraph.Clique
 import Mathlib.Data.Finset.Sym
+import Mathlib.Data.Nat.Choose.Bounds
 import Mathlib.Tactic.GCongr
 import Mathlib.Tactic.Positivity
 
@@ -252,29 +253,14 @@ end DecidableEq
 
 variable [Nonempty α]
 
-lemma FarFromTriangleFree.lt_half (hG : G.FarFromTriangleFree ε) : ε < 2⁻¹ := by
-  classical
-  by_contra! hε
-  refine lt_irrefl (ε * card α ^ 2) ?_
-  have hε₀ : 0 < ε := hε.trans_lt' (by simp)
-  rw [inv_le_iff_one_le_mul₀ (zero_lt_two' 𝕜)] at hε
-  calc
-    _ ≤ (#G.edgeFinset : 𝕜) := by
-      simpa using hG.le_card_sub_card bot_le (cliqueFree_bot (le_succ _))
-    _ ≤ ε * 2 * #G.edgeFinset := le_mul_of_one_le_left (by positivity) (by assumption)
-    _ < ε * card α ^ 2 := ?_
-  rw [mul_assoc, mul_lt_mul_left hε₀]
-  norm_cast
+lemma FarFromTriangleFree.lt_half (hε : G.FarFromTriangleFree ε) : ε < 2⁻¹ := by
+  refine lt_of_mul_lt_mul_right (α := 𝕜) (a := Fintype.card α ^ 2) ?_ (by positivity)
   calc
-    _ ≤ 2 * (completeGraph α).edgeFinset.card := by gcongr; exact le_top
-    _ < card α ^ 2 := ?_
-  rw [edgeFinset_top, filter_not, card_sdiff_of_subset (subset_univ _), Finset.card_univ, Sym2.card]
-  simp_rw [choose_two_right, Nat.add_sub_cancel, Nat.mul_comm _ (card α),
-    funext (propext <| Sym2.isDiag_iff_mem_range_diag ·), univ_filter_mem_range, mul_tsub,
-    Nat.mul_div_cancel' (card α).even_mul_succ_self.two_dvd]
-  rw [card_image_of_injective _ Sym2.diag_injective, Finset.card_univ, mul_add_one (α := ℕ),
-    two_mul, sq, add_tsub_add_eq_tsub_right]
-  apply tsub_lt_self <;> positivity
+        ε * Fintype.card α ^ 2
+    _ ≤ #G.edgeFinset := by simpa using hε.le_card_edgeFinset (by simp)
+    _ ≤ (Fintype.card α).choose 2 := by gcongr; exact card_edgeFinset_le_card_choose_two
+    _ < 2⁻¹ * Fintype.card α ^ 2 := by
+      simpa [← div_eq_inv_mul] using Nat.choose_lt_pow_div (by positivity) le_rfl
 
 lemma FarFromTriangleFree.lt_one (hG : G.FarFromTriangleFree ε) : ε < 1 :=
   hG.lt_half.trans two_inv_lt_one

Mathlib/Combinatorics/SimpleGraph/Triangle/Removal.lean

@@ -29,12 +29,16 @@ namespace SimpleGraph
 /-- An explicit form for the constant in the triangle removal lemma.
 
 Note that this depends on `SzemerediRegularity.bound`, which is a tower-type exponential. This means
-`triangleRemovalBound` is in practice absolutely tiny. -/
+`triangleRemovalBound` is in practice absolutely tiny.
+
+This definition is meant to be used for small values of `ε`, and in particular is junk for values
+of `ε` greater than or equal to `1`. The junk value is chosen to be positive, so that
+`0 < ε → 0 < triangleRemovalBound ε` regardless of whether `ε < 1` or not. -/
 noncomputable def triangleRemovalBound (ε : ℝ) : ℝ :=
-  min (2 * ⌈4/ε⌉₊^3)⁻¹ ((1 - ε/4) * (ε/(16 * bound (ε/8) ⌈4/ε⌉₊))^3)
+  min (2 * ⌈4/ε⌉₊^3)⁻¹ ((1 - min 1 ε/4) * (ε/(16 * bound (ε/8) ⌈4/ε⌉₊))^3)
 
-lemma triangleRemovalBound_pos (hε : 0 < ε) (hε₁ : ε ≤ 1) : 0 < triangleRemovalBound ε := by
-  have : 0 < 1 - ε / 4 := by linarith
+lemma triangleRemovalBound_pos (hε : 0 < ε) : 0 < triangleRemovalBound ε := by
+  have : 0 < 1 - min 1 ε/4 := by have := min_le_left 1 ε; linarith
   unfold triangleRemovalBound
   positivity
 
@@ -48,6 +52,10 @@ lemma triangleRemovalBound_mul_cube_lt (hε : 0 < ε) :
     _ = 2⁻¹ := by rw [mul_inv, inv_mul_cancel_right₀]; positivity
     _ < 1 := by norm_num
 
+lemma triangleRemovalBound_le (hε₁ : ε ≤ 1) :
+    triangleRemovalBound ε ≤ (1 - ε/4) * (ε/(16 * bound (ε/8) ⌈4/ε⌉₊)) ^ 3 := by
+  simp [triangleRemovalBound, hε₁]
+
 private lemma aux {n k : ℕ} (hk : 0 < k) (hn : k ≤ n) : n < 2 * k * (n / k) := by
   rw [mul_assoc, two_mul, ← add_lt_add_iff_right (n % k), add_right_comm, add_assoc,
     mod_add_div n k, add_comm, add_lt_add_iff_right]
@@ -65,7 +73,7 @@ private lemma card_bound (hP₁ : P.IsEquipartition) (hP₃ : #P.parts ≤ bound
       (div_le_iff₀' (by positivity)).2 <| mod_cast (aux ‹_› P.card_parts_le_card).le
     _ ≤ (#s : ℝ) := mod_cast hP₁.average_le_card_part hX
 
-private lemma triangle_removal_aux (hε : 0 < ε) (hP₁ : P.IsEquipartition)
+private lemma triangle_removal_aux (hε : 0 < ε) (hε₁ : ε ≤ 1) (hP₁ : P.IsEquipartition)
     (hP₃ : #P.parts ≤ bound (ε / 8) ⌈4 / ε⌉₊)
     (ht : t ∈ (G.regularityReduced P (ε / 8) (ε / 4)).cliqueFinset 3) :
     triangleRemovalBound ε * card α ^ 3 ≤ #(G.cliqueFinset 3) := by
@@ -84,7 +92,7 @@ private lemma triangle_removal_aux (hε : 0 < ε) (hP₁ : P.IsEquipartition)
     have : ε / 4 ≤ 1 := ‹ε / 4 ≤ _›.trans (by exact mod_cast G.edgeDensity_le_one _ _); linarith
   calc
     _ ≤ (1 - ε/4) * (ε/(16 * bound (ε/8) ⌈4/ε⌉₊))^3 * card α ^ 3 := by
-      gcongr; exact min_le_right _ _
+      gcongr; exact triangleRemovalBound_le hε₁
     _ = (1 - 2 * (ε / 8)) * (ε / 8) ^ 3 * (card α / (2 * bound (ε / 8) ⌈4 / ε⌉₊)) *
           (card α / (2 * bound (ε / 8) ⌈4 / ε⌉₊)) * (card α / (2 * bound (ε / 8) ⌈4 / ε⌉₊)) := by
       ring
@@ -132,7 +140,7 @@ lemma FarFromTriangleFree.le_card_cliqueFinset (hG : G.FarFromTriangleFree ε) :
   rcases le_total (card α) l with hl' | hl'
   · calc
       _ ≤ triangleRemovalBound ε * ↑l ^ 3 := by
-        gcongr; exact (triangleRemovalBound_pos hε hG.lt_one.le).le
+        gcongr; exact (triangleRemovalBound_pos hε).le
       _ ≤ (1 : ℝ) := (triangleRemovalBound_mul_cube_lt hε).le
       _ ≤ _ := by simpa [one_le_iff_ne_zero] using (hG.cliqueFinset_nonempty hε).card_pos.ne'
   obtain ⟨P, hP₁, hP₂, hP₃, hP₄⟩ := szemeredi_regularity G (by positivity : 0 < ε / 8) hl'
@@ -141,7 +149,7 @@ lemma FarFromTriangleFree.le_card_cliqueFinset (hG : G.FarFromTriangleFree ε) :
   rw [mul_assoc] at k
   replace k := lt_of_mul_lt_mul_left k zero_le_two
   obtain ⟨t, ht⟩ := hG.cliqueFinset_nonempty' regularityReduced_le k
-  exact triangle_removal_aux hε hP₁ hP₃ ht
+  exact triangle_removal_aux hε hG.lt_one.le hP₁ hP₃ ht
 
 /-- **Triangle Removal Lemma**. If there are not too many triangles (on the order of `(card α)^3`)
 then they can all be removed by removing a few edges (on the order of `(card α)^2`). -/
@@ -154,3 +162,23 @@ lemma triangle_removal (hG : #(G.cliqueFinset 3) < triangleRemovalBound ε * car
   exact le_of_not_gt fun i ↦ h G' hG _ i hG'
 
 end SimpleGraph
+
+namespace Mathlib.Meta.Positivity
+open Lean.Meta Qq SimpleGraph
+
+/-- Extension for the `positivity` tactic: `SimpleGraph.triangleRemovalBound ε` is positive
+if `ε` is.
+
+This exploits the positivity of the junk value of `triangleRemovalBound ε` for `ε ≥ 1`. -/
+@[positivity triangleRemovalBound _]
+def evalTriangleRemovalBound : PositivityExt where eval {u α} _zα _pα e := do
+  match u, α, e with
+  | 0, ~q(ℝ), ~q(triangleRemovalBound $ε) =>
+    let .positive hε ← core q(inferInstance) q(inferInstance) ε | failure
+    assertInstancesCommute
+    pure (.positive q(triangleRemovalBound_pos $hε))
+  | _, _, _ => throwError "failed to match on Int.ceil application"
+
+example (ε : ℝ) (hε : 0 < ε) : 0 < triangleRemovalBound ε := by positivity
+
+end Mathlib.Meta.Positivity

Mathlib/Data/Nat/Choose/Bounds.lean

@@ -23,7 +23,7 @@ bounds `n^r/r^r ≤ n.choose r ≤ e^r n^r/r^r` in the future.
 
 open Nat
 
-variable {α : Type*} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α]
+variable {α : Type*} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {n k : ℕ}
 
 namespace Nat
 
@@ -34,15 +34,25 @@ theorem choose_le_pow_div (r n : ℕ) : (n.choose r : α) ≤ (n ^ r : α) / r !
     exact n.descFactorial_le_pow r
   exact mod_cast r.factorial_pos
 
+lemma choose_lt_pow_div (hn : n ≠ 0) (hk : 2 ≤ k) : (n.choose k : α) < (n ^ k : α) / k ! := by
+  rw [lt_div_iff₀' (mod_cast k.factorial_pos)]
+  norm_cast
+  rw [← Nat.descFactorial_eq_factorial_mul_choose]
+  exact descFactorial_lt_pow hn hk
+
 lemma choose_le_descFactorial (n k : ℕ) : n.choose k ≤ n.descFactorial k := by
   rw [choose_eq_descFactorial_div_factorial]
   exact Nat.div_le_self _ _
 
-/-- This lemma was changed on 2024/08/29, the old statement is available
-in `Nat.choose_le_pow_div`. -/
+lemma choose_lt_descFactorial (hk : 2 ≤ k) (hkn : k ≤ n) : n.choose k < n.descFactorial k := by
+  rw [choose_eq_descFactorial_div_factorial]; exact Nat.div_lt_self (by simpa) (by simpa)
+
 lemma choose_le_pow (n k : ℕ) : n.choose k ≤ n ^ k :=
   (choose_le_descFactorial n k).trans (descFactorial_le_pow n k)
 
+lemma choose_lt_pow (hn : n ≠ 0) (hk : 2 ≤ k) : n.choose k < n ^ k :=
+  (choose_le_descFactorial n k).trans_lt (descFactorial_lt_pow hn hk)
+
 -- horrific casting is due to ℕ-subtraction
 theorem pow_le_choose (r n : ℕ) : ((n + 1 - r : ℕ) ^ r : α) / r ! ≤ n.choose r := by
   rw [div_le_iff₀']

Mathlib/Data/Nat/Factorial/Basic.lean

@@ -346,6 +346,9 @@ theorem descFactorial_eq_zero_iff_lt {n : ℕ} : ∀ {k : ℕ}, n.descFactorial
       Nat.sub_eq_zero_iff_le, Nat.lt_iff_le_and_ne, or_iff_left_iff_imp, and_imp]
     exact fun h _ => h
 
+@[simp]
+lemma descFactorial_pos {n k : ℕ} : 0 < n.descFactorial k ↔ k ≤ n := by simp [Nat.pos_iff_ne_zero]
+
 alias ⟨_, descFactorial_of_lt⟩ := descFactorial_eq_zero_iff_lt
 
 theorem add_descFactorial_eq_ascFactorial (n : ℕ) : ∀ k : ℕ,
@@ -434,13 +437,12 @@ theorem descFactorial_le_pow (n : ℕ) : ∀ k : ℕ, n.descFactorial k ≤ n ^
     rw [descFactorial_succ, Nat.pow_succ, Nat.mul_comm _ n]
     exact Nat.mul_le_mul (Nat.sub_le _ _) (descFactorial_le_pow _ k)
 
-theorem descFactorial_lt_pow {n : ℕ} (hn : 1 ≤ n) : ∀ {k : ℕ}, 2 ≤ k → n.descFactorial k < n ^ k
+theorem descFactorial_lt_pow {n : ℕ} (hn : n ≠ 0) : ∀ {k : ℕ}, 2 ≤ k → n.descFactorial k < n ^ k
   | 0 => by rintro ⟨⟩
   | 1 => by intro; contradiction
   | k + 2 => fun _ => by
     rw [descFactorial_succ, pow_succ', Nat.mul_comm, Nat.mul_comm n]
-    exact Nat.mul_lt_mul_of_le_of_lt (descFactorial_le_pow _ _) (Nat.sub_lt hn k.zero_lt_succ)
-      (Nat.pow_pos (Nat.lt_of_succ_le hn))
+    exact Nat.mul_lt_mul_of_le_of_lt (descFactorial_le_pow _ _) (by omega) (Nat.pow_pos <| by omega)
 
 end DescFactorial