Theorem: interval_approx_sup (PrimeNumberTheoremAnd/Wiener.lean)

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)
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 + ε

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)
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 + ε

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
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 + ε

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
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 + ε

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
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 + ε

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, ?_, ?_, ?_⟩
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 + ε

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
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

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
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

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]
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
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

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)
State after:
no goals

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
State after:
no goals

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
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 + ε

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
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 + ε

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
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 + ε

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
l6 : Ioo (a - ε / 2) (b + ε / 2) ∩ Ioi 0 = Ioo (a - ε / 2) (b + ε / 2)
⊢ ∫ (y : ℝ) in Ioi 0, ψ y ≤ b - a + ε
Tactic:
have l7 : ∫ y in Ioi 0, indicator (Ioo (a - ε / 2) (b + ε / 2)) 1 y = b - a + ε := by
  simp [l6] ; convert ENNReal.toReal_ofReal l4 using 3 ; ring
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)
l7 : ∫ (y : ℝ) in Ioi 0, (Ioo (a - ε / 2) (b + ε / 2)).indicator 1 y = b - a + ε
⊢ ∫ (y : ℝ) in Ioi 0, ψ y ≤ b - a + ε

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
l6 : Ioo (a - ε / 2) (b + ε / 2) ∩ Ioi 0 = Ioo (a - ε / 2) (b + ε / 2)
l7 : ∫ (y : ℝ) in Ioi 0, (Ioo (a - ε / 2) (b + ε / 2)).indicator 1 y = b - a + ε
⊢ ∫ (y : ℝ) in Ioi 0, ψ y ≤ b - a + ε
Tactic:
have l8 : IntegrableOn ψ (Ioi 0) volume := (h1.continuous.integrable_of_hasCompactSupport h2).integrableOn
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)
l7 : ∫ (y : ℝ) in Ioi 0, (Ioo (a - ε / 2) (b + ε / 2)).indicator 1 y = b - a + ε
l8 : IntegrableOn ψ (Ioi 0) volume
⊢ ∫ (y : ℝ) in Ioi 0, ψ y ≤ b - a + ε

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
l6 : Ioo (a - ε / 2) (b + ε / 2) ∩ Ioi 0 = Ioo (a - ε / 2) (b + ε / 2)
l7 : ∫ (y : ℝ) in Ioi 0, (Ioo (a - ε / 2) (b + ε / 2)).indicator 1 y = b - a + ε
l8 : IntegrableOn ψ (Ioi 0) volume
⊢ ∫ (y : ℝ) in Ioi 0, ψ y ≤ b - a + ε
Tactic:
rw [← l7]
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)
l7 : ∫ (y : ℝ) in Ioi 0, (Ioo (a - ε / 2) (b + ε / 2)).indicator 1 y = b - a + ε
l8 : IntegrableOn ψ (Ioi 0) volume
⊢ ∫ (y : ℝ) in Ioi 0, ψ y ≤ ∫ (y : ℝ) in Ioi 0, (Ioo (a - ε / 2) (b + ε / 2)).indicator 1 y

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
l6 : Ioo (a - ε / 2) (b + ε / 2) ∩ Ioi 0 = Ioo (a - ε / 2) (b + ε / 2)
l7 : ∫ (y : ℝ) in Ioi 0, (Ioo (a - ε / 2) (b + ε / 2)).indicator 1 y = b - a + ε
l8 : IntegrableOn ψ (Ioi 0) volume
⊢ ∫ (y : ℝ) in Ioi 0, ψ y ≤ ∫ (y : ℝ) in Ioi 0, (Ioo (a - ε / 2) (b + ε / 2)).indicator 1 y
Tactic:
refine setIntegral_mono l8 ?_ h4
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)
l7 : ∫ (y : ℝ) in Ioi 0, (Ioo (a - ε / 2) (b + ε / 2)).indicator 1 y = b - a + ε
l8 : IntegrableOn ψ (Ioi 0) volume
⊢ IntegrableOn (fun y => (Ioo (a - ε / 2) (b + ε / 2)).indicator 1 y) (Ioi 0) volume

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
l6 : Ioo (a - ε / 2) (b + ε / 2) ∩ Ioi 0 = Ioo (a - ε / 2) (b + ε / 2)
l7 : ∫ (y : ℝ) in Ioi 0, (Ioo (a - ε / 2) (b + ε / 2)).indicator 1 y = b - a + ε
l8 : IntegrableOn ψ (Ioi 0) volume
⊢ IntegrableOn (fun y => (Ioo (a - ε / 2) (b + ε / 2)).indicator 1 y) (Ioi 0) volume
Tactic:
rw [IntegrableOn, integrable_indicator_iff measurableSet_Ioo]
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)
l7 : ∫ (y : ℝ) in Ioi 0, (Ioo (a - ε / 2) (b + ε / 2)).indicator 1 y = b - a + ε
l8 : IntegrableOn ψ (Ioi 0) volume
⊢ IntegrableOn 1 (Ioo (a - ε / 2) (b + ε / 2)) (volume.restrict (Ioi 0))

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
l6 : Ioo (a - ε / 2) (b + ε / 2) ∩ Ioi 0 = Ioo (a - ε / 2) (b + ε / 2)
l7 : ∫ (y : ℝ) in Ioi 0, (Ioo (a - ε / 2) (b + ε / 2)).indicator 1 y = b - a + ε
l8 : IntegrableOn ψ (Ioi 0) volume
⊢ IntegrableOn 1 (Ioo (a - ε / 2) (b + ε / 2)) (volume.restrict (Ioi 0))
Tactic:
apply IntegrableOn.mono ?_ subset_rfl Measure.restrict_le_self
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)
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)
l7 : ∫ (y : ℝ) in Ioi 0, (Ioo (a - ε / 2) (b + ε / 2)).indicator 1 y = b - a + ε
l8 : IntegrableOn ψ (Ioi 0) volume
⊢ IntegrableOn 1 (Ioo (a - ε / 2) (b + ε / 2)) volume

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 : 0 ≤ b - a + ε
l5 : Ioo (a - ε / 2) (b + ε / 2) ⊆ Ioi 0
l6 : Ioo (a - ε / 2) (b + ε / 2) ∩ Ioi 0 = Ioo (a - ε / 2) (b + ε / 2)
l7 : ∫ (y : ℝ) in Ioi 0, (Ioo (a - ε / 2) (b + ε / 2)).indicator 1 y = b - a + ε
l8 : IntegrableOn ψ (Ioi 0) volume
⊢ IntegrableOn 1 (Ioo (a - ε / 2) (b + ε / 2)) volume
Tactic:
apply integrableOn_const.mpr
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)
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)
l7 : ∫ (y : ℝ) in Ioi 0, (Ioo (a - ε / 2) (b + ε / 2)).indicator 1 y = b - a + ε
l8 : IntegrableOn ψ (Ioi 0) volume
⊢ Real.one = 0 ∨ volume (Ioo (a - ε / 2) (b + ε / 2)) < ⊤

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 : 0 ≤ b - a + ε
l5 : Ioo (a - ε / 2) (b + ε / 2) ⊆ Ioi 0
l6 : Ioo (a - ε / 2) (b + ε / 2) ∩ Ioi 0 = Ioo (a - ε / 2) (b + ε / 2)
l7 : ∫ (y : ℝ) in Ioi 0, (Ioo (a - ε / 2) (b + ε / 2)).indicator 1 y = b - a + ε
l8 : IntegrableOn ψ (Ioi 0) volume
⊢ Real.one = 0 ∨ volume (Ioo (a - ε / 2) (b + ε / 2)) < ⊤
Tactic:
simp
State after:
no goals

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)
⊢ 0 ≤ b - a + ε
Tactic:
linarith
State after:
no goals

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 : 0 ≤ b - a + ε
⊢ Ioo (a - ε / 2) (b + ε / 2) ⊆ Ioi 0
Tactic:
intro t ht
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)
l4 : 0 ≤ b - a + ε
t : ℝ
ht : t ∈ Ioo (a - ε / 2) (b + ε / 2)
⊢ t ∈ Ioi 0

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 : 0 ≤ b - a + ε
t : ℝ
ht : t ∈ Ioo (a - ε / 2) (b + ε / 2)
⊢ t ∈ Ioi 0
Tactic:
simp at ht ⊢
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)
l4 : 0 ≤ b - a + ε
t : ℝ
ht : a - ε / 2 < t ∧ t < b + ε / 2
⊢ 0 < t

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 : 0 ≤ b - a + ε
t : ℝ
ht : a - ε / 2 < t ∧ t < b + ε / 2
⊢ 0 < t
Tactic:
linarith
State after:
no goals

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 : 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, (Ioo (a - ε / 2) (b + ε / 2)).indicator 1 y = b - a + ε
Tactic:
simp [l6]
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)
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)
⊢ (ENNReal.ofReal (b + ε / 2 - (a - ε / 2))).toReal = b - a + ε

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 : 0 ≤ b - a + ε
l5 : Ioo (a - ε / 2) (b + ε / 2) ⊆ Ioi 0
l6 : Ioo (a - ε / 2) (b + ε / 2) ∩ Ioi 0 = Ioo (a - ε / 2) (b + ε / 2)
⊢ (ENNReal.ofReal (b + ε / 2 - (a - ε / 2))).toReal = b - a + ε
Tactic:
convert ENNReal.toReal_ofReal l4 using 3
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 (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)
⊢ b + ε / 2 - (a - ε / 2) = b - a + ε

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 (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)
⊢ b + ε / 2 - (a - ε / 2) = b - a + ε
Tactic:
ring
State after:
no goals