proposition: Lemma diameter_product_init:forall a b c d alpha n H_mualpha, Is_refining_M ((a,b),(c,d)) -> diameter (product_init ((a,b),(c,d)) alpha n) H_mualpha = (Qabs (a*d - b*c)) * (ub alpha n - lb alpha n) * (Qabs (as_Moebius_Q ((0/1,1/1),(c,d)) (lb alpha n)) * Qabs (as_Moebius_Q ((0/1,1/1),(c,d)) (ub alpha n))).
proof: Proof. intros a b c d alpha n. rewrite product_init_product_init_pure. intros H_mualpha H_mu. assert (H_alpha:=(Is_refining_M_product_init_pure alpha n)). rewrite <- (diameter_product_init_pure alpha n H_alpha). rewrite <- product_init_pure_lb. rewrite <- product_init_pure_ub. transitivity (diameter (product (a, b, (c, d)) (product_init_pure alpha n)) (Is_refining_M_product (a, b, (c, d)) (product_init_pure alpha n) H_mu H_alpha)); [apply diameter_PI|]. rewrite (diameter_product _ _ H_mu H_alpha). repeat apply (f_equal2 Qmult); trivial. Qed.
imports: QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier digits ub LNP_Digit homographic hcorrectness Refining_M Bounded_M Incl_M