Theorem: empty_Hpolytope (src/Polytope.lean)

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = ∅
Tactic:
have h := exists_ne (0:E)
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
h : ∃ y, y ≠ 0
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = ∅

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
h : ∃ y, y ≠ 0
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = ∅
Tactic:
rcases h with ⟨ x, hx ⟩
State after:
case intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x : E
hx : x ≠ 0
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = ∅

State before:
case intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x : E
hx : x ≠ 0
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = ∅
Tactic:
let xhat := (norm x)⁻¹ • x
State after:
case intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x : E
hx : x ≠ 0
xhat : E := ‖x‖⁻¹ • x
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = ∅

State before:
case intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x : E
hx : x ≠ 0
xhat : E := ‖x‖⁻¹ • x
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = ∅
Tactic:
let fval : NormedSpace.Dual ℝ E := InnerProductSpace.toDualMap ℝ _ xhat
State after:
case intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x : E
hx : x ≠ 0
xhat : E := ‖x‖⁻¹ • x
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = ∅

State before:
case intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x : E
hx : x ≠ 0
xhat : E := ‖x‖⁻¹ • x
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = ∅
Tactic:
let f : {f : (NormedSpace.Dual ℝ E) // norm f = 1} := ⟨ fval , (by
  change norm (innerSL ℝ ((norm x)⁻¹ • x)) = 1
  have := @norm_smul_inv_norm ℝ _ E _ _ x hx
  rw [IsROrC.ofReal_real_eq_id, id_eq] at this
  rw [innerSL_apply_norm, this]
  done
) ⟩
State after:
case intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x : E
hx : x ≠ 0
xhat : E := ‖x‖⁻¹ • x
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
f : { f // ‖f‖ = 1 } := { val := fval, property := ⋯ }
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = ∅

State before:
case intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x : E
hx : x ≠ 0
xhat : E := ‖x‖⁻¹ • x
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
f : { f // ‖f‖ = 1 } := { val := fval, property := ⋯ }
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = ∅
Tactic:
refine ⟨ {Halfspace.mk f (-1), Halfspace.mk (-f) (-1)} ,
  (by simp only [Set.mem_singleton_iff, Halfspace.mk.injEq, Set.finite_singleton, Set.Finite.insert]) , ?_ ⟩
State after:
case intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x : E
hx : x ≠ 0
xhat : E := ‖x‖⁻¹ • x
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
f : { f // ‖f‖ = 1 } := { val := fval, property := ⋯ }
⊢ Hpolytope ⋯ = ∅

State before:
case intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x : E
hx : x ≠ 0
xhat : E := ‖x‖⁻¹ • x
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
f : { f // ‖f‖ = 1 } := { val := fval, property := ⋯ }
⊢ Hpolytope ⋯ = ∅
Tactic:
ext x
State after:
case intro.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x✝ : E
hx : x✝ ≠ 0
xhat : E := ‖x✝‖⁻¹ • x✝
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
f : { f // ‖f‖ = 1 } := { val := fval, property := ⋯ }
x : E
⊢ x ∈ Hpolytope ⋯ ↔ x ∈ ∅

State before:
case intro.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x✝ : E
hx : x✝ ≠ 0
xhat : E := ‖x✝‖⁻¹ • x✝
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
f : { f // ‖f‖ = 1 } := { val := fval, property := ⋯ }
x : E
⊢ x ∈ Hpolytope ⋯ ↔ x ∈ ∅
Tactic:
rw [Set.mem_empty_iff_false, iff_false, mem_Hpolytope]
State after:
case intro.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x✝ : E
hx : x✝ ≠ 0
xhat : E := ‖x✝‖⁻¹ • x✝
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
f : { f // ‖f‖ = 1 } := { val := fval, property := ⋯ }
x : E
⊢ ¬∀ Hi ∈ {{ f := f, α := -1 }, { f := -f, α := -1 }}, ↑Hi.f x ≤ Hi.α

State before:
case intro.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x✝ : E
hx : x✝ ≠ 0
xhat : E := ‖x✝‖⁻¹ • x✝
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
f : { f // ‖f‖ = 1 } := { val := fval, property := ⋯ }
x : E
⊢ ¬∀ Hi ∈ {{ f := f, α := -1 }, { f := -f, α := -1 }}, ↑Hi.f x ≤ Hi.α
Tactic:
intro h
State after:
case intro.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x✝ : E
hx : x✝ ≠ 0
xhat : E := ‖x✝‖⁻¹ • x✝
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
f : { f // ‖f‖ = 1 } := { val := fval, property := ⋯ }
x : E
h : ∀ Hi ∈ {{ f := f, α := -1 }, { f := -f, α := -1 }}, ↑Hi.f x ≤ Hi.α
⊢ False

State before:
case intro.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x✝ : E
hx : x✝ ≠ 0
xhat : E := ‖x✝‖⁻¹ • x✝
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
f : { f // ‖f‖ = 1 } := { val := fval, property := ⋯ }
x : E
h : ∀ Hi ∈ {{ f := f, α := -1 }, { f := -f, α := -1 }}, ↑Hi.f x ≤ Hi.α
⊢ False
Tactic:
have h1 := h (Halfspace.mk f (-1)) (by simp)
State after:
case intro.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x✝ : E
hx : x✝ ≠ 0
xhat : E := ‖x✝‖⁻¹ • x✝
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
f : { f // ‖f‖ = 1 } := { val := fval, property := ⋯ }
x : E
h : ∀ Hi ∈ {{ f := f, α := -1 }, { f := -f, α := -1 }}, ↑Hi.f x ≤ Hi.α
h1 : ↑{ f := f, α := -1 }.f x ≤ { f := f, α := -1 }.α
⊢ False

State before:
case intro.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x✝ : E
hx : x✝ ≠ 0
xhat : E := ‖x✝‖⁻¹ • x✝
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
f : { f // ‖f‖ = 1 } := { val := fval, property := ⋯ }
x : E
h : ∀ Hi ∈ {{ f := f, α := -1 }, { f := -f, α := -1 }}, ↑Hi.f x ≤ Hi.α
h1 : ↑{ f := f, α := -1 }.f x ≤ { f := f, α := -1 }.α
⊢ False
Tactic:
have h2 := h (Halfspace.mk (-f) (-1)) (by simp)
State after:
case intro.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x✝ : E
hx : x✝ ≠ 0
xhat : E := ‖x✝‖⁻¹ • x✝
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
f : { f // ‖f‖ = 1 } := { val := fval, property := ⋯ }
x : E
h : ∀ Hi ∈ {{ f := f, α := -1 }, { f := -f, α := -1 }}, ↑Hi.f x ≤ Hi.α
h1 : ↑{ f := f, α := -1 }.f x ≤ { f := f, α := -1 }.α
h2 : ↑{ f := -f, α := -1 }.f x ≤ { f := -f, α := -1 }.α
⊢ False

State before:
case intro.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x✝ : E
hx : x✝ ≠ 0
xhat : E := ‖x✝‖⁻¹ • x✝
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
f : { f // ‖f‖ = 1 } := { val := fval, property := ⋯ }
x : E
h : ∀ Hi ∈ {{ f := f, α := -1 }, { f := -f, α := -1 }}, ↑Hi.f x ≤ Hi.α
h1 : ↑{ f := f, α := -1 }.f x ≤ { f := f, α := -1 }.α
h2 : ↑{ f := -f, α := -1 }.f x ≤ { f := -f, α := -1 }.α
⊢ False
Tactic:
rw [unitSphereDual_neg, ContinuousLinearMap.neg_apply, neg_le, neg_neg] at h2
State after:
case intro.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x✝ : E
hx : x✝ ≠ 0
xhat : E := ‖x✝‖⁻¹ • x✝
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
f : { f // ‖f‖ = 1 } := { val := fval, property := ⋯ }
x : E
h : ∀ Hi ∈ {{ f := f, α := -1 }, { f := -f, α := -1 }}, ↑Hi.f x ≤ Hi.α
h1 : ↑{ f := f, α := -1 }.f x ≤ { f := f, α := -1 }.α
h2 : 1 ≤ ↑f x
⊢ False

State before:
case intro.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x✝ : E
hx : x✝ ≠ 0
xhat : E := ‖x✝‖⁻¹ • x✝
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
f : { f // ‖f‖ = 1 } := { val := fval, property := ⋯ }
x : E
h : ∀ Hi ∈ {{ f := f, α := -1 }, { f := -f, α := -1 }}, ↑Hi.f x ≤ Hi.α
h1 : ↑{ f := f, α := -1 }.f x ≤ { f := f, α := -1 }.α
h2 : 1 ≤ ↑f x
⊢ False
Tactic:
change f.1 x ≤ -1 at h1
State after:
case intro.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x✝ : E
hx : x✝ ≠ 0
xhat : E := ‖x✝‖⁻¹ • x✝
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
f : { f // ‖f‖ = 1 } := { val := fval, property := ⋯ }
x : E
h : ∀ Hi ∈ {{ f := f, α := -1 }, { f := -f, α := -1 }}, ↑Hi.f x ≤ Hi.α
h2 : 1 ≤ ↑f x
h1 : ↑f x ≤ -1
⊢ False

State before:
case intro.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x✝ : E
hx : x✝ ≠ 0
xhat : E := ‖x✝‖⁻¹ • x✝
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
f : { f // ‖f‖ = 1 } := { val := fval, property := ⋯ }
x : E
h : ∀ Hi ∈ {{ f := f, α := -1 }, { f := -f, α := -1 }}, ↑Hi.f x ≤ Hi.α
h2 : 1 ≤ ↑f x
h1 : ↑f x ≤ -1
⊢ False
Tactic:
linarith
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x : E
hx : x ≠ 0
xhat : E := ‖x‖⁻¹ • x
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
⊢ ‖fval‖ = 1
Tactic:
change norm (innerSL ℝ ((norm x)⁻¹ • x)) = 1
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x : E
hx : x ≠ 0
xhat : E := ‖x‖⁻¹ • x
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
⊢ ‖(innerSL ℝ) (‖x‖⁻¹ • x)‖ = 1

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x : E
hx : x ≠ 0
xhat : E := ‖x‖⁻¹ • x
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
⊢ ‖(innerSL ℝ) (‖x‖⁻¹ • x)‖ = 1
Tactic:
have := @norm_smul_inv_norm ℝ _ E _ _ x hx
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x : E
hx : x ≠ 0
xhat : E := ‖x‖⁻¹ • x
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
this : ‖(↑‖x‖)⁻¹ • x‖ = 1
⊢ ‖(innerSL ℝ) (‖x‖⁻¹ • x)‖ = 1

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x : E
hx : x ≠ 0
xhat : E := ‖x‖⁻¹ • x
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
this : ‖(↑‖x‖)⁻¹ • x‖ = 1
⊢ ‖(innerSL ℝ) (‖x‖⁻¹ • x)‖ = 1
Tactic:
rw [IsROrC.ofReal_real_eq_id, id_eq] at this
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x : E
hx : x ≠ 0
xhat : E := ‖x‖⁻¹ • x
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
this : ‖‖x‖⁻¹ • x‖ = 1
⊢ ‖(innerSL ℝ) (‖x‖⁻¹ • x)‖ = 1

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x : E
hx : x ≠ 0
xhat : E := ‖x‖⁻¹ • x
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
this : ‖‖x‖⁻¹ • x‖ = 1
⊢ ‖(innerSL ℝ) (‖x‖⁻¹ • x)‖ = 1
Tactic:
rw [innerSL_apply_norm, this]
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x : E
hx : x ≠ 0
xhat : E := ‖x‖⁻¹ • x
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
f : { f // ‖f‖ = 1 } := { val := fval, property := ⋯ }
⊢ Set.Finite {{ f := f, α := -1 }, { f := -f, α := -1 }}
Tactic:
simp only [Set.mem_singleton_iff, Halfspace.mk.injEq, Set.finite_singleton, Set.Finite.insert]
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x✝ : E
hx : x✝ ≠ 0
xhat : E := ‖x✝‖⁻¹ • x✝
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
f : { f // ‖f‖ = 1 } := { val := fval, property := ⋯ }
x : E
h : ∀ Hi ∈ {{ f := f, α := -1 }, { f := -f, α := -1 }}, ↑Hi.f x ≤ Hi.α
⊢ { f := f, α := -1 } ∈ {{ f := f, α := -1 }, { f := -f, α := -1 }}
Tactic:
simp
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x✝ : E
hx : x✝ ≠ 0
xhat : E := ‖x✝‖⁻¹ • x✝
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
f : { f // ‖f‖ = 1 } := { val := fval, property := ⋯ }
x : E
h : ∀ Hi ∈ {{ f := f, α := -1 }, { f := -f, α := -1 }}, ↑Hi.f x ≤ Hi.α
h1 : ↑{ f := f, α := -1 }.f x ≤ { f := f, α := -1 }.α
⊢ { f := -f, α := -1 } ∈ {{ f := f, α := -1 }, { f := -f, α := -1 }}
Tactic:
simp
State after:
no goals