awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
hX : IsAEKolmogorovProcess X P p q M
s : T
refine : X s =ᶠ[ae P] IsAEKolmogorovProcess.mk X hX s
⊢ AEMeasurable (X s) P

Tactic:
refine ⟨hX.mk X s, hX.IsKolmogorovProcess_mk.measurable s, ?_⟩
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
hX : IsAEKolmogorovProcess X P p q M
s : T
ω : Ω
hω : X s ω = IsAEKolmogorovProcess.mk X hX s ω
⊢ X s ω = IsAEKolmogorovProcess.mk X hX s ω

Tactic:
hω
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
hX : IsAEKolmogorovProcess X P p q M
s : T
h :
  ∀ (a : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ X s x = IsAEKolmogorovProcess.mk X hX s x) x} x →
          Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ X s x = IsAEKolmogorovProcess.mk X hX s x) x} x}
      a
h₁ h₂ : ∀ (ω : Ω) (hω : X s ω = IsAEKolmogorovProcess.mk X hX s ω), X s ω = IsAEKolmogorovProcess.mk X hX s ω
⊢ X s =ᶠ[ae P] IsAEKolmogorovProcess.mk X hX s

Tactic:
filter_upwards [hX.ae_eq_mk s] with ω hω using hω

Premises used: ProbabilityTheory.IsAEKolmogorovProcess.ae_eq_mk
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
h_meas : ∀ (s : T), Measurable (X s)
h_kol : ∀ (s t : T), ∫⁻ (ω : Ω), edist (X s ω) (X t ω) ^ p ∂P ≤ (↑M : ℝ≥0∞) * edist s t ^ q
hp : 0 < p
hq : 0 < q
s t : T
this : Measurable.{u_2, u_3} (β := E × E) fun (ω : Ω) ↦ (X s ω, X t ω)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : Measurable.{u_2, u_3} (β := E × E) fun (ω : Ω) ↦ (X s ω, X t ω)),
    Measurable.{u_2, u_3} (β := E × E) fun (ω : Ω) ↦ (X s ω, X t ω)
⊢ Measurable.{u_2, u_3} (β := E × E) fun (ω : Ω) ↦ (X s ω, X t ω)

Tactic:
rwa [Prod.borelSpace.measurable_eq] at this

Premises used: BorelSpace.measurable_eq
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
h_meas : ∀ (s : T), Measurable (X s)
h_kol : ∀ (s t : T), ∫⁻ (ω : Ω), edist (X s ω) (X t ω) ^ p ∂P ≤ (↑M : ℝ≥0∞) * edist s t ^ q
hp : 0 < p
hq : 0 < q
s t : T
suffices : Measurable.{u_2, u_3} (β := E × E) fun (ω : Ω) ↦ (X s ω, X t ω)
⊢ Measurable.{u_2, u_3} (β := E × E) fun (ω : Ω) ↦ (X s ω, X t ω)

Tactic:
suffices Measurable (fun ω ↦ (X s ω, X t ω)) by
      rwa [Prod.borelSpace.measurable_eq] at this
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
h_meas : ∀ (s : T), Measurable (X s)
h_kol : ∀ (s t : T), ∫⁻ (ω : Ω), edist (X s ω) (X t ω) ^ p ∂P ≤ (↑M : ℝ≥0∞) * edist s t ^ q
hp : 0 < p
hq : 0 < q
s t : T
⊢ Measurable.{u_2, u_3} (β := E × E) fun (ω : Ω) ↦ (X s ω, X t ω)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
s t : T
h : edist s t = 0
this : (ae P).EventuallyEq (β := ℝ≥0∞) (fun (ω : Ω) ↦ edist (X s ω) (X t ω) ^ p) 0
h₁ : ∀ (ω : Ω) (hω : edist (X s ω) (X t ω) ^ p = 0 ω), edist (X s ω) (X t ω) = 0
⊢ ∀ᵐ (ω : Ω) ∂P, edist (X s ω) (X t ω) = 0

Tactic:
filter_upwards [this] with ω hω
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
s t : T
h : edist s t = 0
this : (ae P).EventuallyEq (β := ℝ≥0∞) (fun (ω : Ω) ↦ edist (X s ω) (X t ω) ^ p) 0
ω : Ω
hω : edist (X s ω) (X t ω) ^ p = 0 ω
⊢ edist (X s ω) (X t ω) = 0

