mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case pos
Ω : 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 = ⊥
⊢ MeasurableSet {ω | τ ω ≤ ↑t}

pp: case neg
Ω : 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 = ⊥
⊢ MeasurableSet {ω | τ ω ≤ ↑t}

Tactic:
·

Goal state after:
case pos
Ω : 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 = ⊥
⊢ MeasurableSet {ω | τ ω ≤ ↑t}
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case zero
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : ∃ j ∈ Set.Ico (upperCrossingTime a b f N 0 ω) N, f j ω ∈ Set.Iic a
h' : upperCrossingTime a b f N 0 ω < N
⊢ ∃ j ∈ Set.Icc 0 N, f j ω ∈ Set.Iic a

pp: case zero.hi
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : hittingBtwn f (Set.Iic a) (upperCrossingTime a b f N 0 ω) N ω < N
h' : upperCrossingTime a b f N 0 ω < N
⊢ N ≤ N

Tactic:
·

Goal state after:
case zero
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : ∃ j ∈ Set.Ico (upperCrossingTime a b f N 0 ω) N, f j ω ∈ Set.Iic a
h' : upperCrossingTime a b f N 0 ω < N
⊢ ∃ j ∈ Set.Icc 0 N, f j ω ∈ Set.Iic a
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: case pos
Ω : 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
⊢ sInf (Set.Icc n m ∩ {i | u i ω ∈ F}) ≤ sInf (Set.Icc n m ∩ {i | u i ω ∈ E})

pp: case neg
Ω : 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
⊢ sInf (Set.Icc n m ∩ {i | u i ω ∈ F}) ≤ m

pp: case pos
Ω : 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
⊢ m ≤ sInf (Set.Icc n m ∩ {i | u i ω ∈ E})

pp: case neg
Ω : 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
⊢ m ≤ m

Tactic:
·

Goal state after:
case pos
Ω : 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
⊢ sInf (Set.Icc n m ∩ {i | u i ω ∈ F}) ≤ sInf (Set.Icc n m ∩ {i | u i ω ∈ E})
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case zero.hi
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : hittingBtwn f (Set.Iic a) (upperCrossingTime a b f N 0 ω) N ω < N
h' : upperCrossingTime a b f N 0 ω < N
⊢ N ≤ N

Tactic:
·

Goal state after:
case zero.hi
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : hittingBtwn f (Set.Iic a) (upperCrossingTime a b f N 0 ω) N ω < N
h' : upperCrossingTime a b f N 0 ω < N
⊢ N ≤ N
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: case neg
Ω : 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
⊢ sInf (Set.Icc n m ∩ {i | u i ω ∈ F}) ≤ m

pp: case pos
Ω : 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
⊢ m ≤ sInf (Set.Icc n m ∩ {i | u i ω ∈ E})

pp: case neg
Ω : 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
⊢ m ≤ m

Tactic:
·

Goal state after:
case neg
Ω : 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
⊢ sInf (Set.Icc n m ∩ {i | u i ω ∈ F}) ≤ m
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
k : ℕ
ih :
  upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
    lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω
h : lowerCrossingTime a b f N (k + 1) ω < N
h' : ∃ j ∈ Set.Ico (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b
⊢ upperCrossingTime a b f M k.succ ω = upperCrossingTime a b f N k.succ ω

pp: case hi
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
k : ℕ
ih :
  upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
    lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω
h : lowerCrossingTime a b f N (k + 1) ω < N
h' : hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f N k ω) N ω < N
⊢ N ≤ N

Tactic:
·

Goal state after:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
k : ℕ
ih :
  upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
    lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω
h : lowerCrossingTime a b f N (k + 1) ω < N
h' : ∃ j ∈ Set.Ico (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b
⊢ upperCrossingTime a b f M k.succ ω = upperCrossingTime a b f N k.succ ω
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: case pos
Ω : 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
⊢ m ≤ sInf (Set.Icc n m ∩ {i | u i ω ∈ E})

pp: case neg
Ω : 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
⊢ m ≤ m

Tactic:
·

Goal state after:
case pos
Ω : 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
⊢ m ≤ sInf (Set.Icc n m ∩ {i | u i ω ∈ E})
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: case neg
Ω : 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
⊢ m ≤ m

Tactic:
·

Goal state after:
case neg
Ω : 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
⊢ m ≤ m
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case hi
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
k : ℕ
ih :
  upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
    lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω
h : lowerCrossingTime a b f N (k + 1) ω < N
h' : hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f N k ω) N ω < N
⊢ N ≤ N

Tactic:
·

Goal state after:
case hi
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
k : ℕ
ih :
  upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
    lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω
h : lowerCrossingTime a b f N (k + 1) ω < N
h' : hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f N k ω) N ω < N
⊢ N ≤ N
Module: Mathlib.Probability.Martingale.Basic

