V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))
⊢ range (continuousLinearMapOfBilin B) = ⊤
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
⊢ range (continuousLinearMapOfBilin B) = ⊤
haveI := coercive.closed_range.completeSpace_coe
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))
⊢ (range (continuousLinearMapOfBilin B))ᗮᗮ = ⊤
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))
⊢ range (continuousLinearMapOfBilin B) = ⊤
rw [← (range B♯).orthogonal_orthogonal]
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))
⊢ ∀ (x : V), x ∈ (range (continuousLinearMapOfBilin B))ᗮᗮ
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))
⊢ (range (continuousLinearMapOfBilin B))ᗮᗮ = ⊤
rw [Submodule.eq_top_iff']
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))
v w : V
mem_w_orthogonal : w ∈ (range (continuousLinearMapOfBilin B))ᗮ
⊢ inner w v = 0
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))
⊢ ∀ (x : V), x ∈ (range (continuousLinearMapOfBilin B))ᗮᗮ
intro v w mem_w_orthogonal
case intro.intro
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))
v w : V
mem_w_orthogonal : w ∈ (range (continuousLinearMapOfBilin B))ᗮ
C : ℝ
C_pos : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ ↑(↑B u) u
⊢ inner w v = 0
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))
v w : V
mem_w_orthogonal : w ∈ (range (continuousLinearMapOfBilin B))ᗮ
⊢ inner w v = 0
rcases coercive with ⟨C, C_pos, coercivity⟩
no goals
case intro.intro
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))
v : V
C : ℝ
C_pos : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ ↑(↑B u) u
mem_w_orthogonal : 0 ∈ (range (continuousLinearMapOfBilin B))ᗮ
⊢ inner 0 v = 0
exact inner_zero_left _
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))
v w : V
mem_w_orthogonal : w ∈ (range (continuousLinearMapOfBilin B))ᗮ
C : ℝ
C_pos : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ ↑(↑B u) u
⊢ C * ‖w‖ * ‖w‖ = 0
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))
v w : V
mem_w_orthogonal : w ∈ (range (continuousLinearMapOfBilin B))ᗮ
C : ℝ
C_pos : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ ↑(↑B u) u
⊢ w = 0
rw [← norm_eq_zero, ← mul_self_eq_zero, ← mul_right_inj' C_pos.ne', MulZeroClass.mul_zero, ←
  mul_assoc]
case a
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))
v w : V
mem_w_orthogonal : w ∈ (range (continuousLinearMapOfBilin B))ᗮ
C : ℝ
C_pos : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ ↑(↑B u) u
⊢ C * ‖w‖ * ‖w‖ ≤ 0

case a
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))
v w : V
mem_w_orthogonal : w ∈ (range (continuousLinearMapOfBilin B))ᗮ
C : ℝ
C_pos : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ ↑(↑B u) u
⊢ 0 ≤ C * ‖w‖ * ‖w‖
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))
v w : V
mem_w_orthogonal : w ∈ (range (continuousLinearMapOfBilin B))ᗮ
C : ℝ
C_pos : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ ↑(↑B u) u
⊢ C * ‖w‖ * ‖w‖ = 0
apply le_antisymm
no goals
case a
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))
v w : V
mem_w_orthogonal : w ∈ (range (continuousLinearMapOfBilin B))ᗮ
C : ℝ
C_pos : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ ↑(↑B u) u
⊢ C * ‖w‖ * ‖w‖ ≤ 0
calc
  C * ‖w‖ * ‖w‖ ≤ B w w := coercivity w
  _ = ⟪B♯ w, w⟫_ℝ := (continuousLinearMapOfBilin_apply B w w).symm
  _ = 0 := mem_w_orthogonal _ ⟨w, rfl⟩
no goals
case a
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))
v w : V
mem_w_orthogonal : w ∈ (range (continuousLinearMapOfBilin B))ᗮ
C : ℝ
C_pos : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ ↑(↑B u) u
⊢ 0 ≤ C * ‖w‖ * ‖w‖
exact mul_nonneg (mul_nonneg C_pos.le (norm_nonneg w)) (norm_nonneg w)