feat(measure_theory/integral): change of variables for integrals over…

… `Ioi` domains (#17542)

This is the change-of-variable formula for integrals over one-sided infinite integrals.

- [x] depends on: #17540

src/measure_theory/function/jacobian.lean

@@ -1243,6 +1243,25 @@ begin
   refl
 end
 
+/-- Change of variable formula for differentiable functions (one-variable version): if a function
+`f` is injective and differentiable on a measurable set `s ⊆ ℝ`, then the Bochner integral of a
+function `g : ℝ → F` on `f '' s` coincides with the integral of `|(f' x).det| • g ∘ f` on `s`. -/
+theorem integral_image_eq_integral_abs_deriv_smul {s : set ℝ} {f : ℝ → ℝ} {f' : ℝ → ℝ}
+  [complete_space F] (hs : measurable_set s) (hf' : ∀ x ∈ s, has_deriv_within_at f (f' x) s x)
+  (hf : inj_on f s) (g : ℝ → F) :
+  ∫ x in f '' s, g x = ∫ x in s, |(f' x)| • g (f x) :=
+begin
+  convert integral_image_eq_integral_abs_det_fderiv_smul volume hs
+    (λ x hx, (hf' x hx).has_fderiv_within_at) hf g,
+  ext1 x,
+  rw (by { ext, simp } : (1 : ℝ →L[ℝ] ℝ).smul_right (f' x) = (f' x) • (1 : ℝ →L[ℝ] ℝ)),
+  rw [continuous_linear_map.det, continuous_linear_map.coe_smul],
+  have : ((1 : ℝ →L[ℝ] ℝ) : ℝ →ₗ[ℝ] ℝ) = (1 : ℝ →ₗ[ℝ] ℝ) := by refl,
+  rw [this, linear_map.det_smul, finite_dimensional.finrank_self],
+  suffices : (1 : ℝ →ₗ[ℝ] ℝ).det = 1, { rw this, simp },
+  exact linear_map.det_id,
+end
+
 theorem integral_target_eq_integral_abs_det_fderiv_smul [complete_space F]
   {f : local_homeomorph E E} (hf' : ∀ x ∈ f.source, has_fderiv_at f (f' x) x) (g : E → F) :
   ∫ x in f.target, g x ∂μ = ∫ x in f.source, |(f' x).det| • g (f x) ∂μ :=

src/measure_theory/integral/integral_eq_improper.lean

@@ -5,6 +5,7 @@ Authors: Anatole Dedecker, Bhavik Mehta
 -/
 import measure_theory.integral.interval_integral
 import order.filter.at_top_bot
+import measure_theory.function.jacobian
 
 /-!
 # Links between an integral and its "improper" version
@@ -659,4 +660,93 @@ end
 
 end integral_of_interval_integral
 
+section Ioi_change_variables
+
+open real
+open_locale interval
+
+variables {E : Type*} {μ : measure ℝ} {f : ℝ → E}
+  [normed_add_comm_group E] [normed_space ℝ E] [complete_space E]
+
+/-- Change-of-variables formula for `Ioi` integrals of vector-valued functions, proved by taking
+limits from the result for finite intervals. -/
+lemma integral_comp_smul_deriv_Ioi {f f' : ℝ → ℝ} {g : ℝ → E} {a : ℝ}
+  (hf : continuous_on f $ Ici a)
+  (hft : tendsto f at_top at_top)
+  (hff' : ∀ x ∈ Ioi a, has_deriv_within_at f (f' x) (Ioi x) x)
+  (hg_cont : continuous_on g $ f '' Ioi a)
+  (hg1 : integrable_on g $ f '' Ici a)
+  (hg2 : integrable_on (λ x, f' x • (g ∘ f) x) (Ici a)) :
+  ∫ x in Ioi a, f' x • (g ∘ f) x = ∫ u in Ioi (f a), g u :=
+begin
+  have eq : ∀ b : ℝ, a < b → ∫ x in a..b, f' x • (g ∘ f) x = ∫ u in f a .. f b, g u,
+  { intros b hb,
+    have i1 : Ioo (min a b) (max a b) ⊆ Ioi a,
+    { rw min_eq_left hb.le, exact Ioo_subset_Ioi_self },
+    have i2 : [a, b] ⊆ Ici a,
+    { rw interval_of_le hb.le, exact Icc_subset_Ici_self },
+    refine interval_integral.integral_comp_smul_deriv''' (hf.mono i2)
+      (λ x hx, hff' x $ mem_of_mem_of_subset hx i1) (hg_cont.mono $ image_subset _ _)
+      (hg1.mono_set $ image_subset _ _) (hg2.mono_set i2),
+    { rw min_eq_left hb.le, exact Ioo_subset_Ioi_self },
+    { rw interval_of_le hb.le, exact Icc_subset_Ici_self } },
+  rw integrable_on_Ici_iff_integrable_on_Ioi at hg2,
+  have t2 := interval_integral_tendsto_integral_Ioi _ hg2 tendsto_id,
+  have : Ioi (f a) ⊆ f '' Ici a := (Ioi_subset_Ici_self.trans $
+    is_preconnected.intermediate_value_Ici is_preconnected_Ici left_mem_Ici
+    (le_principal_iff.mpr $ Ici_mem_at_top _) hf hft),
+  have t1 := (interval_integral_tendsto_integral_Ioi _ (hg1.mono_set this) tendsto_id).comp hft,
+  exact tendsto_nhds_unique (tendsto.congr' (eventually_eq_of_mem (Ioi_mem_at_top a) eq) t2) t1,
+end
+
+/-- Change-of-variables formula for `Ioi` integrals of scalar-valued functions -/
+lemma integral_comp_mul_deriv_Ioi {f f' : ℝ → ℝ} {g : ℝ → ℝ} {a : ℝ}
+  (hf : continuous_on f $ Ici a)
+  (hft : tendsto f at_top at_top)
+  (hff' : ∀ x ∈ Ioi a, has_deriv_within_at f (f' x) (Ioi x) x)
+  (hg_cont : continuous_on g $ f '' Ioi a)
+  (hg1 : integrable_on g $ f '' Ici a)
+  (hg2 : integrable_on (λ x, (g ∘ f) x * f' x) (Ici a)) :
+  ∫ x in Ioi a, (g ∘ f) x * f' x = ∫ u in Ioi (f a), g u :=
+begin
+  have hg2' : integrable_on (λ x, f' x • (g ∘ f) x) (Ici a) := by simpa [mul_comm] using hg2,
+  simpa [mul_comm] using integral_comp_smul_deriv_Ioi hf hft hff' hg_cont hg1 hg2',
+end
+
+/-- Substitution `y = x ^ p` in integrals over `Ioi 0` -/
+lemma integral_comp_rpow_Ioi (g : ℝ → E) {p : ℝ} (hp : p ≠ 0) :
+  ∫ x in Ioi 0, (|p| * x ^ (p - 1)) • g (x ^ p) = ∫ y in Ioi 0, g y :=
+begin
+  let S := Ioi (0 : ℝ),
+  have a1 : ∀ x:ℝ, x ∈ S → has_deriv_within_at (λ (t:ℝ), t ^ p) (p * x ^ (p - 1)) S x :=
+    λ x hx, (has_deriv_at_rpow_const (or.inl (mem_Ioi.mp hx).ne')).has_deriv_within_at,
+  have a2 : inj_on (λ x:ℝ, x ^ p) S,
+  { rcases lt_or_gt_of_ne hp,
+    { apply strict_anti_on.inj_on,
+      intros x hx y hy hxy,
+      rw [←inv_lt_inv (rpow_pos_of_pos hx p) (rpow_pos_of_pos hy p),
+      ←rpow_neg (le_of_lt hx), ←rpow_neg (le_of_lt hy)],
+      exact rpow_lt_rpow (le_of_lt hx) hxy (neg_pos.mpr h), },
+    exact strict_mono_on.inj_on (λ x hx y hy hxy, rpow_lt_rpow (mem_Ioi.mp hx).le hxy h),},
+  have a3 : (λ (t : ℝ), t ^ p) '' S = S,
+  { ext1, rw mem_image, split,
+    { rintro ⟨y, hy, rfl⟩, exact rpow_pos_of_pos hy p },
+    { intro hx, refine ⟨x ^ (1 / p), rpow_pos_of_pos hx _, _⟩,
+      rw [←rpow_mul (le_of_lt hx), one_div_mul_cancel hp, rpow_one], } },
+  have := integral_image_eq_integral_abs_deriv_smul measurable_set_Ioi a1 a2 g,
+  rw a3 at this, rw this,
+  refine set_integral_congr measurable_set_Ioi _,
+  intros x hx, dsimp only,
+  rw [abs_mul, abs_of_nonneg (rpow_nonneg_of_nonneg (le_of_lt hx) _)],
+end
+
+lemma integral_comp_rpow_Ioi_of_pos {g : ℝ → E} {p : ℝ} (hp : 0 < p) :
+  ∫ x in Ioi 0, (p * x ^ (p - 1)) • g (x ^ p) = ∫ y in Ioi 0, g y :=
+begin
+  convert integral_comp_rpow_Ioi g hp.ne',
+  funext, congr, rw abs_of_nonneg hp.le,
+end
+
+end Ioi_change_variables
+
 end measure_theory