11.4. HardyZeta.FiniteDifferenceCompact
theorem continuous_dslope_sinh : Continuous (dslope Real.sinh 0) := ⊢ Continuous (dslope Real.sinh 0)
⊢ ∀ (x : ℝ), ContinuousAt (dslope Real.sinh 0) x
x:ℝ⊢ ContinuousAt (dslope Real.sinh 0) x
x:ℝhx:x = 0⊢ ContinuousAt (dslope Real.sinh 0) xx:ℝhx:¬x = 0⊢ ContinuousAt (dslope Real.sinh 0) x
x:ℝhx:x = 0⊢ ContinuousAt (dslope Real.sinh 0) x ⊢ ContinuousAt (dslope Real.sinh 0) 0
All goals completed! 🐙
x:ℝhx:¬x = 0⊢ ContinuousAt (dslope Real.sinh 0) x All goals completed! 🐙theorem continuous_dslope_sin : Continuous (dslope Real.sin 0) := ⊢ Continuous (dslope Real.sin 0)
⊢ ∀ (x : ℝ), ContinuousAt (dslope Real.sin 0) x
x:ℝ⊢ ContinuousAt (dslope Real.sin 0) x
x:ℝhx:x = 0⊢ ContinuousAt (dslope Real.sin 0) xx:ℝhx:¬x = 0⊢ ContinuousAt (dslope Real.sin 0) x
x:ℝhx:x = 0⊢ ContinuousAt (dslope Real.sin 0) x ⊢ ContinuousAt (dslope Real.sin 0) 0
All goals completed! 🐙
x:ℝhx:¬x = 0⊢ ContinuousAt (dslope Real.sin 0) x All goals completed! 🐙
/-- Continuous extension at zero step size of P_h(t)/h². -/def extendedDifferenceMultiplier (h t : ℝ) : ℝ :=
4 * ((t / 2 * dslope Real.sinh 0 (h * t / 2)) ^ 2 +
(1 / 4 * dslope Real.sin 0 (h / 4)) ^ 2)theorem extendedDifferenceMultiplier_zero (t : ℝ) :
extendedDifferenceMultiplier 0 t = t ^ 2 + 1 / 4 := t:ℝ⊢ extendedDifferenceMultiplier 0 t = t ^ 2 + 1 / 4
t:ℝ⊢ 4 * ((t / 2) ^ 2 + (4 ^ 2)⁻¹) = t ^ 2 + 4⁻¹
All goals completed! 🐙theorem continuous_extendedDifferenceMultiplier :
Continuous (fun p : ℝ × ℝ ↦ extendedDifferenceMultiplier p.1 p.2) := ⊢ Continuous fun p => extendedDifferenceMultiplier p.1 p.2
hs:Continuous (dslope Real.sinh 0)⊢ Continuous fun p => extendedDifferenceMultiplier p.1 p.2
hs:Continuous (dslope Real.sinh 0)hc:Continuous (dslope Real.sin 0)⊢ Continuous fun p => extendedDifferenceMultiplier p.1 p.2
hs:Continuous (dslope Real.sinh 0)hc:Continuous (dslope Real.sin 0)⊢ Continuous fun p => 4 * ((p.2 / 2 * dslope Real.sinh 0 (p.1 * p.2 / 2)) ^ 2 + (1 / 4 * dslope Real.sin 0 (p.1 / 4)) ^ 2)
All goals completed! 🐙theorem extendedDifferenceMultiplier_eq {h : ℝ} (hh : h ≠ 0) (t : ℝ) :
extendedDifferenceMultiplier h t = differenceMultiplier h t / h ^ 2 := h:ℝhh:h ≠ 0t:ℝ⊢ extendedDifferenceMultiplier h t = differenceMultiplier h t / h ^ 2
h:ℝhh:h ≠ 0t:ℝhs:(h * t / 2 - 0) • dslope Real.sinh 0 (h * t / 2) = Real.sinh (h * t / 2) - Real.sinh 0⊢ extendedDifferenceMultiplier h t = differenceMultiplier h t / h ^ 2
h:ℝhh:h ≠ 0t:ℝhs:(h * t / 2 - 0) • dslope Real.sinh 0 (h * t / 2) = Real.sinh (h * t / 2) - Real.sinh 0hc:(h / 4 - 0) • dslope Real.sin 0 (h / 4) = Real.sin (h / 4) - Real.sin 0⊢ extendedDifferenceMultiplier h t = differenceMultiplier h t / h ^ 2
h:ℝhh:h ≠ 0t:ℝhs:h * t / 2 * dslope Real.sinh 0 (h * t / 2) = Real.sinh (h * t / 2)hc:h / 4 * dslope Real.sin 0 (h / 4) = Real.sin (h / 4)⊢ extendedDifferenceMultiplier h t = differenceMultiplier h t / h ^ 2
h:ℝhh:h ≠ 0t:ℝhs:h * t / 2 * dslope Real.sinh 0 (h * t / 2) = Real.sinh (h * t / 2)hc:h / 4 * dslope Real.sin 0 (h / 4) = Real.sin (h / 4)⊢ extendedDifferenceMultiplier h t =
4 * ((h * t / 2 * dslope Real.sinh 0 (h * t / 2)) ^ 2 + (h / 4 * dslope Real.sin 0 (h / 4)) ^ 2) / h ^ 2
h:ℝhh:h ≠ 0t:ℝhs:h * t / 2 * dslope Real.sinh 0 (h * t / 2) = Real.sinh (h * t / 2)hc:h / 4 * dslope Real.sin 0 (h / 4) = Real.sin (h / 4)⊢ 4 * ((t / 2 * dslope Real.sinh 0 (h * t / 2)) ^ 2 + (1 / 4 * dslope Real.sin 0 (h / 4)) ^ 2) =
4 * ((h * t / 2 * dslope Real.sinh 0 (h * t / 2)) ^ 2 + (h / 4 * dslope Real.sin 0 (h / 4)) ^ 2) / h ^ 2
All goals completed! 🐙
/-- The normalized kernels converge under integration on every compact interval. -/theorem tendsto_integral_differenceKernel_Icc {g : ℝ → ℝ} (hg : Continuous g)
(a c l r : ℝ) (k : ℕ) :
Tendsto (fun h : ℝ ↦ ∫ t in Icc l r,
g t * (differenceMultiplier h t / h ^ 2) ^ k * Real.cosh ((a - c * h) * t))
(𝓝[>] 0) (𝓝 (∫ t in Icc l r, g t * (t ^ 2 + 1 / 4) ^ k * Real.cosh (a * t))) := g:ℝ → ℝhg:Continuous ga:ℝc:ℝl:ℝr:ℝk:ℕ⊢ Tendsto (fun h => ∫ (t : ℝ) in Icc l r, g t * (differenceMultiplier h t / h ^ 2) ^ k * Real.cosh ((a - c * h) * t))
(𝓝[>] 0) (𝓝 (∫ (t : ℝ) in Icc l r, g t * (t ^ 2 + 1 / 4) ^ k * Real.cosh (a * t)))
g:ℝ → ℝhg:Continuous ga:ℝc:ℝl:ℝr:ℝk:ℕhe:Continuous fun p => extendedDifferenceMultiplier p.1 p.2⊢ Tendsto (fun h => ∫ (t : ℝ) in Icc l r, g t * (differenceMultiplier h t / h ^ 2) ^ k * Real.cosh ((a - c * h) * t))
(𝓝[>] 0) (𝓝 (∫ (t : ℝ) in Icc l r, g t * (t ^ 2 + 1 / 4) ^ k * Real.cosh (a * t)))
g:ℝ → ℝhg:Continuous ga:ℝc:ℝl:ℝr:ℝk:ℕhe:Continuous fun p => extendedDifferenceMultiplier p.1 p.2hc:Continuous fun p => g p.2 * extendedDifferenceMultiplier p.1 p.2 ^ k * Real.cosh ((a - c * p.1) * p.2)⊢ Tendsto (fun h => ∫ (t : ℝ) in Icc l r, g t * (differenceMultiplier h t / h ^ 2) ^ k * Real.cosh ((a - c * h) * t))
(𝓝[>] 0) (𝓝 (∫ (t : ℝ) in Icc l r, g t * (t ^ 2 + 1 / 4) ^ k * Real.cosh (a * t)))
g:ℝ → ℝhg:Continuous ga:ℝc:ℝl:ℝr:ℝk:ℕhe:Continuous fun p => extendedDifferenceMultiplier p.1 p.2hc:Continuous fun p => g p.2 * extendedDifferenceMultiplier p.1 p.2 ^ k * Real.cosh ((a - c * p.1) * p.2)hi:Continuous fun x => ∫ (y : ℝ) in Icc l r, g y * extendedDifferenceMultiplier x y ^ k * Real.cosh ((a - c * x) * y)⊢ Tendsto (fun h => ∫ (t : ℝ) in Icc l r, g t * (differenceMultiplier h t / h ^ 2) ^ k * Real.cosh ((a - c * h) * t))
(𝓝[>] 0) (𝓝 (∫ (t : ℝ) in Icc l r, g t * (t ^ 2 + 1 / 4) ^ k * Real.cosh (a * t)))
g:ℝ → ℝhg:Continuous ga:ℝc:ℝl:ℝr:ℝk:ℕhe:Continuous fun p => extendedDifferenceMultiplier p.1 p.2hc:Continuous fun p => g p.2 * extendedDifferenceMultiplier p.1 p.2 ^ k * Real.cosh ((a - c * p.1) * p.2)hi:Continuous fun x => ∫ (y : ℝ) in Icc l r, g y * extendedDifferenceMultiplier x y ^ k * Real.cosh ((a - c * x) * y)hl:Tendsto (fun x => ∫ (y : ℝ) in Icc l r, g y * extendedDifferenceMultiplier x y ^ k * Real.cosh ((a - c * x) * y))
(𝓝[>] 0) (𝓝 (∫ (y : ℝ) in Icc l r, g y * extendedDifferenceMultiplier 0 y ^ k * Real.cosh ((a - c * 0) * y)))⊢ Tendsto (fun h => ∫ (t : ℝ) in Icc l r, g t * (differenceMultiplier h t / h ^ 2) ^ k * Real.cosh ((a - c * h) * t))
(𝓝[>] 0) (𝓝 (∫ (t : ℝ) in Icc l r, g t * (t ^ 2 + 1 / 4) ^ k * Real.cosh (a * t)))
g:ℝ → ℝhg:Continuous ga:ℝc:ℝl:ℝr:ℝk:ℕhe:Continuous fun p => extendedDifferenceMultiplier p.1 p.2hc:Continuous fun p => g p.2 * extendedDifferenceMultiplier p.1 p.2 ^ k * Real.cosh ((a - c * p.1) * p.2)hi:Continuous fun x => ∫ (y : ℝ) in Icc l r, g y * extendedDifferenceMultiplier x y ^ k * Real.cosh ((a - c * x) * y)hl:Tendsto (fun x => ∫ (y : ℝ) in Icc l r, g y * extendedDifferenceMultiplier x y ^ k * Real.cosh ((a - c * x) * y))
(𝓝[>] 0) (𝓝 (∫ (y : ℝ) in Icc l r, g y * (y ^ 2 + 1 / 4) ^ k * Real.cosh (a * y)))⊢ Tendsto (fun h => ∫ (t : ℝ) in Icc l r, g t * (differenceMultiplier h t / h ^ 2) ^ k * Real.cosh ((a - c * h) * t))
(𝓝[>] 0) (𝓝 (∫ (t : ℝ) in Icc l r, g t * (t ^ 2 + 1 / 4) ^ k * Real.cosh (a * t)))
g:ℝ → ℝhg:Continuous ga:ℝc:ℝl:ℝr:ℝk:ℕhe:Continuous fun p => extendedDifferenceMultiplier p.1 p.2hc:Continuous fun p => g p.2 * extendedDifferenceMultiplier p.1 p.2 ^ k * Real.cosh ((a - c * p.1) * p.2)hi:Continuous fun x => ∫ (y : ℝ) in Icc l r, g y * extendedDifferenceMultiplier x y ^ k * Real.cosh ((a - c * x) * y)hl:Tendsto (fun x => ∫ (y : ℝ) in Icc l r, g y * extendedDifferenceMultiplier x y ^ k * Real.cosh ((a - c * x) * y))
(𝓝[>] 0) (𝓝 (∫ (y : ℝ) in Icc l r, g y * (y ^ 2 + 1 / 4) ^ k * Real.cosh (a * y)))⊢ (fun x => ∫ (y : ℝ) in Icc l r, g y * extendedDifferenceMultiplier x y ^ k * Real.cosh ((a - c * x) * y)) =ᶠ[𝓝[>] 0]
fun h => ∫ (t : ℝ) in Icc l r, g t * (differenceMultiplier h t / h ^ 2) ^ k * Real.cosh ((a - c * h) * t)
filter_upwards [self_mem_nhdsWithin] with h g:ℝ → ℝhg:Continuous ga:ℝc:ℝl:ℝr:ℝk:ℕhe:Continuous fun p => extendedDifferenceMultiplier p.1 p.2hc:Continuous fun p => g p.2 * extendedDifferenceMultiplier p.1 p.2 ^ k * Real.cosh ((a - c * p.1) * p.2)hi:Continuous fun x => ∫ (y : ℝ) in Icc l r, g y * extendedDifferenceMultiplier x y ^ k * Real.cosh ((a - c * x) * y)hl:Tendsto (fun x => ∫ (y : ℝ) in Icc l r, g y * extendedDifferenceMultiplier x y ^ k * Real.cosh ((a - c * x) * y))
(𝓝[>] 0) (𝓝 (∫ (y : ℝ) in Icc l r, g y * (y ^ 2 + 1 / 4) ^ k * Real.cosh (a * y)))h:ℝhh:h ∈ Ioi 0⊢ ∫ (y : ℝ) in Icc l r, g y * extendedDifferenceMultiplier h y ^ k * Real.cosh ((a - c * h) * y) =
∫ (t : ℝ) in Icc l r, g t * (differenceMultiplier h t / h ^ 2) ^ k * Real.cosh ((a - c * h) * t)
g:ℝ → ℝhg:Continuous ga:ℝc:ℝl:ℝr:ℝk:ℕhe:Continuous fun p => extendedDifferenceMultiplier p.1 p.2hc:Continuous fun p => g p.2 * extendedDifferenceMultiplier p.1 p.2 ^ k * Real.cosh ((a - c * p.1) * p.2)hi:Continuous fun x => ∫ (y : ℝ) in Icc l r, g y * extendedDifferenceMultiplier x y ^ k * Real.cosh ((a - c * x) * y)hl:Tendsto (fun x => ∫ (y : ℝ) in Icc l r, g y * extendedDifferenceMultiplier x y ^ k * Real.cosh ((a - c * x) * y))
(𝓝[>] 0) (𝓝 (∫ (y : ℝ) in Icc l r, g y * (y ^ 2 + 1 / 4) ^ k * Real.cosh (a * y)))h:ℝhh:h ∈ Ioi 0⊢ EqOn (fun x => g x * extendedDifferenceMultiplier h x ^ k * Real.cosh ((a - c * h) * x))
(fun x => g x * (differenceMultiplier h x / h ^ 2) ^ k * Real.cosh ((a - c * h) * x)) (Icc l r)
g:ℝ → ℝhg:Continuous ga:ℝc:ℝl:ℝr:ℝk:ℕhe:Continuous fun p => extendedDifferenceMultiplier p.1 p.2hc:Continuous fun p => g p.2 * extendedDifferenceMultiplier p.1 p.2 ^ k * Real.cosh ((a - c * p.1) * p.2)hi:Continuous fun x => ∫ (y : ℝ) in Icc l r, g y * extendedDifferenceMultiplier x y ^ k * Real.cosh ((a - c * x) * y)hl:Tendsto (fun x => ∫ (y : ℝ) in Icc l r, g y * extendedDifferenceMultiplier x y ^ k * Real.cosh ((a - c * x) * y))
(𝓝[>] 0) (𝓝 (∫ (y : ℝ) in Icc l r, g y * (y ^ 2 + 1 / 4) ^ k * Real.cosh (a * y)))h:ℝhh:h ∈ Ioi 0t:ℝa✝:t ∈ Icc l r⊢ (fun x => g x * extendedDifferenceMultiplier h x ^ k * Real.cosh ((a - c * h) * x)) t =
(fun x => g x * (differenceMultiplier h x / h ^ 2) ^ k * Real.cosh ((a - c * h) * x)) t
g:ℝ → ℝhg:Continuous ga:ℝc:ℝl:ℝr:ℝk:ℕhe:Continuous fun p => extendedDifferenceMultiplier p.1 p.2hc:Continuous fun p => g p.2 * extendedDifferenceMultiplier p.1 p.2 ^ k * Real.cosh ((a - c * p.1) * p.2)hi:Continuous fun x => ∫ (y : ℝ) in Icc l r, g y * extendedDifferenceMultiplier x y ^ k * Real.cosh ((a - c * x) * y)hl:Tendsto (fun x => ∫ (y : ℝ) in Icc l r, g y * extendedDifferenceMultiplier x y ^ k * Real.cosh ((a - c * x) * y))
(𝓝[>] 0) (𝓝 (∫ (y : ℝ) in Icc l r, g y * (y ^ 2 + 1 / 4) ^ k * Real.cosh (a * y)))h:ℝhh:h ∈ Ioi 0t:ℝa✝:t ∈ Icc l r⊢ g t * extendedDifferenceMultiplier h t ^ k * Real.cosh ((a - c * h) * t) =
g t * (differenceMultiplier h t / h ^ 2) ^ k * Real.cosh ((a - c * h) * t)
All goals completed! 🐙