awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f : α → β → ℝ≥0
g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
a : α
⊢ Measurable (α := α × β) (β := ℝ≥0∞) (Function.uncurry fun (a : α) (x : β) ↦ (↑(f a x) : ℝ≥0∞))

Tactic:
measurable_coe_nnreal_ennreal.comp hf

Premises used: Measurable.comp, measurable_coe_nnreal_ennreal
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f : α → β → ℝ≥0
g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
a : α
⊢ Measurable (α := α × β) (β := ℝ≥0∞) (Function.uncurry fun (a : α) (x : β) ↦ (↑(f a x) : ℝ≥0∞))

Tactic:
exact measurable_coe_nnreal_ennreal.comp hf

Premises used: Measurable.comp, measurable_coe_nnreal_ennreal
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f : α → β → ℝ≥0
g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
a : α
⊢ Measurable (β := ℝ≥0∞) fun (x : β) ↦ (↑(f a x) : ℝ≥0∞)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f : α → β → ℝ≥0
g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
a : α
⊢ Measurable (β := ℝ≥0∞) fun (x : β) ↦ g a x

Tactic:
fun_prop
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
ℱ : Filtration ι m0
μ : Measure Ω
inst_3 : IsFiniteMeasure μ
x : E
i j : ι
h : i ≤ j
rw rw₁ : EventuallyEq.{u_1, u_2} (β := E) (ae μ) (fun (x_1 : Ω) ↦ x) fun (x_1 : Ω) ↦ x
⊢ EventuallyEq.{u_1, u_2} (β := E) (ae μ) μ[(fun (x_1 : ι) (x_2 : Ω) ↦ x) j | (↑ℱ : ι → MeasurableSpace Ω) i]
    ((fun (x_1 : ι) (x_2 : Ω) ↦ x) i)

Tactic:
rw [condExp_const (ℱ.le _)]

Premises used: MeasureTheory.condExp_const, MeasureTheory.Filtration.le
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : OrderBot ι
ℱ : Filtration ι m0
μ : Measure Ω
inst_4 : SigmaFiniteFiltration μ ℱ
f : Ω → E
hf : StronglyMeasurable f
hfint : Integrable f μ
⊢ Martingale.{u_1, u_2, u_3} (E := E) (fun (x : ι) ↦ f) ℱ μ

Tactic:
⟨fun i => hf.mono <| ℱ.mono bot_le, fun i j _ => ?_⟩

Premises used: MeasureTheory.Martingale, MeasureTheory.StronglyMeasurable.mono, And.intro, MeasureTheory.Filtration.mono, bot_le
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : OrderBot ι
ℱ : Filtration ι m0
μ : Measure Ω
inst_4 : SigmaFiniteFiltration μ ℱ
f : Ω → E
hf : StronglyMeasurable f
hfint : Integrable f μ
refine :
  ∀ (i j : ι),
    i ≤ j →
      EventuallyEq.{u_1, u_2} (β := E) (ae μ) μ[(fun (x : ι) ↦ f) j | (↑ℱ : ι → MeasurableSpace Ω) i]
        ((fun (x : ι) ↦ f) i)
⊢ Martingale.{u_1, u_2, u_3} (E := E) (fun (x : ι) ↦ f) ℱ μ

Tactic:
refine ⟨fun i => hf.mono <| ℱ.mono bot_le, fun i j _ => ?_⟩
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : OrderBot ι
ℱ : Filtration ι m0
μ : Measure Ω
inst_4 : SigmaFiniteFiltration μ ℱ
f : Ω → E
hf : StronglyMeasurable f
hfint : Integrable f μ
i j : ι
h : i ≤ j
rw rw₁ : f =ᶠ[ae μ] f
⊢ EventuallyEq.{u_1, u_2} (β := E) (ae μ) μ[(fun (x : ι) ↦ f) j | (↑ℱ : ι → MeasurableSpace Ω) i] ((fun (x : ι) ↦ f) i)

