awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) ω ∂μ)
refine :
  ∀ (i j : ℕ) (hij : i ≤ j) (s : Set Ω) (hs : MeasurableSet s),
    LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)
⊢ Submartingale f 𝒢 μ

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

Premises used: MeasureTheory.submartingale_of_setIntegral_le
-- 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) ω ∂μ)
i j : ℕ
s : Set Ω
hs : MeasurableSet s
⊢ LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f i ω ∂μ)

Tactic:
rfl
-- 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) ω ∂μ)
i j : ℕ
s : Set Ω
hs : MeasurableSet s
m : ℕ
hk₁ : i.le m
hk₂ : LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f m ω ∂μ)
⊢ LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f m.succ ω ∂μ)

Tactic:
hk₂.trans (hf _ s (𝒢.mono hk₁ _ hs))

Premises used: MeasureTheory.Filtration.mono, LE.le.trans
-- 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) ω ∂μ)
i j : ℕ
s : Set Ω
hs : MeasurableSet s
m : ℕ
hk₁ : i.le m
hk₂ : LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f m ω ∂μ)
⊢ LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f m.succ ω ∂μ)

Tactic:
exact hk₂.trans (hf _ s (𝒢.mono hk₁ _ hs))

Premises used: MeasureTheory.Filtration.mono, LE.le.trans
-- 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) ω ∂μ)
i j : ℕ
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
refl : LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f i ω ∂μ)
step :
  ∀ {m : ℕ} (hk₁ : i.le m) (hk₂ : LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f m ω ∂μ)),
    LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f m.succ ω ∂μ)
⊢ LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)

Tactic:
induction hij with
  | refl => rfl
  | step hk₁ hk₂ => exact hk₂.trans (hf _ s (𝒢.mono hk₁ _ hs))

Premises used: refl
-- 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 + 1) ω ∂μ) (∫ (ω : Ω) in s, f i ω ∂μ)
rw : Supermartingale (- -f) 𝒢 μ
⊢ Supermartingale f 𝒢 μ

Tactic:
rw [← neg_neg f]

Premises used: neg_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 + 1) ω ∂μ) (∫ (ω : Ω) in s, f i ω ∂μ)
⊢ Supermartingale (- -f) 𝒢 μ

Tactic:
(submartingale_of_setIntegral_le_succ hadp.neg (fun i => (hint i).neg) ?_).neg

Premises used: MeasureTheory.Integrable.neg, MeasureTheory.submartingale_of_setIntegral_le_succ, MeasureTheory.StronglyAdapted.neg, 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 + 1) ω ∂μ) (∫ (ω : Ω) in s, f i ω ∂μ)
refine :
  ∀ (i : ℕ) (s : Set Ω),
    MeasurableSet s → LE.le (α := ℝ) (∫ (ω : Ω) in s, (-f) i ω ∂μ) (∫ (ω : Ω) in s, (-f) (i + 1) ω ∂μ)
⊢ Supermartingale (- -f) 𝒢 μ

Tactic:
refine (submartingale_of_setIntegral_le_succ hadp.neg (fun i => (hint i).neg) ?_).neg

Premises used: MeasureTheory.Integrable.neg, MeasureTheory.submartingale_of_setIntegral_le_succ, MeasureTheory.StronglyAdapted.neg, 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 + 1) ω ∂μ) (∫ (ω : Ω) in s, f i ω ∂μ)
⊢ ∀ (i : ℕ) (s : Set Ω),
    MeasurableSet s → LE.le (α := ℝ) (∫ (ω : Ω) in s, (-f) i ω ∂μ) (∫ (ω : Ω) in s, (-f) (i + 1) ω ∂μ)

Tactic:
simpa only [integral_neg, Pi.neg_apply, neg_le_neg_iff]

Premises used: MeasureTheory.integral_neg, Pi.neg_apply, neg_le_neg_iff
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedModule ℝ E
inst_7 : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ E) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), f i ≤ᶠ[ae μ] μ[f (i + 1) | (↑𝒢 : ℕ → 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
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedModule ℝ E
inst_7 : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ E) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), f i ≤ᶠ[ae μ] μ[f (i + 1) | (↑𝒢 : ℕ → 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
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedModule ℝ E
inst_7 : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ E) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), f i ≤ᶠ[ae μ] μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
i j : ℕ
⊢ f i ≤ᶠ[ae μ] μ[f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i]

Tactic:
ae_of_all _ fun _ ↦ ?_

