Elementary real charts for one-dimensional changes of variables

This file records reusable calculus facts about elementary real charts that recur in density and special-function computations.

Main results

• TauCeti.div_one_sub_strictMonoOn, TauCeti.injOn_div_one_sub_Ioo, TauCeti.image_div_one_sub_Ioo, and TauCeti.hasDerivAt_div_one_sub describe the chart u ↦ u / (1 - u) on intervals below 1;
• TauCeti.image_sq_div_const_Ioi, TauCeti.injOn_sq_div_const_Ioi, and TauCeti.hasDerivAt_sq_div_const describe the square chart z ↦ z ^ 2 / ν on positive half-lines.

The chart u ↦ u / (1 - u)

theorem TauCeti.div_one_sub_strictMonoOn : StrictMonoOn (fun (u : ℝ) => u / (1 - u)) (Set.Iio 1)

The chart u ↦ u / (1 - u) is strictly increasing on (-∞, 1).

theorem TauCeti.injOn_div_one_sub_Ioo {u0 : ℝ} : Set.InjOn (fun (u : ℝ) => u / (1 - u)) (Set.Ioo u0 1)

The chart u ↦ u / (1 - u) is injective on (u₀, 1).

theorem TauCeti.image_div_one_sub_Ioo {u0 : ℝ} (hu1 : u0 < 1) : (fun (u : ℝ) => u / (1 - u)) '' Set.Ioo u0 1 = Set.Ioi (u0 / (1 - u0))

The chart u ↦ u / (1 - u) carries (u₀, 1) onto (u₀ / (1 - u₀), ∞) for u₀ < 1.

theorem TauCeti.hasDerivAt_div_one_sub {u : ℝ} (hu : u ≠ 1) : HasDerivAt (fun (t : ℝ) => t / (1 - t)) ((1 - u) ^ 2)⁻¹ u

The derivative of the chart u ↦ u / (1 - u) is (1 - u) ^ (-2).

The square chart on the positive half-line

theorem TauCeti.image_sq_div_const_Ioi {ν : ℝ} (hν : 0 < ν) {y : ℝ} (hy : 0 ≤ y) : (fun (z : ℝ) => z ^ 2 / ν) '' Set.Ioi y = Set.Ioi (y ^ 2 / ν)

The square chart z ↦ z ^ 2 / ν carries (y, ∞) onto (y ^ 2 / ν, ∞) for 0 ≤ y and 0 < ν.

theorem TauCeti.injOn_sq_div_const_Ioi {ν : ℝ} (hν : ν ≠ 0) : Set.InjOn (fun (z : ℝ) => z ^ 2 / ν) (Set.Ioi 0)

The chart z ↦ z ^ 2 / ν is injective on the positive half-line for nonzero ν.

theorem TauCeti.hasDerivAt_sq_div_const (ν z : ℝ) : HasDerivAt (fun (x : ℝ) => x ^ 2 / ν) (2 * z / ν) z

The derivative of the chart z ↦ z ^ 2 / ν.