awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ 0 ≤ᶠ[ae (μ.trim ⋯)] μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] - f i

Tactic:
ae_nonneg_of_forall_setIntegral_nonneg
    ((integrable_condExp.sub (hint i)).trim _ (stronglyMeasurable_condExp.sub <| hadp i))
      fun s hs _ => ?_

Premises used: MeasureTheory.StronglyMeasurable.sub, MeasureTheory.integrable_condExp, MeasureTheory.Integrable.sub, MeasureTheory.stronglyMeasurable_condExp, MeasureTheory.ae_nonneg_of_forall_setIntegral_nonneg, MeasureTheory.Integrable.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
refine :
  ∀ (s : Set Ω) (hs : MeasurableSet s),
    LT.lt (α := ℝ≥0∞) ((μ.trim ⋯ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
      LE.le (α := ℝ) 0 (∫ (x : Ω) in s, (μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] - f i) x ∂μ.trim ⋯)
⊢ 0 ≤ᶠ[ae (μ.trim ⋯)] μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] - f i

Tactic:
refine ae_nonneg_of_forall_setIntegral_nonneg
    ((integrable_condExp.sub (hint i)).trim _ (stronglyMeasurable_condExp.sub <| hadp i))
      fun s hs _ => ?_

Premises used: MeasureTheory.StronglyMeasurable.sub, MeasureTheory.integrable_condExp, MeasureTheory.Integrable.sub, MeasureTheory.stronglyMeasurable_condExp, MeasureTheory.ae_nonneg_of_forall_setIntegral_nonneg, MeasureTheory.Integrable.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
s : Set Ω
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((μ.trim ⋯ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)

Tactic:
specialize hf i j hij s hs
-- 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) μ
i j : ι
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((μ.trim ⋯ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)
rwa : LE.le (α := ℝ) 0 (∫ (x : Ω) in s, (μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] - f i) x ∂μ)
rwa₁ : 0 ≤ HSub.hSub (α := ℝ) (∫ (a : Ω) in s, μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] a ∂μ) (∫ (a : Ω) in s, f i a ∂μ)
rwa₂ : LE.le (α := ℝ) (∫ (a : Ω) in s, f i a ∂μ) (∫ (a : Ω) in s, μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] a ∂μ)
rwa₃ rwa₄ rwa₅ rwa₆ : LE.le (α := ℝ) (∫ (a : Ω) in s, f i a ∂μ) (∫ (x : Ω) in s, f j x ∂μ)
⊢ LE.le (α := ℝ) 0 (∫ (x : Ω) in s, (μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] - f i) x ∂μ.trim ⋯)

Tactic:
rwa [← setIntegral_trim _ (stronglyMeasurable_condExp.sub <| hadp i) hs,
    integral_sub' integrable_condExp.integrableOn (hint i).integrableOn, sub_nonneg,
    setIntegral_condExp (ℱ.le i) (hint j) hs]

Premises used: MeasureTheory.setIntegral_condExp, MeasureTheory.StronglyMeasurable.sub, MeasureTheory.integrable_condExp, MeasureTheory.setIntegral_trim, MeasureTheory.integral_sub', MeasureTheory.stronglyMeasurable_condExp, MeasureTheory.Filtration.le, MeasureTheory.Integrable.integrableOn, sub_nonneg
-- 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 : SigmaFiniteFiltration μ ℱ
f : ι → Ω → E
hadp : StronglyAdapted (β := fun (i : ι) ↦ E) ℱ f
hint : ∀ (i : ι), Integrable (f i) μ
hf : ∀ (i j : ι), i ≤ j → 0 ≤ᶠ[ae μ] μ[f j - f i | (↑ℱ : ι → MeasurableSpace Ω) i]
⊢ Submartingale f ℱ μ

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

Premises used: MeasureTheory.Submartingale, 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 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
inst_6 : SigmaFiniteFiltration μ ℱ
f : ι → Ω → E
hadp : StronglyAdapted (β := fun (i : ι) ↦ E) ℱ f
hint : ∀ (i : ι), Integrable (f i) μ
hf : ∀ (i j : ι), i ≤ j → 0 ≤ᶠ[ae μ] μ[f j - f i | (↑ℱ : ι → MeasurableSpace Ω) i]
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
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 : SigmaFiniteFiltration μ ℱ
f : ι → Ω → E
hadp : StronglyAdapted (β := fun (i : ι) ↦ E) ℱ f
hint : ∀ (i : ι), Integrable (f i) μ
hf : ∀ (i j : ι), i ≤ j → 0 ≤ᶠ[ae μ] μ[f j - f i | (↑ℱ : ι → MeasurableSpace Ω) i]
i j : ι
hij : i ≤ j
rw : 0 ≤ᶠ[ae μ] μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] - μ[f i | (↑ℱ : ι → MeasurableSpace Ω) i]
⊢ f i ≤ᶠ[ae μ] μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i]

