proposition: Lemma ProdIntegrableSimplifyApply : forall {I J : IntegrationSpace} (hn : list (@ProdIntegrable I J)) (x : X (ElemFunc I)) (y : X (ElemFunc J)) (xyH : Domain (ProdLFunc hn) (x,y)) (xyS : Domain (ProdLFunc (ProdIntegrableSimplify hn)) (x,y)), partialApply _ _ xyS == SubsetIntersectFactor hn (ProdIntegrableSubsetLeft hn x y xyH) (ProdIntegrableSubsetRight hn x y xyH).
proof: Proof. intros. destruct (SubsetUnionLeftDec hn x y xyH) as [inunionf|notinunionf]. destruct (SubsetUnionRightDec hn x y xyH) as [inuniong|notinuniong]. pose proof (FreeSubsetsFull (ProdIntegrableSubsetLeft hn x y xyH)) as [kf H]. rewrite ProdIntegrableSubsetLeft_length in H. pose proof (FreeSubsetsFull (ProdIntegrableSubsetRight hn x y xyH)) as [kg H0]. rewrite ProdIntegrableSubsetRight_length in H0. assert (kg + kf * (length (FreeSubsets (length hn))) < length (ProdIntegrableSimplify hn))%nat. { unfold ProdIntegrableSimplify. rewrite map_length, prod_length. destruct H. apply (Nat.lt_le_trans _ (length (FreeSubsets (length hn)) + kf * length (FreeSubsets (length hn)))). rewrite <- Nat.add_lt_mono_r. apply H0. apply (Nat.mul_le_mono_nonneg_r (S kf) _ (length (FreeSubsets (length hn)))). apply Nat.le_0_l. exact H. } rewrite (ProdLFuncApplyUnique (ProdIntegrableSimplify hn) x y xyS (kg + kf * (length (FreeSubsets (length hn)))) H1). - assert (kg + kf * (length (FreeSubsets (length hn))) < length (FreeSubsets (length hn)) * length (FreeSubsets (length hn)))%nat. { unfold ProdIntegrableSimplify in H1 ; rewrite map_length, prod_length in H1. exact H1. } pose proof (nth_list_prod (FreeSubsets (length hn)) (FreeSubsets (length hn)) nil nil (kg + kf * (length (FreeSubsets (length hn)))) H2). rewrite Nat.div_add, Nat.mod_add, Nat.div_small, Nat.mod_small in H3. 2: apply H0. 2: apply H0. symmetry. rewrite <- CRmult_1_r. apply CRmult_morph. rewrite <- CRmult_1_r. apply CRmult_morph. + unfold ProdIntegrableSimplify. rewrite (nth_indep _ (ProdIntegrableZero I J) (ProdSubsetIntersect hn (fst (nil,@nil bool)) (snd (@nil bool, nil)))). rewrite (map_nth (fun xy => ProdSubsetIntersect hn (fst xy) (snd xy))), H3. unfold fst, snd. destruct H, H0. simpl (0 + kf)%nat. rewrite H4, H5. reflexivity. rewrite map_length. rewrite prod_length. exact H2. + destruct (DomainProdLFuncInc (ProdIntegrableSimplify hn) x y xyS (kg + kf * length (FreeSubsets (length hn))) H1). destruct d. reflexivity. exfalso. simpl in n. apply n. unfold ProdIntegrableSimplify. rewrite (nth_indep _ (ProdIntegrableZero I J) (ProdSubsetIntersect hn (fst (nil,@nil bool)) (snd (@nil bool, nil)))). rewrite (map_nth (fun xy => ProdSubsetIntersect hn (fst xy) (snd xy))), H3. simpl. destruct H. rewrite H4. apply ProdIntegrableSubsetLeft_match. apply inunionf. exact H1. + destruct (DomainProdLFuncInc (ProdIntegrableSimplify hn) x y xyS (kg + kf * length (FreeSubsets (length hn))) H1). destruct d0. reflexivity. exfalso. simpl in n. apply n. unfold ProdIntegrableSimplify. rewrite (nth_indep _ (ProdIntegrableZero I J) (ProdSubsetIntersect hn (fst (nil,@nil bool)) (snd (@nil bool, nil)))). rewrite (map_nth (fun xy => ProdSubsetIntersect hn (fst xy) (snd xy))), H3. simpl. destruct H0. rewrite H4. apply ProdIntegrableSubsetRight_match. apply inuniong. exact H1. + intros abs. destruct H. rewrite abs in H. inversion H. + intros abs. destruct H. rewrite abs in H. inversion H. - intros. simpl. rewrite CRmult_assoc. rewrite (CRmult_morph _ _ _ (CReq_refl _) _ 0). apply CRmult_0_r. destruct (DomainProdLFuncInc (ProdIntegrableSimplify hn) x y xyS k ltkh). destruct d. destruct d0. 2: unfold snd; apply CRmult_0_r. 2: unfold fst; apply CRmult_0_l. exfalso. assert (k < length (FreeSubsets (length hn)) * length (FreeSubsets (length hn)))%nat. { unfold ProdIntegrableSimplify in ltkh. rewrite map_length, prod_length in ltkh. exact ltkh. } pose proof (nth_list_prod (FreeSubsets (length hn)) (FreeSubsets (length hn)) nil nil k H3). unfold fst, ProdIntegrableSimplify in p. rewrite (nth_indep _ (ProdIntegrableZero I J) (ProdSubsetIntersect hn (fst (nil,@nil bool)) (snd (@nil bool, nil)))) in p. rewrite (map_nth (fun xy => ProdSubsetIntersect hn (fst xy) (snd xy))), H4 in p. unfold fst, snd in p. unfold fst, ProdIntegrableSimplify in p0. rewrite (nth_indep _ (ProdIntegrableZero I J) (ProdSubsetIntersect hn (fst (nil,@nil bool)) (snd (@nil bool, nil)))) in p0. rewrite (map_nth (fun xy => ProdSubsetIntersect hn (fst xy) (snd xy))), H4 in p0. unfold fst, snd in p0. 2: rewrite map_length, prod_length; exact H3. 2: rewrite map_length, prod_length; exact H3. clear H4. assert (0 < length (FreeSubsets (length hn)))%nat as lenPos. { apply (Nat.le_lt_trans _ kg _ (Nat.le_0_l _)). apply H0. } destruct (Nat.eq_dec (k / length (FreeSubsets (length hn))) kf). + rewrite e in p0. clear p. simpl in p0. apply (ProdIntegrableSubsetsDisjoint (map prodint_g hn) (nth (k mod length (FreeSubsets (length hn))) (FreeSubsets (length hn)) nil) (ProdIntegrableSubsetRight hn x y xyH) y). rewrite ProdIntegrableSubsetRight_length. apply FreeSubsetsLength. apply nth_In. apply Nat.mod_bound_pos. apply Nat.le_0_l. exact lenPos. apply FreeSubsetsLength. rewrite map_length. apply nth_In. apply Nat.mod_bound_pos. apply Nat.le_0_l. exact lenPos. destruct H0. rewrite <- H4. apply FreeSubsetsDifferent. intro abs. subst kg. subst kf. pose proof (Nat.div_mod k (length (FreeSubsets (length hn)))). rewrite Nat.add_comm, Nat.mul_comm in H5. apply H2, H5. intro abs. rewrite abs in lenPos. inversion lenPos. apply Nat.mod_bound_pos. apply Nat.le_0_l. exact lenPos. exact H0. split. exact p0. apply ProdIntegrableSubsetRight_match. apply inuniong. + clear p0. simpl in p. assert (k / length (FreeSubsets (length hn)) < length (FreeSubsets (length hn)))%nat. { apply Nat.div_lt_upper_bound in H3. exact H3. intro abs. rewrite abs in lenPos. inversion lenPos. } apply (ProdIntegrableSubsetsDisjoint (map prodint_f hn) (nth (k / length (FreeSubsets (length hn))) (FreeSubsets (length hn)) nil) (ProdIntegrableSubsetLeft hn x y xyH) x). rewrite ProdIntegrableSubsetLeft_length. apply FreeSubsetsLength. apply nth_In. exact H4. apply FreeSubsetsLength. rewrite map_length. apply nth_In. exact H4. destruct H. rewrite <- H5. apply FreeSubsetsDifferent. exact n. exact H4. exact H. split. exact p. apply ProdIntegrableSubsetLeft_match. apply inunionf. - rewrite ApplyOutsidePointLeft. 2: apply notinuniong. apply ProdLFuncApplyZero. intros. simpl. destruct (DomainProdLFuncInc (ProdIntegrableSimplify hn) x y xyS n ltnh), d0. 2: apply CRmult_0_r. exfalso. clear d. simpl in p. unfold ProdIntegrableSimplify in p. rewrite (nth_indep _ (ProdIntegrableZero I J) (ProdSubsetIntersect hn (fst (nil,@nil bool)) (snd (@nil bool, nil)))) in p. 2: exact ltnh. rewrite (map_nth (fun xy => ProdSubsetIntersect hn (fst xy) (snd xy))), nth_list_prod in p. unfold fst, snd in p. apply SubsetIntersectFilter_init in p. destruct (SubsetUnionRightDec hn x y xyH). destruct H, notinuniong. contradiction. destruct H, notinuniong. contradiction. unfold ProdIntegrableSimplify in ltnh. rewrite map_length, prod_length in ltnh. exact ltnh. - rewrite ApplyOutsidePointRight. 2: apply notinunionf. apply ProdLFuncApplyZero. intros. simpl. destruct (DomainProdLFuncInc (ProdIntegrableSimplify hn) x y xyS n ltnh), d. 2: rewrite CRmult_0_r; apply CRmult_0_l. exfalso. clear d0. simpl in p. unfold ProdIntegrableSimplify in p. rewrite (nth_indep _ (ProdIntegrableZero I J) (ProdSubsetIntersect hn (fst (nil,@nil bool)) (snd (@nil bool, nil)))) in p. 2: exact ltnh. rewrite (map_nth (fun xy => ProdSubsetIntersect hn (fst xy) (snd xy))), nth_list_prod in p. unfold fst, snd in p. apply SubsetIntersectFilter_init in p. destruct (SubsetUnionLeftDec hn x y xyH). destruct H, notinunionf. contradiction. destruct H, notinunionf. contradiction. unfold ProdIntegrableSimplify in ltnh. rewrite map_length, prod_length in ltnh. exact ltnh. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile