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

Goal state before:
pp: case hft
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ IntegrableOn (stoppedValue f fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω))
    {ω | ((range (n + 1)).sup' ⋯ fun k ↦ f k ω) < ↑ε} μ

pp: case hp
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ 0 ≤
    ∫ (ω : Ω) in {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω},
      stoppedValue f (fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω)) ω ∂μ

pp: case hq
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ 0 ≤
    ∫ (ω : Ω) in {ω | ((range (n + 1)).sup' ⋯ fun k ↦ f k ω) < ↑ε},
      stoppedValue f (fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω)) ω ∂μ

Tactic:
·

Goal state after:
case hft
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ IntegrableOn (stoppedValue f fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω))
    {ω | ((range (n + 1)).sup' ⋯ fun k ↦ f k ω) < ↑ε} μ
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Nonempty ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
inst✝ : LinearOrder ι
i : ι
ω : Ω
hτ : ¬τ ω = ⊤
hσ : ¬σ ω = ⊤
hστ : ¬σ ω ≤ τ ω
⊢ min (↑i) (σ ω) ≠ ⊤

Tactic:
·

Goal state after:
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Nonempty ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
inst✝ : LinearOrder ι
i : ι
ω : Ω
hτ : ¬τ ω = ⊤
hσ : ¬σ ω = ⊤
hστ : ¬σ ω ≤ τ ω
⊢ min (↑i) (σ ω) ≠ ⊤
Module: Mathlib.Probability.Martingale.BorelCantelli

Goal state before:
pp: Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ c, Tendsto (fun n ↦ stoppedAbove f (↑i) n ω) atTop (𝓝 c)
ω : Ω
hω : ∀ (i : ℕ), ∃ c, Tendsto (fun n ↦ stoppedAbove f (↑i) n ω) atTop (𝓝 c)
hωb : (upperBounds (Set.range fun n ↦ f n ω)).Nonempty
i : ℕ
hi : hωb.some < ↑i
hib : ∀ (n : ℕ), f n ω < ↑i
n : ℕ
⊢ ∀ (j : ℕ), ⊥ ≤ j → f j ω ∉ Set.Ici ↑i

Tactic:
·

Goal state after:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ c, Tendsto (fun n ↦ stoppedAbove f (↑i) n ω) atTop (𝓝 c)
ω : Ω
hω : ∀ (i : ℕ), ∃ c, Tendsto (fun n ↦ stoppedAbove f (↑i) n ω) atTop (𝓝 c)
hωb : (upperBounds (Set.range fun n ↦ f n ω)).Nonempty
i : ℕ
hi : hωb.some < ↑i
hib : ∀ (n : ℕ), f n ω < ↑i
n : ℕ
⊢ ∀ (j : ℕ), ⊥ ≤ j → f j ω ∉ Set.Ici ↑i
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case refine_1
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁷ : Nonempty ι
τ : Ω → WithTop ι
inst✝⁶ : LinearOrder ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
f : Filtration ι m
inst✝ : PseudoMetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑f i)
m_set : (t : Set (↑(Set.Iic i) × Ω)) → MeasurableSpace ↑t := fun x ↦ Subtype.instMeasurableSpace
s : Set (↑(Set.Iic i) × Ω) := {p | τ p.2 ≤ ↑i}
hs : MeasurableSet s
h_meas_fst : ∀ (t : Set (↑(Set.Iic i) × Ω)), Measurable fun x ↦ ↑(↑x).1
⊢ Measurable (s.domRestrict fun p ↦ min (↑↑p.1) (τ p.2))

pp: case refine_2
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁷ : Nonempty ι
τ : Ω → WithTop ι
inst✝⁶ : LinearOrder ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
f : Filtration ι m
inst✝ : PseudoMetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑f i)
m_set : (t : Set (↑(Set.Iic i) × Ω)) → MeasurableSpace ↑t := fun x ↦ Subtype.instMeasurableSpace
s : Set (↑(Set.Iic i) × Ω) := {p | τ p.2 ≤ ↑i}
hs : MeasurableSet s
h_meas_fst : ∀ (t : Set (↑(Set.Iic i) × Ω)), Measurable fun x ↦ ↑(↑x).1
⊢ Measurable (sᶜ.domRestrict fun p ↦ min (↑↑p.1) (τ p.2))

Tactic:
·

Goal state after:
case refine_1
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁷ : Nonempty ι
τ : Ω → WithTop ι
inst✝⁶ : LinearOrder ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
f : Filtration ι m
inst✝ : PseudoMetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑f i)
m_set : (t : Set (↑(Set.Iic i) × Ω)) → MeasurableSpace ↑t := fun x ↦ Subtype.instMeasurableSpace
s : Set (↑(Set.Iic i) × Ω) := {p | τ p.2 ≤ ↑i}
hs : MeasurableSet s
h_meas_fst : ∀ (t : Set (↑(Set.Iic i) × Ω)), Measurable fun x ↦ ↑(↑x).1
⊢ Measurable (s.domRestrict fun p ↦ min (↑↑p.1) (τ p.2))
Module: Mathlib.Probability.ConditionalExpectation

