English
The Hurwitz Even Fourier–Euler pair is a structured object (f,g) constructed from evenKernel and cosKernel that satisfies a collection of integrability, topological, and decay properties, encoding the functional equation between the two kernels.
Русский
Объект Hurwitz Even FE-пара — это структурированный элемент (f,g), построенный из evenKernel и cosKernel, удовлетворяющий набору интегрируемости, топологических и распадных свойств, кодирующий функциональное уравнение между двумя ядрами.
LaTeX
$$$$ \\text{There exists a WeakFEPair } (f,g) \\text{ with } f = \\mathrm{ofReal} \\circ \\mathrm{evenKernel}(a), \\ g = \\mathrm{ofReal} \\circ \\mathrm{cosKernel}(a), \\text{ satisfying the listed topological and decay properties.} $$$$
Lean4
/-- A `WeakFEPair` structure with `f = evenKernel a` and `g = cosKernel a`. -/
def hurwitzEvenFEPair (a : UnitAddCircle) : WeakFEPair ℂ
where
f := ofReal ∘ evenKernel a
g := ofReal ∘ cosKernel a
hf_int := (continuous_ofReal.comp_continuousOn (continuousOn_evenKernel a)).locallyIntegrableOn measurableSet_Ioi
hg_int := (continuous_ofReal.comp_continuousOn (continuousOn_cosKernel a)).locallyIntegrableOn measurableSet_Ioi
k := 1 / 2
hk := one_half_pos
ε := 1
hε := one_ne_zero
f₀ := if a = 0 then 1 else 0
hf_top
r := by
let ⟨v, hv, hv'⟩ := isBigO_atTop_evenKernel_sub a
rw [← isBigO_norm_left] at hv' ⊢
conv at hv' => enter [2, x]; rw [← norm_real, ofReal_sub, apply_ite ((↑) : ℝ → ℂ), ofReal_one, ofReal_zero]
exact hv'.trans (isLittleO_exp_neg_mul_rpow_atTop hv _).isBigO
g₀ := 1
hg_top
r := by
obtain ⟨p, hp, hp'⟩ := isBigO_atTop_cosKernel_sub a
simpa using isBigO_ofReal_left.mpr <| hp'.trans (isLittleO_exp_neg_mul_rpow_atTop hp r).isBigO
h_feq x hx := by simp [← ofReal_mul, evenKernel_functional_equation, inv_rpow (le_of_lt hx)]
