mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Martingale.Basic

Goal state before:
pp: Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : Preorder ι
m0 : MeasurableSpace Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : OrderBot ι
ℱ : Filtration ι m0
μ : Measure Ω
inst✝ : SigmaFiniteFiltration μ ℱ
f : Ω → E
hf : StronglyMeasurable f
hfint : Integrable f μ
⊢ Martingale (fun x ↦ f) ℱ μ

Tactic:
by
  refine ⟨fun i => hf.mono <| ℱ.mono bot_le, fun i j _ => ?_⟩
  rw [condExp_of_stronglyMeasurable (ℱ.le _) (hf.mono <| ℱ.mono bot_le) hfint]

Goal state after:
Module: Mathlib.Probability.Martingale.Basic

Goal state before:
pp: Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f g : ι → Ω → E
ℱ : Filtration ι m0
inst✝ : CompleteSpace E
hf : Martingale f ℱ μ
hg : Martingale g ℱ μ
⊢ Martingale (f + -g) ℱ μ

Tactic:
;

Goal state after:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f g : ι → Ω → E
ℱ : Filtration ι m0
inst✝ : CompleteSpace E
hf : Martingale f ℱ μ
hg : Martingale g ℱ μ
⊢ Martingale (f + -g) ℱ μ
Module: Mathlib.Probability.Martingale.Basic

Goal state before:
pp: Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁵ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
f g : ι → Ω → E
ℱ : Filtration ι m0
inst✝² : CompleteSpace E
inst✝¹ : Preorder E
inst✝ : AddLeftMono E
hf : Submartingale f ℱ μ
hg : Supermartingale g ℱ μ
⊢ Submartingale (f + -g) ℱ μ

Tactic:
;

Goal state after:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁵ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
f g : ι → Ω → E
ℱ : Filtration ι m0
inst✝² : CompleteSpace E
inst✝¹ : Preorder E
inst✝ : AddLeftMono E
hf : Submartingale f ℱ μ
hg : Supermartingale g ℱ μ
⊢ Submartingale (f + -g) ℱ μ
Module: Mathlib.Probability.Martingale.Basic

Goal state before:
pp: case neg
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁵ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
ℱ : Filtration ι m0
inst✝² : CompleteSpace E
inst✝¹ : PartialOrder E
inst✝ : IsOrderedAddMonoid E
f : ι → Ω → E
hf : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
h : ¬SigmaFinite (μ.trim ⋯)
⊢ 0 ≤ᵐ[μ] μ[f j - f i | ↑ℱ i]

pp: case pos
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁵ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
ℱ : Filtration ι m0
inst✝² : CompleteSpace E
inst✝¹ : PartialOrder E
inst✝ : IsOrderedAddMonoid E
f : ι → Ω → E
hf : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
h : SigmaFinite (μ.trim ⋯)
⊢ 0 ≤ᵐ[μ] μ[f j - f i | ↑ℱ i]

Tactic:
;

Goal state after:
case neg
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁵ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
ℱ : Filtration ι m0
inst✝² : CompleteSpace E
inst✝¹ : PartialOrder E
inst✝ : IsOrderedAddMonoid E
f : ι → Ω → E
hf : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
h : ¬SigmaFinite (μ.trim ⋯)
⊢ 0 ≤ᵐ[μ] μ[f j - f i | ↑ℱ i]

case pos
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁵ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
ℱ : Filtration ι m0
inst✝² : CompleteSpace E
inst✝¹ : PartialOrder E
inst✝ : IsOrderedAddMonoid E
f : ι → Ω → E
hf : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
h : SigmaFinite (μ.trim ⋯)
⊢ 0 ≤ᵐ[μ] μ[f j - f i | ↑ℱ i]
Module: Mathlib.Probability.Martingale.Basic

Goal state before:
pp: Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁵ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
f g : ι → Ω → E
ℱ : Filtration ι m0
inst✝² : CompleteSpace E
inst✝¹ : Preorder E
inst✝ : AddLeftMono E
hf : Supermartingale f ℱ μ
hg : Submartingale g ℱ μ
⊢ Supermartingale (f + -g) ℱ μ

Tactic:
;

