[GOAL]
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‖
[PROOFSTEP]
rcases coercive with ⟨C, C_ge_0, coercivity⟩
[GOAL]
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‖
[PROOFSTEP]
refine' ⟨C, C_ge_0, _⟩
[GOAL]
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‖
[PROOFSTEP]
intro v
[GOAL]
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‖
[PROOFSTEP]
by_cases h : 0 < ‖v‖
[GOAL]
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‖
[PROOFSTEP]
refine' (mul_le_mul_right h).mp _
[GOAL]
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‖
[PROOFSTEP]
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
[GOAL]
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‖
[PROOFSTEP]
have : v = 0 := by simpa using h
[GOAL]
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
[PROOFSTEP]
simpa using h
[GOAL]
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‖
[PROOFSTEP]
simp [this]
[GOAL]
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
⊢ ∃ C, 0 < C ∧ AntilipschitzWith C ↑(continuousLinearMapOfBilin B)
[PROOFSTEP]
rcases coercive.bounded_below with ⟨C, C_pos, below_bound⟩
[GOAL]
case intro.intro
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
C : ℝ
C_pos : 0 < C
below_bound : ∀ (v : V), C * ‖v‖ ≤ ‖↑(continuousLinearMapOfBilin B) v‖
⊢ ∃ C, 0 < C ∧ AntilipschitzWith C ↑(continuousLinearMapOfBilin B)
[PROOFSTEP]
refine' ⟨C⁻¹.toNNReal, Real.toNNReal_pos.mpr (inv_pos.mpr C_pos), _⟩
[GOAL]
case intro.intro
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
C : ℝ
C_pos : 0 < C
below_bound : ∀ (v : V), C * ‖v‖ ≤ ‖↑(continuousLinearMapOfBilin B) v‖
⊢ AntilipschitzWith (Real.toNNReal C⁻¹) ↑(continuousLinearMapOfBilin B)
[PROOFSTEP]
refine' ContinuousLinearMap.antilipschitz_of_bound B♯ _
[GOAL]
case intro.intro
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
C : ℝ
C_pos : 0 < C
below_bound : ∀ (v : V), C * ‖v‖ ≤ ‖↑(continuousLinearMapOfBilin B) v‖
⊢ ∀ (x : V), ‖x‖ ≤ ↑(Real.toNNReal C⁻¹) * ‖↑(continuousLinearMapOfBilin B) x‖
[PROOFSTEP]
simp_rw [Real.coe_toNNReal', max_eq_left_of_lt (inv_pos.mpr C_pos), ← inv_mul_le_iff (inv_pos.mpr C_pos)]
[GOAL]
case intro.intro
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
C : ℝ
C_pos : 0 < C
below_bound : ∀ (v : V), C * ‖v‖ ≤ ‖↑(continuousLinearMapOfBilin B) v‖
⊢ ∀ (x : V), C⁻¹⁻¹ * ‖x‖ ≤ ‖↑(continuousLinearMapOfBilin B) x‖
[PROOFSTEP]
simpa using below_bound
[GOAL]
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
⊢ ker (continuousLinearMapOfBilin B) = ⊥
[PROOFSTEP]
rw [LinearMapClass.ker_eq_bot]
[GOAL]
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
⊢ Function.Injective ↑(continuousLinearMapOfBilin B)
[PROOFSTEP]
rcases coercive.antilipschitz with ⟨_, _, antilipschitz⟩
[GOAL]
case intro.intro
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
w✝ : ℝ≥0
left✝ : 0 < w✝
antilipschitz : AntilipschitzWith w✝ ↑(continuousLinearMapOfBilin B)
⊢ Function.Injective ↑(continuousLinearMapOfBilin B)
[PROOFSTEP]
exact antilipschitz.injective
[GOAL]
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
⊢ IsClosed ↑(range (continuousLinearMapOfBilin B))
[PROOFSTEP]
rcases coercive.antilipschitz with ⟨_, _, antilipschitz⟩
[GOAL]
case intro.intro
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
w✝ : ℝ≥0
left✝ : 0 < w✝
antilipschitz : AntilipschitzWith w✝ ↑(continuousLinearMapOfBilin B)
⊢ IsClosed ↑(range (continuousLinearMapOfBilin B))
[PROOFSTEP]
exact antilipschitz.isClosed_range B♯.uniformContinuous
[GOAL]
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
⊢ range (continuousLinearMapOfBilin B) = ⊤
[PROOFSTEP]
haveI := coercive.closed_range.completeSpace_coe
[GOAL]
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) = ⊤
[PROOFSTEP]
rw [← (range B♯).orthogonal_orthogonal]
[GOAL]
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))ᗮᗮ = ⊤
[PROOFSTEP]
rw [Submodule.eq_top_iff']
[GOAL]
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))ᗮᗮ
[PROOFSTEP]
intro v w mem_w_orthogonal
[GOAL]
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
[PROOFSTEP]
rcases coercive with ⟨C, C_pos, coercivity⟩
[GOAL]
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
[PROOFSTEP]
obtain rfl : w = 0 :=
  by
  rw [← norm_eq_zero, ← mul_self_eq_zero, ← mul_right_inj' C_pos.ne', mul_zero, ← mul_assoc]
  apply le_antisymm
  ·
    calc
      C * ‖w‖ * ‖w‖ ≤ B w w := coercivity w
      _ = ⟪B♯ w, w⟫_ℝ := (continuousLinearMapOfBilin_apply B w w).symm
      _ = 0 := mem_w_orthogonal _ ⟨w, rfl⟩
  · exact mul_nonneg (mul_nonneg C_pos.le (norm_nonneg w)) (norm_nonneg w)
[GOAL]
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
[PROOFSTEP]
rw [← norm_eq_zero, ← mul_self_eq_zero, ← mul_right_inj' C_pos.ne', mul_zero, ← mul_assoc]
[GOAL]
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
[PROOFSTEP]
apply le_antisymm
[GOAL]
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
[PROOFSTEP]
calc
  C * ‖w‖ * ‖w‖ ≤ B w w := coercivity w
  _ = ⟪B♯ w, w⟫_ℝ := (continuousLinearMapOfBilin_apply B w w).symm
  _ = 0 := mem_w_orthogonal _ ⟨w, rfl⟩
[GOAL]
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‖
[PROOFSTEP]
exact mul_nonneg (mul_nonneg C_pos.le (norm_nonneg w)) (norm_nonneg w)
[GOAL]
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
[PROOFSTEP]
exact inner_zero_left _