Tactic:
rw [condExp_of_stronglyMeasurable (ℱ.le _) (hf.mono <| ℱ.mono bot_le) hfint]

Premises used: MeasureTheory.condExp_of_stronglyMeasurable, MeasureTheory.StronglyMeasurable.mono, MeasureTheory.Filtration.mono, MeasureTheory.Filtration.le, bot_le
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
ℱ : Filtration ι m0
μ : Measure Ω
i j : ι
h : i ≤ j
⊢ EventuallyEq.{u_1, u_2} (β := E) (ae μ) μ[0 j | (↑ℱ : ι → MeasurableSpace Ω) i] (0 i)

Tactic:
simp
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : ι → Ω → E
ℱ : Filtration ι m0
hf : Martingale f ℱ μ
⊢ StronglyAdapted (β := fun (i : ι) ↦ E) ℱ f

Tactic:
hf.1

Premises used: And.left
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : ι → Ω → E
ℱ : Filtration ι m0
hf : Martingale f ℱ μ
i : ι
⊢ StronglyMeasurable (f i)

Tactic:
hf.stronglyAdapted i

Premises used: MeasureTheory.Martingale.stronglyAdapted
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : ι → Ω → E
ℱ : Filtration ι m0
hf : Martingale f ℱ μ
i j : ι
hij : i ≤ j
⊢ μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] =ᶠ[ae μ] f i

Tactic:
hf.2 i j hij

Premises used: And.right
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
hf : Martingale f ℱ μ
i : ι
⊢ Integrable (f i) μ

Tactic:
integrable_condExp.congr (hf.condExp_ae_eq (le_refl i))

Premises used: le_refl, MeasureTheory.integrable_condExp, MeasureTheory.Integrable.congr, MeasureTheory.Martingale.condExp_ae_eq
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : SigmaFiniteFiltration μ ℱ
hf : Martingale f ℱ μ
i j : ι
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
rw : Eq.{u_2 + 1} (α := E) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (x : Ω) in s, μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] x ∂μ)
⊢ Eq.{u_2 + 1} (α := E) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)

Tactic:
rw [← setIntegral_condExp (ℱ.le i) (hf.integrable j) hs]

Premises used: MeasureTheory.setIntegral_condExp, MeasureTheory.Martingale.integrable, MeasureTheory.Filtration.le
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : SigmaFiniteFiltration μ ℱ
hf : Martingale f ℱ μ
i j : ι
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
⊢ Eq.{u_2 + 1} (α := E) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (x : Ω) in s, μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] x ∂μ)

Tactic:
setIntegral_congr_ae (ℱ.le i s hs) ?_

Premises used: MeasureTheory.setIntegral_congr_ae, MeasureTheory.Filtration.le
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : SigmaFiniteFiltration μ ℱ
hf : Martingale f ℱ μ
i j : ι
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
refine : ∀ᵐ (x : Ω) ∂μ, x ∈ s → f i x = μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] x
⊢ Eq.{u_2 + 1} (α := E) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (x : Ω) in s, μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] x ∂μ)

Tactic:
refine setIntegral_congr_ae (ℱ.le i s hs) ?_

Premises used: MeasureTheory.setIntegral_congr_ae, MeasureTheory.Filtration.le
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : SigmaFiniteFiltration μ ℱ
hf : Martingale f ℱ μ
i j : ι
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
a : Ω
heq : μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] a = f i a
h : a ∈ s → f i a = μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] a
⊢ a ∈ s → f i a = μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] a

Tactic:
_
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : SigmaFiniteFiltration μ ℱ
hf : Martingale f ℱ μ
i j : ι
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
a : Ω
heq : μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] a = f i a
h : a ∈ s
⊢ f i a = μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] a

Tactic:
heq.symm

