From 7a4b066c3509d73d7d955a69d844ff6e2effcc5b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9my=20Degenne?= Date: Tue, 27 Sep 2022 17:24:12 +0000 Subject: [PATCH] chore(probability/martingale): use volume_tac in definitions (#16619) Use the tactic `volume_tac` in the definitions `martingale`, `submartingale`, `supermartingale`, `martingale_part` and `predictable_part`. In order to do that, change the order of the arguments of `martingale_part` and `predictable_part`. --- src/probability/martingale/basic.lean | 8 ++- .../martingale/borel_cantelli.lean | 6 +- src/probability/martingale/centering.lean | 58 +++++++++---------- 3 files changed, 37 insertions(+), 35 deletions(-) diff --git a/src/probability/martingale/basic.lean b/src/probability/martingale/basic.lean index e9e8381497f03..241afacb1cdc2 100644 --- a/src/probability/martingale/basic.lean +++ b/src/probability/martingale/basic.lean @@ -47,19 +47,21 @@ variables {Ω E ι : Type*} [preorder ι] /-- A family of functions `f : ι → Ω → E` is a martingale with respect to a filtration `ℱ` if `f` is adapted with respect to `ℱ` and for all `i ≤ j`, `μ[f j | ℱ i] =ᵐ[μ] f i`. -/ -def martingale (f : ι → Ω → E) (ℱ : filtration ι m0) (μ : measure Ω) : Prop := +def martingale (f : ι → Ω → E) (ℱ : filtration ι m0) (μ : measure Ω . volume_tac) : Prop := adapted ℱ f ∧ ∀ i j, i ≤ j → μ[f j | ℱ i] =ᵐ[μ] f i /-- A family of integrable functions `f : ι → Ω → E` is a supermartingale with respect to a filtration `ℱ` if `f` is adapted with respect to `ℱ` and for all `i ≤ j`, `μ[f j | ℱ.le i] ≤ᵐ[μ] f i`. -/ -def supermartingale [has_le E] (f : ι → Ω → E) (ℱ : filtration ι m0) (μ : measure Ω) : Prop := +def supermartingale [has_le E] (f : ι → Ω → E) (ℱ : filtration ι m0) (μ : measure Ω . volume_tac) : + Prop := adapted ℱ f ∧ (∀ i j, i ≤ j → μ[f j | ℱ i] ≤ᵐ[μ] f i) ∧ ∀ i, integrable (f i) μ /-- A family of integrable functions `f : ι → Ω → E` is a submartingale with respect to a filtration `ℱ` if `f` is adapted with respect to `ℱ` and for all `i ≤ j`, `f i ≤ᵐ[μ] μ[f j | ℱ.le i]`. -/ -def submartingale [has_le E] (f : ι → Ω → E) (ℱ : filtration ι m0) (μ : measure Ω) : Prop := +def submartingale [has_le E] (f : ι → Ω → E) (ℱ : filtration ι m0) (μ : measure Ω . volume_tac) : + Prop := adapted ℱ f ∧ (∀ i j, i ≤ j → f i ≤ᵐ[μ] μ[f j | ℱ i]) ∧ ∀ i, integrable (f i) μ lemma martingale_const (ℱ : filtration ι m0) (μ : measure Ω) [is_finite_measure μ] (x : E) : diff --git a/src/probability/martingale/borel_cantelli.lean b/src/probability/martingale/borel_cantelli.lean index 1af4452345f8f..ba26caf71b6ad 100644 --- a/src/probability/martingale/borel_cantelli.lean +++ b/src/probability/martingale/borel_cantelli.lean @@ -297,7 +297,7 @@ lemma adapted_process (hs : ∀ n, measurable_set[ℱ n] (s n)) : ℱ.mono (finset.mem_range.1 hk) _ $ hs _ lemma martingale_part_process_ae_eq (ℱ : filtration ℕ m0) (μ : measure Ω) (s : ℕ → set Ω) (n : ℕ) : - martingale_part ℱ μ (process s) n = + martingale_part (process s) ℱ μ n = ∑ k in finset.range n, ((s (k + 1)).indicator 1 - μ[(s (k + 1)).indicator 1 | ℱ k]) := begin simp only [martingale_part_eq_sum, process_zero, zero_add], @@ -306,7 +306,7 @@ begin end lemma predictable_part_process_ae_eq (ℱ : filtration ℕ m0) (μ : measure Ω) (s : ℕ → set Ω) (n : ℕ) : - predictable_part ℱ μ (process s) n = + predictable_part (process s) ℱ μ n = ∑ k in finset.range n, μ[(s (k + 1)).indicator (1 : Ω → ℝ) | ℱ k] := begin have := martingale_part_process_ae_eq ℱ μ s n, @@ -339,7 +339,7 @@ lemma tendsto_sum_indicator_at_top_iff [is_finite_measure μ] (hf : adapted ℱ f) (hint : ∀ n, integrable (f n) μ) (hbdd : ∀ᵐ ω ∂μ, ∀ n, |f (n + 1) ω - f n ω| ≤ R) : ∀ᵐ ω ∂μ, tendsto (λ n, f n ω) at_top at_top ↔ - tendsto (λ n, predictable_part ℱ μ f n ω) at_top at_top := + tendsto (λ n, predictable_part f ℱ μ n ω) at_top at_top := begin have h₁ := (martingale_martingale_part hf hint).ae_not_tendsto_at_top_at_top (martingale_part_bdd_difference ℱ hbdd), diff --git a/src/probability/martingale/centering.lean b/src/probability/martingale/centering.lean index 7bda4b917d673..dd3190e9ebaec 100644 --- a/src/probability/martingale/centering.lean +++ b/src/probability/martingale/centering.lean @@ -12,20 +12,20 @@ import probability.martingale.basic Any `ℕ`-indexed stochastic process which is adapted and integrable can be written as the sum of a martingale and a predictable process. This result is also known as **Doob's decomposition theorem**. From a process `f`, a filtration `ℱ` and a measure `μ`, we define two processes -`martingale_part ℱ μ f` and `predictable_part ℱ μ f`. +`martingale_part f ℱ μ` and `predictable_part f ℱ μ`. ## Main definitions -* `measure_theory.predictable_part ℱ μ f`: a predictable process such that - `f = predictable_part ℱ μ f + martingale_part ℱ μ f` -* `measure_theory.martingale_part ℱ μ f`: a martingale such that - `f = predictable_part ℱ μ f + martingale_part ℱ μ f` +* `measure_theory.predictable_part f ℱ μ`: a predictable process such that + `f = predictable_part f ℱ μ + martingale_part f ℱ μ` +* `measure_theory.martingale_part f ℱ μ`: a martingale such that + `f = predictable_part f ℱ μ + martingale_part f ℱ μ` ## Main statements -* `measure_theory.adapted_predictable_part`: `(λ n, predictable_part ℱ μ f (n+1))` is adapted. That +* `measure_theory.adapted_predictable_part`: `(λ n, predictable_part f ℱ μ (n+1))` is adapted. That is, `predictable_part` is predictable. -* `measure_theory.martingale_martingale_part`: `martingale_part ℱ μ f` is a martingale. +* `measure_theory.martingale_martingale_part`: `martingale_part f ℱ μ` is a martingale. -/ @@ -43,17 +43,17 @@ variables {Ω E : Type*} {m0 : measurable_space Ω} {μ : measure Ω} process. This is the predictable process. See `martingale_part` for the martingale. -/ noncomputable def predictable_part {m0 : measurable_space Ω} - (ℱ : filtration ℕ m0) (μ : measure Ω) (f : ℕ → Ω → E) : ℕ → Ω → E := + (f : ℕ → Ω → E) (ℱ : filtration ℕ m0) (μ : measure Ω . volume_tac) : ℕ → Ω → E := λ n, ∑ i in finset.range n, μ[f (i+1) - f i | ℱ i] -@[simp] lemma predictable_part_zero : predictable_part ℱ μ f 0 = 0 := +@[simp] lemma predictable_part_zero : predictable_part f ℱ μ 0 = 0 := by simp_rw [predictable_part, finset.range_zero, finset.sum_empty] -lemma adapted_predictable_part : adapted ℱ (λ n, predictable_part ℱ μ f (n+1)) := +lemma adapted_predictable_part : adapted ℱ (λ n, predictable_part f ℱ μ (n+1)) := λ n, finset.strongly_measurable_sum' _ (λ i hin, strongly_measurable_condexp.mono (ℱ.mono (finset.mem_range_succ_iff.mp hin))) -lemma adapted_predictable_part' : adapted ℱ (λ n, predictable_part ℱ μ f n) := +lemma adapted_predictable_part' : adapted ℱ (λ n, predictable_part f ℱ μ n) := λ n, finset.strongly_measurable_sum' _ (λ i hin, strongly_measurable_condexp.mono (ℱ.mono (finset.mem_range_le hin))) @@ -61,15 +61,15 @@ lemma adapted_predictable_part' : adapted ℱ (λ n, predictable_part ℱ μ f n process. This is the martingale. See `predictable_part` for the predictable process. -/ noncomputable def martingale_part {m0 : measurable_space Ω} - (ℱ : filtration ℕ m0) (μ : measure Ω) (f : ℕ → Ω → E) : ℕ → Ω → E := -λ n, f n - predictable_part ℱ μ f n + (f : ℕ → Ω → E) (ℱ : filtration ℕ m0) (μ : measure Ω . volume_tac) : ℕ → Ω → E := +λ n, f n - predictable_part f ℱ μ n lemma martingale_part_add_predictable_part (ℱ : filtration ℕ m0) (μ : measure Ω) (f : ℕ → Ω → E) : - martingale_part ℱ μ f + predictable_part ℱ μ f = f := + martingale_part f ℱ μ + predictable_part f ℱ μ = f := sub_add_cancel _ _ lemma martingale_part_eq_sum : - martingale_part ℱ μ f = + martingale_part f ℱ μ = λ n, f 0 + ∑ i in finset.range n, (f (i+1) - f i - μ[f (i+1) - f i | ℱ i]) := begin rw [martingale_part, predictable_part], @@ -78,11 +78,11 @@ begin end lemma adapted_martingale_part (hf : adapted ℱ f) : - adapted ℱ (martingale_part ℱ μ f) := + adapted ℱ (martingale_part f ℱ μ) := adapted.sub hf adapted_predictable_part' lemma integrable_martingale_part (hf_int : ∀ n, integrable (f n) μ) (n : ℕ) : - integrable (martingale_part ℱ μ f n) μ := + integrable (martingale_part f ℱ μ n) μ := begin rw martingale_part_eq_sum, exact (hf_int 0).add @@ -91,11 +91,11 @@ end lemma martingale_martingale_part (hf : adapted ℱ f) (hf_int : ∀ n, integrable (f n) μ) [sigma_finite_filtration μ ℱ] : - martingale (martingale_part ℱ μ f) ℱ μ := + martingale (martingale_part f ℱ μ) ℱ μ := begin refine ⟨adapted_martingale_part hf, λ i j hij, _⟩, - -- ⊢ μ[martingale_part ℱ μ f j | ℱ i] =ᵐ[μ] martingale_part ℱ μ f i - have h_eq_sum : μ[martingale_part ℱ μ f j | ℱ i] + -- ⊢ μ[martingale_part f ℱ μ j | ℱ i] =ᵐ[μ] martingale_part f ℱ μ i + have h_eq_sum : μ[martingale_part f ℱ μ j | ℱ i] =ᵐ[μ] f 0 + ∑ k in finset.range j, (μ[f (k+1) - f k | ℱ i] - μ[μ[f (k+1) - f k | ℱ k] | ℱ i]), { rw martingale_part_eq_sum, refine (condexp_add (hf_int 0) _).trans _, @@ -140,11 +140,11 @@ end lemma martingale_part_add_ae_eq [sigma_finite_filtration μ ℱ] {f g : ℕ → Ω → E} (hf : martingale f ℱ μ) (hg : adapted ℱ (λ n, g (n + 1))) (hg0 : g 0 = 0) (hgint : ∀ n, integrable (g n) μ) (n : ℕ) : - martingale_part ℱ μ (f + g) n =ᵐ[μ] f n := + martingale_part (f + g) ℱ μ n =ᵐ[μ] f n := begin - set h := f - martingale_part ℱ μ (f + g) with hhdef, - have hh : h = predictable_part ℱ μ (f + g) - g, - { rw [hhdef, sub_eq_sub_iff_add_eq_add, add_comm (predictable_part ℱ μ (f + g)), + set h := f - martingale_part (f + g) ℱ μ with hhdef, + have hh : h = predictable_part (f + g) ℱ μ - g, + { rw [hhdef, sub_eq_sub_iff_add_eq_add, add_comm (predictable_part (f + g) ℱ μ), martingale_part_add_predictable_part] }, have hhpred : adapted ℱ (λ n, h (n + 1)), { rw hh, @@ -162,7 +162,7 @@ end lemma predictable_part_add_ae_eq [sigma_finite_filtration μ ℱ] {f g : ℕ → Ω → E} (hf : martingale f ℱ μ) (hg : adapted ℱ (λ n, g (n + 1))) (hg0 : g 0 = 0) (hgint : ∀ n, integrable (g n) μ) (n : ℕ) : - predictable_part ℱ μ (f + g) n =ᵐ[μ] g n := + predictable_part (f + g) ℱ μ n =ᵐ[μ] g n := begin filter_upwards [martingale_part_add_ae_eq hf hg hg0 hgint n] with ω hω, rw ← add_right_inj (f n ω), @@ -175,7 +175,7 @@ section difference lemma predictable_part_bdd_difference {R : ℝ≥0} {f : ℕ → Ω → ℝ} (ℱ : filtration ℕ m0) (hbdd : ∀ᵐ ω ∂μ, ∀ i, |f (i + 1) ω - f i ω| ≤ R) : - ∀ᵐ ω ∂μ, ∀ i, |predictable_part ℱ μ f (i + 1) ω - predictable_part ℱ μ f i ω| ≤ R := + ∀ᵐ ω ∂μ, ∀ i, |predictable_part f ℱ μ (i + 1) ω - predictable_part f ℱ μ i ω| ≤ R := begin simp_rw [predictable_part, finset.sum_apply, finset.sum_range_succ_sub_sum], exact ae_all_iff.2 (λ i, ae_bdd_condexp_of_ae_bdd $ ae_all_iff.1 hbdd i), @@ -183,12 +183,12 @@ end lemma martingale_part_bdd_difference {R : ℝ≥0} {f : ℕ → Ω → ℝ} (ℱ : filtration ℕ m0) (hbdd : ∀ᵐ ω ∂μ, ∀ i, |f (i + 1) ω - f i ω| ≤ R) : - ∀ᵐ ω ∂μ, ∀ i, |martingale_part ℱ μ f (i + 1) ω - martingale_part ℱ μ f i ω| ≤ ↑(2 * R) := + ∀ᵐ ω ∂μ, ∀ i, |martingale_part f ℱ μ (i + 1) ω - martingale_part f ℱ μ i ω| ≤ ↑(2 * R) := begin filter_upwards [hbdd, predictable_part_bdd_difference ℱ hbdd] with ω hω₁ hω₂ i, simp only [two_mul, martingale_part, pi.sub_apply], - have : |f (i + 1) ω - predictable_part ℱ μ f (i + 1) ω - (f i ω - predictable_part ℱ μ f i ω)| = - |(f (i + 1) ω - f i ω) - (predictable_part ℱ μ f (i + 1) ω - predictable_part ℱ μ f i ω)|, + have : |f (i + 1) ω - predictable_part f ℱ μ (i + 1) ω - (f i ω - predictable_part f ℱ μ i ω)| = + |(f (i + 1) ω - f i ω) - (predictable_part f ℱ μ (i + 1) ω - predictable_part f ℱ μ i ω)|, { ring_nf }, -- `ring` suggests `ring_nf` despite proving the goal rw this, exact (abs_sub _ _).trans (add_le_add (hω₁ i) (hω₂ i)),