internlm/Lean-Github huggingface dataset:
Theorem: MellinConvolutionTransform
Proof state before:
case calc_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
⊢ ∫ (x : ℝ) in Ioi 0, f y * g (x * y / y) / ↑y * (↑x * ↑y) ^ (s - 1) * ↑y =
    ∫ (x : ℝ) in Ioi 0, f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1))
Tactic:
rw [setIntegral_congr (by simp)]
Proof state after:
case calc_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
⊢ EqOn (fun x => f y * g (x * y / y) / ↑y * (↑x * ↑y) ^ (s - 1) * ↑y)
    (fun x => f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1))) (Ioi 0)
Theorem: MellinConvolutionTransform
Proof state before:
case calc_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
⊢ EqOn (fun x => f y * g (x * y / y) / ↑y * (↑x * ↑y) ^ (s - 1) * ↑y)
    (fun x => f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1))) (Ioi 0)
Tactic:
intro x hx
Proof state after:
case calc_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
x : ℝ
hx : x ∈ Ioi 0
⊢ (fun x => f y * g (x * y / y) / ↑y * (↑x * ↑y) ^ (s - 1) * ↑y) x =
    (fun x => f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1))) x
Theorem: MellinConvolutionTransform
Proof state before:
case calc_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
x : ℝ
hx : x ∈ Ioi 0
⊢ (fun x => f y * g (x * y / y) / ↑y * (↑x * ↑y) ^ (s - 1) * ↑y) x =
    (fun x => f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1))) x
Tactic:
have y_ne_zeroℝ : y ≠ 0 := ne_of_gt (mem_Ioi.mp hy)
Proof state after:
case calc_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
x : ℝ
hx : x ∈ Ioi 0
y_ne_zeroℝ : y ≠ 0
⊢ (fun x => f y * g (x * y / y) / ↑y * (↑x * ↑y) ^ (s - 1) * ↑y) x =
    (fun x => f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1))) x
Theorem: MellinConvolutionTransform
Proof state before:
case calc_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
x : ℝ
hx : x ∈ Ioi 0
y_ne_zeroℝ : y ≠ 0
⊢ (fun x => f y * g (x * y / y) / ↑y * (↑x * ↑y) ^ (s - 1) * ↑y) x =
    (fun x => f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1))) x
Tactic:
have y_ne_zeroℂ : (y : ℂ) ≠ 0 := by exact_mod_cast y_ne_zeroℝ
Proof state after:
case calc_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
x : ℝ
hx : x ∈ Ioi 0
y_ne_zeroℝ : y ≠ 0
y_ne_zeroℂ : ↑y ≠ 0
⊢ (fun x => f y * g (x * y / y) / ↑y * (↑x * ↑y) ^ (s - 1) * ↑y) x =
    (fun x => f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1))) x
Theorem: MellinConvolutionTransform
Proof state before:
case calc_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
x : ℝ
hx : x ∈ Ioi 0
y_ne_zeroℝ : y ≠ 0
y_ne_zeroℂ : ↑y ≠ 0
⊢ (fun x => f y * g (x * y / y) / ↑y * (↑x * ↑y) ^ (s - 1) * ↑y) x =
    (fun x => f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1))) x
Tactic:
field_simp [mul_cpow_ofReal_nonneg (LT.lt.le hx) (LT.lt.le hy)]
Proof state after:
case calc_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
x : ℝ
hx : x ∈ Ioi 0
y_ne_zeroℝ : y ≠ 0
y_ne_zeroℂ : ↑y ≠ 0
⊢ f y * g x * (↑x ^ (s - 1) * ↑y ^ (s - 1)) = f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1))
Theorem: MellinConvolutionTransform
Proof state before:
case calc_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
x : ℝ
hx : x ∈ Ioi 0
y_ne_zeroℝ : y ≠ 0
y_ne_zeroℂ : ↑y ≠ 0
⊢ f y * g x * (↑x ^ (s - 1) * ↑y ^ (s - 1)) = f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1))
Tactic:
ring
Proof state after:
no goals
Theorem: MellinConvolutionTransform
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
⊢ MeasurableSet (Ioi 0)
Tactic:
simp
Proof state after:
no goals
Theorem: MellinConvolutionTransform
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
x : ℝ
hx : x ∈ Ioi 0
y_ne_zeroℝ : y ≠ 0
⊢ ↑y ≠ 0
Tactic:
exact_mod_cast y_ne_zeroℝ
Proof state after:
no goals
Theorem: MellinConvolutionTransform
Proof state before:
case calc_4
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
⊢ ∫ (x : ℝ) in Ioi 0, f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1)) =
    f y * ↑y ^ (s - 1) * ∫ (x : ℝ) in Ioi 0, g x * ↑x ^ (s - 1)
