2607.19283v1 / ENOTV/Estimates.lean
all files
import ENOTV.Counterexample
/-!
# Quantitative bounds for Euler blocks
The constants in this file are deliberately explicit coefficient sums. Their
numerical values are irrelevant; only dependence on the fixed degree matters.
-/
noncomputable section
open scoped BigOperators
open Polynomial
namespace ENOTV
/-- Sum of absolute values of all coefficients (including one harmless
trailing zero slot when appropriate). -/
def coeffAbsSum (p : ℚ[X]) : ℚ :=
∑ i ∈ Finset.range (p.natDegree + 1), |p.coeff i|
theorem coeffAbsSum_nonneg (p : ℚ[X]) : 0 ≤ coeffAbsSum p := by
apply Finset.sum_nonneg
intro i hi
positivity
theorem abs_eval_le_coeffAbsSum (p : ℚ[X]) {x : ℚ} (hx : |x| ≤ 1) :
|p.eval x| ≤ coeffAbsSum p := by
rw [Polynomial.eval_eq_sum_range]
calc
|∑ i ∈ Finset.range (p.natDegree + 1), p.coeff i * x ^ i| ≤
∑ i ∈ Finset.range (p.natDegree + 1), |p.coeff i * x ^ i| :=
Finset.abs_sum_le_sum_abs _ _
_ ≤ ∑ i ∈ Finset.range (p.natDegree + 1), |p.coeff i| := by
apply Finset.sum_le_sum
intro i hi
rw [abs_mul, abs_pow]
exact mul_le_of_le_one_right (abs_nonneg (p.coeff i))
(pow_le_one₀ (abs_nonneg x) hx)
_ = coeffAbsSum p := rfl
/-- A fixed degree-dependent upper-bound constant. -/
def eulerUpper (d : ℕ) : ℚ := 2 ^ d * coeffAbsSum (eulerPoly d)
theorem eulerUpper_nonneg (d : ℕ) : 0 ≤ eulerUpper d := by
exact mul_nonneg (by positivity) (coeffAbsSum_nonneg _)
theorem abs_blockPoly_le (d L t : ℕ) (hL : 0 < L) (ht : t ≤ 2 * L) :
|blockPoly d L t| ≤ eulerUpper d * L ^ d := by
have hden : (0 : ℚ) < 2 * L := by positivity
have hx0 : (0 : ℚ) ≤ (t : ℚ) / (2 * L) := by positivity
have hx1 : (t : ℚ) / (2 * L) ≤ 1 := by
apply (div_le_one hden).2
exact_mod_cast ht
have hxabs : |(t : ℚ) / (2 * L)| ≤ 1 := by
rw [abs_of_nonneg hx0]
exact hx1
have he := abs_eval_le_coeffAbsSum (eulerPoly d) hxabs
rw [blockPoly, abs_mul, abs_pow, abs_of_nonneg (show (0 : ℚ) ≤ 2 * L by positivity)]
calc
(2 * (L : ℚ)) ^ d *
|(eulerPoly d).eval ((t : ℚ) / (2 * L))| ≤
(2 * (L : ℚ)) ^ d * coeffAbsSum (eulerPoly d) := by gcongr
_ = eulerUpper d * (L : ℚ) ^ d := by
rw [eulerUpper]
push_cast
ring
theorem abs_realBlock_le (d L t : ℕ) (hL : 0 < L) (ht : t ≤ 2 * L) :
|realBlock d L t| ≤ (eulerUpper d : ℝ) * (L : ℝ) ^ d := by
change |((blockPoly d L t : ℚ) : ℝ)| ≤
(eulerUpper d : ℝ) * (L : ℝ) ^ d
norm_cast
simpa only [Nat.cast_pow] using abs_blockPoly_le d L t hL ht
theorem abs_blockPrefix_le (d L r : ℕ) (hL : 0 < L) (hr : r ≤ 2 * L) :
|blockPrefix d L r| ≤
(2 * (L : ℝ)) * ((eulerUpper d : ℝ) * (L : ℝ) ^ d) := by
rw [blockPrefix]
calc
|∑ t ∈ Finset.range r, realBlock d L t| ≤
∑ t ∈ Finset.range r, |realBlock d L t| :=
Finset.abs_sum_le_sum_abs _ _
_ ≤ ∑ _t ∈ Finset.range r,
((eulerUpper d : ℝ) * (L : ℝ) ^ d) := by
apply Finset.sum_le_sum
intro t ht
apply abs_realBlock_le d L t hL
have := Finset.mem_range.mp ht
omega
_ ≤ (2 * (L : ℝ)) * ((eulerUpper d : ℝ) * (L : ℝ) ^ d) := by
simp only [Finset.sum_const, Finset.card_range, nsmul_eq_mul]
apply mul_le_mul_of_nonneg_right
· exact_mod_cast hr
· have hE := eulerUpper_nonneg d
norm_cast at hE
positivity
/-- Uniform amplitude bound for a single positive/negative pair. -/
theorem pairDatum_pointwise_bound (d L : ℕ) (hL : 0 < L) (i : ℤ) :
|pairDatum d L i| ≤
4 * (eulerUpper d : ℝ) * (L : ℝ) ^ (d + 1) := by
have hE : 0 ≤ (eulerUpper d : ℝ) := by
exact_mod_cast eulerUpper_nonneg d
have hbound : 0 ≤ 4 * (eulerUpper d : ℝ) * (L : ℝ) ^ (d + 1) := by
positivity
by_cases hi : 0 ≤ i
· obtain ⟨r, rfl⟩ := Int.eq_ofNat_of_zero_le hi
simp only [pairDatum, liftNat_apply_nat, pairDatumNat_apply]
by_cases h2 : r ≤ 2 * L
· rw [if_pos h2]
have hp := abs_blockPrefix_le d L r hL h2
calc
|blockPrefix d L r| ≤
(2 * (L : ℝ)) * ((eulerUpper d : ℝ) * (L : ℝ) ^ d) := hp
_ ≤ 4 * (eulerUpper d : ℝ) * (L : ℝ) ^ (d + 1) := by
have hleft : 0 ≤
(2 * (L : ℝ)) * ((eulerUpper d : ℝ) * (L : ℝ) ^ d) := by
positivity
calc
(2 * (L : ℝ)) * ((eulerUpper d : ℝ) * (L : ℝ) ^ d) ≤
2 * ((2 * (L : ℝ)) *
((eulerUpper d : ℝ) * (L : ℝ) ^ d)) := by linarith
_ = 4 * (eulerUpper d : ℝ) * (L : ℝ) ^ (d + 1) := by
rw [pow_succ]
ring
· by_cases h4 : r ≤ 4 * L
· rw [if_neg h2, if_pos h4]
have hrsub : r - 2 * L ≤ 2 * L := by omega
have hp1 := abs_blockPrefix_le d L (2 * L) hL (le_refl _)
have hp2 := abs_blockPrefix_le d L (r - 2 * L) hL hrsub
calc
|blockPrefix d L (2 * L) - blockPrefix d L (r - 2 * L)| ≤
|blockPrefix d L (2 * L)| + |blockPrefix d L (r - 2 * L)| :=
abs_sub _ _
_ ≤ 2 * ((2 * (L : ℝ)) *
((eulerUpper d : ℝ) * (L : ℝ) ^ d)) := by linarith
_ = 4 * (eulerUpper d : ℝ) * (L : ℝ) ^ (d + 1) := by
rw [pow_succ]
ring
· simpa [h2, h4] using hbound
· have hineg : i < 0 := lt_of_not_ge hi
simpa [pairDatum, liftNat_apply_of_neg _ hineg] using hbound
theorem camplitude_le_of_pointwise {f : CSeq} {C : ℝ} (hC : 0 ≤ C)
(h : ∀ i, |f i| ≤ C) :
camplitude f ≤ C := by
unfold camplitude
rw [Finset.max'_le_iff]
intro x hx
simp only [Finset.mem_insert, Finset.mem_image] at hx
rcases hx with rfl | ⟨i, hi, rfl⟩
· exact hC
· exact h i
theorem pairDatum_amplitude_bound (d L : ℕ) (hL : 0 < L) :
camplitude (pairDatum d L) ≤
4 * (eulerUpper d : ℝ) * (L : ℝ) ^ (d + 1) := by
apply camplitude_le_of_pointwise
· have hE := eulerUpper_nonneg d
norm_cast at hE
positivity
· exact pairDatum_pointwise_bound d L hL
theorem multiDatum_amplitude_bound (d L P : ℕ) (hL : 0 < L) :
camplitude (multiDatum d L P) ≤
4 * (eulerUpper d : ℝ) * (L : ℝ) ^ (d + 1) := by
calc
camplitude (multiDatum d L P) ≤ camplitude (pairDatum d L) := by
apply camplitude_le_of_pointwise (camplitude_nonneg _)
exact multiDatum_pointwise_le_pair d L P
_ ≤ 4 * (eulerUpper d : ℝ) * (L : ℝ) ^ (d + 1) :=
pairDatum_amplitude_bound d L hL
end ENOTV