Support Disjointness and Orthogonality

When t > 2L, the intervals (-L, L) and (-L + t, L + t) are disjoint, so zeroExtend G I and S_t(zeroExtend G I) have disjoint support. This gives the Pythagorean identity ‖G̃ - S_t G̃‖² = 2‖G‖² which saturates the unitary identity bound.

Reference: lamportform.tex, Section 2, Remark 2.

Interval disjointness

theorem ConnesLean.Ioo_disjoint_shift {L t : ℝ} (_hL : 0 < L) (ht : 2 * L < t) : Disjoint (Set.Ioo (-L) L) (Set.Ioo (-L + t) (L + t))

When t > 2 * L and L > 0, the intervals (-L, L) and (-L + t, L + t) are disjoint. This is because the right endpoint of (-L, L) is L, while the left endpoint of (-L + t, L + t) is -L + t > -L + 2L = L.

theorem ConnesLean.translationOp_zeroExtend_eq_zero {G : ℝ → ℂ} {a b t u : ℝ} (hu : u ∉ Set.Ioo (a + t) (b + t)) : translationOp t (zeroExtend G (Set.Ioo a b)) u = 0

The support of translationOp t (zeroExtend G I) is contained in the shifted interval. Specifically, if I = Ioo a b, then translationOp t (zeroExtend G I) vanishes outside Ioo (a + t) (b + t).

Pointwise product vanishing and norm identities

theorem ConnesLean.pointwise_mul_zero_of_large_shift {G : ℝ → ℂ} {L t : ℝ} (_hL : 0 < L) (ht : 2 * L < t) (u : ℝ) : zeroExtend G (logInterval L) u * (starRingEnd ℂ) (translationOp t (zeroExtend G (logInterval L)) u) = 0

When t > 2L and L > 0, the zero-extended function and its translation have disjoint support. Their pointwise product vanishes everywhere.

theorem ConnesLean.lintegral_norm_sub_eq_add_of_large_shift {G : ℝ → ℂ} {L t : ℝ} (_hL : 0 < L) (ht : 2 * L < t) (hG : Measurable G) : ∫⁻ (u : ℝ), ↑‖zeroExtend G (logInterval L) u - translationOp t (zeroExtend G (logInterval L)) u‖₊ ^ 2 = (∫⁻ (u : ℝ), ↑‖zeroExtend G (logInterval L) u‖₊ ^ 2) + ∫⁻ (u : ℝ), ↑‖translationOp t (zeroExtend G (logInterval L)) u‖₊ ^ 2

The L² norm of zeroExtend G I - translationOp t (zeroExtend G I) when t > 2L: the squared norm of the difference equals the sum of squared norms (Pythagorean identity from disjoint support).

‖G̃ - S_t G̃‖² = ‖G̃‖² + ‖S_t G̃‖²

theorem ConnesLean.lintegral_norm_translationOp_zeroExtend (t : ℝ) (G : ℝ → ℂ) (I : Set ℝ) : ∫⁻ (u : ℝ), ↑‖translationOp t (zeroExtend G I) u‖₊ ^ 2 = ∫⁻ (u : ℝ), ↑‖zeroExtend G I u‖₊ ^ 2

When t > 2L, the squared norm of the translated function equals the original: ‖S_t G̃‖² = ‖G̃‖², by translation invariance of Lebesgue measure. Combined with the Pythagorean identity, this gives ‖G̃ - S_t G̃‖² = 2‖G̃‖².