Simple iteration lemma

theorem simple_iteration_lemma    {ρ : ℝ → ℝ} {A_iter : ℝ}    (hA_iter : 0 ≤ A_iter)    (hρ_nonneg : ∀ t : ℝ, 1 / 2 ≤ t → t < 1 → 0 ≤ ρ t)    (hρ_bdd : ∃ M : ℝ, ∀ t : ℝ, 1 / 2 ≤ t → t < 1 → (1 - t) ^ 2 * ρ t ≤ M)    (hρ_contract : ∀ s t : ℝ, 1 / 2 ≤ s → s < t → t < 1 →      ρ s ≤ 1 / 2 * ρ t + A_iter * (t - s) ⁻¹ ^ 2) :    ρ (1 / 2) ≤ C_iter * A_iter := by  /- Proof using δ = 1/4: for s ∈ [1/2,1), set t = s + (1-s)/4 = (3s+1)/4.     Then t-s = (1-s)/4, 1-t = 3(1-s)/4, (1-s)/(1-t) = 4/3.     Multiplying the contraction by (1-s)² gives       (1-s)² ρ(s) ≤ (8/9)(1-t)² ρ(t) + 16 A_iter.     Iterating: if M bounds (1-t)² ρ(t), then (8/9)M + 16 A_iter also does.     After n iterations the bound is (8/9)^n M + 144(1-(8/9)^n) A_iter.     As n → ∞ this tends to 144 A_iter. So (1/2)² ρ(1/2) ≤ 144 A_iter,     hence ρ(1/2) ≤ 576 A_iter ≤ 1024 A_iter = C_iter A_iter. -/  -- Extract M from hρ_bdd and make it nonneg  obtain ⟨M₀, hM₀⟩ := hρ_bdd  set M : ℝ := max M₀ 0 with hM_def  have hM_nn : 0 ≤ M := le_max_right _ _  have hM_bound : ∀ t : ℝ, 1 / 2 ≤ t → t < 1 → (1 - t) ^ 2 * ρ t ≤ M := by    intro t ht1 ht2    exact le_trans (hM₀ t ht1 ht2) (le_max_left _ _)  -- Key one-step improvement: for any upper bound B ≥ 0 on (1-t)²ρ(t),  -- (8/9)B + 16 A_iter is also an upper bound.  have improvement : ∀ B : ℝ, 0 ≤ B →      (∀ t : ℝ, 1 / 2 ≤ t → t < 1 → (1 - t) ^ 2 * ρ t ≤ B) →      (∀ s : ℝ, 1 / 2 ≤ s → s < 1 → (1 - s) ^ 2 * ρ s ≤ 8 / 9 * B + 16 * A_iter) := by    intro B hB_nn hB_bound s hs1 hs2    -- Set t = (3s + 1) / 4    set t := (3 * s + 1) / 4 with ht_def    have ht_gt_s : s < t := by linarith    have ht_lt_1 : t < 1 := by linarith    have ht_ge : 1 / 2 ≤ t := by linarith    have h1ms_pos : 0 < 1 - s := by linarith    have h1mt_pos : 0 < 1 - t := by linarith    have hts_pos : 0 < t - s := by linarith    -- Compute key ratios    have h1mt : 1 - t = 3 / 4 * (1 - s) := by rw [ht_def]; ring    have hts : t - s = 1 / 4 * (1 - s) := by rw [ht_def]; ring    -- Apply the contraction hypothesis    have hcontr := hρ_contract s t hs1 ht_gt_s ht_lt_1    -- Multiply both sides by (1-s)²    have hρ_s_nn : 0 ≤ ρ s := hρ_nonneg s hs1 hs2    have hρ_t_nn : 0 ≤ ρ t := hρ_nonneg t ht_ge ht_lt_1    -- (1-s)² ρ(s) ≤ (1-s)² ((1/2) ρ(t) + A_iter (t-s)⁻²)    have step1 : (1 - s) ^ 2 * ρ s ≤        (1 - s) ^ 2 * (1 / 2 * ρ t + A_iter * (t - s)⁻¹ ^ 2) := by      exact mul_le_mul_of_nonneg_left hcontr (sq_nonneg _)    -- (1-s)² · (t-s)⁻¹² = 16    have hprod1 : (1 - s) ^ 2 * ((t - s)⁻¹ ^ 2) = 16 := by      rw [hts]      have : 1 / 4 * (1 - s) ≠ 0 := by positivity      field_simp      ring    -- Also (1-s)² · (1/2) ρ(t) = (1/2) ((1-s)/(1-t))² (1-t)² ρ(t)    -- = (1/2)(4/3)²(1-t)² ρ(t) = (8/9)(1-t)² ρ(t)    have hratio : (1 - s) ^ 2 * (1 / 2 * ρ t) = 8 / 9 * ((1 - t) ^ 2 * ρ t) := by      rw [h1mt]; ring    -- Combine    calc (1 - s) ^ 2 * ρ s        ≤ (1 - s) ^ 2 * (1 / 2 * ρ t + A_iter * (t - s)⁻¹ ^ 2) := step1      _ = (1 - s) ^ 2 * (1 / 2 * ρ t) + A_iter * ((1 - s) ^ 2 * (t - s)⁻¹ ^ 2) := by ring      _ = 8 / 9 * ((1 - t) ^ 2 * ρ t) + A_iter * 16 := by rw [hratio, hprod1]      _ ≤ 8 / 9 * B + 16 * A_iter := by          have := hB_bound t ht_ge ht_lt_1          nlinarith  -- Iterate the improvement n times: after n steps the bound is  -- (8/9)^n M + 144(1 - (8/9)^n) A_iter  -- Define the iterated bound  let bound : ℕ → ℝ := fun n => (8 / 9) ^ n * M + (1 - (8 / 9) ^ n) * (144 * A_iter)  have hbound_nn : ∀ n, 0 ≤ bound n := by    intro n    have h89 : (0 : ℝ) ≤ (8 / 9) ^ n := by positivity    have h89_le1 : (8 / 9 : ℝ) ^ n ≤ 1 := pow_le_one₀ (by positivity) (by norm_num)    nlinarith [mul_nonneg h89 hM_nn]  -- Show that bound n is an upper bound for all n  have hbound_is_bound : ∀ n, ∀ t : ℝ, 1 / 2 ≤ t → t < 1 →      (1 - t) ^ 2 * ρ t ≤ bound n := by    intro n    induction n with    | zero =>      intro t ht1 ht2      simp only [bound, pow_zero, one_mul, sub_self, zero_mul, add_zero]      exact hM_bound t ht1 ht2    | succ n ih =>      intro s hs1 hs2      have him := improvement (bound n) (hbound_nn n) ih s hs1 hs2      -- Need: 8/9 * bound n + 16 * A_iter ≤ bound (n+1)      -- bound (n+1) = (8/9)^(n+1) M + (1 - (8/9)^(n+1)) * 144 * A_iter      -- 8/9 * bound n + 16 * A_iter      --   = 8/9 * ((8/9)^n M + (1-(8/9)^n) * 144 A_iter) + 16 A_iter      --   = (8/9)^(n+1) M + (8/9)(1-(8/9)^n) * 144 A_iter + 16 A_iter      --   = (8/9)^(n+1) M + (8/9 - (8/9)^(n+1)) * 144 A_iter + 16 A_iter      --   = (8/9)^(n+1) M + (8/9)*144 A_iter - (8/9)^(n+1)*144 A_iter + 16 A_iter      --   = (8/9)^(n+1) M + 128 A_iter + 16 A_iter - (8/9)^(n+1) * 144 A_iter      --   = (8/9)^(n+1) M + 144 A_iter - (8/9)^(n+1) * 144 A_iter      --   = (8/9)^(n+1) M + (1 - (8/9)^(n+1)) * 144 A_iter = bound (n+1) ✓      suffices 8 / 9 * bound n + 16 * A_iter = bound (n + 1) by linarith      show 8 / 9 * ((8 / 9) ^ n * M + (1 - (8 / 9) ^ n) * (144 * A_iter)) + 16 * A_iter =        (8 / 9) ^ (n + 1) * M + (1 - (8 / 9) ^ (n + 1)) * (144 * A_iter)      rw [pow_succ]      ring  -- ρ(1/2) ≤ 4 * bound n for all n  have hρ_le_4bound : ∀ n, ρ (1 / 2) ≤ 4 * bound n := by    intro n    have h12 : (1 : ℝ) / 2 ≤ 1 / 2 := le_refl _    have h12_lt : (1 : ℝ) / 2 < 1 := by norm_num    have := hbound_is_bound n (1 / 2) h12 h12_lt    -- (1 - 1/2)² ρ(1/2) ≤ bound n, i.e., (1/4) ρ(1/2) ≤ bound n    have h14 : (1 - 1 / 2 : ℝ) ^ 2 = 1 / 4 := by norm_num    rw [h14] at this    -- ρ(1/2) ≤ 4 * bound n    have hρ12_nn : 0 ≤ ρ (1 / 2) := hρ_nonneg (1 / 2) h12 h12_lt    linarith  -- Now: bound n → 144 * A_iter as n → ∞ (since (8/9)^n → 0)  -- We need: ρ(1/2) ≤ 576 * A_iter  -- Use: for all ε > 0, exists n such that bound n ≤ 144 * A_iter + ε  -- Then ρ(1/2) ≤ 4 * (144 * A_iter + ε) = 576 * A_iter + 4ε  -- Since ε arbitrary, ρ(1/2) ≤ 576 * A_iter  suffices h576 : ρ (1 / 2) ≤ 576 * A_iter by    calc ρ (1 / 2) ≤ 576 * A_iter := h576      _ ≤ C_iter * A_iter := by unfold C_iter; nlinarith [hA_iter]  -- Prove via le_of_forall_pos_lt_add  rw [show (576 : ℝ) * A_iter = 4 * (144 * A_iter) from by ring]  apply le_of_forall_pos_lt_add  intro ε hε  -- Find n such that (8/9)^n * M < ε / 4  have h89_lt : (8 : ℝ) / 9 < 1 := by norm_num  have h89_nn : (0 : ℝ) ≤ 8 / 9 := by norm_num  have hε4 : (0 : ℝ) < ε / 4 := by linarith  have htend : Filter.Tendsto (fun n => (8 / 9 : ℝ) ^ n * M) Filter.atTop (nhds 0) := by    have := (tendsto_pow_atTop_nhds_zero_of_lt_one h89_nn h89_lt).mul_const M    rwa [zero_mul] at this  rw [tendsto_atTop_nhds] at htend  obtain ⟨N, hN⟩ := htend (Set.Iio (ε / 4)) (show (0 : ℝ) ∈ Set.Iio (ε / 4) from hε4)    isOpen_Iio  have hN' : (8 / 9) ^ N * M < ε / 4 := hN N (le_refl _)  -- bound N ≤ (8/9)^N * M + 144 * A_iter  have hboundN : bound N ≤ (8 / 9) ^ N * M + 144 * A_iter := by    show (8 / 9) ^ N * M + (1 - (8 / 9) ^ N) * (144 * A_iter) ≤      (8 / 9) ^ N * M + 144 * A_iter    nlinarith [pow_nonneg h89_nn N, hA_iter]  calc ρ (1 / 2)      ≤ 4 * bound N := hρ_le_4bound N    _ ≤ 4 * ((8 / 9) ^ N * M + 144 * A_iter) := by nlinarith    _ < 4 * (ε / 4 + 144 * A_iter) := by nlinarith    _ = 4 * (144 * A_iter) + ε := by ring