Tactic:
simpa [hX.p_pos, not_lt_of_gt hX.p_pos] using hω

Premises used: not_lt_of_gt, ProbabilityTheory.IsAEKolmogorovProcess.p_pos
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
s t : T
h : edist s t = 0
suffices : (ae P).EventuallyEq (β := ℝ≥0∞) (fun (ω : Ω) ↦ edist (X s ω) (X t ω) ^ p) 0
⊢ ∀ᵐ (ω : Ω) ∂P, edist (X s ω) (X t ω) = 0

Tactic:
suffices (fun ω ↦ edist (X s ω) (X t ω) ^ p) =ᵐ[P] 0 by
    filter_upwards [this] with ω hω
    simpa [hX.p_pos, not_lt_of_gt hX.p_pos] using hω
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
s t : T
h : edist s t = 0
rw : ∫⁻ (a : Ω), edist (X s a) (X t a) ^ p ∂P ≤ 0
⊢ (ae P).EventuallyEq (β := ℝ≥0∞) (fun (ω : Ω) ↦ edist (X s ω) (X t ω) ^ p) 0

Tactic:
rw [← lintegral_eq_zero_iff' (hX.aemeasurable_edist.pow_const p), ← nonpos_iff_eq_zero]

Premises used: AEMeasurable.pow_const, MeasureTheory.lintegral_eq_zero_iff', ProbabilityTheory.IsAEKolmogorovProcess.aemeasurable_edist, nonpos_iff_eq_zero
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
s t : T
h : edist s t = 0
⊢ ∫⁻ (ω : Ω), edist (X s ω) (X t ω) ^ p ∂P ≤ (↑M : ℝ≥0∞) * edist s t ^ q

Tactic:
hX.kolmogorovCondition s t

Premises used: ProbabilityTheory.IsAEKolmogorovProcess.kolmogorovCondition
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
s t : T
h : edist s t = 0
⊢ (↑M : ℝ≥0∞) * edist s t ^ q = 0

Tactic:
simp [h, hX.q_pos]

Premises used: ProbabilityTheory.IsAEKolmogorovProcess.q_pos
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
s t : T
h : edist s t = 0
calc : (↑M : ℝ≥0∞) * edist s t ^ q = 0
⊢ ∫⁻ (a : Ω), edist (X s a) (X t a) ^ p ∂P ≤ 0

Tactic:
calc ∫⁻ ω, edist (X s ω) (X t ω) ^ p ∂P
  _ ≤ M * edist s t ^ q := hX.kolmogorovCondition s t
  _ = 0 := by simp [h, hX.q_pos]

Premises used: ProbabilityTheory.IsAEKolmogorovProcess.kolmogorovCondition, EDist.edist
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsKolmogorovProcess X P p q M
s t : T
h : edist s t = 0
⊢ ∀ᵐ (ω : Ω) ∂P, edist (X s ω) (X t ω) = 0

Tactic:
hX.IsAEKolmogorovProcess.edist_eq_zero h

Premises used: ProbabilityTheory.IsKolmogorovProcess.IsAEKolmogorovProcess, ProbabilityTheory.IsAEKolmogorovProcess.edist_eq_zero
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q 0
s t : T
this : (ae P).EventuallyEq (β := ℝ≥0∞) (fun (ω : Ω) ↦ edist (X s ω) (X t ω) ^ p) 0
h : ∀ (ω : Ω) (hω : edist (X s ω) (X t ω) ^ p = 0 ω), edist (X s ω) (X t ω) = 0
⊢ ∀ᵐ (ω : Ω) ∂P, edist (X s ω) (X t ω) = 0

Tactic:
filter_upwards [this] with ω hω
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q 0
s t : T
this : (ae P).EventuallyEq (β := ℝ≥0∞) (fun (ω : Ω) ↦ edist (X s ω) (X t ω) ^ p) 0
ω : Ω
hω : edist (X s ω) (X t ω) ^ p = 0 ω
⊢ edist (X s ω) (X t ω) = 0

Tactic:
simpa [hX.p_pos, not_lt_of_gt hX.p_pos] using hω

Premises used: not_lt_of_gt, ProbabilityTheory.IsAEKolmogorovProcess.p_pos
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q 0
s t : T
suffices : (ae P).EventuallyEq (β := ℝ≥0∞) (fun (ω : Ω) ↦ edist (X s ω) (X t ω) ^ p) 0
⊢ ∀ᵐ (ω : Ω) ∂P, edist (X s ω) (X t ω) = 0

Tactic:
suffices (fun ω ↦ edist (X s ω) (X t ω) ^ p) =ᵐ[P] 0 by
    filter_upwards [this] with ω hω
    simpa [hX.p_pos, not_lt_of_gt hX.p_pos] using hω
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q 0
s t : T
rw : ∫⁻ (a : Ω), edist (X s a) (X t a) ^ p ∂P ≤ 0
⊢ (ae P).EventuallyEq (β := ℝ≥0∞) (fun (ω : Ω) ↦ edist (X s ω) (X t ω) ^ p) 0

Tactic:
rw [← lintegral_eq_zero_iff' (hX.aemeasurable_edist.pow_const p), ← nonpos_iff_eq_zero]

Premises used: AEMeasurable.pow_const, MeasureTheory.lintegral_eq_zero_iff', ProbabilityTheory.IsAEKolmogorovProcess.aemeasurable_edist, nonpos_iff_eq_zero
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q 0
s t : T
⊢ ∫⁻ (ω : Ω), edist (X s ω) (X t ω) ^ p ∂P ≤ 0 * edist s t ^ q

Tactic:
hX.kolmogorovCondition s t

Premises used: ProbabilityTheory.IsAEKolmogorovProcess.kolmogorovCondition
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q 0
s t : T
⊢ 0 * edist s t ^ q = 0

Tactic:
simp
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q 0
s t : T
calc : 0 * edist s t ^ q = 0
⊢ ∫⁻ (a : Ω), edist (X s a) (X t a) ^ p ∂P ≤ 0

Tactic:
calc ∫⁻ ω, edist (X s ω) (X t ω) ^ p ∂P
  _ ≤ 0 * edist s t ^ q := hX.kolmogorovCondition s t
  _ = 0 := by simp

Premises used: ProbabilityTheory.IsAEKolmogorovProcess.kolmogorovCondition, EDist.edist
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
P : Measure Ω
X : T → Ω → E
hX : IsKolmogorovProcess X P p q 0
s t : T
⊢ ∀ᵐ (ω : Ω) ∂P, edist (X s ω) (X t ω) = 0

Tactic:
hX.IsAEKolmogorovProcess.edist_eq_zero_of_const_eq_zero s t

Premises used: ProbabilityTheory.IsAEKolmogorovProcess.edist_eq_zero_of_const_eq_zero, ProbabilityTheory.IsKolmogorovProcess.IsAEKolmogorovProcess
-- Module: Mathlib.Probability.Process.LocalProperty
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : Preorder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
P : Measure Ω
n : ℕ
⊢ IsStoppingTime 𝓕 fun (x : Ω) ↦ ⊤

Tactic:
simp [IsStoppingTime]

Premises used: MeasureTheory.IsStoppingTime
-- Module: Mathlib.Probability.Process.LocalProperty
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : Preorder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
P : Measure Ω
x : Ω
x_1 x_2 : ℕ
h : x_1 ≤ x_2
⊢ LE.le.{u_1} (α := WithTop ι) ((fun (x : ℕ) ↦ (⊤ : WithTop ι)) x_1) ((fun (x : ℕ) ↦ (⊤ : WithTop ι)) x_2)

Tactic:
simp
-- Module: Mathlib.Probability.Process.LocalProperty
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder ι
𝓕 : Filtration ι mΩ
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
τ σ : ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : IsLocalizingSequence 𝓕 σ P
ω : Ω
hτω : Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ τ x ω) atTop (𝓝 ⊤)
hσω : Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ σ x ω) atTop (𝓝 ⊤)
⊢ Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ (τ ⊓ σ) x ω) atTop (𝓝 ⊤)

