awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
inst_6 : IsOrderedModule ℝ E
inst_7 : ClosedIciTopology E
inst_8 : SigmaFiniteFiltration μ ℱ
f : ι → Ω → E
hf : Supermartingale f ℱ μ
i j : ι
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
rw : LE.le.{u_2} (α := E) (∫ (x : Ω) in s, μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] x ∂μ) (∫ (ω : Ω) in s, f i ω ∂μ)
⊢ LE.le.{u_2} (α := E) (∫ (ω : Ω) in s, f j ω ∂μ) (∫ (ω : Ω) in s, f i ω ∂μ)

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

Premises used: MeasureTheory.setIntegral_condExp, MeasureTheory.Supermartingale.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
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
inst_6 : IsOrderedModule ℝ E
inst_7 : ClosedIciTopology E
inst_8 : SigmaFiniteFiltration μ ℱ
f : ι → Ω → E
hf : Supermartingale f ℱ μ
i j : ι
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
⊢ LE.le.{u_2} (α := E) (∫ (x : Ω) in s, μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] x ∂μ) (∫ (ω : Ω) in s, f i ω ∂μ)

Tactic:
setIntegral_mono_ae integrable_condExp.integrableOn (hf.integrable i).integrableOn ?_

Premises used: MeasureTheory.integrable_condExp, MeasureTheory.Supermartingale.integrable, MeasureTheory.Integrable.integrableOn, MeasureTheory.setIntegral_mono_ae
-- 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
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
inst_6 : IsOrderedModule ℝ E
inst_7 : ClosedIciTopology E
inst_8 : SigmaFiniteFiltration μ ℱ
f : ι → Ω → E
hf : Supermartingale f ℱ μ
i j : ι
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
refine : μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] ≤ᶠ[ae μ] f i
⊢ LE.le.{u_2} (α := E) (∫ (x : Ω) in s, μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] x ∂μ) (∫ (ω : Ω) in s, f i ω ∂μ)

Tactic:
refine setIntegral_mono_ae integrable_condExp.integrableOn (hf.integrable i).integrableOn ?_

Premises used: MeasureTheory.integrable_condExp, MeasureTheory.Supermartingale.integrable, MeasureTheory.Integrable.integrableOn, MeasureTheory.setIntegral_mono_ae
-- 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
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
inst_6 : IsOrderedModule ℝ E
inst_7 : ClosedIciTopology E
inst_8 : SigmaFiniteFiltration μ ℱ
f : ι → Ω → E
hf : Supermartingale f ℱ μ
i j : ι
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
a : Ω
heq : μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] a ≤ f i a
⊢ μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] a ≤ f i a

Tactic:
heq
-- 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
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
inst_6 : IsOrderedModule ℝ E
inst_7 : ClosedIciTopology E
inst_8 : SigmaFiniteFiltration μ ℱ
f : ι → Ω → E
hf : Supermartingale 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 : Ω) ↦ μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] x ≤ f i x) x} x}
      a
h₁ h₂ :
  ∀ (a : Ω) (heq : μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] a ≤ f i a), μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] a ≤ f i a
⊢ μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] ≤ᶠ[ae μ] f i

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

Premises used: And.right, 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 g : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : LE E
hf : Supermartingale f ℱ μ
hg : StronglyAdapted (β := fun (i : ι) ↦ E) ℱ g
h_eq : ∀ (t : ι), f t =ᶠ[ae μ] g t
⊢ Supermartingale g ℱ μ

Tactic:
⟨hg, fun i j hij ↦ ?_, fun i ↦ (integrable_congr (h_eq i)).mp (hf.integrable i)⟩

Premises used: MeasureTheory.integrable_congr, MeasureTheory.Supermartingale.integrable, And.intro, Iff.mp, 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 g : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : LE E
hf : Supermartingale 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
⊢ Supermartingale g ℱ μ

Tactic:
refine ⟨hg, fun i j hij ↦ ?_, fun i ↦ (integrable_congr (h_eq i)).mp (hf.integrable i)⟩
-- 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
inst_4 : LE E
hf : Supermartingale f ℱ μ
hg : StronglyAdapted (β := fun (i : ι) ↦ E) ℱ g
h_eq : ∀ (t : ι), f t =ᶠ[ae μ] g t
i j : ι
hij : i ≤ j
h :
  ∀ (ω : Ω) (h_le : μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] ω ≤ f i ω)
    (hcond : μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] ω = μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i] ω)
    (h_eq : f i ω = g i ω), μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i] ω ≤ g i ω
⊢ μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i] ≤ᶠ[ae μ] g i

