internlm/Lean-Github huggingface dataset:
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
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
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)
l7 : ∫ (y : ℝ) in Ioi 0, (Ioo (a - ε / 2) (b + ε / 2)).indicator 1 y = 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 + ε
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
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)
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 + ε
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
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]
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)
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
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
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
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)
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
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
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]
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)
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))
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
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
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)
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
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 : 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
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)
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)) < ⊤
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 : 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
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)
⊢ 0 ≤ b - 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
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
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)
l4 : 0 ≤ b - a + ε
t : ℝ
ht : t ∈ Ioo (a - ε / 2) (b + ε / 2)
⊢ t ∈ Ioi 0
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 : 0 ≤ b - a + ε
t : ℝ
ht : t ∈ Ioo (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 (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
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 : 0 ≤ b - a + ε
t : ℝ
ht : a - ε / 2 < t ∧ t < b + ε / 2
⊢ 0 < t
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 : 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]
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)
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 + ε
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 : 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
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 (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 + ε
Theorem: interval_approx_sup
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 (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
Proof state after:
no goals
Theorem: WI_summable
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
g : ℝ → ℝ
hg : HasCompactSupport g
hx : 0 < x
⊢ Summable fun n => f n * g (↑n / x)
Tactic:
obtain ⟨M, hM⟩ := hg.bddAbove.mono subset_closure
Proof state after:
case intro
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
g : ℝ → ℝ
hg : HasCompactSupport g
hx : 0 < x
M : ℝ
hM : M ∈ upperBounds (Function.support g)
⊢ Summable fun n => f n * g (↑n / x)
Theorem: WI_summable
Proof state before:
case intro
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
g : ℝ → ℝ
hg : HasCompactSupport g
hx : 0 < x
M : ℝ
hM : M ∈ upperBounds (Function.support g)
⊢ Summable fun n => f n * g (↑n / x)
Tactic:
apply summable_of_finite_support
Proof state after:
case intro.h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
g : ℝ → ℝ
hg : HasCompactSupport g
hx : 0 < x
M : ℝ
hM : M ∈ upperBounds (Function.support g)
⊢ (Function.support fun n => f n * g (↑n / x)).Finite
Theorem: WI_summable
Proof state before:
case intro.h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
g : ℝ → ℝ
hg : HasCompactSupport g
hx : 0 < x
M : ℝ
hM : M ∈ upperBounds (Function.support g)
⊢ (Function.support fun n => f n * g (↑n / x)).Finite
Tactic:
simp only [Function.support_mul]
Proof state after:
case intro.h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
g : ℝ → ℝ
hg : HasCompactSupport g
hx : 0 < x
M : ℝ
hM : M ∈ upperBounds (Function.support g)
⊢ ((Function.support fun x => f x) ∩ Function.support fun x_1 => g (↑x_1 / x)).Finite
Theorem: WI_summable
Proof state before:
case intro.h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
g : ℝ → ℝ
hg : HasCompactSupport g
hx : 0 < x
M : ℝ
hM : M ∈ upperBounds (Function.support g)
⊢ ((Function.support fun x => f x) ∩ Function.support fun x_1 => g (↑x_1 / x)).Finite
Tactic:
apply Finite.inter_of_right
Proof state after:
case intro.h.hs
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
g : ℝ → ℝ
hg : HasCompactSupport g
hx : 0 < x
M : ℝ
hM : M ∈ upperBounds (Function.support g)
⊢ (Function.support fun x_1 => g (↑x_1 / x)).Finite
Theorem: WI_summable
Proof state before:
case intro.h.hs
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
g : ℝ → ℝ
hg : HasCompactSupport g
hx : 0 < x
M : ℝ
hM : M ∈ upperBounds (Function.support g)
⊢ (Function.support fun x_1 => g (↑x_1 / x)).Finite
Tactic:
rw [finite_iff_bddAbove]
Proof state after:
case intro.h.hs
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
g : ℝ → ℝ
hg : HasCompactSupport g
hx : 0 < x
M : ℝ
hM : M ∈ upperBounds (Function.support g)
⊢ BddAbove (Function.support fun x_1 => g (↑x_1 / x))
Theorem: WI_summable
Proof state before:
case intro.h.hs
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
g : ℝ → ℝ
hg : HasCompactSupport g
hx : 0 < x
M : ℝ
hM : M ∈ upperBounds (Function.support g)
⊢ BddAbove (Function.support fun x_1 => g (↑x_1 / x))
Tactic:
exact ⟨Nat.ceil (M * x), fun i hi => by simpa using Nat.ceil_mono ((div_le_iff hx).mp (hM hi))⟩
Proof state after:
no goals
Theorem: WI_summable
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
g : ℝ → ℝ
hg : HasCompactSupport g
hx : 0 < x
M : ℝ
hM : M ∈ upperBounds (Function.support g)
i : ℕ
hi : i ∈ Function.support fun x_1 => g (↑x_1 / x)
⊢ i ≤ ⌈M * x⌉₊
Tactic:
simpa using Nat.ceil_mono ((div_le_iff hx).mp (hM hi))
Proof state after:
no goals
Theorem: WI_sum_le
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
g₁ g₂ : ℝ → ℝ
hf : 0 ≤ f
hg : g₁ ≤ g₂
hx : 0 < x
hg₁ : HasCompactSupport g₁
hg₂ : HasCompactSupport g₂
⊢ (∑' (n : ℕ), f n * g₁ (↑n / x)) / x ≤ (∑' (n : ℕ), f n * g₂ (↑n / x)) / x
Tactic:
apply div_le_div_of_nonneg_right ?_ hx.le
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
g₁ g₂ : ℝ → ℝ
hf : 0 ≤ f
hg : g₁ ≤ g₂
hx : 0 < x
hg₁ : HasCompactSupport g₁
hg₂ : HasCompactSupport g₂
⊢ ∑' (n : ℕ), f n * g₁ (↑n / x) ≤ ∑' (n : ℕ), f n * g₂ (↑n / x)
Theorem: WI_sum_le
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
g₁ g₂ : ℝ → ℝ
hf : 0 ≤ f
hg : g₁ ≤ g₂
hx : 0 < x
hg₁ : HasCompactSupport g₁
hg₂ : HasCompactSupport g₂
⊢ ∑' (n : ℕ), f n * g₁ (↑n / x) ≤ ∑' (n : ℕ), f n * g₂ (↑n / x)
Tactic:
exact tsum_le_tsum (fun n => mul_le_mul_of_nonneg_left (hg _) (hf _)) (WI_summable hg₁ hx) (WI_summable hg₂ hx)
Proof state after:
no goals
Theorem: WI_sum_Iab_le
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
⊢ (∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x)) / x ≤ C * 2 * b
Tactic:
have hb' : 0 < 2 / b := by positivity
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
⊢ (∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x)) / x ≤ C * 2 * b