MusicalInterval

formal source

  94
  95/-! ## Musical Interval Structure -/
  96
  97structure MusicalInterval where
  98  ratio : ℝ
  99  ratio_pos : 0 < ratio
 100
 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