Goal state before:
pp: case pos.refine_4
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : μ s < ∞
⊢ IsClosed {f | μ.real s • ∫ (x : Ω), ↑↑↑f x ∂μ = ∫ (x : Ω) in s, ↑↑↑f x ∂μ}

pp: case pos.refine_5
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : μ s < ∞
⊢ ∀ ⦃f g : Ω → E⦄,
    f =ᵐ[μ] g →
      MemLp f 1 μ →
        μ.real s • ∫ (x : Ω), f x ∂μ = ∫ (x : Ω) in s, f x ∂μ → μ.real s • ∫ (x : Ω), g x ∂μ = ∫ (x : Ω) in s, g x ∂μ

Tactic:
·

Goal state after:
case pos.refine_4
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : μ s < ∞
⊢ IsClosed {f | μ.real s • ∫ (x : Ω), ↑↑↑f x ∂μ = ∫ (x : Ω) in s, ↑↑↑f x ∂μ}
Module: Mathlib.Probability.ConditionalExpectation

Goal state before:
pp: case pos.refine_5
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : μ s < ∞
⊢ ∀ ⦃f g : Ω → E⦄,
    f =ᵐ[μ] g →
      MemLp f 1 μ →
        μ.real s • ∫ (x : Ω), f x ∂μ = ∫ (x : Ω) in s, f x ∂μ → μ.real s • ∫ (x : Ω), g x ∂μ = ∫ (x : Ω) in s, g x ∂μ

Tactic:
·

Goal state after:
case pos.refine_5
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : μ s < ∞
⊢ ∀ ⦃f g : Ω → E⦄,
    f =ᵐ[μ] g →
      MemLp f 1 μ →
        μ.real s • ∫ (x : Ω), f x ∂μ = ∫ (x : Ω) in s, f x ∂μ → μ.real s • ∫ (x : Ω), g x ∂μ = ∫ (x : Ω) in s, g x ∂μ
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case refine_2
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁷ : Nonempty ι
τ : Ω → WithTop ι
inst✝⁶ : LinearOrder ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
f : Filtration ι m
inst✝ : PseudoMetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑f i)
m_set : (t : Set (↑(Set.Iic i) × Ω)) → MeasurableSpace ↑t := fun x ↦ Subtype.instMeasurableSpace
s : Set (↑(Set.Iic i) × Ω) := {p | τ p.2 ≤ ↑i}
hs : MeasurableSet s
h_meas_fst : ∀ (t : Set (↑(Set.Iic i) × Ω)), Measurable fun x ↦ ↑(↑x).1
⊢ Measurable (sᶜ.domRestrict fun p ↦ min (↑↑p.1) (τ p.2))

Tactic:
·

Goal state after:
case refine_2
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁷ : Nonempty ι
τ : Ω → WithTop ι
inst✝⁶ : LinearOrder ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
f : Filtration ι m
inst✝ : PseudoMetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑f i)
m_set : (t : Set (↑(Set.Iic i) × Ω)) → MeasurableSpace ↑t := fun x ↦ Subtype.instMeasurableSpace
s : Set (↑(Set.Iic i) × Ω) := {p | τ p.2 ≤ ↑i}
hs : MeasurableSet s
h_meas_fst : ∀ (t : Set (↑(Set.Iic i) × Ω)), Measurable fun x ↦ ↑(↑x).1
⊢ Measurable (sᶜ.domRestrict fun p ↦ min (↑↑p.1) (τ p.2))
Module: Mathlib.Probability.Martingale.BorelCantelli

Goal state before:
pp: case e'_1
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := ⋯
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R
ω : Ω
hω : BddAbove (Set.range fun n ↦ g n ω) ↔ ∃ c, Tendsto (fun n ↦ g n ω) atTop (𝓝 c)
⊢ BddAbove (Set.range fun n ↦ f n ω) ↔ BddAbove (Set.range fun n ↦ g n ω)

