Stream: Coq users

Topic: Lax–Milgram theorem

Koundinya Vajjha (Jun 23 2020 at 20:35):

Hello. I was going through this paper (https://hal.inria.fr/hal-01391578/file/article.pdf) on the formal proof of the Lax-Milgram theorem, and came across this line on page 3:
"Note that in practice, we rely on a version of this theorem on CompleteNormedModule, where is_eq can be replaced by the native equality and the phi_distanceable hypothesis can be removed."

Could someone please explain on why this is true?

Koundinya Vajjha (Jun 23 2020 at 20:37):

Relevant definitions are:

Require Import Reals Coquelicot.Coquelicot.

Context {V : CompleteSpace}.
Variable f: V -> V.
Variable phi: V -> Prop.

Hypothesis phi_distanceable:
   forall (x y:V), phi x -> phi y-> exists M, 0 <= M /\ ball x M y.

Definition is_eq:V→V→Prop := fun a b⇒forall eps:posreal,ball a eps b

Koundinya Vajjha (Jun 23 2020 at 20:43):

I'm guessing this has something to do with classical reasoning. In a CompleteNormedModule, one can replace phi_distanceable by exhibiting an explicit M = dist x y where dist is the metric induced by the norm. Have I understood this correctly?

Cyril Cohen (Jun 23 2020 at 21:19):

@Koundinya Vajjha in the paper you are reading,

• is_eq can be read as "arbitrarily closed", which under any separation assumption (from T0) implies equality, in particular normed modules are T2 hence T0 hence is_eq impllies equality...
• indeed phi_distanceable can be removed in normed modules, because the norm being finite implies any two point are at finite distance from each other.

Koundinya Vajjha (Jun 23 2020 at 22:04):

Thank you @Cyril Cohen !

Last updated: Oct 13 2024 at 01:02 UTC