Tactic:
filter_upwards [condExp_ae_le hf hij, condExp_congr_ae (h_eq j), h_eq i] with ω h_le hcond h_eq

Premises used: MeasureTheory.condExp_congr_ae, MeasureTheory.Supermartingale.condExp_ae_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 g : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : LE E
hf : Supermartingale f ℱ μ
hg : StronglyAdapted (β := fun (i : ι) ↦ E) ℱ g
h_eq_1 : ∀ (t : ι), f t =ᶠ[ae μ] g t
i j : ι
hij : i ≤ j
ω : Ω
h_le : μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] ω ≤ f i ω
hcond : μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] ω = μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i] ω
h_eq : f i ω = g i ω
h : μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] ω ≤ g i ω
h₁ h₂ h₃ h₄ : μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] ω ≤ f i ω
⊢ μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i] ω ≤ g i ω

Tactic:
rwa [← hcond, ← h_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 g : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : Preorder E
inst_5 : AddLeftMono E
hf : Supermartingale f ℱ μ
hg : Supermartingale g ℱ μ
⊢ Supermartingale (f + g) ℱ μ

Tactic:
⟨hf.1.add hg.1, fun i j hij => ?_, fun i => (hf.2.2 i).add (hg.2.2 i)⟩

Premises used: And.right, And.left, And.intro, MeasureTheory.Integrable.add, MeasureTheory.StronglyAdapted.add, 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 g : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : Preorder E
inst_5 : AddLeftMono E
hf : Supermartingale f ℱ μ
hg : Supermartingale g ℱ μ
refine : ∀ (i j : ι) (hij : i ≤ j), μ[(f + g) j | (↑ℱ : ι → MeasurableSpace Ω) i] ≤ᶠ[ae μ] (f + g) i
⊢ Supermartingale (f + g) ℱ μ

Tactic:
refine ⟨hf.1.add hg.1, fun i j hij => ?_, fun i => (hf.2.2 i).add (hg.2.2 i)⟩
-- 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
inst_4 : Preorder E
inst_5 : AddLeftMono E
hf : Supermartingale f ℱ μ
hg : Supermartingale g ℱ μ
i j : ι
hij : i ≤ j
⊢ μ[(f + g) j | (↑ℱ : ι → MeasurableSpace Ω) i] ≤ᶠ[ae μ] (f + g) i

Tactic:
(condExp_add (hf.integrable j) (hg.integrable j) _).le.trans ?_

Premises used: MeasureTheory.Supermartingale.integrable, Filter.EventuallyEq.le, MeasureTheory.condExp_add, Filter.EventuallyLE.trans
-- 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
inst_4 : Preorder E
inst_5 : AddLeftMono E
hf : Supermartingale f ℱ μ
hg : Supermartingale g ℱ μ
i j : ι
hij : i ≤ j
refine : μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] + μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i] ≤ᶠ[ae μ] (f + g) i
⊢ μ[(f + g) j | (↑ℱ : ι → MeasurableSpace Ω) i] ≤ᶠ[ae μ] (f + g) i

Tactic:
refine (condExp_add (hf.integrable j) (hg.integrable j) _).le.trans ?_

Premises used: MeasureTheory.Supermartingale.integrable, Filter.EventuallyEq.le, MeasureTheory.condExp_add, Filter.EventuallyLE.trans
-- 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
inst_4 : Preorder E
inst_5 : AddLeftMono E
hf : Supermartingale f ℱ μ
hg : Supermartingale g ℱ μ
i j : ι
hij : i ≤ j
h :
  ∀ (a : Ω),
    μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] a ≤ f i a →
      μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i] a ≤ g i a →
        (μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] + μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i]) a ≤ (f + g) i a
⊢ μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] + μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i] ≤ᶠ[ae μ] (f + g) i

Tactic:
filter_upwards [hf.2.1 i j hij, hg.2.1 i j hij]

Premises used: And.right, 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 g : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : Preorder E
inst_5 : AddLeftMono E
hf : Supermartingale f ℱ μ
hg : Supermartingale g ℱ μ
i j : ι
hij : i ≤ j
a : Ω
h : μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] a ≤ f i a
h_1 : μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i] a ≤ g i a
⊢ (μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] + μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i]) a ≤ (f + g) i a

Tactic:
add_le_add ?_ ?_

