IndisputableMonolith.Cosmology.BITKernelFamilies

declarations in this module (14)

• inductive KernelFamily L30
• def name L38
• def kernel L46
• theorem kernel_at_zero L53
• theorem constant_kernel_eq_one L58
• theorem inv_one_plus_z_pos L62
• theorem exp_kernel_pos L68
• def delta_w0_max L74
• theorem delta_w0_max_pos L76
• theorem delta_w0_max_lt_one L81
• def w_eff L87
• theorem w_eff_at_zero L91
• structure BITKernelFamiliesCert L100
• def bitKernelFamiliesCert L112