Theorem: Smooth1LeOne_aux (PrimeNumberTheoremAnd/MellinCalculus.lean)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
Ψ : ℝ → ℝ
xpos : 0 < x
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
Tactic:
calc
  _ = ∫ (y : ℝ) in Ioi 0, (Ψ (y ^ (1 / ε)) / ε) / y := ?_
  _ = ∫ (y : ℝ) in Ioi 0, Ψ y / y := ?_
  _ = 1 := mass_one
State after:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
Ψ : ℝ → ℝ
xpos : 0 < x
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = ∫ (y : ℝ) in Ioi 0, Ψ (y ^ (1 / ε)) / ε / y

case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
Ψ : ℝ → ℝ
xpos : 0 < x
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ ∫ (y : ℝ) in Ioi 0, Ψ (y ^ (1 / ε)) / ε / y = ∫ (y : ℝ) in Ioi 0, Ψ y / y

State before:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
Ψ : ℝ → ℝ
xpos : 0 < x
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = ∫ (y : ℝ) in Ioi 0, Ψ (y ^ (1 / ε)) / ε / y
Tactic:
have := integral_comp_div_I0i_haar (fun y ↦ Ψ ((x / y) ^ (1 / ε)) / ε) xpos
State after:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
Ψ : ℝ → ℝ
xpos : 0 < x
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
this :
  ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) (x / y) / ↑y =
    ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) y / ↑y
⊢ ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = ∫ (y : ℝ) in Ioi 0, Ψ (y ^ (1 / ε)) / ε / y

State before:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
Ψ : ℝ → ℝ
xpos : 0 < x
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
this :
  ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) (x / y) / ↑y =
    ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) y / ↑y
⊢ ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = ∫ (y : ℝ) in Ioi 0, Ψ (y ^ (1 / ε)) / ε / y
Tactic:
convert this.symm using 1
State after:
case h.e'_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
Ψ : ℝ → ℝ
xpos : 0 < x
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
this :
  ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) (x / y) / ↑y =
    ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) y / ↑y
⊢ ∫ (y : ℝ) in Ioi 0, Ψ (y ^ (1 / ε)) / ε / y = ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) (x / y) / ↑y

State before:
case h.e'_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
Ψ : ℝ → ℝ
xpos : 0 < x
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
this :
  ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) (x / y) / ↑y =
    ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) y / ↑y
⊢ ∫ (y : ℝ) in Ioi 0, Ψ (y ^ (1 / ε)) / ε / y = ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) (x / y) / ↑y
Tactic:
congr
State after:
case h.e'_3.e_f
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
Ψ : ℝ → ℝ
xpos : 0 < x
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
this :
  ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) (x / y) / ↑y =
    ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) y / ↑y
⊢ (fun y => Ψ (y ^ (1 / ε)) / ε / y) = fun y => (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) (x / y) / ↑y

State before:
case h.e'_3.e_f
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
Ψ : ℝ → ℝ
xpos : 0 < x
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
this :
  ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) (x / y) / ↑y =
    ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) y / ↑y
⊢ (fun y => Ψ (y ^ (1 / ε)) / ε / y) = fun y => (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) (x / y) / ↑y
Tactic:
funext y
State after:
case h.e'_3.e_f.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
Ψ : ℝ → ℝ
xpos : 0 < x
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
this :
  ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) (x / y) / ↑y =
    ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) y / ↑y
y : ℝ
⊢ Ψ (y ^ (1 / ε)) / ε / y = (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) (x / y) / ↑y

State before:
case h.e'_3.e_f.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
Ψ : ℝ → ℝ
xpos : 0 < x
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
this :
  ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) (x / y) / ↑y =
    ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) y / ↑y
y : ℝ
⊢ Ψ (y ^ (1 / ε)) / ε / y = (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) (x / y) / ↑y
Tactic:
congr
State after:
case h.e'_3.e_f.h.e_a.e_a.e_a.e_a
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
Ψ : ℝ → ℝ
xpos : 0 < x
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
this :
  ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) (x / y) / ↑y =
    ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) y / ↑y
y : ℝ
⊢ y = x / (x / y)

State before:
case h.e'_3.e_f.h.e_a.e_a.e_a.e_a
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
Ψ : ℝ → ℝ
xpos : 0 < x
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
this :
  ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) (x / y) / ↑y =
    ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) y / ↑y
y : ℝ
⊢ y = x / (x / y)
Tactic:
field_simp [mul_comm]
State after:
no goals

State before:
case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
Ψ : ℝ → ℝ
xpos : 0 < x
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ ∫ (y : ℝ) in Ioi 0, Ψ (y ^ (1 / ε)) / ε / y = ∫ (y : ℝ) in Ioi 0, Ψ y / y
Tactic:
have := integral_comp_rpow_I0i_haar_real (fun y ↦ Ψ y) (one_div_ne_zero εpos.ne')
State after:
case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
Ψ : ℝ → ℝ
xpos : 0 < x
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
this : ∫ (y : ℝ) in Ioi 0, |1 / ε| * (fun y => Ψ y) (y ^ (1 / ε)) / y = ∫ (y : ℝ) in Ioi 0, (fun y => Ψ y) y / y
⊢ ∫ (y : ℝ) in Ioi 0, Ψ (y ^ (1 / ε)) / ε / y = ∫ (y : ℝ) in Ioi 0, Ψ y / y

State before:
case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
Ψ : ℝ → ℝ
xpos : 0 < x
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
this : ∫ (y : ℝ) in Ioi 0, |1 / ε| * (fun y => Ψ y) (y ^ (1 / ε)) / y = ∫ (y : ℝ) in Ioi 0, (fun y => Ψ y) y / y
⊢ ∫ (y : ℝ) in Ioi 0, Ψ (y ^ (1 / ε)) / ε / y = ∫ (y : ℝ) in Ioi 0, Ψ y / y
Tactic:
field_simp [ ← this, abs_of_pos <| one_div_pos.mpr εpos]
State after:
no goals