-- Mathlib/Probability/Martingale/Centering.lean
theorem martingale_martingalePart (hf : Adapted ℱ f) (hf_int : ∀ n, Integrable (f n) μ)
    [SigmaFiniteFiltration μ ℱ] : Martingale (martingalePart f ℱ μ) ℱ μ

Proof state:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
hf_int : ∀ (n : ℕ), Integrable (f n) μ
inst✝ : SigmaFiniteFiltration μ ℱ
i✝ j : ℕ
hij : i✝ ≤ j
i : ℕ
x✝ : i ∈ Finset.range j
⊢ Integrable (f (i + 1) - f i - μ[f (i + 1) - f i|↑ℱ i]) μ

Tactic:
fun_prop

Result:
no goals

Proof state:
case refine_2.hfi
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
hf_int : ∀ (n : ℕ), Integrable (f n) μ
inst✝ : SigmaFiniteFiltration μ ℱ
i j : ℕ
hij : i ≤ j
h_eq_sum :
  μ[martingalePart f ℱ μ j|↑ℱ i] =ᶠ[ae μ]
    f 0 + ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k|↑ℱ i] - μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i])
h_ge : ∀ (k : ℕ), i ≤ k → μ[f (k + 1) - f k|↑ℱ i] - μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i] =ᶠ[ae μ] 0
k : ℕ
hk : k < i
⊢ Integrable (μ[f (k + 1) - f k|↑ℱ k]) μ

Tactic:
exact integrable_condExp

Result:
no goals

Proof state:
case h
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
hf_int : ∀ (n : ℕ), Integrable (f n) μ
inst✝ : SigmaFiniteFiltration μ ℱ
i j : ℕ
hij : i ≤ j
h_eq_sum :
  μ[martingalePart f ℱ μ j|↑ℱ i] =ᶠ[ae μ]
    f 0 + ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k|↑ℱ i] - μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i])
k : ℕ
hk : i ≤ k
this : μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i] =ᶠ[ae μ] μ[f (k + 1) - f k|↑ℱ i]
x : Ω
hx : (μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i]) x = (μ[f (k + 1) - f k|↑ℱ i]) x
⊢ (μ[f (k + 1) - f k|↑ℱ i] - μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i]) x = 0 x

Tactic:
rw [Pi.sub_apply, Pi.zero_apply, hx, sub_self]

Result:
no goals

Proof state:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
hf_int : ∀ (n : ℕ), Integrable (f n) μ
inst✝ : SigmaFiniteFiltration μ ℱ
i j : ℕ
hij : i ≤ j
⊢ (fun x =>
      (μ[f 0|↑ℱ i]) x +
        (∑ i_1 ∈ Finset.range j, μ[f (i_1 + 1) - f i_1 - μ[f (i_1 + 1) - f i_1|↑ℱ i_1]|↑ℱ i]) x) =ᶠ[ae μ]
    f 0 + ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k|↑ℱ i] - μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i])

Tactic:
refine EventuallyEq.add ?_ ?_

Result:
case refine_1
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
hf_int : ∀ (n : ℕ), Integrable (f n) μ
inst✝ : SigmaFiniteFiltration μ ℱ
i j : ℕ
hij : i ≤ j
⊢ μ[f 0|↑ℱ i] =ᶠ[ae μ] f 0

case refine_2
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
hf_int : ∀ (n : ℕ), Integrable (f n) μ
inst✝ : SigmaFiniteFiltration μ ℱ
i j : ℕ
hij : i ≤ j
⊢ ∑ i_1 ∈ Finset.range j, μ[f (i_1 + 1) - f i_1 - μ[f (i_1 + 1) - f i_1|↑ℱ i_1]|↑ℱ i] =ᶠ[ae μ]
    ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k|↑ℱ i] - μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i])

Proof state:
case refine_1
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
hf_int : ∀ (n : ℕ), Integrable (f n) μ
inst✝ : SigmaFiniteFiltration μ ℱ
i j : ℕ
hij : i ≤ j
⊢ μ[f 0|↑ℱ i] =ᶠ[ae μ] f 0