Tactic:
apply integral_mul_left
Proof state after:
no goals
Theorem: SmoothExistence
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
⊢ ∃ Ψ, ContDiff ℝ ⊤ Ψ ∧ (∀ (x : ℝ), 0 ≤ Ψ x) ∧ Function.support Ψ ⊆ Icc (1 / 2) 2 ∧ 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
Tactic:
have := smooth_urysohn_support_Ioo (a := 1 / 2) (b := 1) (c := 3/2) (d := 2) (by linarith)
  (by linarith)
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
this :
  ∃ Ψ,
    ContDiff ℝ ⊤ Ψ ∧
      HasCompactSupport Ψ ∧
        (Icc 1 (3 / 2)).indicator 1 ≤ Ψ ∧ Ψ ≤ (Ioo (1 / 2) 2).indicator 1 ∧ Function.support Ψ = Ioo (1 / 2) 2
⊢ ∃ Ψ, ContDiff ℝ ⊤ Ψ ∧ (∀ (x : ℝ), 0 ≤ Ψ x) ∧ Function.support Ψ ⊆ Icc (1 / 2) 2 ∧ 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
Theorem: SmoothExistence
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
this :
  ∃ Ψ,
    ContDiff ℝ ⊤ Ψ ∧
      HasCompactSupport Ψ ∧
        (Icc 1 (3 / 2)).indicator 1 ≤ Ψ ∧ Ψ ≤ (Ioo (1 / 2) 2).indicator 1 ∧ Function.support Ψ = Ioo (1 / 2) 2
