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

Goal state before:
pp: case neg
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
ω : Ω
h₁ : ∃ j ∈ Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k ω) N, (f j ω - a)⁺ ∈ Set.Ici (b - a)
h₂ : ¬∃ j ∈ Set.Icc (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b
⊢ sInf (Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k ω) N ∩ {i | b ≤ (f i ω - a)⁺ + a}) = N

pp: case pos
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
ω : Ω
h₁ : ¬∃ j ∈ Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k ω) N, (f j ω - a)⁺ ∈ Set.Ici (b - a)
h₂ : ∃ j ∈ Set.Icc (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b
⊢ N = sInf (Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k ω) N ∩ {i | b ≤ f i ω})

pp: case neg
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
ω : Ω
h₁ : ¬∃ j ∈ Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k ω) N, (f j ω - a)⁺ ∈ Set.Ici (b - a)
h₂ : ¬∃ j ∈ Set.Icc (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b
⊢ N = N

Tactic:
·

Goal state after:
case neg
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
ω : Ω
h₁ : ∃ j ∈ Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k ω) N, (f j ω - a)⁺ ∈ Set.Ici (b - a)
h₂ : ¬∃ j ∈ Set.Icc (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b
⊢ sInf (Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k ω) N ∩ {i | b ≤ (f i ω - a)⁺ + a}) = N
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case pos
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
this : ∀ (j : WithTop ι), {ω | τ ω = ↑i} ∩ {ω | τ ω ≤ j} = {ω | τ ω = ↑i} ∩ {_ω | ↑i ≤ j}
h : MeasurableSet (s ∩ {ω | τ ω = ↑i})
j : ι
hij : i ≤ j
⊢ MeasurableSet (s ∩ ({ω | τ ω = ↑i} ∩ {_ω | ↑i ≤ ↑j}))

pp: case neg
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
this : ∀ (j : WithTop ι), {ω | τ ω = ↑i} ∩ {ω | τ ω ≤ j} = {ω | τ ω = ↑i} ∩ {_ω | ↑i ≤ j}
h : MeasurableSet (s ∩ {ω | τ ω = ↑i})
j : ι
hij : ¬i ≤ j
⊢ MeasurableSet (s ∩ ({ω | τ ω = ↑i} ∩ {_ω | ↑i ≤ ↑j}))

Tactic:
·

Goal state after:
case pos
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
this : ∀ (j : WithTop ι), {ω | τ ω = ↑i} ∩ {ω | τ ω ≤ j} = {ω | τ ω = ↑i} ∩ {_ω | ↑i ≤ j}
h : MeasurableSet (s ∩ {ω | τ ω = ↑i})
j : ι
hij : i ≤ j
⊢ MeasurableSet (s ∩ ({ω | τ ω = ↑i} ∩ {_ω | ↑i ≤ ↑j}))
Module: Mathlib.Probability.Martingale.OptionalStopping

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : SigmaFiniteFiltration μ 𝒢
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf :
  ∀ (τ π : Ω → ℕ∞),
    IsStoppingTime 𝒢 τ →
      IsStoppingTime 𝒢 π →
        τ ≤ π → (∃ N, ∀ (ω : Ω), π ω ≤ ↑N) → ∫ (x : Ω), stoppedValue f τ x ∂μ ≤ ∫ (x : Ω), stoppedValue f π x ∂μ
i j : ℕ
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
⊢ (s.piecewise (fun x ↦ ↑i) fun x ↦ ↑j) ≤ fun x ↦ ↑j

pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : SigmaFiniteFiltration μ 𝒢
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
i j : ℕ
hij : i ≤ j
s : Set Ω
hf : ∫ (x : Ω), stoppedValue f (s.piecewise (fun x ↦ ↑i) fun x ↦ ↑j) x ∂μ ≤ ∫ (x : Ω), stoppedValue f (fun x ↦ ↑j) x ∂μ
hs : MeasurableSet s
⊢ ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f j ω ∂μ

