internlm/Lean-Github huggingface dataset:
Theorem: MellinOfDeltaSpike
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
⊢ ∫ (x : ℝ) in Ioi 0, (fun x => ↑(Ψ (x ^ (1 / ε)) / ε)) x * ↑x ^ (s - 1) =
    ∫ (x : ℝ) in Ioi 0, (fun x => ↑(Ψ x)) x * ↑x ^ (↑ε * s - 1)
Tactic:
rw [← integral_comp_rpow_Ioi (fun z ↦ ((Ψ z) : ℂ) * (z : ℂ) ^ ((ε : ℂ) * s - 1))
  (one_div_ne_zero (ne_of_gt εpos))]
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
⊢ ∫ (x : ℝ) in Ioi 0, (fun x => ↑(Ψ (x ^ (1 / ε)) / ε)) x * ↑x ^ (s - 1) =
    ∫ (x : ℝ) in Ioi 0, (|1 / ε| * x ^ (1 / ε - 1)) • (↑(Ψ (x ^ (1 / ε))) * ↑(x ^ (1 / ε)) ^ (↑ε * s - 1))
Theorem: MellinOfDeltaSpike
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
⊢ ∫ (x : ℝ) in Ioi 0, (fun x => ↑(Ψ (x ^ (1 / ε)) / ε)) x * ↑x ^ (s - 1) =
    ∫ (x : ℝ) in Ioi 0, (|1 / ε| * x ^ (1 / ε - 1)) • (↑(Ψ (x ^ (1 / ε))) * ↑(x ^ (1 / ε)) ^ (↑ε * s - 1))
Tactic:
apply setIntegral_congr_ae measurableSet_Ioi
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
⊢ ∀ᵐ (x : ℝ),
    x ∈ Ioi 0 →
      (fun x => ↑(Ψ (x ^ (1 / ε)) / ε)) x * ↑x ^ (s - 1) =
        (|1 / ε| * x ^ (1 / ε - 1)) • (↑(Ψ (x ^ (1 / ε))) * ↑(x ^ (1 / ε)) ^ (↑ε * s - 1))
Theorem: MellinOfDeltaSpike
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
⊢ ∀ᵐ (x : ℝ),
    x ∈ Ioi 0 →
      (fun x => ↑(Ψ (x ^ (1 / ε)) / ε)) x * ↑x ^ (s - 1) =
        (|1 / ε| * x ^ (1 / ε - 1)) • (↑(Ψ (x ^ (1 / ε))) * ↑(x ^ (1 / ε)) ^ (↑ε * s - 1))
Tactic:
filter_upwards with x hx
Proof state after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
⊢ ↑(Ψ (x ^ (1 / ε)) / ε) * ↑x ^ (s - 1) =
    (|1 / ε| * x ^ (1 / ε - 1)) • (↑(Ψ (x ^ (1 / ε))) * ↑(x ^ (1 / ε)) ^ (↑ε * s - 1))
Theorem: MellinOfDeltaSpike
Proof state before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
⊢ ↑(Ψ (x ^ (1 / ε)) / ε) * ↑x ^ (s - 1) =
    (|1 / ε| * x ^ (1 / ε - 1)) • (↑(Ψ (x ^ (1 / ε))) * ↑(x ^ (1 / ε)) ^ (↑ε * s - 1))
Tactic:
have log_x_real: (Complex.log (x : ℂ)).im = 0 := by
  rw [← ofReal_log, ofReal_im]
  exact LT.lt.le hx
Proof state after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ ↑(Ψ (x ^ (1 / ε)) / ε) * ↑x ^ (s - 1) =
    (|1 / ε| * x ^ (1 / ε - 1)) • (↑(Ψ (x ^ (1 / ε))) * ↑(x ^ (1 / ε)) ^ (↑ε * s - 1))
