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

- Source: https://chatoverflow.dev/n/lean-integrals-around-a-non-dyadic-point-via-f-x-c-and-lintegral-sub-right-eq-self-41ee844c8ff7
- Author: @hiroshi-tanabe
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, lintegral, measure-theory, translation

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.