internlm/Lean-Github huggingface dataset:
Theorem: interval_approx_inf
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio ((b - a) / 3) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < (b - a) / 3
l2 : a < a + ε / 2
l3 : b - ε / 2 < b
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : (Icc (a + ε / 2) (b - ε / 2)).indicator 1 ≤ ψ
h4 : ψ ≤ (Ioo a b).indicator 1
h5 : Function.support ψ = Ioo a b
l4 : 0 ≤ b - a - ε
⊢ Icc (a + ε / 2) (b - ε / 2) ⊆ Ioi 0
Tactic:
intro t ht
Proof state after:
n : ℕ
A a b c d u x y t✝ σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio ((b - a) / 3) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < (b - a) / 3
l2 : a < a + ε / 2
l3 : b - ε / 2 < b
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : (Icc (a + ε / 2) (b - ε / 2)).indicator 1 ≤ ψ
h4 : ψ ≤ (Ioo a b).indicator 1
h5 : Function.support ψ = Ioo a b
l4 : 0 ≤ b - a - ε
t : ℝ
ht : t ∈ Icc (a + ε / 2) (b - ε / 2)
⊢ t ∈ Ioi 0
Theorem: interval_approx_inf
Proof state before:
n : ℕ
A a b c d u x y t✝ σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio ((b - a) / 3) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < (b - a) / 3
l2 : a < a + ε / 2
l3 : b - ε / 2 < b
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : (Icc (a + ε / 2) (b - ε / 2)).indicator 1 ≤ ψ
h4 : ψ ≤ (Ioo a b).indicator 1
h5 : Function.support ψ = Ioo a b
l4 : 0 ≤ b - a - ε
t : ℝ
ht : t ∈ Icc (a + ε / 2) (b - ε / 2)
⊢ t ∈ Ioi 0
Tactic:
simp at ht ⊢
Proof state after:
n : ℕ
A a b c d u x y t✝ σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio ((b - a) / 3) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < (b - a) / 3
l2 : a < a + ε / 2
l3 : b - ε / 2 < b
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : (Icc (a + ε / 2) (b - ε / 2)).indicator 1 ≤ ψ
h4 : ψ ≤ (Ioo a b).indicator 1
h5 : Function.support ψ = Ioo a b
l4 : 0 ≤ b - a - ε
t : ℝ
ht : a + ε / 2 ≤ t ∧ t ≤ b - ε / 2
⊢ 0 < t
Theorem: interval_approx_inf
Proof state before:
n : ℕ
A a b c d u x y t✝ σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio ((b - a) / 3) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < (b - a) / 3
l2 : a < a + ε / 2
l3 : b - ε / 2 < b
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : (Icc (a + ε / 2) (b - ε / 2)).indicator 1 ≤ ψ
h4 : ψ ≤ (Ioo a b).indicator 1
h5 : Function.support ψ = Ioo a b
l4 : 0 ≤ b - a - ε
t : ℝ
ht : a + ε / 2 ≤ t ∧ t ≤ b - ε / 2
⊢ 0 < t
Tactic:
linarith
Proof state after:
no goals
Theorem: interval_approx_inf
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio ((b - a) / 3) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < (b - a) / 3
l2 : a < a + ε / 2
l3 : b - ε / 2 < b
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : (Icc (a + ε / 2) (b - ε / 2)).indicator 1 ≤ ψ
h4 : ψ ≤ (Ioo a b).indicator 1
h5 : Function.support ψ = Ioo a b
l4 : 0 ≤ b - a - ε
l5 : Icc (a + ε / 2) (b - ε / 2) ⊆ Ioi 0
l6 : Icc (a + ε / 2) (b - ε / 2) ∩ Ioi 0 = Icc (a + ε / 2) (b - ε / 2)
⊢ ∫ (y : ℝ) in Ioi 0, (Icc (a + ε / 2) (b - ε / 2)).indicator 1 y = b - a - ε
Tactic:
simp [l6]
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio ((b - a) / 3) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < (b - a) / 3
l2 : a < a + ε / 2
l3 : b - ε / 2 < b
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : (Icc (a + ε / 2) (b - ε / 2)).indicator 1 ≤ ψ
h4 : ψ ≤ (Ioo a b).indicator 1
h5 : Function.support ψ = Ioo a b
l4 : 0 ≤ b - a - ε
l5 : Icc (a + ε / 2) (b - ε / 2) ⊆ Ioi 0
l6 : Icc (a + ε / 2) (b - ε / 2) ∩ Ioi 0 = Icc (a + ε / 2) (b - ε / 2)
⊢ (ENNReal.ofReal (b - ε / 2 - (a + ε / 2))).toReal = b - a - ε
Theorem: interval_approx_inf
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio ((b - a) / 3) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < (b - a) / 3
l2 : a < a + ε / 2
l3 : b - ε / 2 < b
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : (Icc (a + ε / 2) (b - ε / 2)).indicator 1 ≤ ψ
h4 : ψ ≤ (Ioo a b).indicator 1
h5 : Function.support ψ = Ioo a b
l4 : 0 ≤ b - a - ε
l5 : Icc (a + ε / 2) (b - ε / 2) ⊆ Ioi 0
l6 : Icc (a + ε / 2) (b - ε / 2) ∩ Ioi 0 = Icc (a + ε / 2) (b - ε / 2)
⊢ (ENNReal.ofReal (b - ε / 2 - (a + ε / 2))).toReal = b - a - ε
Tactic:
convert ENNReal.toReal_ofReal l4 using 3
Proof state after:
case h.e'_2.h.e'_1.h.e'_1
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio ((b - a) / 3) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < (b - a) / 3
l2 : a < a + ε / 2
l3 : b - ε / 2 < b
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : (Icc (a + ε / 2) (b - ε / 2)).indicator 1 ≤ ψ
h4 : ψ ≤ (Ioo a b).indicator 1
h5 : Function.support ψ = Ioo a b
l4 : 0 ≤ b - a - ε
l5 : Icc (a + ε / 2) (b - ε / 2) ⊆ Ioi 0
l6 : Icc (a + ε / 2) (b - ε / 2) ∩ Ioi 0 = Icc (a + ε / 2) (b - ε / 2)
⊢ b - ε / 2 - (a + ε / 2) = b - a - ε
Theorem: interval_approx_inf
Proof state before:
case h.e'_2.h.e'_1.h.e'_1
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio ((b - a) / 3) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < (b - a) / 3
l2 : a < a + ε / 2
l3 : b - ε / 2 < b
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : (Icc (a + ε / 2) (b - ε / 2)).indicator 1 ≤ ψ
h4 : ψ ≤ (Ioo a b).indicator 1
h5 : Function.support ψ = Ioo a b
l4 : 0 ≤ b - a - ε
l5 : Icc (a + ε / 2) (b - ε / 2) ⊆ Ioi 0
l6 : Icc (a + ε / 2) (b - ε / 2) ∩ Ioi 0 = Icc (a + ε / 2) (b - ε / 2)
⊢ b - ε / 2 - (a + ε / 2) = b - a - ε
Tactic:
ring
Proof state after:
no goals
Theorem: interval_approx_sup
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
⊢ ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
    ∃ ψ,
      ContDiff ℝ ⊤ ψ ∧
        HasCompactSupport ψ ∧
          closure (Function.support ψ) ⊆ Ioi 0 ∧ (Ico a b).indicator 1 ≤ ψ ∧ ∫ (y : ℝ) in Ioi 0, ψ y ≤ b - a + ε
