Real.dyadic_trailing_inv_term_le

lemma dyadic_trailing_inv_term_le (C L r0 τ : ℝ) (k : ℕ) (hr0 : 0 ≤ r0) :    (C / L) * ((r0 * (2 : ℝ) ^ (k : ℝ))⁻¹ ^ τ)      ≤ (((C / L) + 1) * (r0⁻¹ : ℝ) ^ τ) * ((2 : ℝ) ^ (-τ)) ^ k := by  rw [inv_dyadicRadius_rpow_eq r0 τ k hr0]  have hcoeff : C / L ≤ C / L + 1 := by linarith  have hr0Inv_nonneg : 0 ≤ (r0⁻¹ : ℝ) ^ τ :=    Real.rpow_nonneg (inv_nonneg.2 hr0) _  have hmul :      (C / L) * ((r0⁻¹ : ℝ) ^ τ)        ≤ ((C / L) + 1) * ((r0⁻¹ : ℝ) ^ τ) :=    mul_le_mul_of_nonneg_right hcoeff hr0Inv_nonneg  have hqpow_nonneg : 0 ≤ ((2 : ℝ) ^ (-τ)) ^ k :=    pow_nonneg (le_of_lt (Real.rpow_pos_of_pos (by norm_num : (0 : ℝ) < 2) _)) _  have := mul_le_mul_of_nonneg_right hmul hqpow_nonneg  simpa [mul_assoc, mul_left_comm, mul_comm] using this