Theorem: MellinOfDeltaSpike
Proof state before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ ↑(Ψ (x ^ (1 / ε)) / ε) * ↑x ^ (s - 1) =
    (|1 / ε| * x ^ (1 / ε - 1)) • (↑(Ψ (x ^ (1 / ε))) * ↑(x ^ (1 / ε)) ^ (↑ε * s - 1))
Tactic:
rw [div_eq_mul_inv, ofReal_mul, abs_of_pos (one_div_pos.mpr εpos)]
Proof state after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ ↑(Ψ (x ^ (1 / ε))) * ↑ε⁻¹ * ↑x ^ (s - 1) =
    (1 / ε * x ^ (1 / ε - 1)) • (↑(Ψ (x ^ (1 / ε))) * ↑(x ^ (1 / ε)) ^ (↑ε * s - 1))
Theorem: MellinOfDeltaSpike
Proof state before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ ↑(Ψ (x ^ (1 / ε))) * ↑ε⁻¹ * ↑x ^ (s - 1) =
    (1 / ε * x ^ (1 / ε - 1)) • (↑(Ψ (x ^ (1 / ε))) * ↑(x ^ (1 / ε)) ^ (↑ε * s - 1))
Tactic:
simp only [real_smul, ofReal_mul, ofReal_div, ofReal_one, Complex.ofReal_rpow hx]
Proof state after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ ↑(Ψ (x ^ (1 / ε))) * ↑ε⁻¹ * ↑x ^ (s - 1) =
    1 / ↑ε * ↑x ^ ↑(1 / ε - 1) * (↑(Ψ (x ^ (1 / ε))) * (↑x ^ (1 / ↑ε)) ^ (↑ε * s - 1))
Theorem: MellinOfDeltaSpike
Proof state before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ ↑(Ψ (x ^ (1 / ε))) * ↑ε⁻¹ * ↑x ^ (s - 1) =
    1 / ↑ε * ↑x ^ ↑(1 / ε - 1) * (↑(Ψ (x ^ (1 / ε))) * (↑x ^ (1 / ↑ε)) ^ (↑ε * s - 1))
Tactic:
rw [← Complex.cpow_mul _ ?_ ?_, mul_sub]
Proof state after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ ↑(Ψ (x ^ (1 / ε))) * ↑ε⁻¹ * ↑x ^ (s - 1) =
    1 / ↑ε * ↑x ^ ↑(1 / ε - 1) * (↑(Ψ (x ^ (1 / ε))) * ↑x ^ (1 / ↑ε * (↑ε * s) - 1 / ↑ε * 1))

𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ -π < ((↑x).log * (1 / ↑ε)).im

𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ ((↑x).log * (1 / ↑ε)).im ≤ π
Theorem: MellinOfDeltaSpike
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
⊢ (↑x).log.im = 0
Tactic:
rw [← ofReal_log, ofReal_im]
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
⊢ 0 ≤ x
Theorem: MellinOfDeltaSpike
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
⊢ 0 ≤ x
Tactic:
exact LT.lt.le hx
Proof state after:
no goals
Theorem: MellinOfDeltaSpike
Proof state before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ ↑(Ψ (x ^ (1 / ε))) * ↑ε⁻¹ * ↑x ^ (s - 1) =
    1 / ↑ε * ↑x ^ ↑(1 / ε - 1) * (↑(Ψ (x ^ (1 / ε))) * ↑x ^ (1 / ↑ε * (↑ε * s) - 1 / ↑ε * 1))
Tactic:
simp only [← mul_assoc, ofReal_sub, ofReal_div, ofReal_one, mul_one, ofReal_inv]
Proof state after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ ↑(Ψ (x ^ (1 / ε))) * (↑ε)⁻¹ * ↑x ^ (s - 1) =
    1 / ↑ε * ↑x ^ (1 / ↑ε - 1) * ↑(Ψ (x ^ (1 / ε))) * ↑x ^ (1 / ↑ε * ↑ε * s - 1 / ↑ε)
