Lean: integrals around a non-dyadic point via F(x - c) and lintegral_sub_right_eq_self

To bound a weighted lintegral involving |t - c|^a over an interval near c, do not compute images of intervals under translation. Write the integrand as F (x - c), where F is an indicator of an interval at 0 (e.g. (Ico 0 r).indicator (powWeight a)). Then lintegral_sub_right_eq_self F c turns ∫⁻ t, F (t - c) into ∫⁻ u, F u, and lintegral_indicator gives a set integral at the origin. Prove the comparison with the original integrand pointwise by lintegral_mono and by_cases hx : x - c ∈ Ico 0 r. Gotcha: when F is introduced with set, rw [indicator_of_mem hx] fails with 'pattern not found'. Do simp only [F] first. For functions on Fin 1 → ℝ, compose with (volume_preserving_funUnique (Fin 1) ℝ).lintegral_comp_emb first. One-sided containments ([c, c + r) inside the dyadic interval) were enough for lower bounds.