mathlib-initiative/mathlib-tactics huggingface dataset:
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 < ∞
u v : Ω → E
huv : u =ᵐ[μ] v
a✝ : MemLp u 1 μ
hueq : μ.real s • ∫ (x : Ω), u x ∂μ = ∫ (x : Ω) in s, u x ∂μ
⊢ μ.real s • ∫ (a : Ω), u a ∂μ = ∫ (x : Ω) in s, u x ∂μ

pp: Ω : 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 < ∞
u v : Ω → E
huv : u =ᵐ[μ] v
a✝ : MemLp u 1 μ
hueq : μ.real s • ∫ (x : Ω), u x ∂μ = ∫ (x : Ω) in s, u x ∂μ
⊢ ∀ᵐ (x : Ω) ∂μ, x ∈ s → u x = v 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 < ∞
u v : Ω → E
huv : u =ᵐ[μ] v
a✝ : MemLp u 1 μ
hueq : μ.real s • ∫ (x : Ω), u x ∂μ = ∫ (x : Ω) in s, u x ∂μ
⊢ μ.real s • ∫ (a : Ω), u a ∂μ = ∫ (x : Ω) in s, u x ∂μ

Ω : 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 < ∞
u v : Ω → E
huv : u =ᵐ[μ] v
a✝ : MemLp u 1 μ
hueq : μ.real s • ∫ (x : Ω), u x ∂μ = ∫ (x : Ω) in s, u x ∂μ
⊢ ∀ᵐ (x : Ω) ∂μ, x ∈ s → u x = v x
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h_int : Integrable X μ
⊢ ∫ (a : Ω), X a ∂μ - ∫ (a : Ω), ∫ (x : Ω), X x ∂μ ∂μ = (1 - μ.real Set.univ) * ∫ (x : Ω), X x ∂μ

Tactic:
]

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h_int : Integrable X μ
⊢ ∫ (a : Ω), X a ∂μ - ∫ (a : Ω), ∫ (x : Ω), X x ∂μ ∂μ = (1 - μ.real Set.univ) * ∫ (x : Ω), X 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
sc : Set (↑(Set.Iic i) × Ω) := sᶜ
ω : ↑sc
⊢ ↑↑(↑ω).1 = ↑↑(↑ω).1

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
sc : Set (↑(Set.Iic i) × Ω) := sᶜ
ω : ↑sc
⊢ ↑↑(↑ω).1 ≤ τ (↑ω).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
sc : Set (↑(Set.Iic i) × Ω) := sᶜ
ω : ↑sc
⊢ ↑↑(↑ω).1 ≤ τ (↑ω).2
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 μ
⊢ (1 - μ.real Set.univ) * ∫ (x : Ω), X x ∂μ = 0

Tactic:
]

Goal state after:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : Integrable X μ
⊢ (1 - μ.real Set.univ) * ∫ (x : Ω), X x ∂μ = 0
Module: Mathlib.Probability.BorelCantelli

Goal state before:
pp: Ω : 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))
⊢ Tendsto (fun n ↦ ∑ k ∈ Finset.range n, μ (s (k + 1))) atTop (𝓝 (∑' (n : ℕ), μ (s (n + 1))))

Tactic:
]

Goal state after:
Ω : 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))
⊢ Tendsto (fun n ↦ ∑ k ∈ Finset.range n, μ (s (k + 1))) atTop (𝓝 (∑' (n : ℕ), μ (s (n + 1))))
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : ¬Integrable X μ
h_sub : Integrable (fun x ↦ X x - integral μ X) μ
h_add : X = (fun x ↦ X x - integral μ X) + fun x ↦ integral μ X
⊢ Integrable ((fun x ↦ X x - integral μ X) + fun x ↦ integral μ X) μ

Tactic:
]

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : ¬Integrable X μ
h_sub : Integrable (fun x ↦ X x - integral μ X) μ
h_add : X = (fun x ↦ X x - integral μ X) + fun x ↦ integral μ X
⊢ Integrable ((fun x ↦ X x - integral μ X) + fun x ↦ integral μ X) μ
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 μ
this : ¬Integrable (fun x ↦ X x - integral μ X) μ
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Probability.BorelCantelli

Goal state before:
pp: Ω : 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))
⊢ Tendsto (fun n ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1))) atTop atTop

Tactic:
]