Premises used: add_le_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
inst_4 : Preorder E
inst_5 : AddLeftMono E
hf : Supermartingale f ℱ μ
hg : Supermartingale g ℱ μ
i j : ι
hij : i ≤ j
a : Ω
h_1 : μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] a ≤ f i a
h_2 : μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i] a ≤ g i a
h : μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] a ≤ f i a
h₁ : μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i] a ≤ g i a
⊢ (μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] + μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i]) a ≤ (f + g) i a

Tactic:
refine add_le_add ?_ ?_

Premises used: add_le_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
inst_4 : Preorder E
inst_5 : AddLeftMono E
hf : Supermartingale f ℱ μ
hg : Supermartingale g ℱ μ
i j : ι
hij : i ≤ j
a : Ω
h : μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] a ≤ f i a
h_1 : μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i] a ≤ g i a
⊢ μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] a ≤ f i a

Tactic:
assumption
-- 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
inst_4 : Preorder E
inst_5 : AddLeftMono E
hf : Supermartingale f ℱ μ
hg : Supermartingale g ℱ μ
i j : ι
hij : i ≤ j
a : Ω
h : μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] a ≤ f i a
h_1 : μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i] a ≤ g i a
⊢ μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i] a ≤ g i a

Tactic:
assumption
-- 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
inst_4 : Preorder E
inst_5 : AddLeftMono E
hf : Supermartingale f ℱ μ
hg : Martingale g ℱ μ
⊢ Supermartingale (f + g) ℱ μ

Tactic:
hf.add hg.supermartingale

Premises used: MeasureTheory.Martingale.supermartingale, MeasureTheory.Supermartingale.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
inst_4 : Preorder E
inst_5 : AddLeftMono E
hf : Supermartingale f ℱ μ
⊢ Submartingale (-f) ℱ μ

Tactic:
⟨hf.1.neg, fun i j hij => ?_, fun i => (hf.2.2 i).neg⟩

Premises used: MeasureTheory.Integrable.neg, MeasureTheory.Submartingale, MeasureTheory.StronglyAdapted.neg, And.right, And.left, 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
inst_4 : Preorder E
inst_5 : AddLeftMono E
hf : Supermartingale f ℱ μ
refine : ∀ (i j : ι) (hij : i ≤ j), (-f) i ≤ᶠ[ae μ] μ[(-f) j | (↑ℱ : ι → MeasurableSpace Ω) i]
⊢ Submartingale (-f) ℱ μ

Tactic:
refine ⟨hf.1.neg, fun i j hij => ?_, fun i => (hf.2.2 i).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
inst_4 : Preorder E
inst_5 : AddLeftMono E
hf : Supermartingale f ℱ μ
i j : ι
hij : i ≤ j
⊢ (-f) i ≤ᶠ[ae μ] μ[(-f) j | (↑ℱ : ι → MeasurableSpace Ω) i]

Tactic:
EventuallyLE.trans ?_ (condExp_neg ..).symm.le

Premises used: MeasureTheory.condExp_neg, Filter.EventuallyEq.le, Filter.EventuallyLE.trans, 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 : Preorder E
inst_5 : AddLeftMono E
hf : Supermartingale f ℱ μ
i j : ι
hij : i ≤ j
refine : (-f) i ≤ᶠ[ae μ] -μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i]
⊢ (-f) i ≤ᶠ[ae μ] μ[(-f) j | (↑ℱ : ι → MeasurableSpace Ω) i]

Tactic:
refine EventuallyLE.trans ?_ (condExp_neg ..).symm.le

Premises used: MeasureTheory.condExp_neg, Filter.EventuallyEq.le, Filter.EventuallyLE.trans, 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 : Preorder E
inst_5 : AddLeftMono E
hf : Supermartingale f ℱ μ
i j : ι
hij : i ≤ j
a : Ω
h : μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] a ≤ f i a → (-f) i a ≤ (-μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i]) a
⊢ μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] a ≤ f i a → (-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 : Preorder E
inst_5 : AddLeftMono E
hf : Supermartingale f ℱ μ
i j : ι
hij : i ≤ j
h :
  ∀ (a : Ω), μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] a ≤ f i a → (-f) i a ≤ (-μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i]) a
⊢ (-f) i ≤ᶠ[ae μ] -μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i]

Tactic:
filter_upwards [hf.2.1 i j hij] with _ _

Premises used: And.right, 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 : CompleteSpace E
inst_4 : Preorder E
inst_5 : AddLeftMono E
hf : Supermartingale f ℱ μ
i j : ι
hij : i ≤ j
a : Ω
h : μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] a ≤ f i a
⊢ (-f) i a ≤ (-μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i]) a

Tactic:
simpa
-- 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 : Submartingale 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 : Submartingale f ℱ μ
i : ι
⊢ StronglyMeasurable (f i)

