`causalityBoundsPoissonCert`

definition

show as: view math explainer →

module: IndisputableMonolith.ILG.PoissonKernel
domain: ILG
line: 146 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.ILG.PoissonKernel on GitHub at line 146.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 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.