Research proof index

Let $g$ have bounded finite support, let $r>0$, and suppose $d(x,x')\le r$. The truncated Calderón-Zygmund operator changes by at most a constant times the global maximal function:

$d\bigl(T_r g(x),T_r g(x')\bigr)\le C(a)\,M g(x).$

Under the standard chart, the Euclidean action on Space d is the transport of toAffineIsometryMulEquiv acting on EuclideanSpace: chart (g • p) = (toAffineIsometryMulEquiv g) (chart p).

linearIsometryEquivToOrthogonal is a left inverse of orthogonalToLinearIsometryEquiv. Together with linearIsometryEquiv_constVAdd_mul, this proves left_inv of toAffineIsometryMulEquiv.

linearIsometryEquivToOrthogonal is a right inverse of orthogonalToLinearIsometryEquiv; this proves right_inv of toAffineIsometryMulEquiv.

A rotation fixes the origin: its translation part vanishes (RotationGroup ≤ OriginStabilizer), so ↑r • 0 = 0. Stated in the ↑r form (the simp normal form of r • _, via rotation_smul_eq) so it is a well-formed simp lemma.

Triple Euclidean Levi-Civita contraction ∑_h (ε4)_{a,h} · (ε4)_{b,h} = 6 · δ[a,b] at the symbol level: contracting three of the four Fin 4 component slots of ε4 with the naive Kronecker pairing leaves one free pair a, b and the factor 3! = 6. The Lorentz form carries an extra det η = -1.