noncomputable def k (x : ℝ) : ℂ

Equations

• k x = ↑(max (1 - |x|) 0) / (1 - Complex.exp (Complex.I * ↑x))

theorem k_of_neg_eq_conj_k {x : ℝ} : k (-x) = (starRingEnd ℂ) (k x)

theorem k_of_abs_le_one {x : ℝ} (abs_le_one : |x| ≤ 1) : k x = (1 - ↑|x|) / (1 - Complex.exp (Complex.I * ↑x))

theorem k_of_one_le_abs {x : ℝ} (abs_le_one : 1 ≤ |x|) : k x = 0

theorem k_measurable : Measurable k

noncomputable def K : ℝ → ℝ → ℂ

Equations

• K x y = k (x - y)

theorem K_def : K = fun (x y : ℝ) => k (x - y)

theorem Hilbert_kernel_conj_symm {x y : ℝ} : K y x = (starRingEnd ℂ) (K x y)

theorem Hilbert_kernel_measurable : Measurable (Function.uncurry K)

theorem Hilbert_kernel_bound {x y : ℝ} : ‖K x y‖ ≤ 2 ^ 2 / (2 * |x - y|)

theorem Hilbert_kernel_regularity_main_part {y y' : ℝ} (yy'nonneg : 0 ≤ y ∧ 0 ≤ y') (ypos : 0 < y) (y2ley' : y / 2 ≤ y') (hy : y ≤ 1) (hy' : y' ≤ 1) : ‖k (-y) - k (-y')‖ ≤ 2 ^ 6 * (1 / |y|) * (|y - y'| / |y|)

theorem Hilbert_kernel_regularity {x y y' : ℝ} : 2 * |y - y'| ≤ |x - y| → ‖K x y - K x y'‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)