⊢ ∃ Ψ, ContDiff ℝ ⊤ Ψ ∧ (∀ (x : ℝ), 0 ≤ Ψ x) ∧ Function.support Ψ ⊆ Icc (1 / 2) 2 ∧ 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
Tactic:
rcases this with ⟨Ψ, hΨContDiff, _, hΨ0, hΨ1, hΨSupport⟩
Proof state after:
case intro.intro.intro.intro.intro
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨ0 : (Icc 1 (3 / 2)).indicator 1 ≤ Ψ
hΨ1 : Ψ ≤ (Ioo (1 / 2) 2).indicator 1
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
⊢ ∃ Ψ, ContDiff ℝ ⊤ Ψ ∧ (∀ (x : ℝ), 0 ≤ Ψ x) ∧ Function.support Ψ ⊆ Icc (1 / 2) 2 ∧ 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
Theorem: SmoothExistence
Proof state before:
case intro.intro.intro.intro.intro
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨ0 : (Icc 1 (3 / 2)).indicator 1 ≤ Ψ
hΨ1 : Ψ ≤ (Ioo (1 / 2) 2).indicator 1
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
⊢ ∃ Ψ, ContDiff ℝ ⊤ Ψ ∧ (∀ (x : ℝ), 0 ≤ Ψ x) ∧ Function.support Ψ ⊆ Icc (1 / 2) 2 ∧ 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
Tactic:
use Ψ, hΨContDiff
Proof state after:
case right
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨ0 : (Icc 1 (3 / 2)).indicator 1 ≤ Ψ
hΨ1 : Ψ ≤ (Ioo (1 / 2) 2).indicator 1
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
⊢ (∀ (x : ℝ), 0 ≤ Ψ x) ∧ Function.support Ψ ⊆ Icc (1 / 2) 2 ∧ 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
Theorem: SmoothExistence
Proof state before:
case right
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨ0 : (Icc 1 (3 / 2)).indicator 1 ≤ Ψ
hΨ1 : Ψ ≤ (Ioo (1 / 2) 2).indicator 1
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
⊢ (∀ (x : ℝ), 0 ≤ Ψ x) ∧ Function.support Ψ ⊆ Icc (1 / 2) 2 ∧ 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
Tactic:
unfold indicator at hΨ0 hΨ1
Proof state after:
case right
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨ0 : (fun x => if x ∈ Icc 1 (3 / 2) then 1 x else 0) ≤ Ψ
hΨ1 : Ψ ≤ fun x => if x ∈ Ioo (1 / 2) 2 then 1 x else 0
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
⊢ (∀ (x : ℝ), 0 ≤ Ψ x) ∧ Function.support Ψ ⊆ Icc (1 / 2) 2 ∧ 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
Theorem: SmoothExistence
Proof state before:
case right
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨ0 : (fun x => if x ∈ Icc 1 (3 / 2) then 1 x else 0) ≤ Ψ
hΨ1 : Ψ ≤ fun x => if x ∈ Ioo (1 / 2) 2 then 1 x else 0
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
⊢ (∀ (x : ℝ), 0 ≤ Ψ x) ∧ Function.support Ψ ⊆ Icc (1 / 2) 2 ∧ 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
Tactic:
simp only [mem_Icc, Pi.one_apply, Pi.le_def, mem_Ioo] at hΨ0 hΨ1
Proof state after:
case right
𝕂 : 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 : ℝ), 0 ≤ Ψ x) ∧ Function.support Ψ ⊆ Icc (1 / 2) 2 ∧ 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
Theorem: SmoothExistence
Proof state before:
case right
𝕂 : 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 : ℝ), 0 ≤ Ψ x) ∧ Function.support Ψ ⊆ Icc (1 / 2) 2 ∧ 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
Tactic:
simp only [hΨSupport, subset_def, mem_Ioo, mem_Icc, and_imp]
Proof state after:
case right
𝕂 : 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 : ℝ), 0 ≤ Ψ x) ∧ (∀ (x : ℝ), 1 / 2 < x → x < 2 → 1 / 2 ≤ x ∧ x ≤ 2) ∧ 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
Theorem: SmoothExistence
Proof state before:
case right
𝕂 : 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 : ℝ), 0 ≤ Ψ x) ∧ (∀ (x : ℝ), 1 / 2 < x → x < 2 → 1 / 2 ≤ x ∧ x ≤ 2) ∧ 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
Tactic:
split_ands
Proof state after:
case right.refine_1
𝕂 : 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 : ℝ), 0 ≤ Ψ x

