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

@@ -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) :

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),

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,33 +43,33 @@ 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)))
 
 /-- Any `ℕ`-indexed stochastic process can be written as the sum of a martingale and a predictable
 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,20 +175,20 @@ 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),
 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)),