proposition: Lemma ProdIntegrableSimplifyDomain : forall {I J : IntegrationSpace} (hn : list (@ProdIntegrable I J)) (x : X (ElemFunc I)) (y : X (ElemFunc J)), Domain (ProdLFunc (ProdIntegrableSimplify hn)) (x,y) -> Domain (ProdLFunc hn) (x,y).
proof: Proof. intros I J hn x y H. assert (lt O (length (FreeSubsets (length hn)))) as flen. { destruct (FreeSubsets (length hn)) eqn:des. exfalso. exact (FreeSubsetsNotNil _ des). apply le_n_S, Nat.le_0_l. } apply DomainProdLFuncSplitCoord. - destruct (ProdLFuncDomainLeft _ x y H) as [[nl isinl] | H0]. + intros. destruct isinl. unfold ProdIntegrableSimplify in H2. rewrite (nth_indep _ (ProdIntegrableZero I J) (ProdSubsetIntersect hn (fst (nil,@nil bool)) (snd (@nil bool, nil)))) in H2. 2: exact H1. unfold ProdIntegrableSimplify in H1. rewrite map_length, prod_length in H1. rewrite (map_nth (fun xy : list bool * list bool => ProdSubsetIntersect hn (fst xy) (snd xy))) in H2. simpl in H2. unfold SubsetIntersectLeft in H2. apply (DomainProdSubsetIntersect (map prodint_f hn) _ _ _ n) in H2. destruct (nth_error (map prodint_f hn) n) eqn:des. apply (nth_error_nth (map prodint_f hn) n (prodint_f (ProdIntegrableZero I J))) in des. subst P. destruct (nth_error (fst (nth nl (list_prod (FreeSubsets (length hn)) (FreeSubsets (length hn))) (nil, nil))) n) eqn:des2. destruct b. left. rewrite map_nth in H2. exact H2. rewrite map_nth in H2. right. exact H2. exfalso. apply nth_error_None in des2. rewrite nth_list_prod in des2. unfold fst in des2. rewrite (FreeSubsetsLength (length hn) (nth (nl / length (FreeSubsets (length hn))) (FreeSubsets (length hn)) nil)) in des2. exact (proj1 (Nat.lt_nge _ _) H0 des2). apply nth_In. apply Nat.div_lt_upper_bound in H1. exact H1. intro abs. rewrite abs in flen. inversion flen. exact H1. exfalso. apply nth_error_None in des. rewrite map_length in des. exact (proj1 (Nat.lt_nge _ _) H0 des). + assert (Forall (fun h => ~h x) (map prodint_f hn)). { apply SubsetIntersectFilterOut. intros. destruct (FreeSubsetsFull filter) as [n [H2 H3]]. specialize (H0 (n * (length (FreeSubsets (length hn))))%nat). rewrite map_length in H1. intro abs. apply H0. unfold ProdIntegrableSimplify. rewrite map_length, prod_length. rewrite <- Nat.mul_lt_mono_pos_r. rewrite <- H1. exact H2. exact flen. clear H0. unfold ProdIntegrableSimplify. rewrite (nth_indep _ (ProdIntegrableZero I J) (ProdSubsetIntersect hn (fst (nil,@nil bool)) (snd (@nil bool, nil)))). rewrite (map_nth (fun xy : list bool * list bool => ProdSubsetIntersect hn (fst xy) (snd xy))). simpl. unfold SubsetIntersectLeft. rewrite (nth_list_prod (FreeSubsets (length hn)) (FreeSubsets (length hn)) nil nil (n * (length (FreeSubsets (length hn))))). unfold fst. rewrite Nat.div_mul. rewrite <- H1, H3. exact abs. intro H4. rewrite H4 in flen. inversion flen. rewrite <- Nat.mul_lt_mono_pos_r. rewrite <- H1. exact H2. exact flen. rewrite map_length, prod_length. rewrite <- Nat.mul_lt_mono_pos_r. rewrite <- H1. exact H2. exact flen. } intros. right. rewrite Forall_forall in H1. apply (H1 (prodint_f (nth n hn (ProdIntegrableZero I J)))). apply in_map, nth_In, H2. - destruct (ProdLFuncDomainRight _ x y H) as [[nl isinl] | H0]. + intros. destruct isinl. unfold ProdIntegrableSimplify in H2. rewrite (nth_indep _ (ProdIntegrableZero I J) (ProdSubsetIntersect hn (fst (nil,@nil bool)) (snd (@nil bool, nil)))) in H2. 2: exact H1. unfold ProdIntegrableSimplify in H1. rewrite map_length, prod_length in H1. rewrite (map_nth (fun xy : list bool * list bool => ProdSubsetIntersect hn (fst xy) (snd xy))) in H2. simpl in H2. unfold SubsetIntersectLeft in H2. apply (DomainProdSubsetIntersect (map prodint_g hn) _ _ _ n) in H2. destruct (nth_error (map prodint_g hn) n) eqn:des. apply (nth_error_nth (map prodint_g hn) n (prodint_g (ProdIntegrableZero I J))) in des. subst P. destruct (nth_error (snd (nth nl (list_prod (FreeSubsets (length hn)) (FreeSubsets (length hn))) (nil, nil))) n) eqn:des2. destruct b. left. rewrite map_nth in H2. exact H2. rewrite map_nth in H2. right. exact H2. exfalso. apply nth_error_None in des2. rewrite nth_list_prod in des2. unfold snd in des2. rewrite (FreeSubsetsLength (length hn) (nth (nl mod length (FreeSubsets (length hn))) (FreeSubsets (length hn)) nil)) in des2. exact (proj1 (Nat.lt_nge _ _) H0 des2). apply nth_In. apply Nat.mod_bound_pos. apply Nat.le_0_l. exact flen. exact H1. exfalso. apply nth_error_None in des. rewrite map_length in des. exact (proj1 (Nat.lt_nge _ _) H0 des). + assert (Forall (fun h => ~h y) (map prodint_g hn)). { apply SubsetIntersectFilterOut. intros. destruct (FreeSubsetsFull filter) as [n [H2 H3]]. specialize (H0 n). rewrite map_length in H1. intro abs. apply H0. unfold ProdIntegrableSimplify. rewrite map_length, prod_length. apply (Nat.lt_le_trans _ (1 * length (FreeSubsets (length hn)))). rewrite Nat.mul_1_l. rewrite <- H1. exact H2. apply Nat.mul_le_mono_nonneg_r. apply Nat.le_0_l. exact flen. clear H0. unfold ProdIntegrableSimplify. rewrite (nth_indep _ (ProdIntegrableZero I J) (ProdSubsetIntersect hn (fst (nil,@nil bool)) (snd (@nil bool, nil)))). rewrite (map_nth (fun xy : list bool * list bool => ProdSubsetIntersect hn (fst xy) (snd xy))). simpl. unfold SubsetIntersectRight. rewrite (nth_list_prod (FreeSubsets (length hn)) (FreeSubsets (length hn)) nil nil n). unfold snd. rewrite Nat.mod_small. rewrite <- H1, H3. exact abs. rewrite <- H1. exact H2. apply (Nat.lt_le_trans _ (1 * length (FreeSubsets (length hn)))). rewrite Nat.mul_1_l. rewrite <- H1. exact H2. apply Nat.mul_le_mono_nonneg_r. apply Nat.le_0_l. exact flen. rewrite map_length, prod_length. apply (Nat.lt_le_trans _ (1 * length (FreeSubsets (length hn)))). rewrite Nat.mul_1_l. rewrite <- H1. exact H2. apply Nat.mul_le_mono_nonneg_r. apply Nat.le_0_l. exact flen. } intros. right. rewrite Forall_forall in H1. apply (H1 (prodint_g (nth n hn (ProdIntegrableZero I J)))). apply in_map, nth_In, H2. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile