From a grid inequality to an integral inequality in Lean: average over the grid offset

If you prove a lower bound for a mean over a dyadic grid, ∑_{i,j<M} G((i+θ₁)/M, (j+θ₂)/M) ≥ c, and the proof works for every offset θ ∈ [0,1)^2, you get ∫₀¹∫₀¹ G ≥ c/M² with little measure theory. 1D change of variables: ∫₀¹ g = ∑_{i<M} (1/M) ∫₀¹ g((i+θ)/M) dθ. Get it from intervalIntegral.sum_integral_adjacent_intervals with a k = k/M, then intervalIntegral.integral_comp_add_div (f := g) (a := 0) (b := 1) hM.ne' (i/M), which gives ∫₀¹ g(d + θ/M) = M • ∫_{d}^{d+1/M} g. Apply it twice. For the inner integral F(x) = ∫₀¹ G(x,y) dy you need measurability once: StronglyMeasurable.integral_prod_right' with ν := volume.restrict (Ioc 0 1), after intervalIntegral.integral_of_le. Integrability: bounded + measurable via Measure.integrableOn_of_bounded. Swap sums and integrals with intervalIntegral.integral_finsetSum (integral_finset_sum is deprecated). IntervalIntegrable.sum gives integrability of the Pi-sum (∑ i, f i). Convert it to fun θ ↦ ∑ i, f i θ by convert + Finset.sum_apply. The bound fails at θ = 1, so use integral_mono_ae_restrict, not integral_mono_ae: integral_mono_ae wants the inequality a.e. on all of ℝ. Then filter_upwards [ae_restrict_mem measurableSet_Icc, ae_restrict_of_ae ae_ne_one], with ae_ne_one proved by rw [ae_iff]; simp. Pitfall: hmeas.comp (measurable_const.prodMk measurable_id) for the section y ↦ G x y hit a whnf heartbeat timeout. (hmeas).comp (measurable_prodMk_left (x := x) (β := ℝ)) was instant.