case right.refine_2.refine_1
𝕂 : 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

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
⊢ 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
Theorem: SmoothExistence
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
h : ∃ Ψ, ContDiff ℝ ⊤ Ψ ∧ (∀ (x : ℝ), 0 ≤ Ψ x) ∧ Function.support Ψ ⊆ Icc (1 / 2) 2 ∧ 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
⊢ ∃ Ψ, ContDiff ℝ ⊤ Ψ ∧ (∀ (x : ℝ), 0 ≤ Ψ x) ∧ Function.support Ψ ⊆ Icc (1 / 2) 2 ∧ ∫ (x : ℝ) in Ici 0, Ψ x / x = 1
Tactic:
rcases h with ⟨Ψ, hΨ, hΨnonneg, hΨsupp, hΨpos⟩
Proof state after:
case intro.intro.intro.intro
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨ : ContDiff ℝ ⊤ Ψ
hΨnonneg : ∀ (x : ℝ), 0 ≤ Ψ x
hΨsupp : Function.support Ψ ⊆ Icc (1 / 2) 2
hΨpos : 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
⊢ ∃ Ψ, ContDiff ℝ ⊤ Ψ ∧ (∀ (x : ℝ), 0 ≤ Ψ x) ∧ Function.support Ψ ⊆ Icc (1 / 2) 2 ∧ ∫ (x : ℝ) in Ici 0, Ψ x / x = 1
Theorem: SmoothExistence
Proof state before:
case intro.intro.intro.intro
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨ : ContDiff ℝ ⊤ Ψ
hΨnonneg : ∀ (x : ℝ), 0 ≤ Ψ x
hΨsupp : Function.support Ψ ⊆ Icc (1 / 2) 2
hΨpos : 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
⊢ ∃ Ψ, ContDiff ℝ ⊤ Ψ ∧ (∀ (x : ℝ), 0 ≤ Ψ x) ∧ Function.support Ψ ⊆ Icc (1 / 2) 2 ∧ ∫ (x : ℝ) in Ici 0, Ψ x / x = 1
Tactic:
let c := (∫ x in Ici 0, Ψ x / x)
Proof state after:
case intro.intro.intro.intro
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨ : ContDiff ℝ ⊤ Ψ
hΨnonneg : ∀ (x : ℝ), 0 ≤ Ψ x
hΨsupp : Function.support Ψ ⊆ Icc (1 / 2) 2
hΨpos : 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
c : ℝ := ∫ (x : ℝ) in Ici 0, Ψ x / x
⊢ ∃ Ψ, ContDiff ℝ ⊤ Ψ ∧ (∀ (x : ℝ), 0 ≤ Ψ x) ∧ Function.support Ψ ⊆ Icc (1 / 2) 2 ∧ ∫ (x : ℝ) in Ici 0, Ψ x / x = 1
Theorem: SmoothExistence
Proof state before:
case intro.intro.intro.intro
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨ : ContDiff ℝ ⊤ Ψ
hΨnonneg : ∀ (x : ℝ), 0 ≤ Ψ x
hΨsupp : Function.support Ψ ⊆ Icc (1 / 2) 2
hΨpos : 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
c : ℝ := ∫ (x : ℝ) in Ici 0, Ψ x / x
⊢ ∃ Ψ, ContDiff ℝ ⊤ Ψ ∧ (∀ (x : ℝ), 0 ≤ Ψ x) ∧ Function.support Ψ ⊆ Icc (1 / 2) 2 ∧ ∫ (x : ℝ) in Ici 0, Ψ x / x = 1
Tactic:
use fun y ↦ Ψ y / c
Proof state after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨ : ContDiff ℝ ⊤ Ψ
hΨnonneg : ∀ (x : ℝ), 0 ≤ Ψ x
hΨsupp : Function.support Ψ ⊆ Icc (1 / 2) 2
hΨpos : 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
c : ℝ := ∫ (x : ℝ) in Ici 0, Ψ x / x
⊢ (ContDiff ℝ ⊤ fun y => Ψ y / c) ∧
    (∀ (x : ℝ), 0 ≤ Ψ x / c) ∧ (Function.support fun y => Ψ y / c) ⊆ Icc (1 / 2) 2 ∧ ∫ (x : ℝ) in Ici 0, Ψ x / c / x = 1
Theorem: SmoothExistence
Proof state before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨ : ContDiff ℝ ⊤ Ψ
hΨnonneg : ∀ (x : ℝ), 0 ≤ Ψ x
hΨsupp : Function.support Ψ ⊆ Icc (1 / 2) 2
hΨpos : 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
c : ℝ := ∫ (x : ℝ) in Ici 0, Ψ x / x
⊢ (ContDiff ℝ ⊤ fun y => Ψ y / c) ∧
    (∀ (x : ℝ), 0 ≤ Ψ x / c) ∧ (Function.support fun y => Ψ y / c) ⊆ Icc (1 / 2) 2 ∧ ∫ (x : ℝ) in Ici 0, Ψ x / c / x = 1
Tactic:
refine ⟨hΨ.div_const c, fun y ↦ div_nonneg (hΨnonneg y) (le_of_lt hΨpos), ?_, ?_⟩
Proof state after:
case h.refine_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨ : ContDiff ℝ ⊤ Ψ
hΨnonneg : ∀ (x : ℝ), 0 ≤ Ψ x
hΨsupp : Function.support Ψ ⊆ Icc (1 / 2) 2
hΨpos : 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
c : ℝ := ∫ (x : ℝ) in Ici 0, Ψ x / x
⊢ (Function.support fun y => Ψ y / c) ⊆ Icc (1 / 2) 2

