Theorem: MellinOf1 (PrimeNumberTheoremAnd/MellinCalculus.lean)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
s : ℂ
h : s.re > 0
⊢ 𝓜 (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) s = 1 / s
Tactic:
convert (hasMellin_one_Ioc h).right using 1
State after:
case h.e'_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
s : ℂ
h : s.re > 0
⊢ 𝓜 (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) s = mellin ((Ioc 0 1).indicator fun x => 1) s

State before:
case h.e'_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
s : ℂ
h : s.re > 0
⊢ 𝓜 (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) s = mellin ((Ioc 0 1).indicator fun x => 1) s
Tactic:
apply setIntegral_congr_ae measurableSet_Ioi
State after:
case h.e'_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
s : ℂ
h : s.re > 0
⊢ ∀ᵐ (x : ℝ),
    x ∈ Ioi 0 →
      (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) x * ↑x ^ (s - 1) = ↑x ^ (s - 1) • (Ioc 0 1).indicator (fun x => 1) x

State before:
case h.e'_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
s : ℂ
h : s.re > 0
⊢ ∀ᵐ (x : ℝ),
    x ∈ Ioi 0 →
      (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) x * ↑x ^ (s - 1) = ↑x ^ (s - 1) • (Ioc 0 1).indicator (fun x => 1) x
Tactic:
filter_upwards with _ _
State after:
case h.e'_2.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
s : ℂ
h : s.re > 0
a✝¹ : ℝ
a✝ : a✝¹ ∈ Ioi 0
⊢ (if 0 < a✝¹ ∧ a✝¹ ≤ 1 then 1 else 0) * ↑a✝¹ ^ (s - 1) = ↑a✝¹ ^ (s - 1) • (Ioc 0 1).indicator (fun x => 1) a✝¹

State before:
case h.e'_2.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
s : ℂ
h : s.re > 0
a✝¹ : ℝ
a✝ : a✝¹ ∈ Ioi 0
⊢ (if 0 < a✝¹ ∧ a✝¹ ≤ 1 then 1 else 0) * ↑a✝¹ ^ (s - 1) = ↑a✝¹ ^ (s - 1) • (Ioc 0 1).indicator (fun x => 1) a✝¹
Tactic:
rw [smul_eq_mul, mul_comm]
State after:
case h.e'_2.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
s : ℂ
h : s.re > 0
a✝¹ : ℝ
a✝ : a✝¹ ∈ Ioi 0
⊢ (↑a✝¹ ^ (s - 1) * if 0 < a✝¹ ∧ a✝¹ ≤ 1 then 1 else 0) = ↑a✝¹ ^ (s - 1) * (Ioc 0 1).indicator (fun x => 1) a✝¹

State before:
case h.e'_2.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
s : ℂ
h : s.re > 0
a✝¹ : ℝ
a✝ : a✝¹ ∈ Ioi 0
⊢ (↑a✝¹ ^ (s - 1) * if 0 < a✝¹ ∧ a✝¹ ≤ 1 then 1 else 0) = ↑a✝¹ ^ (s - 1) * (Ioc 0 1).indicator (fun x => 1) a✝¹
Tactic:
congr
State after:
no goals