internlm/Lean-Github huggingface dataset:
Theorem: polarDual_zero
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
⊢ polarDual {0} = Set.univ
Tactic:
rw [polarDual]
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
⊢ ⋂₀ (SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' {0}))) = Set.univ
Theorem: polarDual_zero
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
⊢ ⋂₀ (SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' {0}))) = Set.univ
Tactic:
have : (@Subtype.val E fun p => p ≠ 0) ⁻¹' {0} = ∅ := by
  rw [Set.preimage_singleton_eq_empty]
  simp only [ne_eq, Subtype.range_coe_subtype, Set.mem_setOf_eq, not_true, not_false_eq_true]
  done
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
this : Subtype.val ⁻¹' {0} = ∅
⊢ ⋂₀ (SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' {0}))) = Set.univ
Theorem: polarDual_zero
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
this : Subtype.val ⁻¹' {0} = ∅
⊢ ⋂₀ (SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' {0}))) = Set.univ
Tactic:
rw [this, Set.image_empty, Set.image_empty, Set.sInter_empty]
Proof state after:
no goals
Theorem: polarDual_zero
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
⊢ Subtype.val ⁻¹' {0} = ∅
Tactic:
rw [Set.preimage_singleton_eq_empty]
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
⊢ 0 ∉ Set.range Subtype.val
Theorem: polarDual_zero
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
⊢ 0 ∉ Set.range Subtype.val
Tactic:
simp only [ne_eq, Subtype.range_coe_subtype, Set.mem_setOf_eq, not_true, not_false_eq_true]
Proof state after:
no goals
Theorem: compact_polarDual_iff
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
⊢ 0 ∈ interior (polarDual X) ↔ IsCompact X
Tactic:
cases' (em (X \ {0}).Nonempty) with hXnonempty hXempty
Proof state after:
case inl
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
⊢ 0 ∈ interior (polarDual X) ↔ IsCompact X

case inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXempty : ¬Set.Nonempty (X \ {0})
⊢ 0 ∈ interior (polarDual X) ↔ IsCompact X
Theorem: compact_polarDual_iff
Proof state before:
case inl
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
⊢ 0 ∈ interior (polarDual X) ↔ IsCompact X
Tactic:
constructor <;> rw [Metric.isCompact_iff_isClosed_bounded, isBounded_iff_forall_norm_le]
Proof state after:
case inl.mp
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
⊢ 0 ∈ interior (polarDual X) → IsClosed X ∧ ∃ C, ∀ x ∈ X, ‖x‖ ≤ C

case inl.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
⊢ (IsClosed X ∧ ∃ C, ∀ x ∈ X, ‖x‖ ≤ C) → 0 ∈ interior (polarDual X)
Theorem: compact_polarDual_iff
Proof state before:
case inl.mp
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
⊢ 0 ∈ interior (polarDual X) → IsClosed X ∧ ∃ C, ∀ x ∈ X, ‖x‖ ≤ C
Tactic:
intro h
Proof state after:
case inl.mp
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
h : 0 ∈ interior (polarDual X)
⊢ IsClosed X ∧ ∃ C, ∀ x ∈ X, ‖x‖ ≤ C
Theorem: compact_polarDual_iff
Proof state before:
case inl.mp
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
h : 0 ∈ interior (polarDual X)
⊢ IsClosed X ∧ ∃ C, ∀ x ∈ X, ‖x‖ ≤ C
Tactic:
have : IsOpen (interior (polarDual X)) := isOpen_interior
Proof state after:
case inl.mp
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
h : 0 ∈ interior (polarDual X)
this : IsOpen (interior (polarDual X))
⊢ IsClosed X ∧ ∃ C, ∀ x ∈ X, ‖x‖ ≤ C
Theorem: compact_polarDual_iff
Proof state before:
case inl.mp
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
h : 0 ∈ interior (polarDual X)
this : IsOpen (interior (polarDual X))
⊢ IsClosed X ∧ ∃ C, ∀ x ∈ X, ‖x‖ ≤ C
Tactic:
rw [Metric.isOpen_iff] at this
Proof state after:
case inl.mp
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
h : 0 ∈ interior (polarDual X)
this : ∀ x ∈ interior (polarDual X), ∃ ε > 0, Metric.ball x ε ⊆ interior (polarDual X)
⊢ IsClosed X ∧ ∃ C, ∀ x ∈ X, ‖x‖ ≤ C
Theorem: compact_polarDual_iff
Proof state before:
case inl.mp
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
h : 0 ∈ interior (polarDual X)
this : ∀ x ∈ interior (polarDual X), ∃ ε > 0, Metric.ball x ε ⊆ interior (polarDual X)
⊢ IsClosed X ∧ ∃ C, ∀ x ∈ X, ‖x‖ ≤ C
Tactic:
rcases this 0 h with ⟨ ε, hε, hball ⟩
Proof state after:
case inl.mp.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
h : 0 ∈ interior (polarDual X)
this : ∀ x ∈ interior (polarDual X), ∃ ε > 0, Metric.ball x ε ⊆ interior (polarDual X)
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
⊢ IsClosed X ∧ ∃ C, ∀ x ∈ X, ‖x‖ ≤ C
Theorem: compact_polarDual_iff
Proof state before:
case inl.mp.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
h : 0 ∈ interior (polarDual X)
this : ∀ x ∈ interior (polarDual X), ∃ ε > 0, Metric.ball x ε ⊆ interior (polarDual X)
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
⊢ IsClosed X ∧ ∃ C, ∀ x ∈ X, ‖x‖ ≤ C
Tactic:
clear this h
Proof state after:
case inl.mp.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
⊢ IsClosed X ∧ ∃ C, ∀ x ∈ X, ‖x‖ ≤ C
Theorem: compact_polarDual_iff
Proof state before:
case inl.mp.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
⊢ IsClosed X ∧ ∃ C, ∀ x ∈ X, ‖x‖ ≤ C
Tactic:
refine ⟨ hXcl, 2/ε, fun x hx => ?_ ⟩
Proof state after:
case inl.mp.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
⊢ ‖x‖ ≤ 2 / ε
Theorem: compact_polarDual_iff
Proof state before:
case inl.mp.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
⊢ ‖x‖ ≤ 2 / ε
Tactic:
cases' em (x = 0) with hx0 hx0
Proof state after:
case inl.mp.intro.intro.inl
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : x = 0
⊢ ‖x‖ ≤ 2 / ε

case inl.mp.intro.intro.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : ¬x = 0
⊢ ‖x‖ ≤ 2 / ε
Theorem: compact_polarDual_iff
Proof state before:
case inl.mp.intro.intro.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : ¬x = 0
⊢ ‖x‖ ≤ 2 / ε
Tactic:
let u : E := (ε/2/(norm x)) • x
Proof state after:
case inl.mp.intro.intro.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : ¬x = 0
u : E := (ε / 2 / ‖x‖) • x
⊢ ‖x‖ ≤ 2 / ε
Theorem: compact_polarDual_iff
Proof state before:
case inl.mp.intro.intro.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : ¬x = 0
u : E := (ε / 2 / ‖x‖) • x
⊢ ‖x‖ ≤ 2 / ε
Tactic:
have hnormu : ‖u‖ = ε/2 := by
  rw [norm_smul, Real.norm_eq_abs, abs_of_pos (div_pos (half_pos hε) (norm_pos_iff.mpr hx0)),
    div_mul_cancel _ (norm_ne_zero_iff.mpr hx0)]
  done
Proof state after:
case inl.mp.intro.intro.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : ¬x = 0
u : E := (ε / 2 / ‖x‖) • x
hnormu : ‖u‖ = ε / 2
⊢ ‖x‖ ≤ 2 / ε
Theorem: compact_polarDual_iff
Proof state before:
case inl.mp.intro.intro.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : ¬x = 0
u : E := (ε / 2 / ‖x‖) • x
hnormu : ‖u‖ = ε / 2
⊢ ‖x‖ ≤ 2 / ε
Tactic:
have hu : u ∈ Metric.ball (0:E) ε := by
  rw [Metric.mem_ball, dist_zero_right, hnormu]
  exact half_lt_self hε
Proof state after:
case inl.mp.intro.intro.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : ¬x = 0
u : E := (ε / 2 / ‖x‖) • x
hnormu : ‖u‖ = ε / 2
hu : u ∈ Metric.ball 0 ε
⊢ ‖x‖ ≤ 2 / ε
Theorem: compact_polarDual_iff
Proof state before:
case inl.mp.intro.intro.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : ¬x = 0
u : E := (ε / 2 / ‖x‖) • x
hnormu : ‖u‖ = ε / 2
hu : u ∈ Metric.ball 0 ε
⊢ ‖x‖ ≤ 2 / ε
Tactic:
have h := interior_subset <| hball hu
Proof state after:
case inl.mp.intro.intro.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : ¬x = 0
u : E := (ε / 2 / ‖x‖) • x
hnormu : ‖u‖ = ε / 2
hu : u ∈ Metric.ball 0 ε
h : u ∈ polarDual X
⊢ ‖x‖ ≤ 2 / ε
Theorem: compact_polarDual_iff
Proof state before:
case inl.mp.intro.intro.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : ¬x = 0
u : E := (ε / 2 / ‖x‖) • x
hnormu : ‖u‖ = ε / 2
hu : u ∈ Metric.ball 0 ε
h : u ∈ polarDual X
⊢ ‖x‖ ≤ 2 / ε
Tactic:
rw [mem_polarDual] at h
Proof state after:
case inl.mp.intro.intro.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : ¬x = 0
u : E := (ε / 2 / ‖x‖) • x
hnormu : ‖u‖ = ε / 2
hu : u ∈ Metric.ball 0 ε
h : ∀ x ∈ X, ⟪x, u⟫_ℝ ≤ 1
⊢ ‖x‖ ≤ 2 / ε
Theorem: compact_polarDual_iff
Proof state before:
case inl.mp.intro.intro.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : ¬x = 0
u : E := (ε / 2 / ‖x‖) • x
hnormu : ‖u‖ = ε / 2
hu : u ∈ Metric.ball 0 ε
h : ∀ x ∈ X, ⟪x, u⟫_ℝ ≤ 1
⊢ ‖x‖ ≤ 2 / ε
Tactic:
specialize h x hx
Proof state after:
case inl.mp.intro.intro.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : ¬x = 0
u : E := (ε / 2 / ‖x‖) • x
hnormu : ‖u‖ = ε / 2
hu : u ∈ Metric.ball 0 ε
h : ⟪x, u⟫_ℝ ≤ 1
⊢ ‖x‖ ≤ 2 / ε
Theorem: compact_polarDual_iff
Proof state before:
case inl.mp.intro.intro.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : ¬x = 0
u : E := (ε / 2 / ‖x‖) • x
hnormu : ‖u‖ = ε / 2
hu : u ∈ Metric.ball 0 ε
h : ⟪x, u⟫_ℝ ≤ 1
⊢ ‖x‖ ≤ 2 / ε
Tactic:
rw [real_inner_smul_right, real_inner_self_eq_norm_mul_norm, ←mul_assoc,
  div_mul_cancel _ (norm_ne_zero_iff.mpr hx0), mul_comm, ← div_le_div_right (div_pos hε zero_lt_two),
  mul_div_cancel _ (Ne.symm <| ne_of_lt (div_pos hε zero_lt_two)), one_div_div] at h
Proof state after:
case inl.mp.intro.intro.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : ¬x = 0
u : E := (ε / 2 / ‖x‖) • x
hnormu : ‖u‖ = ε / 2
hu : u ∈ Metric.ball 0 ε
h : ‖x‖ ≤ 2 / ε
⊢ ‖x‖ ≤ 2 / ε
Theorem: compact_polarDual_iff
Proof state before:
case inl.mp.intro.intro.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : ¬x = 0
u : E := (ε / 2 / ‖x‖) • x
hnormu : ‖u‖ = ε / 2
hu : u ∈ Metric.ball 0 ε
h : ‖x‖ ≤ 2 / ε
⊢ ‖x‖ ≤ 2 / ε
Tactic:
exact h
Proof state after:
no goals
Theorem: compact_polarDual_iff
Proof state before:
case inl.mp.intro.intro.inl
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : x = 0
⊢ ‖x‖ ≤ 2 / ε
Tactic:
rw [hx0, norm_zero]
Proof state after:
case inl.mp.intro.intro.inl
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : x = 0
⊢ 0 ≤ 2 / ε
Theorem: compact_polarDual_iff
Proof state before:
case inl.mp.intro.intro.inl
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : x = 0
⊢ 0 ≤ 2 / ε
Tactic:
exact div_nonneg zero_le_two (le_of_lt hε)
Proof state after:
no goals
Theorem: compact_polarDual_iff
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : ¬x = 0
u : E := (ε / 2 / ‖x‖) • x
⊢ ‖u‖ = ε / 2
Tactic:
rw [norm_smul, Real.norm_eq_abs, abs_of_pos (div_pos (half_pos hε) (norm_pos_iff.mpr hx0)),
  div_mul_cancel _ (norm_ne_zero_iff.mpr hx0)]
Proof state after:
no goals
Theorem: compact_polarDual_iff
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : ¬x = 0
u : E := (ε / 2 / ‖x‖) • x
hnormu : ‖u‖ = ε / 2
⊢ u ∈ Metric.ball 0 ε
Tactic:
rw [Metric.mem_ball, dist_zero_right, hnormu]
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : ¬x = 0
u : E := (ε / 2 / ‖x‖) • x
hnormu : ‖u‖ = ε / 2
⊢ ε / 2 < ε
Theorem: compact_polarDual_iff
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : ¬x = 0
u : E := (ε / 2 / ‖x‖) • x
hnormu : ‖u‖ = ε / 2
⊢ ε / 2 < ε
Tactic:
exact half_lt_self hε
Proof state after:
no goals
Theorem: compact_polarDual_iff
Proof state before:
case inl.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
⊢ (IsClosed X ∧ ∃ C, ∀ x ∈ X, ‖x‖ ≤ C) → 0 ∈ interior (polarDual X)
Tactic:
rw [interior_eq_compl_closure_compl, Set.mem_compl_iff, Metric.mem_closure_iff, dist_zero_left]
Proof state after:
case inl.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
⊢ (IsClosed X ∧ ∃ C, ∀ x ∈ X, ‖x‖ ≤ C) → ¬∀ ε > 0, ∃ b ∈ (polarDual X)ᶜ, ‖b‖ < ε
Theorem: compact_polarDual_iff
Proof state before:
case inl.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
⊢ (IsClosed X ∧ ∃ C, ∀ x ∈ X, ‖x‖ ≤ C) → ¬∀ ε > 0, ∃ b ∈ (polarDual X)ᶜ, ‖b‖ < ε
Tactic:
push_neg
Proof state after:
case inl.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
⊢ (IsClosed X ∧ ∃ C, ∀ x ∈ X, ‖x‖ ≤ C) → ∃ ε > 0, ∀ b ∈ (polarDual X)ᶜ, ε ≤ ‖b‖
Theorem: compact_polarDual_iff
Proof state before:
case inl.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
⊢ (IsClosed X ∧ ∃ C, ∀ x ∈ X, ‖x‖ ≤ C) → ∃ ε > 0, ∀ b ∈ (polarDual X)ᶜ, ε ≤ ‖b‖
Tactic:
intro h
Proof state after:
case inl.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
h : IsClosed X ∧ ∃ C, ∀ x ∈ X, ‖x‖ ≤ C
⊢ ∃ ε > 0, ∀ b ∈ (polarDual X)ᶜ, ε ≤ ‖b‖
Theorem: compact_polarDual_iff
Proof state before:
case inl.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
h : IsClosed X ∧ ∃ C, ∀ x ∈ X, ‖x‖ ≤ C
⊢ ∃ ε > 0, ∀ b ∈ (polarDual X)ᶜ, ε ≤ ‖b‖
Tactic:
rcases h with ⟨ _, M, hM ⟩
Proof state after:
case inl.mpr.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
hM : ∀ x ∈ X, ‖x‖ ≤ M
⊢ ∃ ε > 0, ∀ b ∈ (polarDual X)ᶜ, ε ≤ ‖b‖
Theorem: compact_polarDual_iff
Proof state before:
case inl.mpr.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
hM : ∀ x ∈ X, ‖x‖ ≤ M
⊢ ∃ ε > 0, ∀ b ∈ (polarDual X)ᶜ, ε ≤ ‖b‖
Tactic:
use 1/M
Proof state after:
case h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
hM : ∀ x ∈ X, ‖x‖ ≤ M
⊢ 1 / M > 0 ∧ ∀ b ∈ (polarDual X)ᶜ, 1 / M ≤ ‖b‖
Theorem: compact_polarDual_iff
Proof state before:
case h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
hM : ∀ x ∈ X, ‖x‖ ≤ M
⊢ 1 / M > 0 ∧ ∀ b ∈ (polarDual X)ᶜ, 1 / M ≤ ‖b‖
Tactic:
refine ⟨ ?_, ?_ ⟩
Proof state after:
case h.refine_1
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
hM : ∀ x ∈ X, ‖x‖ ≤ M
⊢ 1 / M > 0

case h.refine_2
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
hM : ∀ x ∈ X, ‖x‖ ≤ M
⊢ ∀ b ∈ (polarDual X)ᶜ, 1 / M ≤ ‖b‖