Square-root displacement estimates and limits at zero

Two estimates comparing the real square-root and inverse-square-root functions with the identity near 1. These bounds control scalar spectral factors of positive operators close to the identity. The file also records that the square root is 1/2-Hölder, |√t - √s| ≤ √|t - s|, that 1 ≤ √(1 + t²), |t / √(1 + t²)| ≤ 1, that the modular √(1 + t²) - 1 is at most |t| and t² / 2 and is locally Lipschitz, that c √u tends to 0 as u → 0, and through positive values as u → 0⁺ when c > 0, and the cancellation |d| (√(d² c p))⁻¹ = (√c)⁻¹ (√p)⁻¹ used in changes of variables, and that the radial profile t ↦ ψ (√t) / (√t) ^ n of a C^k function supported in (0, ∞) is C^k.

Main results

• Real.abs_sqrt_sub_one_le_abs_sub_one: for every real μ, |√μ - 1| ≤ |μ - 1|.
• Real.abs_one_sub_inv_sqrt_le: if |μ - 1| ≤ δ ≤ 1/2, |1 - (√μ)⁻¹| ≤ δ.
• Real.abs_sqrt_sub_sqrt_le: for all reals t and s, |√t - √s| ≤ √|t - s|.
• Real.one_le_sqrt_one_add_sq: for every real t, 1 ≤ √(1 + t²).
• Real.abs_div_sqrt_one_add_sq_le_one: for every real t, |t / √(1 + t²)| ≤ 1.
• Real.sqrt_one_add_sq_sub_one_le_abs: for every real t, √(1 + t²) - 1 ≤ |t|.
• Real.sqrt_one_add_sq_sub_one_le_sq_div_two: for every real t, √(1 + t²) - 1 ≤ t² / 2.
• Real.abs_sqrt_one_add_sq_sub_sqrt_one_add_sq_le: for all reals a and b, |√(1 + a²) - √(1 + b²)| ≤ |a - b| (|a| + |b|).
• Real.le_sqrt_mul_of_sq_le_mul: if 0 ≤ b and a² ≤ c b² then a ≤ √c * b.
• Real.abs_mul_inv_sqrt_sq_mul_mul: for d ≠ 0 and 0 ≤ c, |d| (√(d² c p))⁻¹ = (√c)⁻¹ (√p)⁻¹.
• Real.tendsto_mul_sqrt_nhds_zero: c √u → 0 as u → 0.
• Real.tendsto_mul_sqrt_nhdsGT_zero, Real.tendsto_sqrt_nhdsGT_zero: for c > 0, c √u → 0⁺ as u → 0⁺.
• Real.add_sqrt_sq_add_pos, Real.hasDerivAt_add_sqrt_sq_add, Real.image_add_sqrt_sq_add_eq_Ioi: the substitution t ↦ t + √(t² + p) is positive, has an explicit derivative, and maps ℝ onto (0, ∞) for p > 0.
• Real.contDiff_div_sqrt_pow: if ψ is C^k with support in (0, ∞), then t ↦ ψ (√t) / (√t) ^ n is C^k.

References

AIQ DKPS formalization, ForTauCeti/Analysis/SpecialFunctions/Sqrt.lean.

Real.add_sqrt_sq_add_pos, Real.hasDerivAt_add_sqrt_sq_add and Real.image_add_sqrt_sq_add_eq_Ioi are extracted from, and their proofs adapted from, Jeremy Tan's Mathlib PR #34397, commit 376352b6e080265bc0380074baaf9aafa0b70a80.

theorem Real.abs_sqrt_sub_one_le_abs_sub_one {μ : ℝ} : |√μ - 1| ≤ |μ - 1|

For every real μ, the square root is no farther from 1 than μ is: |√μ - 1| ≤ |μ - 1|.

theorem Real.abs_one_sub_inv_sqrt_le {μ δ : ℝ} (hδ : δ ≤ 1 / 2) (hμ : |μ - 1| ≤ δ) : |1 - (√μ)⁻¹| ≤ δ

If |μ - 1| ≤ δ ≤ 1 / 2, then |1 - (√μ)⁻¹| ≤ δ.

The hypotheses force μ to be positive and keep the inverse square root bounded near 1.

theorem Real.sqrt_le_sqrt_add_sqrt_abs_sub (t s : ℝ) : √t ≤ √s + √|t - s|

For all reals t and s, √t ≤ √s + √|t - s|.

theorem Real.abs_sqrt_sub_sqrt_le (t s : ℝ) : |√t - √s| ≤ √|t - s|

The square root is 1/2-Hölder. For all reals t and s, |√t - √s| ≤ √|t - s|.

