internlm/Lean-Github huggingface dataset:
Theorem: SmoothExistence
Proof state before:
case right.refine_2.refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
this : Ioo (1 / 2) 2 ∩ (Iio 0 ∪ Ioi 0) ∩ Ici 0 = Ioo (1 / 2) 2
⊢ 1 / 2 < 2
Tactic:
linarith
Proof state after:
no goals
Theorem: SmoothExistence
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
⊢ Ioo (1 / 2) 2 ∩ (Iio 0 ∪ Ioi 0) ∩ Ici 0 = Ioo (1 / 2) 2
Tactic:
ext x
Proof state after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
x : ℝ
⊢ x ∈ Ioo (1 / 2) 2 ∩ (Iio 0 ∪ Ioi 0) ∩ Ici 0 ↔ x ∈ Ioo (1 / 2) 2
Theorem: SmoothExistence
Proof state before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
x : ℝ
⊢ x ∈ Ioo (1 / 2) 2 ∩ (Iio 0 ∪ Ioi 0) ∩ Ici 0 ↔ x ∈ Ioo (1 / 2) 2
Tactic:
simp only [mem_inter_iff, mem_Ioo, mem_Ici, mem_Iio, mem_Ioi,
  mem_union, not_lt, and_true, not_le]
Proof state after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
x : ℝ
⊢ ((1 / 2 < x ∧ x < 2) ∧ (x < 0 ∨ 0 < x)) ∧ 0 ≤ x ↔ 1 / 2 < x ∧ x < 2
Theorem: SmoothExistence
Proof state before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
x : ℝ
⊢ ((1 / 2 < x ∧ x < 2) ∧ (x < 0 ∨ 0 < x)) ∧ 0 ≤ x ↔ 1 / 2 < x ∧ x < 2
Tactic:
constructor
Proof state after:
case h.mp
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
x : ℝ
⊢ ((1 / 2 < x ∧ x < 2) ∧ (x < 0 ∨ 0 < x)) ∧ 0 ≤ x → 1 / 2 < x ∧ x < 2

case h.mpr
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
x : ℝ
⊢ 1 / 2 < x ∧ x < 2 → ((1 / 2 < x ∧ x < 2) ∧ (x < 0 ∨ 0 < x)) ∧ 0 ≤ x
Theorem: SmoothExistence
Proof state before:
case h.mp
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
x : ℝ
⊢ ((1 / 2 < x ∧ x < 2) ∧ (x < 0 ∨ 0 < x)) ∧ 0 ≤ x → 1 / 2 < x ∧ x < 2
Tactic:
exact fun h ↦ h.left.left
Proof state after:
no goals
Theorem: SmoothExistence
Proof state before:
case h.mpr
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
x : ℝ
⊢ 1 / 2 < x ∧ x < 2 → ((1 / 2 < x ∧ x < 2) ∧ (x < 0 ∨ 0 < x)) ∧ 0 ≤ x
Tactic:
intro h
Proof state after:
case h.mpr
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
x : ℝ
h : 1 / 2 < x ∧ x < 2
⊢ ((1 / 2 < x ∧ x < 2) ∧ (x < 0 ∨ 0 < x)) ∧ 0 ≤ x
Theorem: SmoothExistence
Proof state before:
case h.mpr
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
x : ℝ
h : 1 / 2 < x ∧ x < 2
⊢ ((1 / 2 < x ∧ x < 2) ∧ (x < 0 ∨ 0 < x)) ∧ 0 ≤ x
Tactic:
simp only [h, and_self, lt_or_lt_iff_ne, ne_eq, true_and]
Proof state after:
case h.mpr
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
x : ℝ
h : 1 / 2 < x ∧ x < 2
⊢ ¬x = 0 ∧ 0 ≤ x
Theorem: SmoothExistence
Proof state before:
case h.mpr
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
x : ℝ
h : 1 / 2 < x ∧ x < 2
⊢ ¬x = 0 ∧ 0 ≤ x
Tactic:
constructor <;> linarith [h.left]
Proof state after:
no goals
Theorem: SmoothExistence
Proof state before:
case right.refine_2.refine_2.hf
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
⊢ 0 ≤ fun x => Ψ x / x
Tactic:
simp_rw [Pi.le_def, Pi.zero_apply]
Proof state after:
case right.refine_2.refine_2.hf
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
⊢ ∀ (i : ℝ), 0 ≤ Ψ i / i
Theorem: SmoothExistence
Proof state before:
case right.refine_2.refine_2.hf
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
⊢ ∀ (i : ℝ), 0 ≤ Ψ i / i
Tactic:
intro y
Proof state after:
case right.refine_2.refine_2.hf
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
y : ℝ
⊢ 0 ≤ Ψ y / y
Theorem: SmoothExistence
Proof state before:
case right.refine_2.refine_2.hf
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
y : ℝ
⊢ 0 ≤ Ψ y / y
Tactic:
by_cases h : y ∈ Function.support Ψ
Proof state after:
case pos
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
y : ℝ
h : y ∈ Function.support Ψ
⊢ 0 ≤ Ψ y / y

