2607.19283v1 / ENOTV/Endpoint.lean

all files

import ENOTV.Bulk
import Mathlib.Algebra.Polynomial.Div

/-!
# Endpoint decay of Euler blocks

The zeros `E_d(0)=E_d(1)=0` save one power of the block length near
endpoints.  We make the constant explicit through the coefficient norm of
`E_d / X`.
-/

noncomputable section

set_option maxHeartbeats 800000

open Polynomial

namespace ENOTV

def eulerTail (d : ℕ) : ℚ[X] := eulerPoly d /ₘ X

theorem X_mul_eulerTail (d : ℕ) (hd : 0 < d) (heven : Even d) :
    X * eulerTail d = eulerPoly d := by
  have hroot : (eulerPoly d).IsRoot 0 := by
    rw [Polynomial.IsRoot.def, eulerPoly_zero d hd heven]
  simpa [eulerTail] using
    (Polynomial.mul_divByMonic_eq_iff_isRoot
      (p := eulerPoly d) (a := 0)).mpr hroot

theorem eulerPoly_eval_eq_mul_tail (d : ℕ) (hd : 0 < d) (heven : Even d)
    (x : ℚ) :
    (eulerPoly d).eval x = x * (eulerTail d).eval x := by
  have h := congrArg (Polynomial.eval x) (X_mul_eulerTail d hd heven)
  simpa using h.symm

def endpointUpper (d R : ℕ) : ℚ :=
  R * 2 ^ (d - 1) * coeffAbsSum (eulerTail d)

theorem endpointUpper_nonneg (d R : ℕ) : 0 ≤ endpointUpper d R := by
  unfold endpointUpper
  exact mul_nonneg (mul_nonneg (by positivity) (by positivity))
    (coeffAbsSum_nonneg _)

theorem abs_blockPoly_endpoint_le (d R L h : ℕ)
    (hd : 0 < d) (heven : Even d) (hL : 0 < L) (hh : h ≤ R)
    (hinside : h ≤ 2 * L) :
    |blockPoly d L h| ≤ endpointUpper d R * (L : ℚ) ^ (d - 1) := by
  have hden : (0 : ℚ) < 2 * L := by positivity
  have hx0 : (0 : ℚ) ≤ (h : ℚ) / (2 * L) := by positivity
  have hx1 : (h : ℚ) / (2 * L) ≤ 1 := by
    apply (div_le_one hden).2
    exact_mod_cast hinside
  have hxabs : |(h : ℚ) / (2 * L)| ≤ 1 := by
    rw [abs_of_nonneg hx0]
    exact hx1
  have htail := abs_eval_le_coeffAbsSum (eulerTail d) hxabs
  rw [blockPoly, eulerPoly_eval_eq_mul_tail d hd heven, abs_mul, abs_mul,
    abs_pow, abs_of_nonneg (show (0 : ℚ) ≤ 2 * L by positivity),
    abs_of_nonneg hx0]
  have hdform : d = (d - 1) + 1 := by omega
  have hpow :
      (2 * (L : ℚ)) ^ d =
        (2 * (L : ℚ)) ^ (d - 1) * (2 * L) := by
    conv_lhs => rw [hdform, pow_succ]
  rw [hpow]
  calc
    (2 * (L : ℚ)) ^ (d - 1) * (2 * L) *
          ((h : ℚ) / (2 * L) * |(eulerTail d).eval ((h : ℚ) / (2 * L))|) =
        (h : ℚ) * (2 * L) ^ (d - 1) *
          |(eulerTail d).eval ((h : ℚ) / (2 * L))| := by
      field_simp
    _ ≤ (R : ℚ) * (2 * L) ^ (d - 1) *
        coeffAbsSum (eulerTail d) := by
      gcongr
    _ = endpointUpper d R * (L : ℚ) ^ (d - 1) := by
      simp only [endpointUpper]
      push_cast
      rw [mul_pow]
      ring

theorem blockPoly_reflect (d L h : ℕ) (hd : 0 < d) (heven : Even d)
    (hh : h ≤ 2 * L) :
    blockPoly d L (2 * L - h) = blockPoly d L h := by
  by_cases hL : L = 0
  · subst L
    have : h = 0 := by omega
    subst h
    simp
  · unfold blockPoly
    have hden : (2 * (L : ℚ)) ≠ 0 := by positivity
    have harg :
        ((2 * (L : ℚ) - h) / (2 * L)) =
          1 - (h : ℚ) / (2 * L) := by
      field_simp
    rw [harg, eulerPoly_one_sub d heven]

theorem abs_blockPoly_right_endpoint_le (d R L h : ℕ)
    (hd : 0 < d) (heven : Even d) (hL : 0 < L) (hh : h ≤ R)
    (hinside : h ≤ 2 * L) :
    |blockPoly d L (2 * L - h)| ≤
      endpointUpper d R * (L : ℚ) ^ (d - 1) := by
  rw [blockPoly_reflect d L h hd heven hinside]
  exact abs_blockPoly_endpoint_le d R L h hd heven hL hh hinside

theorem abs_realBlock_endpoint_le (d R L h : ℕ)
    (hd : 0 < d) (heven : Even d) (hL : 0 < L) (hh : h ≤ R)
    (hinside : h ≤ 2 * L) :
    |realBlock d L h| ≤
      (endpointUpper d R : ℝ) * (L : ℝ) ^ (d - 1) := by
  unfold realBlock
  exact_mod_cast
    abs_blockPoly_endpoint_le d R L h hd heven hL hh hinside

end ENOTV