Real powers used in quadratic regularizations

This file records elementary facts about the regularization (a ^ 2 + t) ^ e as t → 0⁺. They provide the algebraic identity at t = 0, convergence away from a = 0, and domination for nonpositive exponents.

Main declarations

• TauCeti.sq_rpow_div_two: taking the real power s / 2 of a square gives the power s of a nonnegative base.
• TauCeti.tendsto_sq_add_rpow: a quadratically regularized real power converges as the regularization parameter tends to zero from above.
• TauCeti.sq_add_rpow_le: for a nonpositive exponent, the regularized power is bounded by its value at zero.

theorem TauCeti.sq_rpow_div_two {a : ℝ} (ha : 0 ≤ a) (s : ℝ) : (a ^ 2) ^ (s / 2) = a ^ s

For a nonnegative real number a, taking the real power s / 2 of a ^ 2 gives a ^ s.

theorem TauCeti.tendsto_sq_add_rpow {a : ℝ} (ha : a ≠ 0) (e : ℝ) : Filter.Tendsto (fun (t : ℝ) => (a ^ 2 + t) ^ e) (nhdsWithin 0 (Set.Ioi 0)) (nhds ((a ^ 2 + 0) ^ e))

If a ≠ 0, then (a ^ 2 + t) ^ e converges to (a ^ 2) ^ e as t → 0⁺.

theorem TauCeti.sq_add_rpow_le {a : ℝ} (ha : a ≠ 0) {t : ℝ} (ht : 0 ≤ t) {e : ℝ} (he : e ≤ 0) : (a ^ 2 + t) ^ e ≤ (a ^ 2 + 0) ^ e

If a ≠ 0, t ≥ 0, and e ≤ 0, then the regularized power (a ^ 2 + t) ^ e is bounded by its value at t = 0.