internlm/Lean-Github huggingface dataset:
Theorem: sum_range_succ
Proof state before:
n✝ : ℕ
A a✝ b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℕ → ℝ
n : ℕ
this : ∑ i ∈ Finset.range n, (a (i + 1) - a i) = a n - a 0
⊢ ∑ i ∈ Finset.range n, a (i + 1) = ∑ i ∈ Finset.range (n + 1), a i - a 0
Tactic:
rw [Finset.sum_sub_distrib, sub_eq_iff_eq_add] at this
Proof state after:
n✝ : ℕ
A a✝ b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℕ → ℝ
n : ℕ
this : ∑ x ∈ Finset.range n, a (x + 1) = a n - a 0 + ∑ x ∈ Finset.range n, a x
⊢ ∑ i ∈ Finset.range n, a (i + 1) = ∑ i ∈ Finset.range (n + 1), a i - a 0
Theorem: sum_range_succ
Proof state before:
n✝ : ℕ
A a✝ b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℕ → ℝ
n : ℕ
this : ∑ x ∈ Finset.range n, a (x + 1) = a n - a 0 + ∑ x ∈ Finset.range n, a x
⊢ ∑ i ∈ Finset.range n, a (i + 1) = ∑ i ∈ Finset.range (n + 1), a i - a 0
Tactic:
rw [Finset.sum_range_succ, this]
Proof state after:
n✝ : ℕ
A a✝ b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℕ → ℝ
n : ℕ
this : ∑ x ∈ Finset.range n, a (x + 1) = a n - a 0 + ∑ x ∈ Finset.range n, a x
⊢ a n - a 0 + ∑ x ∈ Finset.range n, a x = ∑ x ∈ Finset.range n, a x + a n - a 0
Theorem: sum_range_succ
Proof state before:
n✝ : ℕ
A a✝ b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℕ → ℝ
n : ℕ
this : ∑ x ∈ Finset.range n, a (x + 1) = a n - a 0 + ∑ x ∈ Finset.range n, a x
⊢ a n - a 0 + ∑ x ∈ Finset.range n, a x = ∑ x ∈ Finset.range n, a x + a n - a 0
Tactic:
ring
Proof state after:
no goals
Theorem: cancel_aux'
Proof state before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hg : 0 ≤ g
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n : ℕ
⊢ ∑ i ∈ Finset.range n, f i * g i ≤
    C * ↑n * g (n - 1) + C * cumsum g (n - 1 - 1 + 1) - C * (↑(n - 1 - 1) + 1) * g (n - 1)
Tactic:
have := cancel_aux hf hg hf' hg' n
Proof state after:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hg : 0 ≤ g
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n : ℕ
this :
  ∑ i ∈ Finset.range n, f i * g i ≤
    g (n - 1) * (C * ↑n) +
      (C * (↑(n - 1 - 1) + 1) * g 0 - C * (↑(n - 1 - 1) + 1) * g (n - 1) -
        ((n - 1 - 1) • (C * g 0) - ∑ x ∈ Finset.range (n - 1 - 1), C * g (x + 1)))
⊢ ∑ i ∈ Finset.range n, f i * g i ≤
    C * ↑n * g (n - 1) + C * cumsum g (n - 1 - 1 + 1) - C * (↑(n - 1 - 1) + 1) * g (n - 1)
Theorem: cancel_aux'
Proof state before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hg : 0 ≤ g
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n : ℕ
this :
  ∑ i ∈ Finset.range n, f i * g i ≤
    g (n - 1) * (C * ↑n) +
      (C * (↑(n - 1 - 1) + 1) * g 0 - C * (↑(n - 1 - 1) + 1) * g (n - 1) -
        ((n - 1 - 1) • (C * g 0) - ∑ x ∈ Finset.range (n - 1 - 1), C * g (x + 1)))
⊢ ∑ i ∈ Finset.range n, f i * g i ≤
    C * ↑n * g (n - 1) + C * cumsum g (n - 1 - 1 + 1) - C * (↑(n - 1 - 1) + 1) * g (n - 1)
