Theorem: DeltaSpikeMass (PrimeNumberTheoremAnd/MellinCalculus.lean)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
⊢ ∫ (x : ℝ) in Ioi 0, DeltaSpike Ψ ε x / x =
    ∫ (x : ℝ) in Ioi 0, (|1 / ε| * x ^ (1 / ε - 1)) • (fun z => Ψ z / z) (x ^ (1 / ε))
Tactic:
apply setIntegral_congr_ae measurableSet_Ioi
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
⊢ ∀ᵐ (x : ℝ), x ∈ Ioi 0 → DeltaSpike Ψ ε x / x = (|1 / ε| * x ^ (1 / ε - 1)) • (fun z => Ψ z / z) (x ^ (1 / ε))

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
⊢ ∀ᵐ (x : ℝ), x ∈ Ioi 0 → DeltaSpike Ψ ε x / x = (|1 / ε| * x ^ (1 / ε - 1)) • (fun z => Ψ z / z) (x ^ (1 / ε))
Tactic:
filter_upwards with x hx
State after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
hx : x ∈ Ioi 0
⊢ DeltaSpike Ψ ε x / x = (|1 / ε| * x ^ (1 / ε - 1)) • (Ψ (x ^ (1 / ε)) / x ^ (1 / ε))

State before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
hx : x ∈ Ioi 0
⊢ DeltaSpike Ψ ε x / x = (|1 / ε| * x ^ (1 / ε - 1)) • (Ψ (x ^ (1 / ε)) / x ^ (1 / ε))
Tactic:
simp only [mem_Ioi, smul_eq_mul, abs_of_pos (one_div_pos.mpr εpos)]
State after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
hx : x ∈ Ioi 0
⊢ DeltaSpike Ψ ε x / x = 1 / ε * x ^ (1 / ε - 1) * (Ψ (x ^ (1 / ε)) / x ^ (1 / ε))

State before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
hx : x ∈ Ioi 0
⊢ DeltaSpike Ψ ε x / x = 1 / ε * x ^ (1 / ε - 1) * (Ψ (x ^ (1 / ε)) / x ^ (1 / ε))
Tactic:
symm
State after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
hx : x ∈ Ioi 0
⊢ 1 / ε * x ^ (1 / ε - 1) * (Ψ (x ^ (1 / ε)) / x ^ (1 / ε)) = DeltaSpike Ψ ε x / x

State before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
hx : x ∈ Ioi 0
⊢ 1 / ε * x ^ (1 / ε - 1) * (Ψ (x ^ (1 / ε)) / x ^ (1 / ε)) = DeltaSpike Ψ ε x / x
Tactic:
calc
_ = (Ψ (x ^ (1 / ε)) / x ^ (1 / ε)) * x ^ (1 / ε - 1) * (1 / ε) := by ring
_ = _ := by rw [rpow_sub hx, rpow_one]
_ = (Ψ (x ^ (1 / ε)) / x ^ (1 / ε) * x ^ (1 / ε) / x) * (1/ ε) := by ring
_ = _ := by rw [div_mul_cancel₀ _ (ne_of_gt (rpow_pos_of_pos hx (1/ε)))]
_ = (Ψ (x ^ (1 / ε)) / ε / x) := by ring
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
hx : x ∈ Ioi 0
⊢ 1 / ε * x ^ (1 / ε - 1) * (Ψ (x ^ (1 / ε)) / x ^ (1 / ε)) = Ψ (x ^ (1 / ε)) / x ^ (1 / ε) * x ^ (1 / ε - 1) * (1 / ε)
Tactic:
ring
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
hx : x ∈ Ioi 0
⊢ Ψ (x ^ (1 / ε)) / x ^ (1 / ε) * x ^ (1 / ε - 1) * (1 / ε) = ?m.397146
Tactic:
rw [rpow_sub hx, rpow_one]
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
hx : x ∈ Ioi 0
⊢ Ψ (x ^ (1 / ε)) / x ^ (1 / ε) * (x ^ (1 / ε) / x) * (1 / ε) =
    Ψ (x ^ (1 / ε)) / x ^ (1 / ε) * x ^ (1 / ε) / x * (1 / ε)
Tactic:
ring
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
hx : x ∈ Ioi 0
⊢ Ψ (x ^ (1 / ε)) / x ^ (1 / ε) * x ^ (1 / ε) / x * (1 / ε) = ?m.397745
Tactic:
rw [div_mul_cancel₀ _ (ne_of_gt (rpow_pos_of_pos hx (1/ε)))]
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
hx : x ∈ Ioi 0
⊢ Ψ (x ^ (1 / ε)) / x * (1 / ε) = Ψ (x ^ (1 / ε)) / ε / x
Tactic:
ring
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
⊢ ∫ (x : ℝ) in Ioi 0, (|1 / ε| * x ^ (1 / ε - 1)) • (fun z => Ψ z / z) (x ^ (1 / ε)) = 1
Tactic:
rw [integral_comp_rpow_Ioi (fun z ↦ (Ψ z) / z), ← mass_one]
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
⊢ 1 / ε ≠ 0

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
⊢ 1 / ε ≠ 0
Tactic:
simp only [ne_eq, div_eq_zero_iff, one_ne_zero, εpos.ne', or_self, not_false_eq_true]
State after:
no goals