Goal state after:
Ω : 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))
⊢ Tendsto (fun n ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1))) atTop atTop
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

Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
c : ℝ
⊢ μ.real Set.univ ≠ 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) + t * c = log (μ.real Set.univ) + t * c

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Moments.Basic

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

Tactic:
Measure.measure_univ_eq_zero

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
c : ℝ
⊢ ¬μ = 0
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
c : ℝ
⊢ ¬μ = 0

Tactic:
]

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
c : ℝ
⊢ ¬μ = 0
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : 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
h : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ ↑n
hτ_le' : ∀ (ω : Ω), (τ ω).untopA ≤ n
this : stoppedValue u τ = (fun p ↦ u (↑p.1) p.2) ∘ fun ω ↦ (⟨(τ ω).untopA, ⋯⟩, ω)
⊢ StronglyMeasurable ((fun p ↦ u (↑p.1) p.2) ∘ fun ω ↦ (⟨(τ ω).untopA, ⋯⟩, ω))

Tactic:
]

Goal state after:
Ω : 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
h : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ ↑n
hτ_le' : ∀ (ω : Ω), (τ ω).untopA ≤ n
this : stoppedValue u τ = (fun p ↦ u (↑p.1) p.2) ∘ fun ω ↦ (⟨(τ ω).untopA, ⋯⟩, ω)
⊢ StronglyMeasurable ((fun p ↦ u (↑p.1) p.2) ∘ fun ω ↦ (⟨(τ ω).untopA, ⋯⟩, ω))
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))
n : ℕ
⊢ 0 ≤ μ.real (s (n + 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))
n : ℕ
⊢ 0 ≤ μ.real (s (n + 1))
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : 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 β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
hf_prog : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
t : Set β
ht : MeasurableSet t
i : ι
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun ω ↦ min (τ ω) ↑i)
this : stoppedValue u τ ⁻¹' t ∩ {ω | τ ω ≤ ↑i} = (stoppedValue u fun ω ↦ min (τ ω) ↑i) ⁻¹' t ∩ {ω | τ ω ≤ ↑i}
⊢ MeasurableSet ((stoppedValue u fun ω ↦ min (τ ω) ↑i) ⁻¹' t ∩ {ω | τ ω ≤ ↑i})

Tactic:
]

Goal state after:
Ω : 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 β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
hf_prog : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
t : Set β
ht : MeasurableSet t
i : ι
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun ω ↦ min (τ ω) ↑i)
this : stoppedValue u τ ⁻¹' t ∩ {ω | τ ω ≤ ↑i} = (stoppedValue u fun ω ↦ min (τ ω) ↑i) ⁻¹' t ∩ {ω | τ ω ≤ ↑i}
⊢ MeasurableSet ((stoppedValue u fun ω ↦ min (τ ω) ↑i) ⁻¹' t ∩ {ω | τ ω ≤ ↑i})
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (fun ω ↦ rexp (t * X ω)) μ
this : ∫ (x : Ω), rexp (t * X x) ∂μ = ∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ
⊢ 0 < μ ((Function.support fun x ↦ rexp (t * X x)) ∩ Set.univ)

pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (fun ω ↦ rexp (t * X ω)) μ
this : ∫ (x : Ω), rexp (t * X x) ∂μ = ∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ
⊢ 0 ≤ᵐ[μ.restrict Set.univ] fun x ↦ rexp (t * X x)

pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (fun ω ↦ rexp (t * X ω)) μ
this : ∫ (x : Ω), rexp (t * X x) ∂μ = ∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ
⊢ IntegrableOn (fun x ↦ rexp (t * X x)) Set.univ μ

Tactic:
]

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (fun ω ↦ rexp (t * X ω)) μ
this : ∫ (x : Ω), rexp (t * X x) ∂μ = ∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ
⊢ 0 < μ ((Function.support fun x ↦ rexp (t * X x)) ∩ Set.univ)

Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (fun ω ↦ rexp (t * X ω)) μ
this : ∫ (x : Ω), rexp (t * X x) ∂μ = ∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ
⊢ 0 ≤ᵐ[μ.restrict Set.univ] fun x ↦ rexp (t * X x)

Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (fun ω ↦ rexp (t * X ω)) μ
this : ∫ (x : Ω), rexp (t * X x) ∂μ = ∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ
⊢ IntegrableOn (fun x ↦ rexp (t * X x)) Set.univ μ
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (fun ω ↦ rexp (t * X ω)) μ
this : ∫ (x : Ω), rexp (t * X x) ∂μ = ∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ
h_eq_univ : (Function.support fun x ↦ rexp (t * X x)) = Set.univ
⊢ 0 < μ Set.univ

