Supersolution iteration inverse

theorem supersolution_iteration_inverse    (hd : 2 < (d : ℝ))    (A : NormalizedEllipticCoeff d (Metric.ball (0 : E) 1))    {u : E → ℝ} {p₀ : ℝ} (hp₀ : 0 < p₀)    (hu_pos : ∀ x ∈ Metric.ball (0 : E) 1, 0 < u x)    (hsuper : IsSupersolution A.1 u)    (hpInt :      IntegrableOn (fun x => |(u x)⁻¹| ^ p₀)        (Metric.ball (0 : E) 1) volume) :    ∀ n : ℕ,      IntegrableOn (fun x => |(u x)⁻¹| ^ moserExponentSeq d p₀ n)          (Metric.ball (0 : E) (moserRadius n)) volume ∧        superIterNormInv (d := d) (u := u) p₀ n ≤          (∏ i ∈ Finset.range n, superStepConstInv (d := d) A p₀ i) *            superIterNormInv (d := d) (u := u) p₀ 0 := by  intro n  induction n with  | zero =>    constructor    · -- Base case: moserRadius 0 = 1 and moserExponentSeq _ _ 0 = p₀      rwa [moserExponentSeq_zero, moserRadius_zero]    · -- Product over empty range is 1      simp  | succ n ihn =>    obtain ⟨hInt_n, hbound_n⟩ := ihn    let p_n := moserExponentSeq d p₀ n    have hp_n : 0 < p_n := moserExponentSeq_pos hd hp₀ n    -- Apply the one-step inverse-power bound    have hpre :=      supersolution_preMoser_inverse hd A (p := p_n)        (r := moserRadius (n + 1)) (s := moserRadius n)        hp_n (moserRadius_pos (n + 1)) (moserRadius_succ_lt n)        (moserRadius_le_one n) hu_pos hsuper        (by simpa [p_n] using hInt_n)    obtain ⟨hInt_succ, hNorm_succ⟩ := hpre    refine ⟨?_, ?_⟩    · -- Integrability: convert moserChi * p_n to p_{n+1}      have heq : moserChi d * p_n = moserExponentSeq d p₀ (n + 1) := by        rw [moserExponentSeq_succ]      rwa [heq] at hInt_succ    · -- Bound: multiply step bound with inductive hypothesis      have heq_norm : superIterNormInv (d := d) (u := u) p₀ (n + 1) =          (∫ x in Metric.ball (0 : E) (moserRadius (n + 1)),            |(u x)⁻¹| ^ (moserChi d * p_n) ∂volume) ^              (1 / (moserChi d * p_n)) := by        simp [superIterNormInv, superIterIntegralInv, p_n, moserExponentSeq_succ]      have heq_step : superStepConstInv (d := d) A p₀ n =          ((C_MoserAnchor d / (moserRadius n - moserRadius (n + 1)) ^ 2) *            (A.1.Λ * (p_n / (1 + p_n)) ^ 2 + 1)) ^ (1 / p_n) := by        simp [superStepConstInv, p_n]      have hstep_nonneg : 0 ≤ superStepConstInv (d := d) A p₀ n := by        rw [heq_step]        apply Real.rpow_nonneg        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 (p_n / (1 + p_n))]      -- The one-step bound gives:      --   ‖u⁻¹‖_{n+1} ≤ step_n * ‖u⁻¹‖_n      have hstep_bound :          superIterNormInv (d := d) (u := u) p₀ (n + 1) ≤            superStepConstInv (d := d) A p₀ n *              superIterNormInv (d := d) (u := u) p₀ n := by        rw [heq_norm, heq_step]        convert hNorm_succ using 2      -- Combine with IH      calc superIterNormInv (d := d) (u := u) p₀ (n + 1)          ≤ superStepConstInv (d := d) A p₀ n *              superIterNormInv (d := d) (u := u) p₀ n := hstep_bound        _ ≤ superStepConstInv (d := d) A p₀ n *              ((∏ i ∈ Finset.range n, superStepConstInv (d := d) A p₀ i) *                superIterNormInv (d := d) (u := u) p₀ 0) := by            exact mul_le_mul_of_nonneg_left hbound_n hstep_nonneg        _ = (∏ i ∈ Finset.range (n + 1), superStepConstInv (d := d) A p₀ i) *              superIterNormInv (d := d) (u := u) p₀ 0 := by            rw [Finset.prod_range_succ]            ring