Make proof shorter, use suffices a lot

FurstenbergSarkozy/Basic.lean

@@ -62,29 +62,40 @@ noncomputable def almostMaxOfCountOfSquares (n : ℕ) :=
 
 lemma uniform_δ_indicator_at_least_sqr_δ_density_of_countOfSquares_minus_error
     {n : ℕ} {δ : ℝ} (δ_in_unit_interval : 0 ≤ δ ∧ δ ≤ 1)
-    (n_is_large : (upperBoundOnr n + upperBoundOnh n)^2 < n) :
-    δ ^ 2 * (almostMaxOfCountOfSquares n) ≤ countOfSquares n (δ • (mrange n).indicator) := by
+    (n_is_large : (upperBoundOny n + upperBoundOnz n)^2 < n) :
+    δ ^ 2 * (almostMaxOfCountOfSquares n) ≤ countOfSquares n (δ • (range' n).indicator) := by
+
+  let innerTerm (x : ℕ) :=
+    ∑ y ∈ range' (upperBoundOny n),
+      ∑ z ∈ range' (upperBoundOnz n),
+        if x + (y + z) ^ 2 < n then δ * δ else 0
+
+  let almost_n := almostN n
+  suffices reduction :
+      countOfSquares n (δ • (range' n).indicator) ≥ ∑ x ∈ range' almost_n, innerTerm x by
+
+    suffices another_reduction :
+        δ ^ 2 * (almostMaxOfCountOfSquares n) = ∑ x ∈ range' almost_n, innerTerm x by
+      apply Eq.trans_le another_reduction
+      simp_rw [← ge_iff_le]
+      exact reduction
+
+    dsimp [innerTerm]
+    have const_sum_for_range :
+        ∀ x ∈ range' almost_n, ∀ y ∈ range' (upperBoundOny n), ∀ z ∈ range' (upperBoundOnz n),
+        x + (y + z)^2 < n := by
+      sorry
+
+    sorry
+
   dsimp [almostMaxOfCountOfSquares, countOfSquares, generalizedCountOfSquares, indicator]
-  dsimp [piecewise, id']
+  dsimp [Set.indicator, const]
   simp only [mul_assoc, ite_mul]
   simp
-  unfold mrange
-  simp
-  rw [← ge_iff_le]
+  simp_rw [← ge_iff_le]
+  dsimp [innerTerm]
 
-  let almost_n := n - (upperBoundOnr n + upperBoundOnh n)^2
-  have can_go_to_subset {f : ℕ → ℕ} (fpos : ∀ (x : ℕ), 0 ≤ f x) :
-      (∑ x ∈ range n, f x ≥ ∑ x ∈ range almost_n, f x) := by
-    apply sum_le_sum_of_subset_of_nonneg ?_ fun i a a ↦ fpos i
-    simp
-    omega
-
-  let innerTerm (x : ℕ) :=
-    ∑ r ∈ range (upperBoundOnr n),
-      ∑ h ∈ range (upperBoundOnh n),
-        if ∃ a < n, a + 1 = x + 1 + (r + 1 + (h + 1)) ^ 2 then δ * δ else 0
-
-  have innerTerm_pos : ∀ (x : ℕ), 0 ≤ innerTerm x := by
+  have innerTerm_nneg : ∀ (x : ℕ), 0 ≤ innerTerm x := by
     intro x
     dsimp [innerTerm]
     apply sum_nonneg
@@ -94,54 +105,17 @@ lemma uniform_δ_indicator_at_least_sqr_δ_density_of_countOfSquares_minus_error
     apply ite_nonneg (mul_self_nonneg δ)
     rfl
 
-  have to_subset : (∑ x ∈ range n, innerTerm x) ≥ (∑ x ∈ range almost_n, innerTerm x) := by
-    apply sum_le_sum_of_subset_of_nonneg ?_ fun i a a ↦ innerTerm_pos i
-    simp
+  have range'_subset {m n : ℕ} (m_le_n : m ≤ n) : (range' m) ⊆ (range' n) := by
+    dsimp [range']
+    apply Ioc_subset_Ioc_right
+    assumption
+
+  have almost_n_le_n : almost_n ≤ n := by
+    dsimp [almost_n, almostN]
     omega
 
-  convert to_subset using 1
-  dsimp [innerTerm, almost_n]
-
-  have eq_in_innerTerm : ∀ x ∈ range almost_n, ∀ r ∈ range (upperBoundOnr n), ∀ h ∈ range (upperBoundOnh n),
-      ∃ a < n, a + 1 = x + 1 + (r + 1 + (h + 1)) ^ 2 := by
-    intros x hx r hr h hh
-    use (x + (r + h + 2)^2)
-    constructor
-    · dsimp [almost_n, upperBoundOnr, upperBoundOnh] at *
-      simp only [mem_range] at *
-      calc x + (r + h + 2)^2
-        _ ≤ x + (upperBoundOnr n + h + 1)^2 := by
-          simp
-          have : (r + h + 2) ≤ (upperBoundOnr n + h + 1) := by
-            dsimp [upperBoundOnr]
-            omega
-          calc (r + h + 2)^2
-            _ = (r + h + 2) * (r + h + 2) := pow_two (r + h + 2)
-            _ ≤ (upperBoundOnr n + h + 1) * (r + h + 2) := by simp; omega
-            _ ≤ (upperBoundOnr n + h + 1) * (upperBoundOnr n + h + 1) := by simp; omega
-            _ = (upperBoundOnr n + h + 1) ^ 2 := by rw [pow_two]
-        _ ≤ x + (upperBoundOnr n + upperBoundOnh n)^2 := by
-          simp
-          have : (upperBoundOnr n + h + 1) ≤ (upperBoundOnr n + upperBoundOnh n) := by
-            dsimp [upperBoundOnh]
-            omega
-          calc (upperBoundOnr n + h + 1)^2
-            _ = (upperBoundOnr n + h + 1) * (upperBoundOnr n + h + 1) := by rw [pow_two]
-            _ ≤ (upperBoundOnr n + upperBoundOnh n) * (upperBoundOnr n + h + 1) := by simp; omega
-            _ ≤ (upperBoundOnr n + upperBoundOnh n) * (upperBoundOnr n + upperBoundOnh n) :=
-              Nat.mul_le_mul_left (upperBoundOnr n + upperBoundOnh n) (by omega)
-            _ = (upperBoundOnr n + upperBoundOnh n) ^ 2 := by rw [pow_two]
-        _ < n - (upperBoundOnr n + upperBoundOnh n)^2 + (upperBoundOnr n + upperBoundOnh n)^2 := by
-          simp
-          dsimp [upperBoundOnr, upperBoundOnh]
-          exact hx
-        _ = n := by
-          dsimp [upperBoundOnr, upperBoundOnh]
-          omega
-    · linarith
-
-  -- apply sum_eq_card_nsmul
-  sorry
+  rw [ge_iff_le]
+  apply sum_le_sum_of_subset_of_nonneg (range'_subset almost_n_le_n) ?_
 
 -- approach should be the following: do cases. if we have not many fewer than
 -- expected square differences in S, then we are done. otherwise, we can go to a