B_of

formal source

   7/-! Binary scales and φ-exponential wrappers -/
   8
   9/-- Binary scale factor `B = 2^k` as a real. -/
  10def B_of (k : Nat) : ℝ := (2 : ℝ) ^ k
  11
  12@[simp] lemma B_of_zero : B_of 0 = 1 := by simp [B_of]
  13
  14@[simp] lemma B_of_succ (k : Nat) : B_of (k+1) = 2 * B_of k := by
  15  simp [B_of, pow_succ, mul_comm]
  16
  17lemma B_of_pos (k : Nat) : 0 < B_of k := by
  18  have : 0 < (2:ℝ) := by norm_num
  19  simpa [B_of] using pow_pos this k
  20
  21@[simp] lemma B_of_one : B_of 1 = 2 := by simp [B_of]
  22
  23lemma one_le_B_of (k : Nat) : (1 : ℝ) ≤ B_of k := by
  24  induction k with
  25  | zero => simp [B_of]
  26  | succ k ih =>
  27      have hmul : (2 : ℝ) ≤ 2 * B_of k := by
  28        have : 2 * (1 : ℝ) ≤ 2 * B_of k := by
  29          have hnonneg : 0 ≤ (2 : ℝ) := by norm_num
  30          exact mul_le_mul_of_nonneg_left ih hnonneg
  31        simpa using this
  32      have h12 : (1 : ℝ) ≤ 2 := by norm_num
  33      have : (1 : ℝ) ≤ 2 * B_of k := le_trans h12 hmul
  34      simpa [B_of_succ, mul_comm] using this
  35
  36/-- Two to an integer power: 2^k for k ∈ ℤ. -/
  37noncomputable def twoPowZ (k : Int) : ℝ :=
  38  if 0 ≤ k then (2 : ℝ) ^ (Int.toNat k)
  39  else 1 / ((2 : ℝ) ^ (Int.toNat (-k)))
  40