Premises used: Eq.symm
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : SigmaFiniteFiltration μ ℱ
hf : Martingale f ℱ μ
i j : ι
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
h :
  ∀ (a : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] x = f i x) x} x →
          Membership.mem (γ := Set Ω)
            {x : Ω | (fun (x : Ω) ↦ x ∈ s → f i x = μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] x) x} x}
      a
h₁ h₂ :
  ∀ (a : Ω) (heq : μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] a = f i a),
    a ∈ s → f i a = μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] a
⊢ ∀ᵐ (x : Ω) ∂μ, x ∈ s → f i x = μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] x

Tactic:
filter_upwards [hf.2 i j hij] with _ heq _ using heq.symm

Premises used: And.right
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f g : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
hf : Martingale f ℱ μ
hg : StronglyAdapted (β := fun (i : ι) ↦ E) ℱ g
h_eq : ∀ (t : ι), f t =ᶠ[ae μ] g t
⊢ Martingale g ℱ μ

Tactic:
⟨hg, fun i j hij ↦ ?_⟩

Premises used: MeasureTheory.Martingale, And.intro
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f g : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
hf : Martingale f ℱ μ
hg : StronglyAdapted (β := fun (i : ι) ↦ E) ℱ g
h_eq : ∀ (t : ι), f t =ᶠ[ae μ] g t
refine : ∀ (i j : ι) (hij : i ≤ j), μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i] =ᶠ[ae μ] g i
⊢ Martingale g ℱ μ

Tactic:
refine ⟨hg, fun i j hij ↦ ?_⟩
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f g : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
hf : Martingale f ℱ μ
hg : StronglyAdapted (β := fun (i : ι) ↦ E) ℱ g
h_eq : ∀ (t : ι), f t =ᶠ[ae μ] g t
i j : ι
hij : i ≤ j
⊢ μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i] =ᶠ[ae μ] μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i]

Tactic:
(condExp_congr_ae (h_eq j)).symm

Premises used: MeasureTheory.condExp_congr_ae, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f g : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
hf : Martingale f ℱ μ
hg : StronglyAdapted (β := fun (i : ι) ↦ E) ℱ g
h_eq : ∀ (t : ι), f t =ᶠ[ae μ] g t
i j : ι
hij : i ≤ j
⊢ μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] =ᶠ[ae μ] g i

Tactic:
(hf.2 i j hij).trans (h_eq i)

Premises used: Filter.EventuallyEq.trans, And.right
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f g : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
hf : Martingale f ℱ μ
hg : StronglyAdapted (β := fun (i : ι) ↦ E) ℱ g
h_eq : ∀ (t : ι), f t =ᶠ[ae μ] g t
i j : ι
hij : i ≤ j
⊢ μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i] =ᶠ[ae μ] g i

Tactic:
calc μ[g j | ℱ i] =ᵐ[μ] μ[f j | ℱ i] := (condExp_congr_ae (h_eq j)).symm
    _ =ᵐ[μ] g i := (hf.2 i j hij).trans (h_eq i)

Premises used: Filter.EventuallyEq.trans, MeasureTheory.Filtration.seq, MeasureTheory.condExp_congr_ae, And.right, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f g : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
hf : Martingale f ℱ μ
hg : Martingale g ℱ μ
⊢ Martingale (f + g) ℱ μ

Tactic:
⟨hf.stronglyAdapted.add hg.stronglyAdapted, fun i j hij => ?_⟩

Premises used: MeasureTheory.Martingale.stronglyAdapted, MeasureTheory.Martingale, And.intro, MeasureTheory.StronglyAdapted.add
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f g : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
hf : Martingale f ℱ μ
hg : Martingale g ℱ μ
refine : ∀ (i j : ι) (hij : i ≤ j), μ[(f + g) j | (↑ℱ : ι → MeasurableSpace Ω) i] =ᶠ[ae μ] (f + g) i
⊢ Martingale (f + g) ℱ μ

