Commit 2025-05-22 00:24 f13eeded

feat(Analysis/SpecialFunctions): extend tendsto_one_plus_div_rpow_exp (#23804) This PR

• Proves 12 theorems (they are stated separately because of differences in rexp vs cexp and pow vs rpow):
  • The limit of x * log (1 + t/x + o(1/x)) as x → ∞ is t for t : ℂ or ℝ and x : ℝ or ℕ.
  • The limit of (1 + t/x + o(1/x)) ^ x as x → ∞ is exp t for t : ℂ or ℝ and x : ℝ or ℕ.
  • The limit of (1 + t/x) ^ x as x → ∞ is exp t for t : ℂ or ℝ and x : ℝ or ℕ.
  • (Note: the last row of theorems for t : ℝ already exist and are now replaced)
• Renames plus to add in affected theorems The little-o theorem for t : ℂ is needed for CLT. Moves:
• tendsto_one_plus_div_rpow_exp -> Real.tendsto_one_add_div_rpow_exp
• tendsto_one_plus_div_pow_exp -> Real.tendsto_one_add_div_pow_exp
• tendsto_integral_mul_one_plus_inv_smul_sq_pow -> tendsto_integral_mul_one_add_inv_smul_sq_pow