Stream: Coq users

Topic: Lax–Milgram theorem


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Cyril Cohen (Jun 23 2020 at 21:19):

@Koundinya Vajjha in the paper you are reading,

view this post on Zulip Koundinya Vajjha (Jun 23 2020 at 22:04):

Thank you @Cyril Cohen !


Last updated: Oct 05 2023 at 02:01 UTC