module module

`IndisputableMonolith.Gravity.CausalKernelChain`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.CaldeiraLeggett module_import

declarations in this module (10)

theorem integral_exp_smul_neg L41
lemma norm_exp_neg_mul_ofReal L91
theorem tendsto_exp_neg_mul_ofReal_atTop L99
def transfer_function_complex L127
def debye_kernel L136
def kernel_response_trunc L145
def laplaceExponent L164
theorem kernel_response_limit L169
theorem transfer_function_eq_one_plus_kernel L257
theorem response_function_is_real_part L264