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)
116structure VoiceForcingConditions where
117 jbar : ℝ
118 jbar_below_threshold : jbar < voiceThreshold
119 jbar_nonneg : 0 ≤ jbar
120 rhat_active : Bool
121 snr_above_one : Bool
122 fs_readout : Bool
123
124/-- Under voice forcing conditions, voice quality is positive. -/
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (5)
Lean names referenced from this declaration's body.
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
voiceThreshold
in IndisputableMonolith.Foundation.VoiceForcing
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use