[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
x✝¹ : E
x✝ : x✝¹ ∈ s
⊢ ‖↑(↑B x✝¹) 0‖ ≤ 1
[PROOFSTEP]
simp only [map_zero, norm_zero, zero_le_one]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
⊢ polar B s = ⋂ (x : E) (_ : x ∈ s), {y | ‖↑(↑B x) y‖ ≤ 1}
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
x✝ : F
⊢ x✝ ∈ polar B s ↔ x✝ ∈ ⋂ (x : E) (_ : x ∈ s), {y | ‖↑(↑B x) y‖ ≤ 1}
[PROOFSTEP]
simp only [polar_mem_iff, Set.mem_iInter, Set.mem_setOf_eq]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
⊢ polar B {0} = Set.univ
[PROOFSTEP]
refine' Set.eq_univ_iff_forall.mpr fun y x hx => _
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
y : F
x : E
hx : x ∈ {0}
⊢ ‖↑(↑B x) y‖ ≤ 1
[PROOFSTEP]
rw [Set.mem_singleton_iff.mp hx, map_zero, LinearMap.zero_apply, norm_zero]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
y : F
x : E
hx : x ∈ {0}
⊢ 0 ≤ 1
[PROOFSTEP]
exact zero_le_one
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
x : E
hx : x ∈ s
y : F
hy : y ∈ polar B s
⊢ ‖↑(↑(flip B) y) x‖ ≤ 1
[PROOFSTEP]
rw [B.flip_apply]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
x : E
hx : x ∈ s
y : F
hy : y ∈ polar B s
⊢ ‖↑(↑B x) y‖ ≤ 1
[PROOFSTEP]
exact hy x hx
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
⊢ IsClosed (polar B s)
[PROOFSTEP]
rw [polar_eq_iInter]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
⊢ IsClosed (⋂ (x : E) (_ : x ∈ s), {y | ‖↑(↑B x) y‖ ≤ 1})
[PROOFSTEP]
refine' isClosed_iInter fun x => isClosed_iInter fun _ => _
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
x : E
x✝ : x ∈ s
⊢ IsClosed {y | ‖↑(↑B x) y‖ ≤ 1}
[PROOFSTEP]
exact isClosed_le (WeakBilin.eval_continuous B.flip x).norm continuous_const
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : SeparatingRight B
⊢ polar B Set.univ = {0}
[PROOFSTEP]
rw [Set.eq_singleton_iff_unique_mem]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : SeparatingRight B
⊢ 0 ∈ polar B Set.univ ∧ ∀ (x : F), x ∈ polar B Set.univ → x = 0
[PROOFSTEP]
refine' ⟨by simp only [zero_mem_polar], fun y hy => h _ fun x => _⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : SeparatingRight B
⊢ 0 ∈ polar B Set.univ
[PROOFSTEP]
simp only [zero_mem_polar]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : SeparatingRight B
y : F
hy : y ∈ polar B Set.univ
x : E
⊢ ↑(↑B x) y = 0
[PROOFSTEP]
refine' norm_le_zero_iff.mp (le_of_forall_le_of_dense fun ε hε => _)
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : SeparatingRight B
y : F
hy : y ∈ polar B Set.univ
x : E
ε : ℝ
hε : 0 < ε
⊢ ‖↑(↑B x) y‖ ≤ ε
[PROOFSTEP]
rcases NormedField.exists_norm_lt 𝕜 hε with ⟨c, hc, hcε⟩
[GOAL]
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : SeparatingRight B
y : F
hy : y ∈ polar B Set.univ
x : E
ε : ℝ
hε : 0 < ε
c : 𝕜
hc : 0 < ‖c‖
hcε : ‖c‖ < ε
⊢ ‖↑(↑B x) y‖ ≤ ε
[PROOFSTEP]
calc
  ‖B x y‖ = ‖c‖ * ‖B (c⁻¹ • x) y‖ := by
    rw [B.map_smul, LinearMap.smul_apply, Algebra.id.smul_eq_mul, norm_mul, norm_inv, mul_inv_cancel_left₀ hc.ne']
  _ ≤ ε * 1 := by gcongr; exact hy _ trivial
  _ = ε := mul_one _
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : SeparatingRight B
y : F
hy : y ∈ polar B Set.univ
x : E
ε : ℝ
hε : 0 < ε
c : 𝕜
hc : 0 < ‖c‖
hcε : ‖c‖ < ε
⊢ ‖↑(↑B x) y‖ = ‖c‖ * ‖↑(↑B (c⁻¹ • x)) y‖
[PROOFSTEP]
rw [B.map_smul, LinearMap.smul_apply, Algebra.id.smul_eq_mul, norm_mul, norm_inv, mul_inv_cancel_left₀ hc.ne']
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : SeparatingRight B
y : F
hy : y ∈ polar B Set.univ
x : E
ε : ℝ
hε : 0 < ε
c : 𝕜
hc : 0 < ‖c‖
hcε : ‖c‖ < ε
⊢ ‖c‖ * ‖↑(↑B (c⁻¹ • x)) y‖ ≤ ε * 1
[PROOFSTEP]
gcongr
[GOAL]
case h₂
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : SeparatingRight B
y : F
hy : y ∈ polar B Set.univ
x : E
ε : ℝ
hε : 0 < ε
c : 𝕜
hc : 0 < ‖c‖
hcε : ‖c‖ < ε
⊢ ‖↑(↑B (c⁻¹ • x)) y‖ ≤ 1
[PROOFSTEP]
exact hy _ trivial
