Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.integral_comp_mul_right_I0i_haar

PrimeNumberTheoremAnd.MellinCalculus · PrimeNumberTheoremAnd/MellinCalculus.lean:34 to 44

Mathematical statement

Exact Lean statement

lemma MeasureTheory.integral_comp_mul_right_I0i_haar
    (f : ℝ → 𝕂) {a : ℝ} (ha : 0 < a) :
    ∫ (y : ℝ) in Ioi 0, f (y * a) / y = ∫ (y : ℝ) in Ioi 0, f y / y

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma MeasureTheory.integral_comp_mul_right_I0i_haar    (f : ℝ → 𝕂) {a : ℝ} (ha : 0 < a) :    ∫ (y : ℝ) in Ioi 0, f (y * a) / y = ∫ (y : ℝ) in Ioi 0, f y / y := by  have := integral_comp_mul_right_Ioi (fun y ↦ f y / y) 0 ha  simp only [RCLike.ofReal_mul, zero_mul, eq_inv_smul_iff₀ (ne_of_gt ha)] at this  rw [← integral_smul] at this  rw [← this, setIntegral_congr_fun (by simp)]  intro _ _  simp only [RCLike.real_smul_eq_coe_mul]  rw [mul_comm (a : 𝕂), div_mul, mul_div_assoc, div_self ?_, mul_one]  exact (RCLike.ofReal_ne_zero).mpr <| ne_of_gt ha