internlm/Lean-Github huggingface dataset:
Theorem: LipschitzWith.le
Proof state before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
f : G → ℝ
k : ℝ≥0
fk : LipschitzWith k f
x y : G
⊢ f x = f y + (f x - f y)
Tactic:
ring_nf
Proof state after:
no goals
Theorem: LipschitzWith.le
Proof state before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
f : G → ℝ
k : ℝ≥0
fk : LipschitzWith k f
x y : G
⊢ f y + (f x - f y) ≤ f y + |f x - f y|
Tactic:
bound
Proof state after:
no goals
Theorem: LipschitzWith.le
Proof state before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
f : G → ℝ
k : ℝ≥0
fk : LipschitzWith k f
x y : G
⊢ f y + |f x - f y| = f y + dist (f x) (f y)
Tactic:
rw [Real.dist_eq]
Proof state after:
no goals
Theorem: LipschitzWith.le
Proof state before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
f : G → ℝ
k : ℝ≥0
fk : LipschitzWith k f
x y : G
⊢ f y + dist (f x) (f y) ≤ f y + ↑k * dist x y
Tactic:
linarith [fk.dist_le_mul x y]
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
⊢ g ‖x‖ = ⨆ n, g ‖(duals n) x‖
Tactic:
by_cases k0 : k = 0
Proof state after:
case pos
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
⊢ g ‖x‖ = ⨆ n, g ‖(duals n) x‖

