awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : AddCommMonoid E
n : ι
ω : Ω
h : τ ω < (↑n : WithTop ι)
⊢ τ ω ∈ WithTop.some '' (↑(Finset.Iio n) : Set ι)
have simp : ∃ x < n, (↑x : WithTop ι) = τ ω
Tactic: simp only [Finset.coe_Iio, Set.mem_image, Set.mem_Iio]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : AddCommMonoid E
n : ι
ω : Ω
h : τ ω < (↑n : WithTop ι)
⊢ ∃ x < n, (↑x : WithTop ι) = τ ω
have h_top : τ ω ≠ ⊤
Tactic: have h_top : τ ω ≠ ⊤ := fun h_contra ↦ by simp [h_contra] at h
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : AddCommMonoid E
n : ι
ω : Ω
h : τ ω < (↑n : WithTop ι)
h_top : τ ω ≠ ⊤
⊢ ∃ x < n, (↑x : WithTop ι) = τ ω
have lift : ∀ (i : ι) (hi : (↑i : WithTop ι) = τ ω) (h : (↑i : WithTop ι) < (↑n : WithTop ι)),
  ∃ x < n, (↑x : WithTop ι) = (↑i : WithTop ι)
Tactic: lift τ ω to ι using h_top with i hi
Cleared hypotheses: h, h_top
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : AddCommMonoid E
n : ι
⊢ stoppedProcess u τ n =
    Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n) +
      ∑ i ∈ Finset.Iio n, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)
have h_mem : ∀ (ω : Ω), τ ω < (↑n : WithTop ι) → τ ω ∈ WithTop.some '' (↑(Finset.Iio n) : Set ι)
Tactic: have h_mem : ∀ ω, τ ω < n → τ ω ∈ WithTop.some '' (Finset.Iio n) := by
    intro ω h
    simp only [Finset.coe_Iio, Set.mem_image, Set.mem_Iio]
    have h_top : τ ω ≠ ⊤ := fun h_contra ↦ by simp [h_contra] at h
    lift τ ω to ι using h_top with i hi
    exact ⟨i, mod_cast h, rfl⟩
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : AddCommMonoid E
n : ι
h_mem : ∀ (ω : Ω), τ ω < (↑n : WithTop ι) → τ ω ∈ WithTop.some '' (↑(Finset.Iio n) : Set ι)
⊢ stoppedProcess u τ n =
    Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n) +
      ∑ i ∈ Finset.Iio n, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)
have rw : Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n) +
    ∑ i ∈ Finset.Iio n with i < n, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i) =
  Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n) +
    ∑ i ∈ Finset.Iio n, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)
Tactic: rw [stoppedProcess_eq_of_mem_finset n h_mem]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
inst : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : AddCommMonoid E
n : ι
h_mem : ∀ (ω : Ω), τ ω < (↑n : WithTop ι) → τ ω ∈ WithTop.some '' (↑(Finset.Iio n) : Set ι)
⊢ Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n) +
      ∑ i ∈ Finset.Iio n with i < n, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i) =
    Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n) +
      ∑ i ∈ Finset.Iio n, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)