Goal state before:
pp: case ha
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst✝⁵ : CompleteSpace E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedModule ℝ E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsFiniteMeasure μ
R : ℝ
f : ℕ → Ω → E
ξ : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
C : ℕ → ℝ
hC : ∀ (i : ℕ) (ω : Ω), ‖ξ i ω‖ ≤ C i
hint : ∀ (m : ℕ), Integrable (∑ k ∈ Finset.range m, ξ k • (f (k + 1) - f k)) μ
hadp : StronglyAdapted 𝒢 fun n ↦ ∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k)
i : ℕ
ω : Ω
hω1 : 0 ≤ μ[f (i + 1) - f i | ↑𝒢 i] ω
hω2 : μ[ξ i • (f (i + 1) - f i) | ↑𝒢 i] ω = ξ i ω • μ[f (i + 1) - f i | ↑𝒢 i] ω
⊢ 0 ≤ ξ i ω

pp: case hb
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst✝⁵ : CompleteSpace E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedModule ℝ E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsFiniteMeasure μ
R : ℝ
f : ℕ → Ω → E
ξ : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
C : ℕ → ℝ
hC : ∀ (i : ℕ) (ω : Ω), ‖ξ i ω‖ ≤ C i
hint : ∀ (m : ℕ), Integrable (∑ k ∈ Finset.range m, ξ k • (f (k + 1) - f k)) μ
hadp : StronglyAdapted 𝒢 fun n ↦ ∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k)
i : ℕ
ω : Ω
hω1 : 0 ≤ μ[f (i + 1) - f i | ↑𝒢 i] ω
hω2 : μ[ξ i • (f (i + 1) - f i) | ↑𝒢 i] ω = ξ i ω • μ[f (i + 1) - f i | ↑𝒢 i] ω
⊢ 0 ≤ 0

Tactic:
·

Goal state after:
case ha
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst✝⁵ : CompleteSpace E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedModule ℝ E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsFiniteMeasure μ
R : ℝ
f : ℕ → Ω → E
ξ : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
C : ℕ → ℝ
hC : ∀ (i : ℕ) (ω : Ω), ‖ξ i ω‖ ≤ C i
hint : ∀ (m : ℕ), Integrable (∑ k ∈ Finset.range m, ξ k • (f (k + 1) - f k)) μ
hadp : StronglyAdapted 𝒢 fun n ↦ ∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k)
i : ℕ
ω : Ω
hω1 : 0 ≤ μ[f (i + 1) - f i | ↑𝒢 i] ω
hω2 : μ[ξ i • (f (i + 1) - f i) | ↑𝒢 i] ω = ξ i ω • μ[f (i + 1) - f i | ↑𝒢 i] ω
⊢ 0 ≤ ξ i ω
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: case pos
Ω : 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
⊢ ↑(sInf {j | n ≤ j ∧ u j ω ∈ F}) ≤ ↑(sInf {j | n ≤ j ∧ u j ω ∈ E})

pp: case neg
Ω : 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
⊢ ↑(sInf {j | n ≤ j ∧ u j ω ∈ F}) ≤ ⊤

pp: case pos
Ω : 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
⊢ ⊤ ≤ ↑(sInf {j | n ≤ j ∧ u j ω ∈ E})

pp: case neg
Ω : 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
⊢ ⊤ ≤ ⊤

Tactic:
·

Goal state after:
case pos
Ω : 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
⊢ ↑(sInf {j | n ≤ j ∧ u j ω ∈ F}) ≤ ↑(sInf {j | n ≤ j ∧ u j ω ∈ E})
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: case neg
Ω : 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
⊢ ↑(sInf {j | n ≤ j ∧ u j ω ∈ F}) ≤ ⊤

pp: case pos
Ω : 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
⊢ ⊤ ≤ ↑(sInf {j | n ≤ j ∧ u j ω ∈ E})

pp: case neg
Ω : 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
⊢ ⊤ ≤ ⊤

Tactic:
·

Goal state after:
case neg
Ω : 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
⊢ ↑(sInf {j | n ≤ j ∧ u j ω ∈ F}) ≤ ⊤
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: case pos
Ω : 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
⊢ ⊤ ≤ ↑(sInf {j | n ≤ j ∧ u j ω ∈ E})

pp: case neg
Ω : 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
⊢ ⊤ ≤ ⊤

Tactic:
·

Goal state after:
case pos
Ω : 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
⊢ ⊤ ≤ ↑(sInf {j | n ≤ j ∧ u j ω ∈ E})
Module: Mathlib.Probability.Martingale.Basic

Goal state before:
pp: case hb
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst✝⁵ : CompleteSpace E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedModule ℝ E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsFiniteMeasure μ
R : ℝ
f : ℕ → Ω → E
ξ : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
C : ℕ → ℝ
hC : ∀ (i : ℕ) (ω : Ω), ‖ξ i ω‖ ≤ C i
hint : ∀ (m : ℕ), Integrable (∑ k ∈ Finset.range m, ξ k • (f (k + 1) - f k)) μ
hadp : StronglyAdapted 𝒢 fun n ↦ ∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k)
i : ℕ
ω : Ω
hω1 : 0 ≤ μ[f (i + 1) - f i | ↑𝒢 i] ω
hω2 : μ[ξ i • (f (i + 1) - f i) | ↑𝒢 i] ω = ξ i ω • μ[f (i + 1) - f i | ↑𝒢 i] ω
⊢ 0 ≤ 0

Tactic:
·

Goal state after:
case hb
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst✝⁵ : CompleteSpace E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedModule ℝ E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsFiniteMeasure μ
R : ℝ
f : ℕ → Ω → E
ξ : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
C : ℕ → ℝ
hC : ∀ (i : ℕ) (ω : Ω), ‖ξ i ω‖ ≤ C i
hint : ∀ (m : ℕ), Integrable (∑ k ∈ Finset.range m, ξ k • (f (k + 1) - f k)) μ
hadp : StronglyAdapted 𝒢 fun n ↦ ∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k)
i : ℕ
ω : Ω
hω1 : 0 ≤ μ[f (i + 1) - f i | ↑𝒢 i] ω
hω2 : μ[ξ i • (f (i + 1) - f i) | ↑𝒢 i] ω = ξ i ω • μ[f (i + 1) - f i | ↑𝒢 i] ω
⊢ 0 ≤ 0
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: case neg
Ω : 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
⊢ ⊤ ≤ ⊤

Tactic:
·

Goal state after:
case neg
Ω : 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
⊢ ⊤ ≤ ⊤
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 β
n m₁ m₂ : ι
hm : m₁ ≤ m₂
h : ∃ j ∈ Set.Icc n m₁, u j ω ∈ s
⊢ (fun x ↦ hittingBtwn u s n x ω) m₁ ≤ (fun x ↦ hittingBtwn u s n x ω) m₂

pp: case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
ω : Ω
u : ι → Ω → β
s : Set β
n m₁ m₂ : ι
hm : m₁ ≤ m₂
h : ¬∃ j ∈ Set.Icc n m₁, u j ω ∈ s
⊢ (fun x ↦ hittingBtwn u s n x ω) m₁ ≤ (fun x ↦ hittingBtwn u s n x ω) m₂

Tactic:
·

Goal state after:
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
ω : Ω
u : ι → Ω → β
s : Set β
n m₁ m₂ : ι
hm : m₁ ≤ m₂
h : ∃ j ∈ Set.Icc n m₁, u j ω ∈ s
⊢ (fun x ↦ hittingBtwn u s n x ω) m₁ ≤ (fun x ↦ hittingBtwn u s n x ω) m₂
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : ∃ j ∈ Set.Ico (lowerCrossingTime a b f N n ω) N, f j ω ∈ Set.Ici b
this : lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
⊢ ∃ j ∈ Set.Icc (lowerCrossingTime a b f N n ω) N, f j ω ∈ Set.Ici b

pp: case hi
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f N n ω) N ω < N
this : lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
⊢ N ≤ N

Tactic:
·

Goal state after:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : ∃ j ∈ Set.Ico (lowerCrossingTime a b f N n ω) N, f j ω ∈ Set.Ici b
this : lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
⊢ ∃ j ∈ Set.Icc (lowerCrossingTime a b f N n ω) N, f j ω ∈ Set.Ici b
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
ω : Ω
u : ι → Ω → β
s : Set β
n m₁ m₂ : ι
hm : m₁ ≤ m₂
h : ¬∃ j ∈ Set.Icc n m₁, u j ω ∈ s
⊢ (fun x ↦ hittingBtwn u s n x ω) m₁ ≤ (fun x ↦ hittingBtwn u s n x ω) m₂

Tactic:
·

Goal state after:
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
ω : Ω
u : ι → Ω → β
s : Set β
n m₁ m₂ : ι
hm : m₁ ≤ m₂
h : ¬∃ j ∈ Set.Icc n m₁, u j ω ∈ s
⊢ (fun x ↦ hittingBtwn u s n x ω) m₁ ≤ (fun x ↦ hittingBtwn u s n x ω) m₂
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case hi
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f N n ω) N ω < N
this : lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
⊢ N ≤ N

Tactic:
·

Goal state after:
case hi
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f N n ω) N ω < N
this : lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
⊢ N ≤ N
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case zero
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : upperCrossingTime a b f N 0 ω < N
⊢ upperCrossingTime a b f M 0 ω = upperCrossingTime a b f N 0 ω

