internlm/Lean-Github huggingface dataset:
Theorem: Smooth1Properties_below
Proof state before:
case h.right
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
⊢ Smooth1 Ψ ε x = 1
Tactic:
rewrite [← DeltaSpikeMass mass_one εpos]
Proof state after:
case h.right
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
⊢ Smooth1 Ψ ε x = ∫ (x : ℝ) in Ioi 0, DeltaSpike (fun x => Ψ x) ε x / x
Theorem: Smooth1Properties_below
Proof state before:
case h.right
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
⊢ Smooth1 Ψ ε x = ∫ (x : ℝ) in Ioi 0, DeltaSpike (fun x => Ψ x) ε x / x
Tactic:
unfold Smooth1 MellinConvolution
Proof state after:
case h.right
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
⊢ ∫ (y : ℝ) in Ioi 0, (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) y * DeltaSpike Ψ ε (x / y) / ↑y =
    ∫ (x : ℝ) in Ioi 0, DeltaSpike (fun x => Ψ x) ε x / x
Theorem: Smooth1Properties_below
Proof state before:
case h.right
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
⊢ ∫ (y : ℝ) in Ioi 0, (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) y * DeltaSpike Ψ ε (x / y) / ↑y =
    ∫ (x : ℝ) in Ioi 0, DeltaSpike (fun x => Ψ x) ε x / x
Tactic:
calc
  _ = ∫ (y : ℝ) in Ioi 0, indicator (Ioc 0 1) (fun y ↦ DeltaSpike Ψ ε (x / y) / ↑y) y := ?_
  _ = ∫ (y : ℝ) in Ioi 0, DeltaSpike Ψ ε (x / y) / y := ?_
  _ = _ := integral_comp_div_I0i_haar (fun y ↦ DeltaSpike Ψ ε y) xpos
Proof state after:
case h.right.calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
⊢ ∫ (y : ℝ) in Ioi 0, (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) y * DeltaSpike Ψ ε (x / y) / ↑y =
    ∫ (y : ℝ) in Ioi 0, (Ioc 0 1).indicator (fun y => DeltaSpike Ψ ε (x / y) / y) y

case h.right.calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
⊢ ∫ (y : ℝ) in Ioi 0, (Ioc 0 1).indicator (fun y => DeltaSpike Ψ ε (x / y) / y) y =
    ∫ (y : ℝ) in Ioi 0, DeltaSpike Ψ ε (x / y) / y
Theorem: Smooth1Properties_below
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
⊢ 1 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: Smooth1Properties_below
Proof state before:
case h.right.calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
⊢ ∫ (y : ℝ) in Ioi 0, (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) y * DeltaSpike Ψ ε (x / y) / ↑y =
    ∫ (y : ℝ) in Ioi 0, (Ioc 0 1).indicator (fun y => DeltaSpike Ψ ε (x / y) / y) y
Tactic:
rw [setIntegral_congr (by simp)]
Proof state after:
case h.right.calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
⊢ EqOn (fun y => (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) y * DeltaSpike Ψ ε (x / y) / ↑y)
    (fun x_1 => (Ioc 0 1).indicator (fun y => DeltaSpike Ψ ε (x / y) / y) x_1) (Ioi 0)
Theorem: Smooth1Properties_below
Proof state before:
case h.right.calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
⊢ EqOn (fun y => (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) y * DeltaSpike Ψ ε (x / y) / ↑y)
    (fun x_1 => (Ioc 0 1).indicator (fun y => DeltaSpike Ψ ε (x / y) / y) x_1) (Ioi 0)
Tactic:
intro y hy
Proof state after:
case h.right.calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
⊢ (fun y => (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) y * DeltaSpike Ψ ε (x / y) / ↑y) y =
    (fun x_1 => (Ioc 0 1).indicator (fun y => DeltaSpike Ψ ε (x / y) / y) x_1) y
Theorem: Smooth1Properties_below
Proof state before:
case h.right.calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
⊢ (fun y => (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) y * DeltaSpike Ψ ε (x / y) / ↑y) y =
    (fun x_1 => (Ioc 0 1).indicator (fun y => DeltaSpike Ψ ε (x / y) / y) x_1) y
Tactic:
by_cases h : y ≤ 1 <;> simp [indicator, mem_Ioi.mp hy, h]
Proof state after:
no goals
Theorem: Smooth1Properties_below
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
⊢ MeasurableSet (Ioi 0)
Tactic:
simp
Proof state after:
no goals
Theorem: Smooth1Properties_below
Proof state before:
case h.right.calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
⊢ ∫ (y : ℝ) in Ioi 0, (Ioc 0 1).indicator (fun y => DeltaSpike Ψ ε (x / y) / y) y =
    ∫ (y : ℝ) in Ioi 0, DeltaSpike Ψ ε (x / y) / y