have e_a : ∀ (i : ι), i ∈ {i ∈ Finset.Iio n | i < n} ↔ i ∈ Finset.Iio n
Tactic: congr with i
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst_1 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' (↑s : Set ι)
⊢ MemLp (stoppedValue u τ) p μ
have rw : MemLp.{u_1, u_4} (ε := E) (∑ i ∈ s, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)) p μ
Tactic: rw [stoppedValue_eq_of_mem_finset hbdd]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst_1 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' (↑s : Set ι)
⊢ MemLp.{u_1, u_4} (ε := E) (∑ i ∈ s, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)) p μ
have refine : ∀ i ∈ s, MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
Tactic: refine memLp_finsetSum' _ fun i _ => MemLp.indicator ?_ (hu i)
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst_1 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' (↑s : Set ι)
i : ι
h : i ∈ s
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
have refine : (Set.range τ).Countable
Tactic: refine ℱ.le i {a : Ω | τ a = i} (hτ.measurableSet_eq_of_countable_range ?_ i)
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst_1 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' (↑s : Set ι)
i : ι
h : i ∈ s
⊢ (Set.range τ).Countable
have this : Set.range τ ⊆ WithTop.some '' (↑s : Set ι)
Tactic: have : Set.range τ ⊆ WithTop.some '' s := by
    rintro x ⟨y, rfl⟩
    exact hbdd y
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst_1 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
inst_3 : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
N : ι
hbdd : ∀ (ω : Ω), τ ω ≤ (↑N : WithTop ι)
⊢ MemLp (stoppedValue u τ) p μ
have refine : ∀ (ω : Ω), τ ω ∈ WithTop.some '' (↑(Finset.Iic N) : Set ι)
Tactic: refine memLp_stoppedValue_of_mem_finset hτ hu (s := Finset.Iic N) fun ω => ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst_1 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
inst_3 : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
N : ι
hbdd : ∀ (ω : Ω), τ ω ≤ (↑N : WithTop ι)
ω : Ω
⊢ τ ω ∈ WithTop.some '' (↑(Finset.Iic N) : Set ι)
have simp : ∃ x ≤ N, (↑x : WithTop ι) = τ ω
Tactic: simp only [Finset.coe_Iic, Set.mem_image, Set.mem_Iic]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst_1 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
inst_3 : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
N : ι
hbdd : ∀ (ω : Ω), τ ω ≤ (↑N : WithTop ι)
ω : Ω
⊢ ∃ x ≤ N, (↑x : WithTop ι) = τ ω
have hbdd₁ : τ ω ≤ (↑N : WithTop ι)
Tactic: specialize hbdd ω
Cleared hypotheses: hbdd
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst_1 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
inst_3 : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
N : ι
ω : Ω
hbdd : τ ω ≤ (↑N : WithTop ι)
⊢ ∃ x ≤ N, (↑x : WithTop ι) = τ ω
have h_top : τ ω ≠ ⊤
Tactic: have h_top : τ ω ≠ ⊤ := fun h_contra ↦ by simp [h_contra] at hbdd
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst_1 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
inst_3 : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
N : ι
ω : Ω
hbdd : τ ω ≤ (↑N : WithTop ι)
h_top : τ ω ≠ ⊤
⊢ ∃ x ≤ N, (↑x : WithTop ι) = τ ω
have lift : ∀ (i : ι) (hi : (↑i : WithTop ι) = τ ω) (hbdd : (↑i : WithTop ι) ≤ (↑N : WithTop ι)),
  ∃ x ≤ N, (↑x : WithTop ι) = (↑i : WithTop ι)
Tactic: lift τ ω to ι using h_top with i hi
Cleared hypotheses: hbdd, h_top
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), Integrable (u n) μ
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' (↑s : Set ι)
⊢ Integrable (stoppedValue u τ) μ
have simp_rw : ∀ (hu : ∀ (n : ι), MemLp (u n) 1 μ), MemLp (stoppedValue u τ) 1 μ
Tactic: simp_rw [← memLp_one_iff_integrable] at hu ⊢
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
inst_3 : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), Integrable (u n) μ
N : ι
hbdd : ∀ (ω : Ω), τ ω ≤ (↑N : WithTop ι)
⊢ Integrable (stoppedValue u τ) μ
have refine : ∀ (ω : Ω), τ ω ∈ WithTop.some '' (↑(Finset.Iic N) : Set ι)
Tactic: refine integrable_stoppedValue_of_mem_finset hτ hu (s := Finset.Iic N) fun ω => ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
inst_3 : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), Integrable (u n) μ
N : ι
hbdd : ∀ (ω : Ω), τ ω ≤ (↑N : WithTop ι)
ω : Ω
⊢ τ ω ∈ WithTop.some '' (↑(Finset.Iic N) : Set ι)
have simp : ∃ x ≤ N, (↑x : WithTop ι) = τ ω
Tactic: simp only [Finset.coe_Iic, Set.mem_image, Set.mem_Iic]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
inst_3 : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), Integrable (u n) μ
N : ι
hbdd : ∀ (ω : Ω), τ ω ≤ (↑N : WithTop ι)
ω : Ω
⊢ ∃ x ≤ N, (↑x : WithTop ι) = τ ω
have hbdd₁ : τ ω ≤ (↑N : WithTop ι)
Tactic: specialize hbdd ω
Cleared hypotheses: hbdd
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
inst_3 : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), Integrable (u n) μ
N : ι
ω : Ω
hbdd : τ ω ≤ (↑N : WithTop ι)
⊢ ∃ x ≤ N, (↑x : WithTop ι) = τ ω
have h_top : τ ω ≠ ⊤
Tactic: have h_top : τ ω ≠ ⊤ := fun h_contra ↦ by simp [h_contra] at hbdd
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : PartialOrder ι
ℱ : Filtration ι m
inst_2 : NormedAddCommGroup E
inst_3 : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), Integrable (u n) μ
N : ι
ω : Ω
hbdd : τ ω ≤ (↑N : WithTop ι)
h_top : τ ω ≠ ⊤
⊢ ∃ x ≤ N, (↑x : WithTop ι) = τ ω
have lift : ∀ (i : ι) (hi : (↑i : WithTop ι) = τ ω) (hbdd : (↑i : WithTop ι) ≤ (↑N : WithTop ι)),
  ∃ x ≤ N, (↑x : WithTop ι) = (↑i : WithTop ι)