Tactic:
·

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : SigmaFiniteFiltration μ 𝒢
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf :
  ∀ (τ π : Ω → ℕ∞),
    IsStoppingTime 𝒢 τ →
      IsStoppingTime 𝒢 π →
        τ ≤ π → (∃ N, ∀ (ω : Ω), π ω ≤ ↑N) → ∫ (x : Ω), stoppedValue f τ x ∂μ ≤ ∫ (x : Ω), stoppedValue f π x ∂μ
i j : ℕ
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
⊢ (s.piecewise (fun x ↦ ↑i) fun x ↦ ↑j) ≤ fun x ↦ ↑j
Module: Mathlib.Probability.Martingale.OptionalStopping

Goal state before:
pp: case pos
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : SigmaFiniteFiltration μ 𝒢
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf :
  ∀ (τ π : Ω → ℕ∞),
    IsStoppingTime 𝒢 τ →
      IsStoppingTime 𝒢 π →
        τ ≤ π → (∃ N, ∀ (ω : Ω), π ω ≤ ↑N) → ∫ (x : Ω), stoppedValue f τ x ∂μ ≤ ∫ (x : Ω), stoppedValue f π x ∂μ
i j : ℕ
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
ω : Ω
hω : ω ∈ s
⊢ ↑i ≤ ↑j

pp: case neg
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : SigmaFiniteFiltration μ 𝒢
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf :
  ∀ (τ π : Ω → ℕ∞),
    IsStoppingTime 𝒢 τ →
      IsStoppingTime 𝒢 π →
        τ ≤ π → (∃ N, ∀ (ω : Ω), π ω ≤ ↑N) → ∫ (x : Ω), stoppedValue f τ x ∂μ ≤ ∫ (x : Ω), stoppedValue f π x ∂μ
i j : ℕ
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
ω : Ω
hω : ω ∉ s
⊢ ↑j ≤ ↑j

Tactic:
·

Goal state after:
case pos
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : SigmaFiniteFiltration μ 𝒢
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf :
  ∀ (τ π : Ω → ℕ∞),
    IsStoppingTime 𝒢 τ →
      IsStoppingTime 𝒢 π →
        τ ≤ π → (∃ N, ∀ (ω : Ω), π ω ≤ ↑N) → ∫ (x : Ω), stoppedValue f τ x ∂μ ≤ ∫ (x : Ω), stoppedValue f π x ∂μ
i j : ℕ
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
ω : Ω
hω : ω ∈ s
⊢ ↑i ≤ ↑j
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case neg
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
this : ∀ (j : WithTop ι), {ω | τ ω = ↑i} ∩ {ω | τ ω ≤ j} = {ω | τ ω = ↑i} ∩ {_ω | ↑i ≤ j}
h : MeasurableSet (s ∩ {ω | τ ω = ↑i})
j : ι
hij : ¬i ≤ j
⊢ MeasurableSet (s ∩ ({ω | τ ω = ↑i} ∩ {_ω | ↑i ≤ ↑j}))

Tactic:
·

Goal state after:
case neg
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
this : ∀ (j : WithTop ι), {ω | τ ω = ↑i} ∩ {ω | τ ω ≤ j} = {ω | τ ω = ↑i} ∩ {_ω | ↑i ≤ j}
h : MeasurableSet (s ∩ {ω | τ ω = ↑i})
j : ι
hij : ¬i ≤ j
⊢ MeasurableSet (s ∩ ({ω | τ ω = ↑i} ∩ {_ω | ↑i ≤ ↑j}))
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case pos
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
ω : Ω
h₁ : ¬∃ j ∈ Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k ω) N, (f j ω - a)⁺ ∈ Set.Ici (b - a)
h₂ : ∃ j ∈ Set.Icc (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b
⊢ N = sInf (Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k ω) N ∩ {i | b ≤ f i ω})

