proposition: Theorem quadratic_correctness : forall (xi:Tensor) (alpha beta:Reals) (H:productive_q xi alpha beta) (r1 r2:Rdefinitions.R), rep alpha r1 -> rep beta r2-> rep (quadratic xi alpha beta H) (as_Tensor xi r1 r2).
proof: Proof. cofix. intros xi alpha beta H_productive r1 r2 Hr1_alpha Hr2_beta; destruct (quadratic_emits_strong xi alpha beta 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_Tensor xi r1 r2) with (as_Tensor (m_product LL (m_product inv_LL xi)) r1 r2); [ idtac | rewrite <- m_product_inv_L; reflexivity]; replace (m_product inv_LL xi) with (m_product inv_LL (right_product (left_product (product_init_zip xi alpha beta n) (product_init_rev alpha n)) (product_init_rev beta n))); [ idtac | rewrite <- product_init_zip_init_rev_id; trivial]. assert (H_base: (-1<=as_Tensor (m_product inv_LL (right_product (left_product (product_init_zip xi alpha beta n) (product_init_rev alpha n)) (product_init_rev beta n))) r1 r2 <= 1)%R). rewrite m_product_left_right_product_associative. rewrite as_Tensor_right_left_product_as_Moebius. apply Is_refining_T_property; try (apply rep_drop_in_range; assumption). replace inv_LL with (inv_digit LL); trivial; apply Incl_T_absorbs_Is_refining_T; assumption. apply denom_nonvanishing_product_init; assumption. apply denom_nonvanishing_product_init; assumption. apply rep_drop_in_range; assumption. apply rep_drop_in_range; assumption. replace inv_LL with (inv_digit LL); trivial; apply Incl_T_absorbs_Is_refining_T; assumption. rewrite as_Tensor_L; try exact H_base. refine (rep_L (quadratic (m_product inv_LL (product_init_zip xi alpha beta n)) (drop n alpha) (drop n beta) H_productive_dropped) _ _ _ _ H_bis). exact H_base. rewrite m_product_left_right_product_associative; rewrite as_Tensor_right_left_product_as_Moebius. apply quadratic_correctness; [ apply (rep_drop _ _ n Hr1_alpha) | apply (rep_drop _ _ n Hr2_beta) ]. apply denom_nonvanishing_product_init; assumption. apply denom_nonvanishing_product_init; assumption. apply rep_drop_in_range; assumption. apply rep_drop_in_range; assumption. replace inv_LL with (inv_digit LL); trivial; apply Incl_T_absorbs_Is_refining_T; assumption. rewrite m_product_left_right_product_associative; apply denom_nonvanishing_T_left_right_product. apply denom_nonvanishing_product_init; assumption. apply denom_nonvanishing_product_init; assumption. apply rep_drop_in_range; assumption. apply rep_drop_in_range; assumption. replace inv_LL with (inv_digit LL); trivial; apply Incl_T_absorbs_Is_refining_T; assumption. replace (as_Tensor xi r1 r2) with (as_Tensor (m_product RR (m_product inv_RR xi)) r1 r2); [ idtac | rewrite <- m_product_inv_R; reflexivity]; replace (m_product inv_RR xi) with (m_product inv_RR (right_product (left_product (product_init_zip xi alpha beta n) (product_init_rev alpha n)) (product_init_rev beta n))); [ idtac | rewrite <- product_init_zip_init_rev_id; trivial]. assert (H_base: (-1<=as_Tensor (m_product inv_RR (right_product (left_product (product_init_zip xi alpha beta n) (product_init_rev alpha n)) (product_init_rev beta n))) r1 r2 <= 1)%R). rewrite m_product_left_right_product_associative. rewrite as_Tensor_right_left_product_as_Moebius. apply Is_refining_T_property; try (apply rep_drop_in_range; assumption). replace inv_RR with (inv_digit RR); trivial; apply Incl_T_absorbs_Is_refining_T; assumption. apply denom_nonvanishing_product_init; assumption. apply denom_nonvanishing_product_init; assumption. apply rep_drop_in_range; assumption. apply rep_drop_in_range; assumption. replace inv_RR with (inv_digit RR); trivial; apply Incl_T_absorbs_Is_refining_T; assumption. rewrite as_Tensor_R; try exact H_base. refine (rep_R (quadratic (m_product inv_RR (product_init_zip xi alpha beta n)) (drop n alpha) (drop n beta) H_productive_dropped) _ _ _ _ H_bis). exact H_base. rewrite m_product_left_right_product_associative; rewrite as_Tensor_right_left_product_as_Moebius. apply quadratic_correctness; [ apply (rep_drop _ _ n Hr1_alpha) | apply (rep_drop _ _ n Hr2_beta) ]. apply denom_nonvanishing_product_init; assumption. apply denom_nonvanishing_product_init; assumption. apply rep_drop_in_range; assumption. apply rep_drop_in_range; assumption. replace inv_RR with (inv_digit RR); trivial; apply Incl_T_absorbs_Is_refining_T; assumption. rewrite m_product_left_right_product_associative; apply denom_nonvanishing_T_left_right_product. apply denom_nonvanishing_product_init; assumption. apply denom_nonvanishing_product_init; assumption. apply rep_drop_in_range; assumption. apply rep_drop_in_range; assumption. replace inv_RR with (inv_digit RR); trivial; apply Incl_T_absorbs_Is_refining_T; assumption. replace (as_Tensor xi r1 r2) with (as_Tensor (m_product MM (m_product inv_MM xi)) r1 r2); [ idtac | rewrite <- m_product_inv_M; reflexivity]; replace (m_product inv_MM xi) with (m_product inv_MM (right_product (left_product (product_init_zip xi alpha beta n) (product_init_rev alpha n)) (product_init_rev beta n))); [ idtac | rewrite <- product_init_zip_init_rev_id; trivial]. assert (H_base: (-1<=as_Tensor (m_product inv_MM (right_product (left_product (product_init_zip xi alpha beta n) (product_init_rev alpha n)) (product_init_rev beta n))) r1 r2 <= 1)%R). rewrite m_product_left_right_product_associative. rewrite as_Tensor_right_left_product_as_Moebius. apply Is_refining_T_property; try (apply rep_drop_in_range; assumption). replace inv_MM with (inv_digit MM); trivial; apply Incl_T_absorbs_Is_refining_T; assumption. apply denom_nonvanishing_product_init; assumption. apply denom_nonvanishing_product_init; assumption. apply rep_drop_in_range; assumption. apply rep_drop_in_range; assumption. replace inv_MM with (inv_digit MM); trivial; apply Incl_T_absorbs_Is_refining_T; assumption. rewrite as_Tensor_M; try exact H_base. refine (rep_M (quadratic (m_product inv_MM (product_init_zip xi alpha beta n)) (drop n alpha) (drop n beta) H_productive_dropped) _ _ _ _ H_bis). exact H_base. rewrite m_product_left_right_product_associative; rewrite as_Tensor_right_left_product_as_Moebius. apply quadratic_correctness; [ apply (rep_drop _ _ n Hr1_alpha) | apply (rep_drop _ _ n Hr2_beta) ]. apply denom_nonvanishing_product_init; assumption. apply denom_nonvanishing_product_init; assumption. apply rep_drop_in_range; assumption. apply rep_drop_in_range; assumption. replace inv_MM with (inv_digit MM); trivial; apply Incl_T_absorbs_Is_refining_T; assumption. rewrite m_product_left_right_product_associative; apply denom_nonvanishing_T_left_right_product. apply denom_nonvanishing_product_init; assumption. apply denom_nonvanishing_product_init; assumption. apply rep_drop_in_range; assumption. apply rep_drop_in_range; assumption. replace inv_MM with (inv_digit MM); trivial; apply Incl_T_absorbs_Is_refining_T; assumption. Defined.
imports: digits Refining_T quadratic Streams_addenda rep RIneq QArithSternBrocot(R_addenda)