pp: case e'_2
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := ⋯
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R
ω : Ω
hω : BddAbove (Set.range fun n ↦ g n ω) ↔ ∃ c, Tendsto (fun n ↦ g n ω) atTop (𝓝 c)
⊢ (∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)) ↔ ∃ c, Tendsto (fun n ↦ g n ω) atTop (𝓝 c)

Tactic:
·

Goal state after:
case e'_1
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := ⋯
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R
ω : Ω
hω : BddAbove (Set.range fun n ↦ g n ω) ↔ ∃ c, Tendsto (fun n ↦ g n ω) atTop (𝓝 c)
⊢ BddAbove (Set.range fun n ↦ f n ω) ↔ BddAbove (Set.range fun n ↦ g n ω)
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: case inl
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
inst✝ : IsZeroOrProbabilityMeasure 0
⊢ centralMoment X 1 0 = 0

pp: case inr
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
⊢ centralMoment X 1 μ = 0

Tactic:
·

Goal state after:
case inl
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
inst✝ : IsZeroOrProbabilityMeasure 0
⊢ centralMoment X 1 0 = 0
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : Integrable X μ
⊢ centralMoment X 1 μ = 0

pp: case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : ¬Integrable X μ
⊢ centralMoment X 1 μ = 0

Tactic:
·

Goal state after:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : Integrable X μ
⊢ centralMoment X 1 μ = 0
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case pos
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁷ : Nonempty ι
τ : Ω → WithTop ι
inst✝⁶ : LinearOrder ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
f : Filtration ι m
inst✝ : PseudoMetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑f i)
m_set : (t : Set (↑(Set.Iic i) × Ω)) → MeasurableSpace ↑t := fun x ↦ Subtype.instMeasurableSpace
s : Set (↑(Set.Iic i) × Ω) := {p | τ p.2 ≤ ↑i}
hs : MeasurableSet s
h_meas_fst : ∀ (t : Set (↑(Set.Iic i) × Ω)), Measurable fun x ↦ ↑(↑x).1
sc : Set (↑(Set.Iic i) × Ω) := sᶜ
ω : ↑sc
hx_fst_le : ↑(↑ω).1 ≤ i
h : τ (↑ω).2 = ⊤
⊢ ↑↑(↑ω).1 ≤ τ (↑ω).2

pp: case neg
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁷ : Nonempty ι
τ : Ω → WithTop ι
inst✝⁶ : LinearOrder ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
f : Filtration ι m
inst✝ : PseudoMetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑f i)
m_set : (t : Set (↑(Set.Iic i) × Ω)) → MeasurableSpace ↑t := fun x ↦ Subtype.instMeasurableSpace
s : Set (↑(Set.Iic i) × Ω) := {p | τ p.2 ≤ ↑i}
hs : MeasurableSet s
h_meas_fst : ∀ (t : Set (↑(Set.Iic i) × Ω)), Measurable fun x ↦ ↑(↑x).1
sc : Set (↑(Set.Iic i) × Ω) := sᶜ
ω : ↑sc
hx_fst_le : ↑(↑ω).1 ≤ i
h : ¬τ (↑ω).2 = ⊤
⊢ ↑↑(↑ω).1 ≤ τ (↑ω).2

Tactic:
·

Goal state after:
case pos
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁷ : Nonempty ι
τ : Ω → WithTop ι
inst✝⁶ : LinearOrder ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
f : Filtration ι m
inst✝ : PseudoMetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑f i)
m_set : (t : Set (↑(Set.Iic i) × Ω)) → MeasurableSpace ↑t := fun x ↦ Subtype.instMeasurableSpace
s : Set (↑(Set.Iic i) × Ω) := {p | τ p.2 ≤ ↑i}
hs : MeasurableSet s
h_meas_fst : ∀ (t : Set (↑(Set.Iic i) × Ω)), Measurable fun x ↦ ↑(↑x).1
sc : Set (↑(Set.Iic i) × Ω) := sᶜ
ω : ↑sc
hx_fst_le : ↑(↑ω).1 ≤ i
h : τ (↑ω).2 = ⊤
⊢ ↑↑(↑ω).1 ≤ τ (↑ω).2
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : ¬Integrable X μ
⊢ centralMoment X 1 μ = 0

Tactic:
·