case neg
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
⊢ g ‖x‖ = ⨆ n, g ‖(duals n) x‖
Theorem: norm_eq_duals_supr'
Proof state before:
case neg
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
⊢ g ‖x‖ = ⨆ n, g ‖(duals n) x‖
Tactic:
have kp : 0 < (k : ℝ) := by simp only [NNReal.coe_pos]; exact Ne.bot_lt k0
Proof state after:
case neg
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
⊢ g ‖x‖ = ⨆ n, g ‖(duals n) x‖
Theorem: norm_eq_duals_supr'
Proof state before:
case neg
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
⊢ g ‖x‖ = ⨆ n, g ‖(duals n) x‖
Tactic:
apply le_antisymm
Proof state after:
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
⊢ g ‖x‖ ≤ ⨆ n, g ‖(duals n) x‖

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‖
Theorem: norm_eq_duals_supr'
Proof state before:
case pos
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
⊢ g ‖x‖ = ⨆ n, g ‖(duals n) x‖
Tactic:
rw [k0] at gk
Proof state after:
case pos
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith 0 g
x : E
k0 : k = 0
⊢ g ‖x‖ = ⨆ n, g ‖(duals n) x‖
Theorem: norm_eq_duals_supr'
Proof state before:
case pos
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith 0 g
x : E
k0 : k = 0
⊢ g ‖x‖ = ⨆ n, g ‖(duals n) x‖
Tactic:
have g0 := gk.is_const 0
Proof state after:
case pos
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith 0 g
x : E
k0 : k = 0
g0 : ∀ (y : ℝ), g 0 = g y
⊢ g ‖x‖ = ⨆ n, g ‖(duals n) x‖
Theorem: norm_eq_duals_supr'
Proof state before:
case pos
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith 0 g
x : E
k0 : k = 0
g0 : ∀ (y : ℝ), g 0 = g y
⊢ g ‖x‖ = ⨆ n, g ‖(duals n) x‖
Tactic:
simp only [← g0 _, ciSup_const]
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
⊢ 0 < ↑k
Tactic:
simp only [NNReal.coe_pos]
Proof state after:
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
⊢ 0 < k
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
⊢ 0 < k
Tactic:
exact Ne.bot_lt k0
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
⊢ g ‖x‖ ≤ ⨆ n, g ‖(duals n) x‖
Tactic:
apply le_of_forall_pos_le_add
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
⊢ ∀ (ε : ℝ), 0 < ε → g ‖x‖ ≤ (⨆ n, g ‖(duals n) 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
⊢ ∀ (ε : ℝ), 0 < ε → g ‖x‖ ≤ (⨆ n, g ‖(duals n) x‖) + ε
Tactic:
intro e ep
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
e : ℝ
ep : 0 < e
⊢ g ‖x‖ ≤ (⨆ n, g ‖(duals n) x‖) + e
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
e : ℝ
ep : 0 < e
⊢ g ‖x‖ ≤ (⨆ n, g ‖(duals n) x‖) + e
Tactic:
rcases Metric.denseRange_iff.mp (TopologicalSpace.denseRange_denseSeq E)
  x (e / 2 / k) (by bound) with ⟨n, nx⟩
Proof state after:
case neg.a.h.intro
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 : ℕ
nx : dist x (TopologicalSpace.denseSeq E n) < e / 2 / ↑k
⊢ g ‖x‖ ≤ (⨆ n, g ‖(duals n) x‖) + e
Theorem: norm_eq_duals_supr'
Proof state before:
case neg.a.h.intro
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 : ℕ
nx : dist x (TopologicalSpace.denseSeq E n) < e / 2 / ↑k
⊢ g ‖x‖ ≤ (⨆ n, g ‖(duals n) x‖) + e
Tactic:
generalize hy : TopologicalSpace.denseSeq E n = y
Proof state after:
case neg.a.h.intro
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 : ℕ
nx : dist x (TopologicalSpace.denseSeq E n) < e / 2 / ↑k
y : E
hy : TopologicalSpace.denseSeq E n = y
⊢ g ‖x‖ ≤ (⨆ n, g ‖(duals n) x‖) + e
Theorem: norm_eq_duals_supr'
Proof state before:
case neg.a.h.intro
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 : ℕ
nx : dist x (TopologicalSpace.denseSeq E n) < e / 2 / ↑k
y : E
hy : TopologicalSpace.denseSeq E n = y
⊢ g ‖x‖ ≤ (⨆ n, g ‖(duals n) x‖) + e
Tactic:
rw [hy] at nx
Proof state after:
case neg.a.h.intro
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
hy : TopologicalSpace.denseSeq E n = y
⊢ g ‖x‖ ≤ (⨆ n, g ‖(duals n) x‖) + e
Theorem: norm_eq_duals_supr'
Proof state before:
case neg.a.h.intro
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
hy : TopologicalSpace.denseSeq E n = y
⊢ g ‖x‖ ≤ (⨆ n, g ‖(duals n) x‖) + e
Tactic:
have hn : duals n = dualVector y := by rw [← hy, duals]
Proof state after:
case neg.a.h.intro
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
hy : TopologicalSpace.denseSeq E n = y
hn : duals n = dualVector y
⊢ g ‖x‖ ≤ (⨆ n, g ‖(duals n) x‖) + e
Theorem: norm_eq_duals_supr'
Proof state before:
case neg.a.h.intro
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
hy : TopologicalSpace.denseSeq E n = y
hn : duals n = dualVector y
⊢ g ‖x‖ ≤ (⨆ n, g ‖(duals n) x‖) + e
Tactic:
have h := le_ciSup (duals_bddAbove gm x) n
Proof state after:
case neg.a.h.intro
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
hy : TopologicalSpace.denseSeq E n = y
hn : duals n = dualVector y
h : g ‖(duals n) x‖ ≤ ⨆ n, g ‖(duals n) x‖
⊢ g ‖x‖ ≤ (⨆ n, g ‖(duals n) x‖) + e
Theorem: norm_eq_duals_supr'
Proof state before:
case neg.a.h.intro
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
hy : TopologicalSpace.denseSeq E n = y
hn : duals n = dualVector y
h : g ‖(duals n) x‖ ≤ ⨆ n, g ‖(duals n) x‖
⊢ g ‖x‖ ≤ (⨆ n, g ‖(duals n) x‖) + e
Tactic:
generalize hs : ⨆ n, g ‖duals n x‖ = s
Proof state after:
case neg.a.h.intro
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
hy : TopologicalSpace.denseSeq E n = y
hn : duals n = dualVector y
h : g ‖(duals n) x‖ ≤ ⨆ n, g ‖(duals n) x‖
s : ℝ
hs : ⨆ n, g ‖(duals n) x‖ = s
⊢ g ‖x‖ ≤ s + e
Theorem: norm_eq_duals_supr'
Proof state before:
case neg.a.h.intro
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
hy : TopologicalSpace.denseSeq E n = y
hn : duals n = dualVector y
h : g ‖(duals n) x‖ ≤ ⨆ n, g ‖(duals n) x‖
s : ℝ
hs : ⨆ n, g ‖(duals n) x‖ = s
⊢ g ‖x‖ ≤ s + e
Tactic:
simp_rw [hs, hn] at h
Proof state after:
case neg.a.h.intro
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
hy : TopologicalSpace.denseSeq E n = y
hn : duals n = dualVector y
s : ℝ
hs : ⨆ n, g ‖(duals n) x‖ = s
h : g ‖(dualVector y) x‖ ≤ s
⊢ g ‖x‖ ≤ s + e
Theorem: norm_eq_duals_supr'
Proof state before:
case neg.a.h.intro
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
hy : TopologicalSpace.denseSeq E n = y
hn : duals n = dualVector y
s : ℝ
hs : ⨆ n, g ‖(duals n) x‖ = s
h : g ‖(dualVector y) x‖ ≤ s
⊢ g ‖x‖ ≤ s + e
Tactic:
clear hs hn hy
Proof state after:
case neg.a.h.intro
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 ‖(dualVector y) x‖ ≤ s
⊢ g ‖x‖ ≤ s + e
Theorem: norm_eq_duals_supr'
Proof state before:
case neg.a.h.intro
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 ‖(dualVector y) x‖ ≤ s
⊢ g ‖x‖ ≤ s + e
Tactic:
simp only [Complex.norm_eq_abs] at h
Proof state after:
case neg.a.h.intro
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
⊢ g ‖x‖ ≤ s + e
Theorem: norm_eq_duals_supr'
Proof state before:
case neg.a.h.intro
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
⊢ g ‖x‖ ≤ s + e
Tactic:
have gk' : LipschitzWith k fun x ↦ g (abs (dualVector y x)) := by
  have k11 : (k : ℝ≥0) = k * 1 * 1 := by norm_num
  rw [k11]
  simp_rw [←Complex.norm_eq_abs]; apply (gk.comp lipschitzWith_one_norm).comp
  exact (dualVector y).lipschitz.weaken (dualVector_nnnorm y)
Proof state after:
case neg.a.h.intro
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 ‖x‖ ≤ s + e
Theorem: norm_eq_duals_supr'
Proof state before:
case neg.a.h.intro
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 ‖x‖ ≤ s + e
Tactic:
calc g ‖x‖
  _ ≤ g ‖y‖ + k * 1 * dist x y := (gk.comp lipschitzWith_one_norm).le x y
  _ ≤ g ‖y‖ + k * 1 * (e / 2 / k) := by bound
  _ = g ‖y‖ + k / k * e / 2 := by ring
  _ ≤ g ‖y‖ + 1 * e / 2 := by bound
  _ = g ‖y‖ + e / 2 := by simp only [one_mul]
  _ = g (abs (dualVector y y)) + e / 2 := by
    simp only [dualVector_apply, Complex.abs_ofReal, abs_norm]
  _ ≤ g (abs (dualVector y x)) + k * dist y x + e / 2 := by bound [gk'.le]
  _ ≤ s + k * dist y x + e / 2 := by linarith
  _ = s + k * dist x y + e / 2 := by rw [dist_comm]
  _ ≤ s + k * (e / 2 / k) + e / 2 := by bound
  _ = s + k / k * e / 2 + e / 2 := by ring_nf
  _ ≤ s + 1 * e / 2 + e / 2 := by bound
  _ = s + e := by 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
⊢ e / 2 / ↑k > 0
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
hy : TopologicalSpace.denseSeq E n = y
⊢ duals n = dualVector y
Tactic:
rw [← hy, duals]
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
⊢ LipschitzWith k fun x => g (Complex.abs ((dualVector y) x))
Tactic:
have k11 : (k : ℝ≥0) = k * 1 * 1 := by norm_num
Proof state after:
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
k11 : k = k * 1 * 1
⊢ LipschitzWith k fun x => g (Complex.abs ((dualVector y) x))
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
k11 : k = k * 1 * 1
⊢ LipschitzWith k fun x => g (Complex.abs ((dualVector y) x))
Tactic:
rw [k11]
Proof state after:
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
k11 : k = k * 1 * 1
⊢ LipschitzWith (k * 1 * 1) fun x => g (Complex.abs ((dualVector y) x))
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
k11 : k = k * 1 * 1
⊢ LipschitzWith (k * 1 * 1) fun x => g (Complex.abs ((dualVector y) x))
Tactic:
simp_rw [←Complex.norm_eq_abs]
Proof state after:
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
k11 : k = k * 1 * 1
⊢ LipschitzWith (k * 1 * 1) fun x => g ‖(dualVector y) x‖
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
k11 : k = k * 1 * 1
⊢ LipschitzWith (k * 1 * 1) fun x => g ‖(dualVector y) x‖
Tactic:
apply (gk.comp lipschitzWith_one_norm).comp
Proof state after:
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
k11 : k = k * 1 * 1
⊢ LipschitzWith 1 fun x => (dualVector y) x
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
k11 : k = k * 1 * 1
⊢ LipschitzWith 1 fun x => (dualVector y) x
Tactic:
exact (dualVector y).lipschitz.weaken (dualVector_nnnorm y)
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
⊢ k = k * 1 * 1
Tactic:
norm_num
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 * 1 * dist x y ≤ g ‖y‖ + ↑k * 1 * (e / 2 / ↑k)
Tactic:
bound
Proof state after:
no goals