Tactic:
rw [← condExp_of_stronglyMeasurable (ℱ.le _) (hadp _) (hint _), ← eventually_sub_nonneg]

Premises used: Filter.eventually_sub_nonneg, MeasureTheory.condExp_of_stronglyMeasurable, 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 : SigmaFiniteFiltration μ ℱ
f : ι → Ω → E
hadp : StronglyAdapted (β := fun (i : ι) ↦ E) ℱ f
hint : ∀ (i : ι), Integrable (f i) μ
hf : ∀ (i j : ι), i ≤ j → 0 ≤ᶠ[ae μ] μ[f j - f i | (↑ℱ : ι → MeasurableSpace Ω) i]
i j : ι
hij : i ≤ j
⊢ 0 ≤ᶠ[ae μ] μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] - μ[f i | (↑ℱ : ι → MeasurableSpace Ω) i]

Tactic:
EventuallyLE.trans (hf i j hij) (condExp_sub (hint _) (hint _) _).le

Premises used: Filter.EventuallyEq.le, MeasureTheory.condExp_sub, 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 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
inst_6 : SigmaFiniteFiltration μ ℱ
f : ι → Ω → E
hadp : StronglyAdapted (β := fun (i : ι) ↦ E) ℱ f
hint : ∀ (i : ι), Integrable (f i) μ
hf : ∀ (i j : ι), i ≤ j → 0 ≤ᶠ[ae μ] μ[f j - f i | (↑ℱ : ι → MeasurableSpace Ω) i]
i j : ι
hij : i ≤ j
⊢ 0 ≤ᶠ[ae μ] μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] - μ[f i | (↑ℱ : ι → MeasurableSpace Ω) i]

Tactic:
exact EventuallyLE.trans (hf i j hij) (condExp_sub (hint _) (hint _) _).le

Premises used: Filter.EventuallyEq.le, MeasureTheory.condExp_sub, 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 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
f : ι → Ω → E
hf : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
pos : ∀ (h : SigmaFinite (μ.trim ⋯)), 0 ≤ᶠ[ae μ] μ[f j - f i | (↑ℱ : ι → MeasurableSpace Ω) i]
neg : ∀ (h : ¬SigmaFinite (μ.trim ⋯)), 0 ≤ᶠ[ae μ] μ[f j - f i | (↑ℱ : ι → MeasurableSpace Ω) i]
⊢ 0 ≤ᶠ[ae μ] μ[f j - f i | (↑ℱ : ι → MeasurableSpace Ω) i]

Tactic:
by_cases h : SigmaFinite (μ.trim (ℱ.le i))

Premises used: MeasureTheory.SigmaFinite, MeasureTheory.Measure.trim, 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
f : ι → Ω → E
hf : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
h : ¬SigmaFinite (μ.trim ⋯)
neg neg₁ : EventuallyLE.{u_1, u_2} (β := E) (ae μ) 0 0
⊢ 0 ≤ᶠ[ae μ] μ[f j - f i | (↑ℱ : ι → MeasurableSpace Ω) i]

Tactic:
rw [condExp_of_not_sigmaFinite (ℱ.le i) h]

Premises used: MeasureTheory.condExp_of_not_sigmaFinite, 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
f : ι → Ω → E
hf : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
h : SigmaFinite (μ.trim ⋯)
⊢ 0 ≤ᶠ[ae μ] μ[f j - f i | (↑ℱ : ι → MeasurableSpace Ω) i]

Tactic:
EventuallyLE.trans ?_ (condExp_sub (hf.integrable _) (hf.integrable _) _).symm.le

