BKLNW_app.besselI0_sub_partial_le

lemma besselI0_sub_partial_le (x : ℝ) (N : ℕ) :    besselI0 x - ∑ m ∈ Finset.range N, (x / 2) ^ (2 * m) / ((m.factorial : ℝ)) ^ 2 ≤      (x / 2) ^ (2 * N) / ((N.factorial : ℝ)) ^ 2 * besselI0 x := by  have hsum := besselI0_summable x  have hb : besselI0 x = ∑' m : ℕ, (x / 2) ^ (2 * m) / ((m.factorial : ℝ)) ^ 2 := rfl  have hsplit := hsum.sum_add_tsum_nat_add N  have hterm : ∀ k : ℕ, (x / 2) ^ (2 * (k + N)) / (((k + N).factorial : ℝ)) ^ 2 ≤      (x / 2) ^ (2 * N) / ((N.factorial : ℝ)) ^ 2 *        ((x / 2) ^ (2 * k) / ((k.factorial : ℝ)) ^ 2) := by    intro k    have hfact : (N.factorial : ℝ) * (k.factorial : ℝ) ≤ ((k + N).factorial : ℝ) := by      exact_mod_cast Nat.le_of_dvd (k + N).factorial_pos        (by simpa [mul_comm] using Nat.factorial_mul_factorial_dvd_factorial_add k N)    have hN : (0 : ℝ) < ((N.factorial : ℝ)) ^ 2 :=      pow_pos (by exact_mod_cast N.factorial_pos) 2    have hk : (0 : ℝ) < ((k.factorial : ℝ)) ^ 2 :=      pow_pos (by exact_mod_cast k.factorial_pos) 2    have hNk : (0 : ℝ) ≤ (N.factorial : ℝ) * (k.factorial : ℝ) := by positivity    rw [show 2 * (k + N) = 2 * N + 2 * k by ring, pow_add, div_mul_div_comm]    gcongr (x / 2) ^ (2 * N) * (x / 2) ^ (2 * k) / ?_ <;>      first        | exact mul_pos hN hk        | (rw [pow_mul, pow_mul]; positivity)        | nlinarith [hfact, hNk]  have htail : (∑' k : ℕ, (x / 2) ^ (2 * (k + N)) / (((k + N).factorial : ℝ)) ^ 2) ≤      (x / 2) ^ (2 * N) / ((N.factorial : ℝ)) ^ 2 * besselI0 x := by    calc (∑' k : ℕ, (x / 2) ^ (2 * (k + N)) / (((k + N).factorial : ℝ)) ^ 2)        ≤ ∑' k : ℕ, (x / 2) ^ (2 * N) / ((N.factorial : ℝ)) ^ 2 *            ((x / 2) ^ (2 * k) / ((k.factorial : ℝ)) ^ 2) :=          Summable.tsum_le_tsum hterm ((summable_nat_add_iff N).mpr hsum)            (hsum.mul_left ((x / 2) ^ (2 * N) / ((N.factorial : ℝ)) ^ 2))      _ = (x / 2) ^ (2 * N) / ((N.factorial : ℝ)) ^ 2 * besselI0 x := by          rw [tsum_mul_left, ← hb]  linarith [hsplit, htail, hb.le, hb.ge]