proposition: Lemma locally_2d_1d_strong : forall (P : R -> R -> Prop) x y, locally_2d P x y -> locally_2d (fun u v => forall t, 0 <= t <= 1 -> locally t (fun z => locally_2d P (x + z * (u - x)) (y + z * (v - y)))) x y.
proof: Proof. intros P x y. apply locally_2d_align => eps HP u v Hu Hv t Ht. assert (Zm: 0 <= Rmax (Rabs (u - x)) (Rabs (v - y))). apply Rmax_case ; apply Rabs_pos. destruct Zm as [Zm|Zm]. assert (H1: Rmax (Rabs (u - x)) (Rabs (v - y)) < eps). now apply Rmax_case. set (d1 := mkposreal _ (Rlt_Rminus _ _ H1)). assert (H2: 0 < pos_div_2 d1 / Rmax (Rabs (u - x)) (Rabs (v - y))). apply Rmult_lt_0_compat. apply cond_pos. now apply Rinv_0_lt_compat. set (d2 := mkposreal _ H2). exists d2 => z Hz. exists (pos_div_2 d1) => p q Hp Hq. apply HP. replace (p - x) with (p - (x + z * (u - x)) + (z - t + t) * (u - x)) by ring. apply Rle_lt_trans with (1 := Rabs_triang _ _). replace (pos eps) with (pos_div_2 d1 + (eps - pos_div_2 d1)) by ring. apply Rplus_lt_le_compat with (1 := Hp). rewrite Rabs_mult. apply Rle_trans with ((d2 + 1) * Rmax (Rabs (u - x)) (Rabs (v - y))). apply Rmult_le_compat. apply Rabs_pos. apply Rabs_pos. apply Rle_trans with (1 := Rabs_triang _ _). apply Rplus_le_compat. now apply Rlt_le. now rewrite Rabs_pos_eq. apply Rmax_l. rewrite /d2 /d1 /=. field_simplify. apply Rle_refl. now apply Rgt_not_eq. replace (q - y) with (q - (y + z * (v - y)) + (z - t + t) * (v - y)) by ring. apply Rle_lt_trans with (1 := Rabs_triang _ _). replace (pos eps) with (pos_div_2 d1 + (eps - pos_div_2 d1)) by ring. apply Rplus_lt_le_compat with (1 := Hq). rewrite Rabs_mult. apply Rle_trans with ((d2 + 1) * Rmax (Rabs (u - x)) (Rabs (v - y))). apply Rmult_le_compat. apply Rabs_pos. apply Rabs_pos. apply Rle_trans with (1 := Rabs_triang _ _). apply Rplus_le_compat. now apply Rlt_le. now rewrite Rabs_pos_eq. apply Rmax_r. rewrite /d2 /d1 /=. field_simplify. apply Rle_refl. now apply Rgt_not_eq. apply filter_forall => z. exists eps => p q. replace (u - x) with 0. replace (v - y) with 0. rewrite Rmult_0_r 2!Rplus_0_r. apply HP. apply sym_eq. apply Rabs_eq_0. apply Rle_antisym. rewrite Zm. apply Rmax_r. apply Rabs_pos. apply sym_eq. apply Rabs_eq_0. apply Rle_antisym. rewrite Zm. apply Rmax_l. apply Rabs_pos. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub