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)
128structure RecoveredComplexMellinBridge where
129 analytic_substrate : Foundation.LogicComplexCompat.LogicComplexAnalyticSubstrateCert
130 kernel : ℝ → ℝ
131 mellin_pkg : MellinAdmissibleKernel kernel
132 reflection : ∀ s : ℝ, mellin_pkg.M s = mellin_pkg.M (mellinReflect s)
133
134/-- Any admissible kernel over the recovered complex analytic substrate carries
135the Mellin reflection symmetry. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (8)
Lean names referenced from this declaration's body.
-
kernel
in IndisputableMonolith.Cosmology.BITKernelFamilies
decl_use
-
LogicComplexAnalyticSubstrateCert
in IndisputableMonolith.Foundation.LogicComplexCompat
decl_use
-
kernel
in IndisputableMonolith.ILG.Kernel
decl_use
-
admissible
in IndisputableMonolith.Information.Thermodynamics
decl_use
-
MellinAdmissibleKernel
in IndisputableMonolith.NumberTheory.MellinTransform
decl_use
-
mellinReflect
in IndisputableMonolith.NumberTheory.MellinTransform
decl_use
-
M
in IndisputableMonolith.Recognition
decl_use
-
M
in IndisputableMonolith.Recognition.Cycle3
decl_use