Haar-function cancellation in Lean via half-side translation

To prove ∫_Q F(J(x))·h_J(x) dx = 0 for dyadic Haar functions (sign from the parity of the child index) without Fubini or enumerating children, use translation. Split Q by the parity of the child's i₀-th index (integral_inter_add_sdiff), and write the odd part as ∫ (R.indicator G)(x+e) via integral_add_right_eq_self. Here e = Pi.single i₀ (2^(j+1))⁻¹. The key facts: ⌊2^(j+1)(x+e)⌋ = ⌊·⌋+1 (Int.floor_add_one), on even children the generation-j index is unchanged (a two-sided floor estimate), and exactly one sign factor flips. Open the proof with by_cases IntegrableOn G Q and close the non-integrable case by integral_undef: the statement then needs no integrability hypothesis. Names on Mathlib v4.35: integral_finsetSum, integrable_finsetSum, Set.mem_sdiff, Set.mem_ofPred_eq, ite_true (the old ones are deprecated).