internlm/Lean-Github huggingface dataset:
Theorem: mem_polarDual
Proof state before:
case mp.inr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v x : E
hx : x ∈ X
hx0 : ¬x = 0
h : ⟪↑{ val := x, property := hx0 }, v⟫_ℝ ≤ 1
⊢ ⟪x, v⟫_ℝ ≤ 1
Tactic:
exact h
Proof state after:
no goals
Theorem: mem_polarDual
Proof state before:
case mp.inl
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), v ∈ t
x : E
hx : x ∈ X
hx0 : x = 0
⊢ ⟪x, v⟫_ℝ ≤ 1
Tactic:
rw [hx0, inner_zero_left]
Proof state after:
case mp.inl
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), v ∈ t
x : E
hx : x ∈ X
hx0 : x = 0
⊢ 0 ≤ 1
Theorem: mem_polarDual
Proof state before:
case mp.inl
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), v ∈ t
x : E
hx : x ∈ X
hx0 : x = 0
⊢ 0 ≤ 1
Tactic:
exact zero_le_one
Proof state after:
no goals
Theorem: mem_polarDual
Proof state before:
case mp.inr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), v ∈ t
x : E
hx : x ∈ X
hx0 : ¬x = 0
⊢ ↑(pointDual { val := x, property := hx0 }) ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X))
Tactic:
apply Set.mem_image_of_mem
Proof state after:
case mp.inr.h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), v ∈ t
x : E
hx : x ∈ X
hx0 : ¬x = 0
⊢ pointDual { val := x, property := hx0 } ∈ pointDual '' (Subtype.val ⁻¹' X)
Theorem: mem_polarDual
Proof state before:
case mp.inr.h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), v ∈ t
x : E
hx : x ∈ X
hx0 : ¬x = 0
⊢ pointDual { val := x, property := hx0 } ∈ pointDual '' (Subtype.val ⁻¹' X)
Tactic:
apply Set.mem_image_of_mem
Proof state after:
case mp.inr.h.h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), v ∈ t
x : E
hx : x ∈ X
hx0 : ¬x = 0
⊢ { val := x, property := hx0 } ∈ Subtype.val ⁻¹' X
Theorem: mem_polarDual
Proof state before:
case mp.inr.h.h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), v ∈ t
x : E
hx : x ∈ X
hx0 : ¬x = 0
⊢ { val := x, property := hx0 } ∈ Subtype.val ⁻¹' X
Tactic:
rw [Set.mem_preimage]
Proof state after:
case mp.inr.h.h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), v ∈ t
x : E
hx : x ∈ X
hx0 : ¬x = 0
⊢ ↑{ val := x, property := hx0 } ∈ X
Theorem: mem_polarDual
Proof state before:
case mp.inr.h.h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), v ∈ t
x : E
hx : x ∈ X
hx0 : ¬x = 0
⊢ ↑{ val := x, property := hx0 } ∈ X
Tactic:
exact hx
Proof state after:
no goals
Theorem: mem_polarDual
Proof state before:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
⊢ (∀ x ∈ X, ⟪x, v⟫_ℝ ≤ 1) → ∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), v ∈ t
Tactic:
intro h Hi_s hHi_s
Proof state after:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ x ∈ X, ⟪x, v⟫_ℝ ≤ 1
Hi_s : Set E
hHi_s : Hi_s ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X))
⊢ v ∈ Hi_s
Theorem: mem_polarDual
Proof state before:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ x ∈ X, ⟪x, v⟫_ℝ ≤ 1
Hi_s : Set E
hHi_s : Hi_s ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X))
⊢ v ∈ Hi_s
Tactic:
rw [Set.mem_image] at hHi_s
Proof state after:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ x ∈ X, ⟪x, v⟫_ℝ ≤ 1
Hi_s : Set E
hHi_s : ∃ x ∈ pointDual '' (Subtype.val ⁻¹' X), ↑x = Hi_s
⊢ v ∈ Hi_s
Theorem: mem_polarDual
Proof state before:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ x ∈ X, ⟪x, v⟫_ℝ ≤ 1
Hi_s : Set E
hHi_s : ∃ x ∈ pointDual '' (Subtype.val ⁻¹' X), ↑x = Hi_s
⊢ v ∈ Hi_s
Tactic:
rcases hHi_s with ⟨ Hi_, hHi_, rfl ⟩
Proof state after:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ x ∈ X, ⟪x, v⟫_ℝ ≤ 1
Hi_ : Halfspace E
hHi_ : Hi_ ∈ pointDual '' (Subtype.val ⁻¹' X)
⊢ v ∈ ↑Hi_
Theorem: mem_polarDual
Proof state before:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ x ∈ X, ⟪x, v⟫_ℝ ≤ 1
Hi_ : Halfspace E
hHi_ : Hi_ ∈ pointDual '' (Subtype.val ⁻¹' X)
⊢ v ∈ ↑Hi_
Tactic:
rw [Set.mem_image] at hHi_
Proof state after:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ x ∈ X, ⟪x, v⟫_ℝ ≤ 1
Hi_ : Halfspace E
hHi_ : ∃ x ∈ Subtype.val ⁻¹' X, pointDual x = Hi_
⊢ v ∈ ↑Hi_
Theorem: mem_polarDual
Proof state before:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ x ∈ X, ⟪x, v⟫_ℝ ≤ 1
Hi_ : Halfspace E
hHi_ : ∃ x ∈ Subtype.val ⁻¹' X, pointDual x = Hi_
⊢ v ∈ ↑Hi_
Tactic:
rcases hHi_ with ⟨ p, hp, rfl ⟩
Proof state after:
case mpr.intro.intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ x ∈ X, ⟪x, v⟫_ℝ ≤ 1
p : { p // p ≠ 0 }
hp : p ∈ Subtype.val ⁻¹' X
⊢ v ∈ ↑(pointDual p)
Theorem: mem_polarDual
Proof state before:
case mpr.intro.intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ x ∈ X, ⟪x, v⟫_ℝ ≤ 1
p : { p // p ≠ 0 }
hp : p ∈ Subtype.val ⁻¹' X
⊢ v ∈ ↑(pointDual p)
Tactic:
specialize h p.1 hp
Proof state after:
case mpr.intro.intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
p : { p // p ≠ 0 }
hp : p ∈ Subtype.val ⁻¹' X
h : ⟪↑p, v⟫_ℝ ≤ 1
⊢ v ∈ ↑(pointDual p)
Theorem: mem_polarDual
Proof state before:
case mpr.intro.intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
p : { p // p ≠ 0 }
hp : p ∈ Subtype.val ⁻¹' X
h : ⟪↑p, v⟫_ℝ ≤ 1
⊢ v ∈ ↑(pointDual p)
Tactic:
rw [mem_pointDual]
Proof state after:
case mpr.intro.intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
p : { p // p ≠ 0 }
hp : p ∈ Subtype.val ⁻¹' X
h : ⟪↑p, v⟫_ℝ ≤ 1
⊢ ⟪↑p, v⟫_ℝ ≤ 1
Theorem: mem_polarDual
Proof state before:
case mpr.intro.intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
p : { p // p ≠ 0 }
hp : p ∈ Subtype.val ⁻¹' X
h : ⟪↑p, v⟫_ℝ ≤ 1
⊢ ⟪↑p, v⟫_ℝ ≤ 1
Tactic:
exact h
Proof state after:
no goals
Theorem: mem_polarDual'
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
⊢ v ∈ polarDual X ↔ ∀ x ∈ X, ⟪v, x⟫_ℝ ≤ 1
Tactic:
simp_rw [mem_polarDual, real_inner_comm]
Proof state after:
no goals
Theorem: polarDual_comm_half
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Y : Set E
⊢ X ⊆ polarDual Y → Y ⊆ polarDual X
Tactic:
rw [Set.subset_def, Set.subset_def]
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Y : Set E
⊢ (∀ x ∈ X, x ∈ polarDual Y) → ∀ x ∈ Y, x ∈ polarDual X
Theorem: polarDual_comm_half
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Y : Set E
⊢ (∀ x ∈ X, x ∈ polarDual Y) → ∀ x ∈ Y, x ∈ polarDual X
Tactic:
intro h y hy
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Y : Set E
h : ∀ x ∈ X, x ∈ polarDual Y
y : E
hy : y ∈ Y
⊢ y ∈ polarDual X
Theorem: polarDual_comm_half
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Y : Set E
h : ∀ x ∈ X, x ∈ polarDual Y
y : E
hy : y ∈ Y
⊢ y ∈ polarDual X
Tactic:
rw [mem_polarDual]
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Y : Set E
h : ∀ x ∈ X, x ∈ polarDual Y
y : E
hy : y ∈ Y
⊢ ∀ x ∈ X, ⟪x, y⟫_ℝ ≤ 1
Theorem: polarDual_comm_half
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Y : Set E
h : ∀ x ∈ X, x ∈ polarDual Y
y : E
hy : y ∈ Y
⊢ ∀ x ∈ X, ⟪x, y⟫_ℝ ≤ 1
Tactic:
intro x hx
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Y : Set E
h : ∀ x ∈ X, x ∈ polarDual Y
y : E
hy : y ∈ Y
x : E
hx : x ∈ X
⊢ ⟪x, y⟫_ℝ ≤ 1
Theorem: polarDual_comm_half
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Y : Set E
h : ∀ x ∈ X, x ∈ polarDual Y
y : E
hy : y ∈ Y
x : E
hx : x ∈ X
⊢ ⟪x, y⟫_ℝ ≤ 1
Tactic:
rw [real_inner_comm]
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Y : Set E
h : ∀ x ∈ X, x ∈ polarDual Y
y : E
hy : y ∈ Y
x : E
hx : x ∈ X
⊢ ⟪y, x⟫_ℝ ≤ 1
Theorem: polarDual_comm_half
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Y : Set E
h : ∀ x ∈ X, x ∈ polarDual Y
y : E
hy : y ∈ Y
x : E
hx : x ∈ X
⊢ ⟪y, x⟫_ℝ ≤ 1
Tactic:
specialize h x hx
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Y : Set E
y : E
hy : y ∈ Y
x : E
hx : x ∈ X
h : x ∈ polarDual Y
⊢ ⟪y, x⟫_ℝ ≤ 1
Theorem: polarDual_comm_half
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Y : Set E
y : E
hy : y ∈ Y
x : E
hx : x ∈ X
h : x ∈ polarDual Y
⊢ ⟪y, x⟫_ℝ ≤ 1
Tactic:
rw [mem_polarDual] at h
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Y : Set E
y : E
hy : y ∈ Y
x : E
hx : x ∈ X
h : ∀ x_1 ∈ Y, ⟪x_1, x⟫_ℝ ≤ 1
⊢ ⟪y, x⟫_ℝ ≤ 1
Theorem: polarDual_comm_half
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Y : Set E
y : E
hy : y ∈ Y
x : E
hx : x ∈ X
h : ∀ x_1 ∈ Y, ⟪x_1, x⟫_ℝ ≤ 1
⊢ ⟪y, x⟫_ℝ ≤ 1
Tactic:
specialize h y hy
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Y : Set E
y : E
hy : y ∈ Y
x : E
hx : x ∈ X
h : ⟪y, x⟫_ℝ ≤ 1
⊢ ⟪y, x⟫_ℝ ≤ 1
Theorem: polarDual_comm_half
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Y : Set E
y : E
hy : y ∈ Y
x : E
hx : x ∈ X
h : ⟪y, x⟫_ℝ ≤ 1
⊢ ⟪y, x⟫_ℝ ≤ 1
Tactic:
exact h
Proof state after:
no goals
Theorem: polarDual_comm
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Y : Set E
⊢ X ⊆ polarDual Y ↔ Y ⊆ polarDual X
Tactic:
constructor <;> exact fun h => polarDual_comm_half _ _ h
Proof state after:
no goals
Theorem: doublePolarDual_self
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
hXcl : IsClosed X
hXcv : Convex ℝ X
hX0 : 0 ∈ X
⊢ polarDual (polarDual X) = X
Tactic:
apply subset_antisymm
Proof state after:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
hXcl : IsClosed X
hXcv : Convex ℝ X
hX0 : 0 ∈ X
⊢ polarDual (polarDual X) ⊆ X

case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
hXcl : IsClosed X
hXcv : Convex ℝ X
hX0 : 0 ∈ X
⊢ X ⊆ polarDual (polarDual X)
Theorem: doublePolarDual_self
Proof state before:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
hXcl : IsClosed X
hXcv : Convex ℝ X
hX0 : 0 ∈ X
⊢ polarDual (polarDual X) ⊆ X
Tactic:
intro x hx
Proof state after:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
hXcl : IsClosed X
hXcv : Convex ℝ X
hX0 : 0 ∈ X
x : E
hx : x ∈ polarDual (polarDual X)
⊢ x ∈ X
Theorem: doublePolarDual_self
Proof state before:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
hXcl : IsClosed X
hXcv : Convex ℝ X
hX0 : 0 ∈ X
x : E
hx : x ∈ polarDual (polarDual X)
⊢ x ∈ X
Tactic:
contrapose! hx
Proof state after:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
hXcl : IsClosed X
hXcv : Convex ℝ X
hX0 : 0 ∈ X
x : E
hx : x ∉ X
⊢ x ∉ polarDual (polarDual X)
Theorem: doublePolarDual_self
Proof state before:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
hXcl : IsClosed X
hXcv : Convex ℝ X
hX0 : 0 ∈ X
x : E
hx : x ∉ X
⊢ x ∉ polarDual (polarDual X)
Tactic:
rw [mem_polarDual]
Proof state after:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
hXcl : IsClosed X
hXcv : Convex ℝ X
hX0 : 0 ∈ X
x : E
hx : x ∉ X
⊢ ¬∀ x_1 ∈ polarDual X, ⟪x_1, x⟫_ℝ ≤ 1
Theorem: doublePolarDual_self
Proof state before:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
hXcl : IsClosed X
hXcv : Convex ℝ X
hX0 : 0 ∈ X
x : E
hx : x ∉ X
⊢ ¬∀ x_1 ∈ polarDual X, ⟪x_1, x⟫_ℝ ≤ 1
Tactic:
push_neg
Proof state after:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
hXcl : IsClosed X
hXcv : Convex ℝ X
hX0 : 0 ∈ X
x : E
hx : x ∉ X
⊢ ∃ x_1 ∈ polarDual X, 1 < ⟪x_1, x⟫_ℝ
Theorem: doublePolarDual_self
Proof state before:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
hXcl : IsClosed X
hXcv : Convex ℝ X
hX0 : 0 ∈ X
x : E
hx : x ∉ X
⊢ ∃ x_1 ∈ polarDual X, 1 < ⟪x_1, x⟫_ℝ
Tactic:
rcases geometric_hahn_banach_point_closed hXcv hXcl hx with ⟨ f, α, h, hX ⟩
Proof state after:
case a.intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
hXcl : IsClosed X
hXcv : Convex ℝ X
hX0 : 0 ∈ X
x : E
hx : x ∉ X
f : E →L[ℝ] ℝ
α : ℝ
h : f x < α
hX : ∀ b ∈ X, α < f b
⊢ ∃ x_1 ∈ polarDual X, 1 < ⟪x_1, x⟫_ℝ
Theorem: doublePolarDual_self
Proof state before:
case a.intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
hXcl : IsClosed X
hXcv : Convex ℝ X
hX0 : 0 ∈ X
x : E
hx : x ∉ X
f : E →L[ℝ] ℝ
α : ℝ
h : f x < α
hX : ∀ b ∈ X, α < f b
⊢ ∃ x_1 ∈ polarDual X, 1 < ⟪x_1, x⟫_ℝ
Tactic:
use (α⁻¹) • (InnerProductSpace.toDual ℝ E).symm f
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
hXcl : IsClosed X
hXcv : Convex ℝ X
hX0 : 0 ∈ X
x : E
hx : x ∉ X
f : E →L[ℝ] ℝ
α : ℝ
h : f x < α
hX : ∀ b ∈ X, α < f b
⊢ α⁻¹ • (LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E)) f ∈ polarDual X ∧
    1 < ⟪α⁻¹ • (LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E)) f, x⟫_ℝ
Theorem: doublePolarDual_self
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
hXcl : IsClosed X
hXcv : Convex ℝ X
hX0 : 0 ∈ X
x : E
hx : x ∉ X
f : E →L[ℝ] ℝ
α : ℝ
h : f x < α
hX : ∀ b ∈ X, α < f b
⊢ α⁻¹ • (LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E)) f ∈ polarDual X ∧
    1 < ⟪α⁻¹ • (LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E)) f, x⟫_ℝ
Tactic:
rw [mem_polarDual']
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
hXcl : IsClosed X
hXcv : Convex ℝ X
hX0 : 0 ∈ X
x : E
hx : x ∉ X
f : E →L[ℝ] ℝ
α : ℝ
h : f x < α
hX : ∀ b ∈ X, α < f b
⊢ (∀ x ∈ X, ⟪α⁻¹ • (LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E)) f, x⟫_ℝ ≤ 1) ∧
    1 < ⟪α⁻¹ • (LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E)) f, x⟫_ℝ
Theorem: doublePolarDual_self
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
hXcl : IsClosed X
hXcv : Convex ℝ X
hX0 : 0 ∈ X
x : E
hx : x ∉ X
f : E →L[ℝ] ℝ
α : ℝ
h : f x < α
hX : ∀ b ∈ X, α < f b
⊢ (∀ x ∈ X, ⟪α⁻¹ • (LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E)) f, x⟫_ℝ ≤ 1) ∧
    1 < ⟪α⁻¹ • (LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E)) f, x⟫_ℝ
Tactic:
have hαneg : 0 < -α := (neg_pos.mpr ((ContinuousLinearMap.map_zero f) ▸ (hX 0 hX0)))
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
hXcl : IsClosed X
hXcv : Convex ℝ X
hX0 : 0 ∈ X
x : E
hx : x ∉ X
f : E →L[ℝ] ℝ
α : ℝ
h : f x < α
hX : ∀ b ∈ X, α < f b
hαneg : 0 < -α
⊢ (∀ x ∈ X, ⟪α⁻¹ • (LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E)) f, x⟫_ℝ ≤ 1) ∧
    1 < ⟪α⁻¹ • (LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E)) f, x⟫_ℝ
Theorem: doublePolarDual_self
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
hXcl : IsClosed X
hXcv : Convex ℝ X
hX0 : 0 ∈ X
x : E
hx : x ∉ X
f : E →L[ℝ] ℝ
α : ℝ
h : f x < α
hX : ∀ b ∈ X, α < f b
hαneg : 0 < -α
⊢ (∀ x ∈ X, ⟪α⁻¹ • (LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E)) f, x⟫_ℝ ≤ 1) ∧
    1 < ⟪α⁻¹ • (LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E)) f, x⟫_ℝ
