proposition: Theorem homographic_correctness : forall (mu:Matrix) (alpha : Reals) (H : productive_h mu alpha) (r:R), rep alpha r -> rep (homographic mu alpha H) (as_Moebius mu r).
proof: Proof. cofix. intros mu alpha H_productive r Hr_alpha; destruct (homographic_emits_strong mu alpha H_productive) as [n [[ | | ] [H_productive_dropped [H_Incl H_bis]]]]; unfold inv_digit in H_bis; unfold inv_digit; generalize (H_bis H_productive_dropped); clear H_bis; intro H_bis. replace (as_Moebius mu r) with (as_Moebius (product LL (product inv_LL mu)) r); [ idtac | rewrite <- product_inv_L; reflexivity]; replace (product inv_LL mu) with (product inv_LL (product (product_init mu alpha n) (product_init_rev alpha n))); [ idtac | rewrite <- product_init_init_rev_id; trivial]. assert (H_base:(-1 <= as_Moebius (product inv_LL (product (product_init mu alpha n) (product_init_rev alpha n))) r <= 1)%R). rewrite product_associative. rewrite as_Moebius_product. apply Is_refining_M_property. apply rep_drop_in_range; assumption. replace inv_LL with (inv_digit LL); trivial; apply Incl_M_absorbs_Is_refining_M; assumption. apply denom_nonvanishing_product_init; assumption. apply rep_drop_in_range; assumption. replace inv_LL with (inv_digit LL); trivial; apply Incl_M_absorbs_Is_refining_M; assumption... rewrite as_Moebius_L; try exact H_base. refine (rep_L (homographic (product inv_LL (product_init mu alpha n)) (drop n alpha) H_productive_dropped) _ _ _ _ H_bis). exact H_base. rewrite product_associative; rewrite as_Moebius_product. apply homographic_correctness. apply (rep_drop _ _ n Hr_alpha)... apply denom_nonvanishing_product_init; assumption... apply rep_drop_in_range; assumption... replace inv_LL with (inv_digit LL); trivial; apply Incl_M_absorbs_Is_refining_M; assumption... rewrite product_associative; apply denom_nonvanishing_M_product. replace inv_LL with (inv_digit LL); trivial; apply Incl_M_absorbs_Is_refining_M; assumption. apply rep_drop_in_range; assumption. apply denom_nonvanishing_product_init; assumption. replace (as_Moebius mu r) with (as_Moebius (product RR (product inv_RR mu)) r); [ idtac | rewrite <- product_inv_R; reflexivity]; replace (product inv_RR mu) with (product inv_RR (product (product_init mu alpha n) (product_init_rev alpha n))); [ idtac | rewrite <- product_init_init_rev_id; trivial]. assert (H_base:(-1 <= as_Moebius (product inv_RR (product (product_init mu alpha n) (product_init_rev alpha n))) r <= 1)%R). rewrite product_associative. rewrite as_Moebius_product. apply Is_refining_M_property. apply rep_drop_in_range; assumption. replace inv_RR with (inv_digit RR); trivial; apply Incl_M_absorbs_Is_refining_M; assumption. apply denom_nonvanishing_product_init; assumption. apply rep_drop_in_range; assumption. replace inv_RR with (inv_digit RR); trivial; apply Incl_M_absorbs_Is_refining_M; assumption... rewrite as_Moebius_R; try exact H_base. refine (rep_R (homographic (product inv_RR (product_init mu alpha n)) (drop n alpha) H_productive_dropped) _ _ _ _ H_bis). exact H_base. rewrite product_associative; rewrite as_Moebius_product. apply homographic_correctness. apply (rep_drop _ _ n Hr_alpha)... apply denom_nonvanishing_product_init; assumption... apply rep_drop_in_range; assumption... replace inv_RR with (inv_digit RR); trivial; apply Incl_M_absorbs_Is_refining_M; assumption... rewrite product_associative; apply denom_nonvanishing_M_product. replace inv_RR with (inv_digit RR); trivial; apply Incl_M_absorbs_Is_refining_M; assumption. apply rep_drop_in_range; assumption. apply denom_nonvanishing_product_init; assumption. replace (as_Moebius mu r) with (as_Moebius (product MM (product inv_MM mu)) r); [ idtac | rewrite <- product_inv_M; reflexivity]; replace (product inv_MM mu) with (product inv_MM (product (product_init mu alpha n) (product_init_rev alpha n))); [ idtac | rewrite <- product_init_init_rev_id; trivial]. assert (H_base:(-1 <= as_Moebius (product inv_MM (product (product_init mu alpha n) (product_init_rev alpha n))) r <= 1)%R). rewrite product_associative. rewrite as_Moebius_product. apply Is_refining_M_property. apply rep_drop_in_range; assumption. replace inv_MM with (inv_digit MM); trivial; apply Incl_M_absorbs_Is_refining_M; assumption. apply denom_nonvanishing_product_init; assumption. apply rep_drop_in_range; assumption. replace inv_MM with (inv_digit MM); trivial; apply Incl_M_absorbs_Is_refining_M; assumption... rewrite as_Moebius_M; try exact H_base. refine (rep_M (homographic (product inv_MM (product_init mu alpha n)) (drop n alpha) H_productive_dropped) _ _ _ _ H_bis). exact H_base. rewrite product_associative; rewrite as_Moebius_product. apply homographic_correctness. apply (rep_drop _ _ n Hr_alpha)... apply denom_nonvanishing_product_init; assumption... apply rep_drop_in_range; assumption... replace inv_MM with (inv_digit MM); trivial; apply Incl_M_absorbs_Is_refining_M; assumption... rewrite product_associative; apply denom_nonvanishing_M_product. replace inv_MM with (inv_digit MM); trivial; apply Incl_M_absorbs_Is_refining_M; assumption. apply rep_drop_in_range; assumption. apply denom_nonvanishing_product_init; assumption. Defined.
imports: digits Refining_M homographic Streams_addenda RIneq QArithSternBrocot(R_addenda) rep