English
There is a robust StrongFEPair connecting oddKernel and sinKernel: a functional equation structure with f = ofReal ∘ oddKernel a and g = ofReal ∘ sinKernel a, together with analytic and growth data.
Русский
Существует устойчивое пары функциональных уравнений, связывающая oddKernel и sinKernel: структура функционального уравнения с f = ofReal ∘ oddKernel a и g = ofReal ∘ sinKernel a, вместе с аналитическими и ростовыми данными.
LaTeX
$$$$ \text{There exists a StrongFEPair } (f,g) \text{ with } f=\operatorname{ofReal}\circ\operatorname{oddKernel}a, \ g=\operatorname{ofReal}\circ\operatorname{sinKernel}a, \ k=\tfrac{3}{2}, \varepsilon=1, \ f_0=g_0=0, \ \text{and appropriate top/bounds conditions hold.} $$$$
Lean4
/-- A `StrongFEPair` structure with `f = oddKernel a` and `g = sinKernel a`. -/
@[simps]
def hurwitzOddFEPair (a : UnitAddCircle) : StrongFEPair ℂ
where
f := ofReal ∘ oddKernel a
g := ofReal ∘ sinKernel a
hf_int := (continuous_ofReal.comp_continuousOn (continuousOn_oddKernel a)).locallyIntegrableOn measurableSet_Ioi
hg_int := (continuous_ofReal.comp_continuousOn (continuousOn_sinKernel a)).locallyIntegrableOn measurableSet_Ioi
k := 3 / 2
hk := by norm_num
ε := 1
hε := one_ne_zero
f₀ := 0
hf₀ := rfl
g₀ := 0
hg₀ := rfl
hf_top
r := by
let ⟨v, hv, hv'⟩ := isBigO_atTop_oddKernel a
rw [← isBigO_norm_left] at hv' ⊢
simpa using hv'.trans (isLittleO_exp_neg_mul_rpow_atTop hv _).isBigO
hg_top
r := by
let ⟨v, hv, hv'⟩ := isBigO_atTop_sinKernel a
rw [← isBigO_norm_left] at hv' ⊢
simpa using hv'.trans (isLittleO_exp_neg_mul_rpow_atTop hv _).isBigO
h_feq x hx := by simp [← ofReal_mul, oddKernel_functional_equation a, inv_rpow (le_of_lt hx)]