pp: case neg
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
ω : Ω
h₁ : ¬∃ j ∈ Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k ω) N, (f j ω - a)⁺ ∈ Set.Ici (b - a)
h₂ : ¬∃ j ∈ Set.Icc (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b
⊢ N = N

Tactic:
·

Goal state after:
case pos
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
ω : Ω
h₁ : ¬∃ j ∈ Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k ω) N, (f j ω - a)⁺ ∈ Set.Ici (b - a)
h₂ : ∃ j ∈ Set.Icc (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b
⊢ N = sInf (Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k ω) N ∩ {i | b ≤ f i ω})
Module: Mathlib.Probability.Martingale.OptionalStopping

Goal state before:
pp: case neg
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : SigmaFiniteFiltration μ 𝒢
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf :
  ∀ (τ π : Ω → ℕ∞),
    IsStoppingTime 𝒢 τ →
      IsStoppingTime 𝒢 π →
        τ ≤ π → (∃ N, ∀ (ω : Ω), π ω ≤ ↑N) → ∫ (x : Ω), stoppedValue f τ x ∂μ ≤ ∫ (x : Ω), stoppedValue f π x ∂μ
i j : ℕ
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
ω : Ω
hω : ω ∉ s
⊢ ↑j ≤ ↑j

Tactic:
·

Goal state after:
case neg
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : SigmaFiniteFiltration μ 𝒢
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf :
  ∀ (τ π : Ω → ℕ∞),
    IsStoppingTime 𝒢 τ →
      IsStoppingTime 𝒢 π →
        τ ≤ π → (∃ N, ∀ (ω : Ω), π ω ≤ ↑N) → ∫ (x : Ω), stoppedValue f τ x ∂μ ≤ ∫ (x : Ω), stoppedValue f π x ∂μ
i j : ℕ
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
ω : Ω
hω : ω ∉ s
⊢ ↑j ≤ ↑j
Module: Mathlib.Probability.Martingale.OptionalStopping

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : SigmaFiniteFiltration μ 𝒢
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
i j : ℕ
hij : i ≤ j
s : Set Ω
hf : ∫ (x : Ω), stoppedValue f (s.piecewise (fun x ↦ ↑i) fun x ↦ ↑j) x ∂μ ≤ ∫ (x : Ω), stoppedValue f (fun x ↦ ↑j) x ∂μ
hs : MeasurableSet s
⊢ ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f j ω ∂μ

