Linear delay equations with unit delay

For continuous k y₀ : ℝ → ℝ, y = Delay.sol k y₀ (defined in IwaniecLinearSieve.Definitions) is the continuous function with

• y s = y₀ s for s ≤ 3,
• y s = y₀ 3 + ∫ x in 3..s, k x * y (x - 1) for s ≥ 3,

so that y' s = k s * y (s - 1) for s > 3. This is the shape of the equations defining Iwaniec's functions 𝔐, 𝔚 in [I71, §3].

We also record a "first crossing" principle used for the comparison arguments of [I71, §3].

theorem IwaniecLinearSieve.Delay.step_of_le {k y₀ y : ℝ → ℝ} {s : ℝ} (hs : s ≤ 3) : step k y₀ y s = y₀ s

theorem IwaniecLinearSieve.Delay.step_of_ge {k y₀ y : ℝ → ℝ} {s : ℝ} (hs : 3 ≤ s) : step k y₀ y s = y₀ 3 + ∫ (x : ℝ) in 3..s, k x * y (x - 1)

theorem IwaniecLinearSieve.Delay.step_congr {k y₀ y y' : ℝ → ℝ} {m : ℝ} (h : ∀ x ≤ m, y x = y' x) {s : ℝ} (hs : s ≤ m + 1) : step k y₀ y s = step k y₀ y' s

step only looks one unit back.

theorem IwaniecLinearSieve.Delay.iter_succ_eq {k y₀ : ℝ → ℝ} (n : ℕ) {s : ℝ} (hs : s ≤ ↑n + 3) : iter k y₀ (n + 1) s = iter k y₀ n s

theorem IwaniecLinearSieve.Delay.iter_add_eq {k y₀ : ℝ → ℝ} (n j : ℕ) {s : ℝ} (hs : s ≤ ↑n + 3) : iter k y₀ (n + j) s = iter k y₀ n s

theorem IwaniecLinearSieve.Delay.iter_eq_of_le {k y₀ : ℝ → ℝ} {m n : ℕ} (hmn : m ≤ n) {s : ℝ} (hs : s ≤ ↑m + 3) : iter k y₀ n s = iter k y₀ m s

theorem IwaniecLinearSieve.Delay.sol_eq_iter {k y₀ : ℝ → ℝ} {n : ℕ} {s : ℝ} (hs : s ≤ ↑n + 3) : sol k y₀ s = iter k y₀ n s

theorem IwaniecLinearSieve.Delay.sol_eq_step {k y₀ : ℝ → ℝ} (s : ℝ) : sol k y₀ s = step k y₀ (sol k y₀) s

sol is a fixed point of step.

theorem IwaniecLinearSieve.Delay.sol_of_le {k y₀ : ℝ → ℝ} {s : ℝ} (hs : s ≤ 3) : sol k y₀ s = y₀ s

theorem IwaniecLinearSieve.Delay.sol_of_ge {k y₀ : ℝ → ℝ} {s : ℝ} (hs : 3 ≤ s) : sol k y₀ s = y₀ 3 + ∫ (x : ℝ) in 3..s, k x * sol k y₀ (x - 1)

theorem IwaniecLinearSieve.Delay.continuous_step {k y₀ : ℝ → ℝ} (hk : Continuous k) (hy₀ : Continuous y₀) {y : ℝ → ℝ} (hy : Continuous y) : Continuous (step k y₀ y)

theorem IwaniecLinearSieve.Delay.continuous_iter {k y₀ : ℝ → ℝ} (hk : Continuous k) (hy₀ : Continuous y₀) (n : ℕ) : Continuous (iter k y₀ n)

theorem IwaniecLinearSieve.Delay.continuous_sol {k y₀ : ℝ → ℝ} (hk : Continuous k) (hy₀ : Continuous y₀) : Continuous (sol k y₀)

theorem IwaniecLinearSieve.Delay.hasDerivAt_primitive {k y₀ : ℝ → ℝ} (hk : Continuous k) (hy₀ : Continuous y₀) (s : ℝ) : HasDerivAt (fun (t : ℝ) => y₀ 3 + ∫ (x : ℝ) in 3..t, k x * sol k y₀ (x - 1)) (k s * sol k y₀ (s - 1)) s

For s ≥ 3, sol agrees with y₀ 3 + ∫_3^s k x y(x-1) dx, a function with derivative k s * y (s - 1) everywhere.

theorem IwaniecLinearSieve.Delay.hasDerivAt_sol {k y₀ : ℝ → ℝ} (hk : Continuous k) (hy₀ : Continuous y₀) {s : ℝ} (hs : 3 < s) : HasDerivAt (sol k y₀) (k s * sol k y₀ (s - 1)) s

theorem IwaniecLinearSieve.Delay.hasDerivWithinAt_sol_Ici {k y₀ : ℝ → ℝ} (hk : Continuous k) (hy₀ : Continuous y₀) {s : ℝ} (hs : 3 ≤ s) : HasDerivWithinAt (sol k y₀) (k s * sol k y₀ (s - 1)) (Set.Ici s) s

theorem IwaniecLinearSieve.pos_of_first_crossing {f : ℝ → ℝ} {a₀ a : ℝ} (hf : ContinuousOn f (Set.Ici a)) (hinit : ∀ x ∈ Set.Icc a₀ a, 0 ≤ f x) (ha : 0 < f a) (hstep : ∀ s > a, (∀ x ∈ Set.Icc a₀ s, 0 ≤ f x) → (∀ x ∈ Set.Ico a s, 0 < f x) → 0 < f s) (s : ℝ) : a ≤ s → 0 < f s

First-crossing principle. If f is continuous on [a, ∞), nonnegative on [a₀, a], positive at a, and f s > 0 whenever s > a and f ≥ 0 on [a₀, s], f > 0 on [a, s), then f > 0 on [a, ∞).