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)
20noncomputable def spectralGap (k : ℕ) : ℝ := (phi ^ k)⁻¹
proof body
Definition body.
21
used by (10)
From the project-wide theorem graph. These declarations reference this one in their body.
-
asCoreGap
in IndisputableMonolith.NetworkScience.InternetSpectralGap
decl_use
-
InternetSpectralGapCert
in IndisputableMonolith.NetworkScience.InternetSpectralGap
decl_use
-
spectralGap
in IndisputableMonolith.NetworkScience.InternetSpectralGap
decl_use
-
spectralGap_pos
in IndisputableMonolith.NetworkScience.InternetSpectralGap
decl_use
-
spectralGap_ratio
in IndisputableMonolith.NetworkScience.InternetSpectralGap
decl_use
-
spectralGap_strictly_decreasing
in IndisputableMonolith.NetworkScience.InternetSpectralGap
decl_use
-
InternetSpectralGapCert
in IndisputableMonolith.NetworkScience.InternetSpectralGapFromPhiLadder
decl_use
-
spectralGap_k2_val
in IndisputableMonolith.NetworkScience.InternetSpectralGapFromPhiLadder
decl_use
-
spectralGap_pos
in IndisputableMonolith.NetworkScience.InternetSpectralGapFromPhiLadder
decl_use
-
spectralGapRatio
in IndisputableMonolith.NetworkScience.InternetSpectralGapFromPhiLadder
decl_use
depends on (1)
Lean names referenced from this declaration's body.
-
spectralGap
in IndisputableMonolith.NetworkScience.InternetSpectralGap
decl_use