Real.dyadic_growth_mass_mul_inv_le_geometric

lemma dyadic_growth_mass_mul_inv_le_geometric {C L M X T Ctrail r0 ρ τ : ℝ} {k : ℕ}    (hL : 0 < L) (hC : 0 ≤ C) (hr0 : 0 ≤ r0)    (hX : X ≤ M * ((2 : ℝ) ^ ρ) ^ k)    (hT : T ≤ ((C * X + Ctrail) / L) * ((r0 * (2 : ℝ) ^ (k : ℝ))⁻¹ ^ τ)) :    T ≤ (((C / L) * M) * (r0⁻¹ : ℝ) ^ τ) * ((2 : ℝ) ^ (ρ - τ)) ^ k        + (((Ctrail / L) + 1) * (r0⁻¹ : ℝ) ^ τ) * ((2 : ℝ) ^ (-τ)) ^ k := by  have hmul : C * X ≤ C * (M * ((2 : ℝ) ^ ρ) ^ k) :=    mul_le_mul_of_nonneg_left hX hC  have hnum : C * X + Ctrail ≤ C * (M * ((2 : ℝ) ^ ρ) ^ k) + Ctrail :=    add_le_add hmul le_rfl  have hdiv :      (C * X + Ctrail) / L ≤ (C * (M * ((2 : ℝ) ^ ρ) ^ k) + Ctrail) / L :=    div_le_div_of_nonneg_right hnum hL.le  have h2k_nonneg : 0 ≤ (2 : ℝ) ^ (k : ℝ) :=    le_of_lt (Real.rpow_pos_of_pos (by norm_num : (0 : ℝ) < 2) (k : ℝ))  have hrk_nonneg : 0 ≤ r0 * (2 : ℝ) ^ (k : ℝ) :=    mul_nonneg hr0 h2k_nonneg  have hfactor_nonneg : 0 ≤ ((r0 * (2 : ℝ) ^ (k : ℝ))⁻¹ ^ τ) :=    Real.rpow_nonneg (inv_nonneg.2 hrk_nonneg) τ  have hmul' :=    mul_le_mul_of_nonneg_right hdiv hfactor_nonneg  have hdecomp :      ((C * (M * ((2 : ℝ) ^ ρ) ^ k) + Ctrail) / L) *          ((r0 * (2 : ℝ) ^ (k : ℝ))⁻¹ ^ τ)        =        ((C / L) * (M * ((2 : ℝ) ^ ρ) ^ k)) *            ((r0 * (2 : ℝ) ^ (k : ℝ))⁻¹ ^ τ)          + ((Ctrail / L) * ((r0 * (2 : ℝ) ^ (k : ℝ))⁻¹ ^ τ)) := by    let Y : ℝ := (r0 * (2 : ℝ) ^ (k : ℝ))⁻¹ ^ τ    have :        ((C * (M * ((2 : ℝ) ^ ρ) ^ k) + Ctrail) / L) * Y          = ((C / L) * (M * ((2 : ℝ) ^ ρ) ^ k)) * Y            + ((Ctrail / L) * Y) := by      ring    simpa [Y]  have hpre :      T ≤ ((C / L) * (M * ((2 : ℝ) ^ ρ) ^ k)) *            ((r0 * (2 : ℝ) ^ (k : ℝ))⁻¹ ^ τ)          + ((Ctrail / L) * ((r0 * (2 : ℝ) ^ (k : ℝ))⁻¹ ^ τ)) :=    hT.trans (hmul'.trans_eq hdecomp)  have hA := le_of_eq (dyadic_growth_inv_term_eq C L M r0 ρ τ k hr0)  have hB := dyadic_trailing_inv_term_le Ctrail L r0 τ k hr0  exact hpre.trans (by    simpa [mul_assoc, mul_left_comm, mul_comm] using add_le_add hA hB)