Tactic:
simp [← Finset.mul_sum, sum_range_succ] at this
Proof state after:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hg : 0 ≤ g
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n : ℕ
this :
  ∑ i ∈ Finset.range n, f i * g i ≤
    g (n - 1) * (C * ↑n) +
      (C * (↑(n - 1 - 1) + 1) * g 0 - C * (↑(n - 1 - 1) + 1) * g (n - 1) -
        (↑(n - 1 - 1) * (C * g 0) - C * (∑ i ∈ Finset.range (n - 1 - 1 + 1), g i - g 0)))
⊢ ∑ i ∈ Finset.range n, f i * g i ≤
    C * ↑n * g (n - 1) + C * cumsum g (n - 1 - 1 + 1) - C * (↑(n - 1 - 1) + 1) * g (n - 1)
Theorem: cancel_aux'
Proof state before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hg : 0 ≤ g
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n : ℕ
this :
  ∑ i ∈ Finset.range n, f i * g i ≤
    g (n - 1) * (C * ↑n) +
      (C * (↑(n - 1 - 1) + 1) * g 0 - C * (↑(n - 1 - 1) + 1) * g (n - 1) -
        (↑(n - 1 - 1) * (C * g 0) - C * (∑ i ∈ Finset.range (n - 1 - 1 + 1), g i - g 0)))
⊢ ∑ i ∈ Finset.range n, f i * g i ≤
    C * ↑n * g (n - 1) + C * cumsum g (n - 1 - 1 + 1) - C * (↑(n - 1 - 1) + 1) * g (n - 1)
Tactic:
convert this using 1
Proof state after:
case h.e'_4
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hg : 0 ≤ g
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n : ℕ
this :
  ∑ i ∈ Finset.range n, f i * g i ≤
    g (n - 1) * (C * ↑n) +
      (C * (↑(n - 1 - 1) + 1) * g 0 - C * (↑(n - 1 - 1) + 1) * g (n - 1) -
        (↑(n - 1 - 1) * (C * g 0) - C * (∑ i ∈ Finset.range (n - 1 - 1 + 1), g i - g 0)))
⊢ C * ↑n * g (n - 1) + C * cumsum g (n - 1 - 1 + 1) - C * (↑(n - 1 - 1) + 1) * g (n - 1) =
    g (n - 1) * (C * ↑n) +
      (C * (↑(n - 1 - 1) + 1) * g 0 - C * (↑(n - 1 - 1) + 1) * g (n - 1) -
        (↑(n - 1 - 1) * (C * g 0) - C * (∑ i ∈ Finset.range (n - 1 - 1 + 1), g i - g 0)))
Theorem: cancel_aux'
Proof state before:
case h.e'_4
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hg : 0 ≤ g
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n : ℕ
this :
  ∑ i ∈ Finset.range n, f i * g i ≤
    g (n - 1) * (C * ↑n) +
      (C * (↑(n - 1 - 1) + 1) * g 0 - C * (↑(n - 1 - 1) + 1) * g (n - 1) -
        (↑(n - 1 - 1) * (C * g 0) - C * (∑ i ∈ Finset.range (n - 1 - 1 + 1), g i - g 0)))
⊢ C * ↑n * g (n - 1) + C * cumsum g (n - 1 - 1 + 1) - C * (↑(n - 1 - 1) + 1) * g (n - 1) =
    g (n - 1) * (C * ↑n) +
      (C * (↑(n - 1 - 1) + 1) * g 0 - C * (↑(n - 1 - 1) + 1) * g (n - 1) -
        (↑(n - 1 - 1) * (C * g 0) - C * (∑ i ∈ Finset.range (n - 1 - 1 + 1), g i - g 0)))
Tactic:
unfold cumsum
Proof state after:
case h.e'_4
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hg : 0 ≤ g
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n : ℕ
this :
  ∑ i ∈ Finset.range n, f i * g i ≤
    g (n - 1) * (C * ↑n) +
      (C * (↑(n - 1 - 1) + 1) * g 0 - C * (↑(n - 1 - 1) + 1) * g (n - 1) -
        (↑(n - 1 - 1) * (C * g 0) - C * (∑ i ∈ Finset.range (n - 1 - 1 + 1), g i - g 0)))
