def
definition
def or abbrev
schumannMeasured
show as:
view Lean formalization →
formal statement (Lean)
99def schumannMeasured : Fin 5 → ℝ
100 | ⟨0, _⟩ => 7.83
101 | ⟨1, _⟩ => 14.3
102 | ⟨2, _⟩ => 20.8
103 | ⟨3, _⟩ => 27.3
104 | ⟨4, _⟩ => 33.8
105
106/-! ## Part III: Coefficient Reduction
107
108Reduce schumannRS at each harmonic number to a clean φ-expression. -/
109