2607.19283v1 / ENOTV/Junction.lean

all files

import ENOTV.Endpoint

/-!
# Scale-free Euler junctions

At an alternating join, the second block differs from the polynomial
continuation of the first by the truncated monomial `-2 x^d`.  Hence its
`(d+1)`-st difference is independent of the block length.
-/

noncomputable section

open Polynomial

namespace ENOTV

def junctionProfile (d L : ℕ) (x : ℚ) : ℚ :=
  if x ≤ 0 then blockPoly d L (2 * L + x) else -blockPoly d L x

def junctionCorrection (d : ℕ) (x : ℚ) : ℚ :=
  if x ≤ 0 then 0 else -2 * x ^ d

theorem junctionProfile_eq (d L : ℕ) (hL : 0 < L) (x : ℚ) :
    junctionProfile d L x =
      (blockPolynomial d L).eval (2 * L + x) + junctionCorrection d x := by
  by_cases hx : x ≤ 0
  · simp [junctionProfile, junctionCorrection, hx, blockPolynomial_eval]
  · have hid := blockPoly_matching d L hL x
    simp only [junctionProfile, junctionCorrection, if_neg hx,
      blockPolynomial_eval]
    linarith

def shiftedBlockPolynomial (d L : ℕ) : ℚ[X] :=
  (blockPolynomial d L).comp (X + C (2 * L : ℚ))

theorem shiftedBlockPolynomial_eval (d L : ℕ) (x : ℚ) :
    (shiftedBlockPolynomial d L).eval x =
      (blockPolynomial d L).eval (2 * L + x) := by
  simp [shiftedBlockPolynomial, add_comm]

theorem shiftedBlockPolynomial_natDegree_le (d L : ℕ) :
    (shiftedBlockPolynomial d L).natDegree ≤ d := by
  rw [shiftedBlockPolynomial, Polynomial.natDegree_comp,
    Polynomial.natDegree_X_add_C, mul_one]
  exact blockPolynomial_natDegree_le d L

theorem shiftedBlockPolynomial_high_difference (d L : ℕ) :
    (fwdDiff (1 : ℚ))^[d + 1] (shiftedBlockPolynomial d L).eval = 0 := by
  apply Polynomial.fwdDiff_iter_eq_zero_of_degree_lt
  exact (shiftedBlockPolynomial_natDegree_le d L).trans_lt (Nat.lt_succ_self d)

theorem junction_high_difference_eq (d L : ℕ) (hL : 0 < L) (x : ℚ) :
    (fwdDiff (1 : ℚ))^[d + 1] (junctionProfile d L) x =
      (fwdDiff (1 : ℚ))^[d + 1] (junctionCorrection d) x := by
  have hfun : junctionProfile d L =
      (shiftedBlockPolynomial d L).eval + junctionCorrection d := by
    funext y
    rw [Pi.add_apply, shiftedBlockPolynomial_eval, junctionProfile_eq d L hL]
  rw [hfun, fwdDiff_iter_add, shiftedBlockPolynomial_high_difference]
  simp

/-- A finite, explicit degree-dependent bound for all offsets whose
`(d+1)`-point stencil crosses a junction. -/
def junctionUpper (d : ℕ) : ℚ :=
  Finset.sup' (Finset.Icc (-(d + 1 : ℤ)) 0)
    (by simp)
    (fun s : ℤ =>
      |(fwdDiff (1 : ℚ))^[d + 1] (junctionCorrection d) s|)

theorem junctionUpper_nonneg (d : ℕ) : 0 ≤ junctionUpper d := by
  apply le_trans
    (abs_nonneg ((fwdDiff (1 : ℚ))^[d + 1] (junctionCorrection d) 0))
  unfold junctionUpper
  exact Finset.le_sup'
    (f := fun s : ℤ =>
      |(fwdDiff (1 : ℚ))^[d + 1] (junctionCorrection d) (s : ℚ)|)
    (show (0 : ℤ) ∈ Finset.Icc (-(d + 1 : ℤ)) 0 by simp)

theorem junction_difference_le (d L : ℕ) (hL : 0 < L) (s : ℤ)
    (hs0 : -(d + 1 : ℤ) ≤ s) (hs1 : s ≤ 0) :
    |(fwdDiff (1 : ℚ))^[d + 1] (junctionProfile d L) s| ≤
      junctionUpper d := by
  rw [junction_high_difference_eq d L hL]
  unfold junctionUpper
  exact Finset.le_sup'
    (f := fun s : ℤ =>
      |(fwdDiff (1 : ℚ))^[d + 1] (junctionCorrection d) (s : ℚ)|)
    (show s ∈ Finset.Icc (-(d + 1 : ℤ)) 0 by
      simp only [Finset.mem_Icc]
      constructor <;> omega)

end ENOTV