case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
y : ℝ
h : y ∉ Function.support Ψ
⊢ 0 ≤ Ψ y / y
Theorem: SmoothExistence
Proof state before:
case pos
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
y : ℝ
h : y ∈ Function.support Ψ
⊢ 0 ≤ Ψ y / y

case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
y : ℝ
h : y ∉ Function.support Ψ
⊢ 0 ≤ Ψ y / y
Tactic:
. apply div_nonneg <| le_trans (by simp [apply_ite]) (hΨ0 y)
  rw [hΨSupport, mem_Ioo] at h; linarith [h.left]
Proof state after:
case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
y : ℝ
h : y ∉ Function.support Ψ
⊢ 0 ≤ Ψ y / y
Theorem: SmoothExistence
Proof state before:
case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
y : ℝ
h : y ∉ Function.support Ψ
⊢ 0 ≤ Ψ y / y
Tactic:
. simp only [Function.mem_support, ne_eq, not_not] at h; simp [h]
Proof state after:
no goals
Theorem: SmoothExistence
Proof state before:
case pos
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
y : ℝ
h : y ∈ Function.support Ψ
⊢ 0 ≤ Ψ y / y
Tactic:
apply div_nonneg <| le_trans (by simp [apply_ite]) (hΨ0 y)
Proof state after:
case pos
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
y : ℝ
h : y ∈ Function.support Ψ
⊢ 0 ≤ y
Theorem: SmoothExistence
Proof state before:
case pos
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
y : ℝ
h : y ∈ Function.support Ψ
⊢ 0 ≤ y
Tactic:
rw [hΨSupport, mem_Ioo] at h
Proof state after:
case pos
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
y : ℝ
h : 1 / 2 < y ∧ y < 2
⊢ 0 ≤ y
Theorem: SmoothExistence
Proof state before:
case pos
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
y : ℝ
h : 1 / 2 < y ∧ y < 2
⊢ 0 ≤ y
Tactic:
linarith [h.left]
Proof state after:
no goals
Theorem: SmoothExistence
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
y : ℝ
h : y ∈ Function.support Ψ
⊢ 0 ≤ if 1 ≤ y ∧ y ≤ 3 / 2 then 1 else 0
Tactic:
simp [apply_ite]
Proof state after:
no goals
Theorem: SmoothExistence
Proof state before:
case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
y : ℝ
h : y ∉ Function.support Ψ
⊢ 0 ≤ Ψ y / y
Tactic:
simp only [Function.mem_support, ne_eq, not_not] at h
Proof state after:
case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
y : ℝ
h : Ψ y = 0
⊢ 0 ≤ Ψ y / y
Theorem: SmoothExistence
Proof state before:
case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
y : ℝ
h : Ψ y = 0
⊢ 0 ≤ Ψ y / y
Tactic:
simp [h]
Proof state after:
no goals
Theorem: SmoothExistence
Proof state before:
case right.refine_2.refine_2.hfi
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
⊢ Integrable (fun x => Ψ x / x) (volume.restrict (Ici 0))
Tactic:
have : (fun x ↦ Ψ x / x).support ⊆ Icc (1 / 2) 2 := by
  rw [Function.support_div, hΨSupport]
  apply subset_trans (by apply inter_subset_left) Ioo_subset_Icc_self
