`twoPowZ_ofNat`

proved

show as: view math explainer →

module: IndisputableMonolith.RecogSpec.Scales
domain: RecogSpec
line: 42 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.RecogSpec.Scales on GitHub at line 42.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

twoPowZ IndisputableMonolith.RecogSpec.Scales

formal source

  39  else 1 / ((2 : ℝ) ^ (Int.toNat (-k)))
  40
  41@[simp] lemma twoPowZ_zero : twoPowZ 0 = 1 := by simp [twoPowZ]
  42@[simp] lemma twoPowZ_ofNat (k : Nat) : twoPowZ (Int.ofNat k) = (2 : ℝ) ^ k := by simp [twoPowZ]
  43@[simp] lemma twoPowZ_negSucc (k : Nat) : twoPowZ (Int.negSucc k) = 1 / ((2 : ℝ) ^ k.succ) := by
  44  simp [twoPowZ]
  45
  46/-- φ-power wrapper. -/
  47noncomputable def PhiPow (x : ℝ) : ℝ := Real.exp (Real.log (Constants.phi) * x)
  48
  49lemma PhiPow_add (x y : ℝ) : PhiPow (x + y) = PhiPow x * PhiPow y := by
  50  unfold PhiPow
  51  have hx : Real.log (Constants.phi) * (x + y)
  52        = Real.log (Constants.phi) * x + Real.log (Constants.phi) * y := by
  53    ring
  54  simp [hx, Real.exp_add]
  55
  56lemma PhiPow_sub (x y : ℝ) : PhiPow (x - y) = PhiPow x / PhiPow y := by
  57  unfold PhiPow
  58  have hx : Real.log (Constants.phi) * (x - y)
  59        = Real.log (Constants.phi) * x + Real.log (Constants.phi) * (-y) := by
  60    ring
  61  calc
  62    Real.exp (Real.log (Constants.phi) * (x - y))
  63        = Real.exp (Real.log (Constants.phi) * x + Real.log (Constants.phi) * (-y)) := by
  64              simp [hx]
  65    _   = Real.exp (Real.log (Constants.phi) * x)
  66            * Real.exp (Real.log (Constants.phi) * (-y)) := by
  67              simp [Real.exp_add]
  68    _   = Real.exp (Real.log (Constants.phi) * x)
  69            * (Real.exp (Real.log (Constants.phi) * y))⁻¹ := by
  70              simp [Real.exp_neg]
  71    _   = Real.exp (Real.log (Constants.phi) * x)
  72            / Real.exp (Real.log (Constants.phi) * y) := by

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.