Tactic:
rw [setIntegral_congr (by simp)]
Proof state after:
case h.right.calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
⊢ EqOn (fun y => (Ioc 0 1).indicator (fun y => DeltaSpike Ψ ε (x / y) / y) y)
    (fun x_1 => DeltaSpike Ψ ε (x / x_1) / x_1) (Ioi 0)
Theorem: Smooth1Properties_below
Proof state before:
case h.right.calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
⊢ EqOn (fun y => (Ioc 0 1).indicator (fun y => DeltaSpike Ψ ε (x / y) / y) y)
    (fun x_1 => DeltaSpike Ψ ε (x / x_1) / x_1) (Ioi 0)
Tactic:
intro y hy
Proof state after:
case h.right.calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
⊢ (fun y => (Ioc 0 1).indicator (fun y => DeltaSpike Ψ ε (x / y) / y) y) y =
    (fun x_1 => DeltaSpike Ψ ε (x / x_1) / x_1) y
Theorem: Smooth1Properties_below
Proof state before:
case h.right.calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
⊢ (fun y => (Ioc 0 1).indicator (fun y => DeltaSpike Ψ ε (x / y) / y) y) y =
    (fun x_1 => DeltaSpike Ψ ε (x / x_1) / x_1) y
Tactic:
simp only [indicator_apply_eq_self, mem_Ioc, not_and, not_le, div_eq_zero_iff]
Proof state after:
case h.right.calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
⊢ (0 < y → 1 < y) → DeltaSpike Ψ ε (x / y) = 0 ∨ y = 0
Theorem: Smooth1Properties_below
Proof state before:
case h.right.calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
⊢ (0 < y → 1 < y) → DeltaSpike Ψ ε (x / y) = 0 ∨ y = 0
Tactic:
intro hy2
Proof state after:
case h.right.calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 0 < y → 1 < y
⊢ DeltaSpike Ψ ε (x / y) = 0 ∨ y = 0
Theorem: Smooth1Properties_below
Proof state before:
case h.right.calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 0 < y → 1 < y
⊢ DeltaSpike Ψ ε (x / y) = 0 ∨ y = 0
Tactic:
replace hy2 := hy2 <| mem_Ioi.mp hy
Proof state after:
case h.right.calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
⊢ DeltaSpike Ψ ε (x / y) = 0 ∨ y = 0
Theorem: Smooth1Properties_below
Proof state before:
case h.right.calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
⊢ DeltaSpike Ψ ε (x / y) = 0 ∨ y = 0
Tactic:
by_cases h : y = 0
Proof state after:
case pos
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : y = 0
⊢ DeltaSpike Ψ ε (x / y) = 0 ∨ y = 0

case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
⊢ DeltaSpike Ψ ε (x / y) = 0 ∨ y = 0
Theorem: Smooth1Properties_below
Proof state before:
case pos
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : y = 0
⊢ DeltaSpike Ψ ε (x / y) = 0 ∨ y = 0

case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
⊢ DeltaSpike Ψ ε (x / y) = 0 ∨ y = 0
Tactic:
right
Proof state after:
case pos.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : y = 0
⊢ y = 0

case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
⊢ DeltaSpike Ψ ε (x / y) = 0 ∨ y = 0
Theorem: Smooth1Properties_below
Proof state before:
case pos.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : y = 0
⊢ y = 0

case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
⊢ DeltaSpike Ψ ε (x / y) = 0 ∨ y = 0
Tactic:
exact h
Proof state after:
case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
⊢ DeltaSpike Ψ ε (x / y) = 0 ∨ y = 0
Theorem: Smooth1Properties_below
Proof state before:
case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
⊢ DeltaSpike Ψ ε (x / y) = 0 ∨ y = 0
Tactic:
left
Proof state after:
case neg.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
⊢ DeltaSpike Ψ ε (x / y) = 0
Theorem: Smooth1Properties_below
Proof state before:
case neg.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
⊢ DeltaSpike Ψ ε (x / y) = 0
Tactic:
apply DeltaSpikeSupport εpos ?_ suppΨ
Proof state after:
case neg.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
⊢ x / y ∉ Icc (2 ^ (-ε)) (2 ^ ε)

𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
⊢ 0 ≤ x / y
Theorem: Smooth1Properties_below
Proof state before:
case neg.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
⊢ x / y ∉ Icc (2 ^ (-ε)) (2 ^ ε)
Tactic:
simp only [mem_Icc, not_and, not_le]
Proof state after:
case neg.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
⊢ 2 ^ (-ε) ≤ x / y → 2 ^ ε < x / y
Theorem: Smooth1Properties_below
Proof state before:
case neg.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
⊢ 2 ^ (-ε) ≤ x / y → 2 ^ ε < x / y
Tactic:
intro
Proof state after:
case neg.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
a✝ : 2 ^ (-ε) ≤ x / y
⊢ 2 ^ ε < x / y
Theorem: Smooth1Properties_below
Proof state before:
case neg.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
a✝ : 2 ^ (-ε) ≤ x / y
⊢ 2 ^ ε < x / y
Tactic:
linarith [(by apply (div_lt_iff (by linarith)).mpr; nlinarith : x / y < 2 ^ (-ε))]
Proof state after:
no goals
Theorem: Smooth1Properties_below
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
a✝ : 2 ^ (-ε) ≤ x / y
⊢ x / y < 2 ^ (-ε)
Tactic:
apply (div_lt_iff (by linarith)).mpr
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
a✝ : 2 ^ (-ε) ≤ x / y
⊢ x < 2 ^ (-ε) * y
Theorem: Smooth1Properties_below
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
a✝ : 2 ^ (-ε) ≤ x / y
⊢ x < 2 ^ (-ε) * y
Tactic:
nlinarith
Proof state after:
no goals
Theorem: Smooth1Properties_below
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
a✝ : 2 ^ (-ε) ≤ x / y
⊢ 0 < y
Tactic:
linarith
Proof state after:
no goals
Theorem: Smooth1Properties_below
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
⊢ 0 ≤ x / y
Tactic:
rw [le_div_iff (by linarith), zero_mul]
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
⊢ 0 ≤ x
Theorem: Smooth1Properties_below
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
⊢ 0 ≤ x
Tactic:
exact xpos.le
Proof state after:
no goals
Theorem: Smooth1Properties_below
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
⊢ 0 < y
Tactic:
linarith
Proof state after:
no goals
Theorem: Smooth1Properties_above_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
⊢ 2 ^ ε < x
Tactic:
calc
  x ≥ 1 + (2 * Real.log 2) * ε := hx
  _ > 2 ^ ε := ?_
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
⊢ 1 + 2 * Real.log 2 * ε > 2 ^ ε
Theorem: Smooth1Properties_above_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
⊢ 1 + 2 * Real.log 2 * ε > 2 ^ ε
Tactic:
refine lt_add_of_sub_left_lt <| (div_lt_iff hε.1).mp ?_
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
⊢ (2 ^ ε - 1) / ε < 2 * Real.log 2
Theorem: Smooth1Properties_above_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
⊢ (2 ^ ε - 1) / ε < 2 * Real.log 2
Tactic:
calc
  2 * Real.log 2 > 2 * (1 - 2 ^ (-ε)) / ε := ?_
  _ > 2 ^ ε * (1 - 2 ^ (-ε)) / ε := ?_
  _ = (2 ^ ε - 1) / ε := ?_
Proof state after:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
⊢ 2 * Real.log 2 > 2 * (1 - 2 ^ (-ε)) / ε

case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
⊢ 2 * (1 - 2 ^ (-ε)) / ε > 2 ^ ε * (1 - 2 ^ (-ε)) / ε

case calc_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
⊢ 2 ^ ε * (1 - 2 ^ (-ε)) / ε = (2 ^ ε - 1) / ε
Theorem: Smooth1Properties_above_aux
Proof state before:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
⊢ 2 * Real.log 2 > 2 * (1 - 2 ^ (-ε)) / ε
Tactic:
have := (mul_lt_mul_left (a := 2) (by norm_num)).mpr <| Smooth1Properties_estimate hε.1
Proof state after:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
this : 2 * ((1 - 2 ^ (-ε)) / ε) < 2 * Real.log 2
⊢ 2 * Real.log 2 > 2 * (1 - 2 ^ (-ε)) / ε
Theorem: Smooth1Properties_above_aux
Proof state before:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
this : 2 * ((1 - 2 ^ (-ε)) / ε) < 2 * Real.log 2
⊢ 2 * Real.log 2 > 2 * (1 - 2 ^ (-ε)) / ε
Tactic:
field_simp at this
Proof state after:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
this : 2 * (1 - 2 ^ (-ε)) / ε < 2 * Real.log 2
⊢ 2 * Real.log 2 > 2 * (1 - 2 ^ (-ε)) / ε
Theorem: Smooth1Properties_above_aux
Proof state before:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
this : 2 * (1 - 2 ^ (-ε)) / ε < 2 * Real.log 2
⊢ 2 * Real.log 2 > 2 * (1 - 2 ^ (-ε)) / ε
Tactic:
simp [this]
Proof state after:
no goals
Theorem: Smooth1Properties_above_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
⊢ 0 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: Smooth1Properties_above_aux
Proof state before:
case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
⊢ 2 * (1 - 2 ^ (-ε)) / ε > 2 ^ ε * (1 - 2 ^ (-ε)) / ε
Tactic:
have : (2 : ℝ) ^ ε < 2 := by
  nth_rewrite 1 [← pow_one 2]
  convert rpow_lt_rpow_of_exponent_lt (x := 2) (by norm_num) hε.2 <;> norm_num
Proof state after:
case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
this : 2 ^ ε < 2
⊢ 2 * (1 - 2 ^ (-ε)) / ε > 2 ^ ε * (1 - 2 ^ (-ε)) / ε