theorem Real.one_le_sqrt_one_add_sq (t : ℝ) : 1 ≤ √(1 + t ^ 2)

For every real t, 1 ≤ √(1 + t²).

theorem Real.abs_div_sqrt_one_add_sq_le_one (t : ℝ) : |t / √(1 + t ^ 2)| ≤ 1

For every real t, |t / √(1 + t²)| ≤ 1.

theorem Real.sqrt_one_add_sq_sub_one_le_abs (t : ℝ) : √(1 + t ^ 2) - 1 ≤ |t|

The modular √(1 + t²) - 1 grows at most linearly: √(1 + t²) - 1 ≤ |t|.

theorem Real.sqrt_one_add_sq_sub_one_le_sq_div_two (t : ℝ) : √(1 + t ^ 2) - 1 ≤ t ^ 2 / 2

The modular √(1 + t²) - 1 is at most quadratic: √(1 + t²) - 1 ≤ t² / 2.

theorem Real.abs_sqrt_one_add_sq_sub_sqrt_one_add_sq_le (a b : ℝ) : |√(1 + a ^ 2) - √(1 + b ^ 2)| ≤ |a - b| * (|a| + |b|)

The modular √(1 + t²) - 1 is locally Lipschitz with a linear modulus: |√(1 + a²) - √(1 + b²)| ≤ |a - b| (|a| + |b|).

theorem Real.le_sqrt_mul_of_sq_le_mul {a b c : ℝ} (hb : 0 ≤ b) (h : a ^ 2 ≤ c * b ^ 2) : a ≤ √c * b

If a² ≤ c b² with 0 ≤ b, then a ≤ √c * b.

theorem Real.abs_mul_inv_sqrt_sq_mul_mul {d c : ℝ} (hd : d ≠ 0) (hc : 0 ≤ c) (p : ℝ) : |d| * (√(d ^ 2 * c * p))⁻¹ = (√c)⁻¹ * (√p)⁻¹

A square factor cancels against its absolute value. For d ≠ 0 and 0 ≤ c, |d| (√(d² c p))⁻¹ = (√c)⁻¹ (√p)⁻¹. This is the cancellation of the Jacobian |d| of a change of variables against the square root of an integrand that has acquired the factor d².

theorem Real.tendsto_mul_sqrt_nhds_zero (c : ℝ) : Filter.Tendsto (fun (u : ℝ) => c * √u) (nhds 0) (nhds 0)

For every c, c √u tends to 0 as u → 0.

theorem Real.tendsto_mul_sqrt_nhdsGT_zero {c : ℝ} (hc : 0 < c) : Filter.Tendsto (fun (u : ℝ) => c * √u) (nhdsWithin 0 (Set.Ioi 0)) (nhdsWithin 0 (Set.Ioi 0))

For c > 0, c √u tends to 0 through positive values as u → 0⁺.

theorem Real.tendsto_sqrt_nhdsGT_zero : Filter.Tendsto (fun (x : ℝ) => √x) (nhdsWithin 0 (Set.Ioi 0)) (nhdsWithin 0 (Set.Ioi 0))

The square root tends to 0 through positive values as u → 0⁺.

theorem Real.contDiff_div_sqrt_pow {k : WithTop ℕ∞} {ψ : ℝ → ℝ} (hψ : ContDiff ℝ k ψ) (hψs : tsupport ψ ⊆ Set.Ioi 0) (n : ℕ) : ContDiff ℝ k fun (t : ℝ) => ψ √t / √t ^ n

The radial profile t ↦ ψ (√t) / (√t) ^ n of a C^k function ψ supported in (0, ∞) is C^k.

theorem Real.add_sqrt_sq_add_pos {p : ℝ} (hp : 0 < p) (t : ℝ) : 0 < t + √(t ^ 2 + p)

For 0 < p, t + √(t² + p) is positive.

theorem Real.hasDerivAt_add_sqrt_sq_add {p : ℝ} (hp : 0 < p) (t : ℝ) : HasDerivAt (fun (t : ℝ) => t + √(t ^ 2 + p)) ((t + √(t ^ 2 + p)) / √(t ^ 2 + p)) t

The derivative of t ↦ t + √(t² + p) for 0 < p.

theorem Real.image_add_sqrt_sq_add_eq_Ioi {p : ℝ} (hp : 0 < p) : (fun (t : ℝ) => t + √(t ^ 2 + p)) '' Set.univ = Set.Ioi 0

For 0 < p, the map t ↦ t + √(t² + p) sends ℝ onto (0, ∞).

theorem Real.sqrt_add_le_add_sqrt (a b : ℝ) : √(a + b) ≤ √a + √b

Subadditivity of the square root: √(a + b) ≤ √a + √b.