Goal state after:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁵ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
f g : ι → Ω → E
ℱ : Filtration ι m0
inst✝² : CompleteSpace E
inst✝¹ : Preorder E
inst✝ : AddLeftMono E
hf : Supermartingale f ℱ μ
hg : Submartingale g ℱ μ
⊢ Supermartingale (f + -g) ℱ μ
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: Ω : Type u_1
m✝ : MeasurableSpace Ω
E : Type u_3
inst✝ : TopologicalSpace E
𝓕 : Filtration ℕ m✝
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : ℕ → ℕ × Ω → E :=
  fun m x ↦
    match x.1 with
    | 0 => (h₀.approx m) x.2
    | n.succ => (⋯.approx m) x.2
Y : ℕ → ℕ × Ω → E := fun m x ↦ if x.1 ≤ m then X m x else X m (0, x.2)
n : ℕ
ω : Ω
m : ℕ
hm : n ≤ m
⊢ Y m (n, ω) = X m (n, ω)

Tactic:
;

Goal state after:
Ω : Type u_1
m✝ : MeasurableSpace Ω
E : Type u_3
inst✝ : TopologicalSpace E
𝓕 : Filtration ℕ m✝
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : ℕ → ℕ × Ω → E :=
  fun m x ↦
    match x.1 with
    | 0 => (h₀.approx m) x.2
    | n.succ => (⋯.approx m) x.2
Y : ℕ → ℕ × Ω → E := fun m x ↦ if x.1 ≤ m then X m x else X m (0, x.2)
n : ℕ
ω : Ω
m : ℕ
hm : n ≤ m
⊢ Y m (n, ω) = X m (n, ω)
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
hi_min : IsMin i
this : {ω | τ ω < ↑i} = ∅
⊢ MeasurableSet ∅

Tactic:
;

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
hi_min : IsMin i
this : {ω | τ ω < ↑i} = ∅
⊢ MeasurableSet ∅
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Preorder ι
inst✝ : InfSet ι
u : ι → Ω → β
n m : ι
x✝ : Ω
⊢ hittingBtwn u ∅ n m x✝ = m

Tactic:
;

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Preorder ι
inst✝ : InfSet ι
u : ι → Ω → β
n m : ι
x✝ : Ω
⊢ hittingBtwn u ∅ n m x✝ = m
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Preorder ι
inst✝ : InfSet ι
u : ι → Ω → β
n : ι
x✝ : Ω
⊢ hittingAfter u ∅ n x✝ = ⊤

Tactic:
;

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Preorder ι
inst✝ : InfSet ι
u : ι → Ω → β
n : ι
x✝ : Ω
⊢ hittingAfter u ∅ n x✝ = ⊤
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
ω : Ω
m : ι
hmn : m ≤ m
x✝ : ι
| x✝ ∈ Set.Icc m m ∧ u x✝ ω ∈ s → sInf (Set.Icc m m ∩ {i | u i ω ∈ s}) = m

Tactic:
;

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
ω : Ω
m : ι
hmn : m ≤ m
x✝ : ι
| x✝ ∈ Set.Icc m m ∧ u x✝ ω ∈ s → sInf (Set.Icc m m ∩ {i | u i ω ∈ s}) = m
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
ω : Ω
⊢ ω ∈ {ω | τ ω < ↑i} ↔ ω ∈ {ω | τ ω ≤ ↑i} \ {ω | τ ω = ↑i}

Tactic:
;

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
ω : Ω
⊢ ω ∈ {ω | τ ω < ↑i} ↔ ω ∈ {ω | τ ω ≤ ↑i} \ {ω | τ ω = ↑i}
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
ι : Type u_4
inst✝ : LinearOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
ω : Ω
⊢ ω ∈ {ω | ↑i ≤ τ ω} ↔ ω ∈ {ω | τ ω < ↑i}ᶜ

Tactic:
;

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
ι : Type u_4
inst✝ : LinearOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
ω : Ω
⊢ ω ∈ {ω | ↑i ≤ τ ω} ↔ ω ∈ {ω | τ ω < ↑i}ᶜ
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
ω : Ω
⊢ ω ∈ {ω | ↑i < τ ω} ↔ ω ∈ {ω | τ ω ≤ ↑i}ᶜ

Tactic:
;

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
ω : Ω
⊢ ω ∈ {ω | ↑i < τ ω} ↔ ω ∈ {ω | τ ω ≤ ↑i}ᶜ
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : IsMin i
this : {ω | τ ω < ↑i} = ∅
⊢ MeasurableSet ∅

Tactic:
;

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : IsMin i
this : {ω | τ ω < ↑i} = ∅
⊢ MeasurableSet ∅
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case pos.coe
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : IsMin i
ω : Ω
t : ι
⊢ ¬t < i

Tactic:
;

