peakFrequency

formal source

  34theorem omega_0_pos : 0 < omega_0 := by unfold omega_0; norm_num
  35
  36/-- Peak frequency at φ-rung `k`. -/
  37def peakFrequency (k : ℕ) : ℝ := omega_0 * phi ^ k
  38
  39theorem peakFrequency_pos (k : ℕ) : 0 < peakFrequency k :=
  40  mul_pos omega_0_pos (pow_pos phi_pos _)
  41
  42theorem peakFrequency_zero : peakFrequency 0 = omega_0 := by
  43  unfold peakFrequency; simp
  44
  45theorem peakFrequency_succ (k : ℕ) :
  46    peakFrequency (k + 1) = peakFrequency k * phi := by
  47  unfold peakFrequency; rw [pow_succ]; ring
  48
  49theorem peakFrequency_strict_mono {k₁ k₂ : ℕ} (h : k₁ < k₂) :
  50    peakFrequency k₁ < peakFrequency k₂ := by
  51  unfold peakFrequency
  52  exact (mul_lt_mul_iff_of_pos_left omega_0_pos).mpr
  53    (pow_lt_pow_right₀ one_lt_phi h)
  54
  55/-! ## §2. Named ore classes -/
  56
  57inductive OreClass where
  58  | silicate     -- k=0
  59  | carbonate    -- k=1
  60  | oxide        -- k=2
  61  | sulfide      -- k=3
  62  | metallic_Fe  -- k=4
  63  | metallic_Ni  -- k=5
  64  | platinoid    -- k=6
  65  deriving DecidableEq, Repr
  66
  67namespace OreClass