Goal state after:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : ¬Integrable X μ
⊢ centralMoment X 1 μ = 0
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case neg
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁷ : Nonempty ι
τ : Ω → WithTop ι
inst✝⁶ : LinearOrder ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
f : Filtration ι m
inst✝ : PseudoMetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑f i)
m_set : (t : Set (↑(Set.Iic i) × Ω)) → MeasurableSpace ↑t := fun x ↦ Subtype.instMeasurableSpace
s : Set (↑(Set.Iic i) × Ω) := {p | τ p.2 ≤ ↑i}
hs : MeasurableSet s
h_meas_fst : ∀ (t : Set (↑(Set.Iic i) × Ω)), Measurable fun x ↦ ↑(↑x).1
sc : Set (↑(Set.Iic i) × Ω) := sᶜ
ω : ↑sc
hx_fst_le : ↑(↑ω).1 ≤ i
h : ¬τ (↑ω).2 = ⊤
⊢ ↑↑(↑ω).1 ≤ τ (↑ω).2

Tactic:
·

Goal state after:
case neg
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁷ : Nonempty ι
τ : Ω → WithTop ι
inst✝⁶ : LinearOrder ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
f : Filtration ι m
inst✝ : PseudoMetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑f i)
m_set : (t : Set (↑(Set.Iic i) × Ω)) → MeasurableSpace ↑t := fun x ↦ Subtype.instMeasurableSpace
s : Set (↑(Set.Iic i) × Ω) := {p | τ p.2 ≤ ↑i}
hs : MeasurableSet s
h_meas_fst : ∀ (t : Set (↑(Set.Iic i) × Ω)), Measurable fun x ↦ ↑(↑x).1
sc : Set (↑(Set.Iic i) × Ω) := sᶜ
ω : ↑sc
hx_fst_le : ↑(↑ω).1 ≤ i
h : ¬τ (↑ω).2 = ⊤
⊢ ↑↑(↑ω).1 ≤ τ (↑ω).2
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case coe.inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁸ : Nonempty ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst✝⁷ : LinearOrder ι
inst✝⁶ : MeasurableSpace ι
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : OrderTopology ι
inst✝³ : SecondCountableTopology ι
inst✝² : BorelSpace ι
inst✝¹ : TopologicalSpace β
f : Filtration ι m
inst✝ : PseudoMetrizableSpace ι
h : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
h_meas : IsStronglyProgressive f fun i ω ↦ (min (↑i) (τ ω)).untopA
i : ι
ω : Ω
t : ι
h_it : i ≤ t
⊢ (min ↑i ↑t).untopA ≤ i

pp: case coe.inr
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁸ : Nonempty ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst✝⁷ : LinearOrder ι
inst✝⁶ : MeasurableSpace ι
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : OrderTopology ι
inst✝³ : SecondCountableTopology ι
inst✝² : BorelSpace ι
inst✝¹ : TopologicalSpace β
f : Filtration ι m
inst✝ : PseudoMetrizableSpace ι
h : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
h_meas : IsStronglyProgressive f fun i ω ↦ (min (↑i) (τ ω)).untopA
i : ι
ω : Ω
t : ι
h_ti : t ≤ i
⊢ (min ↑i ↑t).untopA ≤ i

Tactic:
·

Goal state after:
case coe.inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁸ : Nonempty ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst✝⁷ : LinearOrder ι
inst✝⁶ : MeasurableSpace ι
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : OrderTopology ι
inst✝³ : SecondCountableTopology ι
inst✝² : BorelSpace ι
inst✝¹ : TopologicalSpace β
f : Filtration ι m
inst✝ : PseudoMetrizableSpace ι
h : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
h_meas : IsStronglyProgressive f fun i ω ↦ (min (↑i) (τ ω)).untopA
i : ι
ω : Ω
t : ι
h_it : i ≤ t
⊢ (min ↑i ↑t).untopA ≤ i
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case coe.inr
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁸ : Nonempty ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst✝⁷ : LinearOrder ι
inst✝⁶ : MeasurableSpace ι
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : OrderTopology ι
inst✝³ : SecondCountableTopology ι
inst✝² : BorelSpace ι
inst✝¹ : TopologicalSpace β
f : Filtration ι m
inst✝ : PseudoMetrizableSpace ι
h : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
h_meas : IsStronglyProgressive f fun i ω ↦ (min (↑i) (τ ω)).untopA
i : ι
ω : Ω
t : ι
h_ti : t ≤ i
⊢ (min ↑i ↑t).untopA ≤ i

Tactic:
·

