Theorem: integral_piSplitAt (ForML/IndexIntegral.lean)

State before:
ι : Type u_1
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
mE : MeasureSpace E
inst✝⁶ : SigmaFinite volume
D : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (D i)
inst✝⁴ : (i : ι) → NormedSpace ℝ (D i)
mD : (i : ι) → MeasureSpace (D i)
inst✝³ : ∀ (i : ι), SigmaFinite volume
F : Type u_4
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
i : ι
f : ((i : ι) → D i) → F
⊢ ∫ (x : (i : ι) → D i), f x = ∫ (p : D i × ((j : { j // j ≠ i }) → D ↑j)), f ((Equiv.piSplitAt i D).symm p)
Tactic:
have he := (MeasurableEquiv.volume_preserving_piSplitAt D i).symm
State after:
ι : Type u_1
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
mE : MeasureSpace E
inst✝⁶ : SigmaFinite volume
D : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (D i)
inst✝⁴ : (i : ι) → NormedSpace ℝ (D i)
mD : (i : ι) → MeasureSpace (D i)
inst✝³ : ∀ (i : ι), SigmaFinite volume
F : Type u_4
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
i : ι
f : ((i : ι) → D i) → F
he : MeasurePreserving ⇑(MeasurableEquiv.piSplitAt D i).symm
⊢ ∫ (x : (i : ι) → D i), f x = ∫ (p : D i × ((j : { j // j ≠ i }) → D ↑j)), f ((Equiv.piSplitAt i D).symm p)

State before:
ι : Type u_1
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
mE : MeasureSpace E
inst✝⁶ : SigmaFinite volume
D : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (D i)
inst✝⁴ : (i : ι) → NormedSpace ℝ (D i)
mD : (i : ι) → MeasureSpace (D i)
inst✝³ : ∀ (i : ι), SigmaFinite volume
F : Type u_4
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
i : ι
f : ((i : ι) → D i) → F
he : MeasurePreserving ⇑(MeasurableEquiv.piSplitAt D i).symm
⊢ ∫ (x : (i : ι) → D i), f x = ∫ (p : D i × ((j : { j // j ≠ i }) → D ↑j)), f ((Equiv.piSplitAt i D).symm p)
Tactic:
rw [← he.map_eq]
State after:
ι : Type u_1
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
mE : MeasureSpace E
inst✝⁶ : SigmaFinite volume
D : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (D i)
inst✝⁴ : (i : ι) → NormedSpace ℝ (D i)
mD : (i : ι) → MeasureSpace (D i)
inst✝³ : ∀ (i : ι), SigmaFinite volume
F : Type u_4
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
i : ι
f : ((i : ι) → D i) → F
he : MeasurePreserving ⇑(MeasurableEquiv.piSplitAt D i).symm
⊢ ∫ (x : (i : ι) → D i), f x ∂Measure.map (⇑(MeasurableEquiv.piSplitAt D i).symm) volume =
    ∫ (p : D i × ((j : { j // j ≠ i }) → D ↑j)), f ((Equiv.piSplitAt i D).symm p)

State before:
ι : Type u_1
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
mE : MeasureSpace E
inst✝⁶ : SigmaFinite volume
D : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (D i)
inst✝⁴ : (i : ι) → NormedSpace ℝ (D i)
mD : (i : ι) → MeasureSpace (D i)
inst✝³ : ∀ (i : ι), SigmaFinite volume
F : Type u_4
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
i : ι
f : ((i : ι) → D i) → F
he : MeasurePreserving ⇑(MeasurableEquiv.piSplitAt D i).symm
⊢ ∫ (x : (i : ι) → D i), f x ∂Measure.map (⇑(MeasurableEquiv.piSplitAt D i).symm) volume =
    ∫ (p : D i × ((j : { j // j ≠ i }) → D ↑j)), f ((Equiv.piSplitAt i D).symm p)
Tactic:
rw [integral_map_equiv]
State after:
ι : Type u_1
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
mE : MeasureSpace E
inst✝⁶ : SigmaFinite volume
D : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (D i)
inst✝⁴ : (i : ι) → NormedSpace ℝ (D i)
mD : (i : ι) → MeasureSpace (D i)
inst✝³ : ∀ (i : ι), SigmaFinite volume
F : Type u_4
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
i : ι
f : ((i : ι) → D i) → F
he : MeasurePreserving ⇑(MeasurableEquiv.piSplitAt D i).symm
⊢ ∫ (x : D i × ((j : { j // j ≠ i }) → D ↑j)), f ((MeasurableEquiv.piSplitAt D i).symm x) ∂volume =
    ∫ (p : D i × ((j : { j // j ≠ i }) → D ↑j)), f ((Equiv.piSplitAt i D).symm p)

State before:
ι : Type u_1
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
mE : MeasureSpace E
inst✝⁶ : SigmaFinite volume
D : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (D i)
inst✝⁴ : (i : ι) → NormedSpace ℝ (D i)
mD : (i : ι) → MeasureSpace (D i)
inst✝³ : ∀ (i : ι), SigmaFinite volume
F : Type u_4
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
i : ι
f : ((i : ι) → D i) → F
he : MeasurePreserving ⇑(MeasurableEquiv.piSplitAt D i).symm
⊢ ∫ (x : D i × ((j : { j // j ≠ i }) → D ↑j)), f ((MeasurableEquiv.piSplitAt D i).symm x) ∂volume =
    ∫ (p : D i × ((j : { j // j ≠ i }) → D ↑j)), f ((Equiv.piSplitAt i D).symm p)
Tactic:
rw [Measure.volume_eq_prod]
State after:
ι : Type u_1
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
mE : MeasureSpace E
inst✝⁶ : SigmaFinite volume
D : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (D i)
inst✝⁴ : (i : ι) → NormedSpace ℝ (D i)
mD : (i : ι) → MeasureSpace (D i)
inst✝³ : ∀ (i : ι), SigmaFinite volume
F : Type u_4
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
i : ι
f : ((i : ι) → D i) → F
he : MeasurePreserving ⇑(MeasurableEquiv.piSplitAt D i).symm
⊢ ∫ (x : D i × ((j : { j // j ≠ i }) → D ↑j)), f ((MeasurableEquiv.piSplitAt D i).symm x) ∂Measure.prod volume volume =
    ∫ (p : D i × ((j : { j // j ≠ i }) → D ↑j)), f ((Equiv.piSplitAt i D).symm p) ∂Measure.prod volume volume

State before:
ι : Type u_1
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
mE : MeasureSpace E
inst✝⁶ : SigmaFinite volume
D : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (D i)
inst✝⁴ : (i : ι) → NormedSpace ℝ (D i)
mD : (i : ι) → MeasureSpace (D i)
inst✝³ : ∀ (i : ι), SigmaFinite volume
F : Type u_4
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
i : ι
f : ((i : ι) → D i) → F
he : MeasurePreserving ⇑(MeasurableEquiv.piSplitAt D i).symm
⊢ ∫ (x : D i × ((j : { j // j ≠ i }) → D ↑j)), f ((MeasurableEquiv.piSplitAt D i).symm x) ∂Measure.prod volume volume =
    ∫ (p : D i × ((j : { j // j ≠ i }) → D ↑j)), f ((Equiv.piSplitAt i D).symm p) ∂Measure.prod volume volume
Tactic:
simp only [MeasurableEquiv.piSplitAt_symm_apply]
State after:
no goals