Super Step Const Inv le

theorem superStepConstInv_le    (hd : 2 < (d : ℝ))    (A : NormalizedEllipticCoeff d (Metric.ball (0 : E) 1))    {p₀ : ℝ} (hp₀ : 0 < p₀) (i : ℕ) :    superStepConstInv (d := d) A p₀ i ≤      (16 * C_MoserAnchor d * (A.1.Λ * p₀ ^ 2 + 1) *        (4 * moserChi d ^ 2) ^ i) ^        (1 / moserExponentSeq d p₀ i) := by  unfold superStepConstInv  apply Real.rpow_le_rpow  · -- Nonnegativity of the base    apply mul_nonneg    · exact div_nonneg (le_trans (by norm_num : (0 : ℝ) ≤ 1) (one_le_C_MoserAnchor (d := d)))        (sq_nonneg _)    · nlinarith [A.1.Λ_nonneg, sq_nonneg (moserExponentSeq d p₀ i / (1 + moserExponentSeq d p₀ i))]  · -- Main bound    have hp_i := moserExponentSeq_pos (d := d) hd hp₀ i    have hgap_eq : C_MoserAnchor d / (moserRadius i - moserRadius (i + 1)) ^ 2 =        C_MoserAnchor d * (4 : ℝ) ^ (i + 2) := by      rw [moserRadius_gap]      have hsq : (((1 / 2 : ℝ) ^ (i + 2)) ^ 2) = (1 / 4 : ℝ) ^ (i + 2) := by        rw [← pow_mul, show (i + 2) * 2 = 2 * (i + 2) by ring, pow_mul]; norm_num      rw [hsq, div_eq_mul_inv,        show (((1 / 4 : ℝ) ^ (i + 2))⁻¹) = (4 : ℝ) ^ (i + 2) by          rw [show (1 / 4 : ℝ) = (4 : ℝ)⁻¹ by norm_num, inv_pow]; norm_num]    have hpow4 : (4 : ℝ) ^ (i + 2) = 16 * 4 ^ i := by rw [pow_add]; ring    -- pₙ/(1+pₙ) ≤ pₙ, so Λ(pₙ/(1+pₙ))² ≤ Λpₙ²    have hratio_le : (moserExponentSeq d p₀ i / (1 + moserExponentSeq d p₀ i)) ^ 2 ≤        (moserExponentSeq d p₀ i) ^ 2 := by      have hdiv_le : moserExponentSeq d p₀ i / (1 + moserExponentSeq d p₀ i) ≤          moserExponentSeq d p₀ i :=        div_le_self hp_i.le (by linarith)      have hdiv_nonneg : 0 ≤ moserExponentSeq d p₀ i / (1 + moserExponentSeq d p₀ i) :=        div_nonneg hp_i.le (by linarith)      nlinarith [sq_nonneg (moserExponentSeq d p₀ i - moserExponentSeq d p₀ i / (1 + moserExponentSeq d p₀ i))]    -- pₙ² = p₀² · χ^{2i}    have hseq_sq : (moserExponentSeq d p₀ i) ^ 2 = p₀ ^ 2 * (moserChi d) ^ (2 * i) := by      rw [moserExponentSeq]; ring    -- Combine: Λ(pₙ/(1+pₙ))² + 1 ≤ (Λp₀² + 1) · χ^{2i}    have hcoeff_le :        A.1.Λ * (moserExponentSeq d p₀ i / (1 + moserExponentSeq d p₀ i)) ^ 2 + 1 ≤          (A.1.Λ * p₀ ^ 2 + 1) * (moserChi d ^ 2) ^ i := by      have hchi_sq_ge_one : 1 ≤ (moserChi d ^ 2) ^ i :=        one_le_pow₀ (by nlinarith [one_lt_moserChi (d := d) hd])      have hΛratio :          A.1.Λ * (moserExponentSeq d p₀ i / (1 + moserExponentSeq d p₀ i)) ^ 2 ≤            A.1.Λ * p₀ ^ 2 * (moserChi d ^ 2) ^ i := by        calc A.1.Λ * (moserExponentSeq d p₀ i / (1 + moserExponentSeq d p₀ i)) ^ 2            ≤ A.1.Λ * (moserExponentSeq d p₀ i) ^ 2 :=              mul_le_mul_of_nonneg_left hratio_le A.1.Λ_nonneg          _ = A.1.Λ * (p₀ ^ 2 * (moserChi d) ^ (2 * i)) := by rw [hseq_sq]          _ = A.1.Λ * p₀ ^ 2 * (moserChi d ^ 2) ^ i := by rw [pow_mul]; ring      nlinarith    rw [hgap_eq, hpow4]    calc C_MoserAnchor d * (16 * 4 ^ i) *            (A.1.Λ * (moserExponentSeq d p₀ i / (1 + moserExponentSeq d p₀ i)) ^ 2 + 1)        ≤ C_MoserAnchor d * (16 * 4 ^ i) *            ((A.1.Λ * p₀ ^ 2 + 1) * (moserChi d ^ 2) ^ i) := by          gcongr          exact mul_nonneg (le_trans (by norm_num : (0 : ℝ) ≤ 1) (one_le_C_MoserAnchor (d := d)))            (by positivity)      _ = 16 * C_MoserAnchor d * (A.1.Λ * p₀ ^ 2 + 1) * (4 * moserChi d ^ 2) ^ i := by          rw [show (4 * moserChi d ^ 2) ^ i = 4 ^ i * (moserChi d ^ 2) ^ i by rw [mul_pow]]          ring  · exact div_nonneg (by norm_num) (moserExponentSeq_pos (d := d) hd hp₀ i).le