Skip to main content
therefore
Sign inSign up
Open navigation
AlexKontorovich/PrimeNumberTheoremAnd
Source indexedlemma Β· leanprover/lean4:v4.32.0

MeasureTheory.integral_comp_inv_I0i_haar

PrimeNumberTheoremAnd.MellinCalculus Β· PrimeNumberTheoremAnd/MellinCalculus.lean:65 to 74

Mathematical statement

Exact Lean statement

lemma MeasureTheory.integral_comp_inv_I0i_haar (f : ℝ β†’ 𝕂) :
    ∫ (y : ℝ) in Ioi 0, f (1 / y) / y = ∫ (y : ℝ) in Ioi 0, f y / y

Complete declaration

Lean source

Canonical source
Full Lean sourceLean 4
lemma MeasureTheory.integral_comp_inv_I0i_haar (f : ℝ β†’ 𝕂) :    ∫ (y : ℝ) in Ioi 0, f (1 / y) / y = ∫ (y : ℝ) in Ioi 0, f y / y := by  have := integral_comp_rpow_Ioi (fun y ↦ f y / y) (p := -1) (by simp)  rw [← this, setIntegral_congr_fun (by simp)]  intro y hy  have : (y : 𝕂) β‰  0 := (RCLike.ofReal_ne_zero).mpr <| LT.lt.ne' hy  simp only [abs_neg, abs_one, rpow_neg_one, map_invβ‚€, div_inv_eq_mul,    RCLike.real_smul_eq_coe_mul, RCLike.algebraMap_eq_ofReal]  ring_nf  simp [field]