ODIn/paper-BagRelationalPDBsAreHard
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

More changes

Browse source
This commit is contained in:
Aaron Huber 2020-04-27 17:02:58 -04:00
parent 6d33fe6de1
commit b1f82a318f
1 changed files with 25 additions and 25 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

50
sop.tex
View file

@ -80,8 +80,8 @@ Notice we have two cases of $\cvar{j, j'}$, the first is when $j = j'$, i.e. $(\
\subsection{$\cvar{j, j'}~|~j \neq j'$} \subsection{$\cvar{j, j'}~|~j \neq j'$}
For notational convenience set For notational convenience set
\begin{align*} \begin{align*}
\term_1\left(\wElem_1,\ldots, \wElem_{\prodsize}\right) = &\ex{\prod_{i = 1}^{\prodsize}\sine(\wElem_i)\conj{\sine(\wElem'_i)}\ind{\hfunc(\wElem_i) = j} \ind{\hfunc(\wElem'_i) = j'}}\\ \term_1\left(\wElem_1,\ldots, \wElem_{\prodsize}, \wElem'_1,\ldots, \wElem'_{\prodsize}\right) = &\ex{\prod_{i = 1}^{\prodsize}\sine(\wElem_i)\conj{\sine(\wElem'_i)}\ind{\hfunc(\wElem_i) = j} \ind{\hfunc(\wElem'_i) = j'}}\\
\term_2\left(\wElem_1,\ldots, \wElem_{\prodsize}\right) = &\ex{\prod_{i = 1}^{\prodsize}\sine(\wElem_i)\ind{\hfunc(\wElem_i) = j}} \cdot \ex{\prod_{i = 1}^{\prodsize}\conj{\sine(\wElem'_i)}\ind{\hfunc(\wElem'_i) = j'}} \term_2\left(\wElem_1,\ldots, \wElem_{\prodsize}, \wElem'_1,\ldots, \wElem'_{\prodsize}\right) = &\ex{\prod_{i = 1}^{\prodsize}\sine(\wElem_i)\ind{\hfunc(\wElem_i) = j}} \cdot \ex{\prod_{i = 1}^{\prodsize}\conj{\sine(\wElem'_i)}\ind{\hfunc(\wElem'_i) = j'}}
\end{align*} \end{align*}
Focusing on $\term_1$, observe that $\term_1 = 1$ if and only if all the $\wElem_i$'s are equal, all the $\wElem'_i$'s are equal, and the two groups of variables do not equal each other, Focusing on $\term_1$, observe that $\term_1 = 1$ if and only if all the $\wElem_i$'s are equal, all the $\wElem'_i$'s are equal, and the two groups of variables do not equal each other,
\begin{equation*} \begin{equation*}
@ -142,9 +142,9 @@ Taking a look at the leftmost term of \cref{eq:sigsq}, we establish bounds the v
\end{align} \end{align}
Before proceeding, we introduce some notation and terminology that will aid in communicating the bounds we are about to establish. We refer to the leftmost expectation of \cref{eq:sig-j-last} in the following way: Before proceeding, we introduce some notation and terminology that will aid in communicating the bounds we are about to establish. We refer to the leftmost expectation of \cref{eq:sig-j-last} in the following way:
\begin{equation}
\[\term_1\left(\wElem_1,\ldots,\wElem_\prodsize, \wElem_1',\ldots, \wElem_\prodsize'\right) = \ex{\prod_{i = 1}^\prodsize s(w_i)\overline{s(w'_i)}\ind{h(w_i) = j}\ind{h(w'_i) = j}}.%\text{, and} \term_1\left(\wElem_1,\ldots,\wElem_\prodsize, \wElem_1',\ldots, \wElem_\prodsize'\right) = \ex{\prod_{i = 1}^\prodsize s(w_i)\overline{s(w'_i)}\ind{h(w_i) = j}\ind{h(w'_i) = j}}\label{eq:term-1}.%\text{, and}
\] \end{equation}
%\[\term_2\left(\wElem_1,\ldots,\wElem_\prodsize, \wElem_1',\ldots, \wElem_\prodsize'\right) = \ex{\prod_{i = 1}^ks(w_i)\ind{h(w_i) = j}}\cdot \ex{\prod_{i = 1}^\prodsize\overline{s(w'_i)}\ind{h(w'_i) = j}}. \] %\[\term_2\left(\wElem_1,\ldots,\wElem_\prodsize, \wElem_1',\ldots, \wElem_\prodsize'\right) = \ex{\prod_{i = 1}^ks(w_i)\ind{h(w_i) = j}}\cdot \ex{\prod_{i = 1}^\prodsize\overline{s(w'_i)}\ind{h(w'_i) = j}}. \]
We will use the vocabulary 'term' to denote $\prod_{i = 1}^{\prodsize}\vect_i(\wElem_i)\vect_i(\wElem_i') \cdot\term_1\left(\wElem_1,\ldots,\wElem_\prodsize\right)$ given a specific set of world values. %To say that a term survives \AR{You should not care about whether the $T_1$ term survives or not. See the above comment on why.} the expectation is to mean that $\term_1 - \term_2 \neq 0$. Note, that the only terms that survive the expectation above are mappings of $w_i = w'_j = w$ for $i, j \in [\prodsize]$, such that each $w_i$ has a match, i.e., no $w_i$ or $w'_j$ stands alone without a matching world in its complimentary set. In other words, the set of values in $\wElem_1,\ldots,\wElem_k$ has a bijective mapping to the set of values in $\wElem'_1,\ldots,\wElem'_k$. We will use the vocabulary 'term' to denote $\prod_{i = 1}^{\prodsize}\vect_i(\wElem_i)\vect_i(\wElem_i') \cdot\term_1\left(\wElem_1,\ldots,\wElem_\prodsize\right)$ given a specific set of world values. %To say that a term survives \AR{You should not care about whether the $T_1$ term survives or not. See the above comment on why.} the expectation is to mean that $\term_1 - \term_2 \neq 0$. Note, that the only terms that survive the expectation above are mappings of $w_i = w'_j = w$ for $i, j \in [\prodsize]$, such that each $w_i$ has a match, i.e., no $w_i$ or $w'_j$ stands alone without a matching world in its complimentary set. In other words, the set of values in $\wElem_1,\ldots,\wElem_k$ has a bijective mapping to the set of values in $\wElem'_1,\ldots,\wElem'_k$.
@ -206,7 +206,7 @@ Next, we argue that $S_1 \subseteq S_2$. Pick an arbitrary tuple $\left(\wElem_
\begin{Lemma} \begin{Lemma}
Given a distinct $\dw_1 \prec \cdots \prec \dw_{\dist}$ over every distinct $\surj:[\prodsize]\mapsto [\dist]$, the tuples $\left(\dw_{\surj(1)},\ldots, \dw_{\surj(\prodsize)}\right)$ are distinct. Given a distinct $\dw_1 \prec \cdots \prec \dw_{\dist}$ over every distinct $\surj:[\prodsize]\mapsto [\dist]$, the tuples $\left(\dw_{\surj(1)},\ldots, \dw_{\surj(\prodsize)}\right)$ are distinct.
\end{Lemma} \end{Lemma}
\AH{Needs a formal proof. Working on that.}
\begin{proof} \begin{proof}
For a given $\prodsize, \dist$, every function $\surj$ in the set of surjective functions ($\surjSet$), applies its mapping to the set of distinct value combinations that respect the total order ($\mtupSet$). In other words, an alternative view is to take the cartesian product of the world values that can be mapped to the $\dist$ $\dw_i$ variables respecting $\prec$, i.e., For a given $\prodsize, \dist$, every function $\surj$ in the set of surjective functions ($\surjSet$), applies its mapping to the set of distinct value combinations that respect the total order ($\mtupSet$). In other words, an alternative view is to take the cartesian product of the world values that can be mapped to the $\dist$ $\dw_i$ variables respecting $\prec$, i.e.,
\[\mtupSet = \left\{\left(\dw_1,\ldots, \dw_{\dist}\right) ~|~ \dw_1,\ldots, \dw_{\dist} \in \wSet, \dw_1 \prec \cdots \prec \dw_{\dist}\right\},\] \[\mtupSet = \left\{\left(\dw_1,\ldots, \dw_{\dist}\right) ~|~ \dw_1,\ldots, \dw_{\dist} \in \wSet, \dw_1 \prec \cdots \prec \dw_{\dist}\right\},\]
@ -221,13 +221,13 @@ For the second case, assume that $\disttup = \disttup'$, which then requires tha
\end{proof} \end{proof}
%, while additionally including all symmetrical counterparts allows for double counting. This double counting is mitigated by the fact that $\dw_1 \prec \cdots \prec \dw_\dist$ based on the fixed order of the world values, which then \AR{I do not see what the ``symmetrical counterparts" comment adds here. Just remove it}. %, while additionally including all symmetrical counterparts allows for double counting. This double counting is mitigated by the fact that $\dw_1 \prec \cdots \prec \dw_\dist$ based on the fixed order of the world values, which then \AR{I do not see what the ``symmetrical counterparts" comment adds here. Just remove it}.
%yields exactly the world value combinations containing $\dist$ distinct values which appear in the cartesian product of the sum. %yields exactly the world value combinations containing $\dist$ distinct values which appear in the cartesian product of the sum.
\AR{Overall comments: (1) The main thing missing if explicitly stating that $(w_1,\dots,w_k)\mapsto (\dw_{\surj(1)},\ldots,\dw_{\surj(\dist)})$. (2) After stating the map you should argue in words why all distinct tuples with $m$ distinct world values are covered.} %\AR{Overall comments: (1) The main thing missing if explicitly stating that $(w_1,\dots,w_k)\mapsto (\dw_{\surj(1)},\ldots,\dw_{\surj(\dist)})$. (2) After stating the map you should argue in words why all distinct tuples with $m$ distinct world values are covered.}
\begin{Definition} \begin{Definition}
Functions $\surj:[\prodsize]\mapsto [\dist], \surj':[\prodsize]\mapsto [\dist']$ are said to be matching, denoted $\match{\surj}{\surj'}$, if and only if Functions $\surj:[\prodsize]\mapsto [\dist], \surj':[\prodsize]\mapsto [\dist']$ are said to be matching, denoted $\match{\surj}{\surj'}$, if and only if
\begin{enumerate} \begin{enumerate}
\item $\dist = \dist'$ %\item $\dist = \dist'$
\item $\forall i \in [\dist], |\surj^{-1}(i)| = |\surj'^{-1}(i)|$, i.e., the cardinality of variables mapped to $\dw_i$ equals the cardinality of variables mapped to $\dw_i'$, for all $i \in [\dist]$. \item $\forall i \in [\dist], |\surj^{-1}(i)| = |\surj'^{-1}(i)|$, i.e., the cardinality of variables mapped to $\dw_i$ equals the cardinality of variables mapped to $\dw_i'$, for all $i \in [\dist]$.
\end{enumerate} \end{enumerate}
\end{Definition} \end{Definition}
@ -235,9 +235,9 @@ Functions $\surj:[\prodsize]\mapsto [\dist], \surj':[\prodsize]\mapsto [\dist']$
\AH{handle $\term_1$ first, then use the lemma to tackle eq 95; use lemma that was stated in terms of $\term_1$, and create another lemma for 95} \AH{handle $\term_1$ first, then use the lemma to tackle eq 95; use lemma that was stated in terms of $\term_1$, and create another lemma for 95}
\AH{explicity note the independence of h and s, to justify pushing expectations through products} \AH{explicity note the independence of h and s, to justify pushing expectations through products}
\begin{Lemma}\label{lem:sig-j-survive} \begin{Lemma}\label{lem:sig-j-survive}
When $\surj, \surj'$are matching, where $\forall j \in[\dist], \dw_{_j} = \dw_{'_j}$, \cref{eq:sig-j-distinct} is exactly When $\surj, \surj'$are matching, where for every $j \in[\dist], \dw_{j} = \dw'_{j}$, %\cref{eq:sig-j-distinct} is exactly
\[ \[
\sum_{\substack{\dw_{_1}, \ldots,\dw_{_\dist},\\\dw_{'_1},\ldots,\dw_{'_{\dist'}}\\ \in W}}\prod_{i = 1}^{\prodsize}\vect_i(\dw_{_{\surj(i)}})\vect_i(\dw_{'_{\surj'(i)}}) \term_1(\dw_{\surj(1)},\dots, \dw_{\surj(\prodsize)}, \dw_{\surj'(1)},\dots, \dw_{\surj'(\prodsize')}) = \sum_{\substack{\dw_{1} \prec \cdots \prec \dw_{_\dist}\\ \in \wSet}}\prod_{i = 1}^{\prodsize}\vect_i(\dw_{\surj(i)})\vect_i(\dw_{\surj'(i)})
\] \]
and $0$ otherwise. and $0$ otherwise.
\end{Lemma} \end{Lemma}
@ -262,19 +262,20 @@ and $0$ otherwise.
%In the above, since we have more than pairwise independence for $\wElem \neq \wElem'$, we can push the expectation into the product. Then by \cref{lem:exp-sine} we get 0 for both expectations.\newline %In the above, since we have more than pairwise independence for $\wElem \neq \wElem'$, we can push the expectation into the product. Then by \cref{lem:exp-sine} we get 0 for both expectations.\newline
\AR{First some typos/things that are incorrect below-- note this is \textbf{not} an exhaustive list. (1) In the proof below the $w_i$ and $w'_i$ should be $\tilde{w}_i$ and $\tilde{w'}_i$ respectively. (2) The expression for $T_1$ below is incorrect since it seems to assume that all the pre-image sizes are $1$-- the expression for $T_2$ is fine except the $j_i$ terms are not defined. However, ``taking out" one term for $\tilde{w'}_{m'}$ for $T_2$ is incorrect since e.g. we could have the pre-image of $m'$ have size $>1$. (3) The proof below never explicitly argues why the condition $\dw_{_j} = \dw_{'_j}$ is needed.} \AR{First some typos/things that are incorrect below-- note this is \textbf{not} an exhaustive list. (1) In the proof below the $w_i$ and $w'_i$ should be $\dw_i$ and $\dw_i$ respectively. (2) The expression for $T_1$ below is incorrect since it seems to assume that all the pre-image sizes are $1$-- the expression for $T_2$ is fine except the $j_i$ terms are not defined. However, ``taking out" one term for $\dw_{m'}$ for $T_2$ is incorrect since e.g. we could have the pre-image of $m'$ have size $>1$. (3) The proof below never explicitly argues why the condition $\dw_{_j} = \dw_{'_j}$ is needed.}
\AR{Here is how I recommend that you re-write the proof. First as mentioned earlier, you should only consider the $T_1$ terms (as you account for the $T_2$ terms later on. Second you should first start off by re-stating the $T_1$ term like so. Consider the ``generic term"-- \AR{Here is how I recommend that you re-write the proof. First as mentioned earlier, you should only consider the $T_1$ terms (as you account for the $T_2$ terms later on. Second you should first start off by re-stating the $T_1$ term like so. Consider the ``generic term"--
\[T_1(\tilde{w}_{\surj(1)},\dots, \tilde{w}_{\surj(m)}, \tilde{w'}_{\surj'(1)},\dots, \tilde{w'}_{\surj'(m')}).\] \[T_1(\dw_{\surj(1)},\dots, \dw_{\surj(m)}, \dw_{\surj'(1)},\dots, \dw_{\surj'(m')}).\]
Then re-write the what the above term is based on the exact definition (BTW I'm dropping the $\mathbf{E}$ terms for convenience but they should be all there below.) In particular, the above term by definition is exactly Then re-write the what the above term is based on the exact definition (BTW I'm dropping the $\mathbf{E}$ terms for convenience but they should be all there below.) In particular, the above term by definition is exactly
\[\prod_{i=1}^k s(\tilde{w}_{\surj(i)})\cdot \overline{s(\tilde{w'}_{\surj'(i)})}.\] \[\prod_{i=1}^k s(\dw_{\surj(i)})\cdot \overline{s(\dw_{\surj'(i)})}.\]
Now re-write the above in terms of ``powers" of distinct worlds: Now re-write the above in terms of ``powers" of distinct worlds:
\[ (\prod_{i=1}^m s(\tilde{w}_{i})^{|\surj^{-1}(i)|})\cdot \overline{(\prod_{j=1}^m s(\tilde{w'}_j)^{|\surj^{-1}(j)|})}\] \[ (\prod_{i=1}^m s(\dw_{i})^{|\surj^{-1}(i)|})\cdot \overline{(\prod_{j=1}^m s(\dw_j)^{|\surj^{-1}(j)|})}\]
Now once you have the above expression, then it will be much easier to argue why if any of the matching conditions are not satisfied then the expression is $0$. I also believe that working with the above expression will also make it more ``obvious" as to why the different conditions are required. Currently the arguments below do not explicitly bring this out... Now once you have the above expression, then it will be much easier to argue why if any of the matching conditions are not satisfied then the expression is $0$. I also believe that working with the above expression will also make it more ``obvious" as to why the different conditions are required. Currently the arguments below do not explicitly bring this out...
} }
\textit{*In the subsequent proofs, at most we assume 2k wise independence for both $\hfunc$ and $\sine$, but we really would like less*}.
\begin{proof} \begin{proof}
Consider the "generic term"-- Note \cref{eq:term-1}, and consider the "generic term"--
\[T_1(\tilde{w}_{\surj(1)},\dots, \tilde{w}_{\surj(\prodsize)}, \tilde{w'}_{\surj'(1)},\dots, \tilde{w'}_{\surj'(\prodsize')}).\] \[\term_1(\dw_{\surj(1)},\dots, \dw_{\surj(\prodsize)}, \dw_{\surj'(1)},\dots, \dw_{\surj'(\prodsize')}).\]
Let's rewrite the term based on its exact definition: Let's rewrite the term based on its exact definition:
\begin{align*} \begin{align*}
@ -286,9 +287,9 @@ Further see how the requirement that $\dw_i = \dw'_i$ gives us the precise combi
To prove that \cref{lem:sig-j-survive} is true, consider what the expectation looks like when $\surj, \surj'$ are not matching. The first condition for $\surj, \surj'$ to be matching is violated when $\dist \neq \dist'$. To prove that \cref{lem:sig-j-survive} is true, consider what the expectation looks like when $\surj, \surj'$ are not matching. The first condition for $\surj, \surj'$ to be matching is violated when $\dist \neq \dist'$.
\AH{The following observation isn't necessary to complete the proof. I'll just leave it for now in case it may be valuable down the road.} \AH{The following observation isn't necessary to complete the proof. I'll just leave it for now in case it may be valuable down the road.}
\AH{Don't use $\exists, \forall$ in prose; mathematcial notation shouldn't be used to replace the prose, only to enhance the prose.}
Observe that $\forall \dist \in [\prodsize], \sum_{i = 1}^{\dist}|\surj^{-1}(i)| = \prodsize$ and that this fact implies for $\dist, \dist' \in [\prodsize] ~|~\dist \neq \dist', \exists i \in [m] ~|~\forall j \in [m], \surj^{-1}(i)| \neq |\surj'^{-1}(j)|$, meaning that if we have that $\dist \neq \dist'$, then the second matching condition is also violated. Observe that for all $\dist \in [\prodsize], \sum_{i = 1}^{\dist}|\surj^{-1}(i)| = \prodsize$ and that this fact implies for $\dist, \dist' \in [\prodsize]$ such that $\dist \neq \dist'$, there exists $i \in [m]$ such that $|\surj^{-1}(i)| \neq |\surj'^{-1}(i)|$, meaning that if we have that $\dist \neq \dist'$, then the second matching condition is also violated.
\AH{Moving on...}Note that $\dw_1\ldots\dw_\dist, \dw_1'\ldots\dw_{\dist'}'$ are distinct world values such that $\forall i \neq j \in [\dist], \dw_i = \dw_i' \neq \dw_j = \dw_j'$. To make things easier, assume that $\dist < \dist'$. The opposite case of $\dist > \dist'$ has a symmetrical proof. Fixing variables $\dw_1\ldots\dw_\dist, \dw_1'\ldots\dw_\dist$, we have at least one $\dw_i$ without a conjugate, and at least one extra distinct value, $\dw_{\dist'}'$, for which no $\dw_{\dist'}$ exists. This (these) distinct term(s) cancel(s) out all the other values in the expectations. \AH{Moving on...}Note that $\dw_1\ldots\dw_\dist, \dw_1'\ldots\dw_{\dist'}'$ are distinct world values such that $\forall i \neq j \in [\dist], \dw_i = \dw_i' \neq \dw_j = \dw_j'$. To make things easier, assume that $\dist < \dist'$. The opposite case of $\dist > \dist'$ has a symmetrical proof. Fixing variables $\dw_1\ldots\dw_\dist, \dw_1'\ldots\dw'_{\dist'}$, we have at least one $\dw_i$ without a conjugate, and at least one extra distinct value, $\dw_{\dist'}'$, for which no $\dw_{\dist'}$ exists. This (these) distinct term(s) cancel(s) out all the other values in the expectations.
\begin{align} \begin{align}
@ -297,8 +298,7 @@ Observe that $\forall \dist \in [\prodsize], \sum_{i = 1}^{\dist}|\surj^{-1}(i)|
= &\ex{\left(\prod_{i = 1}^{\dist}\sine(\dw_{i})^{|\surj^{-1}(i)|}\right) \cdot \left(\prod_{j = 1}^{\dist}\conj{\sine(\dw'_{j})}^{|\surj^{-1}(j)|}\right)} \cdot \prod_{l = \dist + 1}^{\dist'} \ex{\conj{\sine(\dw_l)}^{|\surj^{-1}(l)|}} = 0.\label{eq:lem-fmatch-pt1} = &\ex{\left(\prod_{i = 1}^{\dist}\sine(\dw_{i})^{|\surj^{-1}(i)|}\right) \cdot \left(\prod_{j = 1}^{\dist}\conj{\sine(\dw'_{j})}^{|\surj^{-1}(j)|}\right)} \cdot \prod_{l = \dist + 1}^{\dist'} \ex{\conj{\sine(\dw_l)}^{|\surj^{-1}(l)|}} = 0.\label{eq:lem-fmatch-pt1}
\end{align} \end{align}
In \cref{eq:lem-fmatch-pt1} the expectation can be pushed through the last product group since we know that all the operands are distinct from any others appearing in the overall product. Then, by \cref{lem:exp-sine} we get $0$ for that rightmost term, and this cancels out the rest of the terms in the overall product. In \cref{eq:lem-fmatch-pt1} the expectation can be pushed through the last product group since we know that all the operands are distinct from any others appearing in the overall product. Then, by \cref{lem:exp-sine} we get $0$ for that rightmost term, and this cancels out the rest of the terms in the overall product.
\textit{Here at most we assume 2k wise independence, but we really would like less}.
\AH{Can we bring it down to k-wise, since we have $<$ k terms which we are pushing the expectation through?} \AH{Can we bring it down to k-wise, since we have $<$ k terms which we are pushing the expectation through?}
To complete the proof, we now approach the case where $\dist = \dist'$, but there is a $\dw_i, \dw_i'$ with an unequal number of mappings. To complete the proof, we now approach the case where $\dist = \dist'$, but there is a $\dw_i, \dw_i'$ with an unequal number of mappings.
@ -317,16 +317,16 @@ Let $n = \{i ~|~ |\surj^{-1}(i)| \neq |\surj'^{-1}(i)|\}$. Further, let $\dist_
\begin{align} \begin{align}
\term_1 = &\ex{\left(\prod_{i \in [\dist_*]} \sine(\dw_i)^{|\surj^{-1}(i)|} \conj{\sine(\dw'_i)}^{|\surj'^{-1}(i)|}\right) \term_1 = &\ex{\left(\prod_{i \in [\dist_*]} \sine(\dw_i)^{|\surj^{-1}(i)|} \conj{\sine(\dw'_i)}^{|\surj'^{-1}(i)|}\right)
\left(\prod_{j \in [n]}\sine(\dw_i)^{|\surj^{*-1}|} \conj{\sine(\dw'_i)}^{|\surj^{*-1}|}\right) \left(\prod_{j \in [n]}\sine(\dw_i)^{|\surj^{*-1}(j)|} \conj{\sine(\dw'_i)}^{|\surj^{*-1}(j)|}\right)
\left(\prod_{\substack{i' \in [n],\\\surj^{-1}(i') > \surj'^{-1}(i')}} \sine(\dw_{i'})^{|\surj^{-1}(i')| - |\surj'^{-1}(i')|} \prod_{\substack{j' \in n ~|~\\ \surj'^{-1}('j) > \surj^{-1}(j')}} \conj{\sine(\dw'_{j'})}^{|\surj'^{-1}(j')| - |\surj^{-1}(j')|}\right)} \label{eq:lem-match-pt2-line1}\\ \left(\prod_{\substack{i' \in [n],\\\surj^{-1}(i') > \surj'^{-1}(i')}} \sine(\dw_{i'})^{|\surj^{-1}(i')| - |\surj'^{-1}(i')|} \prod_{\substack{j' \in n ~|~\\ \surj'^{-1}('j) > \surj^{-1}(j')}} \conj{\sine(\dw'_{j'})}^{|\surj'^{-1}(j')| - |\surj^{-1}(j')|}\right)} \label{eq:lem-match-pt2-line1}\\
= &\ex{\left(\prod_{i \in [\dist_*]} \sine(\dw_i)^{|\surj^{-1}(i)|} \conj{\sine(\dw'_i)}^{|\surj'^{-1}(i)|}\right) = &\ex{\left(\prod_{i \in [\dist_*]} \sine(\dw_i)^{|\surj^{-1}(i)|} \conj{\sine(\dw'_i)}^{|\surj'^{-1}(i)|}\right)
\left(\prod_{j \in [n]}\sine(\dw_i)^{|\surj^{*-1}|} \conj{\sine(\dw'_i)}^{|\surj^{*-1}|}\right)} \cdot \left(\prod_{j \in [n]}\sine(\dw_i)^{|\surj^{*-1}(j)|} \conj{\sine(\dw'_i)}^{|\surj^{*-1}(j)|}\right)} \cdot
\ex{\left(\prod_{\substack{i' \in n ~|~\\\surj^{-1}(i') > \surj'^{-1}(i')}} \sine(\dw_{i'})^{|\surj^{-1}(i')| - |\surj'^{-1}(i')|} \prod_{\substack{j' \in n ~|~\\ \surj'^{-1}('j) > \surj^{-1}(j')}} \conj{\sine(\dw'_{j'})}^{|\surj'^{-1}(j')| - |\surj^{-1}(j')|}\right)}\nonumber\\ \ex{\left(\prod_{\substack{i' \in n ~|~\\\surj^{-1}(i') > \surj'^{-1}(i')}} \sine(\dw_{i'})^{|\surj^{-1}(i')| - |\surj'^{-1}(i')|} \prod_{\substack{j' \in n ~|~\\ \surj'^{-1}('j) > \surj^{-1}(j')}} \conj{\sine(\dw'_{j'})}^{|\surj'^{-1}(j')| - |\surj^{-1}(j')|}\right)}\nonumber\\
= &\ex{\left(\prod_{i \in [\dist_*]} \sine(\dw_i)^{|\surj^{-1}(i)|} \conj{\sine(\dw'_i)}^{|\surj'^{-1}(i)|}\right) = &\ex{\left(\prod_{i \in [\dist_*]} \sine(\dw_i)^{|\surj^{-1}(i)|} \conj{\sine(\dw'_i)}^{|\surj'^{-1}(i)|}\right)
\left(\prod_{j \in [n]}\sine(\dw_i)^{|\surj^{*-1}|} \conj{\sine(\dw'_i)}^{|\surj^{*-1}|}\right)} \cdot \left(\prod_{j \in [n]}\sine(\dw_i)^{|\surj^{*-1}(j)|} \conj{\sine(\dw'_i)}^{|\surj^{*-1}(j)|}\right)} \cdot
\ex{\prod_{\substack{i' \in n ~|~\\\surj^{-1}(i') > \surj'^{-1}(i')}} \sine(\dw_{i'})^{|\surj^{-1}(i')| - |\surj'^{-1}(i')|}} \cdot \ex{\prod_{\substack{j' \in n ~|~\\ \surj'^{-1}('j) > \surj^{-1}(j')}} \conj{\sine(\dw'_{j'})}^{|\surj'^{-1}(j')| - |\surj^{-1}(j')|}}\nonumber\\ \ex{\prod_{\substack{i' \in n ~|~\\\surj^{-1}(i') > \surj'^{-1}(i')}} \sine(\dw_{i'})^{|\surj^{-1}(i')| - |\surj'^{-1}(i')|}} \cdot \ex{\prod_{\substack{j' \in n ~|~\\ \surj'^{-1}('j) > \surj^{-1}(j')}} \conj{\sine(\dw'_{j'})}^{|\surj'^{-1}(j')| - |\surj^{-1}(j')|}}\nonumber\\
= &\ex{\left(\prod_{i \in [\dist_*]} \sine(\dw_i)^{|\surj^{-1}(i)|} \conj{\sine(\dw'_i)}^{|\surj'^{-1}(i)|}\right) = &\ex{\left(\prod_{i \in [\dist_*]} \sine(\dw_i)^{|\surj^{-1}(i)|} \conj{\sine(\dw'_i)}^{|\surj'^{-1}(i)|}\right)
\left(\prod_{j \in [n]}\sine(\dw_i)^{|\surj^{*-1}|} \conj{\sine(\dw'_i)}^{|\surj^{*-1}|}\right)} \cdot \left(\prod_{j \in [n]}\sine(\dw_i)^{|\surj^{*-1}(j)|} \conj{\sine(\dw'_i)}^{|\surj^{*-1}(j)|}\right)} \cdot
\prod_{\substack{i' \in n ~|~\\\surj^{-1}(i') > \surj'^{-1}(i')}} \ex{\sine(\dw_{i'})^{|\surj^{-1}(i')| - |\surj'^{-1}(i')|}} \cdot \prod_{\substack{j' \in n ~|~\\ \surj'^{-1}('j) > \surj^{-1}(j')}} \ex{\conj{\sine(\dw'_{j'})}^{|\surj'^{-1}(j')| - |\surj^{-1}(j')|}}\label{eq:lem-match-pt2-last}\\ \prod_{\substack{i' \in n ~|~\\\surj^{-1}(i') > \surj'^{-1}(i')}} \ex{\sine(\dw_{i'})^{|\surj^{-1}(i')| - |\surj'^{-1}(i')|}} \cdot \prod_{\substack{j' \in n ~|~\\ \surj'^{-1}('j) > \surj^{-1}(j')}} \ex{\conj{\sine(\dw'_{j'})}^{|\surj'^{-1}(j')| - |\surj^{-1}(j')|}}\label{eq:lem-match-pt2-last}\\
& = 0.\nonumber & = 0.\nonumber
\end{align} \end{align}