case h.refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨ : ContDiff ℝ ⊤ Ψ
hΨnonneg : ∀ (x : ℝ), 0 ≤ Ψ x
hΨsupp : Function.support Ψ ⊆ Icc (1 / 2) 2
hΨpos : 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
c : ℝ := ∫ (x : ℝ) in Ici 0, Ψ x / x
⊢ ∫ (x : ℝ) in Ici 0, Ψ x / c / x = 1
Theorem: SmoothExistence
Proof state before:
case h.refine_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨ : ContDiff ℝ ⊤ Ψ
hΨnonneg : ∀ (x : ℝ), 0 ≤ Ψ x
hΨsupp : Function.support Ψ ⊆ Icc (1 / 2) 2
hΨpos : 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
c : ℝ := ∫ (x : ℝ) in Ici 0, Ψ x / x
⊢ (Function.support fun y => Ψ y / c) ⊆ Icc (1 / 2) 2
Tactic:
rw [Function.support_div, Function.support_const (ne_of_lt hΨpos).symm, inter_univ]
Proof state after:
case h.refine_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨ : ContDiff ℝ ⊤ Ψ
hΨnonneg : ∀ (x : ℝ), 0 ≤ Ψ x
hΨsupp : Function.support Ψ ⊆ Icc (1 / 2) 2
hΨpos : 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
c : ℝ := ∫ (x : ℝ) in Ici 0, Ψ x / x
⊢ (Function.support fun y => Ψ y) ⊆ Icc (1 / 2) 2
Theorem: SmoothExistence
Proof state before:
case h.refine_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨ : ContDiff ℝ ⊤ Ψ
hΨnonneg : ∀ (x : ℝ), 0 ≤ Ψ x
hΨsupp : Function.support Ψ ⊆ Icc (1 / 2) 2
hΨpos : 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
c : ℝ := ∫ (x : ℝ) in Ici 0, Ψ x / x
⊢ (Function.support fun y => Ψ y) ⊆ Icc (1 / 2) 2
Tactic:
convert hΨsupp
Proof state after:
no goals
Theorem: SmoothExistence
Proof state before:
case h.refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨ : ContDiff ℝ ⊤ Ψ
hΨnonneg : ∀ (x : ℝ), 0 ≤ Ψ x
hΨsupp : Function.support Ψ ⊆ Icc (1 / 2) 2
hΨpos : 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
c : ℝ := ∫ (x : ℝ) in Ici 0, Ψ x / x
⊢ ∫ (x : ℝ) in Ici 0, Ψ x / c / x = 1
Tactic:
simp only [div_right_comm _ c _, integral_div c, div_self <| ne_of_gt hΨpos]
Proof state after:
no goals
Theorem: SmoothExistence
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
⊢ 1 / 2 < 1
Tactic:
linarith
Proof state after:
no goals
Theorem: SmoothExistence
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
⊢ 3 / 2 < 2
Tactic:
linarith
Proof state after:
no goals
Theorem: SmoothExistence
Proof state before:
case right.refine_1
𝕂 : 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 : ℝ), 0 ≤ Ψ x
Tactic:
exact fun x ↦ le_trans (by simp [apply_ite]) (hΨ0 x)
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
x : ℝ
⊢ 0 ≤ if 1 ≤ x ∧ x ≤ 3 / 2 then 1 else 0
Tactic:
simp [apply_ite]
Proof state after:
no goals
Theorem: SmoothExistence
Proof state before:
case right.refine_2.refine_1
𝕂 : 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
Tactic:
exact fun y hy hy' ↦ ⟨by linarith, by 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
y : ℝ
hy : 1 / 2 < y
hy' : y < 2
⊢ 1 / 2 ≤ y
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
y : ℝ
hy : 1 / 2 < y
hy' : y < 2
⊢ y ≤ 2
Tactic:
linarith
Proof state after:
no goals
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
⊢ 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
Tactic:
rw [integral_pos_iff_support_of_nonneg]
Proof state after:
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
⊢ 0 < (volume.restrict (Ici 0)) (Function.support fun x => Ψ x / x)

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

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))
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
⊢ 0 < (volume.restrict (Ici 0)) (Function.support fun x => Ψ x / x)
Tactic:
simp only [Function.support_div, measurableSet_Ici, Measure.restrict_apply', hΨSupport, Function.support_id]
Proof state after:
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
⊢ 0 < volume (Ioo (1 / 2) 2 ∩ (Iio 0 ∪ Ioi 0) ∩ Ici 0)
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
⊢ 0 < volume (Ioo (1 / 2) 2 ∩ (Iio 0 ∪ Ioi 0) ∩ Ici 0)
Tactic:
simp only [this, volume_Ioo, ENNReal.ofReal_pos, sub_pos, gt_iff_lt]
Proof state after:
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