Tactic:
rw [condExp_of_stronglyMeasurable (ℱ.le _) _ (hf_int 0)]

Result:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
hf_int : ∀ (n : ℕ), Integrable (f n) μ
inst✝ : SigmaFiniteFiltration μ ℱ
i j : ℕ
hij : i ≤ j
⊢ StronglyMeasurable (f 0)

Proof state:
case refine_2
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
hf_int : ∀ (n : ℕ), Integrable (f n) μ
inst✝ : SigmaFiniteFiltration μ ℱ
i j : ℕ
hij : i ≤ j
h_eq_sum :
  μ[martingalePart f ℱ μ j|↑ℱ i] =ᶠ[ae μ]
    f 0 + ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k|↑ℱ i] - μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i])
h_ge : ∀ (k : ℕ), i ≤ k → μ[f (k + 1) - f k|↑ℱ i] - μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i] =ᶠ[ae μ] 0
k : ℕ
hk : k < i
⊢ μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i] =ᶠ[ae μ] μ[f (k + 1) - f k|↑ℱ k]

Tactic:
rw [condExp_of_stronglyMeasurable]

Result:
case refine_2.hf
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
hf_int : ∀ (n : ℕ), Integrable (f n) μ
inst✝ : SigmaFiniteFiltration μ ℱ
i j : ℕ
hij : i ≤ j
h_eq_sum :
  μ[martingalePart f ℱ μ j|↑ℱ i] =ᶠ[ae μ]
    f 0 + ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k|↑ℱ i] - μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i])
h_ge : ∀ (k : ℕ), i ≤ k → μ[f (k + 1) - f k|↑ℱ i] - μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i] =ᶠ[ae μ] 0
k : ℕ
hk : k < i
⊢ StronglyMeasurable (μ[f (k + 1) - f k|↑ℱ k])

case refine_2.hfi
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
hf_int : ∀ (n : ℕ), Integrable (f n) μ
inst✝ : SigmaFiniteFiltration μ ℱ
i j : ℕ
hij : i ≤ j
h_eq_sum :
  μ[martingalePart f ℱ μ j|↑ℱ i] =ᶠ[ae μ]
    f 0 + ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k|↑ℱ i] - μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i])
h_ge : ∀ (k : ℕ), i ≤ k → μ[f (k + 1) - f k|↑ℱ i] - μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i] =ᶠ[ae μ] 0
k : ℕ
hk : k < i
⊢ Integrable (μ[f (k + 1) - f k|↑ℱ k]) μ

Proof state:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
hf_int : ∀ (n : ℕ), Integrable (f n) μ
inst✝ : SigmaFiniteFiltration μ ℱ
i j : ℕ
hij : i ≤ j
⊢ Integrable (∑ i ∈ Finset.range j, (f (i + 1) - f i - μ[f (i + 1) - f i|↑ℱ i])) μ

Tactic:
fun_prop

Result:
no goals

Proof state:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
hf_int : ∀ (n : ℕ), Integrable (f n) μ
inst✝ : SigmaFiniteFiltration μ ℱ
⊢ Martingale (martingalePart f ℱ μ) ℱ μ

Tactic:
refine ⟨adapted_martingalePart hf, fun i j hij => ?_⟩

Result:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
hf_int : ∀ (n : ℕ), Integrable (f n) μ
inst✝ : SigmaFiniteFiltration μ ℱ
i j : ℕ
hij : i ≤ j
⊢ μ[martingalePart f ℱ μ j|↑ℱ i] =ᶠ[ae μ] martingalePart f ℱ μ i

Proof state:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
hf_int : ∀ (n : ℕ), Integrable (f n) μ
inst✝ : SigmaFiniteFiltration μ ℱ
i j : ℕ
hij : i ≤ j
⊢ StronglyMeasurable (f 0)

Tactic:
exact (hf 0).mono (ℱ.mono (zero_le i))

Result:
no goals