[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
⊢ ‖inclusionInDoubleDual 𝕜 E‖ ≤ 1
[PROOFSTEP]
rw [inclusionInDoubleDual_norm_eq]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
⊢ ‖ContinuousLinearMap.id 𝕜 (Dual 𝕜 E)‖ ≤ 1
[PROOFSTEP]
exact ContinuousLinearMap.norm_id_le
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
⊢ ‖↑(inclusionInDoubleDual 𝕜 E) x‖ ≤ ‖x‖
[PROOFSTEP]
simpa using ContinuousLinearMap.le_of_op_norm_le _ (inclusionInDoubleDual_norm_le 𝕜 E) x
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
⊢ LinearMap.SeparatingLeft (dualPairing 𝕜 E)
[PROOFSTEP]
rw [LinearMap.separatingLeft_iff_ker_eq_bot, LinearMap.ker_eq_bot]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
⊢ Function.Injective ↑(dualPairing 𝕜 E)
[PROOFSTEP]
exact ContinuousLinearMap.coe_injective
[GOAL]
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
M : ℝ
hMp : 0 ≤ M
hM : ∀ (f : Dual 𝕜 E), ‖↑f x‖ ≤ M * ‖f‖
⊢ ‖x‖ ≤ M
[PROOFSTEP]
classical
by_cases h : x = 0
· simp only [h, hMp, norm_zero]
· obtain ⟨f, hf₁, hfx⟩ : ∃ f : E →L[𝕜] 𝕜, ‖f‖ = 1 ∧ f x = ‖x‖ := exists_dual_vector 𝕜 x h
  calc
    ‖x‖ = ‖(‖x‖ : 𝕜)‖ := IsROrC.norm_coe_norm.symm
    _ = ‖f x‖ := by rw [hfx]
    _ ≤ M * ‖f‖ := (hM f)
    _ = M := by rw [hf₁, mul_one]
[GOAL]
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
M : ℝ
hMp : 0 ≤ M
hM : ∀ (f : Dual 𝕜 E), ‖↑f x‖ ≤ M * ‖f‖
⊢ ‖x‖ ≤ M
[PROOFSTEP]
by_cases h : x = 0
[GOAL]
case pos
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
M : ℝ
hMp : 0 ≤ M
hM : ∀ (f : Dual 𝕜 E), ‖↑f x‖ ≤ M * ‖f‖
h : x = 0
⊢ ‖x‖ ≤ M
[PROOFSTEP]
simp only [h, hMp, norm_zero]
[GOAL]
case neg
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
M : ℝ
hMp : 0 ≤ M
hM : ∀ (f : Dual 𝕜 E), ‖↑f x‖ ≤ M * ‖f‖
h : ¬x = 0
⊢ ‖x‖ ≤ M
[PROOFSTEP]
obtain ⟨f, hf₁, hfx⟩ : ∃ f : E →L[𝕜] 𝕜, ‖f‖ = 1 ∧ f x = ‖x‖ := exists_dual_vector 𝕜 x h
[GOAL]
case neg.intro.intro
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
M : ℝ
hMp : 0 ≤ M
hM : ∀ (f : Dual 𝕜 E), ‖↑f x‖ ≤ M * ‖f‖
h : ¬x = 0
f : E →L[𝕜] 𝕜
hf₁ : ‖f‖ = 1
hfx : ↑f x = ↑‖x‖
⊢ ‖x‖ ≤ M
[PROOFSTEP]
calc
  ‖x‖ = ‖(‖x‖ : 𝕜)‖ := IsROrC.norm_coe_norm.symm
  _ = ‖f x‖ := by rw [hfx]
  _ ≤ M * ‖f‖ := (hM f)
  _ = M := by rw [hf₁, mul_one]
[GOAL]
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
M : ℝ
hMp : 0 ≤ M
hM : ∀ (f : Dual 𝕜 E), ‖↑f x‖ ≤ M * ‖f‖
h : ¬x = 0
f : E →L[𝕜] 𝕜
hf₁ : ‖f‖ = 1
hfx : ↑f x = ↑‖x‖
⊢ ‖↑‖x‖‖ = ‖↑f x‖
[PROOFSTEP]
rw [hfx]
[GOAL]
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
M : ℝ
hMp : 0 ≤ M
hM : ∀ (f : Dual 𝕜 E), ‖↑f x‖ ≤ M * ‖f‖
h : ¬x = 0
f : E →L[𝕜] 𝕜
hf₁ : ‖f‖ = 1
hfx : ↑f x = ↑‖x‖
⊢ M * ‖f‖ = M
[PROOFSTEP]
rw [hf₁, mul_one]
[GOAL]
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : ∀ (f : Dual 𝕜 E), ↑f x = 0
f : Dual 𝕜 E
⊢ ‖↑f x‖ ≤ 0 * ‖f‖
[PROOFSTEP]
simp [h f]
[GOAL]
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : x = 0
⊢ ∀ (g : Dual 𝕜 E), ↑g x = 0
[PROOFSTEP]
simp [hx]
[GOAL]
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
⊢ x = y ↔ ∀ (g : Dual 𝕜 E), ↑g x = ↑g y
[PROOFSTEP]
rw [← sub_eq_zero, eq_zero_iff_forall_dual_eq_zero 𝕜 (x - y)]
[GOAL]
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
⊢ (∀ (g : Dual 𝕜 E), ↑g (x - y) = 0) ↔ ∀ (g : Dual 𝕜 E), ↑g x = ↑g y
[PROOFSTEP]
simp [sub_eq_zero]
[GOAL]
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
src✝ : E →L[𝕜] Dual 𝕜 (Dual 𝕜 E) := inclusionInDoubleDual 𝕜 E
⊢ ∀ (x : E), ‖↑↑src✝ x‖ = ‖x‖
[PROOFSTEP]
intro x
[GOAL]
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
src✝ : E →L[𝕜] Dual 𝕜 (Dual 𝕜 E) := inclusionInDoubleDual 𝕜 E
x : E
⊢ ‖↑↑src✝ x‖ = ‖x‖
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
src✝ : E →L[𝕜] Dual 𝕜 (Dual 𝕜 E) := inclusionInDoubleDual 𝕜 E
x : E
⊢ ‖↑↑src✝ x‖ ≤ ‖x‖
[PROOFSTEP]
exact double_dual_bound 𝕜 E x
[GOAL]
case a
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
src✝ : E →L[𝕜] Dual 𝕜 (Dual 𝕜 E) := inclusionInDoubleDual 𝕜 E
x : E
⊢ ‖x‖ ≤ ‖↑↑src✝ x‖
[PROOFSTEP]
rw [ContinuousLinearMap.norm_def]
[GOAL]
case a
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
src✝ : E →L[𝕜] Dual 𝕜 (Dual 𝕜 E) := inclusionInDoubleDual 𝕜 E
x : E
⊢ ‖x‖ ≤ sInf {c | 0 ≤ c ∧ ∀ (x_1 : Dual 𝕜 E), ‖↑(↑↑src✝ x) x_1‖ ≤ c * ‖x_1‖}
[PROOFSTEP]
refine' le_csInf ContinuousLinearMap.bounds_nonempty _
[GOAL]
case a
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
src✝ : E →L[𝕜] Dual 𝕜 (Dual 𝕜 E) := inclusionInDoubleDual 𝕜 E
x : E
⊢ ∀ (b : ℝ), b ∈ {c | 0 ≤ c ∧ ∀ (x_1 : Dual 𝕜 E), ‖↑(↑↑src✝ x) x_1‖ ≤ c * ‖x_1‖} → ‖x‖ ≤ b
[PROOFSTEP]
rintro c ⟨hc1, hc2⟩
[GOAL]
case a.intro
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
src✝ : E →L[𝕜] Dual 𝕜 (Dual 𝕜 E) := inclusionInDoubleDual 𝕜 E
x : E
c : ℝ
hc1 : 0 ≤ c
hc2 : ∀ (x_1 : Dual 𝕜 E), ‖↑(↑↑src✝ x) x_1‖ ≤ c * ‖x_1‖
⊢ ‖x‖ ≤ c
[PROOFSTEP]
exact norm_le_dual_bound 𝕜 x hc1 hc2
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ IsClosed (polar 𝕜 s)
[PROOFSTEP]
dsimp only [NormedSpace.polar]
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ IsClosed (LinearMap.polar (LinearMap.flip (dualPairing 𝕜 E)) s)
[PROOFSTEP]
simp only [LinearMap.polar_eq_iInter, LinearMap.flip_apply]
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ IsClosed (⋂ (x : E) (_ : x ∈ s), {y | ‖↑(↑(dualPairing 𝕜 E) y) x‖ ≤ 1})
[PROOFSTEP]
refine' isClosed_biInter fun z _ => _
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
z : E
x✝ : z ∈ s
⊢ IsClosed {y | ‖↑(↑(dualPairing 𝕜 E) y) z‖ ≤ 1}
[PROOFSTEP]
exact isClosed_Iic.preimage (ContinuousLinearMap.apply 𝕜 𝕜 z).continuous.norm
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ IsClosed
    ((LinearMap.polar (LinearMap.flip (LinearMap.flip (dualPairing 𝕜 E))) ∘ ↑OrderDual.ofDual)
      (LinearMap.polar (LinearMap.flip (dualPairing 𝕜 E)) s))
[PROOFSTEP]
simpa [LinearMap.flip_flip] using (isClosed_polar _ _).preimage (inclusionInDoubleDual 𝕜 E).continuous
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : Dual 𝕜 E
c : 𝕜
hc : ∀ (z : E), z ∈ s → ‖↑x' z‖ ≤ ‖c‖
⊢ c⁻¹ • x' ∈ polar 𝕜 s
[PROOFSTEP]
by_cases c_zero : c = 0
[GOAL]
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : Dual 𝕜 E
c : 𝕜
hc : ∀ (z : E), z ∈ s → ‖↑x' z‖ ≤ ‖c‖
c_zero : c = 0
⊢ c⁻¹ • x' ∈ polar 𝕜 s
[PROOFSTEP]
simp only [c_zero, inv_zero, zero_smul]
[GOAL]
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : Dual 𝕜 E
c : 𝕜
hc : ∀ (z : E), z ∈ s → ‖↑x' z‖ ≤ ‖c‖
c_zero : c = 0
⊢ 0 ∈ polar 𝕜 s
[PROOFSTEP]
exact (dualPairing 𝕜 E).flip.zero_mem_polar _
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : Dual 𝕜 E
c : 𝕜
hc : ∀ (z : E), z ∈ s → ‖↑x' z‖ ≤ ‖c‖
c_zero : ¬c = 0
⊢ c⁻¹ • x' ∈ polar 𝕜 s
[PROOFSTEP]
have eq : ∀ z, ‖c⁻¹ • x' z‖ = ‖c⁻¹‖ * ‖x' z‖ := fun z => norm_smul c⁻¹ _
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : Dual 𝕜 E
c : 𝕜
hc : ∀ (z : E), z ∈ s → ‖↑x' z‖ ≤ ‖c‖
c_zero : ¬c = 0
eq : ∀ (z : E), ‖c⁻¹ • ↑x' z‖ = ‖c⁻¹‖ * ‖↑x' z‖
⊢ c⁻¹ • x' ∈ polar 𝕜 s
[PROOFSTEP]
have le : ∀ z, z ∈ s → ‖c⁻¹ • x' z‖ ≤ ‖c⁻¹‖ * ‖c‖ := by
  intro z hzs
  rw [eq z]
  apply mul_le_mul (le_of_eq rfl) (hc z hzs) (norm_nonneg _) (norm_nonneg _)
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : Dual 𝕜 E
c : 𝕜
hc : ∀ (z : E), z ∈ s → ‖↑x' z‖ ≤ ‖c‖
c_zero : ¬c = 0
eq : ∀ (z : E), ‖c⁻¹ • ↑x' z‖ = ‖c⁻¹‖ * ‖↑x' z‖
⊢ ∀ (z : E), z ∈ s → ‖c⁻¹ • ↑x' z‖ ≤ ‖c⁻¹‖ * ‖c‖
[PROOFSTEP]
intro z hzs
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : Dual 𝕜 E
c : 𝕜
hc : ∀ (z : E), z ∈ s → ‖↑x' z‖ ≤ ‖c‖
c_zero : ¬c = 0
eq : ∀ (z : E), ‖c⁻¹ • ↑x' z‖ = ‖c⁻¹‖ * ‖↑x' z‖
z : E
hzs : z ∈ s
⊢ ‖c⁻¹ • ↑x' z‖ ≤ ‖c⁻¹‖ * ‖c‖
[PROOFSTEP]
rw [eq z]
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : Dual 𝕜 E
c : 𝕜
hc : ∀ (z : E), z ∈ s → ‖↑x' z‖ ≤ ‖c‖
c_zero : ¬c = 0
eq : ∀ (z : E), ‖c⁻¹ • ↑x' z‖ = ‖c⁻¹‖ * ‖↑x' z‖
z : E
hzs : z ∈ s
⊢ ‖c⁻¹‖ * ‖↑x' z‖ ≤ ‖c⁻¹‖ * ‖c‖
[PROOFSTEP]
apply mul_le_mul (le_of_eq rfl) (hc z hzs) (norm_nonneg _) (norm_nonneg _)
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : Dual 𝕜 E
c : 𝕜
hc : ∀ (z : E), z ∈ s → ‖↑x' z‖ ≤ ‖c‖
c_zero : ¬c = 0
eq : ∀ (z : E), ‖c⁻¹ • ↑x' z‖ = ‖c⁻¹‖ * ‖↑x' z‖
le : ∀ (z : E), z ∈ s → ‖c⁻¹ • ↑x' z‖ ≤ ‖c⁻¹‖ * ‖c‖
⊢ c⁻¹ • x' ∈ polar 𝕜 s
[PROOFSTEP]
have cancel : ‖c⁻¹‖ * ‖c‖ = 1 := by simp only [c_zero, norm_eq_zero, Ne.def, not_false_iff, inv_mul_cancel, norm_inv]
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : Dual 𝕜 E
c : 𝕜
hc : ∀ (z : E), z ∈ s → ‖↑x' z‖ ≤ ‖c‖
c_zero : ¬c = 0
eq : ∀ (z : E), ‖c⁻¹ • ↑x' z‖ = ‖c⁻¹‖ * ‖↑x' z‖
le : ∀ (z : E), z ∈ s → ‖c⁻¹ • ↑x' z‖ ≤ ‖c⁻¹‖ * ‖c‖
⊢ ‖c⁻¹‖ * ‖c‖ = 1
[PROOFSTEP]
simp only [c_zero, norm_eq_zero, Ne.def, not_false_iff, inv_mul_cancel, norm_inv]
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : Dual 𝕜 E
c : 𝕜
hc : ∀ (z : E), z ∈ s → ‖↑x' z‖ ≤ ‖c‖
c_zero : ¬c = 0
eq : ∀ (z : E), ‖c⁻¹ • ↑x' z‖ = ‖c⁻¹‖ * ‖↑x' z‖
le : ∀ (z : E), z ∈ s → ‖c⁻¹ • ↑x' z‖ ≤ ‖c⁻¹‖ * ‖c‖
cancel : ‖c⁻¹‖ * ‖c‖ = 1
⊢ c⁻¹ • x' ∈ polar 𝕜 s
[PROOFSTEP]
rwa [cancel] at le 
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
r : ℝ
hr : 0 < r
⊢ polar 𝕜 (ball 0 r) ⊆ closedBall 0 (‖c‖ / r)
[PROOFSTEP]
intro x' hx'
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
r : ℝ
hr : 0 < r
x' : Dual 𝕜 E
hx' : x' ∈ polar 𝕜 (ball 0 r)
⊢ x' ∈ closedBall 0 (‖c‖ / r)
[PROOFSTEP]
rw [mem_polar_iff] at hx' 
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
r : ℝ
hr : 0 < r
x' : Dual 𝕜 E
hx' : ∀ (z : E), z ∈ ball 0 r → ‖↑x' z‖ ≤ 1
⊢ x' ∈ closedBall 0 (‖c‖ / r)
[PROOFSTEP]
simp only [polar, mem_setOf, mem_closedBall_zero_iff, mem_ball_zero_iff] at *
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
r : ℝ
hr : 0 < r
x' : Dual 𝕜 E
hx' : ∀ (z : E), ‖z‖ < r → ‖↑x' z‖ ≤ 1
⊢ ‖x'‖ ≤ ‖c‖ / r
[PROOFSTEP]
have hcr : 0 < ‖c‖ / r := div_pos (zero_lt_one.trans hc) hr
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
r : ℝ
hr : 0 < r
x' : Dual 𝕜 E
hx' : ∀ (z : E), ‖z‖ < r → ‖↑x' z‖ ≤ 1
hcr : 0 < ‖c‖ / r
⊢ ‖x'‖ ≤ ‖c‖ / r
[PROOFSTEP]
refine' ContinuousLinearMap.op_norm_le_of_shell hr hcr.le hc fun x h₁ h₂ => _
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
r : ℝ
hr : 0 < r
x' : Dual 𝕜 E
hx' : ∀ (z : E), ‖z‖ < r → ‖↑x' z‖ ≤ 1
hcr : 0 < ‖c‖ / r
x : E
h₁ : r / ‖c‖ ≤ ‖x‖
h₂ : ‖x‖ < r
⊢ ‖↑x' x‖ ≤ ‖c‖ / r * ‖x‖
[PROOFSTEP]
calc
  ‖x' x‖ ≤ 1 := hx' _ h₂
  _ ≤ ‖c‖ / r * ‖x‖ := (inv_pos_le_iff_one_le_mul' hcr).1 (by rwa [inv_div])
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
r : ℝ
hr : 0 < r
x' : Dual 𝕜 E
hx' : ∀ (z : E), ‖z‖ < r → ‖↑x' z‖ ≤ 1
hcr : 0 < ‖c‖ / r
x : E
h₁ : r / ‖c‖ ≤ ‖x‖
h₂ : ‖x‖ < r
⊢ (‖c‖ / r)⁻¹ ≤ ‖x‖
[PROOFSTEP]
rwa [inv_div]
[GOAL]
𝕜✝ : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜✝
E✝ : Type u_2
inst✝⁴ : SeminormedAddCommGroup E✝
inst✝³ : NormedSpace 𝕜✝ E✝
𝕜 : Type u_3
E : Type u_4
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
⊢ polar 𝕜 (closedBall 0 r) = closedBall 0 r⁻¹
[PROOFSTEP]
refine' Subset.antisymm _ (closedBall_inv_subset_polar_closedBall 𝕜)
[GOAL]
𝕜✝ : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜✝
E✝ : Type u_2
inst✝⁴ : SeminormedAddCommGroup E✝
inst✝³ : NormedSpace 𝕜✝ E✝
𝕜 : Type u_3
E : Type u_4
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
⊢ polar 𝕜 (closedBall 0 r) ⊆ closedBall 0 r⁻¹
[PROOFSTEP]
intro x' h
[GOAL]
𝕜✝ : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜✝
E✝ : Type u_2
inst✝⁴ : SeminormedAddCommGroup E✝
inst✝³ : NormedSpace 𝕜✝ E✝
𝕜 : Type u_3
E : Type u_4
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
x' : Dual 𝕜 E
h : x' ∈ polar 𝕜 (closedBall 0 r)
⊢ x' ∈ closedBall 0 r⁻¹
[PROOFSTEP]
simp only [mem_closedBall_zero_iff]
[GOAL]
𝕜✝ : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜✝
E✝ : Type u_2
inst✝⁴ : SeminormedAddCommGroup E✝
inst✝³ : NormedSpace 𝕜✝ E✝
𝕜 : Type u_3
E : Type u_4
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
x' : Dual 𝕜 E
h : x' ∈ polar 𝕜 (closedBall 0 r)
⊢ ‖x'‖ ≤ r⁻¹
[PROOFSTEP]
refine' ContinuousLinearMap.op_norm_le_of_ball hr (inv_nonneg.mpr hr.le) fun z _ => _
[GOAL]
𝕜✝ : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜✝
E✝ : Type u_2
inst✝⁴ : SeminormedAddCommGroup E✝
inst✝³ : NormedSpace 𝕜✝ E✝
𝕜 : Type u_3
E : Type u_4
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
x' : Dual 𝕜 E
h : x' ∈ polar 𝕜 (closedBall 0 r)
z : E
x✝ : z ∈ ball 0 r
⊢ ‖↑x' z‖ ≤ r⁻¹ * ‖z‖
[PROOFSTEP]
simpa only [one_div] using LinearMap.bound_of_ball_bound' hr 1 x'.toLinearMap h z
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
s_nhd : s ∈ 𝓝 0
⊢ Metric.Bounded (polar 𝕜 s)
[PROOFSTEP]
obtain ⟨a, ha⟩ : ∃ a : 𝕜, 1 < ‖a‖ := NormedField.exists_one_lt_norm 𝕜
[GOAL]
case intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
s_nhd : s ∈ 𝓝 0
a : 𝕜
ha : 1 < ‖a‖
⊢ Metric.Bounded (polar 𝕜 s)
[PROOFSTEP]
obtain ⟨r, r_pos, r_ball⟩ : ∃ r : ℝ, 0 < r ∧ ball 0 r ⊆ s := Metric.mem_nhds_iff.1 s_nhd
[GOAL]
case intro.intro.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
s_nhd : s ∈ 𝓝 0
a : 𝕜
ha : 1 < ‖a‖
r : ℝ
r_pos : 0 < r
r_ball : ball 0 r ⊆ s
⊢ Metric.Bounded (polar 𝕜 s)
[PROOFSTEP]
exact
  bounded_closedBall.mono
    (((dualPairing 𝕜 E).flip.polar_antitone r_ball).trans <| polar_ball_subset_closedBall_div ha r_pos)
