[GOAL]
ι : Type u_1
I : Box ι
inst✝ : Countable ι
⊢ MeasurableSet ↑I
[PROOFSTEP]
rw [coe_eq_pi]
[GOAL]
ι : Type u_1
I : Box ι
inst✝ : Countable ι
⊢ MeasurableSet (pi univ fun i => Ioc (lower I i) (upper I i))
[PROOFSTEP]
exact MeasurableSet.univ_pi fun i => measurableSet_Ioc
[GOAL]
ι : Type u_1
I : Box ι
inst✝ : Fintype ι
⊢ ↑I =ᵐ[volume] ↑Box.Icc I
[PROOFSTEP]
rw [coe_eq_pi]
[GOAL]
ι : Type u_1
I : Box ι
inst✝ : Fintype ι
⊢ (pi univ fun i => Ioc (lower I i) (upper I i)) =ᵐ[volume] ↑Box.Icc I
[PROOFSTEP]
exact Measure.univ_pi_Ioc_ae_eq_Icc
[GOAL]
ι : Type u_1
inst✝¹ : Finite ι
I : Box ι
π : Prepartition I
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
⊢ ENNReal.toReal (↑↑μ (Prepartition.iUnion π)) = ∑ J in π.boxes, ENNReal.toReal (↑↑μ ↑J)
[PROOFSTEP]
erw [← ENNReal.toReal_sum, π.iUnion_def, measure_biUnion_finset π.pairwiseDisjoint]
[GOAL]
ι : Type u_1
inst✝¹ : Finite ι
I : Box ι
π : Prepartition I
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
⊢ ∀ (b : Box ι), b ∈ π.boxes → MeasurableSet ↑b
ι : Type u_1
inst✝¹ : Finite ι
I : Box ι
π : Prepartition I
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
⊢ ∀ (a : Box ι), a ∈ π.boxes → ↑↑μ ↑a ≠ ⊤
[PROOFSTEP]
exacts [fun J _ => J.measurableSet_coe, fun J _ => (J.measure_coe_lt_top μ).ne]
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
J : Box ι
x✝ : ↑J ≤ ⊤
π : Prepartition J
hπ : Prepartition.IsPartition π
⊢ ∑ Ji in π.boxes, (fun J => ENNReal.toReal (↑↑μ ↑J)) Ji = (fun J => ENNReal.toReal (↑↑μ ↑J)) J
[PROOFSTEP]
rw [← π.measure_iUnion_toReal, hπ.iUnion_eq]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
⊢ ↑(Measure.toBoxAdditive volume) I = ∏ i : ι, (upper I i - lower I i)
[PROOFSTEP]
rw [Measure.toBoxAdditive_apply, coe_eq_pi, Real.volume_pi_Ioc_toReal I.lower_le_upper]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
⊢ ENNReal.toReal (↑↑volume ↑I) = ∏ i : ι, (upper I i - lower I i)
[PROOFSTEP]
rw [coe_eq_pi, Real.volume_pi_Ioc_toReal I.lower_le_upper]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
n : ℕ
i : Fin (n + 1)
I : Box (Fin (n + 1))
⊢ (∏ j : Fin n, (upper (face I i) j - lower (face I i) j)) * (upper I i - lower I i) =
    ∏ j : Fin (n + 1), (upper I j - lower I j)
[PROOFSTEP]
simp only [face_lower, face_upper, (· ∘ ·), Fin.prod_univ_succAbove _ i, mul_comm]
[GOAL]
ι : Type u_1
inst✝² : Fintype ι
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
I : Box ι
x : E
⊢ ↑(↑BoxAdditiveMap.volume I) x = (∏ j : ι, (upper I j - lower I j)) • x
[PROOFSTEP]
rw [BoxAdditiveMap.volume, toSMul_apply]
[GOAL]
ι : Type u_1
inst✝² : Fintype ι
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
I : Box ι
x : E
⊢ ↑(Measure.toBoxAdditive volume) I • x = (∏ j : ι, (upper I j - lower I j)) • x
[PROOFSTEP]
exact congr_arg₂ (· • ·) I.volume_apply rfl