Tactic: lift τ ω to ι using h_top with i hi
Cleared hypotheses: hbdd, h_top
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : TopologicalSpace ι
inst_3 : OrderTopology ι
inst_4 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_5 : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω < (↑n : WithTop ι) → τ ω ∈ WithTop.some '' (↑s : Set ι)
⊢ MemLp (stoppedProcess u τ n) p μ
have rw : MemLp
  (Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n) +
    ∑ i ∈ s with i < n, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i))
  p μ
Tactic: rw [stoppedProcess_eq_of_mem_finset n hbdd]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : TopologicalSpace ι
inst_3 : OrderTopology ι
inst_4 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_5 : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω < (↑n : WithTop ι) → τ ω ∈ WithTop.some '' (↑s : Set ι)
⊢ MemLp
    (Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n) +
      ∑ i ∈ s with i < n, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i))
    p μ
have refine_1 : MemLp (Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n)) p μ
Tactic: refine MemLp.add ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : TopologicalSpace ι
inst_3 : OrderTopology ι
inst_4 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_5 : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω < (↑n : WithTop ι) → τ ω ∈ WithTop.some '' (↑s : Set ι)
refine_1 : MemLp (Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n)) p μ
⊢ MemLp
    (Set.indicator {a : Ω | (↑n : WithTop ι) ≤ τ a} (u n) +
      ∑ i ∈ s with i < n, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i))
    p μ
have refine_2 : MemLp.{u_1, u_4} (ε := E) (∑ i ∈ s with i < n, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)) p μ
Tactic: refine MemLp.add ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : TopologicalSpace ι
inst_3 : OrderTopology ι
inst_4 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_5 : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω < (↑n : WithTop ι) → τ ω ∈ WithTop.some '' (↑s : Set ι)
this :
  MemLp.{u_1, u_4} (ε := E) (fun (ω : Ω) ↦ ∑ i ∈ s with i < n, Set.indicator {a : Ω | τ a = (↑i : WithTop ι)} (u i) ω) p
    μ
⊢ MemLp.{u_1, u_4} (ε := E) (∑ i ∈ s with i < n, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)) p μ
have h : Eq (α := Ω → E) (∑ i ∈ s with i < n, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)) fun (ω : Ω) ↦
  ∑ i ∈ s with i < n, Set.indicator {a : Ω | τ a = (↑i : WithTop ι)} (u i) ω
Tactic: convert! this using 1
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : TopologicalSpace ι
inst_3 : OrderTopology ι
inst_4 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_5 : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω < (↑n : WithTop ι) → τ ω ∈ WithTop.some '' (↑s : Set ι)
this :
  MemLp.{u_1, u_4} (ε := E) (fun (ω : Ω) ↦ ∑ i ∈ s with i < n, Set.indicator {a : Ω | τ a = (↑i : WithTop ι)} (u i) ω) p
    μ
⊢ Eq (α := Ω → E) (∑ i ∈ s with i < n, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)) fun (ω : Ω) ↦
    ∑ i ∈ s with i < n, Set.indicator {a : Ω | τ a = (↑i : WithTop ι)} (u i) ω
have h : ∀ (ω : Ω),
  Eq.{u_4 + 1} (α := E) ((∑ i ∈ s with i < n, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)) ω)
    (∑ i ∈ s with i < n, Set.indicator {a : Ω | τ a = (↑i : WithTop ι)} (u i) ω)
Tactic: ext1 ω
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : TopologicalSpace ι
inst_3 : OrderTopology ι
inst_4 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_5 : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω < (↑n : WithTop ι) → τ ω ∈ WithTop.some '' (↑s : Set ι)
⊢ MemLp.{u_1, u_4} (ε := E) (∑ i ∈ s with i < n, Set.indicator {ω : Ω | τ ω = (↑i : WithTop ι)} (u i)) p μ
have refine_2 : MemLp.{u_1, u_4} (ε := E) (fun (ω : Ω) ↦ ∑ i ∈ s with i < n, Set.indicator {a : Ω | τ a = (↑i : WithTop ι)} (u i) ω) p μ
Tactic: suffices MemLp (fun ω => ∑ i ∈ s with i < n, {a : Ω | τ a = i}.indicator (u i) ω) p μ by
      convert! this using 1; ext1 ω; simp only [Finset.sum_apply]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : TopologicalSpace ι
inst_3 : OrderTopology ι
inst_4 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_5 : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω < (↑n : WithTop ι) → τ ω ∈ WithTop.some '' (↑s : Set ι)
⊢ MemLp.{u_1, u_4} (ε := E) (fun (ω : Ω) ↦ ∑ i ∈ s with i < n, Set.indicator {a : Ω | τ a = (↑i : WithTop ι)} (u i) ω) p
    μ