Proof state after:
case right.refine_2.refine_2.hfi
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
this : (Function.support fun x => Ψ x / x) ⊆ Icc (1 / 2) 2
⊢ Integrable (fun x => Ψ x / x) (volume.restrict (Ici 0))
Theorem: SmoothExistence
Proof state before:
case right.refine_2.refine_2.hfi
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
this : (Function.support fun x => Ψ x / x) ⊆ Icc (1 / 2) 2
⊢ Integrable (fun x => Ψ x / x) (volume.restrict (Ici 0))
Tactic:
apply (integrableOn_iff_integrable_of_support_subset this).mp
Proof state after:
case right.refine_2.refine_2.hfi
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
this : (Function.support fun x => Ψ x / x) ⊆ Icc (1 / 2) 2
⊢ IntegrableOn (fun x => Ψ x / x) (Icc (1 / 2) 2) (volume.restrict (Ici 0))
Theorem: SmoothExistence
Proof state before:
case right.refine_2.refine_2.hfi
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
this : (Function.support fun x => Ψ x / x) ⊆ Icc (1 / 2) 2
⊢ IntegrableOn (fun x => Ψ x / x) (Icc (1 / 2) 2) (volume.restrict (Ici 0))
Tactic:
apply ContinuousOn.integrableOn_compact isCompact_Icc
Proof state after:
case right.refine_2.refine_2.hfi
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
this : (Function.support fun x => Ψ x / x) ⊆ Icc (1 / 2) 2
⊢ ContinuousOn (fun x => Ψ x / x) (Icc (1 / 2) 2)
Theorem: SmoothExistence
Proof state before:
case right.refine_2.refine_2.hfi
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
this : (Function.support fun x => Ψ x / x) ⊆ Icc (1 / 2) 2
⊢ ContinuousOn (fun x => Ψ x / x) (Icc (1 / 2) 2)
Tactic:
apply hΨContDiff.continuous.continuousOn.div continuousOn_id ?_
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
this : (Function.support fun x => Ψ x / x) ⊆ Icc (1 / 2) 2
⊢ ∀ x ∈ Icc (1 / 2) 2, id x ≠ 0
Theorem: SmoothExistence
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
this : (Function.support fun x => Ψ x / x) ⊆ Icc (1 / 2) 2
⊢ ∀ x ∈ Icc (1 / 2) 2, id x ≠ 0
Tactic:
simp only [mem_Icc, ne_eq, and_imp, id_eq]
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
this : (Function.support fun x => Ψ x / x) ⊆ Icc (1 / 2) 2
⊢ ∀ (x : ℝ), 1 / 2 ≤ x → x ≤ 2 → ¬x = 0
Theorem: SmoothExistence
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
this : (Function.support fun x => Ψ x / x) ⊆ Icc (1 / 2) 2
⊢ ∀ (x : ℝ), 1 / 2 ≤ x → x ≤ 2 → ¬x = 0
Tactic:
intros
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
this : (Function.support fun x => Ψ x / x) ⊆ Icc (1 / 2) 2
x✝ : ℝ
a✝¹ : 1 / 2 ≤ x✝
a✝ : x✝ ≤ 2
⊢ ¬x✝ = 0
Theorem: SmoothExistence
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
this : (Function.support fun x => Ψ x / x) ⊆ Icc (1 / 2) 2
x✝ : ℝ
a✝¹ : 1 / 2 ≤ x✝
a✝ : x✝ ≤ 2
⊢ ¬x✝ = 0
Tactic:
linarith
Proof state after:
no goals
Theorem: SmoothExistence
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
⊢ (Function.support fun x => Ψ x / x) ⊆ Icc (1 / 2) 2
Tactic:
rw [Function.support_div, hΨSupport]
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
⊢ (Ioo (1 / 2) 2 ∩ Function.support fun x => x) ⊆ Icc (1 / 2) 2
Theorem: SmoothExistence
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
⊢ (Ioo (1 / 2) 2 ∩ Function.support fun x => x) ⊆ Icc (1 / 2) 2
Tactic:
apply subset_trans (by apply inter_subset_left) Ioo_subset_Icc_self
Proof state after:
no goals
Theorem: SmoothExistence
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
⊢ (Ioo (1 / 2) 2 ∩ Function.support fun x => x) ⊆ Ioo (1 / 2) 2
Tactic:
apply inter_subset_left
Proof state after:
no goals
Theorem: mem_within_strip
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
σ₁ σ₂ : ℝ
⊢ {s | σ₁ ≤ s.re ∧ s.re ≤ σ₂} ∈ 𝓟 {s | σ₁ ≤ s.re ∧ s.re ≤ σ₂}
Tactic:
simp
Proof state after:
no goals
Theorem: MellinOfPsi_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
⊢ ∫ (x : ℝ) in Ioi 0, ↑(Ψ x) * ↑x ^ (s - 1) = -(1 / s) * ∫ (x : ℝ) in Ioi 0, ↑(deriv Ψ x) * ↑x ^ s
Tactic:
let g {s : ℂ} := fun (x : ℝ)  ↦ x ^ s / s
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
⊢ ∫ (x : ℝ) in Ioi 0, ↑(Ψ x) * ↑x ^ (s - 1) = -(1 / s) * ∫ (x : ℝ) in Ioi 0, ↑(deriv Ψ x) * ↑x ^ s
Theorem: MellinOfPsi_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
⊢ ∫ (x : ℝ) in Ioi 0, ↑(Ψ x) * ↑x ^ (s - 1) = -(1 / s) * ∫ (x : ℝ) in Ioi 0, ↑(deriv Ψ x) * ↑x ^ s
Tactic:
calc
  _ =  ∫ (x : ℝ) in Ioi 0, ↑(Ψ x) * deriv (@g s) x := ?_
  _ = -∫ (x : ℝ) in Ioi 0, deriv (fun x ↦ ↑(Ψ x)) x * @g s x := ?_
  _ = -∫ (x : ℝ) in Ioi 0, deriv Ψ x * @g s x := ?_
  _ = -∫ (x : ℝ) in Ioi 0, deriv Ψ x * x ^ s / s := by simp only [mul_div, g]
  _ = _ := ?_
Proof state after:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
⊢ ∫ (x : ℝ) in Ioi 0, ↑(Ψ x) * ↑x ^ (s - 1) = ∫ (x : ℝ) in Ioi 0, ↑(Ψ x) * deriv g x

case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
⊢ ∫ (x : ℝ) in Ioi 0, ↑(Ψ x) * deriv g x = -∫ (x : ℝ) in Ioi 0, deriv (fun x => ↑(Ψ x)) x * g x

case calc_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
⊢ -∫ (x : ℝ) in Ioi 0, deriv (fun x => ↑(Ψ x)) x * g x = -∫ (x : ℝ) in Ioi 0, ↑(deriv Ψ x) * g x

case calc_4
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
⊢ -∫ (x : ℝ) in Ioi 0, ↑(deriv Ψ x) * ↑x ^ s / s = -(1 / s) * ∫ (x : ℝ) in Ioi 0, ↑(deriv Ψ x) * ↑x ^ s