awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
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) ℱ μ
have rw : Submartingale (f + -g) ℱ μ
Tactic: rw [sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
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) ℱ μ
have refine : ∀ (i j : ι) (hij : i ≤ j), (f ⊔ g) i ≤ᶠ[ae μ] μ[(f ⊔ g) j | (↑ℱ : ι → MeasurableSpace Ω) i]
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 _)⟩
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
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]
have refine_1 : f i ≤ᶠ[ae μ] μ[(f ⊔ g) j | (↑ℱ : ι → MeasurableSpace Ω) i]
Tactic: refine EventuallyLE.sup_le ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
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]
⊢ (f ⊔ g) i ≤ᶠ[ae μ] μ[(f ⊔ g) j | (↑ℱ : ι → MeasurableSpace Ω) i]
have refine_2 : g i ≤ᶠ[ae μ] μ[(f ⊔ g) j | (↑ℱ : ι → MeasurableSpace Ω) i]
Tactic: refine EventuallyLE.sup_le ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
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 ℱ μ
have refine : ∀ (i j : ι) (hij : i ≤ j), f i ≤ᶠ[ae μ] μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i]
Tactic: refine ⟨hadp, fun i j hij => ?_, hint⟩
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
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
⊢ f i ≤ᶠ[ae μ] μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i]
have suffices : f i ≤ᶠ[ae (μ.trim sorry)] μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i]
Tactic: suffices f i ≤ᵐ[μ.trim (ℱ.le i)] μ[f j | ℱ i] by exact ae_le_of_ae_le_trim this
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
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
⊢ f i ≤ᶠ[ae (μ.trim ⋯)] μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i]
have h : ∀ (x : Ω) (hx : 0 x ≤ (μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] - f i) x),
  f i x ≤ μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] x
