Theorems · Theorem · real analysis

BoxIntegral.unitPartition.integralSum_eq_tsum_div

∀ {ι : Type u_1} (n : ℕ) [inst : NeZero n] (s : Set (ι → ℝ)) (F : (ι → ℝ) → ℝ) [inst_1 : Fintype ι]
  {B : BoxIntegral.Box ι},
  BoxIntegral.hasIntegralVertices B →
    s ⊆ ↑B →
      BoxIntegral.integralSum (s.indicator F) MeasureTheory.volume.toBoxAdditive.toSMul
          (BoxIntegral.unitPartition.prepartition n B) =
        (∑' (x : ↑(s ∩ (↑n)⁻¹ • ↑(Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))), F ↑x) / ↑n ^ Fintype.card ι

Defined in: Mathlib.Analysis.BoxIntegral.UnitPartition
Cited by: 1 results in Mathlib
Foundations: Depth 258 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: NeZero Fintype

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites76

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Setstatement and proof · cited by 53,352
Realstatement and proof · cited by 25,697
ENNRealproof · cited by 9,879
Top.topstatement · cited by 9,680
SetLike.coestatement and proof · cited by 8,199
Fintypestatement and proof · cited by 7,736
Submodulestatement and proof · cited by 7,192
Set.Elemstatement and proof · cited by 7,166
Finset.sumproof · cited by 5,195
Set.rangestatement and proof · cited by 4,705
WithTopstatement · cited by 3,754

Cited by1

Results whose statement or proof uses this declaration.

tendsto_tsum_div_pow_atTop_integralproof · cited by 1