Goal state after:
case coe.inr
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁸ : Nonempty ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst✝⁷ : LinearOrder ι
inst✝⁶ : MeasurableSpace ι
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : OrderTopology ι
inst✝³ : SecondCountableTopology ι
inst✝² : BorelSpace ι
inst✝¹ : TopologicalSpace β
f : Filtration ι m
inst✝ : PseudoMetrizableSpace ι
h : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
h_meas : IsStronglyProgressive f fun i ω ↦ (min (↑i) (τ ω)).untopA
i : ι
ω : Ω
t : ι
h_ti : t ≤ i
⊢ (min ↑i ↑t).untopA ≤ i
Module: Mathlib.Probability.Martingale.BorelCantelli

Goal state before:
pp: case e'_1.refine_1
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := fun n ω ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R
ω : Ω
hω : BddAbove (Set.range fun n ↦ g n ω) ↔ ∃ c, Tendsto (fun n ↦ g n ω) atTop (𝓝 c)
b : ℝ
hb : b ∈ upperBounds (Set.range fun n ↦ f n ω)
n : ℕ
⊢ (fun n ↦ g n ω) n ≤ b + |f 0 ω|

pp: case e'_1.refine_2
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := fun n ω ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R
ω : Ω
hω : BddAbove (Set.range fun n ↦ g n ω) ↔ ∃ c, Tendsto (fun n ↦ g n ω) atTop (𝓝 c)
b : ℝ
hb : b ∈ upperBounds (Set.range fun n ↦ g n ω)
n : ℕ
⊢ (fun n ↦ f n ω) n ≤ b + |f 0 ω|

Tactic:
·

Goal state after:
case e'_1.refine_1
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := fun n ω ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R
ω : Ω
hω : BddAbove (Set.range fun n ↦ g n ω) ↔ ∃ c, Tendsto (fun n ↦ g n ω) atTop (𝓝 c)
b : ℝ
hb : b ∈ upperBounds (Set.range fun n ↦ f n ω)
n : ℕ
⊢ (fun n ↦ g n ω) n ≤ b + |f 0 ω|
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
c : ℝ
⊢ log (μ.real Set.univ) + log (rexp (t * c)) = log (μ.real Set.univ) + t * c

pp: Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
c : ℝ
⊢ μ.real Set.univ ≠ 0

Tactic:
·

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
c : ℝ
⊢ log (μ.real Set.univ) + log (rexp (t * c)) = log (μ.real Set.univ) + t * c
Module: Mathlib.Probability.BorelCantelli

Goal state before:
pp: case refine_1
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : ∑' (n : ℕ), μ (s n) = ∞
this✝ : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), μ[(s (n + 1)).indicator 1 | ↑(filtrationOfSet hsm) n] ω = (fun x ↦ μ.real (s (n + 1))) ω
ω : Ω
hω : ∀ (n : ℕ), μ[(s (n + 1)).indicator 1 | ↑(filtrationOfSet hsm) n] ω = μ.real (s (n + 1))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, ↑x < ∑ k ∈ Finset.range a, μ (s (k + 1))
⊢ Monotone fun n ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1))

pp: case refine_2
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : ∑' (n : ℕ), μ (s n) = ∞
this✝ : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), μ[(s (n + 1)).indicator 1 | ↑(filtrationOfSet hsm) n] ω = (fun x ↦ μ.real (s (n + 1))) ω
ω : Ω
hω : ∀ (n : ℕ), μ[(s (n + 1)).indicator 1 | ↑(filtrationOfSet hsm) n] ω = μ.real (s (n + 1))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, ↑x < ∑ k ∈ Finset.range a, μ (s (k + 1))
⊢ ¬BddAbove (Set.range fun n ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1)))

Tactic:
·

Goal state after:
case refine_1
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : ∑' (n : ℕ), μ (s n) = ∞
this✝ : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), μ[(s (n + 1)).indicator 1 | ↑(filtrationOfSet hsm) n] ω = (fun x ↦ μ.real (s (n + 1))) ω
ω : Ω
hω : ∀ (n : ℕ), μ[(s (n + 1)).indicator 1 | ↑(filtrationOfSet hsm) n] ω = μ.real (s (n + 1))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, ↑x < ∑ k ∈ Finset.range a, μ (s (k + 1))
⊢ Monotone fun n ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1))
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
c : ℝ
⊢ μ.real Set.univ ≠ 0

Tactic:
·

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
c : ℝ
⊢ μ.real Set.univ ≠ 0