Premises used: MeasureTheory.Submartingale.integrable, Filter.EventuallyEq.le, MeasureTheory.condExp_sub, 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
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
f : ι → Ω → E
hf : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
h : SigmaFinite (μ.trim ⋯)
pos : 0 ≤ᶠ[ae μ] μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] - μ[f i | (↑ℱ : ι → MeasurableSpace Ω) i]
⊢ 0 ≤ᶠ[ae μ] μ[f j - f i | (↑ℱ : ι → MeasurableSpace Ω) i]

Tactic:
refine EventuallyLE.trans ?_ (condExp_sub (hf.integrable _) (hf.integrable _) _).symm.le

Premises used: MeasureTheory.Submartingale.integrable, Filter.EventuallyEq.le, MeasureTheory.condExp_sub, 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
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
f : ι → Ω → E
hf : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
h : SigmaFinite (μ.trim ⋯)
pos : f i ≤ᶠ[ae μ] μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i]
⊢ 0 ≤ᶠ[ae μ] μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] - μ[f i | (↑ℱ : ι → MeasurableSpace Ω) i]

Tactic:
rw [eventually_sub_nonneg,
    condExp_of_stronglyMeasurable (ℱ.le _) (hf.stronglyAdapted _) (hf.integrable _)]

Premises used: Filter.eventually_sub_nonneg, MeasureTheory.Submartingale.integrable, MeasureTheory.condExp_of_stronglyMeasurable, MeasureTheory.Submartingale.stronglyAdapted, 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
f : ι → Ω → E
hf : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
h : SigmaFinite (μ.trim ⋯)
⊢ 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
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
f : ι → Ω → E
hf : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
h : SigmaFinite (μ.trim ⋯)
⊢ f i ≤ᶠ[ae μ] μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i]

Tactic:
exact 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
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
inst_6 : SigmaFiniteFiltration μ ℱ
f : ι → Ω → E
⊢ Submartingale f ℱ μ ↔
    StronglyAdapted (β := fun (i : ι) ↦ E) ℱ f ∧
      (∀ (i : ι), Integrable (f i) μ) ∧ ∀ (i j : ι), i ≤ j → 0 ≤ᶠ[ae μ] μ[f j - f i | (↑ℱ : ι → MeasurableSpace Ω) i]

Tactic:
⟨fun h => ⟨h.stronglyAdapted, h.integrable, fun _ _ => h.condExp_sub_nonneg⟩,
   fun ⟨hadp, hint, h⟩ => submartingale_of_condExp_sub_nonneg hadp hint h⟩

Premises used: MeasureTheory.Submartingale.integrable, MeasureTheory.Submartingale, MeasureTheory.Submartingale.stronglyAdapted, _private.0.MeasureTheory.submartingale_iff_condExp_sub_nonneg.match_1, And.intro, Iff.intro, MeasureTheory.submartingale_of_condExp_sub_nonneg, MeasureTheory.Submartingale.condExp_sub_nonneg
-- 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 : Submartingale g ℱ μ
rw : Supermartingale (f + -g) ℱ μ
⊢ Supermartingale (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 : Supermartingale f ℱ μ
hg : Submartingale g ℱ μ
⊢ Supermartingale (f + -g) ℱ μ

Tactic:
hf.add hg.neg

Premises used: MeasureTheory.Submartingale.neg, 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 g : ι → Ω → E
ℱ : Filtration ι m0
inst_3 : CompleteSpace E
inst_4 : Preorder E
inst_5 : AddLeftMono E
hf : Supermartingale f ℱ μ
hg : Submartingale g ℱ μ
⊢ Supermartingale (f + -g) ℱ μ

Tactic:
exact hf.add hg.neg

Premises used: MeasureTheory.Submartingale.neg, 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 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.sub_submartingale hg.submartingale

Premises used: MeasureTheory.Martingale.submartingale, MeasureTheory.Supermartingale.sub_submartingale
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
F : Type u_4
inst_1 : NormedAddCommGroup F
inst_2 : PartialOrder F
inst_3 : NormedSpace ℝ F
inst_4 : CompleteSpace F
inst_5 : IsOrderedModule ℝ F
f : ι → Ω → F
c : ℝ
hc : 0 ≤ c
hf : Supermartingale f ℱ μ
⊢ Supermartingale (c • f) ℱ μ

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

Premises used: MeasureTheory.Integrable.smul, MeasureTheory.StronglyAdapted.smul, And.right, And.left, And.intro, MeasureTheory.Supermartingale
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
F : Type u_4
inst_1 : NormedAddCommGroup F
inst_2 : PartialOrder F
inst_3 : NormedSpace ℝ F
inst_4 : CompleteSpace F
inst_5 : IsOrderedModule ℝ F
f : ι → Ω → F
c : ℝ
hc : 0 ≤ c
hf : Supermartingale f ℱ μ
refine : ∀ (i j : ι) (hij : i ≤ j), μ[(c • f) j | (↑ℱ : ι → MeasurableSpace Ω) i] ≤ᶠ[ae μ] (c • f) i
⊢ Supermartingale (c • f) ℱ μ

Tactic:
refine ⟨hf.1.smul c, fun i j hij => ?_, fun i => (hf.2.2 i).smul c⟩
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
F : Type u_4
inst_1 : NormedAddCommGroup F
inst_2 : PartialOrder F
inst_3 : NormedSpace ℝ F
inst_4 : CompleteSpace F
inst_5 : IsOrderedModule ℝ F
f : ι → Ω → F
c : ℝ
hc : 0 ≤ c
hf : Supermartingale f ℱ μ
i j : ι
hij : i ≤ j
h :
  ∀ (ω : Ω) (hω : μ[c • f j | (↑ℱ : ι → MeasurableSpace Ω) i] ω = (c • μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i]) ω)
    (hle : μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] ω ≤ f i ω),
    μ[(c • f) j | (↑ℱ : ι → MeasurableSpace Ω) i] ω ≤ (c • f) i ω
