theorem proved term proof

`bandwidth_pos`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  93theorem bandwidth_pos {A : ℝ} (hA : 0 < A) : 0 < bandwidth A :=

Term-mode proof.

  94  div_pos hA bandwidth_denom_pos
  95
  96/-- Alias for bandwidth_pos. -/

From the project-wide theorem graph. These declarations reference this one in their body.

BernsteinBound in IndisputableMonolith.Analysis.BernsteinInequality decl_use
bernstein_bound_pos in IndisputableMonolith.Analysis.BernsteinInequality decl_use
criticalBand_implies_subcritical in IndisputableMonolith.Unification.CriticalRecognitionLoading decl_use
loadRatio_pos in IndisputableMonolith.Unification.CriticalRecognitionLoading decl_use
bandwidth_pos' in IndisputableMonolith.Unification.RecognitionBandwidth decl_use

Lean names referenced from this declaration's body.

A in IndisputableMonolith.Foundation.IntegrationGap decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
bandwidth in IndisputableMonolith.Unification.RecognitionBandwidth decl_use
bandwidth_denom_pos in IndisputableMonolith.Unification.RecognitionBandwidth decl_use