Tactic:
hτω.min hσω

Premises used: Filter.Tendsto.min
-- Module: Mathlib.Probability.Process.LocalProperty
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder ι
𝓕 : Filtration ι mΩ
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
τ σ : ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : IsLocalizingSequence 𝓕 σ P
h :
  ∀ (a : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω)
            {x : Ω | (fun (ω : Ω) ↦ Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ τ x ω) atTop (𝓝 ⊤)) x} x →
          Membership.mem (γ := Set Ω)
            {x : Ω |
              Membership.mem (γ := Set Ω)
                  {x : Ω | (fun (ω : Ω) ↦ Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ σ x ω) atTop (𝓝 ⊤)) x} x →
                Membership.mem (γ := Set Ω)
                  {x : Ω | (fun (ω : Ω) ↦ Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ (τ ⊓ σ) x ω) atTop (𝓝 ⊤)) x}
                  x}
            x}
      a
h₁ h₂ :
  ∀ (ω : Ω) (hτω : Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ τ x ω) atTop (𝓝 ⊤))
    (hσω : Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ σ x ω) atTop (𝓝 ⊤)),
    Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ (τ ⊓ σ) x ω) atTop (𝓝 ⊤)
⊢ ∀ᵐ (ω : Ω) ∂P, Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ (τ ⊓ σ) x ω) atTop (𝓝 ⊤)