Tactic:
refine ⟨hf.stronglyAdapted.add hg.stronglyAdapted, fun i j hij => ?_⟩
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f g : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
hf : Martingale f ℱ μ
hg : Martingale g ℱ μ
i j : ι
hij : i ≤ j
⊢ μ[(f + g) j | (↑ℱ : ι → MeasurableSpace Ω) i] =ᶠ[ae μ] (f + g) i

Tactic:
(condExp_add (hf.integrable j) (hg.integrable j) _).trans
    ((hf.2 i j hij).add (hg.2 i j hij))

Premises used: Filter.EventuallyEq.trans, MeasureTheory.Martingale.integrable, MeasureTheory.condExp_add, And.right, Filter.EventuallyEq.add
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f g : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
hf : Martingale f ℱ μ
hg : Martingale g ℱ μ
i j : ι
hij : i ≤ j
⊢ μ[(f + g) j | (↑ℱ : ι → MeasurableSpace Ω) i] =ᶠ[ae μ] (f + g) i

Tactic:
exact (condExp_add (hf.integrable j) (hg.integrable j) _).trans
    ((hf.2 i j hij).add (hg.2 i j hij))

Premises used: Filter.EventuallyEq.trans, MeasureTheory.Martingale.integrable, MeasureTheory.condExp_add, And.right, Filter.EventuallyEq.add
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
hf : Martingale f ℱ μ
⊢ Martingale (-f) ℱ μ

Tactic:
⟨hf.stronglyAdapted.neg, fun i j hij => (condExp_neg ..).trans (hf.2 i j hij).neg⟩

Premises used: MeasureTheory.Martingale.stronglyAdapted, Filter.EventuallyEq.trans, MeasureTheory.Filtration.seq, MeasureTheory.Martingale, MeasureTheory.condExp_neg, MeasureTheory.StronglyAdapted.neg, And.right, Filter.EventuallyEq.neg, And.intro
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f g : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
hf : Martingale f ℱ μ
hg : Martingale g ℱ μ
rw : Martingale (f + -g) ℱ μ
⊢ Martingale (f - g) ℱ μ

Tactic:
rw [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f g : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
hf : Martingale f ℱ μ
hg : Martingale g ℱ μ
⊢ Martingale (f + -g) ℱ μ

Tactic:
hf.add hg.neg

Premises used: MeasureTheory.Martingale.add, MeasureTheory.Martingale.neg
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f g : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
hf : Martingale f ℱ μ
hg : Martingale g ℱ μ
⊢ Martingale (f + -g) ℱ μ

Tactic:
exact hf.add hg.neg

Premises used: MeasureTheory.Martingale.add, MeasureTheory.Martingale.neg
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
c : ℝ
hf : Martingale f ℱ μ
⊢ Martingale (c • f) ℱ μ

Tactic:
⟨hf.stronglyAdapted.smul c, fun i j hij => ?_⟩

Premises used: MeasureTheory.Martingale.stronglyAdapted, MeasureTheory.Martingale, MeasureTheory.StronglyAdapted.smul, And.intro
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
c : ℝ
hf : Martingale f ℱ μ
refine : ∀ (i j : ι) (hij : i ≤ j), μ[(c • f) j | (↑ℱ : ι → MeasurableSpace Ω) i] =ᶠ[ae μ] (c • f) i
⊢ Martingale (c • f) ℱ μ

Tactic:
refine ⟨hf.stronglyAdapted.smul c, fun i j hij => ?_⟩
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
c : ℝ
hf : Martingale f ℱ μ
i j : ι
hij : i ≤ j
⊢ μ[(c • f) j | (↑ℱ : ι → MeasurableSpace Ω) i] =ᶠ[ae μ] (c • f) i

Tactic:
(condExp_smul ..).trans ((hf.2 i j hij).mono fun x hx => ?_)

Premises used: Filter.EventuallyEq.trans, MeasureTheory.condExp_smul, Filter.Eventually.mono, And.right
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
c : ℝ
hf : Martingale f ℱ μ
i j : ι
hij : i ≤ j
refine :
  ∀ (x : Ω) (hx : μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] x = f i x),
    (c • μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i]) x = (c • f) i x
