case intro.intro
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ ↑(↑B u) u
⊢ ∃ C, 0 < C ∧ ∀ (v : V), C * ‖v‖ ≤ ‖↑(continuousLinearMapOfBilin B) v‖
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
⊢ ∃ C, 0 < C ∧ ∀ (v : V), C * ‖v‖ ≤ ‖↑(continuousLinearMapOfBilin B) v‖
rcases coercive with ⟨C, C_ge_0, coercivity⟩
case intro.intro
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ ↑(↑B u) u
⊢ ∀ (v : V), C * ‖v‖ ≤ ‖↑(continuousLinearMapOfBilin B) v‖
case intro.intro
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ ↑(↑B u) u
⊢ ∃ C, 0 < C ∧ ∀ (v : V), C * ‖v‖ ≤ ‖↑(continuousLinearMapOfBilin B) v‖
refine' ⟨C, C_ge_0, _⟩
case intro.intro
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ ↑(↑B u) u
v : V
⊢ C * ‖v‖ ≤ ‖↑(continuousLinearMapOfBilin B) v‖
case intro.intro
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ ↑(↑B u) u
⊢ ∀ (v : V), C * ‖v‖ ≤ ‖↑(continuousLinearMapOfBilin B) v‖
intro v
case pos
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ ↑(↑B u) u
v : V
h : 0 < ‖v‖
⊢ C * ‖v‖ ≤ ‖↑(continuousLinearMapOfBilin B) v‖

case neg
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ ↑(↑B u) u
v : V
h : ¬0 < ‖v‖
⊢ C * ‖v‖ ≤ ‖↑(continuousLinearMapOfBilin B) v‖
case intro.intro
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ ↑(↑B u) u
v : V
⊢ C * ‖v‖ ≤ ‖↑(continuousLinearMapOfBilin B) v‖
by_cases h : 0 < ‖v‖
case pos
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ ↑(↑B u) u
v : V
h : 0 < ‖v‖
⊢ C * ‖v‖ * ‖v‖ ≤ ‖↑(continuousLinearMapOfBilin B) v‖ * ‖v‖
case pos
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ ↑(↑B u) u
v : V
h : 0 < ‖v‖
⊢ C * ‖v‖ ≤ ‖↑(continuousLinearMapOfBilin B) v‖
refine' (mul_le_mul_right h).mp _
no goals
case pos
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ ↑(↑B u) u
v : V
h : 0 < ‖v‖
⊢ C * ‖v‖ * ‖v‖ ≤ ‖↑(continuousLinearMapOfBilin B) v‖ * ‖v‖
calc
  C * ‖v‖ * ‖v‖ ≤ B v v := coercivity v
  _ = ⟪B♯ v, v⟫_ℝ := (continuousLinearMapOfBilin_apply B v v).symm
  _ ≤ ‖B♯ v‖ * ‖v‖ := real_inner_le_norm (B♯ v) v
case neg
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ ↑(↑B u) u
v : V
h : ¬0 < ‖v‖
this : v = 0
⊢ C * ‖v‖ ≤ ‖↑(continuousLinearMapOfBilin B) v‖
case neg
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ ↑(↑B u) u
v : V
h : ¬0 < ‖v‖
⊢ C * ‖v‖ ≤ ‖↑(continuousLinearMapOfBilin B) v‖
have : v = 0 := by simpa using h
no goals
case neg
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ ↑(↑B u) u
v : V
h : ¬0 < ‖v‖
this : v = 0
⊢ C * ‖v‖ ≤ ‖↑(continuousLinearMapOfBilin B) v‖
simp [this]
no goals
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ ↑(↑B u) u
v : V
h : ¬0 < ‖v‖
⊢ v = 0
simpa using h