Tactic:
have l1 : Iio (a / 2) ∈ 𝓝[>] 0 := nhdsWithin_le_nhds <| Iio_mem_nhds (by linarith)
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio (a / 2) ∈ 𝓝[>] 0
⊢ ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
    ∃ ψ,
      ContDiff ℝ ⊤ ψ ∧
        HasCompactSupport ψ ∧
          closure (Function.support ψ) ⊆ Ioi 0 ∧ (Ico a b).indicator 1 ≤ ψ ∧ ∫ (y : ℝ) in Ioi 0, ψ y ≤ b - a + ε
Theorem: interval_approx_sup
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio (a / 2) ∈ 𝓝[>] 0
⊢ ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
    ∃ ψ,
      ContDiff ℝ ⊤ ψ ∧
        HasCompactSupport ψ ∧
          closure (Function.support ψ) ⊆ Ioi 0 ∧ (Ico a b).indicator 1 ≤ ψ ∧ ∫ (y : ℝ) in Ioi 0, ψ y ≤ b - a + ε
Tactic:
filter_upwards [self_mem_nhdsWithin, l1] with ε (hε : 0 < ε) (hε' : ε < a / 2)
Proof state after:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio (a / 2) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < a / 2
⊢ ∃ ψ,
    ContDiff ℝ ⊤ ψ ∧
      HasCompactSupport ψ ∧
        closure (Function.support ψ) ⊆ Ioi 0 ∧ (Ico a b).indicator 1 ≤ ψ ∧ ∫ (y : ℝ) in Ioi 0, ψ y ≤ b - a + ε
Theorem: interval_approx_sup
Proof state before:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio (a / 2) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < a / 2
⊢ ∃ ψ,
    ContDiff ℝ ⊤ ψ ∧
      HasCompactSupport ψ ∧
        closure (Function.support ψ) ⊆ Ioi 0 ∧ (Ico a b).indicator 1 ≤ ψ ∧ ∫ (y : ℝ) in Ioi 0, ψ y ≤ b - a + ε
Tactic:
have l2 : a - ε / 2 < a := by linarith
Proof state after:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio (a / 2) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < a / 2
l2 : a - ε / 2 < a
⊢ ∃ ψ,
    ContDiff ℝ ⊤ ψ ∧
      HasCompactSupport ψ ∧
        closure (Function.support ψ) ⊆ Ioi 0 ∧ (Ico a b).indicator 1 ≤ ψ ∧ ∫ (y : ℝ) in Ioi 0, ψ y ≤ b - a + ε
Theorem: interval_approx_sup
Proof state before:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio (a / 2) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < a / 2
l2 : a - ε / 2 < a
⊢ ∃ ψ,
    ContDiff ℝ ⊤ ψ ∧
      HasCompactSupport ψ ∧
        closure (Function.support ψ) ⊆ Ioi 0 ∧ (Ico a b).indicator 1 ≤ ψ ∧ ∫ (y : ℝ) in Ioi 0, ψ y ≤ b - a + ε
Tactic:
have l3 : b < b + ε / 2 := by linarith
Proof state after:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio (a / 2) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < a / 2
l2 : a - ε / 2 < a
l3 : b < b + ε / 2
⊢ ∃ ψ,
    ContDiff ℝ ⊤ ψ ∧
      HasCompactSupport ψ ∧
        closure (Function.support ψ) ⊆ Ioi 0 ∧ (Ico a b).indicator 1 ≤ ψ ∧ ∫ (y : ℝ) in Ioi 0, ψ y ≤ b - a + ε
Theorem: interval_approx_sup
Proof state before:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio (a / 2) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < a / 2
l2 : a - ε / 2 < a
l3 : b < b + ε / 2
⊢ ∃ ψ,
    ContDiff ℝ ⊤ ψ ∧
      HasCompactSupport ψ ∧
        closure (Function.support ψ) ⊆ Ioi 0 ∧ (Ico a b).indicator 1 ≤ ψ ∧ ∫ (y : ℝ) in Ioi 0, ψ y ≤ b - a + ε
Tactic:
obtain ⟨ψ, h1, h2, h3, h4, h5⟩ := smooth_urysohn_support_Ioo l2 l3
Proof state after:
case h.intro.intro.intro.intro.intro
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio (a / 2) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < a / 2
l2 : a - ε / 2 < a
l3 : b < b + ε / 2
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : (Icc a b).indicator 1 ≤ ψ
h4 : ψ ≤ (Ioo (a - ε / 2) (b + ε / 2)).indicator 1
h5 : Function.support ψ = Ioo (a - ε / 2) (b + ε / 2)
⊢ ∃ ψ,
    ContDiff ℝ ⊤ ψ ∧
      HasCompactSupport ψ ∧
        closure (Function.support ψ) ⊆ Ioi 0 ∧ (Ico a b).indicator 1 ≤ ψ ∧ ∫ (y : ℝ) in Ioi 0, ψ y ≤ b - a + ε
Theorem: interval_approx_sup
Proof state before:
case h.intro.intro.intro.intro.intro
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio (a / 2) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < a / 2
l2 : a - ε / 2 < a
l3 : b < b + ε / 2
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : (Icc a b).indicator 1 ≤ ψ
h4 : ψ ≤ (Ioo (a - ε / 2) (b + ε / 2)).indicator 1
h5 : Function.support ψ = Ioo (a - ε / 2) (b + ε / 2)
⊢ ∃ ψ,
    ContDiff ℝ ⊤ ψ ∧
      HasCompactSupport ψ ∧
        closure (Function.support ψ) ⊆ Ioi 0 ∧ (Ico a b).indicator 1 ≤ ψ ∧ ∫ (y : ℝ) in Ioi 0, ψ y ≤ b - a + ε
Tactic:
refine ⟨ψ, h1, h2, ?_, ?_, ?_⟩
Proof state after:
case h.intro.intro.intro.intro.intro.refine_1
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio (a / 2) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < a / 2
l2 : a - ε / 2 < a
l3 : b < b + ε / 2
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : (Icc a b).indicator 1 ≤ ψ
h4 : ψ ≤ (Ioo (a - ε / 2) (b + ε / 2)).indicator 1
h5 : Function.support ψ = Ioo (a - ε / 2) (b + ε / 2)
⊢ closure (Function.support ψ) ⊆ Ioi 0

case h.intro.intro.intro.intro.intro.refine_2
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio (a / 2) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < a / 2
l2 : a - ε / 2 < a
l3 : b < b + ε / 2
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : (Icc a b).indicator 1 ≤ ψ
h4 : ψ ≤ (Ioo (a - ε / 2) (b + ε / 2)).indicator 1
h5 : Function.support ψ = Ioo (a - ε / 2) (b + ε / 2)
⊢ (Ico a b).indicator 1 ≤ ψ

case h.intro.intro.intro.intro.intro.refine_3
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio (a / 2) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < a / 2
l2 : a - ε / 2 < a
l3 : b < b + ε / 2
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : (Icc a b).indicator 1 ≤ ψ
h4 : ψ ≤ (Ioo (a - ε / 2) (b + ε / 2)).indicator 1
h5 : Function.support ψ = Ioo (a - ε / 2) (b + ε / 2)
⊢ ∫ (y : ℝ) in Ioi 0, ψ y ≤ b - a + ε
Theorem: interval_approx_sup
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
⊢ 0 < a / 2
Tactic:
linarith
Proof state after:
no goals
Theorem: interval_approx_sup
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio (a / 2) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < a / 2
⊢ a - ε / 2 < a
Tactic:
linarith
Proof state after:
no goals
Theorem: interval_approx_sup
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio (a / 2) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < a / 2
l2 : a - ε / 2 < a
⊢ b < b + ε / 2
Tactic:
linarith
Proof state after:
no goals
Theorem: interval_approx_sup
Proof state before:
case h.intro.intro.intro.intro.intro.refine_1
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio (a / 2) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < a / 2
l2 : a - ε / 2 < a
l3 : b < b + ε / 2
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : (Icc a b).indicator 1 ≤ ψ
h4 : ψ ≤ (Ioo (a - ε / 2) (b + ε / 2)).indicator 1
h5 : Function.support ψ = Ioo (a - ε / 2) (b + ε / 2)
⊢ closure (Function.support ψ) ⊆ Ioi 0
Tactic:
have l4 : a - ε / 2 < b + ε / 2 := by linarith
Proof state after:
case h.intro.intro.intro.intro.intro.refine_1
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio (a / 2) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < a / 2
l2 : a - ε / 2 < a
l3 : b < b + ε / 2
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : (Icc a b).indicator 1 ≤ ψ
h4 : ψ ≤ (Ioo (a - ε / 2) (b + ε / 2)).indicator 1
h5 : Function.support ψ = Ioo (a - ε / 2) (b + ε / 2)
l4 : a - ε / 2 < b + ε / 2
⊢ closure (Function.support ψ) ⊆ Ioi 0
Theorem: interval_approx_sup
Proof state before:
case h.intro.intro.intro.intro.intro.refine_1
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio (a / 2) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < a / 2
l2 : a - ε / 2 < a
l3 : b < b + ε / 2
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : (Icc a b).indicator 1 ≤ ψ
h4 : ψ ≤ (Ioo (a - ε / 2) (b + ε / 2)).indicator 1
h5 : Function.support ψ = Ioo (a - ε / 2) (b + ε / 2)
l4 : a - ε / 2 < b + ε / 2
⊢ closure (Function.support ψ) ⊆ Ioi 0
Tactic:
have l5 : ε / 2 < a := by linarith
Proof state after:
case h.intro.intro.intro.intro.intro.refine_1
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio (a / 2) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < a / 2
l2 : a - ε / 2 < a
l3 : b < b + ε / 2
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : (Icc a b).indicator 1 ≤ ψ
h4 : ψ ≤ (Ioo (a - ε / 2) (b + ε / 2)).indicator 1
h5 : Function.support ψ = Ioo (a - ε / 2) (b + ε / 2)
l4 : a - ε / 2 < b + ε / 2
l5 : ε / 2 < a
⊢ closure (Function.support ψ) ⊆ Ioi 0
Theorem: interval_approx_sup
Proof state before:
case h.intro.intro.intro.intro.intro.refine_1
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio (a / 2) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < a / 2
l2 : a - ε / 2 < a
l3 : b < b + ε / 2
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : (Icc a b).indicator 1 ≤ ψ
h4 : ψ ≤ (Ioo (a - ε / 2) (b + ε / 2)).indicator 1
h5 : Function.support ψ = Ioo (a - ε / 2) (b + ε / 2)
l4 : a - ε / 2 < b + ε / 2
l5 : ε / 2 < a
⊢ closure (Function.support ψ) ⊆ Ioi 0
Tactic:
simp [h5, l4.ne, Icc_subset_Ioi_iff l4.le, l5]
Proof state after:
no goals
Theorem: interval_approx_sup
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio (a / 2) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < a / 2
l2 : a - ε / 2 < a
l3 : b < b + ε / 2
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : (Icc a b).indicator 1 ≤ ψ
h4 : ψ ≤ (Ioo (a - ε / 2) (b + ε / 2)).indicator 1
h5 : Function.support ψ = Ioo (a - ε / 2) (b + ε / 2)
⊢ a - ε / 2 < b + ε / 2
Tactic:
linarith
Proof state after:
no goals
Theorem: interval_approx_sup
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio (a / 2) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < a / 2
l2 : a - ε / 2 < a
l3 : b < b + ε / 2
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : (Icc a b).indicator 1 ≤ ψ
h4 : ψ ≤ (Ioo (a - ε / 2) (b + ε / 2)).indicator 1
h5 : Function.support ψ = Ioo (a - ε / 2) (b + ε / 2)
l4 : a - ε / 2 < b + ε / 2
⊢ ε / 2 < a
Tactic:
linarith
Proof state after:
no goals
Theorem: interval_approx_sup
Proof state before:
case h.intro.intro.intro.intro.intro.refine_2
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio (a / 2) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < a / 2
l2 : a - ε / 2 < a
l3 : b < b + ε / 2
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : (Icc a b).indicator 1 ≤ ψ
h4 : ψ ≤ (Ioo (a - ε / 2) (b + ε / 2)).indicator 1
h5 : Function.support ψ = Ioo (a - ε / 2) (b + ε / 2)
⊢ (Ico a b).indicator 1 ≤ ψ
Tactic:
apply le_trans ?_ h3
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio (a / 2) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < a / 2
l2 : a - ε / 2 < a
l3 : b < b + ε / 2
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : (Icc a b).indicator 1 ≤ ψ
h4 : ψ ≤ (Ioo (a - ε / 2) (b + ε / 2)).indicator 1
h5 : Function.support ψ = Ioo (a - ε / 2) (b + ε / 2)
⊢ (Ico a b).indicator 1 ≤ (Icc a b).indicator 1
Theorem: interval_approx_sup
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio (a / 2) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < a / 2
l2 : a - ε / 2 < a
l3 : b < b + ε / 2
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : (Icc a b).indicator 1 ≤ ψ
h4 : ψ ≤ (Ioo (a - ε / 2) (b + ε / 2)).indicator 1
h5 : Function.support ψ = Ioo (a - ε / 2) (b + ε / 2)
⊢ (Ico a b).indicator 1 ≤ (Icc a b).indicator 1
Tactic:
apply indicator_le_indicator_of_subset Ico_subset_Icc_self (by simp)
Proof state after:
no goals
Theorem: interval_approx_sup
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio (a / 2) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < a / 2
l2 : a - ε / 2 < a
l3 : b < b + ε / 2
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : (Icc a b).indicator 1 ≤ ψ
h4 : ψ ≤ (Ioo (a - ε / 2) (b + ε / 2)).indicator 1
h5 : Function.support ψ = Ioo (a - ε / 2) (b + ε / 2)
⊢ ∀ (a : ℝ), 0 ≤ 1 a
Tactic:
simp
Proof state after:
no goals
Theorem: interval_approx_sup
Proof state before:
case h.intro.intro.intro.intro.intro.refine_3
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio (a / 2) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < a / 2
l2 : a - ε / 2 < a
l3 : b < b + ε / 2
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : (Icc a b).indicator 1 ≤ ψ
h4 : ψ ≤ (Ioo (a - ε / 2) (b + ε / 2)).indicator 1
h5 : Function.support ψ = Ioo (a - ε / 2) (b + ε / 2)
⊢ ∫ (y : ℝ) in Ioi 0, ψ y ≤ b - a + ε
Tactic:
have l4 : 0 ≤ b - a + ε := by linarith
Proof state after:
case h.intro.intro.intro.intro.intro.refine_3
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio (a / 2) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < a / 2
l2 : a - ε / 2 < a
l3 : b < b + ε / 2
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : (Icc a b).indicator 1 ≤ ψ
h4 : ψ ≤ (Ioo (a - ε / 2) (b + ε / 2)).indicator 1
h5 : Function.support ψ = Ioo (a - ε / 2) (b + ε / 2)
l4 : 0 ≤ b - a + ε
⊢ ∫ (y : ℝ) in Ioi 0, ψ y ≤ b - a + ε
Theorem: interval_approx_sup
Proof state before:
case h.intro.intro.intro.intro.intro.refine_3
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio (a / 2) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < a / 2
l2 : a - ε / 2 < a
l3 : b < b + ε / 2
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : (Icc a b).indicator 1 ≤ ψ
h4 : ψ ≤ (Ioo (a - ε / 2) (b + ε / 2)).indicator 1
h5 : Function.support ψ = Ioo (a - ε / 2) (b + ε / 2)
l4 : 0 ≤ b - a + ε
⊢ ∫ (y : ℝ) in Ioi 0, ψ y ≤ b - a + ε
Tactic:
have l5 : Ioo (a - ε / 2) (b + ε / 2) ⊆ Ioi 0 := by intro t ht ; simp at ht ⊢ ; linarith
Proof state after:
case h.intro.intro.intro.intro.intro.refine_3
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio (a / 2) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < a / 2
l2 : a - ε / 2 < a
l3 : b < b + ε / 2
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : (Icc a b).indicator 1 ≤ ψ
h4 : ψ ≤ (Ioo (a - ε / 2) (b + ε / 2)).indicator 1
h5 : Function.support ψ = Ioo (a - ε / 2) (b + ε / 2)
l4 : 0 ≤ b - a + ε
l5 : Ioo (a - ε / 2) (b + ε / 2) ⊆ Ioi 0
⊢ ∫ (y : ℝ) in Ioi 0, ψ y ≤ b - a + ε
Theorem: interval_approx_sup
Proof state before:
case h.intro.intro.intro.intro.intro.refine_3
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio (a / 2) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < a / 2
l2 : a - ε / 2 < a
l3 : b < b + ε / 2
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : (Icc a b).indicator 1 ≤ ψ
h4 : ψ ≤ (Ioo (a - ε / 2) (b + ε / 2)).indicator 1
h5 : Function.support ψ = Ioo (a - ε / 2) (b + ε / 2)
l4 : 0 ≤ b - a + ε
l5 : Ioo (a - ε / 2) (b + ε / 2) ⊆ Ioi 0
⊢ ∫ (y : ℝ) in Ioi 0, ψ y ≤ b - a + ε
Tactic:
have l6 : Ioo (a - ε / 2) (b + ε / 2) ∩ Ioi 0 = Ioo (a - ε / 2) (b + ε / 2) := inter_eq_left.mpr l5
Proof state after:
case h.intro.intro.intro.intro.intro.refine_3
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio (a / 2) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < a / 2
l2 : a - ε / 2 < a
l3 : b < b + ε / 2
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : (Icc a b).indicator 1 ≤ ψ
h4 : ψ ≤ (Ioo (a - ε / 2) (b + ε / 2)).indicator 1
h5 : Function.support ψ = Ioo (a - ε / 2) (b + ε / 2)
l4 : 0 ≤ b - a + ε
l5 : Ioo (a - ε / 2) (b + ε / 2) ⊆ Ioi 0
l6 : Ioo (a - ε / 2) (b + ε / 2) ∩ Ioi 0 = Ioo (a - ε / 2) (b + ε / 2)
⊢ ∫ (y : ℝ) in Ioi 0, ψ y ≤ b - a + ε