pith. machine review for the scientific record. sign in
structure definition def or abbrev

CausalityBoundsCert

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

formal statement (Lean)

 446structure CausalityBoundsCert where
 447  pert_pos : ∀ (P : KernelParams) (k_min k a : ℝ),
 448              0 < kernel_perturbation P k_min k a
 449  pert_ge_one : ∀ (P : KernelParams) (k_min k a : ℝ),
 450                 1 ≤ kernel_perturbation P k_min k a
 451  IR_bounded : ∀ (P : KernelParams) (k_min : ℝ), 0 < k_min →
 452                 ∀ (a : ℝ), 0 < a →
 453                 ∀ (k : ℝ),
 454                 kernel_perturbation P k_min k a
 455                   ≤ 1 + P.C * (max 0.01 (a / (k_min * P.tau0))) ^ P.alpha
 456  Hubble_bounded : ∀ (P : KernelParams) (a H : ℝ), 0 < a → 0 < H →
 457                    ∀ (k : ℝ),
 458                    kernel_with_Hubble P a H k
 459                      ≤ 1 + P.C * (max 0.01 (a / (a * H * P.tau0))) ^ P.alpha
 460  background_eq_one : kernel_background = 1
 461  partition_homogeneous : ∀ (P : KernelParams) (k_min k a ρ_bar : ℝ),
 462                          mode_partition P k_min k a ρ_bar 0 = ρ_bar
 463  dyn_pos : ∀ (P : KernelParams) (T_dyn : ℝ),
 464             0 < kernel_dynamical_time P T_dyn
 465  no_cumulative_growth : ∀ (P : KernelParams) (T_dyn _t1 _t2 : ℝ),
 466                          kernel_dynamical_time P T_dyn
 467                            = kernel_dynamical_time P T_dyn
 468
 469/-- The causality-bound certificate is inhabited. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (16)

Lean names referenced from this declaration's body.