have refine_2 : ∀ i ∈ {i ∈ s | i < n}, MeasurableSet.{u_1} (α := Ω) {a : Ω | τ a = (↑i : WithTop ι)}
Tactic: refine memLp_finsetSum _ fun i _ => MemLp.indicator ?_ (hu i)
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : TopologicalSpace ι
inst_3 : OrderTopology ι
inst_4 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_5 : NormedAddCommGroup E
inst_6 : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
⊢ MemLp (stoppedProcess u τ n) p μ
have refine : ∀ (ω : Ω) (h : τ ω < (↑n : WithTop ι)), τ ω ∈ WithTop.some '' (↑(Finset.Iic n) : Set ι)
Tactic: refine memLp_stoppedProcess_of_mem_finset hτ hu n (s := Finset.Iic n) fun ω h => ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : TopologicalSpace ι
inst_3 : OrderTopology ι
inst_4 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_5 : NormedAddCommGroup E
inst_6 : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
ω : Ω
h : τ ω < (↑n : WithTop ι)
⊢ τ ω ∈ WithTop.some '' (↑(Finset.Iic n) : Set ι)
have simp : ∃ x ≤ n, (↑x : WithTop ι) = τ ω
Tactic: simp only [Finset.coe_Iic, Set.mem_image, Set.mem_Iic]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : TopologicalSpace ι
inst_3 : OrderTopology ι
inst_4 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_5 : NormedAddCommGroup E
inst_6 : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
ω : Ω
h : τ ω < (↑n : WithTop ι)
⊢ ∃ x ≤ n, (↑x : WithTop ι) = τ ω
have h_top : τ ω ≠ ⊤
Tactic: have h_top : τ ω ≠ ⊤ := fun h_contra ↦ by simp [h_contra] at h
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : TopologicalSpace ι
inst_3 : OrderTopology ι
inst_4 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_5 : NormedAddCommGroup E
inst_6 : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
ω : Ω
h : τ ω < (↑n : WithTop ι)
h_top : τ ω ≠ ⊤
⊢ ∃ x ≤ n, (↑x : WithTop ι) = τ ω
have lift : ∀ (i : ι) (hi : (↑i : WithTop ι) = τ ω) (h : (↑i : WithTop ι) < (↑n : WithTop ι)),
  ∃ x ≤ n, (↑x : WithTop ι) = (↑i : WithTop ι)
Tactic: lift τ ω to ι using h_top with i hi
Cleared hypotheses: h, h_top
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : TopologicalSpace ι
inst_3 : OrderTopology ι
inst_4 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_5 : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), Integrable (u n) μ
n : ι
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω < (↑n : WithTop ι) → τ ω ∈ WithTop.some '' (↑s : Set ι)
⊢ Integrable (stoppedProcess u τ n) μ
have simp_rw : ∀ (hu : ∀ (n : ι), MemLp (u n) 1 μ), MemLp (stoppedProcess u τ n) 1 μ
Tactic: simp_rw [← memLp_one_iff_integrable] at hu ⊢
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : TopologicalSpace ι
inst_3 : OrderTopology ι
inst_4 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_5 : NormedAddCommGroup E
inst_6 : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), Integrable (u n) μ
n : ι
⊢ Integrable (stoppedProcess u τ n) μ
have refine : ∀ (ω : Ω) (h : τ ω < (↑n : WithTop ι)), τ ω ∈ WithTop.some '' (↑(Finset.Iic n) : Set ι)
Tactic: refine integrable_stoppedProcess_of_mem_finset hτ hu n (s := Finset.Iic n) fun ω h => ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : TopologicalSpace ι
inst_3 : OrderTopology ι
inst_4 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_5 : NormedAddCommGroup E
inst_6 : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), Integrable (u n) μ
n : ι
ω : Ω
h : τ ω < (↑n : WithTop ι)
⊢ τ ω ∈ WithTop.some '' (↑(Finset.Iic n) : Set ι)
have simp : ∃ x ≤ n, (↑x : WithTop ι) = τ ω
Tactic: simp only [Finset.coe_Iic, Set.mem_image, Set.mem_Iic]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst_1 : LinearOrder ι
inst_2 : TopologicalSpace ι
inst_3 : OrderTopology ι
inst_4 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_5 : NormedAddCommGroup E
inst_6 : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), Integrable (u n) μ
n : ι
ω : Ω
h : τ ω < (↑n : WithTop ι)
⊢ ∃ x ≤ n, (↑x : WithTop ι) = τ ω
have h_top : τ ω ≠ ⊤
Tactic: have h_top : τ ω ≠ ⊤ := fun h_contra ↦ by simp [h_contra] at h