awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
inst_3 : SecondCountableTopology ι
inst_4 : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
T : ℕ → ι
hT : Tendsto T atTop atTop
n : ℕ
hn : ∀ (k : ℕ), (1 / 2) ^ n < (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)}
rw : ∀ (i : ℕ), (1 / 2) ^ n ≤ (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n i ω < min (τ n ω) (↑(T n) : WithTop ι)}
hs :
  ∀ᵐ (ω : Ω) ∂P,
    Antitone (β := Prop) fun (x : ℕ) ↦
      Membership.mem (γ := Set Ω) {ω : Ω | σ n x ω < min (τ n ω) (↑(T n) : WithTop ι)} ω
⊢ (1 / 2) ^ n ≤ (P : (a : Set Ω) → ℝ≥0∞) (⋂ (k : ℕ), {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)})
have hsm : ∀ (i : ℕ), NullMeasurableSet {ω : Ω | σ n i ω < min (τ n ω) (↑(T n) : WithTop ι)} P
Tactic: rw [measure_iInter_of_ae_antitone, le_iInf_iff]
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
inst_3 : SecondCountableTopology ι
inst_4 : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
T : ℕ → ι
hT : Tendsto T atTop atTop
n : ℕ
hn : ∀ (k : ℕ), (1 / 2) ^ n < (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)}
rw : ∀ (i : ℕ), (1 / 2) ^ n ≤ (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n i ω < min (τ n ω) (↑(T n) : WithTop ι)}
hs :
  ∀ᵐ (ω : Ω) ∂P,
    Antitone (β := Prop) fun (x : ℕ) ↦
      Membership.mem (γ := Set Ω) {ω : Ω | σ n x ω < min (τ n ω) (↑(T n) : WithTop ι)} ω
hsm : ∀ (i : ℕ), NullMeasurableSet {ω : Ω | σ n i ω < min (τ n ω) (↑(T n) : WithTop ι)} P
⊢ (1 / 2) ^ n ≤ (P : (a : Set Ω) → ℝ≥0∞) (⋂ (k : ℕ), {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)})
have hfin : ∃ (i : ℕ),
  Ne (α := ℝ≥0∞) ((P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n i ω < min (τ n ω) (↑(T n) : WithTop ι)} : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [measure_iInter_of_ae_antitone, le_iInf_iff]
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
inst_3 : SecondCountableTopology ι
inst_4 : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
T : ℕ → ι
hT : Tendsto T atTop atTop
n : ℕ
hn : ∀ (k : ℕ), (1 / 2) ^ n < (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)}
⊢ ∀ᵐ (ω : Ω) ∂P,
    Antitone (β := Prop) fun (x : ℕ) ↦
      Membership.mem (γ := Set Ω) {ω : Ω | σ n x ω < min (τ n ω) (↑(T n) : WithTop ι)} ω
have h : ∀ (ω : Ω) (hω : Monotone.{0, u_1} (β := WithTop ι) fun (x : ℕ) ↦ σ n x ω),
  Antitone (β := Prop) fun (x : ℕ) ↦ σ n x ω < min (τ n ω) (↑(T n) : WithTop ι)
Tactic: filter_upwards [(hσ n).mono] with ω hω
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (hypothesis)
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
inst_3 : SecondCountableTopology ι
inst_4 : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
T : ℕ → ι
hT : Tendsto T atTop atTop
n : ℕ
hn : ∀ (k : ℕ), (1 / 2) ^ n < (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)}
ω : Ω
hω : Monotone.{0, u_1} (β := WithTop ι) fun (x : ℕ) ↦ σ n x ω
i j : ℕ
hij : i ≤ j
⊢ LE.le (α := Prop) ((fun (x : ℕ) ↦ σ n x ω < min (τ n ω) (↑(T n) : WithTop ι)) j)
    ((fun (x : ℕ) ↦ σ n x ω < min (τ n ω) (↑(T n) : WithTop ι)) i)
