/
LaxMilgram.lean
125 lines (98 loc) · 4.97 KB
/
LaxMilgram.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
/-
Copyright (c) 2022 Daniel Roca González. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Daniel Roca González
-/
import Mathlib.Analysis.InnerProductSpace.Dual
#align_import analysis.inner_product_space.lax_milgram from "leanprover-community/mathlib"@"46b633fd842bef9469441c0209906f6dddd2b4f5"
/-!
# The Lax-Milgram Theorem
We consider a Hilbert space `V` over `ℝ`
equipped with a bounded bilinear form `B : V →L[ℝ] V →L[ℝ] ℝ`.
Recall that a bilinear form `B : V →L[ℝ] V →L[ℝ] ℝ` is *coercive*
iff `∃ C, (0 < C) ∧ ∀ u, C * ‖u‖ * ‖u‖ ≤ B u u`.
Under the hypothesis that `B` is coercive we prove the Lax-Milgram theorem:
that is, the map `InnerProductSpace.continuousLinearMapOfBilin` from
`Analysis.InnerProductSpace.Dual` can be upgraded to a continuous equivalence
`IsCoercive.continuousLinearEquivOfBilin : V ≃L[ℝ] V`.
## References
* We follow the notes of Peter Howard's Spring 2020 *M612: Partial Differential Equations* lecture,
see[howard]
## Tags
dual, Lax-Milgram
-/
noncomputable section
open RCLike LinearMap ContinuousLinearMap InnerProductSpace
open LinearMap (ker range)
open RealInnerProductSpace NNReal
universe u
namespace IsCoercive
variable {V : Type u} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V]
variable {B : V →L[ℝ] V →L[ℝ] ℝ}
local postfix:1024 "♯" => @continuousLinearMapOfBilin ℝ V _ _ _ _
theorem bounded_below (coercive : IsCoercive B) : ∃ C, 0 < C ∧ ∀ v, C * ‖v‖ ≤ ‖B♯ v‖ := by
rcases coercive with ⟨C, C_ge_0, coercivity⟩
refine' ⟨C, C_ge_0, _⟩
intro v
by_cases h : 0 < ‖v‖
· refine' (mul_le_mul_right h).mp _
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
· have : v = 0 := by simpa using h
simp [this]
#align is_coercive.bounded_below IsCoercive.bounded_below
theorem antilipschitz (coercive : IsCoercive B) : ∃ C : ℝ≥0, 0 < C ∧ AntilipschitzWith C B♯ := by
rcases coercive.bounded_below with ⟨C, C_pos, below_bound⟩
refine' ⟨C⁻¹.toNNReal, Real.toNNReal_pos.mpr (inv_pos.mpr C_pos), _⟩
refine' ContinuousLinearMap.antilipschitz_of_bound B♯ _
simp_rw [Real.coe_toNNReal', max_eq_left_of_lt (inv_pos.mpr C_pos), ←
inv_mul_le_iff (inv_pos.mpr C_pos)]
simpa using below_bound
#align is_coercive.antilipschitz IsCoercive.antilipschitz
theorem ker_eq_bot (coercive : IsCoercive B) : ker B♯ = ⊥ := by
rw [LinearMapClass.ker_eq_bot]
rcases coercive.antilipschitz with ⟨_, _, antilipschitz⟩
exact antilipschitz.injective
#align is_coercive.ker_eq_bot IsCoercive.ker_eq_bot
theorem isClosed_range (coercive : IsCoercive B) : IsClosed (range B♯ : Set V) := by
rcases coercive.antilipschitz with ⟨_, _, antilipschitz⟩
exact antilipschitz.isClosed_range B♯.uniformContinuous
#align is_coercive.closed_range IsCoercive.isClosed_range
@[deprecated] alias closed_range := isClosed_range -- 2024-03-29
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 _
#align is_coercive.range_eq_top IsCoercive.range_eq_top
/-- The Lax-Milgram equivalence of a coercive bounded bilinear operator:
for all `v : V`, `continuousLinearEquivOfBilin B v` is the unique element `V`
such that `continuousLinearEquivOfBilin B v, w⟫ = B v w`.
The Lax-Milgram theorem states that this is a continuous equivalence.
-/
def continuousLinearEquivOfBilin (coercive : IsCoercive B) : V ≃L[ℝ] V :=
ContinuousLinearEquiv.ofBijective B♯ coercive.ker_eq_bot coercive.range_eq_top
#align is_coercive.continuous_linear_equiv_of_bilin IsCoercive.continuousLinearEquivOfBilin
@[simp]
theorem continuousLinearEquivOfBilin_apply (coercive : IsCoercive B) (v w : V) :
⟪coercive.continuousLinearEquivOfBilin v, w⟫_ℝ = B v w :=
continuousLinearMapOfBilin_apply B v w
#align is_coercive.continuous_linear_equiv_of_bilin_apply IsCoercive.continuousLinearEquivOfBilin_apply
theorem unique_continuousLinearEquivOfBilin (coercive : IsCoercive B) {v f : V}
(is_lax_milgram : ∀ w, ⟪f, w⟫_ℝ = B v w) : f = coercive.continuousLinearEquivOfBilin v :=
unique_continuousLinearMapOfBilin B is_lax_milgram
#align is_coercive.unique_continuous_linear_equiv_of_bilin IsCoercive.unique_continuousLinearEquivOfBilin
end IsCoercive