Tactic:
constructor <;> intros <;> (try apply le_of_lt) <;> rw [real_inner_smul_left,
  InnerProductSpace.toDual_symm_apply, ←neg_lt_neg_iff, ←neg_mul, mul_comm, neg_inv, ← division_def]
Proof state after:
case h.left.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
hXcl : IsClosed X
hXcv : Convex ℝ X
hX0 : 0 ∈ X
x : E
hx : x ∉ X
f : E →L[ℝ] ℝ
α : ℝ
h : f x < α
hX : ∀ b ∈ X, α < f b
hαneg : 0 < -α
x✝ : E
a✝ : x✝ ∈ X
⊢ -1 < f x✝ / -α

case h.right
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
hXcl : IsClosed X
hXcv : Convex ℝ X
hX0 : 0 ∈ X
x : E
hx : x ∉ X
f : E →L[ℝ] ℝ
α : ℝ
h : f x < α
hX : ∀ b ∈ X, α < f b
hαneg : 0 < -α
⊢ f x / -α < -1
Theorem: doublePolarDual_self
Proof state before:
case h.left
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
hXcl : IsClosed X
hXcv : Convex ℝ X
hX0 : 0 ∈ X
x : E
hx : x ∉ X
f : E →L[ℝ] ℝ
α : ℝ
h : f x < α
hX : ∀ b ∈ X, α < f b
hαneg : 0 < -α
x✝ : E
a✝ : x✝ ∈ X
⊢ ⟪α⁻¹ • (LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E)) f, x✝⟫_ℝ ≤ 1
Tactic:
try apply le_of_lt
Proof state after:
case h.left.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
hXcl : IsClosed X
hXcv : Convex ℝ X
hX0 : 0 ∈ X
x : E
hx : x ∉ X
f : E →L[ℝ] ℝ
α : ℝ
h : f x < α
hX : ∀ b ∈ X, α < f b
hαneg : 0 < -α
x✝ : E
a✝ : x✝ ∈ X
⊢ ⟪α⁻¹ • (LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E)) f, x✝⟫_ℝ < 1
Theorem: doublePolarDual_self
Proof state before:
case h.left
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
hXcl : IsClosed X
hXcv : Convex ℝ X
hX0 : 0 ∈ X
x : E
hx : x ∉ X
f : E →L[ℝ] ℝ
α : ℝ
h : f x < α
hX : ∀ b ∈ X, α < f b
hαneg : 0 < -α
x✝ : E
a✝ : x✝ ∈ X
⊢ ⟪α⁻¹ • (LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E)) f, x✝⟫_ℝ ≤ 1
Tactic:
apply le_of_lt
Proof state after:
case h.left.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
hXcl : IsClosed X
hXcv : Convex ℝ X
hX0 : 0 ∈ X
x : E
hx : x ∉ X
f : E →L[ℝ] ℝ
α : ℝ
h : f x < α
hX : ∀ b ∈ X, α < f b
hαneg : 0 < -α
x✝ : E
a✝ : x✝ ∈ X
⊢ ⟪α⁻¹ • (LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E)) f, x✝⟫_ℝ < 1
Theorem: doublePolarDual_self
Proof state before:
case h.left.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
hXcl : IsClosed X
hXcv : Convex ℝ X
hX0 : 0 ∈ X
x : E
hx : x ∉ X
f : E →L[ℝ] ℝ
α : ℝ
h : f x < α
hX : ∀ b ∈ X, α < f b
hαneg : 0 < -α
x✝ : E
a✝ : x✝ ∈ X
⊢ -1 < f x✝ / -α
Tactic:
rw [lt_div_iff hαneg, neg_one_mul, neg_neg]
Proof state after:
case h.left.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
hXcl : IsClosed X
hXcv : Convex ℝ X
hX0 : 0 ∈ X
x : E
hx : x ∉ X
f : E →L[ℝ] ℝ
α : ℝ
h : f x < α
hX : ∀ b ∈ X, α < f b
hαneg : 0 < -α
x✝ : E
a✝ : x✝ ∈ X
⊢ α < f x✝
Theorem: doublePolarDual_self
Proof state before:
case h.left.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
hXcl : IsClosed X
hXcv : Convex ℝ X
hX0 : 0 ∈ X
x : E
hx : x ∉ X
f : E →L[ℝ] ℝ
α : ℝ
h : f x < α
hX : ∀ b ∈ X, α < f b
hαneg : 0 < -α
x✝ : E
a✝ : x✝ ∈ X
⊢ α < f x✝
Tactic:
exact hX (by assumption) (by assumption)
Proof state after:
no goals
Theorem: doublePolarDual_self
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
hXcl : IsClosed X
hXcv : Convex ℝ X
hX0 : 0 ∈ X
x : E
hx : x ∉ X
f : E →L[ℝ] ℝ
α : ℝ
h : f x < α
hX : ∀ b ∈ X, α < f b
hαneg : 0 < -α
x✝ : E
a✝ : x✝ ∈ X
⊢ E
Tactic:
assumption
Proof state after:
no goals
Theorem: doublePolarDual_self
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
hXcl : IsClosed X
hXcv : Convex ℝ X
hX0 : 0 ∈ X
x : E
hx : x ∉ X
f : E →L[ℝ] ℝ
α : ℝ
h : f x < α
hX : ∀ b ∈ X, α < f b
hαneg : 0 < -α
x✝ : E
a✝ : x✝ ∈ X
⊢ x✝ ∈ X
Tactic:
assumption
Proof state after:
no goals
Theorem: doublePolarDual_self
Proof state before:
case h.right
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
hXcl : IsClosed X
hXcv : Convex ℝ X
hX0 : 0 ∈ X
x : E
hx : x ∉ X
f : E →L[ℝ] ℝ
α : ℝ
h : f x < α
hX : ∀ b ∈ X, α < f b
hαneg : 0 < -α
⊢ f x / -α < -1
Tactic:
rw [div_lt_iff hαneg, neg_one_mul, neg_neg]
Proof state after:
case h.right
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
hXcl : IsClosed X
hXcv : Convex ℝ X
hX0 : 0 ∈ X
x : E
hx : x ∉ X
f : E →L[ℝ] ℝ
α : ℝ
h : f x < α
hX : ∀ b ∈ X, α < f b
hαneg : 0 < -α
⊢ f x < α
Theorem: doublePolarDual_self
Proof state before:
case h.right
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
hXcl : IsClosed X
hXcv : Convex ℝ X
hX0 : 0 ∈ X
x : E
hx : x ∉ X
f : E →L[ℝ] ℝ
α : ℝ
h : f x < α
hX : ∀ b ∈ X, α < f b
hαneg : 0 < -α
⊢ f x < α
Tactic:
exact h
Proof state after:
no goals
Theorem: doublePolarDual_self
Proof state before:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
hXcl : IsClosed X
hXcv : Convex ℝ X
hX0 : 0 ∈ X
⊢ X ⊆ polarDual (polarDual X)
Tactic:
rw [polarDual_comm]
Proof state after:
no goals
Theorem: polarDual_empty
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
⊢ polarDual ∅ = Set.univ
Tactic:
rw [polarDual, Set.preimage_empty, Set.image_empty, Set.image_empty, Set.sInter_empty]
Proof state after:
no goals