proposition: Lemma EVT_max (R : realType) (f : R -> R) (a b : R) : a <= b -> {within `[a, b], continuous f} -> exists2 c, c \in `[a, b]%R & forall t, t \in `[a, b]%R -> f t <= f c.
proof: Proof. move=> leab fcont; set imf := f @` `[a, b]. have imf_sup : has_sup imf. split; first by exists (f a); apply/imageP; rewrite /= in_itv /= lexx. have [M [Mreal imfltM]] : bounded_set (f @` `[a, b]). by apply/compact_bounded/continuous_compact => //; exact: segment_compact. exists (M + 1) => y /imfltM yleM. by rewrite (le_trans _ (yleM _ _)) ?ler_norm ?ltrDl. have [|imf_ltsup] := pselect (exists2 c, c \in `[a, b]%R & f c = sup imf). move=> [c cab fceqsup]; exists c => // t tab; rewrite fceqsup. by apply/sup_upper_bound => //; exact/imageP. have {}imf_ltsup t : t \in `[a, b]%R -> f t < sup imf. move=> tab; case: (ltrP (f t) (sup imf)) => // supleft. rewrite falseE; apply: imf_ltsup; exists t => //; apply/eqP. by rewrite eq_le supleft andbT sup_upper_bound//; exact/imageP. pose g t : R := (sup imf - f t)^-1. have invf_continuous : {within `[a, b], continuous g}. rewrite continuous_subspace_in => t tab; apply: cvgV => //=. by rewrite subr_eq0 gt_eqF // imf_ltsup //; rewrite inE in tab. by apply: cvgD; [exact: cst_continuous | apply: cvgN; exact: (fcont t)]. have /ex_strict_bound_gt0 [k k_gt0 /= imVfltk] : bounded_set (g @` `[a, b]). apply/compact_bounded/continuous_compact; last exact: segment_compact. exact: invf_continuous. have [_ [t tab <-]] : exists2 y, imf y & sup imf - k^-1 < y. by apply: sup_adherent => //; rewrite invr_gt0. rewrite ltrBlDr -ltrBlDl. suff : sup imf - f t > k^-1 by move=> /ltW; rewrite leNgt => /negbTE ->. rewrite -[ltRHS]invrK ltf_pV2// ?qualifE/= ?invr_gt0 ?subr_gt0 ?imf_ltsup//. by rewrite (le_lt_trans (ler_norm _) _) ?imVfltk//; exact: imageP. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum matrix interval) mathcomp(mathcomp_extra boolp classical_sets functions) reals signed topology prodnormedzmodule normedtype landau forms