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
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
refine : (f + g) i ≤ᶠ[ae μ] μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] + μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i]
⊢ (f + g) i ≤ᶠ[ae μ] μ[(f + g) j | (↑ℱ : ι → MeasurableSpace Ω) i]

Tactic:
refine 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
-- 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
h :
  ∀ (a : Ω),
    f i a ≤ μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] a →
      g i a ≤ μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i] a →
        (f + g) i a ≤ (μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] + μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i]) a
⊢ (f + g) i ≤ᶠ[ae μ] μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] + μ[g j | (↑ℱ : ι → MeasurableSpace Ω) 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 : Submartingale f ℱ μ
hg : Submartingale g ℱ μ
i j : ι
hij : i ≤ j
a : Ω
h : f i a ≤ μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] a
h_1 : g i a ≤ μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i] a
⊢ (f + g) i a ≤ (μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] + μ[g j | (↑ℱ : ι → MeasurableSpace Ω) 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 : Submartingale f ℱ μ
hg : Submartingale g ℱ μ
i j : ι
hij : i ≤ j
a : Ω
h_1 : f i a ≤ μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] a
h_2 : g i a ≤ μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i] a
h : f i a ≤ μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] a
h₁ : g i a ≤ μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i] a
⊢ (f + g) i a ≤ (μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] + μ[g j | (↑ℱ : ι → MeasurableSpace Ω) 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 : Submartingale f ℱ μ
hg : Submartingale g ℱ μ
i j : ι
hij : i ≤ j
a : Ω
h : f i a ≤ μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] a
h_1 : g i a ≤ μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i] a
⊢ f i a ≤ μ[f j | (↑ℱ : ι → MeasurableSpace Ω) 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 : Submartingale f ℱ μ
hg : Submartingale g ℱ μ
i j : ι
hij : i ≤ j
a : Ω
h : f i a ≤ μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] a
h_1 : g i a ≤ μ[g j | (↑ℱ : ι → MeasurableSpace Ω) i] a
⊢ g i a ≤ μ[g j | (↑ℱ : ι → MeasurableSpace Ω) 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 : Submartingale f ℱ μ
hg : Martingale g ℱ μ
⊢ Submartingale (f + g) ℱ μ

Tactic:
hf.add hg.submartingale

Premises used: MeasureTheory.Martingale.submartingale, MeasureTheory.Submartingale.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 : Submartingale f ℱ μ
⊢ Supermartingale (-f) ℱ μ

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

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

Tactic:
refine ⟨hf.1.neg, fun i j hij => (condExp_neg ..).le.trans ?_, 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 : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
a : Ω
h : f i a ≤ μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] a → (-μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i]) a ≤ (-f) i a
⊢ f i a ≤ μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] a → (-μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i]) a ≤ (-f) 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 : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
h :
  ∀ (a : Ω), f i a ≤ μ[f j | (↑ℱ : ι → MeasurableSpace Ω) 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 _ _

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 : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
a : Ω
h : f i a ≤ μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] a
⊢ (-μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i]) a ≤ (-f) 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
ℱ : 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 : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
rw : LE.le.{u_2} (α := E) (∫ (a : Ω) in s, -f j a ∂μ) (∫ (a : Ω) in s, -f i a ∂μ)
⊢ LE.le.{u_2} (α := E) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)

Tactic:
rw [← neg_le_neg_iff, ← integral_neg, ← integral_neg]

Premises used: MeasureTheory.integral_neg, neg_le_neg_iff
-- 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 : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
⊢ LE.le.{u_2} (α := E) (∫ (a : Ω) in s, -f j a ∂μ) (∫ (a : Ω) in s, -f i a ∂μ)

Tactic:
Supermartingale.setIntegral_le hf.neg hij hs

Premises used: MeasureTheory.Supermartingale.setIntegral_le, MeasureTheory.Submartingale.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
ℱ : 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 : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
⊢ LE.le.{u_2} (α := E) (∫ (a : Ω) in s, -f j a ∂μ) (∫ (a : Ω) in s, -f i a ∂μ)

Tactic:
exact Supermartingale.setIntegral_le hf.neg hij hs

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

Tactic:
hf.add hg.neg

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

Tactic:
exact hf.add hg.neg

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

Tactic:
hf.sub_supermartingale hg.supermartingale

