gap_zero

formal source

  26
  27/-! ## Basic identities -/
  28
  29@[simp] theorem gap_zero : gap (0 : ℤ) = 0 := by
  30  simp [gap]
  31
  32/-!
  33`gap` can be rewritten as a shifted log-base-φ:
  34
  35  `gap(Z) = log_φ(φ + Z) - 1`
  36
  37for any `Z` with `0 < φ + Z` (in practice all `Z ≥ 0` used in the mass bands).
  38-/
  39theorem gap_eq_log_phi_add_sub_one {Z : ℤ} (hZ : 0 < (phi + (Z : ℝ))) :
  40    gap Z = (Real.log (phi + (Z : ℝ)) / Real.log phi) - 1 := by
  41  have hφpos : 0 < phi := phi_pos
  42  have hφne : (phi : ℝ) ≠ 0 := ne_of_gt hφpos
  43  have hlogφ : Real.log phi ≠ 0 := by
  44    have : (1 : ℝ) < phi := one_lt_phi
  45    exact ne_of_gt (Real.log_pos this)
  46  -- log(1 + Z/φ) = log((φ+Z)/φ) = log(φ+Z) - log(φ)
  47  have h1 : (1 + (Z : ℝ) / phi) = (phi + (Z : ℝ)) / phi := by
  48    field_simp [hφne]
  49  have hpos1 : 0 < (1 + (Z : ℝ) / phi) := by
  50    -- since (φ+Z)/φ > 0
  51    have : 0 < (phi + (Z : ℝ)) / phi := by
  52      exact div_pos hZ hφpos
  53    simpa [h1] using this
  54  calc
  55    gap Z
  56        = Real.log (1 + (Z : ℝ) / phi) / Real.log phi := by rfl
  57    _   = (Real.log ((phi + (Z : ℝ)) / phi)) / Real.log phi := by simp [h1]
  58    _   = (Real.log (phi + (Z : ℝ)) - Real.log phi) / Real.log phi := by
  59            simp [Real.log_div, hZ.ne', hφne]