internlm/Lean-Github huggingface dataset:
Theorem: norm_eq_duals_supr'
Proof state before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
s : ℝ
h : g (Complex.abs ((dualVector y) x)) ≤ s
gk' : LipschitzWith k fun x => g (Complex.abs ((dualVector y) x))
⊢ g ‖y‖ + ↑k * 1 * (e / 2 / ↑k) = g ‖y‖ + ↑k / ↑k * e / 2
Tactic:
ring
Proof state after:
no goals
Theorem: norm_eq_duals_supr'
Proof state before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
s : ℝ
h : g (Complex.abs ((dualVector y) x)) ≤ s
gk' : LipschitzWith k fun x => g (Complex.abs ((dualVector y) x))
⊢ g ‖y‖ + ↑k / ↑k * e / 2 ≤ g ‖y‖ + 1 * e / 2
Tactic:
bound
Proof state after:
no goals
Theorem: norm_eq_duals_supr'
Proof state before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
s : ℝ
h : g (Complex.abs ((dualVector y) x)) ≤ s
gk' : LipschitzWith k fun x => g (Complex.abs ((dualVector y) x))
⊢ g ‖y‖ + 1 * e / 2 = g ‖y‖ + e / 2
Tactic:
simp only [one_mul]
Proof state after:
no goals
Theorem: norm_eq_duals_supr'
Proof state before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
s : ℝ
h : g (Complex.abs ((dualVector y) x)) ≤ s
gk' : LipschitzWith k fun x => g (Complex.abs ((dualVector y) x))
⊢ g ‖y‖ + e / 2 = g (Complex.abs ((dualVector y) y)) + e / 2
Tactic:
simp only [dualVector_apply, Complex.abs_ofReal, abs_norm]
Proof state after:
no goals
Theorem: norm_eq_duals_supr'
Proof state before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
s : ℝ
h : g (Complex.abs ((dualVector y) x)) ≤ s
gk' : LipschitzWith k fun x => g (Complex.abs ((dualVector y) x))
⊢ g (Complex.abs ((dualVector y) y)) + e / 2 ≤ g (Complex.abs ((dualVector y) x)) + ↑k * dist y x + e / 2
Tactic:
bound [gk'.le]
Proof state after:
no goals
Theorem: norm_eq_duals_supr'
Proof state before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
s : ℝ
h : g (Complex.abs ((dualVector y) x)) ≤ s
gk' : LipschitzWith k fun x => g (Complex.abs ((dualVector y) x))
⊢ g (Complex.abs ((dualVector y) x)) + ↑k * dist y x + e / 2 ≤ s + ↑k * dist y x + e / 2
Tactic:
linarith
Proof state after:
no goals
Theorem: norm_eq_duals_supr'
Proof state before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
s : ℝ
h : g (Complex.abs ((dualVector y) x)) ≤ s
gk' : LipschitzWith k fun x => g (Complex.abs ((dualVector y) x))
⊢ s + ↑k * dist y x + e / 2 = s + ↑k * dist x y + e / 2
Tactic:
rw [dist_comm]
Proof state after:
no goals
Theorem: norm_eq_duals_supr'
Proof state before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
s : ℝ
h : g (Complex.abs ((dualVector y) x)) ≤ s
gk' : LipschitzWith k fun x => g (Complex.abs ((dualVector y) x))
⊢ s + ↑k * dist x y + e / 2 ≤ s + ↑k * (e / 2 / ↑k) + e / 2
Tactic:
bound
Proof state after:
no goals
Theorem: norm_eq_duals_supr'
Proof state before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
s : ℝ
h : g (Complex.abs ((dualVector y) x)) ≤ s
gk' : LipschitzWith k fun x => g (Complex.abs ((dualVector y) x))
⊢ s + ↑k * (e / 2 / ↑k) + e / 2 = s + ↑k / ↑k * e / 2 + e / 2
Tactic:
ring_nf
Proof state after:
no goals
Theorem: norm_eq_duals_supr'
Proof state before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
s : ℝ
h : g (Complex.abs ((dualVector y) x)) ≤ s
gk' : LipschitzWith k fun x => g (Complex.abs ((dualVector y) x))
⊢ s + ↑k / ↑k * e / 2 + e / 2 ≤ s + 1 * e / 2 + e / 2
Tactic:
bound
Proof state after:
no goals
Theorem: norm_eq_duals_supr'
Proof state before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
s : ℝ
h : g (Complex.abs ((dualVector y) x)) ≤ s
gk' : LipschitzWith k fun x => g (Complex.abs ((dualVector y) x))
⊢ s + 1 * e / 2 + e / 2 = s + e
Tactic:
ring_nf
Proof state after:
no goals
Theorem: norm_eq_duals_supr'
Proof state before:
case neg.a
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
⊢ ⨆ n, g ‖(duals n) x‖ ≤ g ‖x‖
Tactic:
apply ciSup_le
Proof state after:
case neg.a.H
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
⊢ ∀ (x_1 : ℕ), g ‖(duals x_1) x‖ ≤ g ‖x‖
Theorem: norm_eq_duals_supr'
Proof state before:
case neg.a.H
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
⊢ ∀ (x_1 : ℕ), g ‖(duals x_1) x‖ ≤ g ‖x‖
Tactic:
intro n
Proof state after:
case neg.a.H
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
n : ℕ
⊢ g ‖(duals n) x‖ ≤ g ‖x‖
Theorem: norm_eq_duals_supr'
Proof state before:
case neg.a.H
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
n : ℕ
⊢ g ‖(duals n) x‖ ≤ g ‖x‖
Tactic:
apply gm
Proof state after:
case neg.a.H.a
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
n : ℕ
⊢ ‖(duals n) x‖ ≤ ‖x‖
Theorem: norm_eq_duals_supr'
Proof state before:
case neg.a.H.a
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
n : ℕ
⊢ ‖(duals n) x‖ ≤ ‖x‖
Tactic:
simp only [Complex.norm_eq_abs]
Proof state after:
case neg.a.H.a
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
n : ℕ
⊢ Complex.abs ((duals n) x) ≤ ‖x‖
Theorem: norm_eq_duals_supr'
Proof state before:
case neg.a.H.a
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
n : ℕ
⊢ Complex.abs ((duals n) x) ≤ ‖x‖
Tactic:
apply dualVector_le
Proof state after:
no goals
Theorem: norm_eq_duals_iSup
Proof state before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
x : E
⊢ ‖x‖ = ⨆ n, ‖(duals n) x‖
Tactic:
have h := norm_eq_duals_supr' (@monotone_id ℝ _) LipschitzWith.id x
Proof state after:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
x : E
h : id ‖x‖ = ⨆ n, id ‖(duals n) x‖
⊢ ‖x‖ = ⨆ n, ‖(duals n) x‖
Theorem: norm_eq_duals_iSup
Proof state before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
x : E
h : id ‖x‖ = ⨆ n, id ‖(duals n) x‖
⊢ ‖x‖ = ⨆ n, ‖(duals n) x‖
Tactic:
simpa only [Complex.norm_eq_abs] using h
Proof state after:
no goals
Theorem: Csupr.has_lim
Proof state before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
⊢ Filter.Tendsto (fun n => (partialSups s) n) atTop (𝓝 (⨆ n, s n))
Tactic:
rw [Metric.tendsto_atTop]
Proof state after:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
⊢ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist ((partialSups s) n) (⨆ n, s n) < ε
Theorem: Csupr.has_lim
Proof state before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
⊢ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist ((partialSups s) n) (⨆ n, s n) < ε
Tactic:
intro e ep
Proof state after:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
⊢ ∃ N, ∀ n ≥ N, dist ((partialSups s) n) (⨆ n, s n) < e
Theorem: Csupr.has_lim
Proof state before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
⊢ ∃ N, ∀ n ≥ N, dist ((partialSups s) n) (⨆ n, s n) < e
Tactic:
generalize hb : (⨆ n, s n) - e = b
Proof state after:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
⊢ ∃ N, ∀ n ≥ N, dist ((partialSups s) n) (⨆ n, s n) < e
Theorem: Csupr.has_lim
Proof state before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
⊢ ∃ N, ∀ n ≥ N, dist ((partialSups s) n) (⨆ n, s n) < e
Tactic:
have bs : b < ⨆ n, s n := by rw [← hb]; exact sub_lt_self _ (by linarith)
Proof state after:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
⊢ ∃ N, ∀ n ≥ N, dist ((partialSups s) n) (⨆ n, s n) < e
Theorem: Csupr.has_lim
Proof state before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
⊢ ∃ N, ∀ n ≥ N, dist ((partialSups s) n) (⨆ n, s n) < e
Tactic:
rcases exists_lt_of_lt_ciSup bs with ⟨N, sN⟩
Proof state after:
case intro
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N : ℕ
sN : b < s N
⊢ ∃ N, ∀ n ≥ N, dist ((partialSups s) n) (⨆ n, s n) < e
Theorem: Csupr.has_lim
Proof state before:
case intro
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N : ℕ
sN : b < s N
⊢ ∃ N, ∀ n ≥ N, dist ((partialSups s) n) (⨆ n, s n) < e
Tactic:
use N
Proof state after:
case h
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N : ℕ
sN : b < s N
⊢ ∀ n ≥ N, dist ((partialSups s) n) (⨆ n, s n) < e
Theorem: Csupr.has_lim
Proof state before:
case h
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N : ℕ
sN : b < s N
⊢ ∀ n ≥ N, dist ((partialSups s) n) (⨆ n, s n) < e
Tactic:
intro n nN
Proof state after:
case h
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N : ℕ
sN : b < s N
n : ℕ
nN : n ≥ N
⊢ dist ((partialSups s) n) (⨆ n, s n) < e
Theorem: Csupr.has_lim
Proof state before:
case h
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N : ℕ
sN : b < s N
n : ℕ
nN : n ≥ N
⊢ dist ((partialSups s) n) (⨆ n, s n) < e
Tactic:
rw [Real.dist_eq]
Proof state after:
case h
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N : ℕ
sN : b < s N
n : ℕ
nN : n ≥ N
⊢ |(partialSups s) n - ⨆ n, s n| < e
Theorem: Csupr.has_lim
Proof state before:
case h
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N : ℕ
sN : b < s N
n : ℕ
nN : n ≥ N
⊢ |(partialSups s) n - ⨆ n, s n| < e
Tactic:
rw [abs_lt]
Proof state after:
case h
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N : ℕ
sN : b < s N
n : ℕ
nN : n ≥ N
⊢ -e < (partialSups s) n - ⨆ n, s n ∧ (partialSups s) n - ⨆ n, s n < e
Theorem: Csupr.has_lim
Proof state before:
case h
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N : ℕ
sN : b < s N
n : ℕ
nN : n ≥ N
⊢ -e < (partialSups s) n - ⨆ n, s n ∧ (partialSups s) n - ⨆ n, s n < e
Tactic:
constructor
Proof state after:
case h.left
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N : ℕ
sN : b < s N
n : ℕ
nN : n ≥ N
⊢ -e < (partialSups s) n - ⨆ n, s n

case h.right
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N : ℕ
sN : b < s N
n : ℕ
nN : n ≥ N
⊢ (partialSups s) n - ⨆ n, s n < e
Theorem: Csupr.has_lim
Proof state before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
⊢ b < ⨆ n, s n
Tactic:
rw [← hb]
Proof state after:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
⊢ (⨆ n, s n) - e < ⨆ n, s n
Theorem: Csupr.has_lim
Proof state before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
⊢ (⨆ n, s n) - e < ⨆ n, s n
Tactic:
exact sub_lt_self _ (by linarith)
Proof state after:
no goals
Theorem: Csupr.has_lim
Proof state before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
⊢ 0 < e
Tactic:
linarith
Proof state after:
no goals
Theorem: Csupr.has_lim
Proof state before:
case h.left
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N : ℕ
sN : b < s N
n : ℕ
nN : n ≥ N
⊢ -e < (partialSups s) n - ⨆ n, s n
Tactic:
simp only [neg_lt_sub_iff_lt_add]
Proof state after:
case h.left
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N : ℕ
sN : b < s N
n : ℕ
nN : n ≥ N
⊢ ⨆ n, s n < e + (partialSups s) n
Theorem: Csupr.has_lim
Proof state before:
case h.left
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N : ℕ
sN : b < s N
n : ℕ
nN : n ≥ N
⊢ ⨆ n, s n < e + (partialSups s) n
Tactic:
simp only [←hb] at sN
Proof state after:
case h.left
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N n : ℕ
nN : n ≥ N
sN : (⨆ n, s n) - e < s N
⊢ ⨆ n, s n < e + (partialSups s) n
Theorem: Csupr.has_lim
Proof state before:
case h.left
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N n : ℕ
nN : n ≥ N
sN : (⨆ n, s n) - e < s N
⊢ ⨆ n, s n < e + (partialSups s) n
Tactic:
calc iSup s
  _ = iSup s - e + e := by ring
  _ < s N + e := by linarith
  _ ≤ partialSups s n + e := by linarith [le_partialSups_of_le s nN]
  _ = e + partialSups s n := by ring
Proof state after:
no goals
Theorem: Csupr.has_lim
Proof state before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N n : ℕ
nN : n ≥ N
sN : (⨆ n, s n) - e < s N
⊢ iSup s = iSup s - e + e
Tactic:
ring
Proof state after:
no goals
Theorem: Csupr.has_lim
Proof state before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N n : ℕ
nN : n ≥ N
sN : (⨆ n, s n) - e < s N
⊢ iSup s - e + e < s N + e
Tactic:
linarith
Proof state after:
no goals
Theorem: Csupr.has_lim
Proof state before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N n : ℕ
nN : n ≥ N
sN : (⨆ n, s n) - e < s N
⊢ s N + e ≤ (partialSups s) n + e
Tactic:
linarith [le_partialSups_of_le s nN]
Proof state after:
no goals
Theorem: Csupr.has_lim
Proof state before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N n : ℕ
nN : n ≥ N
sN : (⨆ n, s n) - e < s N
⊢ (partialSups s) n + e = e + (partialSups s) n
Tactic:
ring
Proof state after:
no goals
Theorem: Csupr.has_lim
Proof state before:
case h.right
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N : ℕ
sN : b < s N
n : ℕ
nN : n ≥ N
⊢ (partialSups s) n - ⨆ n, s n < e
Tactic:
have rs : partialSups s n ≤ iSup s := partialSups_le _ _ _ fun a _ ↦ le_ciSup ba a
Proof state after:
case h.right
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N : ℕ
sN : b < s N
n : ℕ
nN : n ≥ N
rs : (partialSups s) n ≤ iSup s
⊢ (partialSups s) n - ⨆ n, s n < e
Theorem: Csupr.has_lim
Proof state before:
case h.right
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N : ℕ
sN : b < s N
n : ℕ
nN : n ≥ N
rs : (partialSups s) n ≤ iSup s
⊢ (partialSups s) n - ⨆ n, s n < e
Tactic:
calc partialSups s n - iSup s
  _ ≤ iSup s - iSup s := by linarith
  _ = 0 := by ring
  _ < e := ep
Proof state after:
no goals
Theorem: Csupr.has_lim
Proof state before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N : ℕ
sN : b < s N
n : ℕ
nN : n ≥ N
rs : (partialSups s) n ≤ iSup s
⊢ (partialSups s) n - iSup s ≤ iSup s - iSup s
Tactic:
linarith
Proof state after:
no goals
Theorem: Csupr.has_lim
Proof state before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N : ℕ
sN : b < s N
n : ℕ
nN : n ≥ N
rs : (partialSups s) n ≤ iSup s
⊢ iSup s - iSup s = 0
Tactic:
ring
Proof state after:
no goals