← all areas

Namespace Real 6 theorems

• Properties of Poitou's kernel e^{-11x^2/100}/cosh(x/2) Real.poitouKernel_admissible_and_archBound 0 below · cited by 1 · depth 11
• Poisson summation on ℝᵈ for the lattice ℤᵈ Real.tsum_comp_add_intCast_eq_tsum_integral_mul_cexp 0 below · cited by 1 · depth 30
• Quadratic decay of a compactly supported C^{2r} function and its Fourier transform Real.norm_le_and_norm_integral_cexp_sum_mul_le_mul_prod_inv_one_add_abs_sq_of_contDiff 0 below · cited by 3 · depth 33
• Absolute value of 1-(± e^X)⁻¹ in exponential coordinates Real.abs_one_sub_exp_inv_eq_exp_neg_mul_abs_one_sub_exp_and_contDiff 0 below · cited by 1 · depth 35
• Quadratic decay of g and ̂ g for a C² function with one corner Real.norm_le_and_norm_integral_cexp_mul_le_mul_inv_one_add_abs_sq_of_piecewise_contDiff_two 0 below · cited by 1 · depth 36
• Derivative bounds for the germ slog s of a positive definite binary form Real.exists_forall_norm_pow_mul_norm_iteratedFDeriv_mul_log_quadratic_le 0 below · cited by 1 · depth 37