Tactic: filter_upwards [this] with x hx
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
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
⊢ f i x ≤ μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] x
have h : 0 ≤ μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] x - f i x
Tactic: rwa [← sub_nonneg]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
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
⊢ f i ≤ᶠ[ae (μ.trim ⋯)] μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i]
have suffices : 0 ≤ᶠ[ae (μ.trim sorry)] μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] - f i
Tactic: suffices 0 ≤ᵐ[μ.trim (ℱ.le i)] μ[f j | ℱ i] - f i by
    filter_upwards [this] with x hx
    rwa [← sub_nonneg]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
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
have refine : ∀ (s : Set Ω) (hs : MeasurableSet s),
  LT.lt (α := ℝ≥0∞) ((μ.trim sorry : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
    LE.le (α := ℝ) 0 (∫ (x : Ω) in s, (μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] - f i) x ∂μ.trim sorry)
Tactic: refine ae_nonneg_of_forall_setIntegral_nonneg
    ((integrable_condExp.sub (hint i)).trim _ (stronglyMeasurable_condExp.sub <| hadp i))
      fun s hs _ => ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (hypothesis)
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 (α := ℝ) 0 (∫ (x : Ω) in s, (μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] - f i) x ∂μ.trim ⋯)
have hf₁ : LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)
Tactic: specialize hf i j hij s hs
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
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 ω ∂μ)
⊢ LE.le (α := ℝ) 0 (∫ (x : Ω) in s, (μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] - f i) x ∂μ.trim ⋯)
have rwa : LE.le (α := ℝ) 0 (∫ (x : Ω) in s, (μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] - f i) x ∂μ)
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]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
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 ∂μ)
⊢ LE.le (α := ℝ) 0 (∫ (x : Ω) in s, (μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] - f i) x ∂μ.trim ⋯)
have rwa₁ : 0 ≤ HSub.hSub (α := ℝ) (∫ (a : Ω) in s, μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] a ∂μ) (∫ (a : Ω) in s, f i a ∂μ)
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]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
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 ∂μ)
⊢ LE.le (α := ℝ) 0 (∫ (x : Ω) in s, (μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] - f i) x ∂μ.trim ⋯)
have rwa₂ : LE.le (α := ℝ) (∫ (a : Ω) in s, f i a ∂μ) (∫ (a : Ω) in s, μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] a ∂μ)
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]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
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 ℱ μ
have refine : ∀ (i j : ι) (hij : i ≤ j), f i ≤ᶠ[ae μ] μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i]
Tactic: refine ⟨hadp, fun i j hij => ?_, hint⟩
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
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
⊢ f i ≤ᶠ[ae μ] μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i]
have rw : 0 ≤ᶠ[ae μ] μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] - μ[f i | (↑ℱ : ι → MeasurableSpace Ω) i]
Tactic: rw [← condExp_of_stronglyMeasurable (ℱ.le _) (hadp _) (hint _), ← eventually_sub_nonneg]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
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
⊢ 0 ≤ᶠ[ae μ] μ[f j - f i | (↑ℱ : ι → MeasurableSpace Ω) i]
have pos : ∀ (h : SigmaFinite (μ.trim sorry)), 0 ≤ᶠ[ae μ] μ[f j - f i | (↑ℱ : ι → MeasurableSpace Ω) i]
Tactic: by_cases h : SigmaFinite (μ.trim (ℱ.le i))
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
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]
⊢ 0 ≤ᶠ[ae μ] μ[f j - f i | (↑ℱ : ι → MeasurableSpace Ω) i]
have neg : ∀ (h : ¬SigmaFinite (μ.trim sorry)), 0 ≤ᶠ[ae μ] μ[f j - f i | (↑ℱ : ι → MeasurableSpace Ω) i]
Tactic: by_cases h : SigmaFinite (μ.trim (ℱ.le i))
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
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]
have neg : EventuallyLE.{u_1, u_2} (β := E) (ae μ) 0 0
Tactic: rw [condExp_of_not_sigmaFinite (ℱ.le i) h]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
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]
have pos : 0 ≤ᶠ[ae μ] μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i] - μ[f i | (↑ℱ : ι → MeasurableSpace Ω) i]
Tactic: refine EventuallyLE.trans ?_ (condExp_sub (hf.integrable _) (hf.integrable _) _).symm.le
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
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 | (↑ℱ : ι → MeasurableSpace Ω) i] - μ[f i | (↑ℱ : ι → MeasurableSpace Ω) i]
have pos : f i ≤ᶠ[ae μ] μ[f j | (↑ℱ : ι → MeasurableSpace Ω) i]
Tactic: rw [eventually_sub_nonneg,
    condExp_of_stronglyMeasurable (ℱ.le _) (hf.stronglyAdapted _) (hf.integrable _)]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
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) ℱ μ
have rw : Supermartingale (f + -g) ℱ μ
Tactic: rw [sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
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) ℱ μ
have refine : ∀ (i j : ι) (hij : i ≤ j), μ[(c • f) j | (↑ℱ : ι → MeasurableSpace Ω) i] ≤ᶠ[ae μ] (c • f) i
Tactic: refine ⟨hf.1.smul c, fun i j hij => ?_, fun i => (hf.2.2 i).smul c⟩
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
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
⊢ μ[(c • f) j | (↑ℱ : ι → MeasurableSpace Ω) i] ≤ᶠ[ae μ] (c • f) i
have 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 ω
Tactic: filter_upwards [condExp_smul c (f j) (ℱ i), hf.2.1 i j hij] with ω hω hle
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
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) ℱ μ
have rw : Submartingale (-(-c • f)) ℱ μ
Tactic: rw [← neg_neg c, neg_smul]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
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) ℱ μ
have rw : Submartingale (-(c • -f)) ℱ μ
Tactic: rw [← neg_neg (c • f), ← smul_neg]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
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) ℱ μ
have rw : Supermartingale (-(-c • f)) ℱ μ
Tactic: rw [← neg_neg c, neg_smul]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
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 𝒢 μ
have refine : ∀ (i j : ℕ) (hij : i ≤ j) (s : Set Ω) (hs : MeasurableSet s),
  LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)
Tactic: refine submartingale_of_setIntegral_le hadp hint fun i j hij s hs => ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
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
⊢ LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)
have refl : LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f i ω ∂μ)
Tactic: induction hij with
  | refl => rfl
  | step hk₁ hk₂ => exact hk₂.trans (hf _ s (𝒢.mono hk₁ _ hs))
Cleared hypotheses: hij
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
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 ω ∂μ)
⊢ LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)
have 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 ω ∂μ)
Tactic: induction hij with
  | refl => rfl
  | step hk₁ hk₂ => exact hk₂.trans (hf _ s (𝒢.mono hk₁ _ hs))
Cleared hypotheses: hij
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
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 𝒢 μ
have rw : Supermartingale (- -f) 𝒢 μ
Tactic: rw [← neg_neg f]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
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) 𝒢 μ
have refine : ∀ (i : ℕ) (s : Set Ω),
  MeasurableSet s → LE.le (α := ℝ) (∫ (ω : Ω) in s, (-f) i ω ∂μ) (∫ (ω : Ω) in s, (-f) (i + 1) ω ∂μ)
Tactic: refine (submartingale_of_setIntegral_le_succ hadp.neg (fun i => (hint i).neg) ?_).neg
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
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 𝒢 μ
have refine : ∀ (i j : ℕ) (hij : i ≤ j), f i ≤ᶠ[ae μ] μ[f j | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
Tactic: refine ⟨hadp, fun i j hij ↦ ?_, hint⟩
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
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]
have base : ∀ (x : Ω), f i x ≤ μ[f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i] x
Tactic: refine ae_of_all _ fun _ ↦ ?_