pp: case succ
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
n✝ : ℕ
h : upperCrossingTime a b f N (n✝ + 1) ω < N
⊢ upperCrossingTime a b f M (n✝ + 1) ω = upperCrossingTime a b f N (n✝ + 1) ω

Tactic:
·

Goal state after:
case zero
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : upperCrossingTime a b f N 0 ω < N
⊢ upperCrossingTime a b f M 0 ω = upperCrossingTime a b f N 0 ω
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 β
n m₁ m₂ : ι
hm : m₁ ≤ m₂
h : ¬∃ j ∈ Set.Icc n m₁, u j ω ∈ s
h' : ∃ j ∈ Set.Icc n m₂, u j ω ∈ s
⊢ m₁ ≤ sInf (Set.Icc n m₂ ∩ {i | u i ω ∈ s})

pp: case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
ω : Ω
u : ι → Ω → β
s : Set β
n m₁ m₂ : ι
hm : m₁ ≤ m₂
h : ¬∃ j ∈ Set.Icc n m₁, u j ω ∈ s
h' : ¬∃ j ∈ Set.Icc n m₂, u j ω ∈ s
⊢ m₁ ≤ m₂

Tactic:
·

Goal state after:
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
ω : Ω
u : ι → Ω → β
s : Set β
n m₁ m₂ : ι
hm : m₁ ≤ m₂
h : ¬∃ j ∈ Set.Icc n m₁, u j ω ∈ s
h' : ∃ j ∈ Set.Icc n m₂, u j ω ∈ s
⊢ m₁ ≤ sInf (Set.Icc n m₂ ∩ {i | u i ω ∈ s})
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case succ
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
n✝ : ℕ
h : upperCrossingTime a b f N (n✝ + 1) ω < N
⊢ upperCrossingTime a b f M (n✝ + 1) ω = upperCrossingTime a b f N (n✝ + 1) ω

Tactic:
·

Goal state after:
case succ
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
n✝ : ℕ
h : upperCrossingTime a b f N (n✝ + 1) ω < N
⊢ upperCrossingTime a b f M (n✝ + 1) ω = upperCrossingTime a b f N (n✝ + 1) ω
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
ω : Ω
u : ι → Ω → β
s : Set β
n m₁ m₂ : ι
hm : m₁ ≤ m₂
h : ¬∃ j ∈ Set.Icc n m₁, u j ω ∈ s
h' : ¬∃ j ∈ Set.Icc n m₂, u j ω ∈ s
⊢ m₁ ≤ m₂

Tactic:
·

Goal state after:
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
ω : Ω
u : ι → Ω → β
s : Set β
n m₁ m₂ : ι
hm : m₁ ≤ m₂
h : ¬∃ j ∈ Set.Icc n m₁, u j ω ∈ s
h' : ¬∃ j ∈ Set.Icc n m₂, u j ω ∈ s
⊢ m₁ ≤ m₂
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case h₁
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
hab : a < b
N M : ℕ
hNM : N ≤ M
ω : Ω
⊢ BddAbove {n | upperCrossingTime a b f M n ω < M}

pp: case a
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
hab : a < b
N M : ℕ
hNM : N ≤ M
ω : Ω
n : ℕ
⊢ upperCrossingTime a b f N n ω < N → upperCrossingTime a b f M n ω < M

Tactic:
·

Goal state after:
case h₁
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
hab : a < b
N M : ℕ
hNM : N ≤ M
ω : Ω
⊢ BddAbove {n | upperCrossingTime a b f M n ω < M}
Module: Mathlib.Probability.Martingale.Convergence

Goal state before:
pp: case pos
Ω : Type u_1
f : ℕ → Ω → ℝ
ω : Ω
hf₁ : liminf (fun n ↦ ↑‖f n ω‖₊) atTop < ∞
hf₂ : ∀ (a b : ℚ), a < b → upcrossings (↑a) (↑b) f ω < ∞
h : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun n ↦ |f n ω|
⊢ ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)

pp: case neg
Ω : Type u_1
f : ℕ → Ω → ℝ
ω : Ω
hf₁ : liminf (fun n ↦ ↑‖f n ω‖₊) atTop < ∞
hf₂ : ∀ (a b : ℚ), a < b → upcrossings (↑a) (↑b) f ω < ∞
h : ¬IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun n ↦ |f n ω|
⊢ ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)

Tactic:
·

Goal state after:
case pos
Ω : Type u_1
f : ℕ → Ω → ℝ
ω : Ω
hf₁ : liminf (fun n ↦ ↑‖f n ω‖₊) atTop < ∞
hf₂ : ∀ (a b : ℚ), a < b → upcrossings (↑a) (↑b) f ω < ∞
h : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun n ↦ |f n ω|
⊢ ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)