ι : Type u
E : Type v
F : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
I J✝ : Box ι
π✝ : TaggedPrepartition I
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π : TaggedPrepartition I
πi : (J : Box ι) → Prepartition J
hπi : ∀ (J : Box ι), J ∈ π → Prepartition.IsPartition (πi J)
J : Box ι
hJ : J ∈ π.boxes
⊢ ∑ J' in (πi J).boxes, ↑(↑vol J') (f (tag (biUnionPrepartition π πi) J')) = ↑(↑vol J) (f (tag π J))
ι : Type u
E : Type v
F : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
I J : Box ι
π✝ : TaggedPrepartition I
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π : TaggedPrepartition I
πi : (J : Box ι) → Prepartition J
hπi : ∀ (J : Box ι), J ∈ π → Prepartition.IsPartition (πi J)
⊢ integralSum f vol (biUnionPrepartition π πi) = integralSum f vol π
refine' (π.sum_biUnion_boxes _ _).trans (sum_congr rfl fun J hJ => _)
no goals
ι : Type u
E : Type v
F : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
I J✝ : Box ι
π✝ : TaggedPrepartition I
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π : TaggedPrepartition I
πi : (J : Box ι) → Prepartition J
hπi : ∀ (J : Box ι), J ∈ π → Prepartition.IsPartition (πi J)
J : Box ι
hJ : J ∈ π.boxes
⊢ ∑ J' in (πi J).boxes, ↑(↑vol J') (f (tag (biUnionPrepartition π πi) J')) = ↑(↑vol J) (f (tag π J))
calc
  (∑ J' in (πi J).boxes, vol J' (f (π.tag <| π.toPrepartition.biUnionIndex πi J'))) =
      ∑ J' in (πi J).boxes, vol J' (f (π.tag J)) :=
    sum_congr rfl fun J' hJ' => by rw [Prepartition.biUnionIndex_of_mem _ hJ hJ']
  _ = vol J (f (π.tag J)) :=
    (vol.map ⟨⟨fun g : E →L[ℝ] F => g (f (π.tag J)), rfl⟩, fun _ _ => rfl⟩).sum_partition_boxes
      le_top (hπi J hJ)
no goals
ι : Type u
E : Type v
F : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
I J✝ : Box ι
π✝ : TaggedPrepartition I
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π : TaggedPrepartition I
πi : (J : Box ι) → Prepartition J
hπi : ∀ (J : Box ι), J ∈ π → Prepartition.IsPartition (πi J)
J : Box ι
hJ : J ∈ π.boxes
J' : Box ι
hJ' : J' ∈ (πi J).boxes
⊢ ↑(↑vol J') (f (tag π (Prepartition.biUnionIndex π.toPrepartition πi J'))) = ↑(↑vol J') (f (tag π J))
rw [Prepartition.biUnionIndex_of_mem _ hJ hJ']