Haar-product integrability for one lifted Green edge

This deterministic helper adjoins one translated Green edge to an integrable function on an arbitrary SFinite measure space. It is the common induction step for both deterministic increasing Green trees and random-parametrix Green paths, so it lives below both layers.

theorem Anderson4D.integrable_greenFn_sub_mul_lift {Y : Type u_1} [MeasurableSpace Y] {ν : MeasureTheory.Measure Y} [MeasureTheory.SFinite ν] (f : Y → ℂ) (shift : Y → T4) (hf : MeasureTheory.Integrable f ν) (hshift : Measurable shift) : MeasureTheory.Integrable (fun (p : T4 × Y) => ↑(greenFn (p.1 - shift p.2)) * f p.2) (paperMeasure.prod ν)

Multiplying an integrable function by a translated Green kernel in a new Haar variable preserves joint integrability. The translation may depend measurably on all old variables.