⊢ μ[(c • f) j | (↑ℱ : ι → MeasurableSpace Ω) i] ≤ᶠ[ae μ] (c • f) i

Tactic:
filter_upwards [condExp_smul c (f j) (ℱ i), hf.2.1 i j hij] with ω hω hle

Premises used: MeasureTheory.Filtration.seq, MeasureTheory.condExp_smul, And.right, And.left
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
F : Type u_4
inst_1 : NormedAddCommGroup F
inst_2 : PartialOrder F
inst_3 : NormedSpace ℝ F
inst_4 : CompleteSpace F
inst_5 : IsOrderedModule ℝ F
f : ι → Ω → F
c : ℝ
hc : 0 ≤ c
hf : Supermartingale f ℱ μ
i j : ι
hij : i ≤ j
ω : Ω
hω : μ[c • f j | (↑ℱ : ι → MeasurableSpace Ω) i] ω = (c • μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i]) ω
hle : μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] ω ≤ f i ω
⊢ μ[(c • f) j | (↑ℱ : ι → MeasurableSpace Ω) i] ω ≤ (c • f) i ω

Tactic:
simpa only [hω, Pi.smul_apply] using smul_le_smul_of_nonneg_left hle hc

Premises used: smul_le_smul_of_nonneg_left, Pi.smul_apply
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
F : Type u_4
inst_1 : NormedAddCommGroup F
inst_2 : PartialOrder F
inst_3 : NormedSpace ℝ F
inst_4 : CompleteSpace F
inst_5 : IsOrderedModule ℝ F
inst_6 : IsOrderedAddMonoid F
f : ι → Ω → F
c : ℝ
hc : c ≤ 0
hf : Supermartingale f ℱ μ
rw : Submartingale (-(-c • f)) ℱ μ
⊢ Submartingale (c • f) ℱ μ

Tactic:
rw [← neg_neg c, neg_smul]

Premises used: neg_smul, neg_neg
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
F : Type u_4
inst_1 : NormedAddCommGroup F
inst_2 : PartialOrder F
inst_3 : NormedSpace ℝ F
inst_4 : CompleteSpace F
inst_5 : IsOrderedModule ℝ F
inst_6 : IsOrderedAddMonoid F
f : ι → Ω → F
c : ℝ
hc : c ≤ 0
hf : Supermartingale f ℱ μ
⊢ Submartingale (-(-c • f)) ℱ μ

Tactic:
(hf.smul_nonneg <| neg_nonneg.2 hc).neg

Premises used: Iff.mpr, neg_nonneg, MeasureTheory.Supermartingale.neg, MeasureTheory.Supermartingale.smul_nonneg
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
F : Type u_4
inst_1 : NormedAddCommGroup F
inst_2 : PartialOrder F
inst_3 : NormedSpace ℝ F
inst_4 : CompleteSpace F
inst_5 : IsOrderedModule ℝ F
inst_6 : IsOrderedAddMonoid F
f : ι → Ω → F
c : ℝ
hc : c ≤ 0
hf : Supermartingale f ℱ μ
⊢ Submartingale (-(-c • f)) ℱ μ