⊢ C * ↑n * g (n - 1) + C * ∑ i ∈ Finset.range (n - 1 - 1 + 1), g i - C * (↑(n - 1 - 1) + 1) * g (n - 1) =
    g (n - 1) * (C * ↑n) +
      (C * (↑(n - 1 - 1) + 1) * g 0 - C * (↑(n - 1 - 1) + 1) * g (n - 1) -
        (↑(n - 1 - 1) * (C * g 0) - C * (∑ i ∈ Finset.range (n - 1 - 1 + 1), g i - g 0)))
Theorem: cancel_aux'
Proof state before:
case h.e'_4
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hg : 0 ≤ g
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n : ℕ
this :
  ∑ i ∈ Finset.range n, f i * g i ≤
    g (n - 1) * (C * ↑n) +
      (C * (↑(n - 1 - 1) + 1) * g 0 - C * (↑(n - 1 - 1) + 1) * g (n - 1) -
        (↑(n - 1 - 1) * (C * g 0) - C * (∑ i ∈ Finset.range (n - 1 - 1 + 1), g i - g 0)))
⊢ C * ↑n * g (n - 1) + C * ∑ i ∈ Finset.range (n - 1 - 1 + 1), g i - C * (↑(n - 1 - 1) + 1) * g (n - 1) =
    g (n - 1) * (C * ↑n) +
      (C * (↑(n - 1 - 1) + 1) * g 0 - C * (↑(n - 1 - 1) + 1) * g (n - 1) -
        (↑(n - 1 - 1) * (C * g 0) - C * (∑ i ∈ Finset.range (n - 1 - 1 + 1), g i - g 0)))
Tactic:
ring
Proof state after:
no goals
Theorem: cancel_main
Proof state before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hg : 0 ≤ g
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n : ℕ
hn : 2 ≤ n
⊢ cumsum (f * g) n ≤ C * cumsum g n
Tactic:
convert cancel_aux' hf hg hf' hg' n using 1
Proof state after:
case h.e'_4
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hg : 0 ≤ g
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n : ℕ
hn : 2 ≤ n
⊢ C * cumsum g n = C * ↑n * g (n - 1) + C * cumsum g (n - 1 - 1 + 1) - C * (↑(n - 1 - 1) + 1) * g (n - 1)
Theorem: cancel_main
Proof state before:
case h.e'_4
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hg : 0 ≤ g
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n : ℕ
hn : 2 ≤ n
⊢ C * cumsum g n = C * ↑n * g (n - 1) + C * cumsum g (n - 1 - 1 + 1) - C * (↑(n - 1 - 1) + 1) * g (n - 1)
Tactic:
match n with
| n + 2 => simp [cumsum_succ] ; ring
Proof state after:
no goals
Theorem: cancel_main
Proof state before:
n✝¹ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hg : 0 ≤ g
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n✝ n : ℕ
hn : 2 ≤ n + 2
⊢ C * cumsum g (n + 2) =
    C * ↑(n + 2) * g (n + 2 - 1) + C * cumsum g (n + 2 - 1 - 1 + 1) - C * (↑(n + 2 - 1 - 1) + 1) * g (n + 2 - 1)
