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)
58theorem constant_kernel_eq_one (z z0 : ℝ) :
59 kernel KernelFamily.constant_kernel z z0 = 1 := rfl
proof body
Term-mode proof.
60
61/-- The 1/(1+z) kernel is positive for `z > -1`. -/
depends on (8)
Lean names referenced from this declaration's body.
-
kernel
in IndisputableMonolith.Cosmology.BITKernelFamilies
decl_use
-
KernelFamily
in IndisputableMonolith.Cosmology.BITKernelFamilies
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
kernel
in IndisputableMonolith.ILG.Kernel
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use