Tactic:
exact (hf.smul_nonneg <| neg_nonneg.2 hc).neg

Premises used: Iff.mpr, neg_nonneg, MeasureTheory.Supermartingale.neg, MeasureTheory.Supermartingale.smul_nonneg
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
F : Type u_4
inst_1 : NormedAddCommGroup F
inst_2 : PartialOrder F
inst_3 : IsOrderedAddMonoid F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
inst_6 : IsOrderedModule ℝ F
f : ι → Ω → F
c : ℝ
hc : 0 ≤ c
hf : Submartingale f ℱ μ
rw : Submartingale (-(c • -f)) ℱ μ
⊢ Submartingale (c • f) ℱ μ

Tactic:
rw [← neg_neg (c • f), ← smul_neg]

Premises used: neg_neg, smul_neg, HSMul.hSMul
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
F : Type u_4
inst_1 : NormedAddCommGroup F
inst_2 : PartialOrder F
inst_3 : IsOrderedAddMonoid F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
inst_6 : IsOrderedModule ℝ F
f : ι → Ω → F
c : ℝ
hc : 0 ≤ c
hf : Submartingale f ℱ μ
⊢ Submartingale (-(c • -f)) ℱ μ

Tactic:
Supermartingale.neg (hf.neg.smul_nonneg hc)

Premises used: MeasureTheory.Submartingale.neg, MeasureTheory.Supermartingale.neg, MeasureTheory.Supermartingale.smul_nonneg
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
F : Type u_4
inst_1 : NormedAddCommGroup F
inst_2 : PartialOrder F
inst_3 : IsOrderedAddMonoid F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
inst_6 : IsOrderedModule ℝ F
f : ι → Ω → F
c : ℝ
hc : 0 ≤ c
hf : Submartingale f ℱ μ
⊢ Submartingale (-(c • -f)) ℱ μ

Tactic:
exact Supermartingale.neg (hf.neg.smul_nonneg hc)

Premises used: MeasureTheory.Submartingale.neg, MeasureTheory.Supermartingale.neg, MeasureTheory.Supermartingale.smul_nonneg
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
F : Type u_4
inst_1 : NormedAddCommGroup F
inst_2 : PartialOrder F
inst_3 : IsOrderedAddMonoid F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
inst_6 : IsOrderedModule ℝ F
f : ι → Ω → F
c : ℝ
hc : c ≤ 0
hf : Submartingale f ℱ μ
rw : Supermartingale (-(-c • f)) ℱ μ
⊢ Supermartingale (c • f) ℱ μ

Tactic:
rw [← neg_neg c, neg_smul]

Premises used: neg_smul, neg_neg
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
F : Type u_4
inst_1 : NormedAddCommGroup F
inst_2 : PartialOrder F
inst_3 : IsOrderedAddMonoid F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
inst_6 : IsOrderedModule ℝ F
f : ι → Ω → F
c : ℝ
hc : c ≤ 0
hf : Submartingale f ℱ μ
⊢ Supermartingale (-(-c • f)) ℱ μ

Tactic:
(hf.smul_nonneg <| neg_nonneg.2 hc).neg

Premises used: Iff.mpr, MeasureTheory.Submartingale.smul_nonneg, neg_nonneg, MeasureTheory.Submartingale.neg
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
ι : Type u_3
inst : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
F : Type u_4
inst_1 : NormedAddCommGroup F
inst_2 : PartialOrder F
inst_3 : IsOrderedAddMonoid F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
inst_6 : IsOrderedModule ℝ F
f : ι → Ω → F
c : ℝ
hc : c ≤ 0
hf : Submartingale f ℱ μ
⊢ Supermartingale (-(-c • f)) ℱ μ

Tactic:
exact (hf.smul_nonneg <| neg_nonneg.2 hc).neg

Premises used: Iff.mpr, MeasureTheory.Submartingale.smul_nonneg, neg_nonneg, MeasureTheory.Submartingale.neg
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ) (s : Set Ω), MeasurableSet s → LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f (i + 1) ω ∂μ)
⊢ Submartingale f 𝒢 μ

Tactic:
submartingale_of_setIntegral_le hadp hint fun i j hij s hs => ?_

Premises used: MeasureTheory.submartingale_of_setIntegral_le