internlm/Lean-Github huggingface dataset:
Theorem: compact_polarDual_iff
Proof state before:
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
Tactic:
rw [gt_iff_lt, one_div]
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
⊢ 0 < M⁻¹
Theorem: compact_polarDual_iff
Proof state before:
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
⊢ 0 < M⁻¹
Tactic:
exact inv_pos.mpr <| lt_of_lt_of_le (norm_pos_iff.mpr hXnonempty.some_mem.2) (hM hXnonempty.some hXnonempty.some_mem.1)
Proof state after:
no goals
Theorem: compact_polarDual_iff
Proof state before:
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‖
Tactic:
intro b hb
Proof state after:
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 : E
hb : b ∈ (polarDual X)ᶜ
⊢ 1 / M ≤ ‖b‖
Theorem: compact_polarDual_iff
Proof state before:
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 : E
hb : b ∈ (polarDual X)ᶜ
⊢ 1 / M ≤ ‖b‖
Tactic:
rw [Set.mem_compl_iff, mem_polarDual] at hb
Proof state after:
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 : E
hb : ¬∀ x ∈ X, ⟪x, b⟫_ℝ ≤ 1
⊢ 1 / M ≤ ‖b‖
Theorem: compact_polarDual_iff
Proof state before:
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 : E
hb : ¬∀ x ∈ X, ⟪x, b⟫_ℝ ≤ 1
⊢ 1 / M ≤ ‖b‖
Tactic:
push_neg at hb
Proof state after:
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 : E
hb : ∃ x ∈ X, 1 < ⟪x, b⟫_ℝ
⊢ 1 / M ≤ ‖b‖
Theorem: compact_polarDual_iff
Proof state before:
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 : E
hb : ∃ x ∈ X, 1 < ⟪x, b⟫_ℝ
⊢ 1 / M ≤ ‖b‖
Tactic:
rcases hb with ⟨ y, hy, hb ⟩
Proof state after:
case h.refine_2.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
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
⊢ 1 / M ≤ ‖b‖
Theorem: compact_polarDual_iff
Proof state before:
case h.refine_2.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
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
⊢ 1 / M ≤ ‖b‖
Tactic:
specialize hM y hy
Proof state after:
case h.refine_2.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 : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
⊢ 1 / M ≤ ‖b‖
Theorem: compact_polarDual_iff
Proof state before:
case h.refine_2.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 : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
⊢ 1 / M ≤ ‖b‖
Tactic:
have hnorminner: |inner y b| ≤ ‖y‖ * ‖b‖ := by
  exact abs_real_inner_le_norm y b
Proof state after:
case h.refine_2.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 : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
hnorminner : |⟪y, b⟫_ℝ| ≤ ‖y‖ * ‖b‖
⊢ 1 / M ≤ ‖b‖
Theorem: compact_polarDual_iff
Proof state before:
case h.refine_2.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 : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
hnorminner : |⟪y, b⟫_ℝ| ≤ ‖y‖ * ‖b‖
⊢ 1 / M ≤ ‖b‖
Tactic:
rw [abs_of_pos (lt_trans zero_lt_one hb)] at hnorminner
Proof state after:
case h.refine_2.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 : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
hnorminner : ⟪y, b⟫_ℝ ≤ ‖y‖ * ‖b‖
⊢ 1 / M ≤ ‖b‖
Theorem: compact_polarDual_iff
Proof state before:
case h.refine_2.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 : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
hnorminner : ⟪y, b⟫_ℝ ≤ ‖y‖ * ‖b‖
⊢ 1 / M ≤ ‖b‖
Tactic:
have : (1:ℝ) ≤ ‖y‖ * ‖b‖ := le_trans (le_of_lt hb) hnorminner
Proof state after:
case h.refine_2.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 : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
hnorminner : ⟪y, b⟫_ℝ ≤ ‖y‖ * ‖b‖
this : 1 ≤ ‖y‖ * ‖b‖
⊢ 1 / M ≤ ‖b‖
Theorem: compact_polarDual_iff
Proof state before:
case h.refine_2.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 : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
hnorminner : ⟪y, b⟫_ℝ ≤ ‖y‖ * ‖b‖
this : 1 ≤ ‖y‖ * ‖b‖
⊢ 1 / M ≤ ‖b‖
Tactic:
have hynezero: y ≠ 0 := by
  rintro rfl
  rw [norm_zero, zero_mul] at this
  exact not_lt_of_le this zero_lt_one
