Lean: integrals of power functions on Fin 1 → ℝ and ∫⁻ notation precedence
To compute averages of t^c over dyadic cubes or balls in Fin 1 → ℝ, pull back along MeasurableEquiv.funUnique (Fin 1) ℝ. Use (volume_preserving_funUnique (Fin 1) ℝ).setLIntegral_comp_preimage_emb (MeasurableEquiv.funUnique _ _).measurableEmbedding g s, and finish with exact, not rw, because funUnique x is x 0 only up to defeq. Express the cube as a preimage via cube_eq_pi + simp [Set.mem_pi, Fin.forall_fin_one], and the ball via ball_pi c hr + Real.ball_eq_Ioo. On ℝ, ∫⁻ t in Ioo 0 b, ofReal t ^ (c-1) = ofReal (b^c/c) follows from ofReal_integral_eq_lintegral_ofReal, intervalIntegral.integral_of_le, integral_rpow and intervalIntegrable_rpow', after replacing Ioo by Ioc with setLIntegral_congr Ioo_ae_eq_Ioc. Gotcha: ∫⁻ t in s, g t + ∫⁻ t in u, g t parses the + inside the first integrand. Parenthesize the first integral, or rw and exact lintegral_union_le _ _ _ fail with puzzling mismatches.
Names checked on Mathlib v4.35.0:
volume_preserving_funUnique,MeasurePreserving.setLIntegral_comp_preimage_emb,ball_pi,Real.ball_eq_Ioo,setLIntegral_congr,Ioo_ae_eq_Ioc,ofReal_integral_eq_lintegral_ofReal,integral_rpowandlintegral_union_leall exist.intervalIntegrable_rpow'isintervalIntegral.intervalIntegrable_rpow'(needsopen intervalIntegral), andcube_eq_piis not in Mathlib, so it must come from your own dyadic-cube file. The precedence gotcha holds:(∫⁻ t in s, g t + ∫⁻ t in u, g t) = ∫⁻ t in s, (g t + ∫⁻ t in u, g t)isrfl.