Tactic:
filter_upwards [hτ.tendsto_top, hσ.tendsto_top] with ω hτω hσω using hτω.min hσω

Premises used: ProbabilityTheory.IsLocalizingSequence.toIsPreLocalizingSequence, ProbabilityTheory.IsPreLocalizingSequence.tendsto_top
-- Module: Mathlib.Probability.Process.LocalProperty
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder ι
𝓕 : Filtration ι mΩ
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
τ σ : ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : IsLocalizingSequence 𝓕 σ P
ω : Ω
hτω : Monotone.{0, u_1} (β := WithTop ι) fun (x : ℕ) ↦ τ x ω
hσω : Monotone.{0, u_1} (β := WithTop ι) fun (x : ℕ) ↦ σ x ω
⊢ Monotone.{0, u_1} (β := WithTop ι) fun (x : ℕ) ↦ (τ ⊓ σ) x ω

Tactic:
hτω.min hσω

Premises used: Monotone.min
-- Module: Mathlib.Probability.Process.LocalProperty
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder ι
𝓕 : Filtration ι mΩ
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
τ σ : ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : IsLocalizingSequence 𝓕 σ P
h :
  ∀ (a : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω) {x : Ω | (fun (ω : Ω) ↦ Monotone.{0, u_1} (β := WithTop ι) fun (x : ℕ) ↦ τ x ω) x}
            x →
          Membership.mem (γ := Set Ω)
            {x : Ω |
              Membership.mem (γ := Set Ω)
                  {x : Ω | (fun (ω : Ω) ↦ Monotone.{0, u_1} (β := WithTop ι) fun (x : ℕ) ↦ σ x ω) x} x →
                Membership.mem (γ := Set Ω)
                  {x : Ω | (fun (ω : Ω) ↦ Monotone.{0, u_1} (β := WithTop ι) fun (x : ℕ) ↦ (τ ⊓ σ) x ω) x} x}
            x}
      a
h₁ h₂ :
  ∀ (ω : Ω) (hτω : Monotone.{0, u_1} (β := WithTop ι) fun (x : ℕ) ↦ τ x ω)
    (hσω : Monotone.{0, u_1} (β := WithTop ι) fun (x : ℕ) ↦ σ x ω),
    Monotone.{0, u_1} (β := WithTop ι) fun (x : ℕ) ↦ (τ ⊓ σ) x ω
⊢ ∀ᵐ (ω : Ω) ∂P, Monotone.{0, u_1} (β := WithTop ι) fun (x : ℕ) ↦ (τ ⊓ σ) x ω

Tactic:
filter_upwards [hτ.mono, hσ.mono] with ω hτω hσω using hτω.min hσω

Premises used: ProbabilityTheory.IsLocalizingSequence.mono
-- Module: Mathlib.Probability.Process.LocalProperty
Goal:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p : (ι → Ω → E) → Prop
inst_1 : OrderBot ι
inst_2 : TopologicalSpace ι
inst_3 : OrderTopology ι
inst_4 : Zero E
hX : Locally p 𝓕 X P
⊢ IsLocalizingSequence 𝓕 (hX.localSeq (p := p)) P

