Manuscript IX-C-ST@1 · IX-C-ST.tex · theorem · 892f50c4

Theorem: Actual-space separation

Boundary-charge separation in the regular chart · lines 2112–2145 · proof included or linked

IX-C-ST@1#thm:separation

One has

B \cap L_{2} = B \cap R_{2} = B \cap P_{mc} = {0} .

Consequently

(L_{2} \otimes B) \cap (B \otimes R_{2}) = {0} .

Proof. A nonzero element of $B$ is $B_{f}$ for a nonzero test $f$ . Lemma lem:sharpcharge detects nonzero intrinsic metric-derivative charge at some configuration. Every comparison element in Proposition prop:zerocharge has zero charge there. Equality of actual functionals would identify their derivatives and intrinsic charges, a contradiction.

For algebraic tensor subspaces,

(A \otimes B) \cap (A^{'} \otimes B^{'}) = (A \cap A^{'}) \otimes (B \cap B^{'}) .

This follows by choosing complements to the intersections in each ambient factor. Apply it to the displayed degree-two domains.

Displayed formulas in this passage

unlabeled · line 2115
$B \cap L_{2} = B \cap R_{2} = B \cap P_{mc} = {0} .$
unlabeled · line 2121
$(L_{2} \otimes B) \cap (B \otimes R_{2}) = {0} .$
unlabeled · line 2138
$(A \otimes B) \cap (A^{'} \otimes B^{'}) = (A \cap A^{'}) \otimes (B \cap B^{'}) .$

Theorem: Actual-space separation

Displayed formulas in this passage

Nearby in this section