have hω₁ : LE.le.{u_1} (α := WithTop ι) ((fun (x : ℕ) ↦ σ n x ω) i) ((fun (x : ℕ) ↦ σ n x ω) j)
Tactic: specialize hω hij
Cleared hypotheses: hω
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
inst_3 : SecondCountableTopology ι
inst_4 : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
T : ℕ → ι
hT : Tendsto T atTop atTop
n : ℕ
hn : ∀ (k : ℕ), (1 / 2) ^ n < (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)}
ω : Ω
i j : ℕ
hij : i ≤ j
hω : LE.le.{u_1} (α := WithTop ι) ((fun (x : ℕ) ↦ σ n x ω) i) ((fun (x : ℕ) ↦ σ n x ω) j)
⊢ LE.le (α := Prop) ((fun (x : ℕ) ↦ σ n x ω < min (τ n ω) (↑(T n) : WithTop ι)) j)
    ((fun (x : ℕ) ↦ σ n x ω < min (τ n ω) (↑(T n) : WithTop ι)) i)
have h : ∀
  (hn :
    ∀ (k : ℕ),
      HPow.hPow (α := ℝ≥0∞) 2⁻¹ n <
        (P : (a : Set Ω) → ℝ≥0∞) fun (ω : Ω) ↦ σ n k ω < τ n ω ∧ σ n k ω < (↑(T n) : WithTop ι)),
  σ n j ω < τ n ω → σ n j ω < (↑(T n) : WithTop ι) → σ n i ω < τ n ω ∧ σ n i ω < (↑(T n) : WithTop ι)