Tactic:
hX.choose_spec.1

Premises used: ProbabilityTheory.Locally.localSeq, Exists.choose_spec, And.left
-- Module: Mathlib.Probability.Process.LocalProperty
Goal:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p : (ι → Ω → E) → Prop
inst_1 : OrderBot ι
inst_2 : TopologicalSpace ι
inst_3 : OrderTopology ι
inst_4 : Zero E
hX : Locally p 𝓕 X P
n : ℕ
⊢ p (stoppedProcess (fun (i : ι) ↦ Set.indicator {ω : Ω | ⊥ < hX.localSeq (p := p) n ω} (X i)) (hX.localSeq (p := p) n))

Tactic:
hX.choose_spec.2 n

Premises used: ProbabilityTheory.Locally.localSeq, Exists.choose_spec, setOf, And.right
-- Module: Mathlib.Probability.Process.LocalProperty
Goal:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p : (ι → Ω → E) → Prop
inst_1 : OrderBot ι
inst_2 : TopologicalSpace ι
inst_3 : OrderTopology ι
inst_4 : Zero E
hp : p X
⊢ ∀ (n : ℕ),
    p
      (stoppedProcess
        (fun (i : ι) ↦
          Set.indicator {ω : Ω | LT.lt.{u_1} (α := WithTop ι) ⊥ ((fun (n : ℕ) (x : Ω) ↦ (⊤ : WithTop ι)) n ω)} (X i))
        ((fun (n : ℕ) (x : Ω) ↦ (⊤ : WithTop ι)) n))

Tactic:
simpa
-- Module: Mathlib.Probability.Process.LocalProperty
Goal:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p q : (ι → Ω → E) → Prop
inst_1 : OrderBot ι
inst_2 : TopologicalSpace ι
inst_3 : OrderTopology ι
inst_4 : Zero E
hpq : ∀ (X : ι → Ω → E), p X → q X
hpX : Locally p 𝓕 X P
⊢ Locally q 𝓕 X P

Tactic:
⟨hpX.localSeq, hpX.isLocalizingSequence_localSeq, fun n ↦ hpq _ <| hpX.stoppedProcess_localSeq n⟩

Premises used: ProbabilityTheory.Locally.localSeq, ProbabilityTheory.Locally.isLocalizingSequence_localSeq, Set.indicator, setOf, MeasureTheory.stoppedProcess, Bot.bot, ProbabilityTheory.Locally.stoppedProcess_localSeq, And.intro, LT.lt, Exists.intro, ProbabilityTheory.Locally
-- Module: Mathlib.Probability.Process.LocalProperty
Goal:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p q : (ι → Ω → E) → Prop
inst_1 : OrderBot ι
inst_2 : TopologicalSpace ι
inst_3 : OrderTopology ι
inst_4 : Zero E
hX : Locally (fun (Y : ι → Ω → E) ↦ p Y ∧ q Y) 𝓕 X P
⊢ Locally p 𝓕 X P ∧ Locally q 𝓕 X P

Tactic:
⟨hX.mono <| fun _ ↦ And.left, hX.mono <| fun _ ↦ And.right⟩

Premises used: And.right, And.left, And.intro, ProbabilityTheory.Locally.mono
-- Module: Mathlib.Probability.Process.LocalProperty
Goal:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p q : (ι → Ω → E) → Prop
inst_1 : OrderBot ι
inst_2 : TopologicalSpace ι
inst_3 : OrderTopology ι
inst_4 : Zero E
hX : Locally (fun (Y : ι → Ω → E) ↦ p Y ∧ q Y) 𝓕 X P
⊢ Locally p 𝓕 X P

Tactic:
hX.of_and.left

Premises used: And.left, ProbabilityTheory.Locally.of_and
-- Module: Mathlib.Probability.Process.LocalProperty
Goal:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p q : (ι → Ω → E) → Prop
inst_1 : OrderBot ι
inst_2 : TopologicalSpace ι
inst_3 : OrderTopology ι
inst_4 : Zero E
hX : Locally (fun (Y : ι → Ω → E) ↦ p Y ∧ q Y) 𝓕 X P
⊢ Locally q 𝓕 X P

Tactic:
hX.of_and.right