Proof state after:
case h.refine_2.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 : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
hnorminner : ⟪y, b⟫_ℝ ≤ ‖y‖ * ‖b‖
this : 1 ≤ ‖y‖ * ‖b‖
hynezero : y ≠ 0
⊢ 1 / M ≤ ‖b‖
Theorem: compact_polarDual_iff
Proof state before:
case h.refine_2.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 : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
hnorminner : ⟪y, b⟫_ℝ ≤ ‖y‖ * ‖b‖
this : 1 ≤ ‖y‖ * ‖b‖
hynezero : y ≠ 0
⊢ 1 / M ≤ ‖b‖
Tactic:
rw [← norm_pos_iff] at hynezero
Proof state after:
case h.refine_2.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 : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
hnorminner : ⟪y, b⟫_ℝ ≤ ‖y‖ * ‖b‖
this : 1 ≤ ‖y‖ * ‖b‖
hynezero : 0 < ‖y‖
⊢ 1 / M ≤ ‖b‖
Theorem: compact_polarDual_iff
Proof state before:
case h.refine_2.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 : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
hnorminner : ⟪y, b⟫_ℝ ≤ ‖y‖ * ‖b‖
this : 1 ≤ ‖y‖ * ‖b‖
hynezero : 0 < ‖y‖
⊢ 1 / M ≤ ‖b‖
Tactic:
apply le_trans (div_le_div (le_of_lt <| lt_trans zero_lt_one hb) (le_of_lt hb) hynezero hM)
Proof state after:
case h.refine_2.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 : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
hnorminner : ⟪y, b⟫_ℝ ≤ ‖y‖ * ‖b‖
this : 1 ≤ ‖y‖ * ‖b‖
hynezero : 0 < ‖y‖
⊢ ⟪y, b⟫_ℝ / ‖y‖ ≤ ‖b‖
Theorem: compact_polarDual_iff
Proof state before:
case h.refine_2.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 : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
hnorminner : ⟪y, b⟫_ℝ ≤ ‖y‖ * ‖b‖
this : 1 ≤ ‖y‖ * ‖b‖
hynezero : 0 < ‖y‖
⊢ ⟪y, b⟫_ℝ / ‖y‖ ≤ ‖b‖
Tactic:
apply div_le_of_nonneg_of_le_mul (le_of_lt hynezero)
Proof state after:
case h.refine_2.intro.intro.hc
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 : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
hnorminner : ⟪y, b⟫_ℝ ≤ ‖y‖ * ‖b‖
this : 1 ≤ ‖y‖ * ‖b‖
hynezero : 0 < ‖y‖
⊢ 0 ≤ ‖b‖

case h.refine_2.intro.intro.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 : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
hnorminner : ⟪y, b⟫_ℝ ≤ ‖y‖ * ‖b‖
this : 1 ≤ ‖y‖ * ‖b‖
hynezero : 0 < ‖y‖
⊢ ⟪y, b⟫_ℝ ≤ ‖b‖ * ‖y‖
Theorem: compact_polarDual_iff
Proof state before:
case h.refine_2.intro.intro.hc
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 : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
hnorminner : ⟪y, b⟫_ℝ ≤ ‖y‖ * ‖b‖
this : 1 ≤ ‖y‖ * ‖b‖
hynezero : 0 < ‖y‖
⊢ 0 ≤ ‖b‖

