Real.one_add_abs_two_mul_dyadicRadius_rpow_le

lemma one_add_abs_two_mul_dyadicRadius_rpow_le {r0 ρ : ℝ} (k : ℕ)    (hr0 : 0 < r0) (hρ : 0 ≤ ρ) :    (1 + |2 * (r0 * (2 : ℝ) ^ ((k : ℝ) + 1))|) ^ ρ      ≤ (1 + 4 * r0) ^ ρ * ((2 : ℝ) ^ ρ) ^ k := by  let Rk : ℝ := r0 * (2 : ℝ) ^ ((k : ℝ) + 1)  have hRk' : |2 * Rk| = 4 * r0 * (2 : ℝ) ^ (k : ℝ) := by    have hnonneg : 0 ≤ (2 : ℝ) * Rk := by      have : 0 ≤ Rk := by        dsimp [Rk]        exact mul_nonneg hr0.le (le_of_lt (Real.rpow_pos_of_pos (by norm_num) _))      nlinarith    have hmul : (2 : ℝ) * Rk = 4 * r0 * (2 : ℝ) ^ (k : ℝ) := by      dsimp [Rk]      calc        (2 : ℝ) * (r0 * (2 : ℝ) ^ ((k : ℝ) + 1))            = (2 * r0) * (2 : ℝ) ^ ((k : ℝ) + 1) := by ring        _ = (2 * r0) * ((2 : ℝ) ^ (k : ℝ) * (2 : ℝ) ^ (1 : ℝ)) := by              simp [Real.rpow_add, mul_assoc]        _ = (2 * r0) * ((2 : ℝ) ^ (k : ℝ) * 2) := by simp [Real.rpow_one]        _ = 4 * r0 * (2 : ℝ) ^ (k : ℝ) := by ring    calc      |2 * Rk| = 2 * Rk := abs_of_nonneg hnonneg      _ = 4 * r0 * (2 : ℝ) ^ (k : ℝ) := hmul  have hbase :      (1 + |2 * Rk|) ≤ (1 + 4 * r0) * (2 : ℝ) ^ (k : ℝ) := by    have h1 : (1 : ℝ) ≤ (2 : ℝ) ^ (k : ℝ) := by      have : (1 : ℝ) ≤ (2 : ℝ) ^ (k : ℕ) := by        simpa using (one_le_pow₀ (by norm_num : (1 : ℝ) ≤ (2 : ℝ)))      simpa [Real.rpow_natCast] using this    have habs :        1 + |2 * Rk| ≤ (2 : ℝ) ^ (k : ℝ) + (4 * r0) * (2 : ℝ) ^ (k : ℝ) := by      rw [hRk']      simpa [add_assoc, add_left_comm, add_comm, mul_assoc, mul_left_comm, mul_comm] using        (add_le_add_right h1 ((4 * r0) * (2 : ℝ) ^ (k : ℝ)))    have hfac :        (2 : ℝ) ^ (k : ℝ) + (4 * r0) * (2 : ℝ) ^ (k : ℝ)          = (1 + 4 * r0) * (2 : ℝ) ^ (k : ℝ) := by      ring    exact habs.trans (le_of_eq hfac)  have hRnonneg : 0 ≤ (1 + |2 * Rk|) := by linarith [abs_nonneg (2 * Rk)]  have :      (1 + |2 * Rk|) ^ ρ ≤ ((1 + 4 * r0) * (2 : ℝ) ^ (k : ℝ)) ^ ρ :=    Real.rpow_le_rpow hRnonneg hbase hρ  have hsplit :      ((1 + 4 * r0) * (2 : ℝ) ^ (k : ℝ)) ^ ρ        = (1 + 4 * r0) ^ ρ * ((2 : ℝ) ^ (k : ℝ)) ^ ρ := by    have h1 : 0 ≤ (1 + 4 * r0) := by nlinarith [hr0.le]    have h2 : 0 ≤ (2 : ℝ) ^ (k : ℝ) :=      le_of_lt (Real.rpow_pos_of_pos (by norm_num) _)    simpa using (Real.mul_rpow h1 h2 (z := ρ))  have hpow : ((2 : ℝ) ^ (k : ℝ)) ^ ρ = ((2 : ℝ) ^ ρ) ^ k := by    have h2nonneg : (0 : ℝ) ≤ 2 := by norm_num    calc      ((2 : ℝ) ^ (k : ℝ)) ^ ρ = (2 : ℝ) ^ ((k : ℝ) * ρ) := by        simp [Real.rpow_mul]      _ = ((2 : ℝ) ^ ρ) ^ (k : ℝ) := by        simpa [mul_comm] using          (Real.rpow_mul (x := (2 : ℝ)) (y := ρ) (z := (k : ℝ)) h2nonneg)      _ = ((2 : ℝ) ^ ρ) ^ k := by        simp [Real.rpow_natCast]  calc    (1 + |2 * (r0 * (2 : ℝ) ^ ((k : ℝ) + 1))|) ^ ρ        = (1 + |2 * Rk|) ^ ρ := by rfl    _ ≤ ((1 + 4 * r0) * (2 : ℝ) ^ (k : ℝ)) ^ ρ := this    _ = (1 + 4 * r0) ^ ρ * ((2 : ℝ) ^ (k : ℝ)) ^ ρ := hsplit    _ = (1 + 4 * r0) ^ ρ * ((2 : ℝ) ^ ρ) ^ k := by      simpa [mul_assoc] using congrArg (fun t => (1 + 4 * r0) ^ ρ * t) hpow