proposition: Lemma Is_refining_M_emits_h_pointwise: forall n mu alpha H_r, let smodu:=semantic_modulus_h mu alpha H_r in n = projT1 smodu -> emits_h mu alpha.
proof: Proof. induction n; intros mu alpha H_r smodu Hn; set (n':=projS1 smodu); set (d:=(proj1_sig (projT2 smodu))); assert (Hn':n'=(projT1 smodu)); trivial; assert (Hd:d=(proj1_sig (projT2 smodu))); trivial; destruct (proj2_sig (projT2 smodu)) as [H1 H3]. simpl in H1. case (Incl_M_dec_D mu LL); intros t_l. constructor 1; trivial. case (Incl_M_dec_D mu RR); intros t_r. constructor 2; trivial. case (Incl_M_dec_D mu MM); intros t_m. constructor 3; trivial. rewrite_all <- Hd; rewrite_all <- Hn'; rewrite_all <- Hn; destruct d; contradiction. rewrite_all <- Hd; rewrite_all <- Hn. generalize (H3 O LL (lt_O_Sn _)); generalize (H3 O RR (lt_O_Sn _)); generalize (H3 O MM (lt_O_Sn _)). simpl; intros t_m t_r t_l. constructor 4; trivial. apply (IHn (product mu (hd alpha)) (tl alpha) (Is_refining_M_product_hd _ _ H_r)). apply eq_add_S. apply (semantic_modulus_h_S_product (S n) (projT1 (semantic_modulus_h (product mu (hd alpha)) (tl alpha) (Is_refining_M_product_hd mu alpha H_r))) mu alpha H_r (Is_refining_M_product_hd _ _ H_r)); trivial. apply lt_O_Sn. Qed.
imports: QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier digits ub LNP_Digit homographic hcorrectness Refining_M Bounded_M Incl_M