Tactic:
hf.stronglyAdapted i

Premises used: MeasureTheory.Submartingale.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 : Submartingale 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 : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
⊢ f i ≤ᶠ[ae μ] μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i]

Tactic:
hf.2.1 i j hij

Premises used: And.right, 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 g : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : LE E
hf : Submartingale f ℱ μ
hg : StronglyAdapted (β := fun (i : ι) ↦ E) ℱ g
h_eq : ∀ (t : ι), f t =ᶠ[ae μ] g t
⊢ Submartingale g ℱ μ

Tactic:
⟨hg, fun i j hij ↦ ?_, fun i ↦ (integrable_congr (h_eq i)).mp (hf.integrable i)⟩

Premises used: MeasureTheory.integrable_congr, MeasureTheory.Submartingale.integrable, MeasureTheory.Submartingale, And.intro, Iff.mp
-- 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
inst_4 : LE E
hf : Submartingale f ℱ μ
hg : StronglyAdapted (β := fun (i : ι) ↦ E) ℱ g
h_eq : ∀ (t : ι), f t =ᶠ[ae μ] g t
refine : ∀ (i j : ι) (hij : i ≤ j), g i ≤ᶠ[ae μ] μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i]
⊢ Submartingale g ℱ μ

Tactic:
refine ⟨hg, fun i j hij ↦ ?_, fun i ↦ (integrable_congr (h_eq i)).mp (hf.integrable i)⟩
-- 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
inst_4 : LE E
hf : Submartingale f ℱ μ
hg : StronglyAdapted (β := fun (i : ι) ↦ E) ℱ g
h_eq : ∀ (t : ι), f t =ᶠ[ae μ] g t
i j : ι
hij : i ≤ j
⊢ g i ≤ᶠ[ae μ] μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i]

Tactic:
(Filter.eventuallyLE_congr (h_eq i) (condExp_congr_ae (h_eq j))).mp (ae_le_condExp hf hij)

Premises used: MeasureTheory.condExp_congr_ae, Filter.eventuallyLE_congr, Iff.mp, MeasureTheory.Submartingale.ae_le_condExp
-- 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
inst_4 : LE E
hf : Submartingale f ℱ μ
hg : StronglyAdapted (β := fun (i : ι) ↦ E) ℱ g
h_eq : ∀ (t : ι), f t =ᶠ[ae μ] g t
i j : ι
hij : i ≤ j
⊢ g i ≤ᶠ[ae μ] μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i]

Tactic:
exact (Filter.eventuallyLE_congr (h_eq i) (condExp_congr_ae (h_eq j))).mp (ae_le_condExp hf hij)

Premises used: MeasureTheory.condExp_congr_ae, Filter.eventuallyLE_congr, Iff.mp, MeasureTheory.Submartingale.ae_le_condExp
-- 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
inst_4 : Preorder E
inst_5 : AddLeftMono E
hf : Submartingale f ℱ μ
hg : Submartingale g ℱ μ
⊢ Submartingale (f + g) ℱ μ

Tactic:
⟨hf.1.add hg.1, fun i j hij => ?_, fun i => (hf.2.2 i).add (hg.2.2 i)⟩

Premises used: MeasureTheory.Submartingale, And.right, And.left, And.intro, MeasureTheory.Integrable.add, 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
inst_4 : Preorder E
inst_5 : AddLeftMono E
hf : Submartingale f ℱ μ
hg : Submartingale g ℱ μ
refine : ∀ (i j : ι) (hij : i ≤ j), (f + g) i ≤ᶠ[ae μ] μ[(f + g) j | (↑ℱ : ι → MeasurableSpace Ω) i]
⊢ Submartingale (f + g) ℱ μ

Tactic:
refine ⟨hf.1.add hg.1, fun i j hij => ?_, fun i => (hf.2.2 i).add (hg.2.2 i)⟩
-- 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
inst_4 : Preorder E
inst_5 : AddLeftMono E
hf : Submartingale f ℱ μ
hg : Submartingale g ℱ μ
i j : ι
hij : i ≤ j
⊢ (f + g) i ≤ᶠ[ae μ] μ[(f + g) j | (↑ℱ : ι → MeasurableSpace Ω) i]

Tactic:
EventuallyLE.trans ?_ (condExp_add (hf.integrable j) (hg.integrable j) _).symm.le

Premises used: MeasureTheory.Submartingale.integrable, Filter.EventuallyEq.le, MeasureTheory.condExp_add, Filter.EventuallyLE.trans, Filter.EventuallyEq.symm