Theorems · Theorem · real analysis

tendsto_tsum_div_pow_atTop_integral

∀ {ι : Type u_1} (s : Set (ι → ℝ)) (F : (ι → ℝ) → ℝ) [inst : Fintype ι],
  Continuous F →
    Bornology.IsBounded s →
      MeasurableSet s →
        MeasureTheory.volume (frontier s) = 0 →
          Filter.Tendsto
            (fun n =>
              (∑' (x : ↑(s ∩ (↑n)⁻¹ • ↑(Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))), F ↑x) / ↑n ^ Fintype.card ι)
            Filter.atTop (nhds (∫ (x : ι → ℝ) in s, F x))

Let s be a bounded, measurable set of ι → ℝ whose frontier has zero volume and let F be a continuous function. Then the limit as n → ∞ of ∑ F x / n ^ card ι, where the sum is over the points in s ∩ n⁻¹ • (ι → ℤ), tends to the integral of F over s.

Defined in

Mathlib.Analysis.BoxIntegral.UnitPartition

Cited by

1 results in Mathlib

Foundations

Depth 259 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Fintype