Tactic:
simp [cumsum_succ]
Proof state after:
n✝¹ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hg : 0 ≤ g
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n✝ n : ℕ
hn : 2 ≤ n + 2
⊢ C * (cumsum g n + g n + g (n + 1)) = C * (↑n + 2) * g (n + 1) + C * (cumsum g n + g n) - C * (↑n + 1) * g (n + 1)
Theorem: cancel_main
Proof state before:
n✝¹ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hg : 0 ≤ g
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n✝ n : ℕ
hn : 2 ≤ n + 2
⊢ C * (cumsum g n + g n + g (n + 1)) = C * (↑n + 2) * g (n + 1) + C * (cumsum g n + g n) - C * (↑n + 1) * g (n + 1)
Tactic:
ring
Proof state after:
no goals
Theorem: cancel_main'
Proof state before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hf0 : f 0 = 0
hg : 0 ≤ g
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n : ℕ
⊢ cumsum (f * g) n ≤ C * cumsum g n
Tactic:
match n with
| 0 => simp [cumsum]
| 1 => specialize hg 0 ; specialize hf' 1 ; simp [cumsum, hf0] at hf' hg ⊢ ; positivity
| n + 2 => convert cancel_aux' hf hg hf' hg' (n + 2) using 1 ; simp [cumsum_succ] ; ring
Proof state after:
no goals
Theorem: cancel_main'
Proof state before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hf0 : f 0 = 0
hg : 0 ≤ g
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n : ℕ
⊢ cumsum (f * g) 0 ≤ C * cumsum g 0
Tactic:
simp [cumsum]
Proof state after:
no goals
Theorem: cancel_main'
Proof state before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hf0 : f 0 = 0
hg : 0 ≤ g
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n : ℕ
⊢ cumsum (f * g) 1 ≤ C * cumsum g 1
Tactic:
specialize hg 0
Proof state after:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hf0 : f 0 = 0
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n : ℕ
hg : 0 0 ≤ g 0
⊢ cumsum (f * g) 1 ≤ C * cumsum g 1
Theorem: cancel_main'
Proof state before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hf0 : f 0 = 0
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n : ℕ
hg : 0 0 ≤ g 0
⊢ cumsum (f * g) 1 ≤ C * cumsum g 1
Tactic:
specialize hf' 1
Proof state after:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hf0 : f 0 = 0
hg' : Antitone g
n : ℕ
hg : 0 0 ≤ g 0
hf' : cumsum f 1 ≤ C * ↑1
⊢ cumsum (f * g) 1 ≤ C * cumsum g 1
Theorem: cancel_main'
Proof state before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hf0 : f 0 = 0
hg' : Antitone g
n : ℕ
hg : 0 0 ≤ g 0
hf' : cumsum f 1 ≤ C * ↑1
⊢ cumsum (f * g) 1 ≤ C * cumsum g 1
Tactic:
simp [cumsum, hf0] at hf' hg ⊢
Proof state after:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hf0 : f 0 = 0
hg' : Antitone g
n : ℕ
hg : 0 ≤ g 0
hf' : 0 ≤ C
⊢ 0 ≤ C * g 0
Theorem: cancel_main'
Proof state before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hf0 : f 0 = 0
hg' : Antitone g
n : ℕ
hg : 0 ≤ g 0
hf' : 0 ≤ C
⊢ 0 ≤ C * g 0
Tactic:
positivity
Proof state after:
no goals
Theorem: cancel_main'
Proof state before:
n✝¹ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hf0 : f 0 = 0
hg : 0 ≤ g
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n✝ n : ℕ
⊢ cumsum (f * g) (n + 2) ≤ C * cumsum g (n + 2)
Tactic:
convert cancel_aux' hf hg hf' hg' (n + 2) using 1
Proof state after:
case h.e'_4
n✝¹ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hf0 : f 0 = 0
hg : 0 ≤ g
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n✝ n : ℕ
⊢ C * cumsum g (n + 2) =
    C * ↑(n + 2) * g (n + 2 - 1) + C * cumsum g (n + 2 - 1 - 1 + 1) - C * (↑(n + 2 - 1 - 1) + 1) * g (n + 2 - 1)
Theorem: cancel_main'
Proof state before:
case h.e'_4
n✝¹ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hf0 : f 0 = 0
hg : 0 ≤ g
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n✝ n : ℕ
⊢ C * cumsum g (n + 2) =
    C * ↑(n + 2) * g (n + 2 - 1) + C * cumsum g (n + 2 - 1 - 1 + 1) - C * (↑(n + 2 - 1 - 1) + 1) * g (n + 2 - 1)