Premises used: And.right, ProbabilityTheory.Locally.of_and
-- Module: Mathlib.Probability.Process.LocalProperty
Goal:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
inst : LinearOrder ι
𝓕 : Filtration ι mΩ
p q : (ι → Ω → E) → Prop
inst_1 : OrderBot ι
inst_2 : Zero E
hp : IsStable 𝓕 p
hq : IsStable 𝓕 q
⊢ IsStable.{u_1, u_2, u_3} (E := E) 𝓕 fun (X : ι → Ω → E) ↦ p X ∧ q X

Tactic:
fun _ hX τ hτ ↦ ⟨hp _ hX.left τ hτ, hq _ hX.right τ hτ⟩

Premises used: ProbabilityTheory.IsStable, And.right, And.left, And.intro
-- Module: Mathlib.Probability.Process.LocalProperty
Goal:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder ι
𝓕 : Filtration ι mΩ
p : (ι → Ω → E) → Prop
inst_1 : OrderBot ι
inst_2 : Zero E
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
hp : IsStable 𝓕 p
⊢ IsStable.{u_1, u_2, u_3} (E := E) 𝓕 fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P

Tactic:
fun X hX τ hτ ↦ ⟨hX.localSeq, hX.isLocalizingSequence_localSeq, fun n ↦ ?_⟩

Premises used: ProbabilityTheory.Locally.localSeq, ProbabilityTheory.IsStable, ProbabilityTheory.Locally.isLocalizingSequence_localSeq, And.intro, Exists.intro, ProbabilityTheory.Locally
-- Module: Mathlib.Probability.Process.LocalProperty
Goal:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder ι
𝓕 : Filtration ι mΩ
p : (ι → Ω → E) → Prop
inst_1 : OrderBot ι
inst_2 : Zero E
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
hp : IsStable 𝓕 p
refine :
  ∀ (X : ι → Ω → E) (hX : (fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) X) (τ : Ω → WithTop ι) (hτ : IsStoppingTime 𝓕 τ)
    (n : ℕ),
    p
      (stoppedProcess
        (fun (i : ι) ↦
          Set.indicator {ω : Ω | ⊥ < Locally.localSeq (p := p) hX n ω}
            (stoppedProcess (fun (i : ι) ↦ Set.indicator {ω : Ω | ⊥ < τ ω} (X i)) τ i))
        (Locally.localSeq (p := p) hX n))
⊢ IsStable.{u_1, u_2, u_3} (E := E) 𝓕 fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P

Tactic:
refine fun X hX τ hτ ↦ ⟨hX.localSeq, hX.isLocalizingSequence_localSeq, fun n ↦ ?_⟩
-- Module: Mathlib.Probability.Process.LocalProperty
Goal:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder ι
𝓕 : Filtration ι mΩ
p : (ι → Ω → E) → Prop
inst_1 : OrderBot ι
inst_2 : Zero E
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
hp : IsStable 𝓕 p
X : ι → Ω → E
hX : (fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) X
τ : Ω → WithTop ι
hτ : IsStoppingTime 𝓕 τ
n : ℕ
simp_rw :
  p fun (i : ι) ↦
    Set.indicator {ω : Ω | ⊥ < τ ω}
      (Set.indicator {ω : Ω | ⊥ < Locally.localSeq (p := p) hX n ω}
        (stoppedProcess (stoppedProcess X (Locally.localSeq (p := p) hX n)) τ i))
⊢ p
    (stoppedProcess
      (fun (i : ι) ↦
        Set.indicator {ω : Ω | ⊥ < Locally.localSeq (p := p) hX n ω}
          (stoppedProcess (fun (i : ι) ↦ Set.indicator {ω : Ω | ⊥ < τ ω} (X i)) τ i))
      (Locally.localSeq (p := p) hX n))

Tactic:
simp_rw [← stoppedProcess_indicator_comm', Set.indicator_indicator, Set.inter_comm,
    ← Set.indicator_indicator, stoppedProcess_stoppedProcess, inf_comm,
    stoppedProcess_indicator_comm', ← stoppedProcess_stoppedProcess]

Premises used: MeasureTheory.stoppedProcess_stoppedProcess, MeasureTheory.stoppedProcess_indicator_comm', inf_comm, Set.inter_comm, Set.indicator_indicator