-
Notifications
You must be signed in to change notification settings - Fork 257
/
Pi.lean
100 lines (88 loc) · 5.11 KB
/
Pi.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
/-
Copyright (c) 2023 Xavier Roblot. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Xavier Roblot
-/
import Mathlib.MeasureTheory.Constructions.Pi
import Mathlib.MeasureTheory.Constructions.Prod.Integral
/-!
# Integration with respect to a finite product of measures
On a finite product of measure spaces, we show that a product of integrable functions each
depending on a single coordinate is integrable, in `MeasureTheory.integrable_fintype_prod`, and
that its integral is the product of the individual integrals,
in `MeasureTheory.integral_fintype_prod_eq_prod`.
-/
open BigOperators Fintype MeasureTheory MeasureTheory.Measure
variable {𝕜 : Type*} [RCLike 𝕜]
namespace MeasureTheory
/-- On a finite product space in `n` variables, for a natural number `n`, a product of integrable
functions depending on each coordinate is integrable. -/
theorem Integrable.fin_nat_prod {n : ℕ} {E : Fin n → Type*}
[∀ i, MeasureSpace (E i)] [∀ i, SigmaFinite (volume : Measure (E i))]
{f : (i : Fin n) → E i → 𝕜} (hf : ∀ i, Integrable (f i)) :
Integrable (fun (x : (i : Fin n) → E i) ↦ ∏ i, f i (x i)) := by
induction n with
| zero => simp only [Nat.zero_eq, Finset.univ_eq_empty, Finset.prod_empty, volume_pi,
integrable_const_iff, one_ne_zero, pi_empty_univ, ENNReal.one_lt_top, or_true]
| succ n n_ih =>
have := ((measurePreserving_piFinSuccAbove (fun i => (volume : Measure (E i))) 0).symm)
rw [volume_pi, ← this.integrable_comp_emb (MeasurableEquiv.measurableEmbedding _)]
simp_rw [MeasurableEquiv.piFinSuccAbove_symm_apply,
Fin.prod_univ_succ, Fin.insertNth_zero]
simp only [Fin.zero_succAbove, cast_eq, Function.comp_def, Fin.cons_zero, Fin.cons_succ]
have : Integrable (fun (x : (j : Fin n) → E (Fin.succ j)) ↦ ∏ j, f (Fin.succ j) (x j)) :=
n_ih (fun i ↦ hf _)
exact Integrable.prod_mul (hf 0) this
/-- On a finite product space, a product of integrable functions depending on each coordinate is
integrable. Version with dependent target. -/
theorem Integrable.fintype_prod_dep {ι : Type*} [Fintype ι] {E : ι → Type*}
{f : (i : ι) → E i → 𝕜} [∀ i, MeasureSpace (E i)] [∀ i, SigmaFinite (volume : Measure (E i))]
(hf : ∀ i, Integrable (f i)) :
Integrable (fun (x : (i : ι) → E i) ↦ ∏ i, f i (x i)) := by
let e := (equivFin ι).symm
simp_rw [← (volume_measurePreserving_piCongrLeft _ e).integrable_comp_emb
(MeasurableEquiv.measurableEmbedding _),
← e.prod_comp, MeasurableEquiv.coe_piCongrLeft, Function.comp_def,
Equiv.piCongrLeft_apply_apply]
exact .fin_nat_prod (fun i ↦ hf _)
/-- On a finite product space, a product of integrable functions depending on each coordinate is
integrable. -/
theorem Integrable.fintype_prod {ι : Type*} [Fintype ι] {E : Type*}
{f : ι → E → 𝕜} [MeasureSpace E] [SigmaFinite (volume : Measure E)]
(hf : ∀ i, Integrable (f i)) :
Integrable (fun (x : ι → E) ↦ ∏ i, f i (x i)) :=
Integrable.fintype_prod_dep hf
/-- A version of **Fubini's theorem** in `n` variables, for a natural number `n`. -/
theorem integral_fin_nat_prod_eq_prod {n : ℕ} {E : Fin n → Type*}
[∀ i, MeasureSpace (E i)] [∀ i, SigmaFinite (volume : Measure (E i))]
(f : (i : Fin n) → E i → 𝕜) :
∫ x : (i : Fin n) → E i, ∏ i, f i (x i) = ∏ i, ∫ x, f i x := by
induction n with
| zero =>
simp only [Nat.zero_eq, volume_pi, Finset.univ_eq_empty, Finset.prod_empty, integral_const,
pi_empty_univ, ENNReal.one_toReal, smul_eq_mul, mul_one, pow_zero, one_smul]
| succ n n_ih =>
calc
_ = ∫ x : E 0 × ((i : Fin n) → E (Fin.succ i)),
f 0 x.1 * ∏ i : Fin n, f (Fin.succ i) (x.2 i) := by
rw [volume_pi, ← ((measurePreserving_piFinSuccAbove
(fun i => (volume : Measure (E i))) 0).symm).integral_comp']
simp_rw [MeasurableEquiv.piFinSuccAbove_symm_apply,
Fin.prod_univ_succ, Fin.insertNth_zero, Fin.cons_succ]
rfl
_ = (∫ x, f 0 x) * ∏ i : Fin n, ∫ (x : E (Fin.succ i)), f (Fin.succ i) x := by
rw [← n_ih, ← integral_prod_mul, volume_eq_prod]
_ = ∏ i, ∫ x, f i x := by rw [Fin.prod_univ_succ]
/-- A version of **Fubini's theorem** with the variables indexed by a general finite type. -/
theorem integral_fintype_prod_eq_prod (ι : Type*) [Fintype ι] {E : ι → Type*}
(f : (i : ι) → E i → 𝕜) [∀ i, MeasureSpace (E i)] [∀ i, SigmaFinite (volume : Measure (E i))] :
∫ x : (i : ι) → E i, ∏ i, f i (x i) = ∏ i, ∫ x, f i x := by
let e := (equivFin ι).symm
rw [← (volume_measurePreserving_piCongrLeft _ e).integral_comp']
simp_rw [← e.prod_comp, MeasurableEquiv.coe_piCongrLeft, Equiv.piCongrLeft_apply_apply,
MeasureTheory.integral_fin_nat_prod_eq_prod]
theorem integral_fintype_prod_eq_pow {E : Type*} (ι : Type*) [Fintype ι] (f : E → 𝕜)
[MeasureSpace E] [SigmaFinite (volume : Measure E)] :
∫ x : ι → E, ∏ i, f (x i) = (∫ x, f x) ^ (card ι) := by
rw [integral_fintype_prod_eq_prod, Finset.prod_const, card]
end MeasureTheory