Tactic:
simp [cumsum_succ]
Proof state after:
case h.e'_4
n✝¹ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hf0 : f 0 = 0
hg : 0 ≤ g
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n✝ n : ℕ
⊢ C * (cumsum g n + g n + g (n + 1)) = C * (↑n + 2) * g (n + 1) + C * (cumsum g n + g n) - C * (↑n + 1) * g (n + 1)
Theorem: cancel_main'
Proof state before:
case h.e'_4
n✝¹ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hf0 : f 0 = 0
hg : 0 ≤ g
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n✝ n : ℕ
⊢ C * (cumsum g n + g n + g (n + 1)) = C * (↑n + 2) * g (n + 1) + C * (cumsum g n + g n) - C * (↑n + 1) * g (n + 1)
Tactic:
ring
Proof state after:
no goals
Theorem: sum_le_integral
Proof state before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hf : AntitoneOn f (Ioc x₀ (x₀ + ↑n))
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑n)) volume
⊢ ∑ i ∈ Finset.range n, f (x₀ + ↑(i + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + ↑n, f x
Tactic:
cases' n with n <;> simp [Nat.succ_eq_add_one] at hf ⊢
Proof state after:
case succ
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
⊢ ∑ x ∈ Finset.range (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + (↑n + 1), f x
Theorem: sum_le_integral
Proof state before:
case succ
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
⊢ ∑ x ∈ Finset.range (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + (↑n + 1), f x
Tactic:
have : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1) := by
  ext i ; by_cases hi : i = 0 <;> simp [hi] ; omega
Proof state after:
case succ
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
⊢ ∑ x ∈ Finset.range (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + (↑n + 1), f x
Theorem: sum_le_integral
Proof state before:
case succ
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
⊢ ∑ x ∈ Finset.range (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + (↑n + 1), f x
Tactic:
simp [this, Finset.sum_union]
Proof state after:
case succ
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
⊢ f (x₀ + 1) + ∑ x ∈ Finset.Ico 1 (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + (↑n + 1), f x
Theorem: sum_le_integral
Proof state before:
case succ
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
⊢ f (x₀ + 1) + ∑ x ∈ Finset.Ico 1 (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + (↑n + 1), f x
Tactic:
have l4 : IntervalIntegrable f volume x₀ (x₀ + 1) := by
  apply IntegrableOn.intervalIntegrable
  simp only [ge_iff_le, le_add_iff_nonneg_right, zero_le_one, uIcc_of_le]
  apply hfi.mono_set
  apply Icc_subset_Icc ; linarith ; simp
Proof state after:
case succ
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
l4 : IntervalIntegrable f volume x₀ (x₀ + 1)
⊢ f (x₀ + 1) + ∑ x ∈ Finset.Ico 1 (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + (↑n + 1), f x
Theorem: sum_le_integral
Proof state before:
case succ
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
l4 : IntervalIntegrable f volume x₀ (x₀ + 1)
⊢ f (x₀ + 1) + ∑ x ∈ Finset.Ico 1 (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + (↑n + 1), f x
Tactic:
have l5 x (hx : x ∈ Ioc x₀ (x₀ + 1)) : (fun x ↦ f (x₀ + 1)) x ≤ f x := by
  rcases hx with ⟨hx1, hx2⟩
  refine hf ⟨hx1, by linarith⟩ ⟨by linarith, by linarith⟩ hx2
Proof state after:
case succ
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
l4 : IntervalIntegrable f volume x₀ (x₀ + 1)
l5 : ∀ x ∈ Ioc x₀ (x₀ + 1), (fun x => f (x₀ + 1)) x ≤ f x
⊢ f (x₀ + 1) + ∑ x ∈ Finset.Ico 1 (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + (↑n + 1), f x
Theorem: sum_le_integral
Proof state before:
case succ
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
l4 : IntervalIntegrable f volume x₀ (x₀ + 1)
l5 : ∀ x ∈ Ioc x₀ (x₀ + 1), (fun x => f (x₀ + 1)) x ≤ f x
⊢ f (x₀ + 1) + ∑ x ∈ Finset.Ico 1 (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + (↑n + 1), f x
Tactic:
have l6 : ∫ x in x₀..x₀ + 1, f (x₀ + 1) = f (x₀ + 1) := by simp
Proof state after:
case succ
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
l4 : IntervalIntegrable f volume x₀ (x₀ + 1)
l5 : ∀ x ∈ Ioc x₀ (x₀ + 1), (fun x => f (x₀ + 1)) x ≤ f x
l6 : ∫ (x : ℝ) in x₀..x₀ + 1, f (x₀ + 1) = f (x₀ + 1)
⊢ f (x₀ + 1) + ∑ x ∈ Finset.Ico 1 (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + (↑n + 1), f x
Theorem: sum_le_integral
Proof state before:
case succ
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
l4 : IntervalIntegrable f volume x₀ (x₀ + 1)
l5 : ∀ x ∈ Ioc x₀ (x₀ + 1), (fun x => f (x₀ + 1)) x ≤ f x
l6 : ∫ (x : ℝ) in x₀..x₀ + 1, f (x₀ + 1) = f (x₀ + 1)
⊢ f (x₀ + 1) + ∑ x ∈ Finset.Ico 1 (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + (↑n + 1), f x
Tactic:
have l1 : f (x₀ + 1) ≤ ∫ x in x₀..x₀ + 1, f x := by
  rw [← l6] ; apply intervalIntegral.integral_mono_ae_restrict (by linarith) (by simp) l4
  apply eventually_of_mem _ l5
  have : (Ioc x₀ (x₀ + 1))ᶜ ∩ Icc x₀ (x₀ + 1) = {x₀} := by simp [← diff_eq_compl_inter]
  simp [ae, this]
Proof state after:
case succ
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
l4 : IntervalIntegrable f volume x₀ (x₀ + 1)
l5 : ∀ x ∈ Ioc x₀ (x₀ + 1), (fun x => f (x₀ + 1)) x ≤ f x
l6 : ∫ (x : ℝ) in x₀..x₀ + 1, f (x₀ + 1) = f (x₀ + 1)
l1 : f (x₀ + 1) ≤ ∫ (x : ℝ) in x₀..x₀ + 1, f x
⊢ f (x₀ + 1) + ∑ x ∈ Finset.Ico 1 (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + (↑n + 1), f x
Theorem: sum_le_integral
Proof state before:
case succ
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
l4 : IntervalIntegrable f volume x₀ (x₀ + 1)
l5 : ∀ x ∈ Ioc x₀ (x₀ + 1), (fun x => f (x₀ + 1)) x ≤ f x
l6 : ∫ (x : ℝ) in x₀..x₀ + 1, f (x₀ + 1) = f (x₀ + 1)
l1 : f (x₀ + 1) ≤ ∫ (x : ℝ) in x₀..x₀ + 1, f x
⊢ f (x₀ + 1) + ∑ x ∈ Finset.Ico 1 (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + (↑n + 1), f x
Tactic:
have l2 : AntitoneOn (fun x ↦ f (x₀ + x)) (Icc 1 ↑(n + 1)) := by
  intro u ⟨hu1, _⟩ v ⟨_, hv2⟩ huv ; push_cast at hv2
  refine hf ⟨?_, ?_⟩ ⟨?_, ?_⟩ ?_ <;> linarith
Proof state after:
case succ
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
l4 : IntervalIntegrable f volume x₀ (x₀ + 1)
l5 : ∀ x ∈ Ioc x₀ (x₀ + 1), (fun x => f (x₀ + 1)) x ≤ f x
l6 : ∫ (x : ℝ) in x₀..x₀ + 1, f (x₀ + 1) = f (x₀ + 1)
l1 : f (x₀ + 1) ≤ ∫ (x : ℝ) in x₀..x₀ + 1, f x
l2 : AntitoneOn (fun x => f (x₀ + x)) (Icc 1 ↑(n + 1))
⊢ f (x₀ + 1) + ∑ x ∈ Finset.Ico 1 (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + (↑n + 1), f x