gap_diminishing_increments

proof body

Tactic-mode proof.

 197  -- Use slope inequality for strict concave functions on ℝ with x=n, y=n+1, z=n+2.
 198  have hsc := strictConcaveOn_gapR_Ici
 199  have hx : (n : ℝ) ∈ Set.Ici (0 : ℝ) := by
 200    simpa [Set.mem_Ici] using (show (0 : ℝ) ≤ (n : ℝ) from by exact_mod_cast (Nat.zero_le n))
 201  have hy : ((n + 1 : ℕ) : ℝ) ∈ Set.Ici (0 : ℝ) := by
 202    simpa [Set.mem_Ici] using (show (0 : ℝ) ≤ ((n + 1 : ℕ) : ℝ) from by exact_mod_cast (Nat.zero_le (n + 1)))
 203  have hz : ((n + 2 : ℕ) : ℝ) ∈ Set.Ici (0 : ℝ) := by
 204    simpa [Set.mem_Ici] using (show (0 : ℝ) ≤ ((n + 2 : ℕ) : ℝ) from by exact_mod_cast (Nat.zero_le (n + 2)))
 205  have hxy : (n : ℝ) < ((n + 1 : ℕ) : ℝ) := by
 206    exact_mod_cast (Nat.lt_succ_self n)
 207  have hyz : ((n + 1 : ℕ) : ℝ) < ((n + 2 : ℕ) : ℝ) := by
 208    exact_mod_cast (Nat.lt_succ_self (n + 1))
 209  have hslope :
 210      (gapR ((n + 2 : ℕ) : ℝ) - gapR ((n + 1 : ℕ) : ℝ)) /
 211          (((n + 2 : ℕ) : ℝ) - ((n + 1 : ℕ) : ℝ)) <
 212        (gapR ((n + 1 : ℕ) : ℝ) - gapR (n : ℝ)) /
 213          (((n + 1 : ℕ) : ℝ) - (n : ℝ)) :=
 214    StrictConcaveOn.slope_anti_adjacent hsc (hx := hx) (hz := hz) hxy hyz
 215  -- simplify denominators (both are 1), noting simp may rewrite `((n+1:ℕ):ℝ)` as `↑n + 1`
 216  have hslope' : gapR ((n + 2 : ℕ) : ℝ) - gapR ((n + 1 : ℕ) : ℝ) <
 217        gapR ((n + 1 : ℕ) : ℝ) - gapR (n : ℝ) := by
 218    -- First simplify the denominators to explicit numerals, then discharge them with `norm_num`.
 219    have hs' :
 220        (gapR (↑n + 2) - gapR (↑n + 1)) / ((2 : ℝ) - 1) <
 221          (gapR (↑n + 1) - gapR (n : ℝ)) / ((1 : ℝ) - 0) := by
 222      -- `simp` rewrites casts like `((n+1:ℕ):ℝ)` into `↑n + 1`.
 223      -- It also rewrites the differences of successive naturals into numerals.
 224      simpa [Nat.cast_add, Nat.cast_ofNat, add_assoc, add_left_comm, add_comm] using hslope
 225    have hdenL : ((2 : ℝ) - 1) = (1 : ℝ) := by norm_num
 226    have hdenR : ((1 : ℝ) - 0) = (1 : ℝ) := by norm_num
 227    -- remove the divisions by 1
 228    simpa [hdenL, hdenR, div_one] using hs'
 229  -- rewrite back from `gapR` on naturals to `gap` on integers.
 230  -- We do this with explicit `simp` so the rewriting doesn't get stuck on expressions like `↑n + k`.
 231  have hfinal :
 232      gap ((n + 2 : ℕ) : ℤ) - gap ((n + 1 : ℕ) : ℤ) <
 233        gap ((n + 1 : ℕ) : ℤ) - gap (n : ℤ) := by
 234    -- `simp` likes to rewrite `((n+k:ℕ):ℝ)` into `↑n + k`, which prevents `gapR_nat` from firing.
 235    -- So we rewrite *back* to the `(n+k : ℕ)` cast form first, then apply `gapR_nat`.
 236    have hslope_cast :
 237        gapR (↑n + 2) - gapR (↑n + 1) < gapR (↑n + 1) - gapR (n : ℝ) := by
 238      -- avoid `simp` here (it can loop on casts); use `rw` with explicit cast equalities.
 239      have h1 : ((n + 1 : ℕ) : ℝ) = (↑n + 1 : ℝ) := by norm_num
 240      have h2 : ((n + 2 : ℕ) : ℝ) = (↑n + 2 : ℝ) := by norm_num
 241      have h := hslope'
 242      -- rewrite nat-casts into `↑n + k`
 243      rw [h1, h2] at h
 244      exact h
 245
 246    have hcast1 : (↑n + 1 : ℝ) = ((n + 1 : ℕ) : ℝ) := by norm_num
 247    have hcast2 : (↑n + 2 : ℝ) = ((n + 2 : ℕ) : ℝ) := by norm_num
 248
 249    -- rewrite the inequality into the nat-cast form
 250    have hslope_nat :
 251        gapR ((n + 2 : ℕ) : ℝ) - gapR ((n + 1 : ℕ) : ℝ) <
 252          gapR ((n + 1 : ℕ) : ℝ) - gapR (n : ℝ) := by
 253      have h := hslope_cast
 254      -- rewrite `↑n + k` back into `((n+k):ℕ):ℝ`
 255      rw [hcast1, hcast2] at h
 256      exact h
 257
 258    -- finally, apply `gapR_nat` on the three natural arguments (using `rw` to avoid cast rewriting).
 259    have h := hslope_nat
 260    rw [gapR_nat (n + 2), gapR_nat (n + 1), gapR_nat n] at h
 261    simpa using h
 262  exact hfinal
 263