Theorem: doublePolarDual_self (src/Polar.lean)

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
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)

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
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

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
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)

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]
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

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
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⟫_ℝ

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 ⟩
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⟫_ℝ

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
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⟫_ℝ

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']
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⟫_ℝ

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)))
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⟫_ℝ

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]
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

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
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

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
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

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]
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✝

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)
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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]
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 < α

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
State after:
no goals

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]
State after:
no goals