case h.refine_2.intro.intro.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 : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
hnorminner : ⟪y, b⟫_ℝ ≤ ‖y‖ * ‖b‖
this : 1 ≤ ‖y‖ * ‖b‖
hynezero : 0 < ‖y‖
⊢ ⟪y, b⟫_ℝ ≤ ‖b‖ * ‖y‖
Tactic:
apply (mul_nonneg_iff_of_pos_left hynezero).mp (le_trans (zero_le_one) this)
Proof state after:
case h.refine_2.intro.intro.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 : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
hnorminner : ⟪y, b⟫_ℝ ≤ ‖y‖ * ‖b‖
this : 1 ≤ ‖y‖ * ‖b‖
hynezero : 0 < ‖y‖
⊢ ⟪y, b⟫_ℝ ≤ ‖b‖ * ‖y‖
Theorem: compact_polarDual_iff
Proof state before:
case h.refine_2.intro.intro.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 : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
hnorminner : ⟪y, b⟫_ℝ ≤ ‖y‖ * ‖b‖
this : 1 ≤ ‖y‖ * ‖b‖
hynezero : 0 < ‖y‖
⊢ ⟪y, b⟫_ℝ ≤ ‖b‖ * ‖y‖
Tactic:
rw [mul_comm]
Proof state after:
case h.refine_2.intro.intro.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 : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
hnorminner : ⟪y, b⟫_ℝ ≤ ‖y‖ * ‖b‖
this : 1 ≤ ‖y‖ * ‖b‖
hynezero : 0 < ‖y‖
⊢ ⟪y, b⟫_ℝ ≤ ‖y‖ * ‖b‖
Theorem: compact_polarDual_iff
Proof state before:
case h.refine_2.intro.intro.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 : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
hnorminner : ⟪y, b⟫_ℝ ≤ ‖y‖ * ‖b‖
this : 1 ≤ ‖y‖ * ‖b‖
hynezero : 0 < ‖y‖
⊢ ⟪y, b⟫_ℝ ≤ ‖y‖ * ‖b‖
Tactic:
exact hnorminner
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})
left✝ : IsClosed X
M : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
⊢ |⟪y, b⟫_ℝ| ≤ ‖y‖ * ‖b‖
Tactic:
exact abs_real_inner_le_norm y b
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})
left✝ : IsClosed X
M : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
hnorminner : ⟪y, b⟫_ℝ ≤ ‖y‖ * ‖b‖
this : 1 ≤ ‖y‖ * ‖b‖
⊢ y ≠ 0
Tactic:
rintro rfl
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})
left✝ : IsClosed X
M : ℝ
b : E
hy : 0 ∈ X
hb : 1 < ⟪0, b⟫_ℝ
hM : ‖0‖ ≤ M
hnorminner : ⟪0, b⟫_ℝ ≤ ‖0‖ * ‖b‖
this : 1 ≤ ‖0‖ * ‖b‖
⊢ False
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})
left✝ : IsClosed X
M : ℝ
b : E
hy : 0 ∈ X
hb : 1 < ⟪0, b⟫_ℝ
hM : ‖0‖ ≤ M
hnorminner : ⟪0, b⟫_ℝ ≤ ‖0‖ * ‖b‖
this : 1 ≤ ‖0‖ * ‖b‖
⊢ False
Tactic:
rw [norm_zero, zero_mul] at this
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})
left✝ : IsClosed X
M : ℝ
b : E
hy : 0 ∈ X
hb : 1 < ⟪0, b⟫_ℝ
hM : ‖0‖ ≤ M
hnorminner : ⟪0, b⟫_ℝ ≤ ‖0‖ * ‖b‖
this : 1 ≤ 0
⊢ False
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})
left✝ : IsClosed X
M : ℝ
b : E
hy : 0 ∈ X
hb : 1 < ⟪0, b⟫_ℝ
hM : ‖0‖ ≤ M
hnorminner : ⟪0, b⟫_ℝ ≤ ‖0‖ * ‖b‖
this : 1 ≤ 0
⊢ False
Tactic:
exact not_lt_of_le this zero_lt_one
Proof state after:
no goals
Theorem: compact_polarDual_iff
Proof state before:
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
Tactic:
rw [Set.not_nonempty_iff_eq_empty, Set.diff_eq_empty, Set.subset_singleton_iff_eq] at hXempty
Proof state after:
case inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXempty : X = ∅ ∨ X = {0}
⊢ 0 ∈ interior (polarDual X) ↔ IsCompact X
Theorem: compact_polarDual_iff
Proof state before:
case inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXempty : X = ∅ ∨ X = {0}
⊢ 0 ∈ interior (polarDual X) ↔ IsCompact X
Tactic:
cases' hXempty with hXempty hX0
Proof state after:
case inr.inl
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXempty : X = ∅
⊢ 0 ∈ interior (polarDual X) ↔ IsCompact X