Theorem: MellinOfDeltaSpike
Proof state before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ ↑(Ψ (x ^ (1 / ε))) * (↑ε)⁻¹ * ↑x ^ (s - 1) =
    1 / ↑ε * ↑x ^ (1 / ↑ε - 1) * ↑(Ψ (x ^ (1 / ε))) * ↑x ^ (1 / ↑ε * ↑ε * s - 1 / ↑ε)
Tactic:
symm
Proof state after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ 1 / ↑ε * ↑x ^ (1 / ↑ε - 1) * ↑(Ψ (x ^ (1 / ε))) * ↑x ^ (1 / ↑ε * ↑ε * s - 1 / ↑ε) =
    ↑(Ψ (x ^ (1 / ε))) * (↑ε)⁻¹ * ↑x ^ (s - 1)
Theorem: MellinOfDeltaSpike
Proof state before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ 1 / ↑ε * ↑x ^ (1 / ↑ε - 1) * ↑(Ψ (x ^ (1 / ε))) * ↑x ^ (1 / ↑ε * ↑ε * s - 1 / ↑ε) =
    ↑(Ψ (x ^ (1 / ε))) * (↑ε)⁻¹ * ↑x ^ (s - 1)
Tactic:
rw [one_div_mul_cancel (by exact slitPlane_ne_zero (Or.inl εpos)), mul_comm (1 / (ε:ℂ)),
    mul_comm, ← mul_assoc, ← mul_assoc]
