IndisputableMonolith.ILG.Kernel

declarations in this module (37)

• structure KernelParams L39
• def rsKernelParams L54
• def eightTickKernelParams L64
• def kernel L79
• def kernelAtRefK L83
• lemma kernelAtRefK_eq L86
• theorem kernel_pos L93
• theorem kernel_ge_one L105
• theorem kernel_at_ratio_one_alpha_zero L117
• theorem kernel_eq_one_of_C_zero L127
• theorem kernel_mono_in_a L135
• theorem rsKernelParams_alpha L164
• theorem rsKernelParams_C L168
• theorem eightTickKernelParams_C L172
• theorem kernel_ratio_dimensionless L178
• structure SelfSimilarKernel L185
• theorem alpha_from_self_similarity L194
• def kernel_perturbation L245
• def kernel_background L254
• theorem kernel_background_eq_one L256
• def kernel_with_Hubble L260
• theorem kernel_perturbation_eq_kernel_of_ge L265
• theorem kernel_perturbation_at_IR_floor L274
• theorem kernel_perturbation_pos L282
• theorem kernel_perturbation_ge_one L294
• theorem kernel_perturbation_bounded_above L313
• theorem kernel_with_Hubble_bounded_above L346
• theorem kernel_background_independent_of_params L357
• def mode_partition L367
• theorem mode_partition_eq L370
• theorem mode_partition_homogeneous L378
• def kernel_dynamical_time L395
• theorem kernel_dynamical_time_pos L399
• theorem kernel_dynamical_time_ge_one L411
• theorem kernel_dynamical_time_stationary L426
• structure CausalityBoundsCert L446
• def causalityBoundsCert L470