Documentation

Carleson.Classical.HilbertKernel

def k (x : ) :
Equations
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
def K (x y : ) :
Equations
Instances For
theorem Hilbert_kernel_conj_symm {x y : } :
K y x = (starRingEnd ) (K x y)
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|)