Proof state after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ ↑x ^ (1 * s - 1 / ↑ε) * ↑x ^ (1 / ↑ε - 1) * (1 / ↑ε) * ↑(Ψ (x ^ (1 / ε))) = ↑(Ψ (x ^ (1 / ε))) * (↑ε)⁻¹ * ↑x ^ (s - 1)
Theorem: MellinOfDeltaSpike
Proof state before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ ↑x ^ (1 * s - 1 / ↑ε) * ↑x ^ (1 / ↑ε - 1) * (1 / ↑ε) * ↑(Ψ (x ^ (1 / ε))) = ↑(Ψ (x ^ (1 / ε))) * (↑ε)⁻¹ * ↑x ^ (s - 1)
Tactic:
rw [← Complex.cpow_add _ _ (by exact slitPlane_ne_zero (Or.inl hx))]
Proof state after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ ↑x ^ (1 * s - 1 / ↑ε + (1 / ↑ε - 1)) * (1 / ↑ε) * ↑(Ψ (x ^ (1 / ε))) = ↑(Ψ (x ^ (1 / ε))) * (↑ε)⁻¹ * ↑x ^ (s - 1)
Theorem: MellinOfDeltaSpike
Proof state before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ ↑x ^ (1 * s - 1 / ↑ε + (1 / ↑ε - 1)) * (1 / ↑ε) * ↑(Ψ (x ^ (1 / ε))) = ↑(Ψ (x ^ (1 / ε))) * (↑ε)⁻¹ * ↑x ^ (s - 1)
Tactic:
ring_nf
Proof state after:
no goals
Theorem: MellinOfDeltaSpike
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ ↑ε ≠ 0
Tactic:
exact slitPlane_ne_zero (Or.inl εpos)
Proof state after:
no goals
Theorem: MellinOfDeltaSpike
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ ↑x ≠ 0
Tactic:
exact slitPlane_ne_zero (Or.inl hx)
Proof state after:
no goals
Theorem: MellinOfDeltaSpike
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ -π < ((↑x).log * (1 / ↑ε)).im
Tactic:
simp [im_mul_ofReal, log_x_real, zero_mul, pi_pos]
Proof state after:
no goals
Theorem: MellinOfDeltaSpike
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ ((↑x).log * (1 / ↑ε)).im ≤ π
Tactic:
simp [im_mul_ofReal, log_x_real, zero_mul, pi_nonneg]
Proof state after:
no goals
Theorem: MellinOfDeltaSpikeAt1
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
⊢ 𝓜 (fun x => ↑(DeltaSpike Ψ ε x)) 1 = 𝓜 (fun x => ↑(Ψ x)) ↑ε
Tactic:
convert MellinOfDeltaSpike Ψ εpos 1
Proof state after:
case h.e'_3.h.e'_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
⊢ ↑ε = ↑ε * 1
Theorem: MellinOfDeltaSpikeAt1
Proof state before:
case h.e'_3.h.e'_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
⊢ ↑ε = ↑ε * 1
Tactic:
simp [mul_one]
Proof state after:
no goals
Theorem: MellinOfDeltaSpikeAt1_asymp
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
diff : DifferentiableWithinAt ℝ (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1) (Ioi 0) 0
⊢ (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1) =O[𝓝[>] 0] id
Tactic:
have := ofReal_zero ▸ diff.isBigO_sub
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
diff : DifferentiableWithinAt ℝ (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1) (Ioi 0) 0
this : (fun x => 𝓜 (fun x => ↑(Ψ x)) ↑x - 1 - (𝓜 (fun x => ↑(Ψ x)) 0 - 1)) =O[𝓝[>] 0] fun x => x - 0
⊢ (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1) =O[𝓝[>] 0] id
Theorem: MellinOfDeltaSpikeAt1_asymp
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
diff : DifferentiableWithinAt ℝ (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1) (Ioi 0) 0
this : (fun x => 𝓜 (fun x => ↑(Ψ x)) ↑x - 1 - (𝓜 (fun x => ↑(Ψ x)) 0 - 1)) =O[𝓝[>] 0] fun x => x - 0
⊢ (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1) =O[𝓝[>] 0] id
Tactic:
simp only [sub_sub_sub_cancel_right, sub_zero] at this
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
diff : DifferentiableWithinAt ℝ (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1) (Ioi 0) 0
this : (fun x => 𝓜 (fun x => ↑(Ψ x)) ↑x - 𝓜 (fun x => ↑(Ψ x)) 0) =O[𝓝[>] 0] fun x => x
⊢ (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1) =O[𝓝[>] 0] id
Theorem: MellinOfDeltaSpikeAt1_asymp
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
diff : DifferentiableWithinAt ℝ (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1) (Ioi 0) 0
this : (fun x => 𝓜 (fun x => ↑(Ψ x)) ↑x - 𝓜 (fun x => ↑(Ψ x)) 0) =O[𝓝[>] 0] fun x => x
⊢ (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1) =O[𝓝[>] 0] id
Tactic:
convert this
Proof state after:
case h.e'_7.h.h.e'_6
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
diff : DifferentiableWithinAt ℝ (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1) (Ioi 0) 0
this : (fun x => 𝓜 (fun x => ↑(Ψ x)) ↑x - 𝓜 (fun x => ↑(Ψ x)) 0) =O[𝓝[>] 0] fun x => x
x✝ : ℝ
⊢ 1 = 𝓜 (fun x => ↑(Ψ x)) 0
Theorem: MellinOfDeltaSpikeAt1_asymp
Proof state before:
case h.e'_7.h.h.e'_6
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
diff : DifferentiableWithinAt ℝ (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1) (Ioi 0) 0
this : (fun x => 𝓜 (fun x => ↑(Ψ x)) ↑x - 𝓜 (fun x => ↑(Ψ x)) 0) =O[𝓝[>] 0] fun x => x
x✝ : ℝ
⊢ 1 = 𝓜 (fun x => ↑(Ψ x)) 0
Tactic:
simp only [MellinTransform, zero_sub, sub_right_inj, cpow_neg_one, ← div_eq_mul_inv, ← ofReal_div]
Proof state after:
case h.e'_7.h.h.e'_6
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
diff : DifferentiableWithinAt ℝ (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1) (Ioi 0) 0
this : (fun x => 𝓜 (fun x => ↑(Ψ x)) ↑x - 𝓜 (fun x => ↑(Ψ x)) 0) =O[𝓝[>] 0] fun x => x
x✝ : ℝ
⊢ 1 = ∫ (x : ℝ) in Ioi 0, ↑(Ψ x / x)
Theorem: MellinOfDeltaSpikeAt1_asymp
Proof state before:
case h.e'_7.h.h.e'_6
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
diff : DifferentiableWithinAt ℝ (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1) (Ioi 0) 0
this : (fun x => 𝓜 (fun x => ↑(Ψ x)) ↑x - 𝓜 (fun x => ↑(Ψ x)) 0) =O[𝓝[>] 0] fun x => x
x✝ : ℝ
⊢ 1 = ∫ (x : ℝ) in Ioi 0, ↑(Ψ x / x)
Tactic:
rw [← ofReal_one, ← mass_one]
Proof state after:
case h.e'_7.h.h.e'_6
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
diff : DifferentiableWithinAt ℝ (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1) (Ioi 0) 0
this : (fun x => 𝓜 (fun x => ↑(Ψ x)) ↑x - 𝓜 (fun x => ↑(Ψ x)) 0) =O[𝓝[>] 0] fun x => x
x✝ : ℝ
⊢ ↑(∫ (x : ℝ) in Ioi 0, Ψ x / x) = ∫ (x : ℝ) in Ioi 0, ↑(Ψ x / x)
Theorem: MellinOfDeltaSpikeAt1_asymp
Proof state before:
case h.e'_7.h.h.e'_6
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
diff : DifferentiableWithinAt ℝ (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1) (Ioi 0) 0
this : (fun x => 𝓜 (fun x => ↑(Ψ x)) ↑x - 𝓜 (fun x => ↑(Ψ x)) 0) =O[𝓝[>] 0] fun x => x
x✝ : ℝ
⊢ ↑(∫ (x : ℝ) in Ioi 0, Ψ x / x) = ∫ (x : ℝ) in Ioi 0, ↑(Ψ x / x)
Tactic:
convert integral_ofReal.symm
Proof state after:
no goals
Theorem: MellinOfDeltaSpikeAt1_asymp
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ DifferentiableWithinAt ℝ (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1) (Ioi 0) 0
Tactic:
apply DifferentiableAt.differentiableWithinAt
Proof state after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ DifferentiableAt ℝ (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1) 0
Theorem: MellinOfDeltaSpikeAt1_asymp
Proof state before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ DifferentiableAt ℝ (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1) 0
Tactic:
simp only [differentiableAt_sub_const_iff, MellinTransform_eq]
Proof state after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ DifferentiableAt ℝ (fun y => mellin (fun x => ↑(Ψ x)) ↑y) 0
Theorem: MellinOfDeltaSpikeAt1_asymp
Proof state before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ DifferentiableAt ℝ (fun y => mellin (fun x => ↑(Ψ x)) ↑y) 0
Tactic:
refine DifferentiableAt.comp_ofReal ?_
Proof state after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ DifferentiableAt ℂ (mellin fun x => ↑(Ψ x)) ↑0
Theorem: MellinOfDeltaSpikeAt1_asymp
Proof state before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ DifferentiableAt ℂ (mellin fun x => ↑(Ψ x)) ↑0
Tactic:
refine mellin_differentiableAt_of_isBigO_rpow (a := 1) (b := -1) ?_ ?_ (by simp) ?_ (by simp)
Proof state after:
case h.refine_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ LocallyIntegrableOn (fun x => ↑(Ψ x)) (Ioi 0) volume

