theorem
proved
sum_epsilon_sq_bound
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.NumberTheory.MeromorphicCircleOrder on GitHub at line 588.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
585 ring
586
587/-- Bound on the inner j-sum of epsilon² at level n+1. -/
588theorem sum_epsilon_sq_bound
589 (qlf : QuantitativeLocalFactorization) {N : ℕ} (n : Fin N) :
590 ∑ j : Fin (8 * (n.val + 1)),
591 ((genuineRegularFactorPhaseAt qlf (n.val + 1) (Nat.succ_pos n.val)).sampleIncrements
592 (n.val + 1) j) ^ 2 ≤
593 qlf.logDerivBound ^ 2 * qlf.radius ^ 2 * (2 * π) ^ 2 /
594 (8 * (↑(n.val) + 1) * (↑(n.val) + 2) ^ 2) := by
595 let B : ℝ :=
596 qlf.logDerivBound * (qlf.radius / (↑(n.val + 1) + 1)) *
597 (2 * π / (8 * ↑(n.val + 1)))
598 have hB_nonneg : 0 ≤ B := by
599 have hlog_nonneg : 0 ≤ qlf.logDerivBound := le_of_lt qlf.logDerivBound_pos
600 have hr_nonneg : 0 ≤ qlf.radius := le_of_lt qlf.radius_pos
601 have hdiv1 : 0 ≤ qlf.radius / (↑(n.val + 1) + 1) := by
602 exact div_nonneg hr_nonneg (by positivity)
603 have hdiv2 : 0 ≤ 2 * π / (8 * ↑(n.val + 1)) := by
604 exact div_nonneg (by positivity) (by positivity)
605 dsimp [B]
606 exact mul_nonneg (mul_nonneg hlog_nonneg hdiv1) hdiv2
607 have hBsq : ∀ j : Fin (8 * (n.val + 1)),
608 ((genuineRegularFactorPhaseAt qlf (n.val + 1) (Nat.succ_pos n.val)).sampleIncrements
609 (n.val + 1) j) ^ 2 ≤ B ^ 2 := by
610 intro j
611 have hj := epsilon_abs_bound qlf (n.val + 1) (Nat.succ_pos n.val) j
612 have hj' :
613 |(genuineRegularFactorPhaseAt qlf (n.val + 1) (Nat.succ_pos n.val)).sampleIncrements
614 (n.val + 1) j| ≤ B := by
615 simpa [B] using hj
616 have hBabs : |B| = B := abs_of_nonneg hB_nonneg
617 exact (sq_le_sq).2 (by simpa [hBabs] using hj')
618 calc