Right way to get a constant out of an integral

Stream: new members

[Colin Jones ⚛️]

Hi,

I'm trying to prove the following statement, but am unable to pull the constant out the integral. Am I missing something? I don't know how to prove this.

import Mathlib

open Real

example : ∫ (x : ℝ) in Set.Ioi 1, (1/x) * 2 = 2 * ∫ (x : ℝ) in Set.Ioi 1, (1/x) := by
  simp_rw [integral_smul_const]

[Chris Wong]

What error message do you get?

[Chris Wong]

In docs#integral_smul_const, the constant is always on the right, but your example switches the constant to the left.

[Aaron Liu]

import Mathlib

open Real

example : ∫ (x : ℝ) in Set.Ioi 1, (1/x) * 2 = 2 * ∫ (x : ℝ) in Set.Ioi 1, (1/x) := by
  simp_rw [← smul_eq_mul, integral_smul_const, smul_eq_mul, mul_comm]

[Floris van Doorn]

There are indeed lemmas missing here. Analogous to docs#intervalIntegral.integral_mul_const it would be nice to have MeasureTheory.integral_mul_const and MeasureTheory.integral_const_mul. Please make a PR!

[Rémy Degenne]

MeasureTheory.integral_mul_right
We should change its name to integral_mul_const.

[Colin Jones ⚛️]

Thanks all. Is there a way to prove this too?

example : ∫ (x : ℝ) in Set.Ioi 1, x * (1/x^3) = ∫ (x : ℝ) in Set.Ioi 1, 1/x^2 := by
  field_simp

[Ruben Van de Velde]

Not without imports, I'm afraid

[Aaron Liu]

import Mathlib

example : ∫ (x : ℝ) in Set.Ioi 1, x * (1/x^3) = ∫ (x : ℝ) in Set.Ioi 1, 1/x^2 := by
  apply MeasureTheory.setIntegral_congr_fun (by measurability)
  intro x _
  by_cases hx : x = 0
  · subst hx
    simp
  · field_simp
    ring

[Colin Jones ⚛️]

Thanks for the help. I've also run into issues with proving integrability and fun_prop doesn't seem to work.

How would I prove something like:

example (\sigma : \R)  : Integrable (fun (r :\R) => -σ / r ^ 4) (volume.restrict (Set.Ioi rc)) := by

[Etienne Marion]

Can you provide a #mwe please?

[Colin Jones ⚛️]

example (σ : ℝ) : Integrable (fun a => σ / a ^ 10) (volume.restrict (Set.Ioi rc)) := by
  dsimp [Integrable]
  sorry

[Aaron Liu]

You need 0 < rc ∨ σ = 0 for this

[Colin Jones ⚛️]

Sorry forgot to include that condition

[Colin Jones ⚛️]

example (σ : ℝ) (hr : 0 < rc) : Integrable (fun a => σ / a ^ 10) (volume.restrict (Set.Ioi rc)) := by
  dsimp [Integrable]
  sorry

[Aaron Liu]

import Mathlib

open MeasureTheory

example (σ : ℝ) (hr : 0 < rc) : Integrable (fun a => σ / a ^ 10) (volume.restrict (Set.Ioi rc)) := by
  apply Integrable.const_mul
  rw [← IntegrableOn]
  have heq : Set.EqOn (fun x ↦ x ^ (-10 : ℝ)) (fun x ↦ (x ^ 10)⁻¹) (Set.Ioi rc) := by
    intro x hx
    simp_rw [Real.rpow_neg (hr.trans hx).le, ← Real.rpow_natCast, Nat.cast_ofNat]
  refine IntegrableOn.congr_fun ?_ heq (by measurability)
  exact integrableOn_Ioi_rpow_of_lt (by norm_num) hr

[Etienne Marion]

Colin Jones ⚛️ said:

Sorry forgot to include that condition

This is still not a #mwe, imports are missing