English
In the Lax-Milgram setup, the range of the associated bilinear map is the whole space, i.e., the map is surjective onto V.
Русский
В рамках теоремы Лакс–Мильграм диапазон соответствующей билинейной формы является всем пространством; отображение сюръективно на V.
LaTeX
$$$ \mathrm{range}(B♯) = \top, $$$
Lean4
theorem range_eq_top (coercive : IsCoercive B) : range B♯ = ⊤ :=
by
haveI := coercive.isClosed_range.completeSpace_coe
rw [← (range B♯).orthogonal_orthogonal]
rw [Submodule.eq_top_iff']
intro v w mem_w_orthogonal
rcases coercive with ⟨C, C_pos, coercivity⟩
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⟩
· positivity
exact inner_zero_left _