Tactic: simp [setOf] at *
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
inst_3 : SecondCountableTopology ι
inst_4 : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
T : ℕ → ι
hT : Tendsto T atTop atTop
n : ℕ
hn : ∀ (k : ℕ), (1 / 2) ^ n < (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)}
⊢ ∀ (i : ℕ), NullMeasurableSet {ω : Ω | σ n i ω < min (τ n ω) (↑(T n) : WithTop ι)} P
have hsm : ∀ (i : ℕ), MeasurableSet.{u_2} (α := Ω) {ω : Ω | σ n i ω < min (τ n ω) (↑(T n) : WithTop ι)}
Tactic: refine fun i ↦ .nullMeasurableSet ?_
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
inst_3 : SecondCountableTopology ι
inst_4 : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
T : ℕ → ι
hT : Tendsto T atTop atTop
n : ℕ
hn : ∀ (k : ℕ), (1 / 2) ^ n < (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)}
i : ℕ
⊢ MeasurableSet.{u_2} (α := Ω) {ω : Ω | σ n i ω < min (τ n ω) (↑(T n) : WithTop ι)}
have hsm : MeasurableSet.{u_2} (α := Ω) ({a : Ω | σ n i a < τ n a} ∩ {a : Ω | σ n i a < (↑(T n) : WithTop ι)})
Tactic: simp_rw [lt_inf_iff, Set.setOf_and]
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
inst_3 : SecondCountableTopology ι
inst_4 : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
⊢ ∃ (nk : ℕ → ℕ) (T : ℕ → ι),
    StrictMono nk ∧
      Tendsto T atTop atTop ∧
        ∀ (n : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n
have obtain : ∀ (T : ℕ → ι) (hT : Tendsto T atTop atTop)
  (h :
    ∀ (n : ℕ), ∃ (k : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n),
  ∃ (nk : ℕ → ℕ) (T : ℕ → ι),
    StrictMono nk ∧
      Tendsto T atTop atTop ∧
        ∀ (n : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n
Tactic: obtain ⟨T, hT, h⟩ := isPreLocalizingSequence_of_isLocalizingSequence_aux' hτ hσ
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
inst_3 : SecondCountableTopology ι
inst_4 : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
T : ℕ → ι
hT : Tendsto T atTop atTop
h : ∀ (n : ℕ), ∃ (k : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n
⊢ ∃ (nk : ℕ → ℕ) (T : ℕ → ι),
    StrictMono nk ∧
      Tendsto T atTop atTop ∧
        ∀ (n : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n
have choose : ∀ (nk : (n : ℕ) → ℕ)
  (hnk : ∀ (n : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n),
  ∃ (nk : ℕ → ℕ) (T : ℕ → ι),
    StrictMono nk ∧
      Tendsto T atTop atTop ∧
        ∀ (n : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n
Tactic: choose nk hnk using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
inst_3 : SecondCountableTopology ι
inst_4 : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
T : ℕ → ι
hT : Tendsto T atTop atTop
nk : (n : ℕ) → ℕ
hnk : ∀ (n : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n
⊢ ∃ (nk : ℕ → ℕ) (T : ℕ → ι),
    StrictMono nk ∧
      Tendsto T atTop atTop ∧
        ∀ (n : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n
have refine : ∀ (n : ℕ),
  {ω : Ω | σ n (mkStrictMonoAux nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ᶠ[ae P]
    {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)}
Tactic: refine ⟨mkStrictMonoAux nk, T, mkStrictMonoAux_strictMono nk, hT,
    fun n ↦ le_trans (EventuallyLE.measure_le ?_) (hnk n)⟩
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
inst_3 : SecondCountableTopology ι
inst_4 : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
T : ℕ → ι
hT : Tendsto T atTop atTop
nk : (n : ℕ) → ℕ
hnk : ∀ (n : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n
n : ℕ
⊢ {ω : Ω | σ n (mkStrictMonoAux nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ᶠ[ae P]
    {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)}
have h : ∀ (ω : Ω) (hω : Monotone.{0, u_1} (β := WithTop ι) fun (x : ℕ) ↦ σ n x ω),
  {ω : Ω | σ n (mkStrictMonoAux nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ω ≤
    {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ω
Tactic: filter_upwards [(hσ n).mono] with ω hω
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (hypothesis)
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
inst_3 : SecondCountableTopology ι
inst_4 : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
T : ℕ → ι
hT : Tendsto T atTop atTop
nk : (n : ℕ) → ℕ
hnk : ∀ (n : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n
n : ℕ
ω : Ω
hω : Monotone.{0, u_1} (β := WithTop ι) fun (x : ℕ) ↦ σ n x ω
⊢ {ω : Ω | σ n (mkStrictMonoAux nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ω ≤
    {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ω
have hω₁ : LE.le.{u_1} (α := WithTop ι) ((fun (x : ℕ) ↦ σ n x ω) (nk n)) ((fun (x : ℕ) ↦ σ n x ω) (mkStrictMonoAux nk n))
Tactic: specialize hω (le_mkStrictMonoAux nk n)
Cleared hypotheses: hω
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
inst_3 : SecondCountableTopology ι
inst_4 : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
T : ℕ → ι
hT : Tendsto T atTop atTop
nk : (n : ℕ) → ℕ
hnk : ∀ (n : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n
n : ℕ
ω : Ω
hω : LE.le.{u_1} (α := WithTop ι) ((fun (x : ℕ) ↦ σ n x ω) (nk n)) ((fun (x : ℕ) ↦ σ n x ω) (mkStrictMonoAux nk n))
⊢ {ω : Ω | σ n (mkStrictMonoAux nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ω ≤
    {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ω
have h : σ n (mkStrictMonoAux nk n) ω < τ n ω →
  σ n (mkStrictMonoAux nk n) ω < (↑(T n) : WithTop ι) → σ n (nk n) ω < τ n ω ∧ σ n (nk n) ω < (↑(T n) : WithTop ι)
Tactic: simp [setOf]
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
inst_3 : SecondCountableTopology ι
inst_4 : IsFiniteMeasure P
inst_5 : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
⊢ ∃ (nk : ℕ → ℕ), StrictMono nk ∧ IsPreLocalizingSequence 𝓕 (fun (i : ℕ) (ω : Ω) ↦ min (τ i ω) (σ i (nk i) ω)) P
have obtain : ∀ (nk : ℕ → ℕ) (T : ℕ → ι) (hnk : StrictMono nk) (hT : Tendsto T atTop atTop)
  (hP : ∀ (n : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n),
  ∃ (nk : ℕ → ℕ), StrictMono nk ∧ IsPreLocalizingSequence 𝓕 (fun (i : ℕ) (ω : Ω) ↦ min (τ i ω) (σ i (nk i) ω)) P
Tactic: obtain ⟨nk, T, hnk, hT, hP⟩ := isPreLocalizingSequence_of_isLocalizingSequence_aux hτ hσ
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
inst_3 : SecondCountableTopology ι
inst_4 : IsFiniteMeasure P
inst_5 : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
nk : ℕ → ℕ
T : ℕ → ι
hnk : StrictMono nk
hT : Tendsto T atTop atTop
hP : ∀ (n : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n
⊢ ∃ (nk : ℕ → ℕ), StrictMono nk ∧ IsPreLocalizingSequence 𝓕 (fun (i : ℕ) (ω : Ω) ↦ min (τ i ω) (σ i (nk i) ω)) P
have refine : ∀ᵐ (ω : Ω) ∂P, Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ min (τ x ω) (σ x (nk x) ω)) atTop (𝓝 ⊤)
Tactic: refine ⟨nk, hnk, fun n ↦ (hτ.isStoppingTime n).min ((hσ _).isStoppingTime _), ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (hypothesis)
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
inst_3 : SecondCountableTopology ι
inst_4 : IsFiniteMeasure P
inst_5 : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
nk : ℕ → ℕ
T : ℕ → ι
hnk : StrictMono nk
hT : Tendsto T atTop atTop
hP : ∀ (n : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n
⊢ ∀ᵐ (ω : Ω) ∂P, Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ min (τ x ω) (σ x (nk x) ω)) atTop (𝓝 ⊤)
have this : LT.lt (α := ℝ≥0∞) (∑' (n : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)}) ∞
Tactic: have : ∑' n, P {ω | σ n (nk n) ω < min (τ n ω) (T n)} < ∞ :=
    lt_of_le_of_lt (ENNReal.summable.tsum_mono ENNReal.summable hP)
      (tsum_geometric_lt_top.2 <| by simp)
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
Goal:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p : (ι → Ω → E) → Prop
inst_3 : SecondCountableTopology ι
inst_4 : IsFiniteMeasure P
inst_5 : DenselyOrdered ι
inst_6 : NoMaxOrder ι
inst_7 : Zero E
inst_8 : 𝓕.IsRightContinuous
hp : IsStable (mΩ := mΩ) 𝓕 p
⊢ Locally (fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) 𝓕 X P ↔ Locally p 𝓕 X P
have refine : ∀ (hL : Locally (fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) 𝓕 X P), Locally p 𝓕 X P
Tactic: refine ⟨fun hL ↦ ?_, fun hL ↦ ⟨hL.localSeq, hL.isLocalizingSequence_localSeq,
    fun n ↦ .of_prop <| hL.stoppedProcess_localSeq n⟩⟩
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
Goal:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p : (ι → Ω → E) → Prop
inst_3 : SecondCountableTopology ι
inst_4 : IsFiniteMeasure P
inst_5 : DenselyOrdered ι
inst_6 : NoMaxOrder ι
inst_7 : Zero E
inst_8 : 𝓕.IsRightContinuous
hp : IsStable (mΩ := mΩ) 𝓕 p
hL : Locally (fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) 𝓕 X P
⊢ Locally p 𝓕 X P
have choose : ∀ (τ : (n : ℕ) → ℕ → Ω → WithTop ι) (hτ₁ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (τ n) P)
  (hτ₂ :
    ∀ (n n_1 : ℕ),
      p
        (stoppedProcess
          (fun (i : ι) ↦
            Set.indicator {ω : Ω | ⊥ < τ n n_1 ω}
              (stoppedProcess
                (fun (i : ι) ↦
                  Set.indicator {ω : Ω | ⊥ < hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω} (X i))
                (hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n) i))
          (τ n n_1))),
  Locally p 𝓕 X P
Tactic: choose τ hτ₁ hτ₂ using hL.stoppedProcess_localSeq
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
Goal:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p : (ι → Ω → E) → Prop
inst_3 : SecondCountableTopology ι
inst_4 : IsFiniteMeasure P
inst_5 : DenselyOrdered ι
inst_6 : NoMaxOrder ι
inst_7 : Zero E
inst_8 : 𝓕.IsRightContinuous
hp : IsStable (mΩ := mΩ) 𝓕 p
hL : Locally (fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) 𝓕 X P
τ : (n : ℕ) → ℕ → Ω → WithTop ι
hτ₁ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (τ n) P
hτ₂ :
  ∀ (n n_1 : ℕ),
    p
      (stoppedProcess
        (fun (i : ι) ↦
          Set.indicator {ω : Ω | ⊥ < τ n n_1 ω}
            (stoppedProcess
              (fun (i : ι) ↦
                Set.indicator {ω : Ω | ⊥ < hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω} (X i))
              (hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n) i))
        (τ n n_1))
⊢ Locally p 𝓕 X P
have obtain : ∀ (nk : ℕ → ℕ) (hnk : StrictMono nk)
  (hpre :
    IsPreLocalizingSequence 𝓕
      (fun (i : ℕ) (ω : Ω) ↦ min (hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) i ω) (τ i (nk i) ω)) P),
  Locally p 𝓕 X P
Tactic: obtain ⟨nk, hnk, hpre⟩ :=
    hL.isLocalizingSequence_localSeq.isPrelocalizingSequence_inf_extraction hτ₁
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
Goal:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p : (ι → Ω → E) → Prop
inst_3 : SecondCountableTopology ι
inst_4 : IsFiniteMeasure P
inst_5 : DenselyOrdered ι
inst_6 : NoMaxOrder ι
inst_7 : Zero E
inst_8 : 𝓕.IsRightContinuous
hp : IsStable (mΩ := mΩ) 𝓕 p
hL : Locally (fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) 𝓕 X P
τ : (n : ℕ) → ℕ → Ω → WithTop ι
hτ₁ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (τ n) P
hτ₂ :
  ∀ (n n_1 : ℕ),
    p
      (stoppedProcess
        (fun (i : ι) ↦
          Set.indicator {ω : Ω | ⊥ < τ n n_1 ω}
            (stoppedProcess
              (fun (i : ι) ↦
                Set.indicator {ω : Ω | ⊥ < hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω} (X i))
              (hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n) i))
        (τ n n_1))
nk : ℕ → ℕ
hnk : StrictMono nk
hpre :
  IsPreLocalizingSequence 𝓕
    (fun (i : ℕ) (ω : Ω) ↦ min (hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) i ω) (τ i (nk i) ω)) P
⊢ Locally p 𝓕 X P
have refine : ∀ (n : ℕ),
  p
    (stoppedProcess
      (fun (i : ι) ↦
        Set.indicator {ω : Ω | ⊥ < min (hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω) (τ n (nk n) ω)}
          (X i))
      fun (ω : Ω) ↦ min (hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω) (τ n (nk n) ω))
Tactic: refine locally_of_isPreLocalizingSequence hp hpre <| fun n ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
Goal:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p : (ι → Ω → E) → Prop
inst_3 : SecondCountableTopology ι
inst_4 : IsFiniteMeasure P
inst_5 : DenselyOrdered ι
inst_6 : NoMaxOrder ι
inst_7 : Zero E
inst_8 : 𝓕.IsRightContinuous
hp : IsStable (mΩ := mΩ) 𝓕 p
hL : Locally (fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) 𝓕 X P
τ : (n : ℕ) → ℕ → Ω → WithTop ι
hτ₁ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (τ n) P
hτ₂ :
  ∀ (n n_1 : ℕ),
    p
      (stoppedProcess
        (fun (i : ι) ↦
          Set.indicator {ω : Ω | ⊥ < τ n n_1 ω}
            (stoppedProcess
              (fun (i : ι) ↦
                Set.indicator {ω : Ω | ⊥ < hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω} (X i))
              (hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n) i))
        (τ n n_1))
nk : ℕ → ℕ
hnk : StrictMono nk
hpre :
  IsPreLocalizingSequence 𝓕
    (fun (i : ℕ) (ω : Ω) ↦ min (hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) i ω) (τ i (nk i) ω)) P
n : ℕ
⊢ p
    (stoppedProcess
      (fun (i : ι) ↦
        Set.indicator {ω : Ω | ⊥ < min (hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω) (τ n (nk n) ω)}
          (X i))
      fun (ω : Ω) ↦ min (hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω) (τ n (nk n) ω))
have h : Eq (α := ι → Ω → E)
  (stoppedProcess
    (fun (i : ι) ↦
      Set.indicator {ω : Ω | ⊥ < min (hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω) (τ n (nk n) ω)}
        (X i))
    fun (ω : Ω) ↦ min (hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω) (τ n (nk n) ω))
  (stoppedProcess
    (fun (i : ι) ↦
      Set.indicator {ω : Ω | ⊥ < τ n (nk n) ω}
        (stoppedProcess
          (fun (i : ι) ↦ Set.indicator {ω : Ω | ⊥ < hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω} (X i))
          (hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n) i))
    (τ n (nk n)))
Tactic: convert! hτ₂ n (nk n) using 1 with