proposition: Lemma bilinear_schwarz (U V' W' : normedModType R) (f : {bilinear U -> V' -> W'}) : continuous (fun p => f p.1 p.2) -> exists2 k, k > 0 & forall u v, `|f u v| <= k * `|u| * `|v|.
proof: Proof. move=> /(_ 0); rewrite /continuous_at linear0r => /(_ _ (nbhsx_ballx _ _ ltr01)). move=> /nbhs_ballP [_ /posnumP[e] he]; exists ((2 / e%:num) ^+2) => // u v. have [|un0] := real_le0P (normr_real u). by rewrite normr_le0 => /eqP->; rewrite linear0l !normr0 mulr0 mul0r. have [|vn0] := real_le0P (normr_real v). by rewrite normr_le0 => /eqP->; rewrite linear0r !normr0 mulr0. rewrite -[`|u|]/((PosNum un0)%:num) -[`|v|]/((PosNum vn0)%:num). set ku := 2 / e%:num * (PosNum un0)%:num. set kv := 2 / e%:num * (PosNum vn0)%:num. rewrite -[X in f X](@scalerKV _ _ ku) /ku // linearZl_LR normrZ. rewrite gtr0_norm // -ler_pdivlMl //. rewrite -[X in f _ X](@scalerKV _ _ kv) /kv // linearZr_LR normrZ. rewrite gtr0_norm // -ler_pdivlMl //. suff /he : ball 0 e%:num (ku^-1 *: u, kv^-1 *: v). rewrite -ball_normE /= distrC subr0 => /ltW /le_trans; apply. rewrite ler_pdivlMl 1?pmulr_lgt0// mulr1 ler_pdivlMl 1?pmulr_lgt0//. by rewrite mulrA [ku * _]mulrAC expr2. rewrite -ball_normE /= distrC subr0. have -> : (ku^-1 *: u, kv^-1 *: v) = (e%:num / 2) *: ((PosNum un0)%:num ^-1 *: u, (PosNum vn0)%:num ^-1 *: v). rewrite invrM ?unitfE // [kv ^-1]invrM ?unitfE //. rewrite mulrC -[_ *: u]scalerA [X in X *: v]mulrC -[_ *: v]scalerA. by rewrite invf_div. rewrite normrZ ger0_norm // -mulrA gtr_pMr // ltr_pdivrMl // mulr1. by rewrite prod_normE/= !normrZ !normfV !normr_id !mulVf ?gt_eqF// maxxx ltr1n. 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