sum_epsilon_abs_bound

formal source

 552
 553/-- Bound on the inner j-sum of |epsilon| at level n+1: the 8(n+1) terms
 554each bounded by `M * R / (n+2) * 2π / (8(n+1))`, summing to ≤ `M * R * 2π / (n+2)`. -/
 555private theorem sum_epsilon_abs_bound
 556    (qlf : QuantitativeLocalFactorization) {N : ℕ} (n : Fin N) :
 557    ∑ j : Fin (8 * (n.val + 1)),
 558      |(genuineRegularFactorPhaseAt qlf (n.val + 1) (Nat.succ_pos n.val)).sampleIncrements
 559        (n.val + 1) j| ≤
 560      qlf.logDerivBound * qlf.radius * (2 * π) / (↑(n.val) + 2) := by
 561  let B : ℝ :=
 562    qlf.logDerivBound * (qlf.radius / (↑(n.val + 1) + 1)) *
 563      (2 * π / (8 * ↑(n.val + 1)))
 564  have hB : ∀ j : Fin (8 * (n.val + 1)),
 565      |(genuineRegularFactorPhaseAt qlf (n.val + 1) (Nat.succ_pos n.val)).sampleIncrements
 566        (n.val + 1) j| ≤ B := by
 567    intro j
 568    simpa [B] using epsilon_abs_bound qlf (n.val + 1) (Nat.succ_pos n.val) j
 569  calc
 570    ∑ j : Fin (8 * (n.val + 1)),
 571        |(genuineRegularFactorPhaseAt qlf (n.val + 1) (Nat.succ_pos n.val)).sampleIncrements
 572          (n.val + 1) j|
 573      ≤ ∑ _j : Fin (8 * (n.val + 1)), B := by
 574          apply Finset.sum_le_sum
 575          intro j _
 576          exact hB j
 577    _ = (8 * (n.val + 1) : ℝ) * B := by
 578          rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
 579          norm_num [Nat.cast_add, Nat.cast_mul]
 580    _ = qlf.logDerivBound * qlf.radius * (2 * π) / (↑(n.val) + 2) := by
 581          have h8n : (8 * ((n.val : ℝ) + 1)) ≠ 0 := by positivity
 582          have hn2 : (n.val : ℝ) + 2 ≠ 0 := by positivity
 583          simp [B, Nat.cast_add]
 584          field_simp [h8n, hn2]
 585          ring