case h.refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ (fun x => ↑(Ψ x)) =O[atTop] fun x => x ^ (-1)

case h.refine_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ (fun x => ↑(Ψ x)) =O[𝓝[>] 0] fun x => x ^ (- -1)
Theorem: MellinOfDeltaSpikeAt1_asymp
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ (↑0).re < 1
Tactic:
simp
Proof state after:
no goals
Theorem: MellinOfDeltaSpikeAt1_asymp
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ -1 < (↑0).re
Tactic:
simp
Proof state after:
no goals
Theorem: MellinOfDeltaSpikeAt1_asymp
Proof state before:
case h.refine_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ LocallyIntegrableOn (fun x => ↑(Ψ x)) (Ioi 0) volume
Tactic:
apply (Continuous.continuousOn ?_).locallyIntegrableOn (by simp)
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ Continuous fun x => ↑(Ψ x)
Theorem: MellinOfDeltaSpikeAt1_asymp
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ Continuous fun x => ↑(Ψ x)
Tactic:
have := diffΨ.continuous
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
this : Continuous Ψ
⊢ Continuous fun x => ↑(Ψ x)
Theorem: MellinOfDeltaSpikeAt1_asymp
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
this : Continuous Ψ
⊢ Continuous fun x => ↑(Ψ x)
Tactic:
continuity
Proof state after:
no goals
Theorem: MellinOfDeltaSpikeAt1_asymp
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ MeasurableSet (Ioi 0)
Tactic:
simp
Proof state after:
no goals
Theorem: MellinOfDeltaSpikeAt1_asymp
Proof state before:
case h.refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ (fun x => ↑(Ψ x)) =O[atTop] fun x => x ^ (-1)
Tactic:
apply Asymptotics.IsBigO.trans_le (g' := fun _ ↦ (0 : ℝ)) ?_ (by simp)
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ (fun x => ↑(Ψ x)) =O[atTop] fun x => 0
Theorem: MellinOfDeltaSpikeAt1_asymp
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ (fun x => ↑(Ψ x)) =O[atTop] fun x => 0
Tactic:
apply BigO_zero_atTop_of_support_in_Icc (a := 1 / 2) (b := 2)
Proof state after:
case fSupp
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ (Function.support fun x => ↑(Ψ x)) ⊆ Icc (1 / 2) 2
Theorem: MellinOfDeltaSpikeAt1_asymp
Proof state before:
case fSupp
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ (Function.support fun x => ↑(Ψ x)) ⊆ Icc (1 / 2) 2
Tactic:
rwa [Ψ.support_ofReal]
Proof state after:
no goals
Theorem: MellinOfDeltaSpikeAt1_asymp
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ ∀ (x : ℝ), ‖(fun x => 0) x‖ ≤ ‖x ^ (-1)‖
Tactic:
simp
Proof state after:
no goals
Theorem: MellinOfDeltaSpikeAt1_asymp
Proof state before:
case h.refine_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ (fun x => ↑(Ψ x)) =O[𝓝[>] 0] fun x => x ^ (- -1)
Tactic:
apply Asymptotics.IsBigO.trans_le (g' := fun _ ↦ (0 : ℝ)) ?_ (by simp)
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ (fun x => ↑(Ψ x)) =O[𝓝[>] 0] fun x => 0
Theorem: MellinOfDeltaSpikeAt1_asymp
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ (fun x => ↑(Ψ x)) =O[𝓝[>] 0] fun x => 0
Tactic:
apply BigO_zero_atZero_of_support_in_Icc (a := 1 / 2) (b := 2) (ha := (by norm_num))
Proof state after:
case fSupp
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ (Function.support fun x => ↑(Ψ x)) ⊆ Icc (1 / 2) 2
Theorem: MellinOfDeltaSpikeAt1_asymp
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ ∀ (x : ℝ), ‖(fun x => 0) x‖ ≤ ‖x ^ (- -1)‖
Tactic:
simp
Proof state after:
no goals
Theorem: MellinOfDeltaSpikeAt1_asymp
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
f : ℝ → ℂ
⊢ 0 < 1 / 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: MellinOf1
Proof 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
Proof 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
Theorem: MellinOf1
Proof 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
Proof 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