[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s✝ t s : Set H
c : ℝ
hc : 0 < c
y : H
hy : y ∈ {y | ∀ (x : H), x ∈ s → 0 ≤ inner x y}
x : H
hx : x ∈ s
⊢ 0 ≤ inner x (c • y)
[PROOFSTEP]
rw [real_inner_smul_right]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s✝ t s : Set H
c : ℝ
hc : 0 < c
y : H
hy : y ∈ {y | ∀ (x : H), x ∈ s → 0 ≤ inner x y}
x : H
hx : x ∈ s
⊢ 0 ≤ c * inner x y
[PROOFSTEP]
exact mul_nonneg hc.le (hy x hx)
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s✝ t s : Set H
u : H
hu : u ∈ {y | ∀ (x : H), x ∈ s → 0 ≤ inner x y}
v : H
hv : v ∈ {y | ∀ (x : H), x ∈ s → 0 ≤ inner x y}
x : H
hx : x ∈ s
⊢ 0 ≤ inner x (u + v)
[PROOFSTEP]
rw [inner_add_right]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s✝ t s : Set H
u : H
hu : u ∈ {y | ∀ (x : H), x ∈ s → 0 ≤ inner x y}
v : H
hv : v ∈ {y | ∀ (x : H), x ∈ s → 0 ≤ inner x y}
x : H
hx : x ∈ s
⊢ 0 ≤ inner x u + inner x v
[PROOFSTEP]
exact add_nonneg (hu x hx) (hv x hx)
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
⊢ innerDualCone univ = 0
[PROOFSTEP]
suffices ∀ x : H, x ∈ (univ : Set H).innerDualCone → x = 0
  by
  apply SetLike.coe_injective
  exact eq_singleton_iff_unique_mem.mpr ⟨fun x _ => (inner_zero_right _).ge, this⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
this : ∀ (x : H), x ∈ innerDualCone univ → x = 0
⊢ innerDualCone univ = 0
[PROOFSTEP]
apply SetLike.coe_injective
[GOAL]
case a
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
this : ∀ (x : H), x ∈ innerDualCone univ → x = 0
⊢ ↑(innerDualCone univ) = ↑0
[PROOFSTEP]
exact eq_singleton_iff_unique_mem.mpr ⟨fun x _ => (inner_zero_right _).ge, this⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
⊢ ∀ (x : H), x ∈ innerDualCone univ → x = 0
[PROOFSTEP]
exact fun x hx => by simpa [← real_inner_self_nonpos] using hx (-x) (mem_univ _)
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
x : H
hx : x ∈ innerDualCone univ
⊢ x = 0
[PROOFSTEP]
simpa [← real_inner_self_nonpos] using hx (-x) (mem_univ _)
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
x : H
x✝ : x ∈ s
⊢ 0 ≤ inner x 0
[PROOFSTEP]
rw [inner_zero_right]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s✝ t : Set H
x : H
s : Set H
⊢ innerDualCone (insert x s) = innerDualCone {x} ⊓ innerDualCone s
[PROOFSTEP]
rw [insert_eq, innerDualCone_union]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
ι : Sort u_6
f : ι → Set H
⊢ innerDualCone (⋃ (i : ι), f i) = ⨅ (i : ι), innerDualCone (f i)
[PROOFSTEP]
refine' le_antisymm (le_iInf fun i x hx y hy => hx _ <| mem_iUnion_of_mem _ hy) _
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
ι : Sort u_6
f : ι → Set H
⊢ ⨅ (i : ι), innerDualCone (f i) ≤ innerDualCone (⋃ (i : ι), f i)
[PROOFSTEP]
intro x hx y hy
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
ι : Sort u_6
f : ι → Set H
x : H
hx : x ∈ ⨅ (i : ι), innerDualCone (f i)
y : H
hy : y ∈ ⋃ (i : ι), f i
⊢ 0 ≤ inner y x
[PROOFSTEP]
rw [ConvexCone.mem_iInf] at hx 
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
ι : Sort u_6
f : ι → Set H
x : H
hx : ∀ (i : ι), x ∈ innerDualCone (f i)
y : H
hy : y ∈ ⋃ (i : ι), f i
⊢ 0 ≤ inner y x
[PROOFSTEP]
obtain ⟨j, hj⟩ := mem_iUnion.mp hy
[GOAL]
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
ι : Sort u_6
f : ι → Set H
x : H
hx : ∀ (i : ι), x ∈ innerDualCone (f i)
y : H
hy : y ∈ ⋃ (i : ι), f i
j : ι
hj : y ∈ f j
⊢ 0 ≤ inner y x
[PROOFSTEP]
exact hx _ _ hj
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
S : Set (Set H)
⊢ innerDualCone (⋃₀ S) = sInf (innerDualCone '' S)
[PROOFSTEP]
simp_rw [sInf_image, sUnion_eq_biUnion, innerDualCone_iUnion]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
⊢ ↑(innerDualCone s) = ⋂ (i : ↑s), ↑(innerDualCone {↑i})
[PROOFSTEP]
rw [← ConvexCone.coe_iInf, ← innerDualCone_iUnion, iUnion_of_singleton_coe]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
⊢ IsClosed ↑(innerDualCone s)
[PROOFSTEP]
rw [innerDualCone_eq_iInter_innerDualCone_singleton]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
⊢ IsClosed (⋂ (i : ↑s), ↑(innerDualCone {↑i}))
[PROOFSTEP]
apply isClosed_iInter
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
⊢ ∀ (i : ↑s), IsClosed ↑(innerDualCone {↑i})
[PROOFSTEP]
intro x
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
x : ↑s
⊢ IsClosed ↑(innerDualCone {↑x})
[PROOFSTEP]
have h : ({↑x} : Set H).innerDualCone = (inner x : H → ℝ) ⁻¹' Set.Ici 0 := by
  rw [innerDualCone_singleton, ConvexCone.coe_comap, ConvexCone.coe_positive, innerₛₗ_apply_coe]
    -- the preimage is closed as `inner x` is continuous and `[0, ∞)` is closed
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
x : ↑s
⊢ ↑(innerDualCone {↑x}) = inner ↑x ⁻¹' Ici 0
[PROOFSTEP]
rw [innerDualCone_singleton, ConvexCone.coe_comap, ConvexCone.coe_positive, innerₛₗ_apply_coe]
  -- the preimage is closed as `inner x` is continuous and `[0, ∞)` is closed
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
x : ↑s
h : ↑(innerDualCone {↑x}) = inner ↑x ⁻¹' Ici 0
⊢ IsClosed ↑(innerDualCone {↑x})
[PROOFSTEP]
rw [h]
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
x : ↑s
h : ↑(innerDualCone {↑x}) = inner ↑x ⁻¹' Ici 0
⊢ IsClosed (inner ↑x ⁻¹' Ici 0)
[PROOFSTEP]
exact isClosed_Ici.preimage (continuous_const.inner continuous_id')
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
⊢ Pointed K
[PROOFSTEP]
obtain ⟨x, hx⟩ := ne
[GOAL]
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
⊢ Pointed K
[PROOFSTEP]
let f : ℝ → H :=
  (· • x)
    -- f (0, ∞) is a subset of K
[GOAL]
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
⊢ Pointed K
[PROOFSTEP]
have fI : f '' Set.Ioi 0 ⊆ (K : Set H) := by
  rintro _ ⟨_, h, rfl⟩
  exact K.smul_mem (Set.mem_Ioi.1 h) hx
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
⊢ f '' Ioi 0 ⊆ ↑K
[PROOFSTEP]
rintro _ ⟨_, h, rfl⟩
[GOAL]
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
w✝ : ℝ
h : w✝ ∈ Ioi 0
⊢ f w✝ ∈ ↑K
[PROOFSTEP]
exact K.smul_mem (Set.mem_Ioi.1 h) hx
[GOAL]
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
fI : f '' Ioi 0 ⊆ ↑K
⊢ Pointed K
[PROOFSTEP]
have clf : closure (f '' Set.Ioi 0) ⊆ (K : Set H) := hc.closure_subset_iff.2 fI
[GOAL]
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
fI : f '' Ioi 0 ⊆ ↑K
clf : closure (f '' Ioi 0) ⊆ ↑K
⊢ Pointed K
[PROOFSTEP]
have fc : ContinuousWithinAt f (Set.Ioi (0 : ℝ)) 0 := (continuous_id.smul continuous_const).continuousWithinAt
[GOAL]
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
fI : f '' Ioi 0 ⊆ ↑K
clf : closure (f '' Ioi 0) ⊆ ↑K
fc : ContinuousWithinAt f (Ioi 0) 0
⊢ Pointed K
[PROOFSTEP]
have mem₀ :=
  fc.mem_closure_image
    (by rw [closure_Ioi (0 : ℝ), mem_Ici])
      -- as 0 ∈ closure f (0, ∞) and closure f (0, ∞) ⊆ K, 0 ∈ K.
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
fI : f '' Ioi 0 ⊆ ↑K
clf : closure (f '' Ioi 0) ⊆ ↑K
fc : ContinuousWithinAt f (Ioi 0) 0
⊢ 0 ∈ closure (Ioi 0)
[PROOFSTEP]
rw [closure_Ioi (0 : ℝ), mem_Ici]
[GOAL]
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
fI : f '' Ioi 0 ⊆ ↑K
clf : closure (f '' Ioi 0) ⊆ ↑K
fc : ContinuousWithinAt f (Ioi 0) 0
mem₀ : f 0 ∈ closure (f '' Ioi 0)
⊢ Pointed K
[PROOFSTEP]
have f₀ : f 0 = 0 := zero_smul ℝ x
[GOAL]
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
fI : f '' Ioi 0 ⊆ ↑K
clf : closure (f '' Ioi 0) ⊆ ↑K
fc : ContinuousWithinAt f (Ioi 0) 0
mem₀ : f 0 ∈ closure (f '' Ioi 0)
f₀ : f 0 = 0
⊢ Pointed K
[PROOFSTEP]
simpa only [f₀, ConvexCone.Pointed, ← SetLike.mem_coe] using mem_of_subset_of_mem clf mem₀
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
b : H
disj : ¬b ∈ K
⊢ ∃ y, (∀ (x : H), x ∈ K → 0 ≤ inner x y) ∧ inner y b < 0
[PROOFSTEP]
obtain ⟨z, hzK, infi⟩ := exists_norm_eq_iInf_of_complete_convex ne hc.isComplete K.convex b
[GOAL]
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
b : H
disj : ¬b ∈ K
z : H
hzK : z ∈ ↑K
infi : ‖b - z‖ = ⨅ (w : ↑↑K), ‖b - ↑w‖
⊢ ∃ y, (∀ (x : H), x ∈ K → 0 ≤ inner x y) ∧ inner y b < 0
[PROOFSTEP]
have hinner := (norm_eq_iInf_iff_real_inner_le_zero K.convex hzK).1 infi
[GOAL]
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
b : H
disj : ¬b ∈ K
z : H
hzK : z ∈ ↑K
infi : ‖b - z‖ = ⨅ (w : ↑↑K), ‖b - ↑w‖
hinner : ∀ (w : H), w ∈ ↑K → inner (b - z) (w - z) ≤ 0
⊢ ∃ y, (∀ (x : H), x ∈ K → 0 ≤ inner x y) ∧ inner y b < 0
[PROOFSTEP]
use z - b
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
b : H
disj : ¬b ∈ K
z : H
hzK : z ∈ ↑K
infi : ‖b - z‖ = ⨅ (w : ↑↑K), ‖b - ↑w‖
hinner : ∀ (w : H), w ∈ ↑K → inner (b - z) (w - z) ≤ 0
⊢ (∀ (x : H), x ∈ K → 0 ≤ inner x (z - b)) ∧ inner (z - b) b < 0
[PROOFSTEP]
constructor
[GOAL]
case h.left
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
b : H
disj : ¬b ∈ K
z : H
hzK : z ∈ ↑K
infi : ‖b - z‖ = ⨅ (w : ↑↑K), ‖b - ↑w‖
hinner : ∀ (w : H), w ∈ ↑K → inner (b - z) (w - z) ≤ 0
⊢ ∀ (x : H), x ∈ K → 0 ≤ inner x (z - b)
[PROOFSTEP]
rintro x hxK
[GOAL]
case h.left
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
b : H
disj : ¬b ∈ K
z : H
hzK : z ∈ ↑K
infi : ‖b - z‖ = ⨅ (w : ↑↑K), ‖b - ↑w‖
hinner : ∀ (w : H), w ∈ ↑K → inner (b - z) (w - z) ≤ 0
x : H
hxK : x ∈ K
⊢ 0 ≤ inner x (z - b)
[PROOFSTEP]
specialize hinner _ (K.add_mem hxK hzK)
[GOAL]
case h.left
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
b : H
disj : ¬b ∈ K
z : H
hzK : z ∈ ↑K
infi : ‖b - z‖ = ⨅ (w : ↑↑K), ‖b - ↑w‖
x : H
hxK : x ∈ K
hinner : inner (b - z) (x + z - z) ≤ 0
⊢ 0 ≤ inner x (z - b)
[PROOFSTEP]
rwa [add_sub_cancel, real_inner_comm, ← neg_nonneg, neg_eq_neg_one_mul, ← real_inner_smul_right, neg_smul, one_smul,
  neg_sub] at hinner 
[GOAL]
case h.right
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
b : H
disj : ¬b ∈ K
z : H
hzK : z ∈ ↑K
infi : ‖b - z‖ = ⨅ (w : ↑↑K), ‖b - ↑w‖
hinner : ∀ (w : H), w ∈ ↑K → inner (b - z) (w - z) ≤ 0
⊢ inner (z - b) b < 0
[PROOFSTEP]
have hinner₀ :=
  hinner 0
    (K.pointed_of_nonempty_of_isClosed ne hc)
      -- the rest of the proof is a straightforward calculation
[GOAL]
case h.right
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
b : H
disj : ¬b ∈ K
z : H
hzK : z ∈ ↑K
infi : ‖b - z‖ = ⨅ (w : ↑↑K), ‖b - ↑w‖
hinner : ∀ (w : H), w ∈ ↑K → inner (b - z) (w - z) ≤ 0
hinner₀ : inner (b - z) (0 - z) ≤ 0
⊢ inner (z - b) b < 0
[PROOFSTEP]
rw [zero_sub, inner_neg_right, Right.neg_nonpos_iff] at hinner₀ 
[GOAL]
case h.right
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
b : H
disj : ¬b ∈ K
z : H
hzK : z ∈ ↑K
infi : ‖b - z‖ = ⨅ (w : ↑↑K), ‖b - ↑w‖
hinner : ∀ (w : H), w ∈ ↑K → inner (b - z) (w - z) ≤ 0
hinner₀ : 0 ≤ inner (b - z) z
⊢ inner (z - b) b < 0
[PROOFSTEP]
have hbz : b - z ≠ 0 := by
  rw [sub_ne_zero]
  contrapose! hzK
  rwa [← hzK]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
b : H
disj : ¬b ∈ K
z : H
hzK : z ∈ ↑K
infi : ‖b - z‖ = ⨅ (w : ↑↑K), ‖b - ↑w‖
hinner : ∀ (w : H), w ∈ ↑K → inner (b - z) (w - z) ≤ 0
hinner₀ : 0 ≤ inner (b - z) z
⊢ b - z ≠ 0
[PROOFSTEP]
rw [sub_ne_zero]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
b : H
disj : ¬b ∈ K
z : H
hzK : z ∈ ↑K
infi : ‖b - z‖ = ⨅ (w : ↑↑K), ‖b - ↑w‖
hinner : ∀ (w : H), w ∈ ↑K → inner (b - z) (w - z) ≤ 0
hinner₀ : 0 ≤ inner (b - z) z
⊢ b ≠ z
[PROOFSTEP]
contrapose! hzK
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
b : H
disj : ¬b ∈ K
z : H
infi : ‖b - z‖ = ⨅ (w : ↑↑K), ‖b - ↑w‖
hinner : ∀ (w : H), w ∈ ↑K → inner (b - z) (w - z) ≤ 0
hinner₀ : 0 ≤ inner (b - z) z
hzK : b = z
⊢ ¬z ∈ ↑K
[PROOFSTEP]
rwa [← hzK]
[GOAL]
case h.right
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
b : H
disj : ¬b ∈ K
z : H
hzK : z ∈ ↑K
infi : ‖b - z‖ = ⨅ (w : ↑↑K), ‖b - ↑w‖
hinner : ∀ (w : H), w ∈ ↑K → inner (b - z) (w - z) ≤ 0
hinner₀ : 0 ≤ inner (b - z) z
hbz : b - z ≠ 0
⊢ inner (z - b) b < 0
[PROOFSTEP]
rw [← neg_zero, lt_neg, ← neg_one_mul, ← real_inner_smul_left, smul_sub, neg_smul, one_smul, neg_smul, neg_sub_neg,
  one_smul]
[GOAL]
case h.right
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
b : H
disj : ¬b ∈ K
z : H
hzK : z ∈ ↑K
infi : ‖b - z‖ = ⨅ (w : ↑↑K), ‖b - ↑w‖
hinner : ∀ (w : H), w ∈ ↑K → inner (b - z) (w - z) ≤ 0
hinner₀ : 0 ≤ inner (b - z) z
hbz : b - z ≠ 0
⊢ 0 < inner (b - z) b
[PROOFSTEP]
calc
  0 < ⟪b - z, b - z⟫_ℝ := lt_of_not_le ((Iff.not real_inner_self_nonpos).2 hbz)
  _ = ⟪b - z, b - z⟫_ℝ + 0 := (add_zero _).symm
  _ ≤ ⟪b - z, b - z⟫_ℝ + ⟪b - z, z⟫_ℝ := (add_le_add rfl.ge hinner₀)
  _ = ⟪b - z, b - z + z⟫_ℝ := (inner_add_right _ _ _).symm
  _ = ⟪b - z, b⟫_ℝ := by rw [sub_add_cancel]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
b : H
disj : ¬b ∈ K
z : H
hzK : z ∈ ↑K
infi : ‖b - z‖ = ⨅ (w : ↑↑K), ‖b - ↑w‖
hinner : ∀ (w : H), w ∈ ↑K → inner (b - z) (w - z) ≤ 0
hinner₀ : 0 ≤ inner (b - z) z
hbz : b - z ≠ 0
⊢ inner (b - z) (b - z + z) = inner (b - z) b
[PROOFSTEP]
rw [sub_add_cancel]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
⊢ innerDualCone ↑(innerDualCone ↑K) = K
[PROOFSTEP]
ext x
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
x : H
⊢ x ∈ innerDualCone ↑(innerDualCone ↑K) ↔ x ∈ K
[PROOFSTEP]
constructor
[GOAL]
case h.mp
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
x : H
⊢ x ∈ innerDualCone ↑(innerDualCone ↑K) → x ∈ K
[PROOFSTEP]
rw [mem_innerDualCone, ← SetLike.mem_coe]
[GOAL]
case h.mp
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
x : H
⊢ (∀ (x_1 : H), x_1 ∈ ↑(innerDualCone ↑K) → 0 ≤ inner x_1 x) → x ∈ ↑K
[PROOFSTEP]
contrapose!
[GOAL]
case h.mp
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
x : H
⊢ ¬x ∈ ↑K → ∃ x_1, x_1 ∈ ↑(innerDualCone ↑K) ∧ inner x_1 x < 0
[PROOFSTEP]
exact K.hyperplane_separation_of_nonempty_of_isClosed_of_nmem ne hc
[GOAL]
case h.mpr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
x : H
⊢ x ∈ K → x ∈ innerDualCone ↑(innerDualCone ↑K)
[PROOFSTEP]
rintro hxK y h
[GOAL]
case h.mpr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
x : H
hxK : x ∈ K
y : H
h : y ∈ ↑(innerDualCone ↑K)
⊢ 0 ≤ inner y x
[PROOFSTEP]
specialize h x hxK
[GOAL]
case h.mpr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
x : H
hxK : x ∈ K
y : H
h : 0 ≤ inner x y
⊢ 0 ≤ inner y x
[PROOFSTEP]
rwa [real_inner_comm]
