internlm/Lean-Github huggingface dataset:
Theorem: interval_approx_inf
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 ((b - a) / 3) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < (b - a) / 3
⊢ ∃ ψ,
    ContDiff ℝ ⊤ ψ ∧
      HasCompactSupport ψ ∧
        closure (Function.support ψ) ⊆ Ioi 0 ∧ ψ ≤ (Ico a b).indicator 1 ∧ b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
Tactic:
have l2 : a < a + ε / 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 ((b - a) / 3) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < (b - a) / 3
l2 : a < a + ε / 2
⊢ ∃ ψ,
    ContDiff ℝ ⊤ ψ ∧
      HasCompactSupport ψ ∧
        closure (Function.support ψ) ⊆ Ioi 0 ∧ ψ ≤ (Ico a b).indicator 1 ∧ b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
Theorem: interval_approx_inf
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 ((b - a) / 3) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < (b - a) / 3
l2 : a < a + ε / 2
⊢ ∃ ψ,
    ContDiff ℝ ⊤ ψ ∧
      HasCompactSupport ψ ∧
        closure (Function.support ψ) ⊆ Ioi 0 ∧ ψ ≤ (Ico a b).indicator 1 ∧ b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
Tactic:
have l3 : b - ε / 2 < b := 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 ((b - a) / 3) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < (b - a) / 3
l2 : a < a + ε / 2
l3 : b - ε / 2 < b
⊢ ∃ ψ,
    ContDiff ℝ ⊤ ψ ∧
      HasCompactSupport ψ ∧
        closure (Function.support ψ) ⊆ Ioi 0 ∧ ψ ≤ (Ico a b).indicator 1 ∧ b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