Premises used: MeasureTheory.Submartingale.sub_supermartingale, MeasureTheory.Martingale.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
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : Lattice E
inst_5 : ContinuousSup E
inst_6 : HasSolidNorm E
inst_7 : IsOrderedAddMonoid E
inst_8 : IsOrderedModule ℝ E
f g : ι → Ω → E
hf : Submartingale f ℱ μ
hg : Submartingale g ℱ μ
⊢ Submartingale (f ⊔ g) ℱ μ

Tactic:
⟨fun i =>
    @StronglyMeasurable.sup _ _ _ _ (ℱ i) _ _ _ (hf.stronglyAdapted i) (hg.stronglyAdapted i),
    fun i j hij => ?_, fun i => Integrable.sup (hf.integrable _) (hg.integrable _)⟩

Premises used: MeasureTheory.Integrable.sup, MeasureTheory.Submartingale.integrable, MeasureTheory.StronglyMeasurable.sup, MeasureTheory.Submartingale, MeasureTheory.Submartingale.stronglyAdapted, 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
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : Lattice E
inst_5 : ContinuousSup E
inst_6 : HasSolidNorm E
inst_7 : IsOrderedAddMonoid E
inst_8 : IsOrderedModule ℝ E
f g : ι → Ω → 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 ⟨fun i =>
    @StronglyMeasurable.sup _ _ _ _ (ℱ i) _ _ _ (hf.stronglyAdapted i) (hg.stronglyAdapted i),
    fun i j hij => ?_, fun i => Integrable.sup (hf.integrable _) (hg.integrable _)⟩
-- 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 : Lattice E
inst_5 : ContinuousSup E
inst_6 : HasSolidNorm E
inst_7 : IsOrderedAddMonoid E
inst_8 : IsOrderedModule ℝ E
f g : ι → Ω → E
hf : Submartingale f ℱ μ
hg : Submartingale g ℱ μ
i j : ι
hij : i ≤ j
⊢ (f ⊔ g) i ≤ᶠ[ae μ] μ[(f ⊔ g) j | (↑ℱ : ι → MeasurableSpace Ω) i]

Tactic:
EventuallyLE.sup_le ?_ ?_

Premises used: Filter.EventuallyLE.sup_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 : Lattice E
inst_5 : ContinuousSup E
inst_6 : HasSolidNorm E
inst_7 : IsOrderedAddMonoid E
inst_8 : IsOrderedModule ℝ E
f g : ι → Ω → E
hf : Submartingale f ℱ μ
hg : Submartingale g ℱ μ
i j : ι
hij : i ≤ j
refine_1 : f i ≤ᶠ[ae μ] μ[(f ⊔ g) j | (↑ℱ : ι → MeasurableSpace Ω) i]
refine_2 : g i ≤ᶠ[ae μ] μ[(f ⊔ g) j | (↑ℱ : ι → MeasurableSpace Ω) i]
⊢ (f ⊔ g) i ≤ᶠ[ae μ] μ[(f ⊔ g) j | (↑ℱ : ι → MeasurableSpace Ω) i]

Tactic:
refine EventuallyLE.sup_le ?_ ?_

Premises used: Filter.EventuallyLE.sup_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 : Lattice E
inst_5 : ContinuousSup E
inst_6 : HasSolidNorm E
inst_7 : IsOrderedAddMonoid E
inst_8 : IsOrderedModule ℝ E
f g : ι → Ω → E
hf : Submartingale f ℱ μ
hg : Submartingale g ℱ μ
i j : ι
hij : i ≤ j
⊢ f i ≤ᶠ[ae μ] μ[(f ⊔ g) j | (↑ℱ : ι → MeasurableSpace Ω) i]

Tactic:
EventuallyLE.trans (hf.2.1 i j hij)
      (condExp_mono (hf.integrable _) (Integrable.sup (hf.integrable j) (hg.integrable j))
        (Eventually.of_forall fun x => le_sup_left))

Premises used: MeasureTheory.Integrable.sup, le_sup_left, MeasureTheory.Submartingale.integrable, MeasureTheory.condExp_mono, Filter.Eventually.of_forall, And.right, And.left, 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
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : Lattice E
inst_5 : ContinuousSup E
inst_6 : HasSolidNorm E
inst_7 : IsOrderedAddMonoid E
inst_8 : IsOrderedModule ℝ E
f g : ι → Ω → E
hf : Submartingale f ℱ μ
hg : Submartingale g ℱ μ
i j : ι
hij : i ≤ j
⊢ f i ≤ᶠ[ae μ] μ[(f ⊔ g) j | (↑ℱ : ι → MeasurableSpace Ω) i]