Tactic:
·

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : SigmaFiniteFiltration μ 𝒢
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
i j : ℕ
hij : i ≤ j
s : Set Ω
hf : ∫ (x : Ω), stoppedValue f (s.piecewise (fun x ↦ ↑i) fun x ↦ ↑j) x ∂μ ≤ ∫ (x : Ω), stoppedValue f (fun x ↦ ↑j) x ∂μ
hs : MeasurableSet s
⊢ ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f j ω ∂μ
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case neg
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
ω : Ω
h₁ : ¬∃ j ∈ Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k ω) N, (f j ω - a)⁺ ∈ Set.Ici (b - a)
h₂ : ¬∃ j ∈ Set.Icc (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b
⊢ N = N

Tactic:
·

Goal state after:
case neg
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
ω : Ω
h₁ : ¬∃ j ∈ Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k ω) N, (f j ω - a)⁺ ∈ Set.Ici (b - a)
h₂ : ¬∃ j ∈ Set.Icc (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b
⊢ N = N
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case refine_1
Ω : Type u_1
β : Type u_2
ι✝ : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst✝² : SemilatticeSup ι
inst✝¹ : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
⊢ MeasurableSpace Ω

pp: case refine_2
Ω : Type u_1
β : Type u_2
ι✝ : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst✝² : SemilatticeSup ι
inst✝¹ : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
⊢ ?refine_1 ≤ hτ.measurableSpace

pp: case refine_3
Ω : Type u_1
β : Type u_2
ι✝ : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst✝² : SemilatticeSup ι
inst✝¹ : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
⊢ SigmaFinite (μ.trim ⋯)

Tactic:
·

Goal state after:
case refine_1
Ω : Type u_1
β : Type u_2
ι✝ : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst✝² : SemilatticeSup ι
inst✝¹ : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
⊢ MeasurableSpace Ω
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case refine_2
Ω : Type u_1
β : Type u_2
ι✝ : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst✝² : SemilatticeSup ι
inst✝¹ : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
⊢ ↑f ⊥ ≤ hτ.measurableSpace

pp: case refine_3
Ω : Type u_1
β : Type u_2
ι✝ : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst✝² : SemilatticeSup ι
inst✝¹ : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
⊢ SigmaFinite (μ.trim ⋯)

Tactic:
·

Goal state after:
case refine_2
Ω : Type u_1
β : Type u_2
ι✝ : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst✝² : SemilatticeSup ι
inst✝¹ : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
⊢ ↑f ⊥ ≤ hτ.measurableSpace
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case refine_3
Ω : Type u_1
β : Type u_2
ι✝ : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst✝² : SemilatticeSup ι
inst✝¹ : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
⊢ SigmaFinite (μ.trim ⋯)

Tactic:
·

Goal state after:
case refine_3
Ω : Type u_1
β : Type u_2
ι✝ : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst✝² : SemilatticeSup ι
inst✝¹ : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
⊢ SigmaFinite (μ.trim ⋯)
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case refine_1
Ω : Type u_1
β : Type u_2
ι✝ : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst✝² : SemilatticeSup ι
inst✝¹ : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ ↑n
⊢ MeasurableSpace Ω

pp: case refine_2
Ω : Type u_1
β : Type u_2
ι✝ : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst✝² : SemilatticeSup ι
inst✝¹ : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ ↑n
⊢ ?refine_1 ≤ hτ.measurableSpace

pp: case refine_3
Ω : Type u_1
β : Type u_2
ι✝ : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst✝² : SemilatticeSup ι
inst✝¹ : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ ↑n
⊢ SigmaFinite (μ.trim ⋯)

Tactic:
·

Goal state after:
case refine_1
Ω : Type u_1
β : Type u_2
ι✝ : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst✝² : SemilatticeSup ι
inst✝¹ : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ ↑n
⊢ MeasurableSpace Ω
Module: Mathlib.Probability.Martingale.OptionalStopping

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ : Ω → ℕ∞
inst✝ : SigmaFiniteFiltration μ 𝒢
h : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
⊢ ∀ (τ_1 π : Ω → ℕ∞),
    IsStoppingTime 𝒢 τ_1 →
      IsStoppingTime 𝒢 π →
        τ_1 ≤ π →
          (∃ N, ∀ (x : Ω), π x ≤ ↑N) →
            ∫ (x : Ω), stoppedValue (stoppedProcess f τ) τ_1 x ∂μ ≤ ∫ (x : Ω), stoppedValue (stoppedProcess f τ) π x ∂μ

pp: case hadp
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ : Ω → ℕ∞
inst✝ : SigmaFiniteFiltration μ 𝒢
h : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
⊢ StronglyAdapted 𝒢 (stoppedProcess f τ)

pp: case hint
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ : Ω → ℕ∞
inst✝ : SigmaFiniteFiltration μ 𝒢
h : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
⊢ ∀ (i : ℕ), Integrable (stoppedProcess f τ i) μ

Tactic:
·

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ : Ω → ℕ∞
inst✝ : SigmaFiniteFiltration μ 𝒢
h : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
⊢ ∀ (τ_1 π : Ω → ℕ∞),
    IsStoppingTime 𝒢 τ_1 →
      IsStoppingTime 𝒢 π →
        τ_1 ≤ π →
          (∃ N, ∀ (x : Ω), π x ≤ ↑N) →
            ∫ (x : Ω), stoppedValue (stoppedProcess f τ) τ_1 x ∂μ ≤ ∫ (x : Ω), stoppedValue (stoppedProcess f τ) π x ∂μ
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case refine_2
Ω : Type u_1
β : Type u_2
ι✝ : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst✝² : SemilatticeSup ι
inst✝¹ : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ ↑n
⊢ ↑f ⊥ ≤ hτ.measurableSpace

pp: case refine_3
Ω : Type u_1
β : Type u_2
ι✝ : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst✝² : SemilatticeSup ι
inst✝¹ : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ ↑n
⊢ SigmaFinite (μ.trim ⋯)

Tactic:
·

Goal state after:
case refine_2
Ω : Type u_1
β : Type u_2
ι✝ : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst✝² : SemilatticeSup ι
inst✝¹ : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ ↑n
⊢ ↑f ⊥ ≤ hτ.measurableSpace
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case refine_3
Ω : Type u_1
β : Type u_2
ι✝ : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst✝² : SemilatticeSup ι
inst✝¹ : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ ↑n
⊢ SigmaFinite (μ.trim ⋯)

Tactic:
·

Goal state after:
case refine_3
Ω : Type u_1
β : Type u_2
ι✝ : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst✝² : SemilatticeSup ι
inst✝¹ : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ ↑n
⊢ SigmaFinite (μ.trim ⋯)
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case neg
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
this : upperCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N (k + 1) = upperCrossingTime a b f N (k + 1)
ω : Ω
h₁ : ∃ j ∈ Set.Icc (upperCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N (k + 1) ω) N, (f j ω - a)⁺ ∈ Set.Iic 0
h₂ : ¬∃ j ∈ Set.Icc (upperCrossingTime a b f N (k + 1) ω) N, f j ω ∈ Set.Iic a
⊢ sInf (Set.Icc (upperCrossingTime a b f N (k + 1) ω) N ∩ {i | (f i ω - a)⁺ ≤ 0}) = N

pp: case pos
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
this : upperCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N (k + 1) = upperCrossingTime a b f N (k + 1)
ω : Ω
h₁ : ¬∃ j ∈ Set.Icc (upperCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N (k + 1) ω) N, (f j ω - a)⁺ ∈ Set.Iic 0
h₂ : ∃ j ∈ Set.Icc (upperCrossingTime a b f N (k + 1) ω) N, f j ω ∈ Set.Iic a
⊢ N = sInf (Set.Icc (upperCrossingTime a b f N (k + 1) ω) N ∩ {i | f i ω ≤ a})

pp: case neg
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
this : upperCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N (k + 1) = upperCrossingTime a b f N (k + 1)
ω : Ω
h₁ : ¬∃ j ∈ Set.Icc (upperCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N (k + 1) ω) N, (f j ω - a)⁺ ∈ Set.Iic 0
h₂ : ¬∃ j ∈ Set.Icc (upperCrossingTime a b f N (k + 1) ω) N, f j ω ∈ Set.Iic a
⊢ N = N

Tactic:
·

Goal state after:
case neg
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
this : upperCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N (k + 1) = upperCrossingTime a b f N (k + 1)
ω : Ω
h₁ : ∃ j ∈ Set.Icc (upperCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N (k + 1) ω) N, (f j ω - a)⁺ ∈ Set.Iic 0
h₂ : ¬∃ j ∈ Set.Icc (upperCrossingTime a b f N (k + 1) ω) N, f j ω ∈ Set.Iic a
⊢ sInf (Set.Icc (upperCrossingTime a b f N (k + 1) ω) N ∩ {i | (f i ω - a)⁺ ≤ 0}) = N
Module: Mathlib.Probability.Martingale.OptionalStopping

Goal state before:
pp: case hadp
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ : Ω → ℕ∞
inst✝ : SigmaFiniteFiltration μ 𝒢
h : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
⊢ StronglyAdapted 𝒢 (stoppedProcess f τ)

pp: case hint
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ : Ω → ℕ∞
inst✝ : SigmaFiniteFiltration μ 𝒢
h : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
⊢ ∀ (i : ℕ), Integrable (stoppedProcess f τ i) μ

Tactic:
·

Goal state after:
case hadp
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ : Ω → ℕ∞
inst✝ : SigmaFiniteFiltration μ 𝒢
h : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
⊢ StronglyAdapted 𝒢 (stoppedProcess f τ)