Premises used: MeasureTheory.ae_of_all, Filter.EventuallyLE
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedModule ℝ E
inst_7 : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ E) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), f i ≤ᶠ[ae μ] μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
i j : ℕ
base : ∀ (x : Ω), f i x ≤ μ[f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i] x
⊢ f i ≤ᶠ[ae μ] μ[f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i]

Tactic:
refine ae_of_all _ fun _ ↦ ?_

Premises used: MeasureTheory.ae_of_all
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedModule ℝ E
inst_7 : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ E) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), f i ≤ᶠ[ae μ] μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
i j : ℕ
x : Ω
base base₁ : f i x ≤ f i x
⊢ f i x ≤ μ[f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i] x

Tactic:
rw [condExp_of_stronglyMeasurable (𝒢.le i) (hadp i) (hint i)]

Premises used: MeasureTheory.condExp_of_stronglyMeasurable, MeasureTheory.Filtration.le
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedModule ℝ E
inst_7 : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ E) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), f i ≤ᶠ[ae μ] μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
i j k : ℕ
hik : i ≤ k
hk : f i ≤ᶠ[ae μ] μ[f k | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
h :
  ∀ (ω : Ω) (hω1 : f i ω ≤ μ[f k | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω)
    (hω2 :
      μ[f k | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω ≤
        μ[μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) k] | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω)
    (hω3 :
      μ[μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) k] | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω =
        μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω),
    f i ω ≤ μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
⊢ f i ≤ᶠ[ae μ] μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]

Tactic:
filter_upwards [hk, condExp_mono (hint k) integrable_condExp (hf k),
      𝒢.condExp_condExp (f (k + 1)) hik] with ω hω1 hω2 hω3

Premises used: MeasureTheory.integrable_condExp, MeasureTheory.Filtration.condExp_condExp, MeasureTheory.condExp_mono, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedModule ℝ E
inst_7 : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ E) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), f i ≤ᶠ[ae μ] μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
i j k : ℕ
hik : i ≤ k
hk : f i ≤ᶠ[ae μ] μ[f k | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
ω : Ω
hω1 : f i ω ≤ μ[f k | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
hω2 :
  μ[f k | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω ≤
    μ[μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) k] | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
hω3 :
  μ[μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) k] | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω =
    μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
h : μ[f k | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω ≤ μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
h₁ :
  μ[μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) k] | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω ≤
    μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
h₂ h₃ : μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω ≤ μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
⊢ f i ω ≤ μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω

Tactic:
grw [hω1, hω2, hω3]
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedModule ℝ E
inst_7 : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ E) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), f i ≤ᶠ[ae μ] μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
i j : ℕ
hij : i ≤ j
base : f i ≤ᶠ[ae μ] μ[f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
succ :
  ∀ (k : ℕ) (hik : i ≤ k) (hk : f i ≤ᶠ[ae μ] μ[f k | (↑𝒢 : ℕ → MeasurableSpace Ω) i]),
    f i ≤ᶠ[ae μ] μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
⊢ f i ≤ᶠ[ae μ] μ[f j | (↑𝒢 : ℕ → MeasurableSpace Ω) i]

Tactic:
induction j, hij using Nat.le_induction with
  | base =>
    refine ae_of_all _ fun _ ↦ ?_
    rw [condExp_of_stronglyMeasurable (𝒢.le i) (hadp i) (hint i)]
  | succ k hik hk =>
    filter_upwards [hk, condExp_mono (hint k) integrable_condExp (hf k),
      𝒢.condExp_condExp (f (k + 1)) hik] with ω hω1 hω2 hω3
    grw [hω1, hω2, hω3]

Premises used: MeasureTheory.condExp_of_stronglyMeasurable, MeasureTheory.ae_of_all, MeasureTheory.Filtration.le
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedModule ℝ E
inst_7 : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ E) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ≤ᶠ[ae μ] f i
rw : Supermartingale (- -f) 𝒢 μ
⊢ Supermartingale f 𝒢 μ

Tactic:
rw [← neg_neg f]

Premises used: neg_neg
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedModule ℝ E
inst_7 : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ E) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ≤ᶠ[ae μ] f i
⊢ Supermartingale (- -f) 𝒢 μ

Tactic:
(submartingale_nat hadp.neg (fun i => (hint i).neg) fun i =>
    EventuallyLE.trans ?_ (condExp_neg ..).symm.le).neg