case inr.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hX0 : X = {0}
⊢ 0 ∈ interior (polarDual X) ↔ IsCompact X
Theorem: compact_polarDual_iff
Proof state before:
case inr.inl
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXempty : X = ∅
⊢ 0 ∈ interior (polarDual X) ↔ IsCompact X
Tactic:
rw [hXempty, polarDual_empty, interior_univ]
Proof state after:
case inr.inl
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXempty : X = ∅
⊢ 0 ∈ Set.univ ↔ IsCompact ∅
Theorem: compact_polarDual_iff
Proof state before:
case inr.inl
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXempty : X = ∅
⊢ 0 ∈ Set.univ ↔ IsCompact ∅
Tactic:
exact ⟨ fun _ => isCompact_empty, fun _ => trivial ⟩
Proof state after:
no goals
Theorem: compact_polarDual_iff
Proof state before:
case inr.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hX0 : X = {0}
⊢ 0 ∈ interior (polarDual X) ↔ IsCompact X
Tactic:
rw [hX0, polarDual_zero, interior_univ]
Proof state after:
case inr.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hX0 : X = {0}
⊢ 0 ∈ Set.univ ↔ IsCompact {0}
Theorem: compact_polarDual_iff
Proof state before:
case inr.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hX0 : X = {0}
⊢ 0 ∈ Set.univ ↔ IsCompact {0}
Tactic:
exact ⟨ fun _ => isCompact_singleton, fun _ => trivial ⟩
Proof state after:
no goals
Theorem: polarDual_compact_if
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXcv : Convex ℝ X
⊢ 0 ∈ interior X → IsCompact (polarDual X)
Tactic:
intro h
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXcv : Convex ℝ X
h : 0 ∈ interior X
⊢ IsCompact (polarDual X)
Theorem: polarDual_compact_if
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXcv : Convex ℝ X
h : 0 ∈ interior X
⊢ IsCompact (polarDual X)
Tactic:
rw [← doublePolarDual_self hXcl hXcv (interior_subset h), compact_polarDual_iff (polarDual_closed _)] at h
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXcv : Convex ℝ X
h : IsCompact (polarDual X)
⊢ IsCompact (polarDual X)
Theorem: polarDual_compact_if
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXcv : Convex ℝ X
h : IsCompact (polarDual X)
⊢ IsCompact (polarDual X)
Tactic:
exact h
Proof state after:
no goals
Theorem: TrussDesign.hminₚ_pos
Proof state before:
hmin hmax : ℝ
hmin_pos : 0 < hmin
hmin_le_hmax : hmin ≤ hmax
wmin wmax : ℝ
wmin_pos : 0 < wmin
wmin_le_wmax : wmin ≤ wmax
Rmax σ F₁ F₂ : ℝ
⊢ 0 < hminₚ
Tactic:
unfold hminₚ
Proof state after:
hmin hmax : ℝ
hmin_pos : 0 < hmin
hmin_le_hmax : hmin ≤ hmax
wmin wmax : ℝ
wmin_pos : 0 < wmin
wmin_le_wmax : wmin ≤ wmax
Rmax σ F₁ F₂ : ℝ
⊢ 0 < 1
Theorem: TrussDesign.hminₚ_pos
Proof state before:
hmin hmax : ℝ
hmin_pos : 0 < hmin
hmin_le_hmax : hmin ≤ hmax
wmin wmax : ℝ
wmin_pos : 0 < wmin
wmin_le_wmax : wmin ≤ wmax
Rmax σ F₁ F₂ : ℝ
⊢ 0 < 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: TrussDesign.hminₚ_le_hmaxₚ
Proof state before:
hmin hmax : ℝ
hmin_pos : 0 < hmin
hmin_le_hmax : hmin ≤ hmax
wmin wmax : ℝ
wmin_pos : 0 < wmin
wmin_le_wmax : wmin ≤ wmax
Rmax σ F₁ F₂ : ℝ
⊢ hminₚ ≤ hmaxₚ
Tactic:
unfold hminₚ hmaxₚ
Proof state after:
hmin hmax : ℝ
hmin_pos : 0 < hmin
hmin_le_hmax : hmin ≤ hmax
wmin wmax : ℝ
wmin_pos : 0 < wmin
wmin_le_wmax : wmin ≤ wmax
Rmax σ F₁ F₂ : ℝ
⊢ 1 ≤ 100
Theorem: TrussDesign.hminₚ_le_hmaxₚ
Proof state before:
hmin hmax : ℝ
hmin_pos : 0 < hmin
hmin_le_hmax : hmin ≤ hmax
wmin wmax : ℝ
wmin_pos : 0 < wmin
wmin_le_wmax : wmin ≤ wmax
Rmax σ F₁ F₂ : ℝ
⊢ 1 ≤ 100
Tactic:
norm_num
Proof state after:
no goals
Theorem: TrussDesign.wminₚ_pos
Proof state before:
hmin hmax : ℝ
hmin_pos : 0 < hmin
hmin_le_hmax : hmin ≤ hmax
wmin wmax : ℝ
wmin_pos : 0 < wmin
wmin_le_wmax : wmin ≤ wmax
Rmax σ F₁ F₂ : ℝ
⊢ 0 < wminₚ
Tactic:
unfold wminₚ
Proof state after:
hmin hmax : ℝ
hmin_pos : 0 < hmin
hmin_le_hmax : hmin ≤ hmax
wmin wmax : ℝ
wmin_pos : 0 < wmin
wmin_le_wmax : wmin ≤ wmax
Rmax σ F₁ F₂ : ℝ
⊢ 0 < 1
Theorem: TrussDesign.wminₚ_pos
Proof state before:
hmin hmax : ℝ
hmin_pos : 0 < hmin
hmin_le_hmax : hmin ≤ hmax
wmin wmax : ℝ
wmin_pos : 0 < wmin
wmin_le_wmax : wmin ≤ wmax
Rmax σ F₁ F₂ : ℝ
⊢ 0 < 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: TrussDesign.wminₚ_le_wmaxₚ
Proof state before:
hmin hmax : ℝ
hmin_pos : 0 < hmin
hmin_le_hmax : hmin ≤ hmax
wmin wmax : ℝ
wmin_pos : 0 < wmin
wmin_le_wmax : wmin ≤ wmax
Rmax σ F₁ F₂ : ℝ
⊢ wminₚ ≤ wmaxₚ
Tactic:
unfold wminₚ wmaxₚ
Proof state after:
hmin hmax : ℝ
hmin_pos : 0 < hmin
hmin_le_hmax : hmin ≤ hmax
wmin wmax : ℝ
wmin_pos : 0 < wmin
wmin_le_wmax : wmin ≤ wmax
Rmax σ F₁ F₂ : ℝ
⊢ 1 ≤ 100
Theorem: TrussDesign.wminₚ_le_wmaxₚ
Proof state before:
hmin hmax : ℝ
hmin_pos : 0 < hmin
hmin_le_hmax : hmin ≤ hmax
wmin wmax : ℝ
wmin_pos : 0 < wmin
wmin_le_wmax : wmin ≤ wmax
Rmax σ F₁ F₂ : ℝ
⊢ 1 ≤ 100
Tactic:
norm_num
Proof state after:
no goals
Theorem: TrussDesign.Rmaxₚ_pos
Proof state before:
hmin hmax : ℝ
hmin_pos : 0 < hmin
hmin_le_hmax : hmin ≤ hmax
wmin wmax : ℝ
wmin_pos : 0 < wmin
wmin_le_wmax : wmin ≤ wmax
Rmax σ F₁ F₂ : ℝ
⊢ 0 < Rmaxₚ
Tactic:
unfold Rmaxₚ
Proof state after:
hmin hmax : ℝ
hmin_pos : 0 < hmin
hmin_le_hmax : hmin ≤ hmax
wmin wmax : ℝ
wmin_pos : 0 < wmin
wmin_le_wmax : wmin ≤ wmax
Rmax σ F₁ F₂ : ℝ
⊢ 0 < 10
Theorem: TrussDesign.Rmaxₚ_pos
Proof state before:
hmin hmax : ℝ
hmin_pos : 0 < hmin
hmin_le_hmax : hmin ≤ hmax
wmin wmax : ℝ
wmin_pos : 0 < wmin
wmin_le_wmax : wmin ≤ wmax
Rmax σ F₁ F₂ : ℝ
⊢ 0 < 10
Tactic:
norm_num
Proof state after:
no goals
Theorem: TrussDesign.σₚ_pos
Proof state before:
hmin hmax : ℝ
hmin_pos : 0 < hmin
hmin_le_hmax : hmin ≤ hmax
wmin wmax : ℝ
wmin_pos : 0 < wmin
wmin_le_wmax : wmin ≤ wmax
Rmax σ F₁ F₂ : ℝ
⊢ 0 < σₚ
Tactic:
unfold σₚ
Proof state after:
hmin hmax : ℝ
hmin_pos : 0 < hmin
hmin_le_hmax : hmin ≤ hmax
wmin wmax : ℝ
wmin_pos : 0 < wmin
wmin_le_wmax : wmin ≤ wmax
Rmax σ F₁ F₂ : ℝ
⊢ 0 < 0.5