⊢ μ[(c • f) j | (↑ℱ : ι → MeasurableSpace Ω) i] =ᶠ[ae μ] (c • f) i

Tactic:
refine (condExp_smul ..).trans ((hf.2 i j hij).mono fun x hx => ?_)

Premises used: Filter.EventuallyEq.trans, MeasureTheory.condExp_smul, Filter.Eventually.mono, And.right
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
c : ℝ
hf : Martingale f ℱ μ
i j : ι
hij : i ≤ j
x : Ω
hx : μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] x = f i x
⊢ (c • μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i]) x = (c • f) i x

Tactic:
simp only [Pi.smul_apply, hx]

Premises used: Pi.smul_apply
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : Preorder E
hf : Martingale f ℱ μ
⊢ Supermartingale f ℱ μ

Tactic:
⟨hf.1, fun i j hij => (hf.2 i j hij).le, fun i => hf.integrable i⟩

Premises used: MeasureTheory.Martingale.integrable, Filter.EventuallyEq.le, And.right, And.left, And.intro, MeasureTheory.Supermartingale
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : Preorder E
hf : Martingale f ℱ μ
⊢ Submartingale f ℱ μ

Tactic:
⟨hf.1, fun i j hij => (hf.2 i j hij).symm.le, fun i => hf.integrable i⟩

Premises used: MeasureTheory.Martingale.integrable, MeasureTheory.Submartingale, Filter.EventuallyEq.le, And.right, And.left, And.intro, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : PartialOrder E
⊢ Martingale f ℱ μ ↔ Supermartingale f ℱ μ ∧ Submartingale f ℱ μ

Tactic:
⟨fun hf => ⟨hf.supermartingale, hf.submartingale⟩, fun ⟨hf₁, hf₂⟩ =>
    ⟨hf₁.1, fun i j hij => (hf₁.2.1 i j hij).antisymm (hf₂.2.1 i j hij)⟩⟩

Premises used: MeasureTheory.Martingale.submartingale, MeasureTheory.Martingale, _private.0.MeasureTheory.martingale_iff.match_1, And.right, And.left, MeasureTheory.Martingale.supermartingale, Filter.EventuallyLE.antisymm, And.intro, Iff.intro
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : Ω → E
ℱ : Filtration ι m0
μ : Measure Ω
inst_4 : SigmaFiniteFiltration μ ℱ
⊢ Martingale.{u_1, u_2, u_3} (E := E) (fun (i : ι) ↦ μ[f | (↑ℱ : ι → MeasurableSpace Ω) i]) ℱ μ

Tactic:
⟨fun _ => stronglyMeasurable_condExp, fun _ j hij => condExp_condExp_of_le (ℱ.mono hij) (ℱ.le j)⟩

Premises used: MeasureTheory.Martingale, MeasureTheory.condExp_condExp_of_le, MeasureTheory.stronglyMeasurable_condExp, And.intro, MeasureTheory.Filtration.mono, MeasureTheory.Filtration.le
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : LE E
hf : Supermartingale f ℱ μ
⊢ StronglyAdapted (β := fun (i : ι) ↦ E) ℱ f

Tactic:
hf.1

Premises used: And.left
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : LE E
hf : Supermartingale f ℱ μ
i : ι
⊢ StronglyMeasurable (f i)

Tactic:
hf.stronglyAdapted i

Premises used: MeasureTheory.Supermartingale.stronglyAdapted
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : LE E
hf : Supermartingale f ℱ μ
i : ι
⊢ Integrable (f i) μ

Tactic:
hf.2.2 i

Premises used: And.right
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : LE E
hf : Supermartingale f ℱ μ
i j : ι
hij : i ≤ j
⊢ μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] ≤ᶠ[ae μ] f i

Tactic:
hf.2.1 i j hij

Premises used: And.right, And.left