Premises used: MeasureTheory.Filtration.seq, MeasureTheory.Integrable.neg, MeasureTheory.submartingale_nat, MeasureTheory.condExp_neg, Filter.EventuallyEq.le, MeasureTheory.StronglyAdapted.neg, MeasureTheory.Submartingale.neg, HAdd.hAdd, OfNat.ofNat, Filter.EventuallyLE.trans, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedModule ℝ E
inst_7 : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ E) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ≤ᶠ[ae μ] f i
refine : ∀ (i : ℕ), (-f) i ≤ᶠ[ae μ] -μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
⊢ Supermartingale (- -f) 𝒢 μ

Tactic:
refine (submartingale_nat hadp.neg (fun i => (hint i).neg) fun i =>
    EventuallyLE.trans ?_ (condExp_neg ..).symm.le).neg

Premises used: MeasureTheory.Filtration.seq, MeasureTheory.Integrable.neg, MeasureTheory.submartingale_nat, MeasureTheory.condExp_neg, Filter.EventuallyEq.le, MeasureTheory.StronglyAdapted.neg, MeasureTheory.Submartingale.neg, HAdd.hAdd, OfNat.ofNat, Filter.EventuallyLE.trans, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedModule ℝ E
inst_7 : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ E) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ≤ᶠ[ae μ] f i
i : ℕ
x : Ω
hx : μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] x ≤ f i x
⊢ (-f) i x ≤ (-μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]) x

Tactic:
neg_le_neg hx

Premises used: neg_le_neg
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedModule ℝ E
inst_7 : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ E) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ≤ᶠ[ae μ] f i
i : ℕ
h :
  ∀ (a : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] x ≤ f i x) x}
            x →
          Membership.mem (γ := Set Ω)
            {x : Ω | (fun (x : Ω) ↦ (-f) i x ≤ (-μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]) x) x} x}
      a
h₁ h₂ :
  ∀ (x : Ω) (hx : μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] x ≤ f i x),
    (-f) i x ≤ (-μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]) x
⊢ (-f) i ≤ᶠ[ae μ] -μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]

Tactic:
filter_upwards [hf i] with x hx using neg_le_neg hx
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedModule ℝ E
inst_7 : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ E) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), 0 ≤ᶠ[ae μ] μ[f (i + 1) - f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
⊢ Submartingale f 𝒢 μ

Tactic:
submartingale_nat hadp hint fun i => ?_

Premises used: MeasureTheory.submartingale_nat
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedModule ℝ E
inst_7 : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ E) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), 0 ≤ᶠ[ae μ] μ[f (i + 1) - f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
refine : ∀ (i : ℕ), f i ≤ᶠ[ae μ] μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
⊢ Submartingale f 𝒢 μ

Tactic:
refine submartingale_nat hadp hint fun i => ?_

Premises used: MeasureTheory.submartingale_nat
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedModule ℝ E
inst_7 : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ E) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), 0 ≤ᶠ[ae μ] μ[f (i + 1) - f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
i : ℕ
rw : 0 ≤ᶠ[ae μ] μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] - μ[f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
⊢ f i ≤ᶠ[ae μ] μ[f (i + 1) | (↑𝒢 : ℕ → 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
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedModule ℝ E
inst_7 : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ E) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), 0 ≤ᶠ[ae μ] μ[f (i + 1) - f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
i : ℕ
⊢ 0 ≤ᶠ[ae μ] μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] - μ[f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i]

Tactic:
EventuallyLE.trans (hf i) (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
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedModule ℝ E
inst_7 : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ E) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), 0 ≤ᶠ[ae μ] μ[f (i + 1) - f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
i : ℕ
⊢ 0 ≤ᶠ[ae μ] μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] - μ[f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i]

Tactic:
exact EventuallyLE.trans (hf i) (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
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedModule ℝ E
inst_7 : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ E) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), 0 ≤ᶠ[ae μ] μ[f i - f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
rw : Supermartingale (- -f) 𝒢 μ
⊢ Supermartingale f 𝒢 μ

Tactic:
rw [← neg_neg f]

Premises used: neg_neg
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedModule ℝ E
inst_7 : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ E) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), 0 ≤ᶠ[ae μ] μ[f i - f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
⊢ Supermartingale (- -f) 𝒢 μ

Tactic:
(submartingale_of_condExp_sub_nonneg_nat hadp.neg (fun i => (hint i).neg) ?_).neg

Premises used: MeasureTheory.Integrable.neg, MeasureTheory.StronglyAdapted.neg, MeasureTheory.submartingale_of_condExp_sub_nonneg_nat, MeasureTheory.Submartingale.neg