def
definition
unisonInterval
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.MusicTheory.HarmonicModes on GitHub at line 104.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
101noncomputable def MusicalInterval.jcost (i : MusicalInterval) : ℝ :=
102 Jcost i.ratio
103
104noncomputable def unisonInterval : MusicalInterval :=
105 ⟨1, by norm_num⟩
106
107noncomputable def octaveInterval : MusicalInterval :=
108 ⟨octave, octave_pos⟩
109
110noncomputable def fifthInterval : MusicalInterval :=
111 ⟨fifth, fifth_pos⟩
112
113noncomputable def fourthInterval : MusicalInterval :=
114 ⟨fourth, fourth_pos⟩
115
116noncomputable def majorThirdInterval : MusicalInterval :=
117 ⟨majorThird, majorThird_pos⟩
118
119noncomputable def minorThirdInterval : MusicalInterval :=
120 ⟨minorThird, minorThird_pos⟩
121
122noncomputable def tritoneInterval : MusicalInterval :=
123 ⟨tritone, tritone_pos⟩
124
125/-! ## J-Cost of Standard Intervals -/
126
127theorem unison_jcost : Jcost (1 : ℝ) = 0 := Jcost_unit0
128
129theorem octave_jcost : Jcost octave = 1 / 4 := by
130 simp [Jcost]; ring
131
132theorem fifth_jcost : Jcost fifth = 1 / 12 := by
133 simp [Jcost]; ring
134