 133  ring
 134
 135/-- **Master certificate for the causality-bound Poisson layer.** -/
 136structure CausalityBoundsPoissonCert where
 137  background_indep : ∀ (P : KernelParams) (a ρ_bar : ℝ),
 138                      poisson_operator_full P 0 0 a ρ_bar 0
 139                        = poisson_operator_background a ρ_bar
 140  perturbation_homogeneous : ∀ (P : KernelParams) (k_min k a : ℝ),
 141                              poisson_operator_perturbation P k_min k a 0 = 0
 142  full_homogeneous : ∀ (P : KernelParams) (k_min k a ρ_bar : ℝ),
 143                      poisson_operator_full P k_min k a ρ_bar 0
 144                        = poisson_operator_background a ρ_bar
 145
 146noncomputable def causalityBoundsPoissonCert : CausalityBoundsPoissonCert where
 147  background_indep := poisson_background_independent_of_kernel
 148  perturbation_homogeneous := poisson_operator_perturbation_homogeneous
 149  full_homogeneous := poisson_operator_full_homogeneous
 150
 151end ILG
 152end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.