Tactic:
exact EventuallyLE.trans (hf.2.1 i j hij)
      (condExp_mono (hf.integrable _) (Integrable.sup (hf.integrable j) (hg.integrable j))
        (Eventually.of_forall fun x => le_sup_left))

Premises used: MeasureTheory.Integrable.sup, le_sup_left, MeasureTheory.Submartingale.integrable, MeasureTheory.condExp_mono, Filter.Eventually.of_forall, And.right, And.left, 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
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : Lattice E
inst_5 : ContinuousSup E
inst_6 : HasSolidNorm E
inst_7 : IsOrderedAddMonoid E
inst_8 : IsOrderedModule ℝ E
f g : ι → Ω → E
hf : Submartingale f ℱ μ
hg : Submartingale g ℱ μ
i j : ι
hij : i ≤ j
⊢ g i ≤ᶠ[ae μ] μ[(f ⊔ g) j | (↑ℱ : ι → MeasurableSpace Ω) i]

Tactic:
EventuallyLE.trans (hg.2.1 i j hij)
      (condExp_mono (hg.integrable _) (Integrable.sup (hf.integrable j) (hg.integrable j))
        (Eventually.of_forall fun x => le_sup_right))

Premises used: MeasureTheory.Integrable.sup, MeasureTheory.Submartingale.integrable, MeasureTheory.condExp_mono, le_sup_right, Filter.Eventually.of_forall, And.right, And.left, 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
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : Lattice E
inst_5 : ContinuousSup E
inst_6 : HasSolidNorm E
inst_7 : IsOrderedAddMonoid E
inst_8 : IsOrderedModule ℝ E
f g : ι → Ω → E
hf : Submartingale f ℱ μ
hg : Submartingale g ℱ μ
i j : ι
hij : i ≤ j
⊢ g i ≤ᶠ[ae μ] μ[(f ⊔ g) j | (↑ℱ : ι → MeasurableSpace Ω) i]

Tactic:
exact EventuallyLE.trans (hg.2.1 i j hij)
      (condExp_mono (hg.integrable _) (Integrable.sup (hf.integrable j) (hg.integrable j))
        (Eventually.of_forall fun x => le_sup_right))

Premises used: MeasureTheory.Integrable.sup, MeasureTheory.Submartingale.integrable, MeasureTheory.condExp_mono, le_sup_right, Filter.Eventually.of_forall, And.right, And.left, 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
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : Lattice E
inst_5 : ContinuousSup E
inst_6 : HasSolidNorm E
inst_7 : IsOrderedAddMonoid E
inst_8 : IsOrderedModule ℝ E
f : ι → Ω → E
hf : Submartingale f ℱ μ
⊢ Submartingale f⁺ ℱ μ

Tactic:
hf.sup (martingale_zero _ _ _).submartingale

Premises used: MeasureTheory.Martingale.submartingale, MeasureTheory.martingale_zero, MeasureTheory.Submartingale.sup
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
inst_1 : SigmaFiniteFiltration μ ℱ
f : ι → Ω → ℝ
hadp : StronglyAdapted (β := fun (i : ι) ↦ ℝ) ℱ f
hint : ∀ (i : ι), Integrable (f i) μ
hf :
  ∀ (i j : ι),
    i ≤ j → ∀ (s : Set Ω), MeasurableSet s → LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)
⊢ Submartingale f ℱ μ

Tactic:
⟨hadp, fun i j hij => ?_, hint⟩

Premises used: MeasureTheory.Submartingale, And.intro
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
inst_1 : SigmaFiniteFiltration μ ℱ
f : ι → Ω → ℝ
hadp : StronglyAdapted (β := fun (i : ι) ↦ ℝ) ℱ f
hint : ∀ (i : ι), Integrable (f i) μ
hf :
  ∀ (i j : ι),
    i ≤ j → ∀ (s : Set Ω), MeasurableSet s → LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)
refine : ∀ (i j : ι) (hij : i ≤ j), f i ≤ᶠ[ae μ] μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i]
⊢ Submartingale f ℱ μ