Goal state after:
case pos.coe
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : IsMin i
ω : Ω
t : ι
⊢ ¬t < i
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : upperCrossingTime a b f N (n + 1) ω ≠ N
⊢ lowerCrossingTime a b f N n ω < upperCrossingTime a b f N (n + 1) ω

Tactic:
refine lt_of_le_of_ne lowerCrossingTime_le_upperCrossingTime_succ fun h =>
    not_le.2 hab <| le_trans (stoppedValue_upperCrossingTime hn) ?_

Goal state after:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : upperCrossingTime a b f N (n + 1) ω ≠ N
h : lowerCrossingTime a b f N n ω = upperCrossingTime a b f N (n + 1) ω
⊢ stoppedValue f (fun ω ↦ ↑(upperCrossingTime a b f N (n + 1) ω)) ω ≤ a
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : ¬IsMin i
seq : ℕ → ι
h_tendsto : Tendsto seq atTop (𝓝 i)
h_bound : ∀ (j : ℕ), seq j < i
h_Iio_eq_Union : Set.Iio ↑i = ⋃ j, {k | k ≤ ↑(seq j)}
ω : Ω
⊢ ω ∈ {ω | τ ω < ↑i} ↔ ω ∈ τ ⁻¹' Set.Iio ↑i

Tactic:
;

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : ¬IsMin i
seq : ℕ → ι
h_tendsto : Tendsto seq atTop (𝓝 i)
h_bound : ∀ (j : ℕ), seq j < i
h_Iio_eq_Union : Set.Iio ↑i = ⋃ j, {k | k ≤ ↑(seq j)}
ω : Ω
⊢ ω ∈ {ω | τ ω < ↑i} ↔ ω ∈ τ ⁻¹' Set.Iio ↑i
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : ¬IsMin i
seq : ℕ → ι
h_tendsto : Tendsto seq atTop (𝓝 i)
h_bound : ∀ (j : ℕ), seq j < i
h_Iio_eq_Union : Set.Iio ↑i = ⋃ j, {k | k ≤ ↑(seq j)}
ω : Ω
⊢ τ ω < ↑i ↔ τ ω < ↑i

Tactic:
;

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : ¬IsMin i
seq : ℕ → ι
h_tendsto : Tendsto seq atTop (𝓝 i)
h_bound : ∀ (j : ℕ), seq j < i
h_Iio_eq_Union : Set.Iio ↑i = ⋃ j, {k | k ≤ ↑(seq j)}
ω : Ω
⊢ τ ω < ↑i ↔ τ ω < ↑i
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted ℱ f
n : ℕ
⊢ StronglyMeasurable fun ω ↦
    ∑ k ∈ Finset.range N,
      ({n | lowerCrossingTime a b f N k ω ≤ n} ∩ {n | n < upperCrossingTime a b f N (k + 1) ω}).indicator 1 n

Tactic:
refine Finset.stronglyMeasurable_fun_sum _ fun i _ =>
    stronglyMeasurable_const.indicator ?_

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted ℱ f
n i : ℕ
x✝ : i ∈ Finset.range N
⊢ MeasurableSet fun ω ↦ ({n | lowerCrossingTime a b f N i ω ≤ n} ∩ {n | n < upperCrossingTime a b f N (i + 1) ω}) n
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m i : ι
hi : i ≤ m
h' : sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) < i
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
hni : n < i
h_le : n ≤ hittingBtwn u s n m ω
⊢ ∀ (x : ι), n ≤ x → x ≤ m → u x ω ∈ s → n ≤ x

Tactic:
;

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m i : ι
hi : i ≤ m
h' : sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) < i
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
hni : n < i
h_le : n ≤ hittingBtwn u s n m ω
⊢ ∀ (x : ι), n ≤ x → x ≤ m → u x ω ∈ s → n ≤ x
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
ω : Ω
⊢ ω ∈ {ω | ↑i ≤ τ ω} ↔ ω ∈ {ω | τ ω < ↑i}ᶜ

Tactic:
;

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
ω : Ω
⊢ ω ∈ {ω | ↑i ≤ τ ω} ↔ ω ∈ {ω | τ ω < ↑i}ᶜ
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
ω : Ω
⊢ ω ∈ {ω | τ ω = ↑i} ↔ ω ∈ {ω | τ ω ≤ ↑i} ∩ {ω | τ ω ≥ ↑i}