Tactic:
]

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (fun ω ↦ rexp (t * X ω)) μ
this : ∫ (x : Ω), rexp (t * X x) ∂μ = ∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ
h_eq_univ : (Function.support fun x ↦ rexp (t * X x)) = Set.univ
⊢ 0 < μ Set.univ
Module: Mathlib.Probability.BorelCantelli

Goal state before:
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))
B : ℝ
hB : ∀ x ∈ Set.range fun n ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1)), x ≤ B
n : ℕ
⊢ ¬↑B.toNNReal < ∑ k ∈ Finset.range n, μ (s (k + 1))

Tactic:
]

Goal state after:
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))
B : ℝ
hB : ∀ x ∈ Set.range fun n ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1)), x ≤ B
n : ℕ
⊢ ¬↑B.toNNReal < ∑ k ∈ Finset.range n, μ (s (k + 1))
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (fun ω ↦ rexp (t * X ω)) μ
this : ∫ (x : Ω), rexp (t * X x) ∂μ = ∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ
x : Ω
⊢ 0 ≤ rexp (t * X x)

Tactic:
]

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (fun ω ↦ rexp (t * X ω)) μ
this : ∫ (x : Ω), rexp (t * X x) ∂μ = ∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ
x : Ω
⊢ 0 ≤ rexp (t * X x)
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (fun ω ↦ rexp (t * X ω)) μ
this : ∫ (x : Ω), rexp (t * X x) ∂μ = ∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ
⊢ Integrable (fun x ↦ rexp (t * X x)) μ

Tactic:
]

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (fun ω ↦ rexp (t * X ω)) μ
this : ∫ (x : Ω), rexp (t * X x) ∂μ = ∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ
⊢ Integrable (fun x ↦ rexp (t * X x)) μ
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : NeZero μ
hX : Integrable (fun ω ↦ rexp (t * X ω)) μ
⊢ mgf X μ t = mgf X μ t

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : 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 β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
hf_prog : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
t : Set β
ht : MeasurableSet t
i : ι
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun ω ↦ min (τ ω) ↑i)
ω : Ω
h : τ ω ≤ ↑i
⊢ u (τ ω).untopA ω ∈ t ↔ u (τ ω).untopA ω ∈ t

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
t : ℝ
⊢ mgf X μ t = mgf X μ t

pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
t : ℝ
⊢ AEStronglyMeasurable (fun ω ↦ rexp (t * id ω)) (Measure.map X μ)

Tactic:
]

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
t : ℝ
⊢ AEStronglyMeasurable (fun ω ↦ rexp (t * id ω)) (Measure.map X μ)
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
h : X =ᵐ[μ] Y
ω : Ω
hω : X ω = Y ω
⊢ rexp (t * Y ω) = rexp (t * Y ω)

Tactic:
]

Goal state after:
Module: Mathlib.Probability.BorelCantelli

Goal state before:
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))
B : ℝ
hB : ∀ x ∈ Set.range fun n ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1)), x ≤ B
n : ℕ
⊢ (fun n ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1))) n = ∑ a ∈ Finset.range n, (μ (s (a + 1))).toReal

Tactic:
]

Goal state after:
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))
B : ℝ
hB : ∀ x ∈ Set.range fun n ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1)), x ≤ B
n : ℕ
⊢ (fun n ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1))) n = ∑ a ∈ Finset.range n, (μ (s (a + 1))).toReal
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : 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 β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
hf_prog : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun ω ↦ min (τ ω) ↑i)
t : Set β
ht : MeasurableSet t
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
ω : Ω
⊢ stoppedValue u τ ω ∈ t → (∃ x, τ ω ≤ ↑(seq x)) ∨ τ ω = ⊤

Tactic:
]

Goal state after:
Ω : 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 β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
hf_prog : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun ω ↦ min (τ ω) ↑i)
t : Set β
ht : MeasurableSet t
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
ω : Ω
⊢ stoppedValue u τ ω ∈ t → (∃ x, τ ω ≤ ↑(seq x)) ∨ τ ω = ⊤
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
μ' : Measure Ω'
Y : Ω' → ℝ
h : IdentDistrib X Y μ μ'
⊢ mgf id (Measure.map Y μ') = mgf id (Measure.map Y μ')

Tactic:
]

Goal state after: