internlm/Lean-Github huggingface dataset:
Theorem: iteratedDeriv_pow
Proof state before:
case succ.h.refine_2
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n i : ℕ
IH : (iteratedDeriv i fun x => x ^ n) = fun x => ↑(Nat.descFactorial n i) * x ^ (n - i)
x : 𝕜
⊢ x ^ (n - i - 1) = x ^ (n - Nat.succ i)
Tactic:
simp [Nat.sub_succ']
Proof state after:
no goals
Theorem: iteratedDeriv_neg'
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜'
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : SMulCommClass 𝕜 𝕜' F
i : ℕ
f : 𝕜 → F
x : 𝕜
hf : ContDiff 𝕜 (↑i) f
⊢ iteratedDeriv i (fun x => -f x) x = -iteratedDeriv i f x
Tactic:
simpa [iteratedDerivWithin_univ] using
  iteratedDerivWithin_neg' (Set.mem_univ x) uniqueDiffOn_univ (contDiffOn_univ.mpr hf)
Proof state after:
no goals
Theorem: iteratedDeriv_const_smul'
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜'
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : SMulCommClass 𝕜 𝕜' F
i : ℕ
c : 𝕜'
f : 𝕜 → F
x : 𝕜
hf : ContDiff 𝕜 (↑i) f
⊢ iteratedDeriv i (fun x => c • f x) x = c • iteratedDeriv i f x
Tactic:
simp only [iteratedDeriv_eq_iteratedFDeriv, ← Pi.smul_def]
Proof state after:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜'
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : SMulCommClass 𝕜 𝕜' F
i : ℕ
c : 𝕜'
f : 𝕜 → F
x : 𝕜
hf : ContDiff 𝕜 (↑i) f
⊢ ((iteratedFDeriv 𝕜 i (c • fun i => f i) x) fun x => 1) = c • (iteratedFDeriv 𝕜 i f x) fun x => 1
Theorem: iteratedDeriv_const_smul'
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜'
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : SMulCommClass 𝕜 𝕜' F
i : ℕ
c : 𝕜'
f : 𝕜 → F
x : 𝕜
hf : ContDiff 𝕜 (↑i) f
⊢ ((iteratedFDeriv 𝕜 i (c • fun i => f i) x) fun x => 1) = c • (iteratedFDeriv 𝕜 i f x) fun x => 1
Tactic:
rw [iteratedFDeriv_const_smul_apply hf]
Proof state after:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜'
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : SMulCommClass 𝕜 𝕜' F
i : ℕ
c : 𝕜'
f : 𝕜 → F
x : 𝕜
hf : ContDiff 𝕜 (↑i) f
⊢ ((c • iteratedFDeriv 𝕜 i f x) fun x => 1) = c • (iteratedFDeriv 𝕜 i f x) fun x => 1
Theorem: iteratedDeriv_const_smul'
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜'
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : SMulCommClass 𝕜 𝕜' F
i : ℕ
c : 𝕜'
f : 𝕜 → F
x : 𝕜
hf : ContDiff 𝕜 (↑i) f
⊢ ((c • iteratedFDeriv 𝕜 i f x) fun x => 1) = c • (iteratedFDeriv 𝕜 i f x) fun x => 1
Tactic:
simp
Proof state after:
no goals
Theorem: integral_piSplitAt
Proof 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
Proof 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)
Theorem: integral_piSplitAt
Proof 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]
Proof 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)
Theorem: integral_piSplitAt
Proof 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]
Proof 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)
Theorem: integral_piSplitAt
Proof 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]
Proof 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
Theorem: integral_piSplitAt
Proof 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]
Proof state after:
no goals
Theorem: integral_funSplitAt
Proof 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 : (ι → E) → F
⊢ ∫ (x : ι → E), f x = ∫ (p : E × ({ j // j ≠ i } → E)), f ((Equiv.funSplitAt i E).symm p)
Tactic:
rw [integral_piSplitAt i]
Proof 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 : (ι → E) → F
⊢ ∫ (p : E × ({ j // j ≠ i } → E)), f ((Equiv.piSplitAt i fun a => E).symm p) =
    ∫ (p : E × ({ j // j ≠ i } → E)), f ((Equiv.funSplitAt i E).symm p)
Theorem: integral_funSplitAt
Proof 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 : (ι → E) → F
⊢ ∫ (p : E × ({ j // j ≠ i } → E)), f ((Equiv.piSplitAt i fun a => E).symm p) =
    ∫ (p : E × ({ j // j ≠ i } → E)), f ((Equiv.funSplitAt i E).symm p)
Tactic:
rfl
Proof state after:
no goals
Theorem: MeasureTheory.Integrable.piSplitAt
Proof 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
hf : Integrable f
⊢ Integrable fun p => f ((Equiv.piSplitAt i D).symm p)
Tactic:
simp_rw [← MeasurableEquiv.piSplitAt_symm_apply]
Proof 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
hf : Integrable f
⊢ Integrable fun p => f ((MeasurableEquiv.piSplitAt D i).symm p)
Theorem: MeasureTheory.Integrable.piSplitAt
Proof 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
hf : Integrable f
⊢ Integrable fun p => f ((MeasurableEquiv.piSplitAt D i).symm p)
Tactic:
change Integrable (f ∘ ((MeasurableEquiv.piSplitAt D i).symm)) _
Proof 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
hf : Integrable f
⊢ Integrable (f ∘ ⇑(MeasurableEquiv.piSplitAt D i).symm)
Theorem: MeasureTheory.Integrable.piSplitAt
Proof 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
hf : Integrable f
⊢ Integrable (f ∘ ⇑(MeasurableEquiv.piSplitAt D i).symm)
Tactic:
rw [← integrable_map_equiv]
Proof 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
hf : Integrable f
⊢ Integrable f
Theorem: MeasureTheory.Integrable.piSplitAt
Proof 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
hf : Integrable f
⊢ Integrable f
Tactic:
have he := (MeasurableEquiv.volume_preserving_piSplitAt D i).symm
Proof 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
hf : Integrable f
he : MeasurePreserving ⇑(MeasurableEquiv.piSplitAt D i).symm
⊢ Integrable f
Theorem: MeasureTheory.Integrable.piSplitAt
Proof 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
hf : Integrable f
he : MeasurePreserving ⇑(MeasurableEquiv.piSplitAt D i).symm
⊢ Integrable f
Tactic:
exact hf
Proof state after:
no goals
Theorem: integral_piSplitAt_left
Proof 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
hf : Integrable f
⊢ ∫ (x : (i : ι) → D i), f x = ∫ (u : D i) (x : (j : { j // j ≠ i }) → D ↑j), f ((Equiv.piSplitAt i D).symm (u, x))
Tactic:
rw [integral_piSplitAt i]
Proof 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
hf : Integrable f
⊢ ∫ (p : D i × ((j : { j // j ≠ i }) → D ↑j)), f ((Equiv.piSplitAt i fun i => D i).symm p) =
    ∫ (u : D i) (x : (j : { j // j ≠ i }) → D ↑j), f ((Equiv.piSplitAt i D).symm (u, x))
Theorem: integral_piSplitAt_left
Proof 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
hf : Integrable f
⊢ ∫ (p : D i × ((j : { j // j ≠ i }) → D ↑j)), f ((Equiv.piSplitAt i fun i => D i).symm p) =
    ∫ (u : D i) (x : (j : { j // j ≠ i }) → D ↑j), f ((Equiv.piSplitAt i D).symm (u, x))
Tactic:
rw [Measure.volume_eq_prod]
Proof 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
hf : Integrable f
⊢ ∫ (p : D i × ((j : { j // j ≠ i }) → D ↑j)), f ((Equiv.piSplitAt i fun i => D i).symm p) ∂Measure.prod volume volume =
    ∫ (u : D i) (x : (j : { j // j ≠ i }) → D ↑j), f ((Equiv.piSplitAt i D).symm (u, x))
Theorem: integral_piSplitAt_left
Proof 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
hf : Integrable f
⊢ ∫ (p : D i × ((j : { j // j ≠ i }) → D ↑j)), f ((Equiv.piSplitAt i fun i => D i).symm p) ∂Measure.prod volume volume =
    ∫ (u : D i) (x : (j : { j // j ≠ i }) → D ↑j), f ((Equiv.piSplitAt i D).symm (u, x))
Tactic:
rw [integral_prod _ (hf.piSplitAt i)]
Proof state after:
no goals
Theorem: integral_piSplitAt_right
Proof 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
hf : Integrable f
⊢ ∫ (x : (i : ι) → D i), f x = ∫ (x : (j : { j // j ≠ i }) → D ↑j) (u : D i), f ((Equiv.piSplitAt i D).symm (u, x))
Tactic:
rw [integral_piSplitAt_left i hf]
Proof 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
hf : Integrable f
⊢ ∫ (u : D i) (x : (j : { j // j ≠ i }) → D ↑j), f ((Equiv.piSplitAt i fun i => D i).symm (u, x)) =
    ∫ (x : (j : { j // j ≠ i }) → D ↑j) (u : D i), f ((Equiv.piSplitAt i D).symm (u, x))
Theorem: integral_piSplitAt_right
Proof 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
hf : Integrable f
⊢ ∫ (u : D i) (x : (j : { j // j ≠ i }) → D ↑j), f ((Equiv.piSplitAt i fun i => D i).symm (u, x)) =
    ∫ (x : (j : { j // j ≠ i }) → D ↑j) (u : D i), f ((Equiv.piSplitAt i D).symm (u, x))
Tactic:
rw [integral_integral_swap]
Proof state after:
case hf
ι : 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
hf : Integrable f
⊢ Integrable (Function.uncurry fun u x => f ((Equiv.piSplitAt i fun i => D i).symm (u, x)))