Tactic:
;

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
ω : Ω
⊢ ω ∈ {ω | τ ω = ↑i} ↔ ω ∈ {ω | τ ω ≤ ↑i} ∩ {ω | τ ω ≥ ↑i}
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
h₁ : 0 ≤ ∫ (x : Ω), (∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ
x✝ : Ω
⊢ ∑ x ∈ Finset.range n, upcrossingStrat a b f N x x✝ * (f (x + 1) x✝ - f x x✝) =
    (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x✝

Tactic:
;

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
h₁ : 0 ≤ ∫ (x : Ω), (∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ
x✝ : Ω
⊢ ∑ x ∈ Finset.range n, upcrossingStrat a b f N x x✝ * (f (x + 1) x✝ - f x x✝) =
    (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x✝
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
h_top : hittingAfter u s n ω ≠ ⊤
h_exists : ∃ j, n ≤ j ∧ u j ω ∈ s
h_le : ↑n ≤ hittingAfter u s n ω
h' : sInf {i | n ≤ i ∧ u i ω ∈ s} < i
⊢ ∀ (x : ι), n ≤ x → u x ω ∈ s → n ≤ x

Tactic:
;

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
h_top : hittingAfter u s n ω ≠ ⊤
h_exists : ∃ j, n ≤ j ∧ u j ω ∈ s
h_le : ↑n ≤ hittingAfter u s n ω
h' : sInf {i | n ≤ i ∧ u i ω ∈ s} < i
⊢ ∀ (x : ι), n ≤ x → u x ω ∈ s → n ≤ x
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case coe
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
inst✝ : Countable ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : ∀ (i : ι), MeasurableSet {ω | τ ω = ↑i}
i : ι
ω : Ω
a : ι
⊢ a ≤ i ↔ ∃ i_1 ≤ i, a = i_1

Tactic:
;

Goal state after:
case coe
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
inst✝ : Countable ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : ∀ (i : ι), MeasurableSet {ω | τ ω = ↑i}
i : ι
ω : Ω
a : ι
⊢ a ≤ i ↔ ∃ i_1 ≤ i, a = i_1
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: case ht
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m₁ m₂ : ι
h : m₁ ≤ m₂
j : ι
hj₁ : j ∈ Set.Icc n m₁
hj₂ : u j ω ∈ s
⊢ BddBelow (Set.Icc n m₂ ∩ {i | u i ω ∈ s})

pp: case hs
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m₁ m₂ : ι
h : m₁ ≤ m₂
j : ι
hj₁ : j ∈ Set.Icc n m₁
hj₂ : u j ω ∈ s
⊢ (Set.Icc n m₁ ∩ {i | u i ω ∈ s}).Nonempty

Tactic:
;

Goal state after:
case ht
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m₁ m₂ : ι
h : m₁ ≤ m₂
j : ι
hj₁ : j ∈ Set.Icc n m₁
hj₂ : u j ω ∈ s
⊢ BddBelow (Set.Icc n m₂ ∩ {i | u i ω ∈ s})

case hs
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m₁ m₂ : ι
h : m₁ ≤ m₂
j : ι
hj₁ : j ∈ Set.Icc n m₁
hj₂ : u j ω ∈ s
⊢ (Set.Icc n m₁ ∩ {i | u i ω ∈ s}).Nonempty
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
⊢ upcrossingsBefore a b f 0 ω = 0 ω

Tactic:
;

Goal state after:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
⊢ upcrossingsBefore a b f 0 ω = 0 ω
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : ConditionallyCompleteLinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet {ω | τ ω < ↑i}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet {ω | τ ω = ↑i}
t : ι
ht : 𝓝[>] t = ⊥
x✝ : Ω
⊢ x✝ ∈ {ω | τ ω ≤ ↑t} ↔ x✝ ∈ {ω | τ ω < ↑t} ∪ {ω | τ ω = ↑t}

Tactic:
;

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : ConditionallyCompleteLinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet {ω | τ ω < ↑i}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet {ω | τ ω = ↑i}
t : ι
ht : 𝓝[>] t = ⊥
x✝ : Ω
⊢ x✝ ∈ {ω | τ ω ≤ ↑t} ↔ x✝ ∈ {ω | τ ω < ↑t} ∪ {ω | τ ω = ↑t}
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n m : ι
E F : Set β
hEF : E ⊆ F
ω : Ω
hF : ∃ j ∈ Set.Icc n m, u j ω ∈ F
hE : ∃ j ∈ Set.Icc n m, u j ω ∈ E
⊢ ∀ (x : ι), n ≤ x → x ≤ m → u x ω ∈ F → n ≤ x

Tactic:
;

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n m : ι
E F : Set β
hEF : E ⊆ F
ω : Ω
hF : ∃ j ∈ Set.Icc n m, u j ω ∈ F
hE : ∃ j ∈ Set.Icc n m, u j ω ∈ E
⊢ ∀ (x : ι), n ≤ x → x ≤ m → u x ω ∈ F → n ≤ x
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n m : ι
E F : Set β
hEF : E ⊆ F
ω : Ω
hE : ¬∃ j ∈ Set.Icc n m, u j ω ∈ E
t : ι
ht : t ∈ Set.Icc n m ∧ u t ω ∈ F
⊢ ∀ (x : ι), n ≤ x → x ≤ m → u x ω ∈ F → n ≤ x

Tactic:
;

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n m : ι
E F : Set β
hEF : E ⊆ F
ω : Ω
hE : ¬∃ j ∈ Set.Icc n m, u j ω ∈ E
t : ι
ht : t ∈ Set.Icc n m ∧ u t ω ∈ F
⊢ ∀ (x : ι), n ≤ x → x ≤ m → u x ω ∈ F → n ≤ x
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n : ι
E F : Set β
hEF : E ⊆ F
ω : Ω
hF : ∃ j, n ≤ j ∧ u j ω ∈ F
hE : ∃ j, n ≤ j ∧ u j ω ∈ E
⊢ ∀ x ∈ {j | n ≤ j ∧ u j ω ∈ F}, n ≤ x

Tactic:
;

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n : ι
E F : Set β
hEF : E ⊆ F
ω : Ω
hF : ∃ j, n ≤ j ∧ u j ω ∈ F
hE : ∃ j, n ≤ j ∧ u j ω ∈ E
⊢ ∀ x ∈ {j | n ≤ j ∧ u j ω ∈ F}, n ≤ x
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : ConditionallyCompleteLinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet {ω | τ ω < ↑i}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet {ω | τ ω = ↑i}
t : ι
ht : ¬𝓝[>] t = ⊥
this✝ : (𝓝[>] t).NeBot
h_freq : ∃ᶠ (x : ι) in 𝓝[>] t, t < x
this : ∃ ns, Tendsto ns atTop (𝓝[>] t) ∧ ∀ (n : ℕ), t < ns n
⊢ ∃ s, (∀ (n : ℕ), t < s n) ∧ Tendsto s atTop (𝓝 t)

Tactic:
tendsto_nhdsWithin_iff

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : ConditionallyCompleteLinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet {ω | τ ω < ↑i}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet {ω | τ ω = ↑i}
t : ι
ht : ¬𝓝[>] t = ⊥
this✝ : (𝓝[>] t).NeBot
h_freq : ∃ᶠ (x : ι) in 𝓝[>] t, t < x
this : ∃ ns, (Tendsto ns atTop (𝓝 t) ∧ ∀ᶠ (n : ℕ) in atTop, ns n ∈ Set.Ioi t) ∧ ∀ (n : ℕ), t < ns n
⊢ ∃ s, (∀ (n : ℕ), t < s n) ∧ Tendsto s atTop (𝓝 t)
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
m n n' : ι
hnn' : n ≤ n'
ω : Ω
h_n : ∃ j ∈ Set.Icc n m, u j ω ∈ s
h_n' : ∃ j ∈ Set.Icc n' m, u j ω ∈ s
⊢ ∀ (x : ι), n ≤ x → x ≤ m → u x ω ∈ s → n ≤ x

Tactic:
;

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
m n n' : ι
hnn' : n ≤ n'
ω : Ω
h_n : ∃ j ∈ Set.Icc n m, u j ω ∈ s
h_n' : ∃ j ∈ Set.Icc n' m, u j ω ∈ s
⊢ ∀ (x : ι), n ≤ x → x ≤ m → u x ω ∈ s → n ≤ x
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
m n n' : ι
hnn' : n ≤ n'
ω : Ω
h_n : ∃ j ∈ Set.Icc n m, u j ω ∈ s
h_n' : ∃ j ∈ Set.Icc n' m, u j ω ∈ s
⊢ sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) ≤ sInf (Set.Icc n' m ∩ {i | u i ω ∈ s})

Tactic:
gcongr
    exacts [⟨n, by simp [mem_lowerBounds]; grind⟩]

Goal state after: