gapAffineLog

formal source

  39  a * Real.log (1 + x / b) + c
  40
  41/-- Integer specialization of the affine-log family. -/
  42def gapAffineLog (a b c : ℝ) (Z : ℤ) : ℝ :=
  43  gapAffineLogR a b c (Z : ℝ)
  44
  45/-- `φ = 1 + 1/φ`, used to normalize the unit-step condition. -/
  46lemma phi_eq_one_add_inv_phi : phi = 1 + (1 : ℝ) / phi := by
  47  have hphi_ne_zero : phi ≠ 0 := phi_ne_zero
  48  calc
  49    phi = phi ^ 2 / phi := by
  50      field_simp [hphi_ne_zero]
  51    _ = (phi + 1) / phi := by simp [phi_sq_eq]
  52    _ = 1 + (1 : ℝ) / phi := by
  53      field_simp [hphi_ne_zero]
  54
  55/-- Equivalent rewrite of `1 + 1/φ = φ`. -/
  56lemma one_add_inv_phi_eq_phi : 1 + (1 : ℝ) / phi = phi := by
  57  simpa using phi_eq_one_add_inv_phi.symm
  58
  59/-- Log rewrite at the canonical shift argument. -/
  60lemma log_one_add_inv_phi_eq_log_phi : Real.log (1 + phi⁻¹) = Real.log phi := by
  61  have hshift : (1 + phi⁻¹ : ℝ) = phi := by
  62    simpa [one_div] using one_add_inv_phi_eq_phi
  63  simp [hshift]
  64
  65/-- Neutral normalization fixes the additive offset. -/
  66lemma zero_normalization_forces_offset
  67    {a c : ℝ}
  68    (h0 : gapAffineLogR a phi c 0 = 0) :
  69    c = 0 := by
  70  simpa [gapAffineLogR] using h0
  71
  72/-- Unit-step calibration fixes the log scale coefficient. -/