Tactic:
refine ⟨hadp, fun i j hij => ?_, hint⟩
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
inst_1 : SigmaFiniteFiltration μ ℱ
f : ι → Ω → ℝ
hadp : StronglyAdapted (β := fun (i : ι) ↦ ℝ) ℱ f
hint : ∀ (i : ι), Integrable (f i) μ
hf :
  ∀ (i j : ι),
    i ≤ j → ∀ (s : Set Ω), MeasurableSet s → LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)
i j : ι
hij : i ≤ j
this : f i ≤ᶠ[ae (μ.trim ⋯)] μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i]
⊢ f i ≤ᶠ[ae μ] μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i]

Tactic:
ae_le_of_ae_le_trim this

Premises used: MeasureTheory.ae_le_of_ae_le_trim
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
inst_1 : SigmaFiniteFiltration μ ℱ
f : ι → Ω → ℝ
hadp : StronglyAdapted (β := fun (i : ι) ↦ ℝ) ℱ f
hint : ∀ (i : ι), Integrable (f i) μ
hf :
  ∀ (i j : ι),
    i ≤ j → ∀ (s : Set Ω), MeasurableSet s → LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)
i j : ι
hij : i ≤ j
this : f i ≤ᶠ[ae (μ.trim ⋯)] μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i]
⊢ f i ≤ᶠ[ae μ] μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i]

Tactic:
exact ae_le_of_ae_le_trim this

Premises used: MeasureTheory.ae_le_of_ae_le_trim
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
inst_1 : SigmaFiniteFiltration μ ℱ
f : ι → Ω → ℝ
hadp : StronglyAdapted (β := fun (i : ι) ↦ ℝ) ℱ f
hint : ∀ (i : ι), Integrable (f i) μ
hf :
  ∀ (i j : ι),
    i ≤ j → ∀ (s : Set Ω), MeasurableSet s → LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)
i j : ι
hij : i ≤ j
suffices : f i ≤ᶠ[ae (μ.trim ⋯)] μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i]
⊢ f i ≤ᶠ[ae μ] μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i]

Tactic:
suffices f i ≤ᵐ[μ.trim (ℱ.le i)] μ[f j | ℱ i] by exact ae_le_of_ae_le_trim this
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
inst_1 : SigmaFiniteFiltration μ ℱ
f : ι → Ω → ℝ
hadp : StronglyAdapted (β := fun (i : ι) ↦ ℝ) ℱ f
hint : ∀ (i : ι), Integrable (f i) μ
hf :
  ∀ (i j : ι),
    i ≤ j → ∀ (s : Set Ω), MeasurableSet s → LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)
i j : ι
hij : i ≤ j
this : 0 ≤ᶠ[ae (μ.trim ⋯)] μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] - f i
h :
  ∀ (x : Ω) (hx : 0 x ≤ (μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] - f i) x),
    f i x ≤ μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] x
⊢ f i ≤ᶠ[ae (μ.trim ⋯)] μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i]

Tactic:
filter_upwards [this] with x hx
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
inst_1 : SigmaFiniteFiltration μ ℱ
f : ι → Ω → ℝ
hadp : StronglyAdapted (β := fun (i : ι) ↦ ℝ) ℱ f
hint : ∀ (i : ι), Integrable (f i) μ
hf :
  ∀ (i j : ι),
    i ≤ j → ∀ (s : Set Ω), MeasurableSet s → LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)
i j : ι
hij : i ≤ j
this : 0 ≤ᶠ[ae (μ.trim ⋯)] μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] - f i
x : Ω
hx : 0 x ≤ (μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] - f i) x
h h₁ h₂ h₃ : 0 ≤ μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] x - f i x
⊢ f i x ≤ μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] x

Tactic:
rwa [← sub_nonneg]

Premises used: sub_nonneg
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
inst_1 : SigmaFiniteFiltration μ ℱ
f : ι → Ω → ℝ
hadp : StronglyAdapted (β := fun (i : ι) ↦ ℝ) ℱ f
hint : ∀ (i : ι), Integrable (f i) μ
hf :
  ∀ (i j : ι),
    i ≤ j → ∀ (s : Set Ω), MeasurableSet s → LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)
i j : ι
hij : i ≤ j
suffices : 0 ≤ᶠ[ae (μ.trim ⋯)] μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] - f i
⊢ f i ≤ᶠ[ae (μ.trim ⋯)] μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i]

Tactic:
suffices 0 ≤ᵐ[μ.trim (ℱ.le i)] μ[f j | ℱ i] - f i by
    filter_upwards [this] with x hx
    rwa [← sub_nonneg]