Theorem: interval_approx_inf
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 ((b - a) / 3) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < (b - a) / 3
l2 : a < a + ε / 2
l3 : b - ε / 2 < b
⊢ ∃ ψ,
    ContDiff ℝ ⊤ ψ ∧
      HasCompactSupport ψ ∧
        closure (Function.support ψ) ⊆ Ioi 0 ∧ ψ ≤ (Ico a b).indicator 1 ∧ b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
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 ((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
⊢ ∃ ψ,
    ContDiff ℝ ⊤ ψ ∧
      HasCompactSupport ψ ∧
        closure (Function.support ψ) ⊆ Ioi 0 ∧ ψ ≤ (Ico a b).indicator 1 ∧ b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
Theorem: interval_approx_inf
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 ((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
⊢ ∃ ψ,
    ContDiff ℝ ⊤ ψ ∧
      HasCompactSupport ψ ∧
        closure (Function.support ψ) ⊆ Ioi 0 ∧ ψ ≤ (Ico a b).indicator 1 ∧ b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
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 ((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
⊢ 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 ((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
⊢ ψ ≤ (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 ((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
⊢ b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
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
⊢ 0 < (b - a) / 3
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
⊢ a < a + ε / 2
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
⊢ b - ε / 2 < b
Tactic:
linarith
Proof state after:
no goals
Theorem: interval_approx_inf
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 ((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
⊢ closure (Function.support ψ) ⊆ Ioi 0
Tactic:
simp [h5, hab.ne, Icc_subset_Ioi_iff hab.le, ha]
Proof state after:
no goals
Theorem: interval_approx_inf
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 ((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
⊢ ψ ≤ (Ico a b).indicator 1
Tactic:
exact h4.trans <| indicator_le_indicator_of_subset Ioo_subset_Ico_self (by simp)
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
⊢ ∀ (a : ℝ), 0 ≤ 1 a
Tactic:
simp
Proof state after:
no goals
Theorem: interval_approx_inf
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 ((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
⊢ b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
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 ((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 - ε
⊢ b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
Theorem: interval_approx_inf
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 ((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 - ε
⊢ b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
Tactic:
have l5 : Icc (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 ((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
⊢ b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
Theorem: interval_approx_inf
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 ((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
⊢ b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
Tactic:
have l6 : Icc (a + ε / 2) (b - ε / 2) ∩ Ioi 0 = Icc (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 ((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 - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
Theorem: interval_approx_inf
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 ((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 - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
Tactic:
have l7 : ∫ y in Ioi 0, indicator (Icc (a + ε / 2) (b - ε / 2)) 1 y = b - a - ε := by
  simp [l6] ; convert ENNReal.toReal_ofReal l4 using 3 ; ring
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 ((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)
l7 : ∫ (y : ℝ) in Ioi 0, (Icc (a + ε / 2) (b - ε / 2)).indicator 1 y = b - a - ε
⊢ b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
Theorem: interval_approx_inf
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 ((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)
l7 : ∫ (y : ℝ) in Ioi 0, (Icc (a + ε / 2) (b - ε / 2)).indicator 1 y = b - a - ε
⊢ b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
Tactic:
have l8 : IntegrableOn ψ (Ioi 0) volume := (h1.continuous.integrable_of_hasCompactSupport h2).integrableOn
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 ((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)
l7 : ∫ (y : ℝ) in Ioi 0, (Icc (a + ε / 2) (b - ε / 2)).indicator 1 y = b - a - ε
l8 : IntegrableOn ψ (Ioi 0) volume
⊢ b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
Theorem: interval_approx_inf
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 ((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)
l7 : ∫ (y : ℝ) in Ioi 0, (Icc (a + ε / 2) (b - ε / 2)).indicator 1 y = b - a - ε
l8 : IntegrableOn ψ (Ioi 0) volume
⊢ b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
Tactic:
rw [← l7]
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 ((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)
l7 : ∫ (y : ℝ) in Ioi 0, (Icc (a + ε / 2) (b - ε / 2)).indicator 1 y = b - a - ε
l8 : IntegrableOn ψ (Ioi 0) volume
⊢ ∫ (y : ℝ) in Ioi 0, (Icc (a + ε / 2) (b - ε / 2)).indicator 1 y ≤ ∫ (y : ℝ) in Ioi 0, ψ y
Theorem: interval_approx_inf
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 ((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)
l7 : ∫ (y : ℝ) in Ioi 0, (Icc (a + ε / 2) (b - ε / 2)).indicator 1 y = b - a - ε
l8 : IntegrableOn ψ (Ioi 0) volume
⊢ ∫ (y : ℝ) in Ioi 0, (Icc (a + ε / 2) (b - ε / 2)).indicator 1 y ≤ ∫ (y : ℝ) in Ioi 0, ψ y
Tactic:
apply setIntegral_mono ?_ l8 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 ((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)
l7 : ∫ (y : ℝ) in Ioi 0, (Icc (a + ε / 2) (b - ε / 2)).indicator 1 y = b - a - ε
l8 : IntegrableOn ψ (Ioi 0) volume
⊢ IntegrableOn ((Icc (a + ε / 2) (b - ε / 2)).indicator 1) (Ioi 0) volume
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)
l7 : ∫ (y : ℝ) in Ioi 0, (Icc (a + ε / 2) (b - ε / 2)).indicator 1 y = b - a - ε
l8 : IntegrableOn ψ (Ioi 0) volume
⊢ IntegrableOn ((Icc (a + ε / 2) (b - ε / 2)).indicator 1) (Ioi 0) volume
Tactic:
rw [IntegrableOn, integrable_indicator_iff measurableSet_Icc]
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)
l7 : ∫ (y : ℝ) in Ioi 0, (Icc (a + ε / 2) (b - ε / 2)).indicator 1 y = b - a - ε
l8 : IntegrableOn ψ (Ioi 0) volume
⊢ IntegrableOn 1 (Icc (a + ε / 2) (b - ε / 2)) (volume.restrict (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 - ε
l5 : Icc (a + ε / 2) (b - ε / 2) ⊆ Ioi 0
l6 : Icc (a + ε / 2) (b - ε / 2) ∩ Ioi 0 = Icc (a + ε / 2) (b - ε / 2)
l7 : ∫ (y : ℝ) in Ioi 0, (Icc (a + ε / 2) (b - ε / 2)).indicator 1 y = b - a - ε
l8 : IntegrableOn ψ (Ioi 0) volume
⊢ IntegrableOn 1 (Icc (a + ε / 2) (b - ε / 2)) (volume.restrict (Ioi 0))
Tactic:
apply IntegrableOn.mono ?_ subset_rfl Measure.restrict_le_self
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)
l7 : ∫ (y : ℝ) in Ioi 0, (Icc (a + ε / 2) (b - ε / 2)).indicator 1 y = b - a - ε
l8 : IntegrableOn ψ (Ioi 0) volume
⊢ IntegrableOn 1 (Icc (a + ε / 2) (b - ε / 2)) volume
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)
l7 : ∫ (y : ℝ) in Ioi 0, (Icc (a + ε / 2) (b - ε / 2)).indicator 1 y = b - a - ε
l8 : IntegrableOn ψ (Ioi 0) volume
⊢ IntegrableOn 1 (Icc (a + ε / 2) (b - ε / 2)) volume
Tactic:
apply integrableOn_const.mpr
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)
l7 : ∫ (y : ℝ) in Ioi 0, (Icc (a + ε / 2) (b - ε / 2)).indicator 1 y = b - a - ε
l8 : IntegrableOn ψ (Ioi 0) volume
⊢ Real.one = 0 ∨ volume (Icc (a + ε / 2) (b - ε / 2)) < ⊤
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)
l7 : ∫ (y : ℝ) in Ioi 0, (Icc (a + ε / 2) (b - ε / 2)).indicator 1 y = b - a - ε
l8 : IntegrableOn ψ (Ioi 0) volume
⊢ Real.one = 0 ∨ volume (Icc (a + ε / 2) (b - ε / 2)) < ⊤
Tactic:
simp
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
⊢ 0 ≤ b - a - ε
Tactic:
linarith
Proof state after:
no goals